Removing the various glob/subst/interp registering functions for

extra argument types and putting them into Genarg.

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

10 files changed, 75 insertions, 134 deletions

diff --git a/Makefile.build b/Makefile.build
index b68a02cf6..0dda6140c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -68,7 +68,7 @@ ALLDEPS:=$(addsuffix .d, \
 VERBOSE=
 NO_RECOMPILE_ML4=
 NO_RECALC_DEPS=
-READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
+READABLE_ML4=1	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
 COQ_XML=	# is "-xml" when building XML library
 VM=		# is "-no-vm" to not use the vm"
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index 71ba6b021..b5830e789 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -139,56 +139,69 @@ let make_rule loc (prods,act) =
 
 let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
   let rawtyp, rawpr, globtyp, globpr = match typ with
-    | `Uniform typ -> typ, pr, typ, pr
+    | `Uniform typ ->
+      typ, pr, typ, pr
     | `Specialized (a, b, c, d) -> a, b, c, d
   in
   let glob = match g with
     | None ->
-	<:expr< fun e x ->
-          out_gen $make_globwit loc rawtyp$
-            (Tacintern.intern_genarg e
-               (Genarg.in_gen $make_rawwit loc rawtyp$ x)) >>
-    | Some f -> <:expr< $lid:f$>> in
+      begin match rawtyp with
+      | Genarg.ExtraArgType s' when CString.equal s s' ->
+        <:expr< fun ist v -> (ist, v) >>
+      | _ ->
+        <:expr< fun ist v ->
+          let ans = out_gen $make_globwit loc rawtyp$
+          (Tacintern.intern_genarg ist
+          (Genarg.in_gen $make_rawwit loc rawtyp$ v)) in
+          (ist, ans) >>
+      end
+    | Some f ->
+      <:expr< fun ist v -> (ist, $lid:f$ ist v) >>
+  in
   let interp = match f with
     | None ->
+      begin match globtyp with
+      | Genarg.ExtraArgType s' when CString.equal s s' ->
+        <:expr< fun ist gl v -> (gl.Evd.sigma, v) >>
+      | _ ->
 	<:expr< fun ist gl x ->
 	  let (sigma,a_interp) =
 	    Tacinterp.interp_genarg ist gl
                (Genarg.in_gen $make_globwit loc globtyp$ x)
 	  in
           (sigma , out_gen $make_topwit loc globtyp$ a_interp)>>
+      end
     | Some f -> <:expr< $lid:f$>> in
-  let substitute = match h with
+  let subst = match h with
     | None ->
-	<:expr< fun s x ->
+      begin match globtyp with
+      | Genarg.ExtraArgType s' when CString.equal s s' ->
+        <:expr< fun s v -> v >>
+      | _ ->
+        <:expr< fun s x ->
           out_gen $make_globwit loc globtyp$
-	    (Tacsubst.subst_genarg s
-               (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
+          (Tacsubst.subst_genarg s
+            (Genarg.in_gen $make_globwit loc globtyp$ x)) >>
+      end
     | Some f -> <:expr< $lid:f$>> in
+  let defs = [
+    <:patt< Genarg.arg0_subst >>, subst;
+    <:patt< Genarg.arg0_glob >>, glob;
+    <:patt< Genarg.arg0_interp >>, interp;
+  ] in
   let se = mlexpr_of_string s in
   let wit = <:expr< $lid:"wit_"^s$ >> in
   let rawwit = <:expr< Genarg.rawwit $wit$ >> in
-  let globwit = <:expr< Genarg.glbwit $wit$ >> in
-  let topwit = <:expr< Genarg.topwit $wit$ >> in
   let rules = mlexpr_of_list (make_rule loc) (List.rev cl) in
   let default_value = <:expr< $make_possibly_empty_subentries loc s cl$ >> in
   declare_str_items loc
    [ <:str_item<
       value ($lid:"wit_"^s$) =
-      Genarg.create_arg $default_value$ $se$>>;
+        let arg = { (Genarg.default_arg0 $se$) with $list:defs$ } in
+      Genarg.make0 $default_value$ $se$ arg >>;
      <:str_item<
       value $lid:s$ = Pcoq.create_generic_entry $se$ $rawwit$ >>;
      <:str_item< do {
-      Tacintern.add_intern_genarg $se$
-        (fun e x ->
-          (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x))));
-      Tacinterp.add_interp_genarg $se$
-        (fun ist gl x ->
-	  let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in
-          (sigma , Genarg.in_gen $topwit$ a_interp));
-      Tacsubst.add_genarg_subst $se$
-        (fun subst x ->
-          (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))));
       Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a))
 	(None, [(None, None, $rules$)]);
       Pptactic.declare_extra_genarg_pprule
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 83a415057..18408c8f5 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -210,36 +210,11 @@ type an_arg_of_this_type = Obj.t
 
 let in_generic t x = (t, Obj.repr x)
 
-let dyntab = ref ([] : (string * glevel generic_argument option) list)
-
 type ('a,'b) abstract_argument_type = argument_type
 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
 
-let create_arg v s =
-  if List.mem_assoc s !dyntab then
-    Errors.anomaly ~label:"Genarg.create" (str ("already declared generic argument " ^ s));
-  let t = ExtraArgType s in
-  dyntab := (s,Option.map (in_gen t) v) :: !dyntab;
-  t
-
-let default_empty_argtype_value s = List.assoc s !dyntab
-
-let default_empty_value t =
-  let rec aux = function
-  | List0ArgType _ -> Some (in_gen t [])
-  | OptArgType _ -> Some (in_gen t None)
-  | PairArgType(t1,t2) ->
-      (match aux t1, aux t2 with
-      | Some (_,v1), Some (_,v2) -> Some (in_gen t (v1,v2))
-      | _ -> None)
-  | ExtraArgType s -> default_empty_argtype_value s
-  | _ -> None in
-  match aux t with
-  | Some v -> Some (out_gen t v)
-  | None -> None
-
 (** New interface for genargs. *)
 
 type glob_sign = {
@@ -344,3 +319,23 @@ let rec interpret ist gl (tpe, v) = match tpe with
   let (ist, ans) = obj.arg0_interp ist gl v in
   (ist, (tpe, ans))
 | _ -> assert false (* TODO *)
+
+(** Compatibility layer *)
+
+let create_arg v s = make0 v s (default_arg0 s)
+
+let default_empty_value t =
+  let rec aux = function
+  | List0ArgType _ -> Some (Obj.repr [])
+  | OptArgType _ -> Some (Obj.repr None)
+  | PairArgType(t1,t2) ->
+      (match aux t1, aux t2 with
+      | Some v1, Some v2 -> Some (Obj.repr (v1, v2))
+      | _ -> None)
+  | ExtraArgType s ->
+    let (_, def) = String.Map.find s !arg0_map in
+    def
+  | _ -> None in
+  match aux t with
+  | Some v -> Some (Obj.obj v)
+  | None -> None
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 291fabdb6..a90c565f1 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -99,23 +99,18 @@ let proof_instr = Gram.entry_create "proofmode:instr"
     indirect through the [proof_instr] grammar entry. *)
 (* spiwack: proposal: doing that directly from argextend.ml4, maybe ? *)
 
-(* [Genarg.create_arg] creates a new embedding into Genarg. *)
-let wit_proof_instr =
-  Genarg.create_arg None "proof_instr"
-let _ = Tacintern.add_intern_genarg "proof_instr"
-  begin fun e x -> (* declares the globalisation function *)
-    Genarg.in_gen (Genarg.glbwit wit_proof_instr)
-      (Decl_interp.intern_proof_instr e (Genarg.out_gen (Genarg.rawwit wit_proof_instr) x))
-  end
-let _ = Tacinterp.add_interp_genarg "proof_instr"
-  begin fun ist gl x -> (* declares the interpretation function *)
-    Tacmach.project gl ,
-    Genarg.in_gen (Genarg.topwit wit_proof_instr)
-      (interp_proof_instr ist gl (Genarg.out_gen (Genarg.glbwit wit_proof_instr) x))
-  end
 (* declares the substitution function, irrelevant in our case : *)
-let _ = Tacsubst.add_genarg_subst "proof_instr" (fun _ x -> x)
-
+let wit_proof_instr =
+  let name = "proof_instr" in
+  let subst _ x = x in
+  let glob ist v = (ist, Decl_interp.intern_proof_instr ist v) in
+  let interp ist gl x = (Tacmach.project gl, interp_proof_instr ist gl x) in
+  let arg = { Genarg.default_arg0 name with
+    Genarg.arg0_subst = subst;
+    Genarg.arg0_glob = glob;
+    Genarg.arg0_interp = interp;
+  } in
+  Genarg.make0 None name arg
 
 let _ = Pptactic.declare_extra_genarg_pprule wit_proof_instr
   pr_raw_proof_instr pr_glob_proof_instr pr_proof_instr
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index dc84fa592..5abba699e 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -67,24 +67,6 @@ let fully_empty_glob_sign =
 let make_empty_glob_sign () =
   { fully_empty_glob_sign with genv = Global.env () }
 
-type intern_genarg_type =
-    glob_sign -> raw_generic_argument -> glob_generic_argument
-
-let genarginterns =
-  ref (String.Map.empty : intern_genarg_type String.Map.t)
-
-let add_intern_genarg id f =
-  genarginterns := String.Map.add id f !genarginterns
-
-let lookup_intern_genarg id =
-  try String.Map.find id !genarginterns
-  with Not_found ->
-    let msg = "No globalization function found for entry "^id in
-    Pp.msg_warning (Pp.strbrk msg);
-    let dflt = fun _ _ -> failwith msg in
-    add_intern_genarg id dflt;
-    dflt
-
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
 let atomic_mactab = ref Id.Map.empty
@@ -821,7 +803,7 @@ and intern_genarg ist x =
           in_gen (glbwit (wit_tactic n)) (intern_tactic_or_tacarg ist
 	    (out_gen (rawwit (wit_tactic n)) x))
       | None ->
-          lookup_intern_genarg s ist x
+          snd (Genarg.globalize ist x)
 
 (** Other entry points *)
 
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 75576516f..ca33cf21e 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -59,12 +59,7 @@ val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located
 
 (** Adds a globalization function for extra generic arguments *)
 
-type intern_genarg_type =
-    glob_sign -> raw_generic_argument -> glob_generic_argument
-
-val add_intern_genarg : string -> intern_genarg_type -> unit
-
-val intern_genarg : intern_genarg_type
+val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
 
 (** Adds a definition of tactics in the table *)
 val add_tacdef :
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e52c2fe24..d9dc233b9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -175,23 +175,6 @@ let () =
 
 (** Generic arguments : table of interpretation functions *)
 
-type interp_genarg_type =
-  interp_sign -> goal sigma -> glob_generic_argument ->
-    Evd.evar_map * typed_generic_argument
-
-let extragenargtab =
-  ref (String.Map.empty : interp_genarg_type String.Map.t)
-let add_interp_genarg id f =
-  extragenargtab := String.Map.add id f !extragenargtab
-let lookup_interp_genarg id =
-  try String.Map.find id !extragenargtab
-  with Not_found ->
-    let msg = "No interpretation function found for entry " ^ id in
-    msg_warning (strbrk msg);
-    let f = fun _ _ _ -> failwith msg in
-    add_interp_genarg id f;
-    f
-
 let push_trace (loc, ck) ist = match TacStore.get ist.extra f_trace with
 | None -> [1, loc, ck]
 | Some trace ->
@@ -1458,7 +1441,7 @@ and interp_genarg ist gl x =
         in_gen (topwit (wit_tactic n)) 
 	  (TacArg(dloc,valueIn (of_tacvalue f)))
       | None ->
-        let (sigma,v) = lookup_interp_genarg s ist gl x in
+        let (sigma,v) = interpret ist gl x in
 	evdref:=sigma;
 	v
   in
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index f079d1dfb..254bb9fdd 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -73,13 +73,8 @@ val get_debug : unit -> debug_info
 
 (** Adds an interpretation function for extra generic arguments *)
 
-type interp_genarg_type =
-    interp_sign -> goal sigma -> glob_generic_argument ->
-      Evd.evar_map * typed_generic_argument
-
-val add_interp_genarg : string -> interp_genarg_type -> unit
-
-val interp_genarg : interp_genarg_type
+val interp_genarg : interp_sign -> goal sigma -> glob_generic_argument ->
+  Evd.evar_map * typed_generic_argument
 
 (** Interprets any expression *)
 val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 3070cf01c..f33e3ccec 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -23,20 +23,6 @@ open Pretyping
 (** For generic arguments, we declare and store substitutions
     in a table *)
 
-type subst_genarg_type =
-    substitution -> glob_generic_argument -> glob_generic_argument
-let genargsubs =
-  ref (String.Map.empty : subst_genarg_type String.Map.t)
-let add_genarg_subst id f =
-  genargsubs := String.Map.add id f !genargsubs
-let lookup_genarg_subst id =
-  try String.Map.find id !genargsubs
-  with Not_found ->
-    Pp.msg_warning (Pp.strbrk ("No substitution found for entry "^id));
-    let dflt = fun _ x -> x in
-    add_genarg_subst id dflt;
-    dflt
-
 let subst_quantified_hypothesis _ x = x
 
 let subst_declared_or_quantified_hypothesis _ x = x
@@ -346,6 +332,6 @@ and subst_genarg subst (x:glob_generic_argument) =
           in_gen (glbwit (Extrawit.wit_tactic n))
             (subst_tactic subst (out_gen (glbwit (Extrawit.wit_tactic n)) x))
       | None ->
-          lookup_genarg_subst s subst x
+          Genarg.substitute subst x
 
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic
diff --git a/tactics/tacsubst.mli b/tactics/tacsubst.mli
index ade3e7cc9..92640d4bc 100644
--- a/tactics/tacsubst.mli
+++ b/tactics/tacsubst.mli
@@ -18,10 +18,7 @@ val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr
 (** For generic arguments, we declare and store substitutions
     in a table *)
 
-type subst_genarg_type =
-    substitution -> glob_generic_argument -> glob_generic_argument
-val subst_genarg : subst_genarg_type
-val add_genarg_subst : string -> subst_genarg_type -> unit
+val subst_genarg : substitution -> glob_generic_argument -> glob_generic_argument
 
 (** Misc *)