Proof-of-concept: moved four easy-to-handle generic arguments to

their own file, Stdarg.

This required a little trick to correctly handle wit_* naming. We
use a dynamic table to remember exactly where those arguments come
from.

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

16 files changed, 113 insertions, 92 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 76fbbfdd5..c16b4abba 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -125,6 +125,7 @@ Lexer
 Ppextend
 Pputils
 Genarg
+Stdarg
 Constrexpr_ops
 Notation_ops
 Topconstr
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4857b16cc..939e9422a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -351,11 +351,7 @@ let pploc x = let (l,r) = Loc.unloc x in
 (* extendable tactic arguments *)
 let rec pr_argument_type = function
   (* Basic types *)
-  | BoolArgType -> str"bool"
-  | IntArgType -> str"int"
   | IntOrVarArgType -> str"int-or-var"
-  | StringArgType -> str"string"
-  | PreIdentArgType -> str"pre-ident"
   | IntroPatternArgType -> str"intro-pattern"
   | IdentArgType true -> str"ident"
   | IdentArgType false -> str"pattern_ident"
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index b5830e789..4ea5f35c1 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -18,20 +18,20 @@ let default_loc = <:expr< Loc.ghost >>
 
 let mk_extraarg s =
   if Extrawit.tactic_genarg_level s = None then
-    <:expr< $lid:"wit_"^s$ >>
+    try
+      let name = Genarg.get_name0 s in
+      <:expr< $lid:name$ >>
+    with Not_found ->
+      <:expr< $lid:"wit_"^s$ >>
   else
-    <:expr<
-      let module WIT = struct
-        open Extrawit;
-        value wit = $lid:"wit_"^s$;
-      end in WIT.wit >>
+      <:expr<
+        let module WIT = struct
+          open Extrawit;
+          value wit = $lid:"wit_"^s$;
+        end in WIT.wit >>
 
 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 >>
   | IntroPatternArgType -> <:expr< Genarg.wit_intro_pattern >>
   | IdentArgType b -> <:expr< Genarg.wit_ident_gen $mlexpr_of_bool b$ >>
   | VarArgType -> <:expr< Genarg.wit_var >>
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 818d220b8..a97b8a2a6 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -27,6 +27,7 @@ Unicode
 Names
 Libnames
 Genarg
+Stdarg
 Tok
 Lexer
 Extrawit
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 0f5be6efb..65aeef11e 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -201,15 +201,11 @@ let mlexpr_of_red_expr = function
       <:expr< Genredexpr.ExtraRedExpr $mlexpr_of_string s$ >>
 
 let rec mlexpr_of_argtype loc = function
-  | Genarg.BoolArgType -> <:expr< Genarg.BoolArgType >>
-  | Genarg.IntArgType -> <:expr< Genarg.IntArgType >>
   | Genarg.IntOrVarArgType -> <:expr< Genarg.IntOrVarArgType >>
   | Genarg.RefArgType -> <:expr< Genarg.RefArgType >>
-  | Genarg.PreIdentArgType -> <:expr< Genarg.PreIdentArgType >>
   | Genarg.IntroPatternArgType -> <:expr< Genarg.IntroPatternArgType >>
   | Genarg.IdentArgType b -> <:expr< Genarg.IdentArgType $mlexpr_of_bool b$ >>
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
-  | Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
   | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 18408c8f5..83038c8ba 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -15,11 +15,7 @@ open Misctypes
 
 type argument_type =
   (* Basic types *)
-  | BoolArgType
-  | IntArgType
   | IntOrVarArgType
-  | StringArgType
-  | PreIdentArgType
   | IntroPatternArgType
   | IdentArgType of bool
   | VarArgType
@@ -41,11 +37,7 @@ type argument_type =
   | ExtraArgType of string
 
 let rec argument_type_eq arg1 arg2 = match arg1, arg2 with
-| BoolArgType, BoolArgType -> true
-| IntArgType, IntArgType -> true
 | IntOrVarArgType, IntOrVarArgType -> true
-| StringArgType, StringArgType -> true
-| PreIdentArgType, PreIdentArgType -> true
 | IntroPatternArgType, IntroPatternArgType -> true
 | IdentArgType b1, IdentArgType b2 -> (b1 : bool) == b2
 | VarArgType, VarArgType -> true
@@ -97,16 +89,8 @@ let rawwit t = t
 let glbwit t = t
 let topwit t = t
 
-let wit_bool = BoolArgType
-
-let wit_int = IntArgType
-
 let wit_int_or_var = IntOrVarArgType
 
