diff options
-rw-r--r-- | grammar/tacextend.ml4 | 2 | ||||
-rw-r--r-- | tactics/g_ltac.ml4 | 2 | ||||
-rw-r--r-- | tactics/hightactics.mllib | 1 | ||||
-rw-r--r-- | tactics/tacentries.ml | 186 | ||||
-rw-r--r-- | tactics/tacentries.mli | 19 | ||||
-rw-r--r-- | toplevel/metasyntax.ml | 170 | ||||
-rw-r--r-- | toplevel/metasyntax.mli | 9 |
7 files changed, 208 insertions, 181 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index bbd3d8a62..2ef30f299 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -120,7 +120,7 @@ let declare_tactic loc s c cl = match cl with let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in let pp = make_printing_rule cl in let gl = mlexpr_of_clause cl in - let obj = <:expr< fun () -> Metasyntax.add_ml_tactic_notation $se$ $gl$ >> in + let obj = <:expr< fun () -> Tacentries.add_ml_tactic_notation $se$ $gl$ >> in declare_str_items loc [ <:str_item< do { try do { diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 index 5c0ae215d..d75073877 100644 --- a/tactics/g_ltac.ml4 +++ b/tactics/g_ltac.ml4 @@ -401,7 +401,7 @@ VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF [ let l = Locality.LocalityFixme.consume () in let n = Option.default 0 n in - Metasyntax.add_tactic_notation (Locality.make_module_locality l, n, r, e) + Tacentries.add_tactic_notation (Locality.make_module_locality l, n, r, e) ] END diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib index 0649f2f72..b18d148ec 100644 --- a/tactics/hightactics.mllib +++ b/tactics/hightactics.mllib @@ -1,3 +1,4 @@ +Tacentries Tacinterp Evar_tactics Tactic_option diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml new file mode 100644 index 000000000..e40f5f46a --- /dev/null +++ b/tactics/tacentries.ml @@ -0,0 +1,186 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Errors +open Util +open Names +open Libobject +open Pcoq +open Egramml +open Egramcoq +open Vernacexpr + +(**********************************************************************) +(* Tactic Notation *) + +let interp_prod_item lev = function + | TacTerm s -> GramTerminal s + | TacNonTerm (loc, nt, (_, sep)) -> + let EntryName (etyp, e) = interp_entry_name lev nt sep in + GramNonTerminal (loc, etyp, e) + +let make_terminal_status = function + | GramTerminal s -> Some s + | GramNonTerminal _ -> None + +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 : Id.t list * Tacexpr.glob_tactic_expr; +} + +let check_key key = + if Tacenv.check_alias key then + error "Conflicting tactic notations keys. This can happen when including \ + twice the same module." + +let cache_tactic_notation (_, tobj) = + let key = tobj.tacobj_key in + let () = check_key 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 (_, 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 (_, tobj) = + let key = tobj.tacobj_key in + let () = check_key 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; + if Int.equal i 1 && not tobj.tacobj_local then + Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram + +let subst_tactic_notation (subst, tobj) = + let (ids, body) = tobj.tacobj_body in + { tobj with + tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; + tacobj_body = (ids, Tacsubst.subst_tactic subst body); + } + +let classify_tactic_notation tacobj = Substitute tacobj + +let inTacticGrammar : tactic_grammar_obj -> obj = + declare_object {(default_object "TacticGrammar") with + open_function = open_tactic_notation; + load_function = load_tactic_notation; + cache_function = cache_tactic_notation; + subst_function = subst_tactic_notation; + classify_function = classify_tactic_notation} + +let cons_production_parameter = function +| TacTerm _ -> None +| TacNonTerm (_, _, (id, _)) -> Some id + +let add_tactic_notation (local,n,prods,e) = + let ids = List.map_filter cons_production_parameter prods in + let prods = List.map (interp_prod_item n) prods in + let pprule = { + Pptactic.pptac_level = n; + pptac_prods = prods; + } in + let tac = Tacintern.glob_tactic_env ids (Global.env()) e in + let parule = { + tacgram_level = n; + tacgram_prods = prods; + } in + let tacobj = { + tacobj_key = make_fresh_key (); + tacobj_local = local; + tacobj_tacgram = parule; + tacobj_tacpp = pprule; + tacobj_body = (ids, tac); + } in + Lib.add_anonymous_leaf (inTacticGrammar tacobj) + +(**********************************************************************) +(* ML Tactic entries *) + +type ml_tactic_grammar_obj = { + mltacobj_name : Tacexpr.ml_tactic_name; + (** ML-side unique name *) + mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list; + (** Grammar rules generating the ML tactic. *) +} + +exception NonEmptyArgument + +(** ML tactic notations whose use can be restricted to an identifier are added + as true Ltac entries. *) +let extend_atomic_tactic name entries = + let open Tacexpr in + let map_prod prods = + let (hd, rem) = match prods with + | GramTerminal s :: rem -> (s, rem) + | _ -> assert false (** Not handled by the ML extension syntax *) + in + let empty_value = function + | GramTerminal s -> raise NonEmptyArgument + | GramNonTerminal (_, typ, e) -> + let Genarg.Rawwit wit = typ in + let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in + let default = epsilon_value inj e in + match default with + | None -> raise NonEmptyArgument + | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def + in + try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None + in + let entries = List.map map_prod entries in + let add_atomic i args = match args with + | None -> () + | Some (id, args) -> + let args = List.map (fun a -> Tacexp a) args in + let entry = { mltac_name = name; mltac_index = i } in + let body = TacML (Loc.ghost, entry, args) in + Tacenv.register_ltac false false (Names.Id.of_string id) body + in + List.iteri add_atomic entries + +let cache_ml_tactic_notation (_, obj) = + extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod + +let open_ml_tactic_notation i obj = + if Int.equal i 1 then cache_ml_tactic_notation obj + +let inMLTacticGrammar : ml_tactic_grammar_obj -> obj = + declare_object { (default_object "MLTacticGrammar") with + open_function = open_ml_tactic_notation; + cache_function = cache_ml_tactic_notation; + classify_function = (fun o -> Substitute o); + subst_function = (fun (_, o) -> o); + } + +let add_ml_tactic_notation name prods = + let obj = { + mltacobj_name = name; + mltacobj_prod = prods; + } in + Lib.add_anonymous_leaf (inMLTacticGrammar obj); + extend_atomic_tactic name prods diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli new file mode 100644 index 000000000..635415b9d --- /dev/null +++ b/tactics/tacentries.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Vernacexpr +open Tacexpr + +(** Adding a tactic notation in the environment *) + +val add_tactic_notation : + locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> + unit + +val add_ml_tactic_notation : ml_tactic_name -> + Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index e5edc7422..6277a8146 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -43,176 +43,6 @@ let inToken : string -> obj = let add_token_obj s = Lib.add_anonymous_leaf (inToken s) (**********************************************************************) -(* Tactic Notation *) - -let interp_prod_item lev = function - | TacTerm s -> GramTerminal s - | TacNonTerm (loc, nt, (_, sep)) -> - let EntryName (etyp, e) = interp_entry_name lev nt sep in - GramNonTerminal (loc, etyp, e) - -let make_terminal_status = function - | GramTerminal s -> Some s - | GramNonTerminal _ -> None - -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 : Id.t list * Tacexpr.glob_tactic_expr; -} - -let check_key key = - if Tacenv.check_alias key then - error "Conflicting tactic notations keys. This can happen when including \ - twice the same module." - -let cache_tactic_notation (_, tobj) = - let key = tobj.tacobj_key in - let () = check_key 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 (_, 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 (_, tobj) = - let key = tobj.tacobj_key in - let () = check_key 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; - if Int.equal i 1 && not tobj.tacobj_local then - Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram - -let subst_tactic_notation (subst, tobj) = - let (ids, body) = tobj.tacobj_body in - { tobj with - tacobj_key = Mod_subst.subst_kn subst tobj.tacobj_key; - tacobj_body = (ids, Tacsubst.subst_tactic subst body); - } - -let classify_tactic_notation tacobj = Substitute tacobj - -let inTacticGrammar : tactic_grammar_obj -> obj = - declare_object {(default_object "TacticGrammar") with - open_function = open_tactic_notation; - load_function = load_tactic_notation; - cache_function = cache_tactic_notation; - subst_function = subst_tactic_notation; - classify_function = classify_tactic_notation} - -let cons_production_parameter = function -| TacTerm _ -> None -| TacNonTerm (_, _, (id, _)) -> Some id - -let add_tactic_notation (local,n,prods,e) = - let ids = List.map_filter cons_production_parameter prods in - let prods = List.map (interp_prod_item n) prods in - let pprule = { - Pptactic.pptac_level = n; - pptac_prods = prods; - } in - let tac = Tacintern.glob_tactic_env ids (Global.env()) e in - let parule = { - tacgram_level = n; - tacgram_prods = prods; - } in - let tacobj = { - tacobj_key = make_fresh_key (); - tacobj_local = local; - tacobj_tacgram = parule; - tacobj_tacpp = pprule; - tacobj_body = (ids, tac); - } in - Lib.add_anonymous_leaf (inTacticGrammar tacobj) - -(**********************************************************************) -(* ML Tactic entries *) - -type ml_tactic_grammar_obj = { - mltacobj_name : Tacexpr.ml_tactic_name; - (** ML-side unique name *) - mltacobj_prod : Tacexpr.raw_tactic_expr grammar_prod_item list list; - (** Grammar rules generating the ML tactic. *) -} - -exception NonEmptyArgument - -(** ML tactic notations whose use can be restricted to an identifier are added - as true Ltac entries. *) -let extend_atomic_tactic name entries = - let open Tacexpr in - let map_prod prods = - let (hd, rem) = match prods with - | GramTerminal s :: rem -> (s, rem) - | _ -> assert false (** Not handled by the ML extension syntax *) - in - let empty_value = function - | GramTerminal s -> raise NonEmptyArgument - | GramNonTerminal (_, typ, e) -> - let Genarg.Rawwit wit = typ in - let inj x = TacArg (Loc.ghost, TacGeneric (Genarg.in_gen typ x)) in - let default = epsilon_value inj e in - match default with - | None -> raise NonEmptyArgument - | Some def -> Tacintern.intern_tactic_or_tacarg Tacintern.fully_empty_glob_sign def - in - try Some (hd, List.map empty_value rem) with NonEmptyArgument -> None - in - let entries = List.map map_prod entries in - let add_atomic i args = match args with - | None -> () - | Some (id, args) -> - let args = List.map (fun a -> Tacexp a) args in - let entry = { mltac_name = name; mltac_index = i } in - let body = TacML (Loc.ghost, entry, args) in - Tacenv.register_ltac false false (Names.Id.of_string id) body - in - List.iteri add_atomic entries - -let cache_ml_tactic_notation (_, obj) = - extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod - -let open_ml_tactic_notation i obj = - if Int.equal i 1 then cache_ml_tactic_notation obj - -let inMLTacticGrammar : ml_tactic_grammar_obj -> obj = - declare_object { (default_object "MLTacticGrammar") with - open_function = open_ml_tactic_notation; - cache_function = cache_ml_tactic_notation; - classify_function = (fun o -> Substitute o); - subst_function = (fun (_, o) -> o); - } - -let add_ml_tactic_notation name prods = - let obj = { - mltacobj_name = name; - mltacobj_prod = prods; - } in - Lib.add_anonymous_leaf (inMLTacticGrammar obj); - extend_atomic_tactic name prods - -(**********************************************************************) (* Printing grammar entries *) let entry_buf = Buffer.create 64 diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 5d01405b2..085cc87c8 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -15,15 +15,6 @@ open Notation_term val add_token_obj : string -> unit -(** Adding a tactic notation in the environment *) - -val add_tactic_notation : - locality_flag * int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> - unit - -val add_ml_tactic_notation : ml_tactic_name -> - Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit - (** Adding a (constr) notation in the environment*) val add_infix : locality_flag -> (lstring * syntax_modifier list) -> |