diff options
-rw-r--r-- | intf/tacexpr.mli | 3 | ||||
-rw-r--r-- | parsing/g_ltac.ml4 | 12 | ||||
-rw-r--r-- | printing/pptactic.ml | 13 | ||||
-rw-r--r-- | tactics/tacintern.ml | 11 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 7 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 3 | ||||
-rw-r--r-- | tactics/tauto.ml4 | 4 |
7 files changed, 32 insertions, 21 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index c253e888d..86ac93d89 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -185,12 +185,11 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = and ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg = | TacDynamic of Loc.t * Dyn.t - | TacVoid + | TacGeneric of 'lev generic_argument | MetaIdArg of Loc.t * bool * string | ConstrMayEval of ('trm,'cst,'pat) may_eval | IntroPattern of intro_pattern_expr located | Reference of 'ref - | Integer of int | TacCall of Loc.t * 'ref * ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_arg list | TacExternal of Loc.t * string * string * diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 482f0df72..b612676e1 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -11,6 +11,7 @@ open Compat open Constrexpr open Tacexpr open Misctypes +open Genarg open Genredexpr open Tok @@ -24,6 +25,9 @@ let arg_of_expr = function TacArg (loc,a) -> a | e -> Tacexp (e:raw_tactic_expr) +let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () +let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n + (* Tactics grammar rules *) GEXTEND Gram @@ -114,14 +118,14 @@ GEXTEND Gram (* Tactic arguments *) tactic_arg: [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> arg_of_expr a - | IDENT "ltac"; ":"; n = natural -> Integer n + | IDENT "ltac"; ":"; n = natural -> TacGeneric (genarg_of_int n) | IDENT "ipattern"; ":"; ipat = simple_intropattern -> IntroPattern ipat | a = may_eval_arg -> a | r = reference -> Reference r | c = Constr.constr -> ConstrMayEval (ConstrTerm c) (* Unambigous entries: tolerated w/o "ltac:" modifier *) | id = METAIDENT -> MetaIdArg (!@loc,true,id) - | "()" -> TacVoid ] ] + | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; may_eval_arg: [ [ c = constr_eval -> ConstrMayEval c @@ -144,9 +148,9 @@ GEXTEND Gram ; tactic_atom: [ [ id = METAIDENT -> MetaIdArg (!@loc,true,id) - | n = integer -> Integer n + | n = integer -> TacGeneric (genarg_of_int n) | r = reference -> TacCall (!@loc,r,[]) - | "()" -> TacVoid ] ] + | "()" -> TacGeneric (genarg_of_unit ()) ] ] ; match_key: [ [ "match" -> false | "lazymatch" -> true ] ] diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 47bc20036..1bf697074 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -555,7 +555,7 @@ let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq let make_pr_tac pr_tac_level (pr_constr,pr_lconstr,pr_pat,pr_lpat, - pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders) = + pr_cst,pr_ind,pr_ref,pr_ident,pr_extend,strip_prod_binders, pr_gen) = (* some shortcuts *) let pr_bindings = pr_bindings pr_lconstr pr_constr in @@ -926,7 +926,7 @@ let rec pr_tac inherited tac = | TacArg(_,ConstrMayEval c) -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c, leval | TacArg(_,TacFreshId l) -> str "fresh" ++ pr_fresh_ids l, latom - | TacArg(_,Integer n) -> int n, latom + | TacArg(_,TacGeneric arg) -> pr_gen arg, latom | TacArg(_,TacCall(loc,f,[])) -> pr_ref f, latom | TacArg(_,TacCall(loc,f,l)) -> pr_with_comments loc @@ -944,14 +944,13 @@ and pr_tacarg = function | MetaIdArg (loc,true,s) -> pr_with_comments loc (str ("$" ^ s)) | MetaIdArg (loc,false,s) -> pr_with_comments loc (str ("constr: $" ^ s)) | IntroPattern ipat -> str "ipattern:" ++ pr_intro_pattern ipat - | TacVoid -> str "()" | Reference r -> pr_ref r | ConstrMayEval c -> pr_may_eval pr_constr pr_lconstr pr_cst pr_pat c | TacFreshId l -> str "fresh" ++ pr_fresh_ids l | TacExternal (_,com,req,la) -> str "external" ++ spc() ++ qs com ++ spc() ++ qs req ++ spc() ++ prlist_with_sep spc pr_tacarg la - | (TacCall _|Tacexp _|Integer _) as a -> + | (TacCall _|Tacexp _ | TacGeneric _) as a -> str "ltac:" ++ pr_tac (latom,E) (TacArg (Loc.ghost,a)) in pr_tac @@ -975,7 +974,8 @@ let raw_printers = pr_reference, pr_or_metaid pr_lident, pr_raw_extend, - strip_prod_binders_expr) + strip_prod_binders_expr, + Genprint.generic_raw_print) let rec pr_raw_tactic_level n (t:raw_tactic_expr) = make_pr_tac pr_raw_tactic_level raw_printers n t @@ -997,7 +997,8 @@ let pr_glob_tactic_level env = pr_ltac_or_var (pr_located pr_ltac_constant), pr_lident, pr_glob_extend, - strip_prod_binders_glob_constr) + strip_prod_binders_glob_constr, + Genprint.generic_glb_print) in let rec prtac n (t:glob_tactic_expr) = make_pr_tac prtac glob_printers n t diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index b1830523b..3f52de11c 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -688,10 +688,10 @@ and intern_tactic_seq onlytac ist = function and intern_tactic_as_arg loc onlytac ist a = match intern_tacarg !strict_check onlytac ist a with - | TacCall _ | TacExternal _ | Reference _ | TacDynamic _ as a -> TacArg (loc,a) + | TacCall _ | TacExternal _ | Reference _ + | TacDynamic _ | TacGeneric _ as a -> TacArg (loc,a) | Tacexp a -> a - | TacVoid | IntroPattern _ | Integer _ - | ConstrMayEval _ | TacFreshId _ as a -> + | IntroPattern _ | ConstrMayEval _ | TacFreshId _ as a -> if onlytac then error_tactic_expected loc else TacArg (loc,a) | MetaIdArg _ -> assert false @@ -705,12 +705,10 @@ and intern_tactic_fun ist (var,body) = (var,intern_tactic_or_tacarg { ist with ltacvars = (lfun',l2) } body) and intern_tacarg strict onlytac ist = function - | TacVoid -> TacVoid | Reference r -> intern_non_tactic_reference strict ist r | IntroPattern ipat -> let lf = ref([],[]) in (*How to know what names the intropattern binds?*) IntroPattern (intern_intro_pattern lf ist ipat) - | Integer n -> Integer n | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c) | MetaIdArg (loc,istac,s) -> (* $id can occur in Grammar tactic... *) @@ -728,6 +726,9 @@ and intern_tacarg strict onlytac ist = function TacExternal (loc,com,req,List.map (intern_tacarg !strict_check false ist) la) | TacFreshId x -> TacFreshId (List.map (intern_or_var ist) x) | Tacexp t -> Tacexp (intern_tactic onlytac ist t) + | TacGeneric arg -> + let (_, arg) = Genintern.generic_intern ist arg in + TacGeneric arg | TacDynamic(loc,t) as x -> (match Dyn.tag t with | "tactic" | "value" -> x diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 09dcb49f4..de72f2b5c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1090,12 +1090,15 @@ and interp_ltac_reference loc' mustbetac ist gl = function and interp_tacarg ist gl arg = let evdref = ref (project gl) in let v = match arg with - | TacVoid -> in_gen (topwit wit_unit) () + | TacGeneric arg -> + let gl = { gl with sigma = !evdref } in + let (sigma, v) = Geninterp.generic_interp ist gl arg in + evdref := sigma; + v | Reference r -> let (sigma,v) = interp_ltac_reference dloc false ist gl r in evdref := sigma; v - | Integer n -> in_gen (topwit wit_int) n | IntroPattern ipat -> let ans = interp_intro_pattern ist gl ipat in in_gen (topwit wit_intro_pattern) ans diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index dcdaf9dbc..274c3b352 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -264,8 +264,9 @@ and subst_tacarg subst = function TacCall (_loc, subst_reference subst f, List.map (subst_tacarg subst) l) | TacExternal (_loc,com,req,la) -> TacExternal (_loc,com,req,List.map (subst_tacarg subst) la) - | (TacVoid | IntroPattern _ | Integer _ | TacFreshId _) as x -> x + | (IntroPattern _ | TacFreshId _) as x -> x | Tacexp t -> Tacexp (subst_tactic subst t) + | TacGeneric arg -> TacGeneric (Genintern.generic_substitute subst arg) | TacDynamic(the_loc,t) as x -> (match Dyn.tag t with | "tactic" | "value" -> x diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index ab31b664d..587ea3311 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -13,6 +13,8 @@ open Hipattern open Names open Globnames open Pp +open Genarg +open Stdarg open Tacticals open Tacinterp open Tactics @@ -174,7 +176,7 @@ let flatten_contravariant_disj flags ist = let hyp = valueIn (Value.of_constr hyp) in iter_tac (List.map_i (fun i arg -> let typ = valueIn (Value.of_constr (mkArrow arg c)) in - let i = Tacexpr.Integer i in + let i = Tacexpr.TacGeneric (in_gen (rawwit wit_int) i) in <:tactic< let typ := $typ in let hyp := $hyp in |