summaryrefslogtreecommitdiff
path: root/library/libnames.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/libnames.ml')
-rw-r--r--library/libnames.ml315
1 files changed, 102 insertions, 213 deletions
diff --git a/library/libnames.ml b/library/libnames.ml
index db97eae9..f2a9d041 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -1,214 +1,112 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
+open Errors
open Util
open Names
-open Nameops
-open Term
-open Mod_subst
-
-(*s Global reference is a kernel side type for all references together *)
-type global_reference =
- | VarRef of variable
- | ConstRef of constant
- | IndRef of inductive
- | ConstructRef of constructor
-
-let isVarRef = function VarRef _ -> true | _ -> false
-let isConstRef = function ConstRef _ -> true | _ -> false
-let isIndRef = function IndRef _ -> true | _ -> false
-let isConstructRef = function ConstructRef _ -> true | _ -> false
-
-let eq_gr gr1 gr2 =
- match gr1,gr2 with
- | ConstRef con1, ConstRef con2 -> eq_constant con1 con2
- | IndRef kn1,IndRef kn2 -> eq_ind kn1 kn2
- | ConstructRef kn1,ConstructRef kn2 -> eq_constructor kn1 kn2
- | _,_ -> gr1=gr2
-
-let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
-let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef"
-let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef"
-let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destConstructRef"
-
-let subst_constructor subst ((kn,i),j as ref) =
- let kn' = subst_ind subst kn in
- if kn==kn' then ref, mkConstruct ref
- else ((kn',i),j), mkConstruct ((kn',i),j)
-
-let subst_global subst ref = match ref with
- | VarRef var -> ref, mkVar var
- | ConstRef kn ->
- let kn',t = subst_con subst kn in
- if kn==kn' then ref, mkConst kn else ConstRef kn', t
- | IndRef (kn,i) ->
- let kn' = subst_ind subst kn in
- if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i)
- | ConstructRef ((kn,i),j as c) ->
- let c',t = subst_constructor subst c in
- if c'==c then ref,t else ConstructRef c', t
-
-let canonical_gr = function
- | ConstRef con -> ConstRef(constant_of_kn(canonical_con con))
- | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i)
- | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j)
- | VarRef id -> VarRef id
-
-let global_of_constr c = match kind_of_term c with
- | Const sp -> ConstRef sp
- | Ind ind_sp -> IndRef ind_sp
- | Construct cstr_cp -> ConstructRef cstr_cp
- | Var id -> VarRef id
- | _ -> raise Not_found
-
-let constr_of_global = function
- | VarRef id -> mkVar id
- | ConstRef sp -> mkConst sp
- | ConstructRef sp -> mkConstruct sp
- | IndRef sp -> mkInd sp
-
-let constr_of_reference = constr_of_global
-let reference_of_constr = global_of_constr
-
-let global_ord_gen fc fmi x y =
- let ind_ord (indx,ix) (indy,iy) =
- let c = Pervasives.compare ix iy in
- if c = 0 then kn_ord (fmi indx) (fmi indy) else c
- in
- match x, y with
- | ConstRef cx, ConstRef cy -> kn_ord (fc cx) (fc cy)
- | IndRef indx, IndRef indy -> ind_ord indx indy
- | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
- let c = Pervasives.compare jx jy in
- if c = 0 then ind_ord indx indy else c
- | _, _ -> Pervasives.compare x y
-
-let global_ord_can = global_ord_gen canonical_con canonical_mind
-let global_ord_user = global_ord_gen user_con user_mind
-
-(* By default, [global_reference] are ordered on their canonical part *)
-
-module RefOrdered = struct
- type t = global_reference
- let compare = global_ord_can
-end
-
-module RefOrdered_env = struct
- type t = global_reference
- let compare = global_ord_user
-end
-
-module Refset = Set.Make(RefOrdered)
-module Refmap = Map.Make(RefOrdered)
-
-(* Extended global references *)
-
-type syndef_name = kernel_name
-
-type extended_global_reference =
- | TrueGlobal of global_reference
- | SynDef of syndef_name
-
-(* We order [extended_global_reference] via their user part
- (cf. pretty printer) *)
-
-module ExtRefOrdered = struct
- type t = extended_global_reference
- let compare x y =
- match x, y with
- | TrueGlobal rx, TrueGlobal ry -> global_ord_user rx ry
- | SynDef knx, SynDef kny -> kn_ord knx kny
- | _, _ -> Pervasives.compare x y
-end
(**********************************************)
-let pr_dirpath sl = (str (string_of_dirpath sl))
+let pr_dirpath sl = (str (DirPath.to_string sl))
(*s Operations on dirpaths *)
-(* Pop the last n module idents *)
-let pop_dirpath_n n dir =
- make_dirpath (list_skipn n (repr_dirpath dir))
+let split_dirpath d = match DirPath.repr d with
+ | id :: l -> DirPath.make l, id
+ | _ -> failwith "split_dirpath"
-let pop_dirpath p = match repr_dirpath p with
- | [] -> anomaly "dirpath_prefix: empty dirpath"
- | _::l -> make_dirpath l
+let pop_dirpath p = match DirPath.repr p with
+ | _::l -> DirPath.make l
+ | [] -> failwith "pop_dirpath"
+
+(* Pop the last n module idents *)
+let pop_dirpath_n n dir = DirPath.make (List.skipn n (DirPath.repr dir))
let is_dirpath_prefix_of d1 d2 =
- list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+ List.prefix_of Id.equal
+ (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
let chop_dirpath n d =
- let d1,d2 = list_chop n (List.rev (repr_dirpath d)) in
- make_dirpath (List.rev d1), make_dirpath (List.rev d2)
+ let d1,d2 = List.chop n (List.rev (DirPath.repr d)) in
+ DirPath.make (List.rev d1), DirPath.make (List.rev d2)
let drop_dirpath_prefix d1 d2 =
- let d = Util.list_drop_prefix (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) in
- make_dirpath (List.rev d)
-
-let append_dirpath d1 d2 = make_dirpath (repr_dirpath d2 @ repr_dirpath d1)
+ let d =
+ List.drop_prefix Id.equal
+ (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2))
+ in
+ DirPath.make (List.rev d)
-(* To know how qualified a name should be to be understood in the current env*)
-let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id])
+let append_dirpath d1 d2 = DirPath.make (DirPath.repr d2 @ DirPath.repr d1)
-let split_dirpath d =
- let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
+let add_dirpath_prefix id d = DirPath.make (DirPath.repr d @ [id])
-let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p)
+let add_dirpath_suffix p id = DirPath.make (id :: DirPath.repr p)
(* parsing *)
let parse_dir s =
let len = String.length s in
let rec decoupe_dirs dirs n =
- if n = len && n > 0 then error (s ^ " is an invalid path.");
+ if Int.equal n len && n > 0 then error (s ^ " is an invalid path.");
if n >= len then dirs else
let pos =
try
String.index_from s n '.'
with Not_found -> len
in
- if pos = n then error (s ^ " is an invalid path.");
+ if Int.equal pos n then error (s ^ " is an invalid path.");
let dir = String.sub s n (pos-n) in
- decoupe_dirs ((id_of_string dir)::dirs) (pos+1)
+ decoupe_dirs ((Id.of_string dir)::dirs) (pos+1)
in
decoupe_dirs [] 0
let dirpath_of_string s =
- make_dirpath (if s = "" then [] else parse_dir s)
-
-let string_of_dirpath = Names.string_of_dirpath
+ let path = match s with
+ | "" -> []
+ | _ -> parse_dir s
+ in
+ DirPath.make path
+let string_of_dirpath = Names.DirPath.to_string
-module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
-module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
+module Dirset = Set.Make(DirPath)
+module Dirmap = Map.Make(DirPath)
(*s Section paths are absolute names *)
type full_path = {
- dirpath : dir_path ;
- basename : identifier }
+ dirpath : DirPath.t ;
+ basename : Id.t }
+
+let dirpath sp = sp.dirpath
+let basename sp = sp.basename
let make_path pa id = { dirpath = pa; basename = id }
let repr_path { dirpath = pa; basename = id } = (pa,id)
+let eq_full_path p1 p2 =
+ Id.equal p1.basename p2.basename &&
+ DirPath.equal p1.dirpath p2.dirpath
+
(* parsing and printing of section paths *)
let string_of_path sp =
let (sl,id) = repr_path sp in
- if repr_dirpath sl = [] then string_of_id id
- else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+ match DirPath.repr sl with
+ | [] -> Id.to_string id
+ | _ -> (DirPath.to_string sl) ^ "." ^ (Id.to_string id)
let sp_ord sp1 sp2 =
let (p1,id1) = repr_path sp1
and (p2,id2) = repr_path sp2 in
- let p_bit = compare p1 p2 in
- if p_bit = 0 then id_ord id1 id2 else p_bit
+ let p_bit = DirPath.compare p1 p2 in
+ if Int.equal p_bit 0 then Id.compare id1 id2 else p_bit
module SpOrdered =
struct
@@ -218,9 +116,6 @@ module SpOrdered =
module Spmap = Map.Make(SpOrdered)
-let dirpath sp = let (p,_) = repr_path sp in p
-let basename sp = let (_,id) = repr_path sp in id
-
let path_of_string s =
try
let dir, id = split_dirpath (dirpath_of_string s) in
@@ -232,34 +127,8 @@ let pr_path sp = str (string_of_path sp)
let restrict_path n sp =
let dir, s = repr_path sp in
- let dir' = list_firstn n (repr_dirpath dir) in
- make_path (make_dirpath dir') s
-
-let encode_mind dir id = make_mind (MPfile dir) empty_dirpath (label_of_id id)
-
-let encode_con dir id = make_con (MPfile dir) empty_dirpath (label_of_id id)
-
-let decode_mind kn =
- let rec dir_of_mp = function
- | MPfile dir -> repr_dirpath dir
- | MPbound mbid ->
- let _,_,dp = repr_mbid mbid in
- let id = id_of_mbid mbid in
- id::(repr_dirpath dp)
- | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
- in
- let mp,sec_dir,l = repr_mind kn in
- if (repr_dirpath sec_dir) = [] then
- (make_dirpath (dir_of_mp mp)),id_of_label l
- else
- anomaly "Section part should be empty!"
-
-let decode_con kn =
- let mp,sec_dir,l = repr_con kn in
- match mp,(repr_dirpath sec_dir) with
- MPfile dir,[] -> (dir,id_of_label l)
- | _ , [] -> anomaly "MPfile expected!"
- | _ -> anomaly "Section part should be empty!"
+ let dir' = List.firstn n (DirPath.repr dir) in
+ make_path (DirPath.make dir') s
(*s qualified names *)
type qualid = full_path
@@ -267,44 +136,51 @@ type qualid = full_path
let make_qualid = make_path
let repr_qualid = repr_path
+let qualid_eq = eq_full_path
+
let string_of_qualid = string_of_path
let pr_qualid = pr_path
let qualid_of_string = path_of_string
let qualid_of_path sp = sp
-let qualid_of_ident id = make_qualid empty_dirpath id
+let qualid_of_ident id = make_qualid DirPath.empty id
let qualid_of_dirpath dir =
let (l,a) = split_dirpath dir in
make_qualid l a
type object_name = full_path * kernel_name
-type object_prefix = dir_path * (module_path * dir_path)
+type object_prefix = DirPath.t * (module_path * DirPath.t)
let make_oname (dirpath,(mp,dir)) id =
- make_path dirpath id, make_kn mp dir (label_of_id id)
+ make_path dirpath id, make_kn mp dir (Label.of_id id)
-(* to this type are mapped dir_path's in the nametab *)
+(* to this type are mapped DirPath.t's in the nametab *)
type global_dir_reference =
| DirOpenModule of object_prefix
| DirOpenModtype of object_prefix
| DirOpenSection of object_prefix
| DirModule of object_prefix
- | DirClosedSection of dir_path
+ | DirClosedSection of DirPath.t
(* this won't last long I hope! *)
-(* | ModRef mp ->
- let mp' = subst_modpath subst mp in if mp==mp' then ref else
- ModRef mp'
- | ModTypeRef kn ->
- let kn' = subst_kernel_name subst kn in if kn==kn' then ref else
- ModTypeRef kn'
-*)
+let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) =
+ DirPath.equal d1 d2 &&
+ DirPath.equal p1 p2 &&
+ mp_eq mp1 mp2
+
+let eq_global_dir_reference 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
+| DirClosedSection dp1, DirClosedSection dp2 -> DirPath.equal dp1 dp2
+| _ -> false
type reference =
- | Qualid of qualid located
- | Ident of identifier located
+ | Qualid of qualid Loc.located
+ | Ident of Id.t Loc.located
let qualid_of_reference = function
| Qualid (loc,qid) -> loc, qid
@@ -312,31 +188,44 @@ let qualid_of_reference = function
let string_of_reference = function
| Qualid (loc,qid) -> string_of_qualid qid
- | Ident (loc,id) -> string_of_id id
+ | Ident (loc,id) -> Id.to_string id
let pr_reference = function
| Qualid (_,qid) -> pr_qualid qid
- | Ident (_,id) -> pr_id id
+ | Ident (_,id) -> str (Id.to_string id)
let loc_of_reference = function
| Qualid (loc,qid) -> loc
| Ident (loc,id) -> loc
-(* popping one level of section in global names *)
-
-let pop_con con =
- let (mp,dir,l) = repr_con con in
- Names.make_con mp (pop_dirpath dir) l
-
-let pop_kn kn =
- let (mp,dir,l) = repr_mind kn in
- Names.make_mind mp (pop_dirpath dir) l
-
-let pop_global_reference = function
- | ConstRef con -> ConstRef (pop_con con)
- | IndRef (kn,i) -> IndRef (pop_kn kn,i)
- | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j)
- | VarRef id -> anomaly "VarRef not poppable"
+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
+| _ -> false
+
+let join_reference ns r =
+ match ns , r with
+ Qualid (_, q1), Qualid (loc, q2) ->
+ let (dp1,id1) = repr_qualid q1 in
+ let (dp2,id2) = repr_qualid q2 in
+ Qualid (loc,
+ make_qualid
+ (append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2)
+ id2)
+ | Qualid (_, q1), Ident (loc, id2) ->
+ let (dp1,id1) = repr_qualid q1 in
+ Qualid (loc,
+ make_qualid
+ (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1)))
+ id2)
+ | Ident (_, id1), Qualid (loc, q2) ->
+ let (dp2,id2) = repr_qualid q2 in
+ Qualid (loc, make_qualid
+ (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2)
+ id2)
+ | Ident (_, id1), Ident (loc, id2) ->
+ Qualid (loc, make_qualid
+ (dirpath_of_string (Names.Id.to_string id1)) id2)
(* Deprecated synonyms *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 09:45:35 +0000