summaryrefslogtreecommitdiff
path: root/plugins/ltac/tacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/tacentries.ml')
-rw-r--r--plugins/ltac/tacentries.ml690
1 files changed, 690 insertions, 0 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
new file mode 100644
index 00000000..e510b9f5
--- /dev/null
+++ b/plugins/ltac/tacentries.ml
@@ -0,0 +1,690 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Libobject
+open Genarg
+open Extend
+open Pcoq
+open Egramml
+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 ('a * Names.Id.t option) Loc.located
+
+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 Pltac.binder_tactic
+ else Aentryl (Pltac.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 Tacarg.wit_tactic, Aself)
+ else if check_lvl (n + 1) then EntryName (rawwit Tacarg.wit_tactic, Anext)
+ else EntryName (rawwit Tacarg.wit_tactic, atactic n)
+
+let get_separator = function
+| None -> user_err Pp.(str "Missing separator.")
+| Some sep -> sep
+
+let check_separator ?loc = function
+| None -> ()
+| Some _ -> user_err ?loc (str "Separator is only for arguments with suffix _list_sep.")
+
+let rec parse_user_entry ?loc 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 ?loc (String.sub s 3 (l-8)) None in
+ check_separator ?loc sep;
+ Ulist1 entry
+ else if l > 12 && coincide s "ne_" 0 &&
+ coincide s "_list_sep" (l-9) then
+ let entry = parse_user_entry ?loc (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 ?loc (String.sub s 0 (l-5)) None in
+ check_separator ?loc sep;
+ Ulist0 entry
+ else if l > 9 && coincide s "_list_sep" (l-9) then
+ let entry = parse_user_entry ?loc (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 ?loc (String.sub s 0 (l-4)) None in
+ check_separator ?loc sep;
+ 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
+ check_separator ?loc sep;
+ Uentryl ("tactic", n)
+ else
+ let _ = check_separator ?loc sep in
+ Uentry s
+
+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
+ Pltac.simple_tactic, None
+ else if Int.equal n 5 then
+ Pltac.binder_tactic, None
+ else if 1<=n && n<5 then
+ Pltac.tactic_expr, Some (Extend.Level (string_of_int n))
+ else
+ user_err Pp.(str ("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 Tacarg.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.tag ~loc (kn,l)):raw_tactic_expr)
+ in
+ let () =
+ if Int.equal tg.tacgram_level 0 && not (head_is_ident tg) then
+ user_err Pp.(str "Notation for simple tactic must start with an identifier.")
+ in
+ let map = function
+ | TacTerm s -> GramTerminal s
+ | TacNonTerm (loc, (s, ido)) ->
+ let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
+ GramNonTerminal (Loc.tag ?loc @@ (Option.map (fun _ -> typ) ido, 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), ido)) ->
+ let symbol = parse_user_entry ?loc 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 -> user_err Pp.(str ("Unknown entry "^s^"."))
+ | Some arg -> arg
+ end
+ | Some n ->
+ (** FIXME: do better someday *)
+ assert (String.equal s "tactic");
+ begin match Tacarg.wit_tactic with
+ | ExtraArg tag -> ArgT.Any tag
+ end
+ in
+ let symbol = interp_entry_name interp symbol in
+ TacNonTerm (loc, (symbol, ido))
+
+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
+ user_err Pp.(str "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 (_, (_, ido)) -> ido
+
+let add_glob_tactic_notation local ~level prods forml ids tac =
+ let parule = {
+ tacgram_level = level;
+ 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 ~level: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.tag @@ 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.tag (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 ~level prods =
+ let len = List.length prods in
+ let iter i prods =
+ let open Tacexpr in
+ let get_id = function
+ | TacTerm s -> None
+ | TacNonTerm (_, (_, ido)) -> ido
+ 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 (CAst.make id)) in
+ let tac = TacML (Loc.tag (entry, List.map map ids)) in
+ add_glob_tactic_notation false ~level prods true ids tac
+ in
+ List.iteri iter (List.rev prods);
+ (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
+ tactic_expr level 0) *)
+ if Int.equal level 0 then 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 (Some loc, v) in
+ let gram = (level, assoc, [Rule (rule, action)]) in
+ Pcoq.grammar_extend Pltac.tactic_arg None (None, [gram])
+
+(** Command *)
+
+
+type tacdef_kind =
+ | NewTac of Id.t
+ | UpdateTac of Tacexpr.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 () ++ Id.print 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
+ | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) ->
+ let kn = Lib.make_kn id in
+ let id_pp = Id.print id in
+ let () = if is_defined_tac kn then
+ CErrors.user_err ?loc
+ (str "There is already an Ltac named " ++ id_pp ++ str".")
+ in
+ let is_shadowed =
+ try
+ match Pcoq.parse_string Pltac.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
+ | Tacexpr.TacticRedefinition (ident, body) ->
+ let kn =
+ try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v
+ with Not_found ->
+ CErrors.user_err ?loc:ident.CAst.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) = Tacenv.push_tactic (Nametab.Until 1) sp kn in
+ let () = List.iter iter_rec recvars in
+ List.map map rfun
+ in
+ (* STATE XXX: Review what is going on here. Why does this needs
+ protection? Why is not the STM level protection enough? Fishy *)
+ let defs = States.with_state_protection defs () in
+ let iter (def, tac) = match def with
+ | NewTac id ->
+ Tacenv.register_ltac false local id tac;
+ Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
+ | UpdateTac kn ->
+ Tacenv.redefine_ltac local kn tac;
+ let name = Tacenv.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 (Tacenv.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 n = spc () ++ Name.print n in
+ hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
+ in
+ Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
+
+let locatable_ltac = "Ltac"
+
+let () =
+ let open Prettyp in
+ let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
+ let locate_all = Tacenv.locate_extended_all_tactic in
+ let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
+ let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
+ let print kn =
+ let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
+ Tacintern.print_ltac qid
+ in
+ let about = name in
+ register_locatable locatable_ltac {
+ locate;
+ locate_all;
+ shortest_qualid;
+ name;
+ print;
+ about;
+ }
+
+let print_located_tactic qid =
+ Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
+
+(** Grammar *)
+
+let () =
+ let entries = [
+ AnyEntry Pltac.tactic_expr;
+ AnyEntry Pltac.binder_tactic;
+ AnyEntry Pltac.simple_tactic;
+ AnyEntry Pltac.tactic_arg;
+ ] in
+ register_grammars_by_name "tactic" entries
+
+type _ ty_sig =
+| TyNil : (Geninterp.interp_sign -> unit Proofview.tactic) ty_sig
+| TyIdent : string * 'r ty_sig -> 'r ty_sig
+| TyArg :
+ (('a, 'b, 'c) Extend.ty_user_symbol * Id.t) Loc.located * 'r ty_sig -> ('c -> 'r) ty_sig
+| TyAnonArg :
+ ('a, 'b, 'c) Extend.ty_user_symbol Loc.located * 'r ty_sig -> 'r ty_sig
+
+type ty_ml = TyML : 'r ty_sig * 'r -> ty_ml
+
+let rec untype_user_symbol : type a b c. (a,b,c) ty_user_symbol -> Genarg.ArgT.any user_symbol = fun tu ->
+ match tu with
+ | TUlist1 l -> Ulist1(untype_user_symbol l)
+ | TUlist1sep(l,s) -> Ulist1sep(untype_user_symbol l, s)
+ | TUlist0 l -> Ulist0(untype_user_symbol l)
+ | TUlist0sep(l,s) -> Ulist0sep(untype_user_symbol l, s)
+ | TUopt(o) -> Uopt(untype_user_symbol o)
+ | TUentry a -> Uentry (Genarg.ArgT.Any a)
+ | TUentryl (a,i) -> Uentryl (Genarg.ArgT.Any a,i)
+
+let rec clause_of_sign : type a. a ty_sig -> Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list =
+ fun sign -> match sign with
+ | TyNil -> []
+ | TyIdent (s, sig') -> TacTerm s :: clause_of_sign sig'
+ | TyArg ((loc,(a,id)),sig') ->
+ TacNonTerm (loc,(untype_user_symbol a,Some id)) :: clause_of_sign sig'
+ | TyAnonArg ((loc,a),sig') ->
+ TacNonTerm (loc,(untype_user_symbol a,None)) :: clause_of_sign sig'
+
+let clause_of_ty_ml = function
+ | TyML (t,_) -> clause_of_sign t
+
+let rec prj : type a b c. (a,b,c) Extend.ty_user_symbol -> (a,b,c) genarg_type = function
+ | TUentry a -> ExtraArg a
+ | TUentryl (a,l) -> ExtraArg a
+ | TUopt(o) -> OptArg (prj o)
+ | TUlist1 l -> ListArg (prj l)
+ | TUlist1sep (l,_) -> ListArg (prj l)
+ | TUlist0 l -> ListArg (prj l)
+ | TUlist0sep (l,_) -> ListArg (prj l)
+
+let rec eval_sign : type a. a ty_sig -> a -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic =
+ fun sign tac ->
+ match sign with
+ | TyNil ->
+ begin fun vals ist -> match vals with
+ | [] -> tac ist
+ | _ :: _ -> assert false
+ end
+ | TyIdent (s, sig') -> eval_sign sig' tac
+ | TyArg ((_loc,(a,id)), sig') ->
+ let f = eval_sign sig' in
+ begin fun tac vals ist -> match vals with
+ | [] -> assert false
+ | v :: vals ->
+ let v' = Taccoerce.Value.cast (topwit (prj a)) v in
+ f (tac v') vals ist
+ end tac
+ | TyAnonArg ((_loc,a), sig') -> eval_sign sig' tac
+
+let eval : ty_ml -> Geninterp.Val.t list -> Geninterp.interp_sign -> unit Proofview.tactic = function
+ | TyML (t,tac) -> eval_sign t tac
+
+let is_constr_entry = function
+| TUentry a -> Option.has_some @@ genarg_type_eq (ExtraArg a) Stdarg.wit_constr
+| _ -> false
+
+let rec only_constr : type a. a ty_sig -> bool = function
+| TyNil -> true
+| TyIdent(_,_) -> false
+| TyArg((_,(u,_)),s) -> if is_constr_entry u then only_constr s else false
+| TyAnonArg((_,u),s) -> if is_constr_entry u then only_constr s else false
+
+let rec mk_sign_vars : type a. a ty_sig -> Name.t list = function
+| TyNil -> []
+| TyIdent (_,s) -> mk_sign_vars s
+| TyArg((_,(_,name)),s) -> Name name :: mk_sign_vars s
+| TyAnonArg((_,_),s) -> Anonymous :: mk_sign_vars s
+
+let dummy_id = Id.of_string "_"
+
+let lift_constr_tac_to_ml_tac vars tac =
+ let tac _ ist = Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Tacmach.New.project gl in
+ let map = function
+ | Anonymous -> None
+ | Name id ->
+ let c = Id.Map.find id ist.Geninterp.lfun in
+ try Some (Taccoerce.Value.of_constr @@ Taccoerce.coerce_to_closed_constr env c)
+ with Taccoerce.CannotCoerceTo ty ->
+ Taccoerce.error_ltac_variable dummy_id (Some (env,sigma)) c ty
+ in
+ let args = List.map_filter map vars in
+ tac args ist
+ end in
+ tac
+
+let tactic_extend plugin_name tacname ~level sign =
+ let open Tacexpr in
+ let ml_tactic_name =
+ { mltac_tactic = tacname;
+ mltac_plugin = plugin_name }
+ in
+ match sign with
+ | [TyML (TyIdent (name, s),tac) as ml_tac] when only_constr s ->
+ (** The extension is only made of a name followed by constr entries: we do not
+ add any grammar nor printing rule and add it as a true Ltac definition. *)
+ (*
+ let patt = make_patt rem in
+ let vars = List.map make_var rem in
+ let vars = mlexpr_of_list (mlexpr_of_name mlexpr_of_ident) vars in
+ *)
+ let vars = mk_sign_vars s in
+ let ml = { Tacexpr.mltac_name = ml_tactic_name; Tacexpr.mltac_index = 0 } in
+ let tac = match s with
+ | TyNil -> eval ml_tac
+ (** Special handling of tactics without arguments: such tactics do not do
+ a Proofview.Goal.nf_enter to compute their arguments. It matters for some
+ whole-prof tactics like [shelve_unifiable]. *)
+ | _ -> lift_constr_tac_to_ml_tac vars (eval ml_tac)
+ in
+ (** Arguments are not passed directly to the ML tactic in the TacML node,
+ the ML tactic retrieves its arguments in the [ist] environment instead.
+ This is the rôle of the [lift_constr_tac_to_ml_tac] function. *)
+ let body = Tacexpr.TacFun (vars, Tacexpr.TacML (Loc.tag (ml, [])))in
+ let id = Names.Id.of_string name in
+ let obj () = Tacenv.register_ltac true false id body in
+ let () = Tacenv.register_ml_tactic ml_tactic_name [|tac|] in
+ Mltop.declare_cache_obj obj plugin_name
+ | _ ->
+ let obj () = add_ml_tactic_notation ml_tactic_name ~level (List.map clause_of_ty_ml sign) in
+ Tacenv.register_ml_tactic ml_tactic_name @@ Array.of_list (List.map eval sign);
+ Mltop.declare_cache_obj obj plugin_name
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-07 13:05:36 +0000