diff options
| -rw-r--r-- | grammar/argextend.ml4 | 4 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 4 | ||||
| -rw-r--r-- | interp/constrarg.ml | 12 | ||||
| -rw-r--r-- | lib/genarg.ml | 12 | ||||
| -rw-r--r-- | lib/genarg.mli | 4 | ||||
| -rw-r--r-- | printing/pptactic.ml | 40 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 19 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 51 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 19 |
9 files changed, 54 insertions, 111 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 08651de64..a49291d94 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -33,14 +33,10 @@ let rec make_wit loc = function | IntOrVarArgType -> <:expr< Constrarg.wit_int_or_var >> | IdentArgType -> <:expr< Constrarg.wit_ident >> | VarArgType -> <:expr< Constrarg.wit_var >> - | QuantHypArgType -> <:expr< Constrarg.wit_quant_hyp >> | GenArgType -> <:expr< Constrarg.wit_genarg >> | ConstrArgType -> <:expr< Constrarg.wit_constr >> | ConstrMayEvalArgType -> <:expr< Constrarg.wit_constr_may_eval >> - | RedExprArgType -> <:expr< Constrarg.wit_red_expr >> | OpenConstrArgType -> <:expr< Constrarg.wit_open_constr >> - | ConstrWithBindingsArgType -> <:expr< Constrarg.wit_constr_with_bindings >> - | BindingsArgType -> <:expr< Constrarg.wit_bindings >> | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> | PairArgType (t1,t2) -> diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index dd97107f7..be438b54a 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -226,11 +226,7 @@ let rec mlexpr_of_argtype loc = function | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >> | Genarg.IdentArgType -> <:expr< Genarg.IdentArgType >> | Genarg.VarArgType -> <:expr< Genarg.VarArgType >> - | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >> | Genarg.OpenConstrArgType -> <:expr< Genarg.OpenConstrArgType >> - | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >> - | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >> - | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >> | Genarg.GenArgType -> <:expr< Genarg.GenArgType >> | Genarg.ConstrArgType -> <:expr< Genarg.ConstrArgType >> | Genarg.ConstrMayEvalArgType -> <:expr< Genarg.ConstrMayEvalArgType >> diff --git a/interp/constrarg.ml b/interp/constrarg.ml index a7241399e..a67143b00 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -36,7 +36,7 @@ let wit_var = unsafe_of_type VarArgType let wit_ref = Genarg.make0 None "ref" -let wit_quant_hyp = unsafe_of_type QuantHypArgType +let wit_quant_hyp = Genarg.make0 None "quant_hyp" let wit_genarg = unsafe_of_type GenArgType @@ -51,14 +51,14 @@ let wit_uconstr = Genarg.make0 None "uconstr" let wit_open_constr = unsafe_of_type OpenConstrArgType -let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType +let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings" -let wit_bindings = unsafe_of_type BindingsArgType +let wit_bindings = Genarg.make0 None "bindings" let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = Genarg.make0 None "hyp_location_flag" -let wit_red_expr = unsafe_of_type RedExprArgType +let wit_red_expr = Genarg.make0 None "redexpr" let wit_clause_dft_concl = Genarg.make0 None "clause_dft_concl" @@ -71,4 +71,8 @@ let () = register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; register_name0 wit_uconstr "Constrarg.wit_uconstr"; + 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"; + register_name0 wit_bindings "Constrarg.wit_bindings"; + register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings"; diff --git a/lib/genarg.ml b/lib/genarg.ml index 149d872c5..8712eda8e 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -18,11 +18,7 @@ type argument_type = | GenArgType | ConstrArgType | ConstrMayEvalArgType - | QuantHypArgType | OpenConstrArgType - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type @@ -35,11 +31,7 @@ let rec argument_type_eq arg1 arg2 = match arg1, arg2 with | GenArgType, GenArgType -> true | ConstrArgType, ConstrArgType -> true | ConstrMayEvalArgType, ConstrMayEvalArgType -> true -| QuantHypArgType, QuantHypArgType -> true | OpenConstrArgType, OpenConstrArgType -> true -| ConstrWithBindingsArgType, ConstrWithBindingsArgType -> true -| BindingsArgType, BindingsArgType -> true -| RedExprArgType, RedExprArgType -> true | ListArgType arg1, ListArgType arg2 -> argument_type_eq arg1 arg2 | OptArgType arg1, OptArgType arg2 -> argument_type_eq arg1 arg2 | PairArgType (arg1l, arg1r), PairArgType (arg2l, arg2r) -> @@ -54,11 +46,7 @@ let rec pr_argument_type = function | GenArgType -> str "genarg" | ConstrArgType -> str "constr" | ConstrMayEvalArgType -> str "constr_may_eval" -| QuantHypArgType -> str "qhyp" | OpenConstrArgType -> str "open_constr" -| ConstrWithBindingsArgType -> str "constr_with_bindings" -| BindingsArgType -> str "bindings" -| RedExprArgType -> str "redexp" | ListArgType t -> pr_argument_type t ++ spc () ++ str "list" | OptArgType t -> pr_argument_type t ++ spc () ++ str "opt" | PairArgType (t1, t2) -> diff --git a/lib/genarg.mli b/lib/genarg.mli index 3a18581d7..2dcaa789f 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -190,11 +190,7 @@ type argument_type = | GenArgType | ConstrArgType | ConstrMayEvalArgType - | QuantHypArgType | OpenConstrArgType - | ConstrWithBindingsArgType - | BindingsArgType - | RedExprArgType | ListArgType of argument_type | OptArgType of argument_type | PairArgType of argument_type * argument_type diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 97917d2c7..dfb8837ec 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -275,15 +275,7 @@ module Make | ConstrMayEvalArgType -> pr_may_eval prc prlc (pr_or_by_notation prref) prpat (out_gen (rawwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat) - (out_gen (rawwit wit_red_expr) x) | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in @@ -320,17 +312,7 @@ module Make pr_may_eval prc prlc (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat (out_gen (glbwit wit_constr_may_eval) x) - | QuantHypArgType -> - pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr - (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat) - (out_gen (glbwit wit_red_expr) x) | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x) | ListArgType _ -> let list_unpacker wit l = let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in @@ -363,16 +345,7 @@ module Make | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x) | ConstrArgType -> prc (out_gen (topwit wit_constr) x) | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x) - | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x) - | RedExprArgType -> - pr_red_expr (prc,prlc,pr_evaluable_reference,prpat) - (out_gen (topwit wit_red_expr) x) | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x)) - | ConstrWithBindingsArgType -> - let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in - pr_with_bindings prc prlc (c,b) - | BindingsArgType -> - pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it | ListArgType _ -> let list_unpacker wit l = let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in @@ -1461,6 +1434,19 @@ let () = (fun (c,_) -> Printer.pr_glob_constr c) Printer.pr_closed_glob ; + Genprint.register_print0 Constrarg.wit_red_expr + (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) + (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) + (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern)); + Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + Genprint.register_print0 Constrarg.wit_bindings + (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_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)) + (fun { Evd.it = it } -> pr_with_bindings pr_constr pr_lconstr it); Genprint.register_print0 Stdarg.wit_int int int int; Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index b5a363371..ac1229f2f 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -739,16 +739,8 @@ and intern_genarg ist x = map_raw wit_constr intern_constr ist x | ConstrMayEvalArgType -> map_raw wit_constr_may_eval intern_constr_may_eval ist x - | QuantHypArgType -> - map_raw wit_quant_hyp intern_quantified_hypothesis ist x - | RedExprArgType -> - map_raw wit_red_expr intern_red_expr ist x | OpenConstrArgType -> map_raw wit_open_constr (fun ist -> on_snd (intern_constr ist)) ist x - | ConstrWithBindingsArgType -> - map_raw wit_constr_with_bindings intern_constr_with_bindings ist x - | BindingsArgType -> - map_raw wit_bindings intern_bindings ist x | ListArgType _ -> let list_unpacker wit l = let map x = @@ -848,10 +840,13 @@ let () = let () = 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)) - -let () = - Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)) + Genintern.register_intern0 wit_sort (fun ist s -> (ist, s)); + Genintern.register_intern0 wit_quant_hyp (lift intern_quantified_hypothesis); + Genintern.register_intern0 wit_uconstr (fun ist c -> (ist,intern_constr ist c)); + 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); + () (***************************************************************************) (* Backwarding recursive needs of tactic glob/interp/eval functions *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b2afba4af..6ac16bd76 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1209,9 +1209,6 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAlias (loc,s,l) -> let body = Tacenv.interp_alias s in let rec f x = match genarg_tag x with - | QuantHypArgType | RedExprArgType - | ConstrWithBindingsArgType - | BindingsArgType | ConstrArgType | ListArgType ConstrArgType | OptArgType _ | PairArgType _ -> (** generic handler *) @@ -1630,29 +1627,12 @@ and interp_genarg ist env sigma concl gl x = let (sigma,c_interp) = interp_constr_may_eval ist env !evdref (out_gen (glbwit wit_constr_may_eval) x) in evdref := sigma; in_gen (topwit wit_constr_may_eval) c_interp - | QuantHypArgType -> - in_gen (topwit wit_quant_hyp) - (interp_declared_or_quantified_hypothesis ist env sigma - (out_gen (glbwit wit_quant_hyp) x)) - | RedExprArgType -> - let (sigma,r_interp) = - interp_red_expr ist env !evdref (out_gen (glbwit wit_red_expr) x) - in - evdref := sigma; - in_gen (topwit wit_red_expr) r_interp | OpenConstrArgType -> let expected_type = WithoutTypeConstraint in in_gen (topwit wit_open_constr) (interp_open_constr ~expected_type ist env !evdref (snd (out_gen (glbwit wit_open_constr) x))) - | ConstrWithBindingsArgType -> - in_gen (topwit wit_constr_with_bindings) - (pack_sigma (interp_constr_with_bindings ist env !evdref - (out_gen (glbwit wit_constr_with_bindings) x))) - | BindingsArgType -> - in_gen (topwit wit_bindings) - (pack_sigma (interp_bindings ist env !evdref (out_gen (glbwit wit_bindings) x))) | ListArgType ConstrArgType -> let (sigma,v) = interp_genarg_constr_list ist env !evdref x in evdref := sigma; @@ -2314,15 +2294,27 @@ let () = let () = declare_uniform wit_pre_ident +let lift f = (); fun ist gl x -> (project gl, f ist (pf_env gl) (project gl) x) +let lifts f = (); fun ist gl x -> f ist (pf_env gl) (project gl) x + +let interp_bindings' ist gl bl = + let (sigma, bl) = interp_bindings ist (pf_env gl) (project gl) bl in + (project gl, pack_sigma (sigma, bl)) + +let interp_constr_with_bindings' ist gl c = + let (sigma, c) = interp_constr_with_bindings ist (pf_env gl) (project gl) c in + (project gl, pack_sigma (sigma, c)) + let () = - let interp ist gl ref = (project gl, interp_reference ist (pf_env gl) (project gl) ref) in - Geninterp.register_interp0 wit_ref interp; - let interp ist gl pat = interp_intro_pattern ist (pf_env gl) (project gl) pat in - Geninterp.register_interp0 wit_intro_pattern interp; - let interp ist gl pat = (project gl, interp_clause ist (pf_env gl) (project gl) pat) in - Geninterp.register_interp0 wit_clause_dft_concl interp; - let interp ist gl s = interp_sort (project gl) s in - Geninterp.register_interp0 wit_sort interp + 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); + Geninterp.register_interp0 wit_sort (lifts (fun _ _ evd s -> interp_sort evd s)); + Geninterp.register_interp0 wit_tacvalue (fun ist gl c -> project gl, c); + 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' let () = let interp ist gl tac = @@ -2336,9 +2328,6 @@ let () = project gl , interp_uconstr ist (pf_env gl) c ) -let () = - Geninterp.register_interp0 wit_tacvalue (fun ist gl c -> project gl, c) - (***************************************************************************) (* Other entry points *) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index f5b6c3250..6d32aa81b 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -289,21 +289,9 @@ and subst_genarg subst (x:glob_generic_argument) = 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)) - | QuantHypArgType -> - in_gen (glbwit wit_quant_hyp) - (subst_declared_or_quantified_hypothesis subst - (out_gen (glbwit wit_quant_hyp) x)) - | RedExprArgType -> - in_gen (glbwit wit_red_expr) (subst_redexp subst (out_gen (glbwit wit_red_expr) x)) | OpenConstrArgType -> in_gen (glbwit wit_open_constr) ((),subst_glob_constr subst (snd (out_gen (glbwit wit_open_constr) x))) - | ConstrWithBindingsArgType -> - in_gen (glbwit wit_constr_with_bindings) - (subst_glob_with_bindings subst (out_gen (glbwit wit_constr_with_bindings) x)) - | BindingsArgType -> - in_gen (glbwit wit_bindings) - (subst_bindings subst (out_gen (glbwit wit_bindings) x)) | ListArgType _ -> let list_unpacker wit l = let map x = @@ -340,4 +328,9 @@ let () = Genintern.register_subst0 wit_tactic subst_tactic; Genintern.register_subst0 wit_sort (fun _ v -> v); Genintern.register_subst0 wit_clause_dft_concl (fun _ v -> v); - Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c) + Genintern.register_subst0 wit_uconstr (fun subst c -> subst_glob_constr subst c); + Genintern.register_subst0 wit_red_expr subst_redexp; + 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; + () |