2 files changed, 149 insertions, 1 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 9975f3848..83a415057 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -253,3 +253,94 @@ module TacStore = Store.Make(struct end)
 type interp_sign = {
   lfun : (Id.t * tlevel generic_argument) list;
   extra : TacStore.t }
+
+type ('raw, 'glb, 'top) arg0 = {
+  arg0_rprint : 'raw -> std_ppcmds;
+  arg0_gprint : 'glb -> std_ppcmds;
+  arg0_tprint : 'top -> std_ppcmds;
+  arg0_glob : glob_sign -> 'raw -> glob_sign * 'glb;
+  arg0_subst : Mod_subst.substitution -> 'glb -> 'glb;
+  arg0_interp : interp_sign ->
+    Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top;
+}
+
+let default_arg0 name = {
+  arg0_rprint = (fun _ -> str "<abstract>");
+  arg0_gprint = (fun _ -> str "<abstract>");
+  arg0_tprint = (fun _ -> str "<abstract>");
+  arg0_glob = (fun _ _ -> failwith ("undefined globalizer for " ^ name));
+  arg0_subst = (fun _ _ -> failwith ("undefined substitutor for " ^ name));
+  arg0_interp = (fun _ _ _ -> failwith ("undefined interpreter for " ^ name));
+}
+
+let default_uniform_arg0 name = {
+  arg0_rprint = (fun _ -> str "<abstract>");
+  arg0_gprint = (fun _ -> str "<abstract>");
+  arg0_tprint = (fun _ -> str "<abstract>");
+  arg0_glob = (fun ist x -> (ist, x));
+  arg0_subst = (fun _ x -> x);
+  arg0_interp = (fun _ gl x -> (gl.Evd.sigma, x));
+}
+
+let arg0_map = ref (String.Map.empty : (Obj.t * Obj.t option) String.Map.t)
+(** First component is the argument itself, second is the default raw
+    inhabitant. *)
+
+let make0 def name arg =
+  let () =
+    if String.Map.mem name !arg0_map then
+      Errors.anomaly (str "Genarg " ++ str name ++ str " already defined")
+  in
+  let arg = Obj.repr arg in
+  let def = Obj.magic def in
+  let () = arg0_map := String.Map.add name (arg, def) !arg0_map in
+  ExtraArgType name
+
+let get_obj name =
+  let (obj, _) = String.Map.find name !arg0_map in
+  (Obj.obj obj : (Obj.t, Obj.t, Obj.t) arg0)
+
+(** For now, the following functions are quite dummy and should only be applied
+    to an extra argument type, otherwise, they will badly fail. *)
+
+let arg_gen = function
+| ExtraArgType name -> Obj.magic (get_obj name)
+| _ -> assert false
+
+let rec raw_print (tpe, v) = match tpe with
+| ExtraArgType name ->
+  let obj = get_obj name in
+  obj.arg0_rprint v
+| _ -> assert false (* TODO *)
+
+let rec glb_print (tpe, v) = match tpe with
+| ExtraArgType name ->
+  let obj = get_obj name in
+  obj.arg0_gprint v
+| _ -> assert false (* TODO *)
+
+let rec top_print (tpe, v) = match tpe with
+| ExtraArgType name ->
+  let obj = get_obj name in
+  obj.arg0_rprint v
+| _ -> assert false (* TODO *)
+
+let rec globalize ist (tpe, v) = match tpe with
+| ExtraArgType name ->
+  let obj = get_obj name in
+  let (ist, ans) = obj.arg0_glob ist v in
+  (ist, (tpe, ans))
+| _ -> assert false (* TODO *)
+
+let rec substitute subst (tpe, v) = match tpe with
+| ExtraArgType name ->
+  let obj = get_obj name in
+  (tpe, obj.arg0_subst subst v)
+| _ -> assert false (* TODO *)
+
+let rec interpret ist gl (tpe, v) = match tpe with
+| ExtraArgType name ->
+  let obj = get_obj name in
+  let (ist, ans) = obj.arg0_interp ist gl v in
+  (ist, (tpe, ans))
+| _ -> assert false (* TODO *)
diff --git a/interp/genarg.mli b/interp/genarg.mli
index ff70bd7a2..20311be66 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -103,7 +103,7 @@ type 'a uniform_genarg_type = ('a, 'a, 'a) genarg_type
 
 val create_arg : 'raw option -> string -> ('raw, 'glob, 'top) genarg_type
 (** Create a new generic type of argument: force to associate
-   unique ML types at each of the three levels. *)
+   unique ML types at each of the three levels. FIXME: almost deprecated. *)
 
 (** {5 Specialized types} *)
 
@@ -201,6 +201,8 @@ val app_pair :
 
 (** {6 High-level creation} *)
 
+(** {5 Genarg environments} *)
+
 type glob_sign = {
   ltacvars : Id.t list * Id.t list;
   ltacrecvars : (Id.t * Nametab.ltac_constant) list;
@@ -213,6 +215,61 @@ type interp_sign = {
   lfun : (Id.t * tlevel generic_argument) list;
   extra : TacStore.t }
 
+(** {5 Generic arguments} *)
+
+type ('raw, 'glb, 'top) arg0 = {
+  arg0_rprint : 'raw -> std_ppcmds;
+  (** Printing at raw level function. *)
+  arg0_gprint : 'glb -> std_ppcmds;
+  (** Printing at glob level function. *)
+  arg0_tprint : 'top -> std_ppcmds;
+  (** Printing at top level function. *)
+  arg0_glob : glob_sign -> 'raw -> glob_sign * 'glb;
+  (** Globalization function. *)
+  arg0_subst : Mod_subst.substitution -> 'glb -> 'glb;
+  (** Substitution function. *)
+  arg0_interp : interp_sign ->
+    Goal.goal Evd.sigma -> 'glb -> Evd.evar_map * 'top;
+  (** Intepretation function. *)
+}
+
+val make0 : 'raw option -> string -> ('raw, 'glb, 'top) arg0 ->
+  ('raw, 'glb, 'top) genarg_type
+(** [make0 def name arg] create a generic argument named [name] with the
+    manipulation functions defined in [arg], and with a default empty value
+    [def]. FIXME: [def] is related to parsing and should be put elsewhere. *)
+
+val default_arg0 : string -> ('raw, 'glb, 'top) arg0
+(** A default [arg0] with a given name. Printing functions print a dummy value
+    and glob/subst/interp all fail. *)
+
+val default_uniform_arg0 : string -> ('a, 'a, 'a) arg0
+(** A default uniform [arg0] with a given name. Printing functions print a dummy
+    value and glob/subst/interp are all identity. *)
+
+val arg_gen : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) arg0
+(** Create the manipulation functions for any generic argument type. *)
+
+(** {5 Generic manipulation functions}
+
+  Those functions are the counterparts of [arg0] fields, but they apply on any
+  generic argument.
+
+  FIXME: only partially implemented for now. *)
+
+val raw_print : rlevel generic_argument -> std_ppcmds
+val glb_print : glevel generic_argument -> std_ppcmds
+val top_print : tlevel generic_argument -> std_ppcmds
+
+val globalize : glob_sign ->
+  rlevel generic_argument -> glob_sign * glevel generic_argument
+
+val substitute : Mod_subst.substitution ->
+  glevel generic_argument -> glevel generic_argument
+
+val interpret : interp_sign -> Goal.goal Evd.sigma ->
+  glevel generic_argument -> Evd.evar_map * tlevel generic_argument
+
 (** {6 Type reification} *)
 
 type argument_type =