diff options
Diffstat (limited to 'ltac/tacentries.ml')
-rw-r--r-- | ltac/tacentries.ml | 513 |
1 files changed, 0 insertions, 513 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml deleted file mode 100644 index 673ac832..00000000 --- a/ltac/tacentries.ml +++ /dev/null @@ -1,513 +0,0 @@ -(************************************************************************) -(* 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 Pp -open CErrors -open Util -open Names -open Libobject -open Genarg -open Extend -open Pcoq -open Egramml -open Egramcoq -open Vernacexpr -open Libnames -open Nameops - -type 'a grammar_tactic_prod_item_expr = 'a Pptactic.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 *) - -let coincide s pat off = - let len = String.length pat in - let break = ref true in - let i = ref 0 in - while !break && !i < len do - let c = Char.code s.[off + !i] in - let d = Char.code pat.[!i] in - break := Int.equal c d; - incr i - done; - !break - -let atactic n = - if n = 5 then Aentry Tactic.binder_tactic - else Aentryl (Tactic.tactic_expr, n) - -type entry_name = EntryName : - 'a raw_abstract_argument_type * (Tacexpr.raw_tactic_expr, 'a) Extend.symbol -> entry_name - -(** Quite ad-hoc *) -let get_tacentry n m = - let check_lvl n = - Int.equal m n - && not (Int.equal m 5) (* Because tactic5 is at binder_tactic *) - && not (Int.equal m 0) (* Because tactic0 is at simple_tactic *) - in - if check_lvl n then EntryName (rawwit Constrarg.wit_tactic, Aself) - else if check_lvl (n + 1) then EntryName (rawwit Constrarg.wit_tactic, Anext) - else EntryName (rawwit Constrarg.wit_tactic, atactic n) - -let get_separator = function -| None -> error "Missing separator." -| Some sep -> sep - -let rec parse_user_entry s sep = - let l = String.length s in - if l > 8 && coincide s "ne_" 0 && coincide s "_list" (l - 5) then - let entry = parse_user_entry (String.sub s 3 (l-8)) None in - Ulist1 entry - else if l > 12 && coincide s "ne_" 0 && - coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 3 (l-12)) None in - Ulist1sep (entry, get_separator sep) - else if l > 5 && coincide s "_list" (l-5) then - let entry = parse_user_entry (String.sub s 0 (l-5)) None in - Ulist0 entry - else if l > 9 && coincide s "_list_sep" (l-9) then - let entry = parse_user_entry (String.sub s 0 (l-9)) None in - Ulist0sep (entry, get_separator sep) - else if l > 4 && coincide s "_opt" (l-4) then - let entry = parse_user_entry (String.sub s 0 (l-4)) None in - Uopt entry - else if Int.equal l 7 && coincide s "tactic" 0 && '5' >= s.[6] && s.[6] >= '0' then - let n = Char.code s.[6] - 48 in - Uentryl ("tactic", n) - else - Uentry s - -let arg_list = function Rawwit t -> Rawwit (ListArg t) -let arg_opt = function Rawwit t -> Rawwit (OptArg t) - -let interp_entry_name interp symb = - let rec eval = function - | Ulist1 e -> Ulist1 (eval e) - | Ulist1sep (e, sep) -> Ulist1sep (eval e, sep) - | Ulist0 e -> Ulist0 (eval e) - | Ulist0sep (e, sep) -> Ulist0sep (eval e, sep) - | Uopt e -> Uopt (eval e) - | Uentry s -> Uentry (interp s None) - | Uentryl (s, n) -> Uentryl (interp s (Some n), n) - in - eval symb - -(**********************************************************************) -(** Grammar declaration for Tactic Notation (Coq level) *) - -let get_tactic_entry n = - if Int.equal n 0 then - Tactic.simple_tactic, None - else if Int.equal n 5 then - Tactic.binder_tactic, None - else if 1<=n && n<5 then - Tactic.tactic_expr, Some (Extend.Level (string_of_int n)) - else - error ("Invalid Tactic Notation level: "^(string_of_int n)^".") - -(**********************************************************************) -(** State of the grammar extensions *) - -type tactic_grammar = { - tacgram_level : int; - tacgram_prods : Pptactic.grammar_terminals; -} - -(* Declaration of the tactic grammar rule *) - -let head_is_ident tg = match tg.tacgram_prods with -| TacTerm _ :: _ -> true -| _ -> false - -let rec prod_item_of_symbol lev = function -| Extend.Ulist1 s -> - let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1 e) -| Extend.Ulist0 s -> - let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0 e) -| Extend.Ulist1sep (s, sep) -> - let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist1sep (e, Atoken (CLexer.terminal sep))) -| Extend.Ulist0sep (s, sep) -> - let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (ListArg typ), Alist0sep (e, Atoken (CLexer.terminal sep))) -| Extend.Uopt s -> - let EntryName (Rawwit typ, e) = prod_item_of_symbol lev s in - EntryName (Rawwit (OptArg typ), Aopt e) -| Extend.Uentry arg -> - let ArgT.Any tag = arg in - let wit = ExtraArg tag in - EntryName (Rawwit wit, Extend.Aentry (genarg_grammar wit)) -| Extend.Uentryl (s, n) -> - let ArgT.Any tag = s in - assert (coincide (ArgT.repr tag) "tactic" 0); - get_tacentry n lev - -(** Tactic grammar extensions *) - -let add_tactic_entry (kn, ml, tg) state = - let open Tacexpr in - let entry, pos = get_tactic_entry tg.tacgram_level in - let mkact loc l = - let map arg = - (** HACK to handle especially the tactic(...) entry *) - let wit = Genarg.rawwit Constrarg.wit_tactic in - if Genarg.has_type arg wit && not ml then - Tacexp (Genarg.out_gen wit arg) - else - TacGeneric arg - in - let l = List.map map l in - (TacAlias (loc,kn,l):raw_tactic_expr) - in - let () = - if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then - error "Notation for simple tactic must start with an identifier." - in - let map = function - | TacTerm s -> GramTerminal s - | TacNonTerm (loc, s, _) -> - let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in - GramNonTerminal (loc, typ, e) - in - let prods = List.map map tg.tacgram_prods in - let rules = make_rule mkact prods in - let r = ExtendRule (entry, None, (pos, [(None, None, [rules])])) in - ([r], state) - -let tactic_grammar = - create_grammar_command "TacticGrammar" add_tactic_entry - -let extend_tactic_grammar kn ml ntn = extend_grammar_command 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 = function - | TacTerm s -> TacTerm s - | TacNonTerm (loc, (nt, sep), id) -> - let symbol = parse_user_entry nt sep in - let interp s = function - | None -> - if String.Map.mem s !entry_names then String.Map.find s !entry_names - else begin match ArgT.name s with - | None -> error ("Unknown entry "^s^".") - | Some arg -> arg - end - | Some n -> - (** FIXME: do better someday *) - assert (String.equal s "tactic"); - begin match Constrarg.wit_tactic with - | ExtraArg tag -> ArgT.Any tag - | _ -> assert false - end - in - let symbol = interp_entry_name interp symbol in - TacNonTerm (loc, symbol, id) - -let make_fresh_key = - let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in - fun prods -> - let cur = incr id; !id in - let map = function - | TacTerm s -> s - | TacNonTerm _ -> "#" - in - let prods = String.concat "_" (List.map map prods) in - (** We embed the hash of the kernel name in the label so that the identifier - should be mostly unique. This ensures that including two modules - together won't confuse the corresponding labels. *) - let hash = (cur lxor (ModPath.hash (Lib.current_mp ()))) land 0x7FFFFFFF in - let lbl = Id.of_string_soft (Printf.sprintf "%s_%08X" prods hash) in - Lib.make_kn lbl - -type tactic_grammar_obj = { - tacobj_key : KerName.t; - tacobj_local : locality_flag; - tacobj_tacgram : tactic_grammar; - 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 = - 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; - 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_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 (pprule tobj.tacobj_tacgram); - if Int.equal i 1 && not tobj.tacobj_local then - extend_tactic_grammar key tobj.tacobj_forml 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_glob_tactic_notation local n prods forml ids tac = - let parule = { - tacgram_level = n; - tacgram_prods = prods; - } in - let tacobj = { - tacobj_key = make_fresh_key prods; - tacobj_local = local; - tacobj_tacgram = parule; - 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 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 *) - -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 - | TacTerm s :: rem -> (s, rem) - | _ -> assert false (** Not handled by the ML extension syntax *) - in - let empty_value = function - | TacTerm s -> raise NonEmptyArgument - | TacNonTerm (_, symb, _) -> - let EntryName (typ, e) = prod_item_of_symbol 0 symb in - 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 add_ml_tactic_notation name prods = - let len = List.length prods in - let iter i prods = - let open Tacexpr in - let get_id = function - | TacTerm s -> None - | TacNonTerm (_, _, id) -> Some id - in - let ids = List.map_filter get_id prods in - let entry = { mltac_name = name; mltac_index = len - i - 1 } 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 (List.rev prods); - extend_atomic_tactic name prods - -(**********************************************************************) -(** Ltac quotations *) - -let ltac_quotations = ref String.Set.empty - -let create_ltac_quotation name cast (e, l) = - let () = - if String.Set.mem name !ltac_quotations then - failwith ("Ltac quotation " ^ name ^ " already registered") - in - let () = ltac_quotations := String.Set.add name !ltac_quotations in - let entry = match l with - | None -> Aentry e - | Some l -> Aentryl (e, l) - in -(* let level = Some "1" in *) - let level = None in - let assoc = None in - let rule = - Next (Next (Next (Next (Next (Stop, - Atoken (CLexer.terminal name)), - Atoken (CLexer.terminal ":")), - Atoken (CLexer.terminal "(")), - entry), - Atoken (CLexer.terminal ")")) - in - let action _ v _ _ _ loc = cast (loc, v) in - let gram = (level, assoc, [Rule (rule, action)]) in - Pcoq.grammar_extend Tactic.tactic_arg None (None, [gram]) - -(** Command *) - - -type tacdef_kind = - | NewTac of Id.t - | UpdateTac of Nametab.ltac_constant - -let is_defined_tac kn = - try ignore (Tacenv.interp_ltac kn); true with Not_found -> false - -let warn_unusable_identifier = - CWarnings.create ~name:"unusable-identifier" ~category:"parsing" - (fun id -> strbrk "The Ltac name" ++ spc () ++ pr_id id ++ spc () ++ - strbrk "may be unusable because of a conflict with a notation.") - -let register_ltac local tacl = - let map tactic_body = - match tactic_body with - | TacticDefinition ((loc,id), body) -> - let kn = Lib.make_kn id in - let id_pp = pr_id id in - let () = if is_defined_tac kn then - CErrors.user_err_loc (loc, "", - str "There is already an Ltac named " ++ id_pp ++ str".") - in - let is_shadowed = - try - match Pcoq.parse_string Pcoq.Tactic.tactic (Id.to_string id) with - | Tacexpr.TacArg _ -> false - | _ -> true (* most probably TacAtom, i.e. a primitive tactic ident *) - with e when CErrors.noncritical e -> true (* prim tactics with args, e.g. "apply" *) - in - let () = if is_shadowed then warn_unusable_identifier id in - NewTac id, body - | TacticRedefinition (ident, body) -> - let loc = loc_of_reference ident in - let kn = - try Nametab.locate_tactic (snd (qualid_of_reference ident)) - with Not_found -> - CErrors.user_err_loc (loc, "", - str "There is no Ltac named " ++ pr_reference ident ++ str ".") - in - UpdateTac kn, body - in - let rfun = List.map map tacl in - let recvars = - let fold accu (op, _) = match op with - | UpdateTac _ -> accu - | NewTac id -> (Lib.make_path id, Lib.make_kn id) :: accu - in - List.fold_left fold [] rfun - in - let ist = Tacintern.make_empty_glob_sign () in - let map (name, body) = - let body = Flags.with_option Tacintern.strict_check (Tacintern.intern_tactic_or_tacarg ist) body in - (name, body) - in - let defs () = - (** Register locally the tactic to handle recursivity. This function affects - the whole environment, so that we transactify it afterwards. *) - let iter_rec (sp, kn) = Nametab.push_tactic (Nametab.Until 1) sp kn in - let () = List.iter iter_rec recvars in - List.map map rfun - in - let defs = Future.transactify defs () in - let iter (def, tac) = match def with - | NewTac id -> - Tacenv.register_ltac false local id tac; - Flags.if_verbose Feedback.msg_info (Nameops.pr_id id ++ str " is defined") - | UpdateTac kn -> - Tacenv.redefine_ltac local kn tac; - let name = Nametab.shortest_qualid_of_tactic kn in - Flags.if_verbose Feedback.msg_info (Libnames.pr_qualid name ++ str " is redefined") - in - List.iter iter defs - -(** Queries *) - -let print_ltacs () = - let entries = KNmap.bindings (Tacenv.ltac_entries ()) in - let sort (kn1, _) (kn2, _) = KerName.compare kn1 kn2 in - let entries = List.sort sort entries in - let map (kn, entry) = - let qid = - try Some (Nametab.shortest_qualid_of_tactic kn) - with Not_found -> None - in - match qid with - | None -> None - | Some qid -> Some (qid, entry.Tacenv.tac_body) - in - let entries = List.map_filter map entries in - let pr_entry (qid, body) = - let (l, t) = match body with - | Tacexpr.TacFun (l, t) -> (l, t) - | _ -> ([], body) - in - let pr_ltac_fun_arg = function - | None -> spc () ++ str "_" - | Some id -> spc () ++ pr_id id - in - hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l) - in - Feedback.msg_notice (prlist_with_sep fnl pr_entry entries) |