Splitted up Genarg in four different levels:

1. Genarg itself which only defines the abstract datatypes needed.
2. Genintern, first file of interp/, defining the intern and subst
   functions.
3. Geninterp, first file of tactics/, defining the interp function.
4. Genprint, first file of printing/, dealing with the printers.

The Genarg file has no dependency and is in lib/, so that we can put
generic arguments everywhere, and in particular in ASTs.

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

8 files changed, 123 insertions, 11 deletions

diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
new file mode 100644
index 0000000000..deba015362
--- /dev/null
+++ b/tactics/geninterp.ml
@@ -0,0 +1,53 @@
+(************************************************************************)
+(*  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 Util
+open Names
+open Genarg
+
+module TacStore = Store.Make(struct end)
+
+type interp_sign = {
+  lfun : (Id.t * tlevel generic_argument) list;
+  extra : TacStore.t }
+
+type ('glb, 'top) interp_fun = interp_sign ->
+    Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top
+
+let arg0_interp_map =
+  ref (String.Map.empty : (Obj.t, Obj.t) interp_fun String.Map.t)
+
+let get_interp0 name =
+  try String.Map.find name !arg0_interp_map
+  with Not_found ->
+    Errors.anomaly (str "interp0 function not found: " ++ str name)
+
+(** For now, the following functions are quite dummy and should only be applied
+    to an extra argument type, otherwise, they will badly fail. *)
+
+let rec obj_interp t = match t with
+| ExtraArgType s -> get_interp0 s
+| _ -> assert false
+
+let interp t = Obj.magic (obj_interp (unquote (rawwit t)))
+
+let generic_interp ist gl v =
+  let t = genarg_tag v in
+  let (sigma, ans) = obj_interp t ist gl (Unsafe.prj v) in
+  (sigma, Unsafe.inj t ans)
+
+(** Registering functions *)
+
+let register_interp0 arg f = match unquote (rawwit arg) with
+| ExtraArgType s ->
+  if String.Map.mem s !arg0_interp_map then
+    Errors.anomaly (str "interp0 function already registered: " ++ str s)
+  else
+    arg0_interp_map := String.Map.add s (Obj.magic f) !arg0_interp_map
+| _ -> assert false
diff --git a/tactics/geninterp.mli b/tactics/geninterp.mli
new file mode 100644
index 0000000000..0f5e6bf0ff
--- /dev/null
+++ b/tactics/geninterp.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Interpretation functions for generic arguments. *)
+
+open Names
+open Genarg
+
+module TacStore : Store.S
+
+type interp_sign = {
+  lfun : (Id.t * tlevel generic_argument) list;
+  extra : TacStore.t }
+
+type ('glb, 'top) interp_fun = interp_sign ->
+    Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top
+
+val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun
+
+val generic_interp : (glob_generic_argument, typed_generic_argument) interp_fun
+
+val register_interp0 :
+  ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index d085704bbb..3e008657fe 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -53,7 +53,7 @@ let skip_metaid = function
 
 (** Generic arguments *)
 
