aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/libnames.ml65
-rw-r--r--library/libnames.mli11
-rw-r--r--library/library.ml4
-rw-r--r--library/library.mli3
-rw-r--r--library/nametab.ml23
-rw-r--r--library/nametab.mli2
6 files changed, 51 insertions, 57 deletions
diff --git a/library/libnames.ml b/library/libnames.ml
index 81af5f2c9..d84731322 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -190,54 +190,51 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2
| _ -> false
-type reference =
- | Qualid of qualid Loc.located
- | Ident of Id.t Loc.located
-
-let qualid_of_reference = function
- | Qualid (loc,qid) -> loc, qid
- | Ident (loc,id) -> loc, qualid_of_ident id
-
-let string_of_reference = function
- | Qualid (loc,qid) -> string_of_qualid qid
- | Ident (loc,id) -> Id.to_string id
-
-let pr_reference = function
- | Qualid (_,qid) -> pr_qualid qid
- | Ident (_,id) -> Id.print id
-
-let loc_of_reference = function
- | Qualid (loc,qid) -> loc
- | Ident (loc,id) -> loc
-
-let eq_reference r1 r2 = match r1, r2 with
-| Qualid (_, q1), Qualid (_, q2) -> qualid_eq q1 q2
-| Ident (_, id1), Ident (_, id2) -> Id.equal id1 id2
+type reference_r =
+ | Qualid of qualid
+ | Ident of Id.t
+type reference = reference_r CAst.t
+
+let qualid_of_reference = CAst.map (function
+ | Qualid qid -> qid
+ | Ident id -> qualid_of_ident id)
+
+let string_of_reference = CAst.with_val (function
+ | Qualid qid -> string_of_qualid qid
+ | Ident id -> Id.to_string id)
+
+let pr_reference = CAst.with_val (function
+ | Qualid qid -> pr_qualid qid
+ | Ident id -> Id.print id)
+
+let eq_reference {CAst.v=r1} {CAst.v=r2} = match r1, r2 with
+| Qualid q1, Qualid q2 -> qualid_eq q1 q2
+| Ident id1, Ident id2 -> Id.equal id1 id2
| _ -> false
-let join_reference ns r =
+let join_reference {CAst.loc=l1;v=ns} {CAst.loc=l2;v=r} =
+ CAst.make ?loc:(Loc.merge_opt l1 l2) (
match ns , r with
- Qualid (_, q1), Qualid (loc, q2) ->
+ Qualid q1, Qualid q2 ->
let (dp1,id1) = repr_qualid q1 in
let (dp2,id2) = repr_qualid q2 in
- Qualid (loc,
- make_qualid
+ Qualid (make_qualid
(append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2)
id2)
- | Qualid (_, q1), Ident (loc, id2) ->
+ | Qualid q1, Ident id2 ->
let (dp1,id1) = repr_qualid q1 in
- Qualid (loc,
- make_qualid
+ Qualid (make_qualid
(append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1)))
id2)
- | Ident (_, id1), Qualid (loc, q2) ->
+ | Ident id1, Qualid q2 ->
let (dp2,id2) = repr_qualid q2 in
- Qualid (loc, make_qualid
+ Qualid (make_qualid
(append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2)
id2)
- | Ident (_, id1), Ident (loc, id2) ->
- Qualid (loc, make_qualid
+ | Ident id1, Ident id2 ->
+ Qualid (make_qualid
(dirpath_of_string (Names.Id.to_string id1)) id2)
+ )
(* Default paths *)
let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/libnames.mli b/library/libnames.mli
index afceef530..9dad26129 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -9,7 +9,6 @@
(************************************************************************)
open Util
-open Loc
open Names
(** {6 Dirpaths } *)
@@ -137,15 +136,15 @@ val eq_global_dir_reference :
global name (referred either by a qualified name or by a single
name) or a variable *)
-type reference =
- | Qualid of qualid located
- | Ident of Id.t located
+type reference_r =
+ | Qualid of qualid
+ | Ident of Id.t
+type reference = reference_r CAst.t
val eq_reference : reference -> reference -> bool
-val qualid_of_reference : reference -> qualid located
+val qualid_of_reference : reference -> qualid CAst.t
val string_of_reference : reference -> string
val pr_reference : reference -> Pp.t
-val loc_of_reference : reference -> Loc.t option
val join_reference : reference -> reference -> reference
(** some preset paths *)
diff --git a/library/library.ml b/library/library.ml
index fb9b54462..56d2709d5 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -577,7 +577,7 @@ let require_library_from_dirpath modrefl export =
(* the function called by Vernacentries.vernac_import *)
-let safe_locate_module (loc,qid) =
+let safe_locate_module {CAst.loc;v=qid} =
try Nametab.locate_module qid
with Not_found ->
user_err ?loc ~hdr:"import_library"
@@ -595,7 +595,7 @@ let import_module export modl =
| [] -> ()
| modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
let rec aux acc = function
- | (loc, dir as m) :: l ->
+ | ({CAst.loc; v=dir} as m) :: l ->
let m,acc =
try Nametab.locate_module dir, acc
with Not_found-> flush acc; safe_locate_module m, [] in
diff --git a/library/library.mli b/library/library.mli
index 82a891acc..0877ebb5a 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Loc
open Names
open Libnames
@@ -37,7 +36,7 @@ type seg_proofs = Constr.constr Future.computation array
(** Open a module (or a library); if the boolean is true then it's also
an export otherwise just a simple import *)
-val import_module : bool -> qualid located list -> unit
+val import_module : bool -> qualid CAst.t list -> unit
(** Start the compilation of a file as a library. The first argument must be
output file, and the
diff --git a/library/nametab.ml b/library/nametab.ml
index 0e996443f..2046bf758 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,8 +18,8 @@ open Globnames
exception GlobalizationError of qualid
-let error_global_not_found ?loc q =
- Loc.raise ?loc (GlobalizationError q)
+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
@@ -459,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 ~hdr:"global"
(str "Unexpected reference to a notation: " ++
- pr_qualid qid)
+ pr_qualid v)
with Not_found ->
- error_global_not_found ?loc qid
+ error_global_not_found qid
(* Exists functions ********************************************************)
@@ -539,13 +539,12 @@ let pr_global_env 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) ~hdr:"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")
(********************************************************************)
diff --git a/library/nametab.mli b/library/nametab.mli
index 3802eaa9a..cd28518ab 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -61,7 +61,7 @@ open Globnames
exception GlobalizationError of qualid
(** Raises a globalization error *)
-val error_global_not_found : ?loc:Loc.t -> qualid -> 'a
+val error_global_not_found : qualid CAst.t -> 'a
(** {6 Register visibility of things } *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 12:13:00 +0000