Merge PR #7797: Remove reference name type.

8 files changed, 79 insertions, 125 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 76071ebcc..f14ad333e 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -161,7 +161,7 @@ module type RefConvertArg =
 sig
   type t
   val compare : t -> t -> int
-  val encode : reference -> t
+  val encode : qualid -> t
   val subst : substitution -> t -> t
   val printer : t -> Pp.t
   val key : option_name
@@ -172,7 +172,7 @@ end
 module RefConvert = functor (A : RefConvertArg) ->
 struct
   type t = A.t
-  type key = reference
+  type key = qualid
   let compare = A.compare
   let table = ref_table
   let encode = A.encode
diff --git a/library/goptions.mli b/library/goptions.mli
index 6c14d19ee..3d7df18fe 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -89,7 +89,7 @@ module MakeRefTable :
     (A : sig
            type t
            val compare : t -> t -> int
-           val encode : reference -> t
+           val encode : qualid -> t
 	   val subst : substitution -> t -> t
            val printer : t -> Pp.t
            val key : option_name
@@ -147,9 +147,9 @@ val get_string_table :
 
 val get_ref_table :
   option_name ->
-    < add : reference -> unit;
-      remove : reference -> unit;
-      mem : reference -> unit;
+    < add : qualid -> unit;
+      remove : qualid -> unit;
+      mem : qualid -> unit;
       print : unit >
 
 (** The first argument is a locality flag. *)
diff --git a/library/libnames.ml b/library/libnames.ml
index 8d5a02a29..23085048a 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -134,23 +134,33 @@ let restrict_path n sp =
   make_path (DirPath.make dir') s
 
 (*s qualified names *)
-type qualid = full_path
+type qualid_r = full_path
+type qualid = qualid_r CAst.t
 
-let make_qualid = make_path
-let repr_qualid = repr_path
+let make_qualid ?loc pa id = CAst.make ?loc (make_path pa id)
+let repr_qualid {CAst.v=qid} = repr_path qid
 
-let qualid_eq = eq_full_path
+let qualid_eq qid1 qid2 = eq_full_path qid1.CAst.v qid2.CAst.v
 
-let string_of_qualid = string_of_path
-let pr_qualid = pr_path
+let string_of_qualid qid = string_of_path qid.CAst.v
+let pr_qualid qid = pr_path qid.CAst.v
 
-let qualid_of_string = path_of_string
+let qualid_of_string ?loc s = CAst.make ?loc @@ path_of_string s
 
-let qualid_of_path sp = sp
-let qualid_of_ident id = make_qualid DirPath.empty id
-let qualid_of_dirpath dir =
+let qualid_of_path ?loc sp = CAst.make ?loc sp
+let qualid_of_ident ?loc id = make_qualid ?loc DirPath.empty id
+let qualid_of_dirpath ?loc dir =
   let (l,a) = split_dirpath dir in
-  make_qualid l a
+  make_qualid ?loc l a
+
+let qualid_is_ident qid =
+  DirPath.is_empty qid.CAst.v.dirpath
+
+let qualid_basename qid =
+  qid.CAst.v.basename
+
+let qualid_path qid =
+  qid.CAst.v.dirpath
 
 type object_name = full_path * KerName.t
 
@@ -183,52 +193,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 | DirModule op1, DirModule op2 -> eq_op op1 op2
 | _ -> false
 
-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 {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 q2 ->
-      let (dp1,id1) = repr_qualid q1 in
-      let (dp2,id2) = repr_qualid q2 in
-      Qualid (make_qualid
-		(append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2)
-		id2)
-  | Qualid q1, Ident id2 ->
-    let (dp1,id1) = repr_qualid q1 in
-    Qualid (make_qualid
-	      (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1)))
-	      id2)
-  | Ident id1, Qualid q2 ->
-    let (dp2,id2) = repr_qualid q2 in
-    Qualid (make_qualid
-      (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2)
-      id2)
-  | 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 5f69b1f0f..447eecbb5 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -65,23 +65,28 @@ val restrict_path : int -> full_path -> full_path
     qualifications of absolute names, including single identifiers.
     The [qualid] are used to access the name table. *)
 
