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

5 files changed, 88 insertions, 28 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 18408c8f50..83038c8ba0 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 20311be66b..bbd783047c 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 6d7e921119..86440bc297 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 0000000000..cfc65bde8b
--- /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 0000000000..276c4c54ca
--- /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