-let wit_string = StringArgType
-
-let wit_pre_ident = PreIdentArgType
-
 let wit_intro_pattern = IntroPatternArgType
 
 let wit_ident_gen b = IdentArgType b
@@ -339,3 +323,19 @@ let default_empty_value t =
   match aux t with
   | Some v -> Some (Obj.obj v)
   | None -> None
+
+(** Hackish part *)
+
+let arg0_names = ref (String.Map.empty : string String.Map.t)
+(** We use this table to associate a name to a given witness, to use it with
+    the extension mechanism. This is REALLY ad-hoc, but I do not know how to
+    do so nicely either. *)
+
+let register_name0 t name = match t with
+| ExtraArgType s ->
+  let () = assert (not (String.Map.mem s !arg0_names)) in
+  arg0_names := String.Map.add s name !arg0_names
+| _ -> failwith "register_name0"
+
+let get_name0 name =
+  String.Map.find name !arg0_names
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 20311be66..bbd783047 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -274,11 +274,7 @@ val interpret : interp_sign -> Goal.goal Evd.sigma ->
 
 type argument_type =
   (** Basic types *)
-  | BoolArgType
-  | IntArgType
   | IntOrVarArgType
-  | StringArgType
-  | PreIdentArgType
   | IntroPatternArgType
   | IdentArgType of bool
   | VarArgType
@@ -311,16 +307,8 @@ val unquote : ('a, 'co) abstract_argument_type -> argument_type
 
 open Evd
 
-val wit_bool : bool uniform_genarg_type
-
-val wit_int : int uniform_genarg_type
-
 val wit_int_or_var : int or_var uniform_genarg_type
 
-val wit_string : string uniform_genarg_type
-
-val wit_pre_ident : string uniform_genarg_type
-
 val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type
 
 val wit_ident : Id.t uniform_genarg_type