-type qualid
+type qualid_r
+type qualid = qualid_r CAst.t
 
-val make_qualid : DirPath.t -> Id.t -> qualid
+val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid
 val repr_qualid : qualid -> DirPath.t * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
 val pr_qualid : qualid -> Pp.t
 val string_of_qualid : qualid -> string
-val qualid_of_string : string -> qualid
+val qualid_of_string : ?loc:Loc.t -> string -> qualid
 
 (** Turns an absolute name, a dirpath, or an Id.t into a
    qualified name denoting the same name *)
 
-val qualid_of_path : full_path -> qualid
-val qualid_of_dirpath : DirPath.t -> qualid
-val qualid_of_ident : Id.t -> qualid
+val qualid_of_path : ?loc:Loc.t -> full_path -> qualid
+val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid
+val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid
+
+val qualid_is_ident : qualid -> bool
+val qualid_path : qualid -> DirPath.t
+val qualid_basename : qualid -> Id.t
 
 (** Both names are passed to objects: a "semantic" [kernel_name], which
    can be substituted and a "syntactic" [full_path] which can be printed
@@ -124,20 +129,6 @@ val eq_global_dir_reference :
   global_dir_reference -> global_dir_reference -> bool
 
 (** {6 ... } *)
-(** A [reference] is the user-level notion of name. It denotes either a
-    global name (referred either by a qualified name or by a single
-    name) or a variable *)
-
-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 CAst.t
-val string_of_reference : reference -> string
-val pr_reference : reference -> Pp.t
-val join_reference : reference -> reference -> reference
 
 (** some preset paths *)
 val default_library : DirPath.t
diff --git a/library/library.ml b/library/library.ml
index 56d2709d5..400f3dcf1 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -577,10 +577,10 @@ let require_library_from_dirpath modrefl export =
 
 (* the function called by Vernacentries.vernac_import *)
 
-let safe_locate_module {CAst.loc;v=qid} =
+let safe_locate_module qid =
   try Nametab.locate_module qid
   with Not_found ->
-    user_err ?loc ~hdr:"import_library"
+    user_err ?loc:qid.CAst.loc ~hdr:"import_library"
       (pr_qualid qid ++ str " is not a module")
 
 let import_module export modl =
@@ -595,18 +595,18 @@ let import_module export modl =
     | [] -> ()
     | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in
   let rec aux acc = function
-    | ({CAst.loc; v=dir} as m) :: l ->
+    | qid :: l ->
         let m,acc =
-          try Nametab.locate_module dir, acc
-          with Not_found-> flush acc; safe_locate_module m, [] in
+          try Nametab.locate_module qid, acc
+          with Not_found-> flush acc; safe_locate_module qid, [] in
         (match m with
         | MPfile dir -> aux (dir::acc) l
         | mp ->
             flush acc;
             try Declaremods.import_module export mp; aux [] l
             with Not_found ->
-              user_err ?loc ~hdr:"import_library"
-                (pr_qualid dir ++ str " is not a module"))
+              user_err ?loc:qid.CAst.loc ~hdr:"import_library"
+                (pr_qualid qid ++ str " is not a module"))
     | [] -> flush acc
   in aux [] modl
 
diff --git a/library/library.mli b/library/library.mli
index 0877ebb5a..d5815afc4 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -36,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 CAst.t list -> unit
+val import_module : bool -> qualid 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 995f44706..a3b3ca6e7 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -18,8 +18,8 @@ open Globnames
 
 exception GlobalizationError of qualid
 
-let error_global_not_found {CAst.loc;v} =
-  Loc.raise ?loc (GlobalizationError v)
+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
@@ -69,7 +69,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
-  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 end
 
@@ -220,7 +220,7 @@ let exists uname tab =
   with
       Not_found -> false
 
