Quelle nametab.ml Sprache: SML

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \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 Names
open Libnames
open Globnames

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

  let equal r1 r2 = match r1, r2 with
    | DirOpenModule op1, DirOpenModule op2 -> ModPath.equal op1 op2
    | DirOpenModtype op1, DirOpenModtype op2 -> ModPath.equal op1 op2
    | DirOpenSection op1, DirOpenSection op2 -> eq_full_path op1 op2
    | (DirOpenModule _ | DirOpenModtype _ | DirOpenSection _), _ -> false

  let compare r1 r2 = match r1, r2 with
    | DirOpenModule op1, DirOpenModule op2 -> ModPath.compare op1 op2
    | DirOpenModule _, _ -> -1
    | _, DirOpenModule _ -> 1
    | DirOpenModtype op1, DirOpenModtype op2 -> ModPath.compare op1 op2
    | DirOpenModtype _, _ -> -1
    | _, DirOpenModtype _ -> 1
    | DirOpenSection op1, DirOpenSection op2 -> compare_full_path op1 op2

end

exception GlobalizationError of qualid

let error_global_not_found ~info qid =
  let info = Option.cata (Loc.add_loc info) info qid.CAst.loc in
  Exninfo.iraise (GlobalizationError qid, info)

(* 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 *******************************************)

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 Mylib.A.B.x, tries
   to find the shortest among x, B.x, A.B.x and Mylib.A.B.x that denotes
   the same object.
*)
module type NAMETREE = sig
  type elt
  type t

  val empty : t
  val push : visibility -> full_path -> elt -> t -> t
  val locate : qualid -> t -> elt
  val find : full_path -> t -> elt
  val remove : full_path -> t -> t
  val exists : full_path -> t -> bool
  val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> full_path -> 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

let masking_absolute = CWarnings.create_warning
    ~from:[Deprecation.Version.v8_8] ~name:"masking-absolute-name" ()

let coq_id = Id.of_string "Coq"
let stdlib_id = Id.of_string "Stdlib"
let corelib_id = Id.of_string "Corelib"

let warn_deprecated_dirpath_Coq =
  CWarnings.create_with_quickfix ~name:"deprecated-dirpath-Coq"
    ~category:Deprecation.Version.v9_0
    (fun (old_id, new_id) ->
      Pp.(old_id ++ spc () ++ str "has been replaced by" ++ spc () ++ new_id ++ str "."))

(* We shadow as to create the quickfix and message at the same time *)
let fix_coq_id coq_repl l =
  (match l with
   | _coq_id :: l -> coq_repl :: l
   | _ -> l)

(* [l] is reversed, thus [Corelib.ssr.bool] for example *)
let warn_deprecated_dirpath_Coq ?loc (coq_repl, l, id) =
  let dp l = DirPath.make (List.rev l) in
  let old_id = pr_qualid @@ Libnames.make_qualid (DirPath.make l) id in
  let new_id = pr_qualid @@ Libnames.make_qualid (dp @@ fix_coq_id coq_repl (List.rev l)) id in
  let quickfix = Option.map (fun loc -> [ Quickfix.make ~loc new_id ]) loc in
  warn_deprecated_dirpath_Coq ?loc ?quickfix (old_id, new_id)