@@ -392,3 +380,11 @@ val in_generic :
   argument_type -> an_arg_of_this_type -> 'co generic_argument
 
 val default_empty_value : ('raw, 'glb, 'top) genarg_type -> 'raw option
+
+val register_name0 : ('a, 'b, 'c) genarg_type -> string -> unit
+(** Used by the extension to give a name to types. The string should be the
+    absolute path of the argument witness, e.g.
+    [register_name0 wit_toto "MyArg.wit_toto"]. *)
+
+val get_name0 : string -> string
+(** Return the absolute path of a given witness. *)
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 6d7e92111..86440bc29 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -5,6 +5,7 @@ Ppextend
 Notation
 Dumpglob
 Genarg
+Stdarg
 Syntax_def
 Smartlocate
 Reserve
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
new file mode 100644
index 000000000..cfc65bde8
--- /dev/null
+++ b/interp/stdarg.ml
@@ -0,0 +1,44 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Genarg
+
+let def_uniform name pr = { (default_uniform_arg0 name) with
+  arg0_rprint = pr;
+  arg0_gprint = pr;
+  arg0_tprint = pr;
+}
+
+let wit_bool : bool uniform_genarg_type =
+  let pr_bool b = str (if b then "true" else "false") in
+  let arg = def_uniform "bool" pr_bool in
+  make0 None "bool" arg
+
+let () = register_name0 wit_bool "Stdarg.wit_bool"
+
+let wit_int : int uniform_genarg_type =
+  let pr_int = int in
+  let arg = def_uniform "int" pr_int in
+  make0 None "int" arg
+
+let () = register_name0 wit_int "Stdarg.wit_int"
+
+let wit_string : string uniform_genarg_type =
+  let pr_string s = str "\"" ++ str s ++ str "\"" in
+  let arg = def_uniform "string" pr_string in
+  make0 None "string" arg
+
+let () = register_name0 wit_string "Stdarg.wit_string"
+
+let wit_pre_ident : string uniform_genarg_type =
+  let pr_pre_ident = str in
+  let arg = def_uniform "preident" pr_pre_ident in
+  make0 None "preident" arg
+
+let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident"
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
new file mode 100644
index 000000000..276c4c54c
--- /dev/null
+++ b/interp/stdarg.mli
@@ -0,0 +1,19 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Basic generic arguments. *)
+
+open Genarg
+
+val wit_bool : bool uniform_genarg_type
+
+val wit_int : int uniform_genarg_type
+
+val wit_string : string uniform_genarg_type
+
+val wit_pre_ident : string uniform_genarg_type
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 3c04503dd..06120a0a0 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -13,6 +13,7 @@ open Errors
 open Util
 open Extend
 open Genarg
+open Stdarg
 open Tacexpr
 open Extrawit
 
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 350d96142..241d72813 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -141,11 +141,7 @@ let if_pattern_ident b pr c = (if b then str "?" else mt()) ++ pr c
 
 let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
   match Genarg.genarg_tag x with
-  | BoolArgType -> str (if out_gen (rawwit wit_bool) x then "true" else "false")
-  | IntArgType -> int (out_gen (rawwit wit_int) x)
   | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
-  | StringArgType -> str "\"" ++ str (out_gen (rawwit wit_string) x) ++ str "\""
-  | PreIdentArgType -> str (out_gen (rawwit wit_pre_ident) x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen (rawwit wit_intro_pattern) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (rawwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
@@ -180,16 +176,12 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
 	  x)
   | ExtraArgType s ->
       try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> str "[no printer for " ++ str s ++ str "]"
+      with Not_found -> Genarg.raw_print x
 
 
 let rec pr_glob_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
-  | BoolArgType -> str (if out_gen (glbwit wit_bool) x then "true" else "false")
-  | IntArgType -> int (out_gen (glbwit wit_int) x)
   | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
-  | StringArgType -> str "\"" ++ str (out_gen (glbwit wit_string) x) ++ str "\""
-  | PreIdentArgType -> str (out_gen (glbwit wit_pre_ident) x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen (glbwit wit_intro_pattern) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (glbwit wit_ident) x)
   | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
@@ -226,15 +218,11 @@ let rec pr_glob_generic prc prlc prtac prpat x =
 	  x)
   | ExtraArgType s ->
       try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> str "[no printer for " ++ str s ++ str "]"
+      with Not_found -> Genarg.glb_print x
 
 let rec pr_generic prc prlc prtac prpat x =
   match Genarg.genarg_tag x with
-  | BoolArgType -> str (if out_gen (topwit wit_bool) x then "true" else "false")
-  | IntArgType -> int (out_gen (topwit wit_int) x)
   | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
-  | StringArgType -> str "\"" ++ str (out_gen (topwit wit_string) x) ++ str "\""
-  | PreIdentArgType -> str (out_gen (topwit wit_pre_ident) x)
   | IntroPatternArgType -> pr_intro_pattern (out_gen (topwit wit_intro_pattern) x)
   | IdentArgType b -> if_pattern_ident b pr_id (out_gen (topwit wit_ident) x)
   | VarArgType -> pr_id (out_gen (topwit wit_var) x)
@@ -267,7 +255,7 @@ let rec pr_generic prc prlc prtac prpat x =
 	  x)
   | ExtraArgType s ->
       try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
-      with Not_found -> str "[no printer for " ++ str s ++ str "]"
+      with Not_found -> Genarg.top_print x
 
 let rec tacarg_using_rule_token pr_gen = function
   | Some s :: l, al -> str s :: tacarg_using_rule_token pr_gen (l,al)
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index d5b3986af..89774ba21 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -14,6 +14,7 @@ open Term
 open Pattern
 open Misctypes
 open Genarg
+open Stdarg
 
 exception CannotCoerceTo of string
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 5abba699e..456779732 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -747,15 +747,9 @@ and intern_match_rule onlytac ist = function
 
 and intern_genarg ist x =
   match genarg_tag x with
-  | BoolArgType -> in_gen (glbwit wit_bool) (out_gen (rawwit wit_bool) x)
-  | IntArgType -> in_gen (glbwit wit_int) (out_gen (rawwit wit_int) x)
   | IntOrVarArgType ->
       in_gen (glbwit wit_int_or_var)
         (intern_or_var ist (out_gen (rawwit wit_int_or_var) x))
-  | StringArgType ->
-      in_gen (glbwit wit_string) (out_gen (rawwit wit_string) x)
-  | PreIdentArgType ->
-      in_gen (glbwit wit_pre_ident) (out_gen (rawwit wit_pre_ident) x)
   | IntroPatternArgType ->
       let lf = ref ([],[]) in
       (* how to know which names are bound by the intropattern *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index d9dc233b9..06a3ad260 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -33,6 +33,7 @@ open Termops
 open Tacexpr
 open Hiddentac
 open Genarg
+open Stdarg
 open Printer
 open Pretyping
 open Extrawit
@@ -1358,15 +1359,9 @@ and interp_genarg ist gl x =
   let rec interp_genarg ist gl x =
     let gl = { gl with sigma = !evdref } in
     match genarg_tag x with
-    | BoolArgType -> in_gen (topwit wit_bool) (out_gen (glbwit wit_bool) x)
-    | IntArgType -> in_gen (topwit wit_int) (out_gen (glbwit wit_int) x)
     | IntOrVarArgType ->
       in_gen (topwit wit_int_or_var)
         (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x)))
