Removing useless tactic arguments, and using generic arguments

instead (proof of concept, to be extended).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16609 85f007b7-540e-0410-9357-904b9bb8a0f7

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