module Make (E : EqualityType) : NAMETREE
  with 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_in masking_absolute
      Pp.(fun n -> str "Trying to mask the absolute name \"" ++ pr_path n ++ str "\"!")

  type path_status =
    | Relative of full_path * elt
    | Absolute of full_path * elt

  let eq_path_status p q = match p, q with
  | Relative (u1, o1), Relative (u2, o2) -> eq_full_path u1 u2 && E.equal o1 o2
  | Absolute (u1, o1), Absolute (u2, o2) -> eq_full_path u1 u2 && E.equal o1 o2
  | (Absolute _ | Relative _), _ -> false

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

  let push_path arg path = match path with
  | [] -> [arg]
  | arg' :: _ -> if eq_path_status arg arg' then path else arg :: path

  let mktree p m = { path=p; map=m }
  let empty_tree = mktree [] Id.Map.empty
  let is_empty_tree tree = tree.path = [] && Id.Map.is_empty tree.map

  type t = nametree Id.Map.t

  let empty = Id.Map.empty

  (* [push_until] is used to register [Until vis] visibility.

     Example: [push_until Top.X.Y.t o (Until 1) tree [Y;X;Top]] adds the
     value [Relative (Top.X.Y.t,o)] to occurrences [Y] and [Y.X] of
     the tree, and [Absolute (Top.X.Y.t,o)] to occurrence [Y.X.Top] of
     the tree. In particular, the tree now includes the following shape:
     { map := Y |-> {map := X |-> {map := Top |-> {map := ...;
                                                   path := Absolute (Top.X.Y.t,o)::...}
                                          ...;
                                   path := Relative (Top.X.Y.t,o)::...}
                             ...;
                     path := Relative (Top.X.Y.t,o)::...}
               ...;
       path := ...}
     where ... denotes what was there before.

     [push_exactly] is to register [Exactly vis] and [push] 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 Id.Map.modify modid modify tree.map
          with Not_found ->
            let ptab = modify () empty_tree in
            Id.Map.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
              | current -> push_path (Relative (uname, o)) current
          else tree.path
        in
        if this == tree.path && map == tree.map then tree
        else mktree this map
    | [] ->
        match tree.path with
          | Absolute (uname',o') :: _ ->
              if E.equal o' o then begin
                assert (eq_full_path 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! *)
                CErrors.user_err
                  Pp.(str "Cannot mask the absolute name \"" ++ pr_path uname' ++ str "\"!")
          | current ->
            let this = push_path (Absolute (uname, o)) current in
            if this == tree.path then tree
            else mktree this tree.map

let rec push_exactly uname o level tree = function
| [] ->
  CErrors.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
        | current -> push_path (Relative (uname, o)) current
    in
    if this == tree.path then tree
    else mktree this tree.map
  else (* not right level *)
    let modify _ mc = push_exactly uname o (level-1) mc path in
    let map =
      try Id.Map.modify modid modify tree.map
      with Not_found ->
        let ptab = modify () empty_tree in
        Id.Map.add modid ptab tree.map
    in
    if map == tree.map then tree
    else mktree tree.path map

let push visibility uname o tab =
  let dir,id = repr_path uname in
  let dir = DirPath.repr dir 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

(** [remove_path uname tree dir] removes all bindings pointing to
    [uname] along the path [dir] in [tree] (i.e. all such bindings are
    assumed to be on this path) *)

let rec remove_path uname tree = function
  | modid :: path ->
      let update = function
        | None -> (* The name was actually not here *) None
        | Some mc ->
          let mc = remove_path uname mc path in
          if is_empty_tree mc then None else Some mc
      in
      let map = Id.Map.update modid update tree.map in
      let this =
        let test = function Relative (uname',_) -> not (eq_full_path uname uname') | _ -> true in
        List.filter test tree.path
      in
      mktree this map
  | [] ->
      let this =
        let test = function Absolute (uname',_) -> not (eq_full_path uname uname') | _ -> true in
        List.filter test tree.path
      in
      mktree this tree.map

(** Remove all bindings pointing to [uname] in [tab] *)

let remove uname tab =
  let dir,id = repr_path uname in
  let dir = DirPath.repr dir in
  let modify _ ptab = remove_path uname ptab dir in
  try Id.Map.modify id modify tab
  with Not_found -> tab

let rec search tree = function
  | modid :: path ->
     begin match Id.Map.find_opt modid tree.map with
     | None -> None
     | Some modid -> search modid path
     end
  | [] -> Some tree.path

let search ?loc id tree dir =
  let dirs = match List.rev dir with
    | last :: l when Id.equal last coq_id ->
      [ (Some stdlib_id, List.rev (stdlib_id :: l));
        (Some corelib_id, List.rev (corelib_id :: l)) ]
    | _ -> [ None, dir ]
  in
  let search_one (warn, dir) =
    match search tree dir with
    | Some v -> Some (warn, v)
    | None -> None
  in
  match List.find_map search_one dirs with
  | Some (coq_repl, p) ->
    Option.iter (fun coq_repl -> warn_deprecated_dirpath_Coq ?loc (coq_repl, dir, id)) coq_repl;
    p
  | None -> raise Not_found

let find_node qid tab =
  let loc = qid.CAst.loc in
  let (dir,id) = repr_qualid qid in
  search ?loc id (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
    | [] -> raise Not_found
  in
    o

let find uname tab =
  let l,id = repr_path uname in
  let l = DirPath.repr l in
  match search id (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_gen ?loc hidden uname tab =
  let dir,id = repr_path uname in
  let dir = DirPath.repr dir in
  let hidden = hidden id 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 eq_full_path u uname && not (is_empty && hidden) -> List.rev pos
    | _ ->
        match dir with
            [] -> raise Not_found
          | id::dir -> find_uname (id::pos) dir (Id.Map.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 (Util.List.mem_f E.equal o l) -> o::l
  | _ -> l

let rec flatten_tree tree l =
  let f _ tree l = flatten_tree tree l in
  Id.Map.fold f tree.map (push_node tree.path l)

let rec search_prefixes tree = function
  | modid :: path -> search_prefixes (Id.Map.find modid tree.map) path
  | [] -> List.rev (flatten_tree tree [])

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
      (* Rocq'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

module type NAMETAB_gen = sig
  type 'a read_tab
  type write_tab

  type elt

  val push : visibility -> full_path -> elt -> write_tab

  val remove : full_path -> elt -> write_tab

  val shortest_qualid_gen : ?loc:Loc.t -> (Id.t -> bool) -> elt -> qualid read_tab

  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> elt -> qualid read_tab

  val pr : elt -> Pp.t read_tab

  val locate : qualid -> elt read_tab

  val locate_all : qualid -> elt list read_tab

  val completion_candidates : qualid -> elt list read_tab

  val to_path : elt -> full_path read_tab

  val of_path : full_path -> elt read_tab

  val exists : full_path -> bool read_tab

  (* XXX add src_loc table? *)
end

module type ValueType = sig
  include EqualityType

  val is_var : t -> Id.t option

  module Map : CSig.UMapS with type key = t
end

module type WarnInfo = sig
  type elt
  type data

  module Map : CSig.UMapS with type key = elt

  val stage : Summary.Stage.t
  val summary_name : string

  val warn : ?loc:Loc.t -> elt -> data -> unit
end

module type Functional_NAMETAB = sig
  type t
  val empty : t
  include NAMETAB_gen with type 'a read_tab := t -> 'a and type write_tab := t -> t
end

module MakeTab (E:ValueType) : Functional_NAMETAB with type elt = E.t = struct
  type elt = E.t

  module Tab = Make(E)

  type t = {
    tab : Tab.t;
    revtab : full_path E.Map.t;
  }

  let empty = {
    tab = Tab.empty;
    revtab = E.Map.empty;
  }

  let push vis sp v { tab; revtab } =
    match vis with
    | Until _ ->
      {
        tab = Tab.push vis sp v tab;
        revtab = E.Map.add v sp revtab;
      }
    | Exactly _ ->
      {
        tab = Tab.push vis sp v tab;
        revtab;
      }

  let remove sp v { tab; revtab } =
    {
      tab = Tab.remove sp tab;
      revtab = E.Map.remove v revtab;
    }

  let shortest_qualid_gen ?loc avoid v { tab; revtab } =
    match E.is_var v with
    | Some id -> make_qualid ?loc DirPath.empty id
    | None ->
      let sp = E.Map.find v revtab in
      Tab.shortest_qualid_gen ?loc avoid sp tab

  let shortest_qualid ?loc avoid v tabs =
    shortest_qualid_gen ?loc (fun id -> Id.Set.mem id avoid) v tabs

  let pr v tab = pr_qualid (shortest_qualid Id.Set.empty v tab)

  let locate qid { tab } = Tab.locate qid tab

  let locate_all qid { tab } = Tab.find_prefixes qid tab

  let completion_candidates qid { tab } = Tab.match_prefixes qid tab

  let to_path v { revtab } = match E.is_var v with
    | Some id -> make_path DirPath.empty id
    | None -> E.Map.find v revtab

  let of_path sp { tab } = Tab.find sp tab

  let exists sp { tab } = Tab.exists sp tab

end

module type NAMETAB = NAMETAB_gen with type 'a read_tab := 'a and type write_tab := unit

module type StateInfo = sig
  val stage : Summary.Stage.t
  val summary_name : string
end

module MakeImperative (Tab:Functional_NAMETAB) (SI:StateInfo) ()
    : NAMETAB with type elt = Tab.elt
= struct
  type elt = Tab.elt

  let the_tab = Summary.ref ~stage:SI.stage ~name:SI.summary_name Tab.empty

  let push vis sp v = the_tab := Tab.push vis sp v !the_tab

  let remove sp v = the_tab := Tab.remove sp v !the_tab

  let shortest_qualid_gen ?loc f v = Tab.shortest_qualid_gen ?loc f v !the_tab

  let shortest_qualid ?loc avoid v = Tab.shortest_qualid ?loc avoid v !the_tab

  let pr v = Tab.pr v !the_tab

  let locate qid = Tab.locate qid !the_tab

  let locate_all qid = Tab.locate_all qid !the_tab

  let completion_candidates qid = Tab.completion_candidates qid !the_tab

  let to_path v = Tab.to_path v !the_tab

  let of_path v = Tab.of_path v !the_tab

  let exists v = Tab.exists v !the_tab
end

module type WarnedTab = sig
  include NAMETAB

  type warning_data

  val push : ?wdata:warning_data -> visibility -> full_path -> elt -> unit
  val is_warned : elt -> warning_data option
  val warn : ?loc:Loc.t -> elt -> warning_data -> unit
  val locate : ?nowarn:bool -> qualid -> elt
end

module MakeWarned (M:NAMETAB)
    (W:WarnInfo with type elt = M.elt)
    ()
    : WarnedTab with type elt = M.elt and type warning_data := W.data
= struct
  include M

  let warntab = Summary.ref ~stage:W.stage ~name:W.summary_name W.Map.empty

  let push ?wdata vis sp elt =
    M.push vis sp elt;
    match wdata with
    | None -> ()
    | Some wdata ->
      let () = match vis with
        | Until _ -> ()
        | Exactly _ -> assert false
      in
      warntab := W.Map.add elt wdata !warntab

  let remove sp elt =
    M.remove sp elt;
    warntab := W.Map.remove elt !warntab

  let is_warned elt = W.Map.find_opt elt !warntab

  let warn = W.warn

  let locate ?(nowarn=false) qid =
    let elt = M.locate qid in
    let () = if nowarn then ()
      else match is_warned elt with
        | None -> ()
        | Some wdata -> warn ?loc:qid.loc elt wdata
    in
    elt
end

module EasyNoWarn (M:sig include ValueType include StateInfo end) () =
  MakeImperative(MakeTab(M))(M)()

module type SimpleWarnS = sig
  val object_name : string
  val warning_name_base : string
end

module Easy (M:sig include ValueType include StateInfo include SimpleWarnS end) () = struct
  module I = EasyNoWarn(M)()

  module WInfo = struct
    type elt = M.t
    type data = elt UserWarn.with_qf

    module Map = M.Map

    let stage = M.stage
    let summary_name = M.summary_name ^ "-warnings"

    let warn = UserWarn.create_depr_and_user_warnings_qf
        ~object_name:M.object_name ~warning_name_base:M.warning_name_base
        ~pp_qf:I.pr I.pr
        ()
  end

  include MakeWarned(I)(WInfo)()
end

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

module XRefV = struct
  include ExtRefOrdered
  let is_var = function
    | TrueGlobal (VarRef id) -> Some id
    | _ -> None

  module Map = ExtRefMap

  let stage = Summary.Stage.Interp
  let summary_name = "xreftab"
end
module XRefNoWarn = EasyNoWarn(XRefV)()

module XRefWarn = struct
  type elt = extended_global_reference
  type data = elt UserWarn.with_qf

  module Map = ExtRefMap

  let pp = XRefNoWarn.pr

  let depr_ref = Deprecation.create_warning_with_qf ~object_name:"Reference" ~warning_name_if_no_since:"deprecated-reference" ~pp_qf:pp pp
  let depr_abbrev = Deprecation.create_warning_with_qf ~object_name:"Notation" ~warning_name_if_no_since:"deprecated-syntactic-definition" ~pp_qf:pp pp
  let user_warn = UserWarn.create_warning ~warning_name_if_no_cats:"warn-reference" ()

  let depr_xref ?loc depr xref =
    match xref with
    | TrueGlobal _ -> depr_ref ?loc (xref,depr)
    | Abbrev _ -> depr_abbrev ?loc (xref,depr)

  let warn ?loc xref uwarns =
      uwarns.UserWarn.depr_qf |> Option.iter (fun depr -> depr_xref ?loc depr xref);
      uwarns.UserWarn.warn_qf |> List.iter (user_warn ?loc)

  let stage = Summary.Stage.Interp
  let summary_name = "xrefwarntab"
end

module XRefs = MakeWarned(XRefNoWarn)(XRefWarn)()

module UnivsV = struct
  include Univ.UGlobal
  let is_var _ = None
  module Map = HMap.Make(Univ.UGlobal)
  let stage = Summary.Stage.Interp
  let summary_name = "univtab"
end
module Univs = EasyNoWarn(UnivsV)()

module QualityV = struct
  include Sorts.QGlobal
  let is_var _ = None
  module Map = HMap.Make(Sorts.QGlobal)
  let stage = Summary.Stage.Interp
  let summary_name = "sorttab"
end
module Quality = EasyNoWarn(QualityV)()

module ModTypeV = struct
  include ModPath
  let is_var _ = None
  module Map = MPmap
  let stage = Summary.Stage.Synterp
  let summary_name = "modtypetab"
end
module ModTypes = EasyNoWarn(ModTypeV)()

module ModuleV = struct
  include ModPath
  let is_var _ = None
  module Map = MPmap
  let stage = Summary.Stage.Synterp
  let summary_name = "moduletab"
end
module Modules = EasyNoWarn(ModuleV)()

module OpenModV = struct
  include GlobDirRef
  let is_var _ = None
  module Map = Map.Make(GlobDirRef)
  let stage = Summary.Stage.Synterp
  let summary_name = "openmodtab"
end
module OpenMods = EasyNoWarn(OpenModV)()

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

let push_abbreviation ?user_warns visibility sp kn =
  XRefs.push ?wdata:user_warns visibility sp (Abbrev kn)

let remove_abbreviation sp kn =
  XRefs.remove sp (Abbrev kn)

let push ?user_warns vis sp kn = XRefs.push ?wdata:user_warns vis sp (TrueGlobal kn)

let push_modtype vis sp kn = ModTypes.push vis sp kn

let push_module vis dir mp = Modules.push vis dir mp

let push_dir vis dir dir_ref = OpenMods.push vis dir dir_ref

let push_universe vis sp univ = Univs.push vis sp univ

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

let path_of_global ref = XRefs.to_path (TrueGlobal ref)

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_abbreviation kn = XRefs.to_path (Abbrev kn)

let path_of_module mp = Modules.to_path mp

let path_of_modtype mp = ModTypes.to_path mp

let path_of_universe mp = Univs.to_path mp

(* Shortest qualid functions **********************************************)

let shortest_qualid_of_global ?loc ctx ref = XRefs.shortest_qualid ?loc ctx (TrueGlobal ref)

let shortest_qualid_of_abbreviation ?loc ctx kn = XRefs.shortest_qualid ?loc ctx (Abbrev kn)

let shortest_qualid_of_module ?loc mp = Modules.shortest_qualid ?loc Id.Set.empty mp

let shortest_qualid_of_modtype ?loc kn = ModTypes.shortest_qualid ?loc Id.Set.empty kn

let shortest_qualid_of_dir ?loc sp = OpenMods.shortest_qualid ?loc Id.Set.empty sp

let shortest_qualid_of_universe ?loc avoid u =
  Univs.shortest_qualid_gen ?loc (fun id -> Id.Map.mem id avoid) u

let pr_global_env env ref =
  try pr_qualid (shortest_qualid_of_global env ref)
  with Not_found as exn ->
    let exn, info = Exninfo.capture exn in
    if !Flags.in_debugger then GlobRef.print ref
    else begin
      let () = if CDebug.(get_flag misc)
        then Feedback.msg_debug (Pp.str "pr_global_env not found")
      in
      Exninfo.iraise (exn, info)
    end

let is_warned_xref = XRefs.is_warned

let warn_user_warn_xref ?loc wdata x = XRefs.warn ?loc x wdata

let locate_extended_nowarn qid = XRefs.locate ~nowarn:true qid

let locate_extended qid = XRefs.locate qid

let locate qid = match locate_extended qid with
  | TrueGlobal ref -> ref
  | Abbrev _ -> raise Not_found

let locate_abbreviation qid = match locate_extended qid with
  | TrueGlobal _ -> raise Not_found
  | Abbrev kn -> kn

let locate_modtype qid = ModTypes.locate qid
let full_name_modtype qid = ModTypes.to_path (locate_modtype qid)

let locate_universe qid = Univs.locate qid

let locate_dir qid = OpenMods.locate qid

let locate_module qid = Modules.locate qid

let full_name_module qid = Modules.to_path (locate_module qid)

let full_name_open_mod qid = OpenMods.to_path (locate_dir qid)

let locate_section qid =
  match locate_dir qid with
    | GlobDirRef.DirOpenSection dir -> dir
    | _ -> raise Not_found

let locate_extended_all qid = XRefs.locate_all qid

let locate_all qid =
  let l = locate_extended_all qid in
  CList.filter_map (function TrueGlobal a -> Some a | Abbrev _ -> None) l

let locate_extended_all_dir qid = OpenMods.locate_all qid

let locate_extended_all_modtype qid = ModTypes.locate_all qid

let locate_extended_all_module qid = Modules.locate_all qid

(* Completion *)
let completion_canditates qualid = XRefs.completion_candidates qualid

(* Derived functions *)

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

let global_of_path sp =
  match XRefs.of_path sp with
  | TrueGlobal ref -> ref
  | _ -> raise Not_found

let extended_global_of_path = XRefs.of_path

let global qid =
  try match locate_extended qid with
    | TrueGlobal ref -> ref
    | Abbrev _ ->
        CErrors.user_err ?loc:qid.CAst.loc
          Pp.(str "Unexpected reference to a notation: " ++
           pr_qualid qid ++ str ".")
  with Not_found as exn ->
    let _, info = Exninfo.capture exn in
    error_global_not_found ~info qid

let global_inductive qid =
  let open GlobRef in
  match global qid with
  | IndRef ind -> ind
  | ref ->
      CErrors.user_err ?loc:qid.CAst.loc
        Pp.(pr_qualid qid ++ spc () ++ str "is not an inductive type.")

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

let exists_cci = XRefs.exists

let exists_dir = OpenMods.exists

let exists_module = Modules.exists

let exists_modtype = ModTypes.exists

let exists_universe = Univs.exists

(* Source locations *)

open Globnames

let cci_loc_table : Loc.t ExtRefMap.t ref = Summary.ref ~name:"constant-loc-table" ExtRefMap.empty

let set_cci_src_loc kn loc = cci_loc_table := ExtRefMap.add kn loc !cci_loc_table

let cci_src_loc kn = ExtRefMap.find_opt kn !cci_loc_table

quality96%

¤ Dauer der Verarbeitung: 0.10 Sekunden ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.