diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/extraargs.ml4 | 10 | ||||
| -rw-r--r-- | ltac/g_ltac.ml4 | 2 | ||||
| -rw-r--r-- | ltac/tacentries.ml | 173 | ||||
| -rw-r--r-- | ltac/tacentries.mli | 40 |
4 files changed, 127 insertions, 98 deletions
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index fbae17bafc..0bddcc9fdd 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -40,6 +40,16 @@ let () = let inject (loc, v) = Tacexpr.Tacexp v in Tacentries.create_ltac_quotation "ltac" inject (Pcoq.Tactic.tactic_expr, Some 5) +(** Backward-compatible tactic notation entry names *) + +let () = + let register name entry = Tacentries.register_tactic_notation_entry name entry in + register "hyp" wit_var; + register "simple_intropattern" wit_intro_pattern; + register "integer" wit_integer; + register "reference" wit_ref; + () + (* Rewriting orientation *) let _ = Metasyntax.add_token_obj "<-" diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index fe750f429f..df499a2c9c 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -405,7 +405,7 @@ VERNAC COMMAND EXTEND VernacTacticNotation [ let l = Locality.LocalityFixme.consume () in let n = Option.default 0 n in - Tacentries.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/ltac/tacentries.ml b/ltac/tacentries.ml index 46e48c6953..f94f84a73b 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -23,6 +23,9 @@ type 'a grammar_tactic_prod_item_expr = | TacTerm of string | TacNonTerm of Loc.t * 'a * Names.Id.t +type raw_argument = string * string option +type argument = Genarg.ArgT.any Extend.user_symbol + (**********************************************************************) (* Interpret entry names of the form "ne_constr_list" as entry keys *) @@ -46,12 +49,6 @@ let atactic n = type entry_name = EntryName : 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name -let try_get_entry u s = - let open Extend in - (** Order the effects: get_entry can raise Not_found *) - let TypedEntry (typ, e) = get_entry u s in - EntryName (typ, Aentry (name_of_entry e)) - (** Quite ad-hoc *) let get_tacentry n m = let open Extend in @@ -91,13 +88,12 @@ let rec parse_user_entry s sep = let n = Char.code s.[6] - 48 in Uentryl ("tactic", n) else - let s = match s with "hyp" -> "var" | _ -> s in Uentry s let arg_list = function Rawwit t -> Rawwit (ListArg t) let arg_opt = function Rawwit t -> Rawwit (OptArg t) -let interp_entry_name up_level s sep = +let interp_entry_name interp symb = let open Extend in let rec eval = function | Ulist1 e -> @@ -115,19 +111,10 @@ let interp_entry_name up_level s sep = | Uopt e -> let EntryName (t, g) = eval e in EntryName (arg_opt t, Aopt g) - | Uentry s -> - begin - try try_get_entry uprim s with Not_found -> - try try_get_entry uconstr s with Not_found -> - try try_get_entry utactic s with Not_found -> - error ("Unknown entry "^s^".") - end - | Uentryl (s, n) -> - (** FIXME: do better someday *) - assert (String.equal s "tactic"); - get_tacentry n up_level + | Uentry s -> interp s None + | Uentryl (s, n) -> interp s (Some n) in - eval (parse_user_entry s sep) + eval symb (**********************************************************************) (** Grammar declaration for Tactic Notation (Coq level) *) @@ -150,21 +137,6 @@ type tactic_grammar = { tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list; } -(** ML Tactic grammar extensions *) - -let add_ml_tactic_entry (name, prods) = - let entry = Tactic.simple_tactic in - let mkact i loc l : Tacexpr.raw_tactic_expr = - let open Tacexpr in - let entry = { mltac_name = name; mltac_index = i } in - let map arg = TacGeneric arg in - TacML (loc, entry, List.map map l) - in - let rules = List.map_i (fun i p -> make_rule (mkact i) p) 0 prods in - synchronize_level_positions (); - grammar_extend entry None (None, [(None, None, List.rev rules)]); - 1 - (* Declaration of the tactic grammar rule *) let head_is_ident tg = match tg.tacgram_prods with @@ -173,7 +145,7 @@ let head_is_ident tg = match tg.tacgram_prods with (** Tactic grammar extensions *) -let add_tactic_entry (kn, tg) = +let add_tactic_entry (kn, ml, tg) = let open Tacexpr in let entry, pos = get_tactic_entry tg.tacgram_level in let mkact loc l = @@ -185,7 +157,7 @@ let add_tactic_entry (kn, tg) = let map arg t = (** HACK to handle especially the tactic(...) entry *) let wit = Genarg.rawwit Constrarg.wit_tactic in - if Genarg.argument_type_eq t (Genarg.unquote wit) then + if Genarg.argument_type_eq t (Genarg.unquote wit) && not ml then Tacexp (Genarg.out_gen wit arg) else TacGeneric arg @@ -205,24 +177,42 @@ let add_tactic_entry (kn, tg) = let tactic_grammar = create_grammar_command "TacticGrammar" add_tactic_entry -let ml_tactic_grammar = - create_grammar_command "MLTacticGrammar" add_ml_tactic_entry - -let extend_tactic_grammar kn ntn = extend_grammar tactic_grammar (kn, ntn) -let extend_ml_tactic_grammar n ntn = extend_grammar ml_tactic_grammar (n, ntn) +let extend_tactic_grammar kn ml ntn = extend_grammar tactic_grammar (kn, ml, ntn) (**********************************************************************) (* Tactic Notation *) +let entry_names = ref String.Map.empty + +let register_tactic_notation_entry name entry = + let entry = match entry with + | ExtraArg arg -> ArgT.Any arg + | _ -> assert false + in + entry_names := String.Map.add name entry !entry_names + 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 symbol = parse_user_entry nt sep in + let interp s = function + | None -> + let ArgT.Any arg = + if String.Map.mem s !entry_names then + String.Map.find s !entry_names + else match ArgT.name s with + | None -> error ("Unknown entry "^s^".") + | Some arg -> arg + in + let wit = ExtraArg arg in + EntryName (Rawwit wit, Extend.Aentry (name_of_entry (genarg_grammar wit))) + | Some n -> + (** FIXME: do better someday *) + assert (String.equal s "tactic"); + get_tacentry n lev + in + let EntryName (etyp, e) = interp_entry_name interp symbol in + GramNonTerminal (loc, etyp, e) let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in @@ -243,8 +233,13 @@ 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; + tacobj_forml : bool; +} + +let pprule pa = { + Pptactic.pptac_level = pa.tacgram_level; + pptac_prods = pa.tacgram_prods; } let check_key key = @@ -256,22 +251,22 @@ let cache_tactic_notation (_, tobj) = let key = tobj.tacobj_key in let () = check_key key in Tacenv.register_alias key tobj.tacobj_body; - extend_tactic_grammar key tobj.tacobj_tacgram; - Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp + extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram; + Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram) let open_tactic_notation i (_, tobj) = let key = tobj.tacobj_key in if Int.equal i 1 && not tobj.tacobj_local then - extend_tactic_grammar key tobj.tacobj_tacgram + extend_tactic_grammar key tobj.tacobj_forml 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; + Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram); if Int.equal i 1 && not tobj.tacobj_local then - extend_tactic_grammar key tobj.tacobj_tacgram + extend_tactic_grammar key tobj.tacobj_forml tobj.tacobj_tacgram let subst_tactic_notation (subst, tobj) = let (ids, body) = tobj.tacobj_body in @@ -294,14 +289,7 @@ 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 add_glob_tactic_notation local n prods forml ids tac = let parule = { tacgram_level = n; tacgram_prods = prods; @@ -310,21 +298,20 @@ let add_tactic_notation (local,n,prods,e) = tacobj_key = make_fresh_key (); tacobj_local = local; tacobj_tacgram = parule; - tacobj_tacpp = pprule; tacobj_body = (ids, tac); + tacobj_forml = forml; } in Lib.add_anonymous_leaf (inTacticGrammar tacobj) +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 tac = Tacintern.glob_tactic_env ids (Global.env()) e in + add_glob_tactic_notation local n prods false ids tac + (**********************************************************************) (* 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 @@ -359,27 +346,33 @@ let extend_atomic_tactic name entries = 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 + let interp_prods = function + | TacTerm s -> None, GramTerminal s + | TacNonTerm (loc, symb, id) -> + let interp (ArgT.Any tag) lev = match lev with + | None -> + let wit = ExtraArg tag in + EntryName (Rawwit wit, Extend.Aentry (Pcoq.name_of_entry (Pcoq.genarg_grammar wit))) + | Some lev -> + assert (coincide (ArgT.repr tag) "tactic" 0); + EntryName (Rawwit Constrarg.wit_tactic, atactic lev) + in + let EntryName (etyp, e) = interp_entry_name interp symb in + Some id, GramNonTerminal (loc, etyp, e) + in + let prods = List.map (fun p -> List.map interp_prods p) prods in + let iter i prods = + let open Tacexpr in + let (ids, prods) = List.split prods in + let ids = List.map_filter (fun x -> x) ids in + let entry = { mltac_name = name; mltac_index = i } in + let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in + let tac = TacML (Loc.ghost, entry, List.map map ids) in + add_glob_tactic_notation false 0 prods true ids tac + in + List.iteri iter prods; + extend_atomic_tactic name (List.map (fun p -> List.map snd p) prods) (**********************************************************************) (** Ltac quotations *) diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 0f4bb2530e..7586bff92f 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -6,25 +6,51 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Ltac toplevel command entries. *) + open Vernacexpr open Tacexpr +(** {5 Tactic Definitions} *) + +val register_ltac : locality_flag -> Vernacexpr.tacdef_body list -> unit +(** Adds new Ltac definitions to the environment. *) + +(** {5 Tactic Notations} *) + type 'a grammar_tactic_prod_item_expr = | TacTerm of string | TacNonTerm of Loc.t * 'a * Names.Id.t -(** Adding a tactic notation in the environment *) +type raw_argument = string * string option +(** An argument type as provided in Tactic notations, i.e. a string like + "ne_foo_list_opt" together with a separator that only makes sense in the + "_sep" cases. *) + +type argument = Genarg.ArgT.any Extend.user_symbol +(** A fully resolved argument type given as an AST with generic arguments on the + leaves. *) val add_tactic_notation : - locality_flag * int * (string * string option) grammar_tactic_prod_item_expr list * raw_tactic_expr -> - unit + locality_flag -> int -> raw_argument grammar_tactic_prod_item_expr list -> + raw_tactic_expr -> unit +(** [add_tactic_notation local level prods expr] adds a tactic notation in the + environment at level [level] with locality [local] made of the grammar + productions [prods] and returning the body [expr] *) + +val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -> unit +(** Register an argument under a given entry name for tactic notations. When + translating [raw_argument] into [argument], atomic names will be first + looked up according to names registered through this function and fallback + to finding an argument by name (as in {!Genarg}) if there is none + matching. *) val add_ml_tactic_notation : ml_tactic_name -> - Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit - -val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit + argument grammar_tactic_prod_item_expr list list -> unit +(** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND + ML-side macro. *) -(** {5 Adding tactic quotations} *) +(** {5 Tactic Quotations} *) val create_ltac_quotation : string -> ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit |