diff options
Diffstat (limited to 'tactics/tacenv.ml')
-rw-r--r-- | tactics/tacenv.ml | 128 |
1 files changed, 128 insertions, 0 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml new file mode 100644 index 00000000..cb20fc93 --- /dev/null +++ b/tactics/tacenv.ml @@ -0,0 +1,128 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Genarg +open Pp +open Names +open Tacexpr + +(** Tactic notations (TacAlias) *) + +type alias = KerName.t + +let alias_map = Summary.ref ~name:"tactic-alias" + (KNmap.empty : glob_tactic_expr KNmap.t) + +let register_alias key tac = + alias_map := KNmap.add key tac !alias_map + +let interp_alias key = + try KNmap.find key !alias_map + with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) + +(** ML tactic extensions (TacML) *) + +type ml_tactic = + typed_generic_argument list -> Geninterp.interp_sign -> unit Proofview.tactic + +module MLName = +struct + type t = ml_tactic_name + let compare tac1 tac2 = + let c = String.compare tac1.mltac_tactic tac2.mltac_tactic in + if c = 0 then String.compare tac1.mltac_plugin tac2.mltac_plugin + else c +end + +module MLTacMap = Map.Make(MLName) + +let pr_tacname t = + t.mltac_plugin ^ "::" ^ t.mltac_tactic + +let tac_tab = ref MLTacMap.empty + +let register_ml_tactic ?(overwrite = false) s (t : ml_tactic) = + let () = + if MLTacMap.mem s !tac_tab then + if overwrite then + let () = tac_tab := MLTacMap.remove s !tac_tab in + msg_warning (str ("Overwriting definition of tactic " ^ pr_tacname s)) + else + Errors.anomaly (str ("Cannot redeclare tactic " ^ pr_tacname s ^ ".")) + in + tac_tab := MLTacMap.add s t !tac_tab + +let interp_ml_tactic s = + try + MLTacMap.find s !tac_tab + with Not_found -> + Errors.errorlabstrm "" + (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.") + +(***************************************************************************) +(* Tactic registration *) + +(* Summary and Object declaration *) + +open Nametab +open Libnames +open Libobject + +let mactab = + Summary.ref (KNmap.empty : (bool * glob_tactic_expr) KNmap.t) + ~name:"tactic-definition" + +let interp_ltac r = snd (KNmap.find r !mactab) + +let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab) + +(* Declaration of the TAC-DEFINITION object *) +let add (kn,td) = mactab := KNmap.add kn td !mactab +let replace (kn,td) = mactab := KNmap.add kn td !mactab + +let load_md i ((sp, kn), (local, id, b, t)) = match id with +| None -> + let () = if not local then Nametab.push_tactic (Until i) sp kn in + add (kn, (b,t)) +| Some kn -> add (kn, (b,t)) + +let open_md i ((sp, kn), (local, id, b, t)) = match id with +| None -> + let () = if not local then Nametab.push_tactic (Exactly i) sp kn in + add (kn, (b,t)) +| Some kn -> add (kn, (b,t)) + +let cache_md ((sp, kn), (local, id ,b, t)) = match id with +| None -> + let () = Nametab.push_tactic (Until 1) sp kn in + add (kn, (b,t)) +| Some kn -> add (kn, (b,t)) + +let subst_kind subst id = match id with +| None -> None +| Some kn -> Some (Mod_subst.subst_kn subst kn) + +let subst_md (subst, (local, id, b, t)) = + (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t) + +let classify_md (local, _, _, _ as o) = Substitute o + +let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj = + declare_object {(default_object "TAC-DEFINITION") with + cache_function = cache_md; + load_function = load_md; + open_function = open_md; + subst_function = subst_md; + classify_function = classify_md} + +let register_ltac for_ml local id tac = + ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac))) + +let redefine_ltac local kn tac = + Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac)) |