-let shortest_qualid ctx uname tab =
+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 =
@@ -235,7 +235,7 @@ let shortest_qualid ctx uname tab =
   in
   let ptab = Id.Map.find id tab in
   let found_dir = find_uname [] dir ptab in
-    make_qualid (DirPath.make found_dir) id
+    make_qualid ?loc (DirPath.make found_dir) id
 
 let push_node node l =
   match node with
@@ -458,14 +458,13 @@ let global_of_path sp =
 
 let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab
 
-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
+let global qid =
+  try match locate_extended qid with
     | TrueGlobal ref -> ref
     | SynDef _ ->
-        user_err ?loc ~hdr:"global"
+        user_err ?loc:qid.CAst.loc ~hdr:"global"
           (str "Unexpected reference to a notation: " ++
-           pr_qualid v)
+           pr_qualid qid)
   with Not_found ->
     error_global_not_found qid
 
@@ -510,40 +509,40 @@ let path_of_universe mp =
 
 (* Shortest qualid functions **********************************************)
 
-let shortest_qualid_of_global ctx ref =
+let shortest_qualid_of_global ?loc ctx ref =
   match ref with
-    | VarRef id -> make_qualid DirPath.empty id
+    | VarRef id -> make_qualid ?loc DirPath.empty id
     | _ ->
         let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in
-        ExtRefTab.shortest_qualid ctx sp !the_ccitab
+        ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
-let shortest_qualid_of_syndef ctx kn =
+let shortest_qualid_of_syndef ?loc ctx kn =
   let sp = path_of_syndef kn in
-    ExtRefTab.shortest_qualid ctx sp !the_ccitab
+    ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab
 
-let shortest_qualid_of_module mp =
+let shortest_qualid_of_module ?loc mp =
   let dir = MPmap.find mp !the_modrevtab in
-    DirTab.shortest_qualid Id.Set.empty dir !the_dirtab
+    DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab
 
-let shortest_qualid_of_modtype kn =
+let shortest_qualid_of_modtype ?loc kn =
   let sp = MPmap.find kn !the_modtyperevtab in
-    MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab
+    MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab
 
-let shortest_qualid_of_universe kn =
+let shortest_qualid_of_universe ?loc kn =
   let sp = UnivIdMap.find kn !the_univrevtab in
-    UnivTab.shortest_qualid Id.Set.empty sp !the_univtab
+    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 ({CAst.loc; v=r} as lr) =
-  match global lr with
+let global_inductive qid =
+  match global qid with
   | IndRef ind -> ind
   | ref ->
-      user_err ?loc ~hdr:"global_inductive"
-        (pr_reference lr ++ spc () ++ str "is not an inductive type")
+      user_err ?loc:qid.CAst.loc ~hdr:"global_inductive"
+        (pr_qualid qid ++ spc () ++ str "is not an inductive type")
 
 (********************************************************************)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index 2ec73a986..57e9141db 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 : qualid CAst.t -> 'a
+val error_global_not_found : qualid -> 'a
 
 (** {6 Register visibility of things } *)
 
@@ -105,8 +105,8 @@ val locate_universe : qualid -> universe_id
    references, like [locate] and co, but raise a nice error message
    in case of failure *)
 
-val global : reference -> GlobRef.t
-val global_inductive : reference -> inductive
+val global : qualid -> GlobRef.t
+val global_inductive : qualid -> inductive
 
 (** These functions locate all global references with a given suffix;
    if [qualid] is valid as such, it comes first in the list *)
@@ -168,11 +168,11 @@ val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t
    Coq.A.B.x that denotes the same object.
    @raise Not_found for unknown objects. *)
 
-val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid
-val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
-val shortest_qualid_of_modtype : ModPath.t -> qualid
-val shortest_qualid_of_module : ModPath.t -> qualid
-val shortest_qualid_of_universe : universe_id -> qualid
+val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
+val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid
+val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid
+val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid
+val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid
 
 (** Deprecated synonyms *)
 
@@ -207,7 +207,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
-  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
+  val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 end