-type glob_sign = Genarg.glob_sign = {
+type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.t list * Id.t list;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
   ltacrecvars : (Id.t * ltac_constant) list;
@@ -798,7 +798,7 @@ and intern_genarg ist x =
           in_gen (glbwit (wit_tactic n)) (intern_tactic_or_tacarg ist
 	    (out_gen (rawwit (wit_tactic n)) x))
       | None ->
-          snd (Genarg.globalize ist x)
+          snd (Genintern.generic_intern ist x)
 
 (** Other entry points *)
 
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index ca33cf21ec..3fa59ed3b9 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -23,7 +23,7 @@ open Nametab
 (** Globalization of tactic expressions :
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
 
-type glob_sign = Genarg.glob_sign = {
+type glob_sign = Genintern.glob_sign = {
   ltacvars : Id.t list * Id.t list;
   ltacrecvars : (Id.t * ltac_constant) list;
   gsigma : Evd.evar_map;
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a13a8faf2e..e0fe2cde41 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -87,7 +87,7 @@ let catch_error call_trace tac g =
     raise located_exc
   end
 
-module TacStore = Genarg.TacStore
+module TacStore = Geninterp.TacStore
 
 let f_avoid_ids : Id.t list TacStore.field = TacStore.field ()
 (* ids inherited from the call context (needed to get fresh ids) *)
@@ -95,7 +95,7 @@ let f_debug : debug_info TacStore.field = TacStore.field ()
 let f_trace : ltac_trace TacStore.field = TacStore.field ()
 
 (* Signature for interpretation: val_interp and interpretation functions *)
-type interp_sign = Genarg.interp_sign = {
+type interp_sign = Geninterp.interp_sign = {
   lfun : (Id.t * value) list;
   extra : TacStore.t }
 
@@ -1437,7 +1437,7 @@ and interp_genarg ist gl x =
         in_gen (topwit (wit_tactic n)) 
 	  (TacArg(dloc,valueIn (of_tacvalue f)))
       | None ->
-        let (sigma,v) = interpret ist gl x in
+        let (sigma,v) = Geninterp.generic_interp ist gl x in
 	evdref:=sigma;
 	v
   in
@@ -1966,7 +1966,7 @@ and interp_atomic ist gl tac =
     | List0ArgType _ -> app_list0 f x
     | List1ArgType _ -> app_list1 f x
     | ExtraArgType _ ->
-      let (sigma, v) = Genarg.interpret ist { gl with sigma = !evdref } x in
+      let (sigma, v) = Geninterp.generic_interp ist { gl with sigma = !evdref } x in
       evdref := sigma;
       v
     | QuantHypArgType | RedExprArgType
@@ -2021,6 +2021,36 @@ let hide_interp t ot gl =
   | None -> t gl
   | Some t' -> (tclTHEN t t') gl
 
+(***************************************************************************)
+(** Register standard arguments *)
+
+let def_intern ist x = (ist, x)
+let def_subst _ x = x
+let def_interp ist gl x = (gl.Evd.sigma, x)
+
+let declare_uniform t pr =
+  Genintern.register_intern0 t def_intern;
+  Genintern.register_subst0 t def_subst;
+  Geninterp.register_interp0 t def_interp;
+  Genprint.register_print0 t pr pr pr
+
+let () =
+  let pr_unit _ = str "()" in
+  declare_uniform wit_unit pr_unit
+
+let () =
+  declare_uniform wit_int int
+
+let () =
+  let pr_bool b = if b then str "true" else str "false" in
+  declare_uniform wit_bool pr_bool
+
+let () =
+  let pr_string s = str "\"" ++ str s ++ str "\"" in
+  declare_uniform wit_string pr_string
+
+let () =
+  declare_uniform wit_pre_ident str
 
 (***************************************************************************)
 (* Other entry points *)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 254bb9fdd8..6affc21a47 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -33,11 +33,11 @@ end
 type value = Value.t
 
 module TacStore : Store.S with
-  type t = Genarg.TacStore.t
-  and type 'a field = 'a Genarg.TacStore.field
+  type t = Geninterp.TacStore.t
+  and type 'a field = 'a Geninterp.TacStore.field
 
 (** Signature for interpretation: val\_interp and interpretation functions *)
-type interp_sign = Genarg.interp_sign = {
+type interp_sign = Geninterp.interp_sign = {
   lfun : (Id.t * value) list;
   extra : TacStore.t }
 
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index f1ada93649..dcdaf9dbc1 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -329,6 +329,6 @@ and subst_genarg subst (x:glob_generic_argument) =
           in_gen (glbwit (Extrawit.wit_tactic n))
             (subst_tactic subst (out_gen (glbwit (Extrawit.wit_tactic n)) x))
       | None ->
-          Genarg.substitute subst x
+          Genintern.generic_substitute subst x
 
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index c08cc66dad..0b97e08527 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,3 +1,4 @@
+Geninterp
 Dn
 Termdn
 Btermdn