diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 14:06:29 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-10-03 18:59:00 +0200 |
commit | 1a6a26d29252da54b86bf663a66ddd909905d1cb (patch) | |
tree | 2489daca9a966cf869025a535f98f5799ff13ceb /plugins/ltac | |
parent | 2b9a34e2ffb2bf066b3b0f8452e35622519cae1c (diff) |
Moving the Ltac-specific part of the nametab to the Ltac plugin.
For now, a few vernacular features were lot in the process, like locating
Ltac definitions. This will be fixed in an upcoming commit.
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/ltac_plugin.mlpack | 4 | ||||
-rw-r--r-- | plugins/ltac/pptactic.ml | 2 | ||||
-rw-r--r-- | plugins/ltac/pptactic.mli | 2 | ||||
-rw-r--r-- | plugins/ltac/tacentries.ml | 10 | ||||
-rw-r--r-- | plugins/ltac/tacenv.ml | 44 | ||||
-rw-r--r-- | plugins/ltac/tacenv.mli | 10 | ||||
-rw-r--r-- | plugins/ltac/tacexpr.mli | 3 | ||||
-rw-r--r-- | plugins/ltac/tacintern.ml | 6 |
8 files changed, 64 insertions, 17 deletions
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack index 12b4c81fc..3972b7aac 100644 --- a/plugins/ltac/ltac_plugin.mlpack +++ b/plugins/ltac/ltac_plugin.mlpack @@ -1,9 +1,9 @@ Tacarg +Tacsubst +Tacenv Pptactic Pltac Taccoerce -Tacsubst -Tacenv Tactic_debug Tacintern Tacentries diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d8bd16620..d588c888c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -336,7 +336,7 @@ type 'a extra_genarg_printer = let pr_ltac_constant kn = if !Flags.in_debugger then KerName.print kn else try - pr_qualid (Nametab.shortest_qualid_of_tactic kn) + pr_qualid (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) str "<" ++ KerName.print kn ++ str ">" diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index c79d5b389..d9da954fe 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -93,7 +93,7 @@ val pr_alias_key : Names.KerName.t -> Pp.t val pr_alias : (Val.t -> Pp.t) -> int -> Names.KerName.t -> Val.t list -> Pp.t -val pr_ltac_constant : Nametab.ltac_constant -> Pp.t +val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : raw_tactic_expr -> Pp.t diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index a8d518fbd..8573da19f 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -409,7 +409,7 @@ let create_ltac_quotation name cast (e, l) = type tacdef_kind = | NewTac of Id.t - | UpdateTac of Nametab.ltac_constant + | UpdateTac of Tacexpr.ltac_constant let is_defined_tac kn = try ignore (Tacenv.interp_ltac kn); true with Not_found -> false @@ -441,7 +441,7 @@ let register_ltac local tacl = | Tacexpr.TacticRedefinition (ident, body) -> let loc = loc_of_reference ident in let kn = - try Nametab.locate_tactic (snd (qualid_of_reference ident)) + try Tacenv.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> CErrors.user_err ?loc (str "There is no Ltac named " ++ pr_reference ident ++ str ".") @@ -464,7 +464,7 @@ let register_ltac local tacl = 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 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 @@ -475,7 +475,7 @@ let register_ltac local tacl = Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> Tacenv.redefine_ltac local kn tac; - let name = Nametab.shortest_qualid_of_tactic kn in + 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 @@ -488,7 +488,7 @@ let print_ltacs () = let entries = List.sort sort entries in let map (kn, entry) = let qid = - try Some (Nametab.shortest_qualid_of_tactic kn) + try Some (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> None in match qid with diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml index 13b44f0e2..8c59a36fa 100644 --- a/plugins/ltac/tacenv.ml +++ b/plugins/ltac/tacenv.ml @@ -11,6 +11,42 @@ open Pp open Names open Tacexpr +(** Nametab for tactics *) + +(** TODO: Share me somewhere *) +module FullPath = +struct + open Libnames + type t = full_path + let equal = eq_full_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (DirPath.repr dir) +end + +module KnTab = Nametab.Make(FullPath)(KerName) + +let tactic_tab = Summary.ref ~name:"LTAC-NAMETAB" (KnTab.empty, KNmap.empty) + +let push_tactic vis sp kn = + let (tab, revtab) = !tactic_tab in + let tab = KnTab.push vis sp kn tab in + let revtab = KNmap.add kn sp revtab in + tactic_tab := (tab, revtab) + +let locate_tactic qid = KnTab.locate qid (fst !tactic_tab) + +let locate_extended_all_tactic qid = KnTab.find_prefixes qid (fst !tactic_tab) + +let exists_tactic kn = KnTab.exists kn (fst !tactic_tab) + +let path_of_tactic kn = KNmap.find kn (snd !tactic_tab) + +let shortest_qualid_of_tactic kn = + let sp = KNmap.find kn (snd !tactic_tab) in + KnTab.shortest_qualid Id.Set.empty sp (fst !tactic_tab) + (** Tactic notations (TacAlias) *) type alias = KerName.t @@ -103,19 +139,19 @@ let replace kn path t = 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 + let () = if not local then push_tactic (Until i) sp kn in add kn b t | Some kn0 -> replace kn0 kn 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 + let () = if not local then push_tactic (Exactly i) sp kn in add kn b t | Some kn0 -> replace kn0 kn t let cache_md ((sp, kn), (local, id ,b, t)) = match id with | None -> - let () = Nametab.push_tactic (Until 1) sp kn in + let () = push_tactic (Until 1) sp kn in add kn b t | Some kn0 -> replace kn0 kn t @@ -128,7 +164,7 @@ let subst_md (subst, (local, id, b, t)) = let classify_md (local, _, _, _ as o) = Substitute o -let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj = +let inMD : bool * ltac_constant option * bool * glob_tactic_expr -> obj = declare_object {(default_object "TAC-DEFINITION") with cache_function = cache_md; load_function = load_md; diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli index 958109e5a..4ecc978fe 100644 --- a/plugins/ltac/tacenv.mli +++ b/plugins/ltac/tacenv.mli @@ -7,11 +7,21 @@ (************************************************************************) open Names +open Libnames open Tacexpr open Geninterp (** This module centralizes the various ways of registering tactics. *) +(** {5 Tactic naming} *) + +val push_tactic : Nametab.visibility -> full_path -> ltac_constant -> unit +val locate_tactic : qualid -> ltac_constant +val locate_extended_all_tactic : qualid -> ltac_constant list +val exists_tactic : full_path -> bool +val path_of_tactic : ltac_constant -> full_path +val shortest_qualid_of_tactic : ltac_constant -> qualid + (** {5 Tactic notations} *) type alias = KerName.t diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 64da097de..2c36faeff 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -10,13 +10,14 @@ open Loc open Names open Constrexpr open Libnames -open Nametab open Genredexpr open Genarg open Pattern open Misctypes open Locus +type ltac_constant = KerName.t + type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index fc6ee6aab..99d7684d3 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -118,7 +118,7 @@ let intern_constr_reference strict ist = function let intern_isolated_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - TacCall (Loc.tag ?loc (ArgArg (loc,locate_tactic qid),[])) + TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) let intern_isolated_tactic_reference strict ist r = (* An ltac reference *) @@ -137,7 +137,7 @@ let intern_isolated_tactic_reference strict ist r = let intern_applied_global_tactic_reference r = let (loc,qid) = qualid_of_reference r in - ArgArg (loc,locate_tactic qid) + ArgArg (loc,Tacenv.locate_tactic qid) let intern_applied_tactic_reference ist r = (* An ltac reference *) @@ -722,7 +722,7 @@ let pr_ltac_fun_arg n = spc () ++ Name.print n let print_ltac id = try - let kn = Nametab.locate_tactic id in + let kn = Tacenv.locate_tactic id in let entries = Tacenv.ltac_entries () in let tac = KNmap.find kn entries in let filter mp = |