From 7a2701e6741fcf1e800e35b7721fc89abe40cbba Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 18 Jun 2013 16:11:36 +0000 Subject: 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 --- Makefile.build | 2 +- grammar/argextend.ml4 | 59 ++++++++++++++++++++++++--------------- interp/genarg.ml | 45 +++++++++++++---------------- plugins/decl_mode/g_decl_mode.ml4 | 27 ++++++++---------- tactics/tacintern.ml | 20 +------------ tactics/tacintern.mli | 7 +---- tactics/tacinterp.ml | 19 +------------ tactics/tacinterp.mli | 9 ++---- tactics/tacsubst.ml | 16 +---------- tactics/tacsubst.mli | 5 +--- 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 *) -- cgit v1.2.3