aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml481
-rw-r--r--interp/constrarg.ml34
-rw-r--r--interp/stdarg.ml10
-rw-r--r--lib/genarg.ml16
-rw-r--r--lib/genarg.mli6
-rw-r--r--plugins/decl_mode/g_decl_mode.ml42
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--tactics/extratactics.ml44
-rw-r--r--tactics/g_rewrite.ml42
-rw-r--r--tactics/taccoerce.ml4
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tauto.ml2
-rw-r--r--toplevel/g_obligations.ml42
13 files changed, 38 insertions, 129 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index be4097f13..46c68ecc3 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -48,82 +48,6 @@ let has_extraarg l =
in
List.exists check l
-let rec is_possibly_empty = function
-| Uopt _ -> true
-| Ulist0 _ -> true
-| Ulist0sep _ -> true
-| Umodifiers _ -> true
-| Ulist1 t -> is_possibly_empty t
-| Ulist1sep (t, _) -> is_possibly_empty t
-| _ -> false
-
-let rec get_empty_entry = function
-| Uopt _ -> <:expr< None >>
-| Ulist0 _ -> <:expr< [] >>
-| Ulist0sep _ -> <:expr< [] >>
-| Umodifiers _ -> <:expr< [] >>
-| Ulist1 t -> <:expr< [$get_empty_entry t$] >>
-| Ulist1sep (t, _) -> <:expr< [$get_empty_entry t$] >>
-| _ -> assert false
-
-let statically_known_possibly_empty s (prods,_) =
- List.for_all (function
- | ExtNonTerminal(t, e, _) ->
- begin match t with
- | ExtraArgType s' ->
- (* For ExtraArg we don't know (we'll have to test dynamically) *)
- (* unless it is a recursive call *)
- s <> s'
- | _ ->
- is_possibly_empty e
- end
- | ExtTerminal _ ->
- (* This consumes a token for sure *) false)
- prods
-
-let possibly_empty_subentries loc (prods,act) =
- let bind_name s v e =
- <:expr< let $lid:s$ = $v$ in $e$ >>
- in
- let rec aux = function
- | [] -> <:expr< let loc = $default_loc$ in let _ = loc in $act$ >>
- | ExtNonTerminal(_, e, s) :: tl when is_possibly_empty e ->
- bind_name s (get_empty_entry e) (aux tl)
- | ExtNonTerminal(t, _, s) :: tl ->
- let t = match t with
- | ExtraArgType _ as t -> t
- | _ -> assert false
- in
- (* We check at runtime if extraarg s parses "epsilon" *)
- <:expr< let $lid:s$ = match Genarg.default_empty_value $make_wit loc t$ with
- [ None -> raise Exit
- | Some v -> v ] in $aux tl$ >>
- | _ -> assert false (* already filtered out *) in
- if has_extraarg prods then
- (* Needs a dynamic check; catch all exceptions if ever some rhs raises *)
- (* an exception rather than returning a value; *)
- (* declares loc because some code can refer to it; *)
- (* ensures loc is used to avoid "unused variable" warning *)
- (true, <:expr< try Some $aux prods$
- with [ Exit -> None ] >>)
- else
- (* Static optimisation *)
- (false, aux prods)
-
-let make_possibly_empty_subentries loc s cl =
- let cl = List.filter (statically_known_possibly_empty s) cl in
- if cl = [] then
- <:expr< None >>
- else
- let rec aux = function
- | (true, e) :: l ->
- <:expr< match $e$ with [ Some v -> Some v | None -> $aux l$ ] >>
- | (false, e) :: _ ->
- <:expr< Some $e$ >>
- | [] ->
- <:expr< None >> in
- aux (List.map (possibly_empty_subentries loc) cl)
-
let make_act loc act pil =
let rec make = function
| [] -> <:expr< (fun loc -> $act$) >>
@@ -214,12 +138,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
let wit = <:expr< $lid:"wit_"^s$ >> in
let rawwit = <:expr< Genarg.rawwit $wit$ >> in
let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
- let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in
declare_str_items loc
[ <:str_item<
value ($lid:"wit_"^s$) =
let dyn = $dyn$ in
- Genarg.make0 ?dyn $default_value$ $se$ >>;
+ Genarg.make0 ?dyn $se$ >>;
<:str_item< Genintern.register_intern0 $wit$ $glob$ >>;
<:str_item< Genintern.register_subst0 $wit$ $subst$ >>;
<:str_item< Geninterp.register_interp0 $wit$ $interp$ >>;
@@ -245,7 +168,7 @@ let declare_vernac_argument loc s pr cl =
declare_str_items loc
[ <:str_item<
value ($lid:"wit_"^s$ : Genarg.genarg_type 'a unit unit) =
- Genarg.create_arg None $se$ >>;
+ Genarg.create_arg $se$ >>;
<:str_item<
value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
<:str_item< do {
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index a48d68375..ead4e3969 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -20,48 +20,48 @@ let loc_of_or_by_notation f = function
| ByNotation (loc,s,_) -> loc
let wit_int_or_var =
- Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var"
+ Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var"
let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type =
- Genarg.make0 None "intropattern"
+ Genarg.make0 "intropattern"
let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
- Genarg.make0 None "tactic"
+ Genarg.make0 "tactic"
let wit_ident =
- Genarg.make0 None "ident"
+ Genarg.make0 "ident"
let wit_var =
- Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) None "var"
+ Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) "var"
-let wit_ref = Genarg.make0 None "ref"
+let wit_ref = Genarg.make0 "ref"
-let wit_quant_hyp = Genarg.make0 None "quant_hyp"
+let wit_quant_hyp = Genarg.make0 "quant_hyp"
let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
- Genarg.make0 None "sort"
+ Genarg.make0 "sort"
let wit_constr =
- Genarg.make0 None "constr"
+ Genarg.make0 "constr"
let wit_constr_may_eval =
- Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval"
+ Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval"
-let wit_uconstr = Genarg.make0 None "uconstr"
+let wit_uconstr = Genarg.make0 "uconstr"
-let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr"
+let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr"
-let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings"
+let wit_constr_with_bindings = Genarg.make0 "constr_with_bindings"
-let wit_bindings = Genarg.make0 None "bindings"
+let wit_bindings = Genarg.make0 "bindings"
let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type =
- Genarg.make0 None "hyp_location_flag"
+ Genarg.make0 "hyp_location_flag"
-let wit_red_expr = Genarg.make0 None "redexpr"
+let wit_red_expr = Genarg.make0 "redexpr"
let wit_clause_dft_concl =
- Genarg.make0 None "clause_dft_concl"
+ Genarg.make0 "clause_dft_concl"
(** Register location *)
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 9c3ed9413..56b995e53 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -9,19 +9,19 @@
open Genarg
let wit_unit : unit uniform_genarg_type =
- make0 None "unit"
+ make0 "unit"
let wit_bool : bool uniform_genarg_type =
- make0 None "bool"
+ make0 "bool"
let wit_int : int uniform_genarg_type =
- make0 None "int"
+ make0 "int"
let wit_string : string uniform_genarg_type =
- make0 None "string"
+ make0 "string"
let wit_pre_ident : string uniform_genarg_type =
- make0 None "preident"
+ make0 "preident"
let () = register_name0 wit_unit "Stdarg.wit_unit"
let () = register_name0 wit_bool "Stdarg.wit_bool"
diff --git a/lib/genarg.ml b/lib/genarg.ml
index c7273ac93..7aada461f 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -246,7 +246,6 @@ struct
end
type ('raw, 'glb, 'top) load = {
- nil : 'raw option;
dyn : 'top Val.tag;
}
@@ -254,30 +253,19 @@ module LoadMap = ArgMap(struct type ('r, 'g, 't) t = ('r, 'g, 't) load end)
let arg0_map = ref LoadMap.empty
-let create_arg opt ?dyn name =
+let create_arg ?dyn name =
match ArgT.name name with
| Some _ ->
Errors.anomaly (str "generic argument already declared: " ++ str name)
| None ->
let dyn = match dyn with None -> Val.Base (ValT.create name) | Some dyn -> dyn in
- let obj = LoadMap.Pack { nil = opt; dyn; } in
+ let obj = LoadMap.Pack { dyn; } in
let name = ArgT.create name in
let () = arg0_map := LoadMap.add name obj !arg0_map in
ExtraArg name
let make0 = create_arg
-let rec default_empty_value : type a b c. (a, b, c) genarg_type -> a option = function
-| ListArg _ -> Some []
-| OptArg _ -> Some None
-| PairArg (t1, t2) ->
- begin match default_empty_value t1, default_empty_value t2 with
- | Some v1, Some v2 -> Some (v1, v2)
- | _ -> None
- end
-| ExtraArg s ->
- match LoadMap.find s !arg0_map with LoadMap.Pack obj -> obj.nil
-
let rec val_tag : type a b c. (a, b, c) genarg_type -> c Val.tag = function
| ListArg t -> Val.List (val_tag t)
| OptArg t -> Val.Opt (val_tag t)
diff --git a/lib/genarg.mli b/lib/genarg.mli
index ce0536cf4..d509649f2 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -110,11 +110,11 @@ end
type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
(** Alias for concision when the three types agree. *)
-val make0 : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val make0 : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
(** Create a new generic type of argument: force to associate
unique ML types at each of the three levels. *)
-val create_arg : 'raw option -> ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
+val create_arg : ?dyn:'top Val.tag -> string -> ('raw, 'glob, 'top) genarg_type
(** Alias for [make0]. *)
(** {5 Specialized types} *)
@@ -250,8 +250,6 @@ val wit_pair : ('a1, 'b1, 'c1) genarg_type -> ('a2, 'b2, 'c2) genarg_type ->
(** {5 Magic used by the parser} *)
-val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
-
val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit
(** Used by the extension to give a name to types. The string should be the
absolute path of the argument witness, e.g.
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index b62cfd6ad..2d096a108 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -87,7 +87,7 @@ let vernac_proof_instr instr =
(* Only declared at raw level, because only used in vernac commands. *)
let wit_proof_instr : (raw_proof_instr, glob_proof_instr, proof_instr) Genarg.genarg_type =
- Genarg.make0 None "proof_instr"
+ Genarg.make0 "proof_instr"
(* We create a new parser entry [proof_mode]. The Declarative proof mode
will replace the normal parser entry for tactics with this one. *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 97b9e95e1..61ada5cc8 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -146,7 +146,7 @@ module Tactic = Pcoq.Tactic
type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genarg.uniform_genarg_type) =
- Genarg.create_arg None "function_rec_definition_loc"
+ Genarg.create_arg "function_rec_definition_loc"
let function_rec_definition_loc =
Pcoq.create_generic_entry "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 85b9d6a08..ae8b83b95 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -931,9 +931,9 @@ type cmp =
type 'i test =
| Test of cmp * 'i * 'i
-let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 None "cmp"
+let wit_cmp : (cmp,cmp,cmp) Genarg.genarg_type = Genarg.make0 "cmp"
let wit_test : (int or_var test,int or_var test,int test) Genarg.genarg_type =
- Genarg.make0 None "tactest"
+ Genarg.make0 "tactest"
let pr_cmp = function
| Eq -> Pp.str"="
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4
index 6b6dc7b21..8b012aa88 100644
--- a/tactics/g_rewrite.ml4
+++ b/tactics/g_rewrite.ml4
@@ -184,7 +184,7 @@ END
type binders_argtype = local_binder list
let wit_binders =
- (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type)
+ (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
let binders = Pcoq.create_generic_entry "binders" (Genarg.rawwit wit_binders)
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 0cd3e0944..358f6d646 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -18,11 +18,11 @@ open Constrarg
exception CannotCoerceTo of string
let (wit_constr_context : (Empty.t, Empty.t, constr) Genarg.genarg_type) =
- Genarg.create_arg None "constr_context"
+ Genarg.create_arg "constr_context"
(* includes idents known to be bound and references *)
let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) =
- Genarg.create_arg None "constr_under_binders"
+ Genarg.create_arg "constr_under_binders"
let has_type : type a. Val.t -> a typed_abstract_argument_type -> bool = fun v wit ->
let Val.Dyn (t, _) = v in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 32f7c3c61..36faba113 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -109,7 +109,7 @@ type tacvalue =
| VRec of value Id.Map.t ref * glob_tactic_expr
let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
- Genarg.create_arg None "tacvalue"
+ Genarg.create_arg "tacvalue"
let of_tacvalue v = in_gen (topwit wit_tacvalue) v
let to_tacvalue v = out_gen (topwit wit_tacvalue) v
diff --git a/tactics/tauto.ml b/tactics/tauto.ml
index d3e0b1f44..a86fdb98a 100644
--- a/tactics/tauto.ml
+++ b/tactics/tauto.ml
@@ -55,7 +55,7 @@ type tauto_flags = {
}
let wit_tauto_flags : tauto_flags uniform_genarg_type =
- Genarg.create_arg None "tauto_flags"
+ Genarg.create_arg "tauto_flags"
let assoc_flags ist =
let v = Id.Map.find (Names.Id.of_string "tauto_flags") ist.lfun in
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index d620febbc..32ccf21d2 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -32,7 +32,7 @@ let sigref = mkRefC (Qualid (Loc.ghost, Libnames.qualid_of_string "Coq.Init.Spec
type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type
let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
- Genarg.create_arg None "withtac"
+ Genarg.create_arg "withtac"
let withtac = Pcoq.create_generic_entry "withtac" (Genarg.rawwit wit_withtac)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 19:28:39 +0000