From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 29 Dec 2018 14:31:27 -0500 Subject: Imported Upstream version 8.8.2 --- plugins/ltac/tacentries.ml | 690 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 690 insertions(+) create mode 100644 plugins/ltac/tacentries.ml (limited to 'plugins/ltac/tacentries.ml') 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 *) +(* 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 -- cgit v1.2.3