Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: nametab.ml Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   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 CErrors
open Util
open Pp
open Names
open Libnames
open Globnames

type object_prefix = {
  obj_dir : DirPath.t;
  obj_mp  : ModPath.t;
  obj_sec : DirPath.t;
}

let eq_op op1 op2 =
  DirPath.equal op1.obj_dir op2.obj_dir &&
  DirPath.equal op1.obj_sec op2.obj_sec &&
  ModPath.equal op1.obj_mp  op2.obj_mp

(* to this type are mapped DirPath.t's in the nametab *)
module GlobDirRef = struct
  type t =
    | DirOpenModule of object_prefix
    | DirOpenModtype of object_prefix
    | DirOpenSection of object_prefix
    | DirModule of object_prefix

  let equal r1 r2 = match r1, r2 with
    | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2
    | DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2
    | DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2
    | DirModule op1, DirModule op2 -> eq_op op1 op2
    | _ -> false

end

type global_dir_reference = GlobDirRef.t
[@@ocaml.deprecated "Use [GlobDirRef.t]"]

let eq_global_dir_reference = GlobDirRef.equal
[@@ocaml.deprecated "Use [GlobDirRef.equal]"]

exception GlobalizationError of qualid

let error_global_not_found qid =
  Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid)

(* The visibility can be registered either
   - for all suffixes not shorter then a given int - when the object
     is loaded inside a module
   or
   - for a precise suffix, when the module containing (the module
     containing ...) the object is open (imported)
*)
type visibility = Until of int | Exactly of int

let map_visibility f = function
  | Until i -> Until (f i)
  | Exactly i -> Exactly (f i)

(* Data structure for nametabs *******************************************)

(* This module type will be instantiated by [full_path] of [DirPath.t] *)
(* The [repr] function is assumed to return the reversed list of idents. *)
module type UserName = sig
  type t
  val equal : t -> t -> bool
  val to_string : t -> string
  val repr : t -> Id.t * module_ident list
end

module type EqualityType =
sig
  type t
  val equal : t -> t -> bool
end

