Implementing a new interface for Genarg, with centralized data

structure. The code is quite dumb for now, as it only handles basic
extended generig arguments (ExtraArgTypes). Soon, code from other
modules will be centralized there.

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

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 =