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, 13 insertions, 27 deletions

diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml
index cdb7dcb11..2e95670d6 100644
--- a/tactics/geninterp.ml
+++ b/tactics/geninterp.ml
@@ -20,34 +20,20 @@ type interp_sign = {
 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)
+module InterpObj =
+struct
+  type ('raw, 'glb, 'top) obj = ('glb, 'top) interp_fun
+  let name = "interp"
+end
 
-let get_interp0 name =
-  try String.Map.find name !arg0_interp_map
-  with Not_found ->
-    Errors.anomaly (str "interp0 function not found: " ++ str name)
+module Interp = Register(InterpObj)
 
-(** 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 interp = Interp.obj
+let register_interp0 = Interp.register0
 
 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
+  let unpack wit v =
+    let (sigma, ans) = interp wit ist gl v in
+    (sigma, in_gen (topwit wit) ans)
+  in
+  glb_unpack { glb_unpack = unpack; } v