Adding a default object to generic argument registering mechanism.

5 files changed, 43 insertions, 40 deletions

diff --git a/interp/genintern.ml b/interp/genintern.ml
index fef32a5ff9..bc41c834a8 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -24,12 +24,14 @@ module InternObj =
 struct
   type ('raw, 'glb, 'top) obj = ('raw, 'glb) intern_fun
   let name = "intern"
+  let default _ = None
 end
 
 module SubstObj =
 struct
   type ('raw, 'glb, 'top) obj = 'glb subst_fun
   let name = "subst"
+  let default _ = None
 end
 
 module Intern = Register (InternObj)
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 3fb8155106..58dfbc91a1 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -194,6 +194,7 @@ module type GenObj =
 sig
   type ('raw, 'glb, 'top) obj
   val name : string
+  val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option
 end
 
 module Register (M : GenObj) =
@@ -213,7 +214,10 @@ struct
   let get_obj0 name =
     try String.Map.find name !arg0_map
     with Not_found ->
-      Errors.anomaly (str M.name ++ str " function not found: " ++ str name)
+      match M.default (ExtraArgType name) with
+      | None ->
+        Errors.anomaly (str M.name ++ str " function not found: " ++ str name)
+      | Some obj -> obj
 
   (** For now, the following function is quite dummy and should only be applied
       to an extra argument type, otherwise, it will badly fail. *)
diff --git a/lib/genarg.mli b/lib/genarg.mli
index f275b0d004..6eea3ac926 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -227,6 +227,9 @@ sig
 
   val name : string
   (** A name for such kind of manipulation, e.g. [interp]. *)
+
+  val default : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) obj option
+  (** A generic object when there is no registered object for this type. *)
 end
 
 module Register (M : GenObj) :
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 5a1da2fd7d..dcd357d5c9 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -10,44 +10,37 @@ open Pp
 open Util
 open Genarg
 
-type printer = {
-  raw : Obj.t -> std_ppcmds;
-  glb : Obj.t -> std_ppcmds;
-  top : Obj.t -> std_ppcmds;
+type ('raw, 'glb, 'top) printer = {
+  raw : 'raw -> std_ppcmds;
+  glb : 'glb -> std_ppcmds;
+  top : 'top -> std_ppcmds;
 }
 
-let default_printer name = (); fun _ -> str "<genarg:" ++ str name ++ str ">"
-
-let default_printer name =
-  let pr = default_printer name in
-  { raw = pr; glb = pr; top = pr; }
-
-let (arg0_printer_map : printer String.Map.t ref) = ref String.Map.empty
-
-let get_printer0 name =
-  try String.Map.find name !arg0_printer_map
-  with Not_found -> default_printer name
-
-let obj_printer t = match t with
-| ExtraArgType s -> get_printer0 s
-| _ -> assert false
-
-let raw_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).raw
-let glb_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).glb
-let top_print arg = Obj.magic (obj_printer (unquote (rawwit arg))).top
-
-let generic_raw_print v =
-  (obj_printer (genarg_tag v)).raw (Unsafe.prj v)
-let generic_glb_print v =
-  (obj_printer (genarg_tag v)).glb (Unsafe.prj v)
-let generic_top_print v =
-  (obj_printer (genarg_tag v)).top (Unsafe.prj v)
-
-let register_print0 arg rpr gpr tpr = match unquote (rawwit arg) with
-| ExtraArgType s ->
-  if String.Map.mem s !arg0_printer_map then
-    Errors.anomaly (str "interp0 function already registered: " ++ str s)
-  else
-    let pr = { raw = Obj.magic rpr; glb = Obj.magic gpr; top = Obj.magic tpr; } in
-    arg0_printer_map := String.Map.add s pr !arg0_printer_map
-| _ -> assert false
+module PrintObj =
+struct
+  type ('raw, 'glb, 'top) obj = ('raw, 'glb, 'top) printer
+  let name = "printer"
+  let default wit = match unquote (rawwit wit) with
+  | ExtraArgType name ->
+    let printer = {
+      raw = (fun _ -> str "<genarg:" ++ str name ++ str ">");
+      glb = (fun _ -> str "<genarg:" ++ str name ++ str ">");
+      top = (fun _ -> str "<genarg:" ++ str name ++ str ">");
+    } in
+    Some printer
+  | _ -> assert false
+end
+
+module Print = Register (PrintObj)
+
+let register_print0 wit raw glb top =
+  let printer = { raw; glb; top; } in
+  Print.register0 wit printer
+
+let raw_print wit v = (Print.obj wit).raw v
+let glb_print wit v = (Print.obj wit).glb v
+let top_print wit v = (Print.obj wit).top v
+
+let generic_raw_print v = raw_unpack { raw_unpack = raw_print; } v
+let generic_glb_print v = glb_unpack { glb_unpack = glb_print; } v
+let generic_top_print v = top_unpack { top_unpack = top_print; } v
diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
index 2e95670d61..e9d3f42925 100644
--- a/tactics/geninterp.ml
+++ b/tactics/geninterp.ml
@@ -24,6 +24,7 @@ module InterpObj =
 struct
   type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun
   let name = "interp"
+  let default _ = None
 end
 
 module Interp = Register(InterpObj)