diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r-- | toplevel/metasyntax.ml | 33 |
1 files changed, 28 insertions, 5 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 161cf824..639ec1e6 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -61,23 +61,42 @@ let rec make_tags = function | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l | [] -> [] +let make_fresh_key = + let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in + fun () -> + let cur = incr id; !id in + let lbl = Id.of_string ("_" ^ string_of_int cur) in + let kn = Lib.make_kn lbl in + let (mp, dir, _) = KerName.repr kn in + (** We embed the full path of the kernel name in the label so that the + identifier should be unique. This ensures that including two modules + together won't confuse the corresponding labels. *) + let lbl = Id.of_string_soft (Printf.sprintf "%s#%s#%i" + (ModPath.to_string mp) (DirPath.to_string dir) cur) + in + KerName.make mp dir (Label.of_id lbl) + type tactic_grammar_obj = { + tacobj_key : KerName.t; tacobj_local : locality_flag; tacobj_tacgram : tactic_grammar; tacobj_tacpp : Pptactic.pp_tactic; tacobj_body : Tacexpr.glob_tactic_expr } -let cache_tactic_notation ((_, key), tobj) = +let cache_tactic_notation (_, tobj) = + let key = tobj.tacobj_key in Tacenv.register_alias key tobj.tacobj_body; Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp -let open_tactic_notation i ((_, key), tobj) = +let open_tactic_notation i (_, tobj) = + let key = tobj.tacobj_key in if Int.equal i 1 && not tobj.tacobj_local then Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram -let load_tactic_notation i ((_, key), tobj) = +let load_tactic_notation i (_, tobj) = + let key = tobj.tacobj_key in (** Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; @@ -85,7 +104,10 @@ let load_tactic_notation i ((_, key), tobj) = Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram let subst_tactic_notation (subst, tobj) = - { tobj with tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; } + { tobj with + tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; + tacobj_body = Tacsubst.subst_tactic subst tobj.tacobj_body; + } let classify_tactic_notation tacobj = Substitute tacobj @@ -115,6 +137,7 @@ let add_tactic_notation (local,n,prods,e) = tacgram_prods = prods; } in let tacobj = { + tacobj_key = make_fresh_key (); tacobj_local = local; tacobj_tacgram = parule; tacobj_tacpp = pprule; @@ -1103,7 +1126,7 @@ let open_notation i (_, nobj) = let scope = nobj.notobj_scope in let (ntn, df) = nobj.notobj_notation in let pat = nobj.notobj_interp in - if Int.equal i 1 then begin + if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin (* Declare the interpretation *) Notation.declare_notation_interpretation ntn scope pat df; (* Declare the uninterpretation *) |