-    | StringArgType ->
-      in_gen (topwit wit_string) (out_gen (glbwit wit_string) x)
-    | PreIdentArgType ->
-      in_gen (topwit wit_pre_ident) (out_gen (glbwit wit_pre_ident) x)
     | IntroPatternArgType ->
       in_gen (topwit wit_intro_pattern)
         (interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x))
@@ -1876,12 +1871,8 @@ and interp_atomic ist gl tac =
   | TacAlias (loc,s,l,(_,body)) -> fun gl ->
     let evdref = ref gl.sigma in
     let rec f x = match genarg_tag x with
-    | IntArgType ->
-        in_gen (topwit wit_int) (out_gen (glbwit wit_int) x)
     | IntOrVarArgType ->
         mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)
-    | PreIdentArgType ->
-	failwith "pre-identifiers cannot be bound"
     | IntroPatternArgType ->
 	let ipat = interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x) in
 	in_gen (topwit wit_intro_pattern) ipat
@@ -1929,10 +1920,6 @@ and interp_atomic ist gl tac =
         let wit = glbwit (wit_list0 wit_var) in
         let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in
         in_gen (topwit (wit_list0 wit_genarg)) ans
-    | List0ArgType IntArgType ->
-        let wit = glbwit (wit_list0 wit_int) in
-        let ans = List.map (fun x -> in_gen (topwit wit_int) x) (out_gen wit x) in
-        in_gen (topwit (wit_list0 wit_genarg)) ans
     | List0ArgType IntOrVarArgType ->
         let wit = glbwit (wit_list0 wit_int_or_var) in
         let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
@@ -1961,10 +1948,6 @@ and interp_atomic ist gl tac =
         let wit = glbwit (wit_list1 wit_var) in
         let ans = List.map (mk_hyp_value ist gl) (out_gen wit x) in
         in_gen (topwit (wit_list1 wit_genarg)) ans
-    | List1ArgType IntArgType ->
-        let wit = glbwit (wit_list1 wit_int) in
-        let ans = List.map (fun x -> in_gen (topwit wit_int) x) (out_gen wit x) in
-        in_gen (topwit (wit_list1 wit_genarg)) ans
     | List1ArgType IntOrVarArgType ->
         let wit = glbwit (wit_list1 wit_int_or_var) in
         let ans = List.map (mk_int_or_var_value ist) (out_gen wit x) in
@@ -1979,12 +1962,16 @@ and interp_atomic ist gl tac =
 	let mk_ipat x = interp_intro_pattern ist gl x in
 	let ans = List.map mk_ipat (out_gen wit x) in
         in_gen (topwit (wit_list1 wit_intro_pattern)) ans
-    | StringArgType | BoolArgType
+    | List0ArgType _ -> app_list0 f x
+    | List1ArgType _ -> app_list1 f x
+    | ExtraArgType _ ->
+      let (sigma, v) = Genarg.interpret ist { gl with sigma = !evdref } x in
+      evdref := sigma;
+      v
     | QuantHypArgType | RedExprArgType
     | OpenConstrArgType _ | ConstrWithBindingsArgType
-    | ExtraArgType _ | BindingsArgType
+    | BindingsArgType
     | OptArgType _ | PairArgType _
-    | List0ArgType _ | List1ArgType _
 	-> error "This argument type is not supported in tactic notations."
 
     in
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index f33e3ccec..ba80d6d6c 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -286,11 +286,7 @@ and subst_match_rule subst = function
 
 and subst_genarg subst (x:glob_generic_argument) =
   match genarg_tag x with
-  | BoolArgType -> in_gen (glbwit wit_bool) (out_gen (glbwit wit_bool) x)
-  | IntArgType -> in_gen (glbwit wit_int) (out_gen (glbwit wit_int) x)
   | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x)
-  | StringArgType -> in_gen (glbwit wit_string) (out_gen (glbwit wit_string) x)
-  | PreIdentArgType -> in_gen (glbwit wit_pre_ident) (out_gen (glbwit wit_pre_ident) x)
   | IntroPatternArgType ->
       in_gen (glbwit wit_intro_pattern) (out_gen (glbwit wit_intro_pattern) x)
   | IdentArgType b ->