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

4 files changed, 124 insertions, 76 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
diff --git a/lib/genarg.ml b/lib/genarg.ml
index 77c8922a0..c201d78b4 100644
--- a/lib/genarg.ml
+++ b/lib/genarg.ml
@@ -147,6 +147,19 @@ type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
+type 'r raw_unpack =
+  { raw_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'a -> 'r }
+
+type 'r glb_unpack =
+  { glb_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'b -> 'r }
+
+type 'r top_unpack =
+  { top_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'c -> 'r }
+
+let raw_unpack pack (t, obj) = pack.raw_unpack t (Obj.obj obj)
+let glb_unpack pack (t, obj) = pack.glb_unpack t (Obj.obj obj)
+let top_unpack pack (t, obj) = pack.top_unpack t (Obj.obj obj)
+
 (** Creating args *)
 
 let (arg0_map : Obj.t option String.Map.t ref) = ref String.Map.empty
@@ -175,6 +188,41 @@ let default_empty_value t =
   | Some v -> Some (Obj.obj v)
   | None -> None
 
+(** Registering genarg-manipulating functions *)
+
+module type GenObj =
+sig
+  type ('raw, 'glb, 'top) obj
+  val name : string
+end
+
+module Register (M : GenObj) =
+struct
+  let arg0_map =
+    ref (String.Map.empty : (Obj.t, Obj.t, Obj.t) M.obj String.Map.t)
+
+  let register0 arg f = match arg with
+  | ExtraArgType s ->
+    if String.Map.mem s !arg0_map then
+      let msg = str M.name ++ str " function already registered: " ++ str s in
+      Errors.anomaly msg
+    else
+      arg0_map := String.Map.add s (Obj.magic f) !arg0_map
+  | _ -> assert false
+
+  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)
+
+  (** For now, the following function is quite dummy and should only be applied
+      to an extra argument type, otherwise, it will badly fail. *)
+  let rec obj t = match t with
+  | ExtraArgType s -> Obj.magic (get_obj0 s)
+  | _ -> assert false
+
+end
+
 (** Hackish part *)
 
 let arg0_names = ref (String.Map.empty : string String.Map.t)
diff --git a/lib/genarg.mli b/lib/genarg.mli
index d395136af..8152a19ed 100644
--- a/lib/genarg.mli
+++ b/lib/genarg.mli
@@ -141,6 +141,22 @@ val has_type : 'co generic_argument -> ('a, 'co) abstract_argument_type -> bool
 (** [has_type v t] tells whether [v] has type [t]. If true, it ensures that
     [out_gen t v] will not raise a dynamic type exception. *)
 
+(** {6 Destructors} *)
+
+type 'r raw_unpack =
+  { raw_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'a -> 'r }
+
+type 'r glb_unpack =
+  { glb_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'b -> 'r }
+
+type 'r top_unpack =
+  { top_unpack : 'a 'b 'c. ('a, 'b, 'c) genarg_type -> 'c -> 'r }
+
+val raw_unpack : 'r raw_unpack -> rlevel generic_argument -> 'r
+val glb_unpack : 'r glb_unpack -> glevel generic_argument -> 'r
+val top_unpack : 'r top_unpack -> tlevel generic_argument -> 'r
+(** Existential-type destructors. *)
+
 (** {6 Manipulation of generic arguments}
 
 Those functions fail if they are applied to an argument which has not the right
@@ -206,6 +222,30 @@ val genarg_tag : 'a generic_argument -> argument_type
 
 val unquote : ('a, 'co) abstract_argument_type -> argument_type
 
+(** {6 Registering genarg-manipulating functions}
+
+  This is boilerplate code used here and there in the code of Coq. *)
+
+module type GenObj =
+sig
+  type ('raw, 'glb, 'top) obj
+  (** An object manipulating generic arguments. *)
+
+  val name : string
+  (** A name for such kind of manipulation, e.g. [interp]. *)
+end
+
+module Register (M : GenObj) :
+sig
+  val register0 : ('raw, 'glb, 'top) genarg_type ->
+    ('raw, 'glb, 'top) M.obj -> unit
+  (** Register a ground type manipulation function. *)
+
+  val obj : ('raw, 'glb, 'top) genarg_type -> ('raw, 'glb, 'top) M.obj
+  (** Recover a manipulation function at a given type. *)
+
+end
+
 (** {5 Basic generic type constructors} *)
 
 (** {6 Parameterized types} *)
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