diff options
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/argextend.ml4 | 91 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 6 | ||||
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 6 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 | ||||
| -rw-r--r-- | parsing/ppconstr.ml | 10 | ||||
| -rw-r--r-- | parsing/ppconstr.mli | 3 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 305 | ||||
| -rw-r--r-- | parsing/pptactic.mli | 68 | ||||
| -rw-r--r-- | parsing/q_coqast.ml4 | 10 | ||||
| -rw-r--r-- | parsing/search.ml | 5 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 59 | ||||
| -rw-r--r-- | parsing/vernacextend.ml4 | 24 |
14 files changed, 363 insertions, 232 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index 4d6edda0e..0f4bc93a8 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -40,6 +40,29 @@ let rec make_rawwit loc = function <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >> | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >> +let rec make_globwit loc = function + | BoolArgType -> <:expr< Genarg.globwit_bool >> + | IntArgType -> <:expr< Genarg.globwit_int >> + | IntOrVarArgType -> <:expr< Genarg.globwit_int_or_var >> + | StringArgType -> <:expr< Genarg.globwit_string >> + | PreIdentArgType -> <:expr< Genarg.globwit_pre_ident >> + | IdentArgType -> <:expr< Genarg.globwit_ident >> + | RefArgType -> <:expr< Genarg.globwit_ref >> + | QuantHypArgType -> <:expr< Genarg.globwit_quant_hyp >> + | SortArgType -> <:expr< Genarg.globwit_sort >> + | ConstrArgType -> <:expr< Genarg.globwit_constr >> + | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >> + | TacticArgType -> <:expr< Genarg.globwit_tactic >> + | RedExprArgType -> <:expr< Genarg.globwit_red_expr >> + | CastedOpenConstrArgType -> <:expr< Genarg.globwit_casted_open_constr >> + | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >> + | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >> + | List1ArgType t -> <:expr< Genarg.wit_list1 $make_globwit loc t$ >> + | OptArgType t -> <:expr< Genarg.wit_opt $make_globwit loc t$ >> + | PairArgType (t1,t2) -> + <:expr< Genarg.wit_pair $make_globwit loc t1$ $make_globwit loc t2$ >> + | ExtraArgType s -> <:expr< $lid:"globwit_"^s$ >> + let rec make_wit loc = function | BoolArgType -> <:expr< Genarg.wit_bool >> | IntArgType -> <:expr< Genarg.wit_int >> @@ -78,33 +101,57 @@ let make_rule loc (prods,act) = let (symbs,pil) = List.split prods in <:expr< ($mlexpr_of_list (fun x -> x) symbs$,$make_act loc act pil$) >> -let declare_tactic_argument for_v8 loc s typ pr f rawtyppr cl = +let declare_tactic_argument for_v8 loc s typ pr f g h rawtyppr globtyppr cl = let interp = match f with - | None -> <:expr< Tacinterp.genarg_interp >> + | None -> <:expr< Tacinterp.interp_genarg >> + | Some f -> <:expr< $lid:f$>> in + let glob = match g with + | None -> <:expr< Tacinterp.intern_genarg >> + | Some f -> <:expr< $lid:f$>> in + let substitute = match h with + | None -> <:expr< Tacinterp.subst_genarg >> | Some f -> <:expr< $lid:f$>> in let rawtyp, rawpr = match rawtyppr with | None -> typ,pr | Some (t,p) -> t,p in + let globtyp, globpr = match globtyppr with + | None -> typ,pr + | Some (t,p) -> t,p in let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in let rawwit = <:expr< $lid:"rawwit_"^s$ >> in + let globwit = <:expr< $lid:"globwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< declare - value ($lid:"wit_"^s$, $lid:"rawwit_"^s$) = Genarg.create_arg $se$; + value ($lid:"wit_"^s$, $lid:"globwit_"^s$, $lid:"rawwit_"^s$) = + Genarg.create_arg $se$; value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; - Tacinterp.add_genarg_interp $se$ + Tacinterp.add_interp_genarg $se$ + ((fun e x -> + (in_gen $globwit$ + (out_gen $make_globwit loc typ$ + ($glob$ e + (in_gen $make_rawwit loc rawtyp$ + (out_gen $rawwit$ x)))))), (fun ist gl x -> (in_gen $wit$ (out_gen $make_wit loc typ$ ($interp$ ist gl - (in_gen $make_rawwit loc rawtyp$ - (out_gen $rawwit$ x)))))); + (in_gen $make_globwit loc rawtyp$ + (out_gen $globwit$ x)))))), + (fun subst x -> + (in_gen $globwit$ + (out_gen $make_globwit loc typ$ + ($substitute$ subst + (in_gen $make_globwit loc rawtyp$ + (out_gen $globwit$ x))))))); Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None [(None, None, $rules$)]; Pptactic.declare_extra_genarg_pprule $mlexpr_of_bool for_v8$ ($rawwit$, $lid:rawpr$) + ($globwit$, $lid:globpr$) ($wit$, $lid:pr$); end >> @@ -112,12 +159,11 @@ let declare_tactic_argument for_v8 loc s typ pr f rawtyppr cl = let declare_vernac_argument for_v8 loc s cl = let se = mlexpr_of_string s in let typ = ExtraArgType s in - let wit = <:expr< $lid:"wit_"^s$ >> in let rawwit = <:expr< $lid:"rawwit_"^s$ >> in let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in <:str_item< declare - value $lid:"rawwit_"^s$ = snd (Genarg.create_arg $se$); + value $lid:"rawwit_"^s$ = let (_,_,x) = Genarg.create_arg $se$ in x; value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$; Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.Entry.e 'a) None [(None, None, $rules$)]; @@ -167,14 +213,20 @@ EXTEND "TYPED"; "AS"; typ = argtype; "PRINTED"; "BY"; pr = LIDENT; f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; + g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; + h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; rawtyppr = - OPT [ "RAW"; "TYPED"; "AS"; t = argtype; - "RAW"; "PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + (* Necessary if the globalized type is different from the final type *) + OPT [ "RAW_TYPED"; "AS"; t = argtype; + "RAW_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + globtyppr = + OPT [ "GLOB_TYPED"; "AS"; t = argtype; + "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> if String.capitalize s = s then failwith "Argument entry names must be lowercase"; - declare_tactic_argument true loc s typ pr f rawtyppr l + declare_tactic_argument true loc s typ pr f g h rawtyppr globtyppr l | "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> @@ -185,14 +237,19 @@ EXTEND "TYPED"; "AS"; typ = argtype; "PRINTED"; "BY"; pr = LIDENT; f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ]; + g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ]; + h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ]; rawtyppr = - OPT [ "RAW"; "TYPED"; "AS"; t = argtype; - "RAW"; "PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + OPT [ "GLOB_TYPED"; "AS"; t = argtype; + "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; + globtyppr = + OPT [ "GLOB_TYPED"; "AS"; t = argtype; + "GLOB_PRINTED"; "BY"; pr = LIDENT -> (t,pr) ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> if String.capitalize s = s then failwith "Argument entry names must be lowercase"; - declare_tactic_argument false loc s typ pr f rawtyppr l + declare_tactic_argument false loc s typ pr f g h rawtyppr globtyppr l | "V7"; "VERNAC"; "ARGUMENT"; "EXTEND"; s = [ UIDENT | LIDENT ]; OPT "|"; l = LIST1 argrule SEP "|"; "END" -> @@ -201,7 +258,11 @@ EXTEND declare_vernac_argument false loc s l ] ] ; argtype: - [ [ e = LIDENT -> fst (interp_entry_name loc e) ] ] + [ [ e = LIDENT -> fst (interp_entry_name loc e) + | e1 = LIDENT; "*"; e2 = LIDENT -> + let e1 = fst (interp_entry_name loc e1) in + let e2 = fst (interp_entry_name loc e2) in + PairArgType (e1, e2) ] ] ; argrule: [ [ "["; l = LIST0 genarg; "]"; "->"; "["; e = Pcaml.expr; "]" -> (l,e) ] ] diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index d05827bfe..f5309fa39 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -31,7 +31,7 @@ open Q type let_clause_kind = | LETTOPCLAUSE of Names.identifier * constr_expr | LETCLAUSE of - (Names.identifier Util.located * constr_expr may_eval option * raw_tactic_arg) + (Names.identifier Util.located * (constr_expr, Libnames.reference Genarg.or_metanum) may_eval option * raw_tactic_arg) ifdef Quotify then module Prelude = struct @@ -62,7 +62,7 @@ open Prelude let arg_of_expr = function TacArg a -> a - | e -> Tacexp e + | e -> Tacexp (e:raw_tactic_expr) (* Tactics grammar rules *) @@ -230,7 +230,7 @@ GEXTEND Gram | n = integer -> Integer n | id = METAIDENT -> MetaIdArg (loc,id) | "?" -> ConstrMayEval (ConstrTerm (CHole loc)) - | "?"; n = natural -> MetaNumArg (loc,n) + | "?"; n = natural -> ConstrMayEval (ConstrTerm (CMeta (loc,n))) | "'"; c = Constr.constr -> ConstrMayEval (ConstrTerm c) ] ] ; diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index 2caad4680..945009ae9 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -31,7 +31,7 @@ open Q type let_clause_kind = | LETTOPCLAUSE of Names.identifier * constr_expr | LETCLAUSE of - (Names.identifier Util.located * constr_expr may_eval option * raw_tactic_arg) + (Names.identifier Util.located * (constr_expr, Libnames.reference Genarg.or_metanum) may_eval option * raw_tactic_arg) ifdef Quotify then module Prelude = struct @@ -60,7 +60,7 @@ end let arg_of_expr = function TacArg a -> a - | e -> Tacexp e + | e -> Tacexp (e:raw_tactic_expr) open Prelude @@ -136,7 +136,7 @@ GEXTEND Gram tactic_atom: [ [ id = METAIDENT -> MetaIdArg (loc,id) | r = reference -> Reference r - | "?"; n = natural -> MetaNumArg (loc,n) + | "?"; n = natural -> ConstrMayEval (ConstrTerm (CMeta (loc,n))) | "()" -> TacVoid ] ] ; input_fun: diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 787ccd07e..862bbd3dd 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -14,6 +14,7 @@ open Pcoq open Util open Tacexpr open Rawterm +open Genarg (* open grammar entries, possibly in quotified form *) ifdef Quotify then open Qast @@ -83,8 +84,8 @@ GEXTEND Gram ; (* Either an hypothesis or a ltac ref (variable or pattern metavariable) *) id_or_ltac_ref: - [ [ id = base_ident -> AN id - | "?"; n = natural -> MetaNum (loc,n) ] ] + [ [ id = base_ident -> Genarg.AN id + | "?"; n = natural -> Genarg.MetaNum (loc,n) ] ] ; (* Either a global ref or a ltac ref (variable or pattern metavariable) *) global_or_ltac_ref: diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4 index dade80611..725a3432f 100644 --- a/parsing/g_tacticnew.ml4 +++ b/parsing/g_tacticnew.ml4 @@ -14,6 +14,7 @@ open Pcoq open Util open Tacexpr open Rawterm +open Genarg let tactic_kw = [ "->"; "<-" ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 325d4f494..8558c2d2f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -151,7 +151,7 @@ module Tactic : open Rawterm val castedopenconstr : constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e - val constrarg : constr_expr may_eval Gram.Entry.e + val constrarg : (constr_expr,reference or_metanum) may_eval Gram.Entry.e val quantified_hypothesis : quantified_hypothesis Gram.Entry.e val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index 97c7d637b..d716e773b 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -312,10 +312,6 @@ open Genarg let pr_occurrences prc (nl,c) = prlist (fun n -> int n ++ spc ()) nl ++ prc c -let pr_metanum pr = function - | AN x -> pr x - | MetaNum (_,n) -> str "?" ++ int n - let pr_red_expr (pr_constr,pr_ref) = function | Red false -> str "Red" | Hnf -> str "Hnf" @@ -337,10 +333,10 @@ let pr_red_expr (pr_constr,pr_ref) = function | ExtraRedExpr (s,c) -> hov 1 (str s ++ pr_arg pr_constr c) -let rec pr_may_eval pr = function +let rec pr_may_eval pr pr2 = function | ConstrEval (r,c) -> hov 0 - (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr_metanum pr_reference) r ++ + (str "Eval" ++ brk (1,1) ++ pr_red_expr (pr,pr2) r ++ spc () ++ str "in" ++ brk (1,1) ++ pr c) | ConstrContext ((_,id),c) -> hov 0 @@ -348,3 +344,5 @@ let rec pr_may_eval pr = function str "[" ++ pr c ++ str "]") | ConstrTypeOf c -> hov 0 (str "Check " ++ brk (1,1) ++ pr c) | ConstrTerm c -> pr c + +let pr_rawconstr c = pr_constr (Constrextern.extern_rawconstr Idset.empty c) diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli index 6dd3d842c..ffb0146ae 100644 --- a/parsing/ppconstr.mli +++ b/parsing/ppconstr.mli @@ -37,4 +37,5 @@ val pr_sort : rawsort -> std_ppcmds val pr_pattern : Tacexpr.pattern_expr -> std_ppcmds val pr_constr : constr_expr -> std_ppcmds val pr_cases_pattern : cases_pattern_expr -> std_ppcmds -val pr_may_eval : ('a -> std_ppcmds) -> 'a may_eval -> std_ppcmds +val pr_may_eval : ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> ('a,'b) may_eval -> std_ppcmds +val pr_rawconstr : rawconstr -> std_ppcmds diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1bdd90d38..3c894dd84 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -31,42 +31,58 @@ let pr_occurrences = Ppconstr.pr_occurrences let prtac_tab_v7 = Hashtbl.create 17 let prtac_tab = Hashtbl.create 17 -let declare_extra_tactic_pprule for_v8 s f g = - Hashtbl.add prtac_tab_v7 s (f,g); - if for_v8 then Hashtbl.add prtac_tab s (f,g) +(* We need system F typing strength *) +type ('a,'b) gen_gram_prod_builder = + ('a,'b) generic_argument list -> + string * Egrammar.grammar_tactic_production list +let inst1 (f:('a,'b) gen_gram_prod_builder) = + (Obj.magic f : (constr_expr,raw_tactic_expr) gen_gram_prod_builder) +let inst2 (f:('a,'b) gen_gram_prod_builder) = + (Obj.magic f : (rawconstr * constr_expr option,glob_tactic_expr) gen_gram_prod_builder) +let inst3 (f:('a,'b) gen_gram_prod_builder) = + (Obj.magic f : (Term.constr,glob_tactic_expr) gen_gram_prod_builder) + +let declare_extra_tactic_pprule for_v8 s f = + let f = inst1 f in + let g = inst2 f in + let h = inst3 f in + Hashtbl.add prtac_tab_v7 s (f,g,h); + if for_v8 then Hashtbl.add prtac_tab s (f,g,h) + +let p = prtac_tab +type 'a raw_extra_genarg_printer = + (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds +type 'a glob_extra_genarg_printer = + (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds +type 'a extra_genarg_printer = + (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds let genarg_pprule_v7 = ref Stringmap.empty let genarg_pprule = ref Stringmap.empty -let declare_extra_genarg_pprule for_v8 (rawwit, f) (wit, g) = +let declare_extra_genarg_pprule for_v8 (rawwit, f) (globwit, g) (wit, h) = let s = match unquote wit with | ExtraArgType s -> s | _ -> error "Can declare a pretty-printing rule only for extra argument types" in - let f x = f (out_gen rawwit x) in - let g x = g (out_gen wit x) in - genarg_pprule_v7 := Stringmap.add s (f,g) !genarg_pprule_v7; + let f prc prtac x = f prc prtac (out_gen rawwit x) in + let g prc prtac x = g prc prtac (out_gen globwit x) in + let h prc prtac x = h prc prtac (out_gen wit x) in + genarg_pprule_v7 := Stringmap.add s (f,g,h) !genarg_pprule_v7; if for_v8 then - genarg_pprule := Stringmap.add s (f,g) !genarg_pprule - -(* [pr_rawtac] is here to cheat with ML typing system, - gen_tactic_expr is polymorphic but with some occurrences of its - instance raw_tactic_expr in it; then pr_tactic should be - polymorphic but with some calls to instance of itself, what ML does - not accept; pr_rawtac0 denotes this instance of pr_tactic on - raw_tactic_expr *) - -let pr_rawtac = - ref (fun _ -> failwith "Printer for raw tactic expr is not defined" - : raw_tactic_expr -> std_ppcmds) -let pr_rawtac0 = - ref (fun _ -> failwith "Printer for raw tactic expr is not defined" - : raw_tactic_expr -> std_ppcmds) + genarg_pprule := Stringmap.add s (f,g,h) !genarg_pprule + +let pi1 (a,_,_) = a +let pi2 (_,a,_) = a +let pi3 (_,_,a) = a let pr_arg pr x = spc () ++ pr x -let pr_metanum pr = function +let pr_or_metanum pr = function | AN x -> pr x | MetaNum (_,n) -> str "?" ++ int n @@ -74,10 +90,22 @@ let pr_or_var pr = function | ArgArg x -> pr x | ArgVar (_,s) -> pr_id s -let pr_or_meta pr = function +let pr_or_metaid pr = function | AI x -> pr x | _ -> failwith "pr_hyp_location: unexpected quotation meta-variable" +let pr_and_short_name pr (c,_) = pr c + +let pr_located pr (loc,x) = pr x + +let pr_ltac_constant sp = pr_qualid (Nametab.shortest_qualid_of_tactic sp) + +let pr_evaluable_reference = function + | EvalVarRef id -> pr_id id + | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) + +let pr_inductive ind = pr_global (Libnames.IndRef ind) + let pr_quantified_hypothesis = function | AnonHyp n -> int n | NamedHyp id -> pr_id id @@ -142,23 +170,23 @@ let pr_induction_arg prc = function | ElimOnIdent (_,id) -> pr_id id | ElimOnAnonHyp n -> int n -let pr_match_pattern = function - | Term a -> Ppconstr.pr_pattern a - | Subterm (None,a) -> str "[" ++ Ppconstr.pr_pattern a ++ str "]" - | Subterm (Some id,a) -> pr_id id ++ str "[" ++ Ppconstr.pr_pattern a ++ str "]" +let pr_match_pattern pr_pat = function + | Term a -> pr_pat a + | Subterm (None,a) -> str "[" ++ pr_pat a ++ str "]" + | Subterm (Some id,a) -> pr_id id ++ str "[" ++ pr_pat a ++ str "]" -let pr_match_hyps = function - | NoHypId mp -> str "_:" ++ pr_match_pattern mp - | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern mp +let pr_match_hyps pr_pat = function + | NoHypId mp -> str "_:" ++ pr_match_pattern pr_pat mp + | Hyp ((_,id),mp) -> pr_id id ++ str ":" ++ pr_match_pattern pr_pat mp -let pr_match_rule m pr = function +let pr_match_rule m pr_pat pr = function | Pat ([],mp,t) when m -> - str "[" ++ pr_match_pattern mp ++ str "]" + str "[" ++ pr_match_pattern pr_pat mp ++ str "]" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t | Pat (rl,mp,t) -> str "[" ++ prlist_with_sep pr_semicolon - pr_match_hyps rl ++ spc () ++ - str "|-" ++ spc () ++ pr_match_pattern mp ++ spc () ++ str "]" ++ + (pr_match_hyps pr_pat) rl ++ spc () ++ + str "|-" ++ spc () ++ pr_match_pattern pr_pat mp ++ spc () ++ str "]" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t | All t -> str "_" ++ spc () ++ str "->" ++ brk (1,2) ++ pr t @@ -203,16 +231,7 @@ let pr_autoarg_usingTDB = function | true -> spc () ++ str "Using TDB" | false -> mt () -let rec pr_tacarg_using_rule pr_gen = function - | Egrammar.TacTerm s :: l, al -> - spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) - | Egrammar.TacNonTerm _ :: l, a :: al -> - pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) - | [], [] -> mt () - | _ -> failwith "Inconsistent arguments of extended tactic" - - -let rec pr_rawgen prc prtac x = +let rec pr_raw_generic prc prtac x = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false") | IntArgType -> pr_arg int (out_gen rawwit_int x) @@ -224,52 +243,80 @@ let rec pr_rawgen prc prtac x = | SortArgType -> pr_arg pr_sort (out_gen rawwit_sort x) | ConstrArgType -> pr_arg prc (out_gen rawwit_constr x) | ConstrMayEvalArgType -> - pr_arg (pr_may_eval prc) (out_gen rawwit_constr_may_eval x) + pr_arg (pr_may_eval prc (pr_or_metanum pr_reference)) + (out_gen rawwit_constr_may_eval x) | QuantHypArgType -> pr_arg pr_quantified_hypothesis (out_gen rawwit_quant_hyp x) | RedExprArgType -> - pr_arg (pr_red_expr (prc,pr_metanum pr_reference)) (out_gen rawwit_red_expr x) + pr_arg (pr_red_expr + (prc,pr_or_metanum pr_reference)) (out_gen rawwit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen rawwit_tactic x) | CastedOpenConstrArgType -> pr_arg prc (out_gen rawwit_casted_open_constr x) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings prc) - (out_gen rawwit_constr_with_bindings x) + pr_arg (pr_with_bindings prc) (out_gen rawwit_constr_with_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_rawgen prc prtac x ++ a) x (mt())) + hov 0 (fold_list0 (fun x a -> pr_raw_generic prc prtac x ++ a) x (mt())) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_rawgen prc prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_rawgen prc prtac) (mt()) x) + hov 0 (fold_list1 (fun x a -> pr_raw_generic prc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prtac) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_rawgen prc prtac a ++ spc () ++ pr_rawgen prc - prtac b) + (fun a b -> pr_raw_generic prc prtac a ++ spc () ++ + pr_raw_generic prc prtac b) x) | ExtraArgType s -> let tab = if Options.do_translate() then !genarg_pprule else !genarg_pprule_v7 in - try fst (Stringmap.find s tab) x + try pi1 (Stringmap.find s tab) prc prtac x with Not_found -> str " [no printer for " ++ str s ++ str "] " -let pr_raw_extend prc prt s l = - let prg = pr_rawgen prc prt in - let tab = if Options.do_translate() then prtac_tab else prtac_tab_v7 in - try - let (s,pl) = fst (Hashtbl.find tab s) l in - str s ++ pr_tacarg_using_rule prg (pl,l) - with Not_found -> - str "TODO(" ++ str s ++ prlist prg l ++ str ")" -open Closure - -let pr_evaluable_reference = function - | EvalVarRef id -> pr_id id - | EvalConstRef sp -> pr_global (Libnames.ConstRef sp) +let rec pr_glob_generic prc prtac x = + match Genarg.genarg_tag x with + | BoolArgType -> pr_arg str (if out_gen globwit_bool x then "true" else "false") + | IntArgType -> pr_arg int (out_gen globwit_int x) + | IntOrVarArgType -> pr_arg (pr_or_var pr_int) (out_gen globwit_int_or_var x) + | StringArgType -> spc () ++ str "\"" ++ str (out_gen globwit_string x) ++ str "\"" + | PreIdentArgType -> pr_arg str (out_gen globwit_pre_ident x) + | IdentArgType -> pr_arg pr_id (out_gen globwit_ident x) + | RefArgType -> pr_arg (pr_or_var (pr_located pr_global)) (out_gen globwit_ref x) + | SortArgType -> pr_arg pr_sort (out_gen globwit_sort x) + | ConstrArgType -> pr_arg prc (out_gen globwit_constr x) + | ConstrMayEvalArgType -> + pr_arg (pr_may_eval prc + (pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)))) (out_gen globwit_constr_may_eval x) + | QuantHypArgType -> + pr_arg pr_quantified_hypothesis (out_gen globwit_quant_hyp x) + | RedExprArgType -> + pr_arg (pr_red_expr + (prc,pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)))) (out_gen globwit_red_expr x) + | TacticArgType -> pr_arg prtac (out_gen globwit_tactic x) + | CastedOpenConstrArgType -> + pr_arg prc (out_gen globwit_casted_open_constr x) + | ConstrWithBindingsArgType -> + pr_arg (pr_with_bindings prc) (out_gen globwit_constr_with_bindings x) + | List0ArgType _ -> + hov 0 (fold_list0 (fun x a -> pr_glob_generic prc prtac x ++ a) x (mt())) + | List1ArgType _ -> + hov 0 (fold_list1 (fun x a -> pr_glob_generic prc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_glob_generic prc prtac) (mt()) x) + | PairArgType _ -> + hov 0 + (fold_pair + (fun a b -> pr_glob_generic prc prtac a ++ spc () ++ + pr_glob_generic prc prtac b) + x) + | ExtraArgType s -> + let tab = if Options.do_translate() then !genarg_pprule + else !genarg_pprule_v7 in + try pi2 (Stringmap.find s tab) prc prtac x + with Not_found -> str " [no printer for " ++ str s ++ str "] " -let pr_inductive ind = pr_global (Libnames.IndRef ind) +open Closure -let rec pr_generic prtac x = +let rec pr_generic prc prtac x = match Genarg.genarg_tag x with | BoolArgType -> pr_arg str (if out_gen wit_bool x then "true" else "false") | IntArgType -> pr_arg int (out_gen wit_int x) @@ -278,50 +325,57 @@ let rec pr_generic prtac x = | PreIdentArgType -> pr_arg str (out_gen wit_pre_ident x) | IdentArgType -> pr_arg pr_id (out_gen wit_ident x) | RefArgType -> pr_arg pr_global (out_gen wit_ref x) - | SortArgType -> pr_arg Printer.prterm (Term.mkSort (out_gen wit_sort x)) - | ConstrArgType -> pr_arg Printer.prterm (out_gen wit_constr x) + | SortArgType -> pr_arg prc (Term.mkSort (out_gen wit_sort x)) + | ConstrArgType -> pr_arg prc (out_gen wit_constr x) | ConstrMayEvalArgType -> - pr_arg Printer.prterm (out_gen wit_constr_may_eval x) + pr_arg prc (out_gen wit_constr_may_eval x) | QuantHypArgType -> pr_arg pr_quantified_hypothesis (out_gen wit_quant_hyp x) | RedExprArgType -> - pr_arg (pr_red_expr (Printer.prterm,pr_evaluable_reference)) (out_gen wit_red_expr x) + pr_arg (pr_red_expr (prc,pr_evaluable_reference)) (out_gen wit_red_expr x) | TacticArgType -> pr_arg prtac (out_gen wit_tactic x) | CastedOpenConstrArgType -> - pr_arg Printer.prterm (snd (out_gen wit_casted_open_constr x)) + pr_arg prc (snd (out_gen wit_casted_open_constr x)) | ConstrWithBindingsArgType -> - pr_arg (pr_with_bindings Printer.prterm) - (out_gen wit_constr_with_bindings x) + pr_arg (pr_with_bindings prc) (out_gen wit_constr_with_bindings x) | List0ArgType _ -> - hov 0 (fold_list0 (fun x a -> pr_generic prtac x ++ a) x (mt())) + hov 0 (fold_list0 (fun x a -> pr_generic prc prtac x ++ a) x (mt())) | List1ArgType _ -> - hov 0 (fold_list1 (fun x a -> pr_generic prtac x ++ a) x (mt())) - | OptArgType _ -> hov 0 (fold_opt (pr_generic prtac) (mt()) x) + hov 0 (fold_list1 (fun x a -> pr_generic prc prtac x ++ a) x (mt())) + | OptArgType _ -> hov 0 (fold_opt (pr_generic prc prtac) (mt()) x) | PairArgType _ -> hov 0 (fold_pair - (fun a b -> pr_generic prtac a ++ spc () ++ pr_generic prtac b) + (fun a b -> pr_generic prc prtac a ++ spc () ++ + pr_generic prc prtac b) x) | ExtraArgType s -> let tab = if Options.do_translate() then !genarg_pprule else !genarg_pprule_v7 in - try snd (Stringmap.find s tab) x - with Not_found -> str "[no printer for " ++ str s ++ str "]" + try pi3 (Stringmap.find s tab) prc prtac x + with Not_found -> str " [no printer for " ++ str s ++ str "]" -let pr_extend prt s l = - let prg = pr_generic prt in +let rec pr_tacarg_using_rule pr_gen = function + | Egrammar.TacTerm s :: l, al -> + spc () ++ str s ++ pr_tacarg_using_rule pr_gen (l,al) + | Egrammar.TacNonTerm _ :: l, a :: al -> + pr_gen a ++ pr_tacarg_using_rule pr_gen (l,al) + | [], [] -> mt () + | _ -> failwith "Inconsistent arguments of extended tactic" + +let pr_extend_gen proj prgen s l = let tab = if Options.do_translate() then prtac_tab else prtac_tab_v7 in try - let (s,pl) = snd (Hashtbl.find tab s) l in - str s ++ pr_tacarg_using_rule prg (pl,l) + let (s,pl) = proj (Hashtbl.find tab s) l in + str s ++ pr_tacarg_using_rule prgen (pl,l) with Not_found -> - str s ++ prlist prg l + str s ++ prlist prgen l ++ str " (Generic printer)" -let make_pr_tac (pr_constr,pr_pattern,pr_cst,pr_ind,pr_ident,pr_extend) = +let make_pr_tac (pr_tac,pr_tac0,pr_constr,pr_pat,pr_cst,pr_ind,pr_ref,pr_ident,pr_extend) = let pr_bindings = pr_bindings pr_constr in let pr_with_bindings = pr_with_bindings pr_constr in -let pr_eliminator cb = str "using" ++ pr_arg pr_with_bindings cb in +let pr_eliminator cb = str "using" ++ pr_arg (pr_with_bindings) cb in let pr_constrarg c = spc () ++ pr_constr c in let pr_intarg n = spc () ++ int n in @@ -341,8 +395,8 @@ let rec pr_atom0 = function (* Main tactic printer *) and pr_atom1 = function - | TacExtend (_,s,l) -> pr_extend !pr_rawtac s l - | TacAlias (s,l,_) -> pr_extend !pr_rawtac s (List.map snd l) + | TacExtend (_,s,l) -> pr_extend pr_constr pr_tac s l + | TacAlias (s,l,_) -> pr_extend pr_constr pr_tac s (List.map snd l) (* Basic tactics *) | TacIntroPattern [] as t -> pr_atom0 t @@ -420,7 +474,7 @@ and pr_atom1 = function hov 1 (str "Decompose Sum" ++ pr_arg pr_constr c) | TacDecompose (l,c) -> hov 1 (str "Decompose" ++ spc () ++ - hov 0 (str "[" ++ prlist_with_sep spc (pr_metanum pr_ind) l + hov 0 (str "[" ++ prlist_with_sep spc (pr_or_metanum pr_ind) l ++ str "]")) | TacSpecialize (n,c) -> hov 1 (str "Specialize" ++ pr_opt int n ++ pr_with_bindings c) @@ -445,9 +499,9 @@ and pr_atom1 = function (* Context management *) | TacClear l -> - hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l) | TacClearBody l -> - hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_metanum pr_id) l) + hov 1 (str "Clear" ++ spc () ++ prlist_with_sep spc (pr_or_metanum pr_id) l) | TacMove (b,(_,id1),(_,id2)) -> (* Rem: only b = true is available for users *) assert b; @@ -464,10 +518,10 @@ and pr_atom1 = function | TacRight l -> hov 1 (str "Right" ++ pr_bindings l) | TacSplit (_,l) -> hov 1 (str "Split" ++ pr_bindings l) | TacAnyConstructor (Some t) -> - hov 1 (str "Constructor" ++ pr_arg !pr_rawtac0 t) + hov 1 (str "Constructor" ++ pr_arg pr_tac0 t) | TacAnyConstructor None as t -> pr_atom0 t | TacConstructor (n,l) -> - hov 1 (str "Constructor" ++ pr_or_meta pr_intarg n ++ pr_bindings l) + hov 1 (str "Constructor" ++ pr_or_metaid pr_intarg n ++ pr_bindings l) (* Conversion *) | TacReduce (r,h) -> @@ -562,18 +616,18 @@ and pr6 = function (List.map (fun (id,c,t) -> ((dummy_loc,id),Some c,t)) llc) ++ fnl () | TacMatch (t,lrul) -> - hov 0 (str "Match" ++ spc () ++ pr_may_eval Ppconstr.pr_constr t ++ spc() + hov 0 (str "Match" ++ spc () ++ pr_may_eval pr_constr pr_cst t ++ spc() ++ str "With" ++ prlist (fun r -> fnl () ++ str "|" ++ spc () ++ - pr_match_rule true prtac r) + pr_match_rule true pr_pat prtac r) lrul) | TacMatchContext (lr,lrul) -> hov 0 ( str (if lr then "Match Reverse Context With" else "Match Context With") ++ prlist (fun r -> fnl () ++ str "|" ++ spc () ++ - pr_match_rule false prtac r) + pr_match_rule false pr_pat prtac r) lrul) | TacFun (lvar,body) -> hov 0 (str "Fun" ++ @@ -583,45 +637,58 @@ and pr6 = function and pr_tacarg0 = function | TacDynamic (_,t) -> str ("<dynamic ["^(Dyn.tag t)^"]>") - | MetaNumArg (_,n) -> str ("?" ^ string_of_int n ) | MetaIdArg (_,s) -> str ("$" ^ s) + | Identifier id -> pr_id id | TacVoid -> str "()" - | Reference r -> pr_reference r + | Reference r -> pr_ref r | ConstrMayEval (ConstrTerm c) -> str "'" ++ pr_constr c - | ConstrMayEval c -> pr_may_eval pr_constr c + | ConstrMayEval c -> pr_may_eval pr_constr pr_cst c | Integer n -> int n | (TacCall _ | Tacexp _) as t -> str "(" ++ pr_tacarg1 t ++ str ")" and pr_tacarg1 = function | TacCall (_,f,l) -> - hov 0 (pr_reference f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l) - | Tacexp t -> !pr_rawtac t + hov 0 (pr_ref f ++ spc () ++ prlist_with_sep spc pr_tacarg0 l) + | Tacexp t -> pr_tac t | t -> pr_tacarg0 t and pr_tacarg x = pr_tacarg1 x and prtac x = pr6 x -in (prtac,pr0,pr_match_rule) +in (prtac,pr0,pr_match_rule false pr_pat pr_tac) -let (pr_raw_tactic,pr_raw_tactic0,pr_match_rule) = - make_pr_tac - (Ppconstr.pr_constr, - Ppconstr.pr_constr, - pr_metanum pr_reference, - pr_reference, - pr_or_meta (fun (loc,id) -> pr_id id), - pr_raw_extend Ppconstr.pr_constr) +let pr_raw_extend prc prtac = pr_extend_gen pi1 (pr_raw_generic prc prtac) +let pr_glob_extend prc prtac = pr_extend_gen pi2 (pr_glob_generic prc prtac) +let pr_extend prc prtac = pr_extend_gen pi3 (pr_generic prc prtac) + +let pr_and_constr_expr pr (c,_) = pr c + +let rec glob_printers = + (pr_glob_tactic, + pr_glob_tactic0, + pr_and_constr_expr Ppconstr.pr_rawconstr, + Printer.pr_pattern, + pr_or_metanum (pr_or_var (pr_and_short_name pr_evaluable_reference)), + pr_or_var pr_inductive, + pr_or_var pr_ltac_constant, + pr_located pr_id, + pr_glob_extend) -let _ = pr_rawtac := pr_raw_tactic -let _ = pr_rawtac0 := pr_raw_tactic0 +and pr_glob_tactic (t:glob_tactic_expr) = pi1 (make_pr_tac glob_printers) t + +and pr_glob_tactic0 t = pi2 (make_pr_tac glob_printers) t + +and pr_glob_match_context t = pi3 (make_pr_tac glob_printers) t let (pr_tactic,_,_) = make_pr_tac - (Printer.prterm, - Ppconstr.pr_constr, + (pr_glob_tactic, + pr_glob_tactic0, + Printer.prterm, + Printer.pr_pattern, pr_evaluable_reference, pr_inductive, + pr_ltac_constant, pr_id, pr_extend) - diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 186a726f6..055b5adf2 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -14,42 +14,70 @@ open Tacexpr open Pretyping open Proof_type open Topconstr +open Rawterm -(* if the boolean is false then the extension applies only to old syntax *) +val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds +val pr_or_metanum : ('a -> std_ppcmds) -> 'a or_metanum -> std_ppcmds +val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds +val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds +val pr_located : ('a -> std_ppcmds) -> 'a Util.located -> std_ppcmds + +type 'a raw_extra_genarg_printer = + (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +type 'a glob_extra_genarg_printer = + (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + +type 'a extra_genarg_printer = + (Term.constr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + 'a -> std_ppcmds + + (* if the boolean is false then the extension applies only to old syntax *) val declare_extra_genarg_pprule : bool -> - ('a raw_abstract_argument_type * ('a -> std_ppcmds)) -> - ('b closed_abstract_argument_type * ('b -> std_ppcmds)) -> unit + ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) -> + ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> + ('b closed_abstract_argument_type * 'b extra_genarg_printer) -> unit + +type ('a,'b) gen_gram_prod_builder = + ('a,'b) generic_argument list -> + string * Egrammar.grammar_tactic_production list -(* idem *) + (* if the boolean is false then the extension applies only to old syntax *) val declare_extra_tactic_pprule : - bool -> string -> - (raw_generic_argument list -> - string * Egrammar.grammar_tactic_production list) - -> (closed_generic_argument list -> - string * Egrammar.grammar_tactic_production list) - -> unit + bool -> string -> ('a,'b) gen_gram_prod_builder -> unit -val pr_match_pattern : pattern_expr match_pattern -> std_ppcmds +val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds -val pr_match_rule : bool -> (raw_tactic_expr -> std_ppcmds) -> - (pattern_expr,raw_tactic_expr) match_rule -> std_ppcmds +val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('a,'b) match_rule -> std_ppcmds -val pr_raw_tactic : raw_tactic_expr -> std_ppcmds +val pr_glob_tactic : glob_tactic_expr -> std_ppcmds val pr_tactic : Proof_type.tactic_expr -> std_ppcmds -val pr_rawgen: +val pr_glob_generic: + (rawconstr_and_expr -> std_ppcmds) -> (glob_tactic_expr -> std_ppcmds) -> + glob_generic_argument -> std_ppcmds + +val pr_raw_generic : (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> (constr_expr, raw_tactic_expr) generic_argument -> std_ppcmds + val pr_raw_extend: (constr_expr -> std_ppcmds) -> (raw_tactic_expr -> std_ppcmds) -> string -> - (constr_expr, raw_tactic_expr) generic_argument list -> - std_ppcmds + raw_generic_argument list -> std_ppcmds + +val pr_glob_extend: + (rawconstr_and_expr -> std_ppcmds) -> + (glob_tactic_expr -> std_ppcmds) -> string -> + glob_generic_argument list -> std_ppcmds + val pr_extend : - (raw_tactic_expr -> std_ppcmds) -> string -> - (Term.constr, raw_tactic_expr) generic_argument list -> - std_ppcmds + (Term.constr -> std_ppcmds) -> + (glob_tactic_expr -> std_ppcmds) -> string -> closed_generic_argument list -> std_ppcmds diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 54b928ef8..f79148911 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -145,9 +145,9 @@ let mlexpr_of_intro_pattern = function let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident) let mlexpr_of_or_metanum f = function - | Rawterm.AN a -> <:expr< Rawterm.AN $f a$ >> - | Rawterm.MetaNum (_,n) -> - <:expr< Rawterm.MetaNum $dloc$ $mlexpr_of_int n$ >> + | Genarg.AN a -> <:expr< Genarg.AN $f a$ >> + | Genarg.MetaNum (_,n) -> + <:expr< Genarg.MetaNum $dloc$ $mlexpr_of_int n$ >> let mlexpr_of_or_metaid f = function | Tacexpr.AI a -> <:expr< Tacexpr.AI $f a$ >> @@ -449,7 +449,7 @@ let rec mlexpr_of_atomic_tactic = function *) | _ -> failwith "Quotation of atomic tactic expressions: TODO" -and mlexpr_of_tactic = function +and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function | Tacexpr.TacAtom (loc,t) -> <:expr< Tacexpr.TacAtom $dloc$ $mlexpr_of_atomic_tactic t$ >> | Tacexpr.TacThen (t1,t2) -> @@ -510,8 +510,6 @@ and mlexpr_of_tactic = function and mlexpr_of_tactic_arg = function | Tacexpr.MetaIdArg (loc,id) -> anti loc id - | Tacexpr.MetaNumArg (loc,n) -> - <:expr< Tacexpr.MetaNumArg $dloc$ $mlexpr_of_int n$ >> | Tacexpr.TacCall (loc,t,tl) -> <:expr< Tacexpr.TacCall $dloc$ $mlexpr_of_reference t$ $mlexpr_of_list mlexpr_of_tactic_arg tl$>> | Tacexpr.Tacexp t -> diff --git a/parsing/search.ml b/parsing/search.ml index fc5792fa0..5e2fc7f2c 100644 --- a/parsing/search.ml +++ b/parsing/search.ml @@ -20,6 +20,7 @@ open Declare open Coqast open Environ open Pattern +open Matching open Printer open Libnames open Nametab @@ -131,9 +132,9 @@ let mk_rewrite_pattern2 eq pattern = let pattern_filter pat _ a c = try try - Pattern.is_matching pat (head c) + is_matching pat (head c) with _ -> - Pattern.is_matching + is_matching pat (head (Typing.type_of (Global.env()) Evd.empty c)) with UserError _ -> false diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index a3d5f496e..a7da88b52 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -11,6 +11,7 @@ open Genarg open Q_util open Q_coqast +open Argextend let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = (0,0) @@ -35,35 +36,19 @@ let rec make_when loc = function <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> | _::l -> make_when loc l -let rec make_wit loc = function - | BoolArgType -> <:expr< Genarg.wit_bool >> - | IntArgType -> <:expr< Genarg.wit_int >> - | IntOrVarArgType -> <:expr< Genarg.wit_int_or_var >> - | StringArgType -> <:expr< Genarg.wit_string >> - | PreIdentArgType -> <:expr< Genarg.wit_pre_ident >> - | IdentArgType -> <:expr< Genarg.wit_ident >> - | RefArgType -> <:expr< Genarg.wit_ref >> - | QuantHypArgType -> <:expr< Genarg.wit_quant_hyp >> - | SortArgType -> <:expr< Genarg.wit_sort >> - | ConstrArgType -> <:expr< Genarg.wit_constr >> - | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >> - | TacticArgType -> <:expr< Genarg.wit_tactic >> - | RedExprArgType -> <:expr< Genarg.wit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.wit_casted_open_constr >> - | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >> - | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >> - | List1ArgType t -> <:expr< Genarg.wit_list1 $make_wit loc t$ >> - | OptArgType t -> <:expr< Genarg.wit_opt $make_wit loc t$ >> - | PairArgType (t1,t2) -> - <:expr< Genarg.wit_pair $make_wit loc t1$ $make_wit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"wit_"^s$ >> - let rec make_let e = function | [] -> e | TacNonTerm(loc,t,_,Some p)::l -> let loc = join_loc loc (MLast.loc_of_expr e) in let e = make_let e l in - <:expr< let $lid:p$ = Genarg.out_gen $make_wit loc t$ $lid:p$ in $e$ >> + let v = <:expr< Genarg.out_gen $make_wit loc t$ $lid:p$ >> in + let v = + (* Special case for tactics which must be stored in algebraic + form to avoid marshalling closures and to be reprinted *) + if t = TacticArgType then + <:expr< ($v$, Tacinterp.eval_tactic $v$) >> + else v in + <:expr< let $lid:p$ = $v$ in $e$ >> | _::l -> make_let e l let add_clause s (_,pt,e) l = @@ -95,6 +80,16 @@ let rec make_args = function <:expr< [ Genarg.in_gen $make_wit loc t$ $lid:p$ :: $make_args l$ ] >> | _::l -> make_args l +let rec make_eval_tactic e = function + | [] -> e + | TacNonTerm(loc,TacticArgType,_,Some p)::l -> + let loc = join_loc loc (MLast.loc_of_expr e) in + let e = make_eval_tactic e l in + (* Special case for tactics which must be stored in algebraic + form to avoid marshalling closures and to be reprinted *) + <:expr< let $lid:p$ = ($lid:p$,Tacinterp.eval_tactic $lid:p$) in $e$ >> + | _::l -> make_eval_tactic e l + let rec make_fun e = function | [] -> e | TacNonTerm(loc,_,_,Some p)::l -> @@ -142,7 +137,7 @@ let declare_tactic_v7 loc s cl = let e = make_fun <:expr< - Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $e$ + Refiner.abstract_extended_tactic $mlexpr_of_string s$ $make_args p$ $make_eval_tactic e p$ >> p in <:str_item< value $lid:stac$ = $e$ >> @@ -153,7 +148,7 @@ let declare_tactic_v7 loc s cl = open Pcoq; Egrammar.extend_tactic_grammar $se$ $gl$; let pp = fun [ $list:pl$ ] in - Pptactic.declare_extra_tactic_pprule False $se$ pp pp; + Pptactic.declare_extra_tactic_pprule False $se$ pp; end >> @@ -170,25 +165,26 @@ let declare_tactic loc s cl = let e = make_fun <:expr< - Refiner.abstract_extended_tactic $mlexpr_of_string s'$ $make_args p$ $e$ + Refiner.abstract_extended_tactic $mlexpr_of_string s'$ $make_args p$ $make_eval_tactic e p$ >> p in <:str_item< value $lid:stac$ = $e$ >> in + let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in let se = mlexpr_of_string s in <:str_item< declare open Pcoq; - declare $list:List.map hide_tac cl'$ end; + declare $list:hidden$ end; try Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ]) with e -> Pp.pp (Cerrors.explain_exn e); Egrammar.extend_tactic_grammar $se'$ $gl'$; let pp' = fun [ $list:pl'$ ] in - Pptactic.declare_extra_tactic_pprule True $se'$ pp' pp'; + Pptactic.declare_extra_tactic_pprule True $se'$ pp'; Egrammar.extend_tactic_grammar $se'$ $gl$; let pp = fun [ $list:pl$ ] in - Pptactic.declare_extra_tactic_pprule False $se'$ pp pp; + Pptactic.declare_extra_tactic_pprule False $se'$ pp; end >> @@ -206,7 +202,8 @@ let rec interp_entry_name loc s = else if l > 4 & String.sub s (l-4) 4 = "_opt" then let t, g = interp_entry_name loc (String.sub s 0 (l-4)) in OptArgType t, <:expr< Gramext.Sopt $g$ >> - else + else + let t, se = match Pcoq.entry_type (Pcoq.get_univ "prim") s with | Some _ as x -> x, <:expr< Prim. $lid:s$ >> diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4 index a910c1c06..3fad196f9 100644 --- a/parsing/vernacextend.ml4 +++ b/parsing/vernacextend.ml4 @@ -12,6 +12,7 @@ open Genarg open Q_util open Q_coqast open Ast +open Argextend let join_loc (deb1,_) (_,fin2) = (deb1,fin2) let loc = (0,0) @@ -35,29 +36,6 @@ let rec make_when loc = function <:expr< Genarg.genarg_tag $lid:p$ = $t$ && $l$ >> | _::l -> make_when loc l -let rec make_rawwit loc = function - | BoolArgType -> <:expr< Genarg.rawwit_bool >> - | IntArgType -> <:expr< Genarg.rawwit_int >> - | IntOrVarArgType -> <:expr< Genarg.rawwit_int_or_var >> - | StringArgType -> <:expr< Genarg.rawwit_string >> - | PreIdentArgType -> <:expr< Genarg.rawwit_pre_ident >> - | IdentArgType -> <:expr< Genarg.rawwit_ident >> - | RefArgType -> <:expr< Genarg.rawwit_ref >> - | SortArgType -> <:expr< Genarg.rawwit_sort >> - | ConstrArgType -> <:expr< Genarg.rawwit_constr >> - | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >> - | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >> - | TacticArgType -> <:expr< Genarg.rawwit_tactic >> - | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >> - | CastedOpenConstrArgType -> <:expr< Genarg.rawwit_casted_open_constr >> - | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >> - | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >> - | List1ArgType t -> <:expr< Genarg.wit_list1 $make_rawwit loc t$ >> - | OptArgType t -> <:expr< Genarg.wit_opt $make_rawwit loc t$ >> - | PairArgType (t1,t2) -> - <:expr< Genarg.wit_pair $make_rawwit loc t1$ $make_rawwit loc t2$ >> - | ExtraArgType s -> <:expr< $lid:"rawwit_"^s$ >> - let rec make_let e = function | [] -> e | VernacNonTerm(loc,t,_,Some p)::l -> |