Using functors to reduce the boilerplate used in registering

generic argument stuff, including the unsafe Obj.magic-like casts.

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

1 files changed, 23 insertions, 49 deletions

diff --git a/interp/genintern.ml b/interp/genintern.ml
index 12d25c785..d7171a4d1 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.ml
@@ -21,62 +21,36 @@ type glob_sign = {
 type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb
 type 'glb subst_fun = substitution -> 'glb -> 'glb
 
-let arg0_intern_map =
-  ref (String.Map.empty : (Obj.t, Obj.t) intern_fun String.Map.t)
-let arg0_subst_map =
-  ref (String.Map.empty : Obj.t subst_fun String.Map.t)
+module InternObj =
+struct
+  type ('raw, 'glb, 'top) obj = ('raw, 'glb) intern_fun
+  let name = "intern"
+end
 
-let get_intern0 name =
-  try String.Map.find name !arg0_intern_map
-  with Not_found ->
-    Errors.anomaly (str "intern0 function not found: " ++ str name)
+module SubstObj =
+struct
+  type ('raw, 'glb, 'top) obj = 'glb subst_fun
+  let name = "subst"
+end
 
-let get_subst0 name =
-  try String.Map.find name !arg0_subst_map
-  with Not_found ->
-    Errors.anomaly (str "subst0 function not found: " ++ str name)
+module Intern = Register (InternObj)
+module Subst = Register (SubstObj)
 
-(** 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_intern t = match t with
-| ExtraArgType s -> get_intern0 s
-| _ -> assert false
-
-let intern t = Obj.magic (obj_intern (unquote (rawwit t)))
+let intern = Intern.obj
+let register_intern0 = Intern.register0
 
 let generic_intern ist v =
-  let t = genarg_tag v in
-  let (ist, ans) = obj_intern t ist (Unsafe.prj v) in
-  (ist, Unsafe.inj t ans)
+  let unpack wit v =
+    let (ist, v) = intern wit ist v in
+    (ist, in_gen (glbwit wit) v)
+  in
+  raw_unpack { raw_unpack = unpack; } v
 
 (** Substitution functions *)
 
-let rec obj_substitute t = match t with
-| ExtraArgType s -> get_subst0 s
-| _ -> assert false
-
-let substitute t = Obj.magic (obj_substitute (unquote (rawwit t)))
+let substitute = Subst.obj
+let register_subst0 = Subst.register0
 
 let generic_substitute subs v =
-  let t = genarg_tag v in
-  let ans = obj_substitute t subs (Unsafe.prj v) in
-  Unsafe.inj t ans
-
-(** Registering functions *)
-
-let register_intern0 arg f = match unquote (rawwit arg) with
-| ExtraArgType s ->
-  if String.Map.mem s !arg0_intern_map then
-    Errors.anomaly (str "intern0 function already registered: " ++ str s)
-  else
-    arg0_intern_map := String.Map.add s (Obj.magic f) !arg0_intern_map
-| _ -> assert false
-
-let register_subst0 arg f = match unquote (rawwit arg) with
-| ExtraArgType s ->
-  if String.Map.mem s !arg0_subst_map then
-    Errors.anomaly (str "subst0 function already registered: " ++ str s)
-  else
-    arg0_subst_map := String.Map.add s (Obj.magic f) !arg0_subst_map
-| _ -> assert false
+  let unpack wit v = in_gen (glbwit wit) (substitute wit subs v) in
+  glb_unpack { glb_unpack = unpack; } v