aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml42
-rw-r--r--grammar/q_coqast.ml42
-rw-r--r--interp/constrarg.ml8
-rw-r--r--interp/stdarg.ml4
-rw-r--r--lib/genarg.ml14
-rw-r--r--lib/genarg.mli2
-rw-r--r--printing/pptactic.ml18
-rw-r--r--tactics/tacintern.ml5
-rw-r--r--tactics/tacinterp.ml26
-rw-r--r--tactics/tacsubst.ml5
10 files changed, 25 insertions, 61 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 842f59809..b9336ce33 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -30,11 +30,9 @@ let mk_extraarg loc s =
<:expr< $lid:"wit_"^s$ >>
let rec make_wit loc = function
- | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >>
| IdentArgType -> <:expr< Constrarg.wit_ident >>
| VarArgType -> <:expr< Constrarg.wit_var >>
| ConstrArgType -> <:expr< Constrarg.wit_constr >>
- | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >>
| OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >>
| ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >>
| OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >>
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3088e0365..7001f5f62 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -223,12 +223,10 @@ let mlexpr_of_red_expr = function
<:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
let rec mlexpr_of_argtype loc = function
- | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
| Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >>
| Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
| Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >>
| Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >>
- | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >>
| Genarg.ListArgType t -> <:expr< Genarg.ListArgType $mlexpr_of_argtype loc t$ >>
| Genarg.OptArgType t -> <:expr< Genarg.OptArgType $mlexpr_of_argtype loc t$ >>
| Genarg.PairArgType (t1,t2) ->
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 84b056ab6..ab54b6197 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -22,7 +22,8 @@ let loc_of_or_by_notation f = function
let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type =
Obj.magic t
-let wit_int_or_var = unsafe_of_type IntOrVarArgType
+let wit_int_or_var =
+ Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "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"
@@ -43,7 +44,8 @@ let wit_sort : (glob_sort, glob_sort, sorts) genarg_type =
let wit_constr = unsafe_of_type ConstrArgType
-let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType
+let wit_constr_may_eval =
+ Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval"
let wit_uconstr = Genarg.make0 None "uconstr"
@@ -64,11 +66,13 @@ let wit_clause_dft_concl =
(** Register location *)
let () =
+ register_name0 wit_int_or_var "Constrarg.wit_int_or_var";
register_name0 wit_ref "Constrarg.wit_ref";
register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
register_name0 wit_tactic "Constrarg.wit_tactic";
register_name0 wit_sort "Constrarg.wit_sort";
register_name0 wit_uconstr "Constrarg.wit_uconstr";
+ register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval";
register_name0 wit_red_expr "Constrarg.wit_red_expr";
register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 5cfe3854a..e155a5217 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -15,9 +15,7 @@ let wit_bool : bool uniform_genarg_type =
make0 None "bool"
let wit_int : int uniform_genarg_type =
- make0 ~dyn:(val_tag (Obj.magic IntOrVarArgType)) None "int"
-(** FIXME: IntOrVarArgType is hardwired, but that definition should be the other
- way around. *)
+ make0 None "int"
let wit_string : string uniform_genarg_type =
make0 None "string"
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 3989cf6df..11a042117 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -13,12 +13,10 @@ module Val = Dyn.Make(struct end)
type argument_type =
(* Basic types *)
- | IntOrVarArgType
| IdentArgType
| VarArgType
(* Specific types *)
| ConstrArgType
- | ConstrMayEvalArgType
| OpenConstrArgType
| ListArgType of argument_type
| OptArgType of argument_type
@@ -26,11 +24,9 @@ type argument_type =
| ExtraArgType of string
let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
-| IntOrVarArgType, IntOrVarArgType -> true
| IdentArgType, IdentArgType -> true
| VarArgType, VarArgType -> true
| ConstrArgType, ConstrArgType -> true
-| ConstrMayEvalArgType, ConstrMayEvalArgType -> true
| OpenConstrArgType, OpenConstrArgType -> true
| ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2
| OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2
@@ -40,11 +36,9 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
| _ -> false
let rec pr_argument_type = function
-| IntOrVarArgType -> str "int_or_var"
| IdentArgType -> str "ident"
| VarArgType -> str "var"
| ConstrArgType -> str "constr"
-| ConstrMayEvalArgType -> str "constr_may_eval"
| OpenConstrArgType -> str "open_constr"
| ListArgType t -> pr_argument_type t ++ spc () ++ str "list"
| OptArgType t -> pr_argument_type t ++ spc () ++ str "opt"
@@ -168,7 +162,6 @@ let default_empty_value t =
| None -> None
(** Beware: keep in sync with the corresponding types *)
-let int_or_var_T = Val.create "int"
let ident_T = Val.create "ident"
let genarg_T = Val.create "genarg"
let constr_T = Val.create "constr"
@@ -179,13 +172,10 @@ let list_val = Val.create "list"
let pair_val = Val.create "pair"
let val_tag = function
-| IntOrVarArgType -> cast_tag int_or_var_T
| IdentArgType -> cast_tag ident_T
| VarArgType -> cast_tag ident_T
(** Must ensure that toplevel types of Var and Ident agree! *)
| ConstrArgType -> cast_tag constr_T
-| ConstrMayEvalArgType -> cast_tag constr_T
- (** Must ensure that toplevel types of Constr and ConstrMayEval agree! *)
| OpenConstrArgType -> cast_tag open_constr_T
| ExtraArgType s -> Obj.magic (String.Map.find s !arg0_map).dyn
(** Recursive types have no associated dynamic tag *)
@@ -207,9 +197,9 @@ let try_prj wit v = match prj (val_tag wit) v with
let rec val_cast : type a. a typed_abstract_argument_type -> Val.t -> a =
fun wit v -> match unquote wit with
-| IntOrVarArgType | IdentArgType
+| IdentArgType
| VarArgType
-| ConstrArgType | ConstrMayEvalArgType
+| ConstrArgType
| OpenConstrArgType | ExtraArgType _ -> try_prj wit v
| ListArgType t ->
let v = match prj list_val v with
diff --git a/lib/genarg.mli b/lib/genarg.mli
index 89ea49ddb..83ba1dd04 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -201,12 +201,10 @@ val pair_val : (Val.t * Val.t) Val.tag
type argument_type =
(** Basic types *)
- | IntOrVarArgType
| IdentArgType
| VarArgType
(** Specific types *)
| ConstrArgType
- | ConstrMayEvalArgType
| OpenConstrArgType
| ListArgType of argument_type
| OptArgType of argument_type
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 94cbc54e9..9c6da350f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -267,13 +267,9 @@ module Make
let rec pr_raw_generic_rec prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
| ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
- | ConstrMayEvalArgType ->
- pr_may_eval prc prlc (pr_or_by_notation prref) prpat
- (out_gen (rawwit wit_constr_may_eval) x)
| OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
@@ -302,14 +298,9 @@ module Make
let rec pr_glb_generic_rec prc prlc prtac prpat x =
match Genarg.genarg_tag x with
- | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
| VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
| ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
- | ConstrMayEvalArgType ->
- pr_may_eval prc prlc
- (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
- (out_gen (glbwit wit_constr_may_eval) x)
| OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
@@ -337,11 +328,9 @@ module Make
let rec pr_top_generic_rec prc prlc prtac prpat x =
match Genarg.genarg_tag x with
- | IntOrVarArgType -> int (out_gen (topwit wit_int_or_var) x)
| IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
| VarArgType -> pr_id (out_gen (topwit wit_var) x)
| ConstrArgType -> prc (out_gen (topwit wit_constr) x)
- | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
| OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
| ListArgType _ ->
let list_unpacker wit l =
@@ -1432,6 +1421,8 @@ let () =
let pr_bool b = if b then str "true" else str "false" in
let pr_unit _ = str "()" in
let pr_string s = str "\"" ++ str s ++ str "\"" in
+ Genprint.register_print0 Constrarg.wit_int_or_var
+ (pr_or_var int) (pr_or_var int) int;
Genprint.register_print0 Constrarg.wit_ref
pr_reference (pr_or_var (pr_located pr_global)) pr_global;
Genprint.register_print0
@@ -1462,6 +1453,11 @@ let () =
(pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
(pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
(fun { Evd.it = it } -> pr_bindings_no_with pr_constr pr_lconstr it);
+ Genprint.register_print0 Constrarg.wit_constr_may_eval
+ (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr)
+ (pr_may_eval (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)
+ (pr_or_var (pr_and_short_name pr_evaluable_reference)) (pr_pat_and_constr_expr pr_glob_constr))
+ pr_constr;
Genprint.register_print0 Constrarg.wit_constr_with_bindings
(pr_with_bindings pr_constr_expr pr_lconstr_expr)
(pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d0f83836d..5e725e182 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -727,7 +727,6 @@ and intern_match_rule onlytac ist = function
and intern_genarg ist x =
match genarg_tag x with
- | IntOrVarArgType -> map_raw wit_int_or_var intern_int_or_var ist x
| IdentArgType ->
let lf = ref Id.Set.empty in
map_raw wit_ident (intern_ident lf) ist x
@@ -735,8 +734,6 @@ and intern_genarg ist x =
map_raw wit_var intern_hyp ist x
| ConstrArgType ->
map_raw wit_constr intern_constr ist x
- | ConstrMayEvalArgType ->
- map_raw wit_constr_may_eval intern_constr_may_eval ist x
| OpenConstrArgType ->
map_raw wit_open_constr (fun ist -> on_snd (intern_constr ist)) ist x
| ListArgType _ ->
@@ -836,6 +833,7 @@ let () =
Genintern.register_intern0 wit_clause_dft_concl intern_clause
let () =
+ Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
Genintern.register_intern0 wit_ref (lift intern_global_reference);
Genintern.register_intern0 wit_tactic (lift intern_tactic_or_tacarg);
Genintern.register_intern0 wit_sort (fun ist s -> (ist, s));
@@ -844,6 +842,7 @@ let () =
Genintern.register_intern0 wit_red_expr (lift intern_red_expr);
Genintern.register_intern0 wit_bindings (lift intern_bindings);
Genintern.register_intern0 wit_constr_with_bindings (lift intern_constr_with_bindings);
+ Genintern.register_intern0 wit_constr_may_eval (lift intern_constr_may_eval);
()
(***************************************************************************)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5a6834ab5..37d9f1825 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1259,8 +1259,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
match tag with
- | IntOrVarArgType ->
- Ftactic.return (mk_int_or_var_value ist (Genarg.out_gen (glbwit wit_int_or_var) x))
| IdentArgType ->
Ftactic.return (value_of_ident (interp_ident ist env sigma
(Genarg.out_gen (glbwit wit_ident) x)))
@@ -1270,20 +1268,10 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let (sigma,v) =
Tacmach.New.of_old (fun gl -> mk_open_constr_value ist gl (snd (Genarg.out_gen (glbwit wit_open_constr) x))) gl in
Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
- | ConstrMayEvalArgType ->
- let (sigma,c_interp) =
- interp_constr_may_eval ist env sigma
- (Genarg.out_gen (glbwit wit_constr_may_eval) x)
- in
- Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
| ListArgType VarArgType ->
let wit = glbwit (wit_list wit_var) in
let ans = List.map (mk_hyp_value ist env sigma) (Genarg.out_gen wit x) in
Ftactic.return (Value.of_list ans)
- | ListArgType IntOrVarArgType ->
- let wit = glbwit (wit_list wit_int_or_var) in
- let ans = List.map (mk_int_or_var_value ist) (Genarg.out_gen wit x) in
- Ftactic.return (Value.of_list ans)
| ListArgType IdentArgType ->
let wit = glbwit (wit_list wit_ident) in
let mk_ident x = value_of_ident (interp_ident ist env sigma x) in
@@ -1638,9 +1626,6 @@ and interp_genarg ist env sigma concl gl x =
let evdref = ref sigma in
let rec interp_genarg x =
match genarg_tag x with
- | IntOrVarArgType ->
- in_gen (topwit wit_int_or_var)
- (interp_int_or_var ist (Genarg.out_gen (glbwit wit_int_or_var) x))
| IdentArgType ->
in_gen (topwit wit_ident)
(interp_ident ist env sigma (Genarg.out_gen (glbwit wit_ident) x))
@@ -1652,10 +1637,6 @@ and interp_genarg ist env sigma concl gl x =
in
evdref := sigma;
in_gen (topwit wit_constr) c_interp
- | ConstrMayEvalArgType ->
- let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (Genarg.out_gen (glbwit wit_constr_may_eval) x) in
- evdref := sigma;
- in_gen (topwit wit_constr_may_eval) c_interp
| OpenConstrArgType ->
let expected_type = WithoutTypeConstraint in
in_gen (topwit wit_open_constr)
@@ -1703,7 +1684,7 @@ and interp_genarg ist env sigma concl gl x =
and global_genarg =
let rec global_tag = function
- | IntOrVarArgType -> true
+ | ExtraArgType "int_or_var" -> true (** FIXME *)
| ListArgType t | OptArgType t -> global_tag t
| PairArgType (t1,t2) -> global_tag t1 && global_tag t2
| _ -> false
@@ -2335,6 +2316,7 @@ let interp_constr_with_bindings' ist gl c =
(project gl, pack_sigma (sigma, c))
let () =
+ Geninterp.register_interp0 wit_int_or_var (fun ist gl n -> project gl, interp_int_or_var ist n);
Geninterp.register_interp0 wit_ref (lift interp_reference);
Geninterp.register_interp0 wit_intro_pattern (lifts interp_intro_pattern);
Geninterp.register_interp0 wit_clause_dft_concl (lift interp_clause);
@@ -2343,7 +2325,9 @@ let () =
Geninterp.register_interp0 wit_red_expr (lifts interp_red_expr);
Geninterp.register_interp0 wit_quant_hyp (lift interp_declared_or_quantified_hypothesis);
Geninterp.register_interp0 wit_bindings interp_bindings';
- Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings'
+ Geninterp.register_interp0 wit_constr_with_bindings interp_constr_with_bindings';
+ Geninterp.register_interp0 wit_constr_may_eval (lifts interp_constr_may_eval);
+ ()
let () =
let interp ist gl tac =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 2884e318b..0c9665362 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -280,14 +280,11 @@ and subst_match_rule subst = function
and subst_genarg subst (x:glob_generic_argument) =
match genarg_tag x with
- | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x)
| IdentArgType ->
in_gen (glbwit wit_ident) (out_gen (glbwit wit_ident) x)
| VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
| ConstrArgType ->
in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
- | ConstrMayEvalArgType ->
- in_gen (glbwit wit_constr_may_eval) (subst_raw_may_eval subst (out_gen (glbwit wit_constr_may_eval) x))
| OpenConstrArgType ->
in_gen (glbwit wit_open_constr)
((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x)))
@@ -322,6 +319,7 @@ and subst_genarg subst (x:glob_generic_argument) =
(** Registering *)
let () =
+ Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
Genintern.register_subst0 wit_ref subst_global_reference;
Genintern.register_subst0 wit_intro_pattern (fun _ v -> v);
Genintern.register_subst0 wit_tactic subst_tactic;
@@ -332,4 +330,5 @@ let () =
Genintern.register_subst0 wit_quant_hyp subst_declared_or_quantified_hypothesis;
Genintern.register_subst0 wit_bindings subst_bindings;
Genintern.register_subst0 wit_constr_with_bindings subst_glob_with_bindings;
+ Genintern.register_subst0 wit_constr_may_eval subst_raw_may_eval;
()
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 01:35:06 +0000