diff options
Diffstat (limited to 'library/nametab.ml')
| -rw-r--r-- | library/nametab.ml | 142 |
1 files changed, 75 insertions, 67 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index fa5db37e..2046bf75 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * 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 *) +(* // * 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 CErrors @@ -16,14 +18,8 @@ open Globnames exception GlobalizationError of qualid -let error_global_not_found_loc loc q = - Loc.raise loc (GlobalizationError q) - -let error_global_not_found q = raise (GlobalizationError q) - -(* Kinds of global names *) - -type ltac_constant = kernel_name +let error_global_not_found {CAst.loc;v} = + Loc.raise ?loc (GlobalizationError v) (* The visibility can be registered either - for all suffixes not shorter then a given int - when the object @@ -87,8 +83,9 @@ struct Module F (X : S). Module X. The argument X of the functor F is masked by the inner module X. *) - let masking_absolute n = - Flags.if_verbose Feedback.msg_info (str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) + let warn_masking_absolute = + CWarnings.create ~name:"masking-absolute-name" ~category:"deprecated" + (fun n -> str ("Trying to mask the absolute name \"" ^ U.to_string n ^ "\"!")) type user_name = U.t @@ -127,7 +124,7 @@ struct | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - masking_absolute n; tree.path + warn_masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) else tree.path @@ -145,8 +142,8 @@ struct (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) (* But ours is also absolute! This is an error! *) - error ("Cannot mask the absolute name \"" - ^ U.to_string uname' ^ "\"!") + user_err Pp.(str @@ "Cannot mask the absolute name \"" + ^ U.to_string uname' ^ "\"!") | Nothing | Relative _ -> mktree (Absolute (uname,o)) tree.map @@ -160,7 +157,7 @@ let rec push_exactly uname o level tree = function | Absolute (n,_) -> (* This is an absolute name, we must keep it otherwise it may become unaccessible forever *) - masking_absolute n; tree.path + warn_masking_absolute n; tree.path | Nothing | Relative _ -> Relative (uname,o) in @@ -276,19 +273,14 @@ struct end module ExtRefEqual = ExtRefOrdered -module KnEqual = Names.KerName module MPEqual = Names.ModPath module ExtRefTab = Make(FullPath)(ExtRefEqual) -module KnTab = Make(FullPath)(KnEqual) module MPTab = Make(FullPath)(MPEqual) type ccitab = ExtRefTab.t let the_ccitab = ref (ExtRefTab.empty : ccitab) -type kntab = KnTab.t -let the_tactictab = ref (KnTab.empty : kntab) - type mptab = MPTab.t let the_modtypetab = ref (MPTab.empty : mptab) @@ -296,7 +288,7 @@ module DirPath' = struct include DirPath let repr dir = match DirPath.repr dir with - | [] -> anomaly (Pp.str "Empty dirpath") + | [] -> anomaly (Pp.str "Empty dirpath.") | id :: l -> (id, l) end @@ -313,6 +305,16 @@ module DirTab = Make(DirPath')(GlobDir) type dirtab = DirTab.t let the_dirtab = ref (DirTab.empty : dirtab) +type universe_id = DirPath.t * int + +module UnivIdEqual = +struct + type t = universe_id + let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i' +end +module UnivTab = Make(FullPath)(UnivIdEqual) +type univtab = UnivTab.t +let the_univtab = ref (UnivTab.empty : univtab) (* Reversed name tables ***************************************************) @@ -329,9 +331,20 @@ let the_modrevtab = ref (MPmap.empty : mprevtab) type mptrevtab = full_path MPmap.t let the_modtyperevtab = ref (MPmap.empty : mptrevtab) -type knrevtab = full_path KNmap.t -let the_tacticrevtab = ref (KNmap.empty : knrevtab) +module UnivIdOrdered = +struct + type t = universe_id + let hash (d, i) = i + DirPath.hash d + let compare (d, i) (d', i') = + let c = Int.compare i i' in + if Int.equal c 0 then DirPath.compare d d' + else c +end + +module UnivIdMap = HMap.Make(UnivIdOrdered) +type univrevtab = full_path UnivIdMap.t +let the_univrevtab = ref (UnivIdMap.empty : univrevtab) (* Push functions *********************************************************) @@ -370,20 +383,18 @@ let push_modtype vis sp kn = the_modtypetab := MPTab.push vis sp kn !the_modtypetab; the_modtyperevtab := MPmap.add kn sp !the_modtyperevtab -(* This is for tactic definition names *) - -let push_tactic vis sp kn = - the_tactictab := KnTab.push vis sp kn !the_tactictab; - the_tacticrevtab := KNmap.add kn sp !the_tacticrevtab - - (* This is to remember absolute Section/Module names and to avoid redundancy *) let push_dir vis dir dir_ref = the_dirtab := DirTab.push vis dir dir_ref !the_dirtab; match dir_ref with - DirModule (_,(mp,_)) -> the_modrevtab := MPmap.add mp dir !the_modrevtab - | _ -> () + | DirModule { obj_mp; _ } -> the_modrevtab := MPmap.add obj_mp dir !the_modrevtab + | _ -> () + +(* This is for global universe names *) +let push_universe vis sp univ = + the_univtab := UnivTab.push vis sp univ !the_univtab; + the_univrevtab := UnivIdMap.add univ sp !the_univrevtab (* Locate functions *******************************************************) @@ -404,23 +415,23 @@ let locate_syndef qid = match locate_extended qid with let locate_modtype qid = MPTab.locate qid !the_modtypetab let full_name_modtype qid = MPTab.user_name qid !the_modtypetab -let locate_tactic qid = KnTab.locate qid !the_tactictab +let locate_universe qid = UnivTab.locate qid !the_univtab let locate_dir qid = DirTab.locate qid !the_dirtab let locate_module qid = match locate_dir qid with - | DirModule (_,(mp,_)) -> mp + | DirModule { obj_mp ; _} -> obj_mp | _ -> raise Not_found let full_name_module qid = match locate_dir qid with - | DirModule (dir,_) -> dir + | DirModule { obj_dir ; _} -> obj_dir | _ -> raise Not_found let locate_section qid = match locate_dir qid with - | DirOpenSection (dir, _) + | DirOpenSection { obj_dir; _ } -> obj_dir | DirClosedSection dir -> dir | _ -> raise Not_found @@ -430,8 +441,6 @@ let locate_all qid = let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab -let locate_extended_all_tactic qid = KnTab.find_prefixes qid !the_tactictab - let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab @@ -450,16 +459,16 @@ let global_of_path sp = let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab -let global r = - let (loc,qid) = qualid_of_reference r in - try match locate_extended qid with +let global ({CAst.loc;v=r} as lr)= + let {CAst.loc; v} as qid = qualid_of_reference lr in + try match locate_extended v with | TrueGlobal ref -> ref | SynDef _ -> - user_err_loc (loc,"global", - str "Unexpected reference to a notation: " ++ - pr_qualid qid) + user_err ?loc ~hdr:"global" + (str "Unexpected reference to a notation: " ++ + pr_qualid v) with Not_found -> - error_global_not_found_loc loc qid + error_global_not_found qid (* Exists functions ********************************************************) @@ -473,7 +482,7 @@ let exists_module = exists_dir let exists_modtype sp = MPTab.exists sp !the_modtypetab -let exists_tactic kn = KnTab.exists kn !the_tactictab +let exists_universe kn = UnivTab.exists kn !the_univtab (* Reverse locate functions ***********************************************) @@ -494,12 +503,12 @@ let path_of_syndef kn = let dirpath_of_module mp = MPmap.find mp !the_modrevtab -let path_of_tactic kn = - KNmap.find kn !the_tacticrevtab - let path_of_modtype mp = MPmap.find mp !the_modtyperevtab +let path_of_universe mp = + UnivIdMap.find mp !the_univrevtab + (* Shortest qualid functions **********************************************) let shortest_qualid_of_global ctx ref = @@ -521,50 +530,49 @@ let shortest_qualid_of_modtype kn = let sp = MPmap.find kn !the_modtyperevtab in MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_tactic kn = - let sp = KNmap.find kn !the_tacticrevtab in - KnTab.shortest_qualid Id.Set.empty sp !the_tactictab +let shortest_qualid_of_universe kn = + let sp = UnivIdMap.find kn !the_univrevtab in + UnivTab.shortest_qualid Id.Set.empty sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e -let global_inductive r = - match global r with +let global_inductive ({CAst.loc; v=r} as lr) = + match global lr with | IndRef ind -> ind | ref -> - user_err_loc (loc_of_reference r,"global_inductive", - pr_reference r ++ spc () ++ str "is not an inductive type") - + user_err ?loc ~hdr:"global_inductive" + (pr_reference lr ++ spc () ++ str "is not an inductive type") (********************************************************************) (********************************************************************) (* Registration of tables as a global table and rollback *) -type frozen = ccitab * dirtab * mptab * kntab - * globrevtab * mprevtab * mptrevtab * knrevtab +type frozen = ccitab * dirtab * mptab * univtab + * globrevtab * mprevtab * mptrevtab * univrevtab let freeze _ : frozen = !the_ccitab, !the_dirtab, !the_modtypetab, - !the_tactictab, + !the_univtab, !the_globrevtab, !the_modrevtab, !the_modtyperevtab, - !the_tacticrevtab + !the_univrevtab -let unfreeze (ccit,dirt,mtyt,tact,globr,modr,mtyr,tacr) = +let unfreeze (ccit,dirt,mtyt,univt,globr,modr,mtyr,univr) = the_ccitab := ccit; the_dirtab := dirt; the_modtypetab := mtyt; - the_tactictab := tact; + the_univtab := univt; the_globrevtab := globr; the_modrevtab := modr; the_modtyperevtab := mtyr; - the_tacticrevtab := tacr + the_univrevtab := univr let _ = Summary.declare_summary "names" |