(* A ['a t] is a map from [user_name] to ['a], with possible lookup by
   partially qualified names of type [qualid]. The mapping of
   partially qualified names to ['a] is determined by the [visibility]
   parameter of [push].

   The [shortest_qualid] function given a user_name Coq.A.B.x, tries
   to find the shortest among x, B.x, A.B.x and Coq.A.B.x that denotes
   the same object.
*)
module type NAMETREE = sig
  type elt
  type t
  type user_name

  val empty : t
  val push : visibility -> user_name -> elt -> t -> t
  val locate : qualid -> t -> elt
  val find : user_name -> t -> elt
  val exists : user_name -> t -> bool
  val user_name : qualid -> t -> user_name
  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
  val find_prefixes : qualid -> t -> elt list

  (** Matches a prefix of [qualid], useful for completion *)
  val match_prefixes : qualid -> t -> elt list
end

module Make (U : UserName) (E : EqualityType) : NAMETREE
  with type user_name = U.t and type elt = E.t =
struct
  type elt = E.t

  (* A name became inaccessible, even with absolute qualification.
     Example:
     Module F (X : S). Module X.
     The argument X of the functor F is masked by the inner module X.
   *)
  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

  type path_status =
      Nothing
    | Relative of user_name * elt
    | Absolute of user_name * elt

  (* Dictionaries of short names *)
  type nametree =
      { path : path_status;
map : nametree ModIdmap.t }

  let mktree p m = { path=p; map=m }
  let empty_tree = mktree Nothing ModIdmap.empty

  type t = nametree Id.Map.t

  let empty = Id.Map.empty

  (* [push_until] is used to register [Until vis] visibility and
     [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)

  let rec push_until uname o level tree = function
    | modid :: path ->
        let modify _ mc = push_until uname o (level-1) mc path in
        let map =
          try ModIdmap.modify modid modify tree.map
          with Not_found ->
            let ptab = modify () empty_tree in
            ModIdmap.add modid ptab tree.map
        in
let this =
          if level <= 0 then
     match tree.path with
       | Absolute (n,_) ->
    (* This is an absolute name, we must keep it
     otherwise it may become unaccessible forever *)
                warn_masking_absolute n; tree.path
       | Nothing
       | Relative _ -> Relative (uname,o)
          else tree.path
in
mktree this map
    | [] ->
match tree.path with
   | Absolute (uname',o') ->
       if E.equal o' o then begin
  assert (U.equal uname uname');
  tree
    (* we are putting the same thing for the second time :) *)
       end
       else
  (* This is an absolute name, we must keep it otherwise it may
   become unaccessible forever *)
  (* But ours is also absolute! This is an error! *)
  user_err Pp.(str @@ "Cannot mask the absolute name \""
                                   ^ U.to_string uname' ^ "\"!")
   | Nothing
   | Relative _ -> mktree (Absolute (uname,o)) tree.map

let rec push_exactly uname o level tree = function
| [] ->
  anomaly (Pp.str "Prefix longer than path! Impossible!")
| modid :: path ->
  if Int.equal level 0 then
    let this =
      match tree.path with
        | Absolute (n,_) ->
            (* This is an absolute name, we must keep it
                otherwise it may become unaccessible forever *)
            warn_masking_absolute n; tree.path
        | Nothing
        | Relative _ -> Relative (uname,o)
    in
    mktree this tree.map
  else (* not right level *)
    let modify _ mc = push_exactly uname o (level-1) mc path in
    let map =
      try ModIdmap.modify modid modify tree.map
      with Not_found ->
        let ptab = modify () empty_tree in
        ModIdmap.add modid ptab tree.map
    in
    mktree tree.path map

let push visibility uname o tab =
  let id,dir = U.repr uname in
  let modify _ ptab = match visibility with
    | Until i -> push_until uname o (i-1) ptab dir
    | Exactly i -> push_exactly uname o (i-1) ptab dir
  in
  try Id.Map.modify id modify tab
  with Not_found ->
    let ptab = modify () empty_tree in
    Id.Map.add id ptab tab

let rec search tree = function
  | modid :: path -> search (ModIdmap.find modid tree.map) path
  | [] -> tree.path

let find_node qid tab =
  let (dir,id) = repr_qualid qid in
    search (Id.Map.find id tab) (DirPath.repr dir)

let locate qid tab =
  let o = match find_node qid tab with
    | Absolute (uname,o) | Relative (uname,o) -> o
    | Nothing -> raise Not_found
  in
    o

let user_name qid tab =
  let uname = match find_node qid tab with
    | Absolute (uname,o) | Relative (uname,o) -> uname
    | Nothing -> raise Not_found
  in
    uname

let find uname tab =
  let id,l = U.repr uname in
    match search (Id.Map.find id tab) l with
Absolute (_,o) -> o
      | _ -> raise Not_found

let exists uname tab =
  try
    let _ = find uname tab in
      true
  with
      Not_found -> false

let shortest_qualid ?loc ctx uname tab =
  let id,dir = U.repr uname in
  let hidden = Id.Set.mem id ctx in
  let rec find_uname pos dir tree =
    let is_empty = match pos with [] -> true | _ -> false in
    match tree.path with
    | Absolute (u,_) | Relative (u,_)
          when U.equal u uname && not (is_empty && hidden) -> List.rev pos
    | _ ->
match dir with
     [] -> raise Not_found
   | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map)
  in
  let ptab = Id.Map.find id tab in
  let found_dir = find_uname [] dir ptab in
    make_qualid ?loc (DirPath.make found_dir) id

let push_node node l =
  match node with
  | Absolute (_,o) | Relative (_,o) when not (List.mem_f E.equal o l) -> o::l
  | _ -> l

let rec flatten_idmap tab l =
  let f _ tree l = flatten_idmap tree.map (push_node tree.path l) in
  ModIdmap.fold f tab l

let rec search_prefixes tree = function
  | modid :: path -> search_prefixes (ModIdmap.find modid tree.map) path
  | [] -> List.rev (flatten_idmap tree.map (push_node tree.path []))

let find_prefixes qid tab =
  try
    let (dir,id) = repr_qualid qid in
    search_prefixes (Id.Map.find id tab) (DirPath.repr dir)
  with Not_found -> []

let match_prefixes =
  let cprefix x y = CString.(compare x (sub y 0 (min (length x) (length y)))) in
  fun qid tab ->
    try
      let (dir,id) = repr_qualid qid in
      let id_prefix = cprefix Id.(to_string id) in
      let matches = Id.Map.filter_range (fun x -> id_prefix Id.(to_string x)) tab in
      let matches = Id.Map.mapi (fun _key tab -> search_prefixes tab (DirPath.repr dir)) matches in
      (* Coq's flatten is "magical", so this is not so bad perf-wise *)
      CList.flatten @@ Id.Map.(fold (fun _ r l -> r :: l) matches [])
    with Not_found -> []

end

(* Global name tables *************************************************)

module FullPath =
struct
  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 ExtRefEqual = ExtRefOrdered
module MPEqual = Names.ModPath

module ExtRefTab = Make(FullPath)(ExtRefEqual)
module MPTab = Make(FullPath)(MPEqual)

type ccitab = ExtRefTab.t
let the_ccitab = Summary.ref ~name:"ccitab" (ExtRefTab.empty : ccitab)

type mptab = MPTab.t
let the_modtypetab = Summary.ref ~name:"modtypetab" (MPTab.empty : mptab)

module DirPath' =
struct
  include DirPath
  let repr dir = match DirPath.repr dir with
    | [] -> anomaly (Pp.str "Empty dirpath.")
    | id :: l -> (id, l)
end

module DirTab = Make(DirPath')(GlobDirRef)

(* If we have a (closed) module M having a submodule N, than N does not
   have the entry in [the_dirtab]. *)
type dirtab = DirTab.t
let the_dirtab = Summary.ref ~name:"dirtab" (DirTab.empty : dirtab)

module UnivIdEqual =
struct
  type t = Univ.Level.UGlobal.t
  let equal = Univ.Level.UGlobal.equal
end
module UnivTab = Make(FullPath)(UnivIdEqual)
type univtab = UnivTab.t
let the_univtab = Summary.ref ~name:"univtab" (UnivTab.empty : univtab)

(* Reversed name tables ***************************************************)

(* This table translates extended_global_references back to section paths *)
module Globrevtab = HMap.Make(ExtRefOrdered)

type globrevtab = full_path Globrevtab.t
let the_globrevtab = Summary.ref ~name:"globrevtab" (Globrevtab.empty : globrevtab)

type mprevtab = DirPath.t MPmap.t
let the_modrevtab = Summary.ref ~name:"modrevtab" (MPmap.empty : mprevtab)

type mptrevtab = full_path MPmap.t
let the_modtyperevtab = Summary.ref ~name:"modtyperevtab" (MPmap.empty : mptrevtab)

module UnivIdOrdered =
struct
  type t = Univ.Level.UGlobal.t
  let hash = Univ.Level.UGlobal.hash
  let compare = Univ.Level.UGlobal.compare
end

module UnivIdMap = HMap.Make(UnivIdOrdered)

type univrevtab = full_path UnivIdMap.t
let the_univrevtab = Summary.ref ~name:"univrevtab" (UnivIdMap.empty : univrevtab)

(* Push functions *********************************************************)

(* This is for permanent constructions (never discharged -- but with
   possibly limited visibility, i.e. Theorem, Lemma, Definition, Axiom,
   Parameter but also Remark and Fact) *)

let push_xref visibility sp xref =
  match visibility with
    | Until _ ->
the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
the_globrevtab := Globrevtab.add xref sp !the_globrevtab
    | _ ->
begin
   if ExtRefTab.exists sp !the_ccitab then
     match ExtRefTab.find sp !the_ccitab with
       | TrueGlobal( ConstRef _) | TrueGlobal( IndRef _) |
      TrueGlobal( ConstructRef _) as xref ->
    the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
       | _ ->
    the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
     else
       the_ccitab := ExtRefTab.push visibility sp xref !the_ccitab;
end

let push_cci visibility sp ref =
  push_xref visibility sp (TrueGlobal ref)

(* This is for Syntactic Definitions *)
let push_syndef visibility sp kn =
  push_xref visibility sp (SynDef kn)

let push = push_cci

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 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
  | GlobDirRef.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 *******************************************************)

(* This should be used when syntactic definitions are allowed *)
let locate_extended qid = ExtRefTab.locate qid !the_ccitab

(* This should be used when no syntactic definitions is expected *)
let locate qid = match locate_extended qid with
  | TrueGlobal ref -> ref
  | SynDef _ -> raise Not_found
let full_name_cci qid = ExtRefTab.user_name qid !the_ccitab

let locate_syndef qid = match locate_extended qid with
  | TrueGlobal _ -> raise Not_found
  | SynDef kn -> kn

let locate_modtype qid = MPTab.locate qid !the_modtypetab
let full_name_modtype qid = MPTab.user_name qid !the_modtypetab

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
    | GlobDirRef.DirModule { obj_mp ; _} -> obj_mp
    | _ -> raise Not_found

let full_name_module qid =
  match locate_dir qid with
    | GlobDirRef.DirModule { obj_dir ; _} -> obj_dir
    | _ -> raise Not_found

let locate_section qid =
  match locate_dir qid with
    | GlobDirRef.DirOpenSection { obj_dir; _ } -> obj_dir
    | _ -> raise Not_found

let locate_all qid =
  List.fold_right (fun a l -> match a with TrueGlobal a -> a::l | _ -> l)
    (ExtRefTab.find_prefixes qid !the_ccitab) []

let locate_extended_all qid = ExtRefTab.find_prefixes qid !the_ccitab

let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab

let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab

(* Completion *)
let completion_canditates qualid =
  ExtRefTab.match_prefixes qualid !the_ccitab

(* Derived functions *)

let locate_constant qid =
  match locate_extended qid with
    | TrueGlobal (ConstRef kn) -> kn
    | _ -> raise Not_found

let global_of_path sp =
  match ExtRefTab.find sp !the_ccitab with
    | TrueGlobal ref -> ref
    | _ -> raise Not_found

let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab

let global qid =
  try match locate_extended qid with
    | TrueGlobal ref -> ref
    | SynDef _ ->
        user_err ?loc:qid.CAst.loc ~hdr:"global"
          (str "Unexpected reference to a notation: " ++
           pr_qualid qid)
  with Not_found ->
    error_global_not_found qid

(* Exists functions ********************************************************)

let exists_cci sp = ExtRefTab.exists sp !the_ccitab

let exists_dir dir = DirTab.exists dir !the_dirtab

let exists_section = exists_dir

let exists_module = exists_dir

let exists_modtype sp = MPTab.exists sp !the_modtypetab

let exists_universe kn = UnivTab.exists kn !the_univtab

(* Reverse locate functions ***********************************************)

let path_of_global ref =
  match ref with
    | VarRef id -> make_path DirPath.empty id
    | _ -> Globrevtab.find (TrueGlobal ref) !the_globrevtab

let dirpath_of_global ref =
  fst (repr_path (path_of_global ref))

let basename_of_global ref =
  snd (repr_path (path_of_global ref))

let path_of_syndef kn =
  Globrevtab.find (SynDef kn) !the_globrevtab

let dirpath_of_module mp =
  MPmap.find mp !the_modrevtab

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 ?loc ctx ref =
  match ref with
    | VarRef id -> make_qualid ?loc DirPath.empty id
    | _ ->
        let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
        ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab

let shortest_qualid_of_syndef ?loc ctx kn =
  let sp = path_of_syndef kn in
    ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab

let shortest_qualid_of_module ?loc mp =
  let dir = MPmap.find mp !the_modrevtab in
    DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab

let shortest_qualid_of_modtype ?loc kn =
  let sp = MPmap.find kn !the_modtyperevtab in
    MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab

let shortest_qualid_of_universe ?loc kn =
  let sp = UnivIdMap.find kn !the_univrevtab in
    UnivTab.shortest_qualid ?loc 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 qid =
  match global qid with
  | IndRef ind -> ind
  | ref ->
      user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
        (pr_qualid qid ++ spc () ++ str "is not an inductive type")

(********************************************************************)

(* Deprecated synonyms *)

let extended_locate = locate_extended
let absolute_reference = global_of_path

¤ Dauer der Verarbeitung: 0.35 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.