diff options
author | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /library/libnames.ml | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'library/libnames.ml')
-rw-r--r-- | library/libnames.ml | 147 |
1 files changed, 86 insertions, 61 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 89a77128..9a7135ea 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: libnames.ml 11878 2009-02-03 12:48:18Z soubiran $ i*) +(*i $Id$ i*) open Pp open Util @@ -23,24 +23,49 @@ type global_reference = | 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_kn subst kn in + 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_kn subst kn in + 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 @@ -57,16 +82,32 @@ let constr_of_global = function let constr_of_reference = constr_of_global let reference_of_constr = global_of_constr -module RefOrdered = - struct - type t = global_reference - let compare = Pervasives.compare - end - +(* outside of the kernel, names are ordered on their canonical part *) +module RefOrdered = struct + type t = global_reference + let compare x y = + let make_name = 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 + in + Pervasives.compare (make_name x) (make_name y) +end + module Refset = Set.Make(RefOrdered) module Refmap = Map.Make(RefOrdered) + +(* Extended global references *) + +type syndef_name = kernel_name -let inductives_table = ref Indmap.empty +type extended_global_reference = + | TrueGlobal of global_reference + | SynDef of syndef_name (**********************************************) @@ -75,10 +116,10 @@ let pr_dirpath sl = (str (string_of_dirpath sl)) (*s Operations on dirpaths *) (* Pop the last n module idents *) -let extract_dirpath_prefix n dir = +let pop_dirpath_n n dir = make_dirpath (list_skipn n (repr_dirpath dir)) -let dirpath_prefix p = match repr_dirpath p with +let pop_dirpath p = match repr_dirpath p with | [] -> anomaly "dirpath_prefix: empty dirpath" | _::l -> make_dirpath l @@ -101,24 +142,8 @@ let add_dirpath_prefix id d = make_dirpath (repr_dirpath d @ [id]) let split_dirpath d = let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l) -let extend_dirpath p id = make_dirpath (id :: repr_dirpath p) +let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p) - -(* -let path_of_constructor env ((sp,tyi),ind) = - let mib = Environ.lookup_mind sp env in - let mip = mib.mind_packets.(tyi) in - let (pa,_) = repr_path sp in - Names.make_path pa (mip.mind_consnames.(ind-1)) - -let path_of_inductive env (sp,tyi) = - if tyi = 0 then sp - else - let mib = Environ.lookup_mind sp env in - let mip = mib.mind_packets.(tyi) in - let (pa,_) = repr_path sp in - Names.make_path pa (mip.mind_typename) -*) (* parsing *) let parse_dir s = let len = String.length s in @@ -127,24 +152,27 @@ let parse_dir s = if n >= len then dirs else let pos = try - String.index_from s n '.' + String.index_from s n '.' with Not_found -> len in if 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 + + 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) (*s Section paths are absolute names *) -type section_path = { +type full_path = { dirpath : dir_path ; basename : identifier } @@ -165,7 +193,7 @@ let sp_ord sp1 sp2 = module SpOrdered = struct - type t = section_path + type t = full_path let compare = sp_ord end @@ -183,41 +211,33 @@ let path_of_string s = with | Invalid_argument _ -> invalid_arg "path_of_string" -let pr_sp sp = str (string_of_path sp) +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 -type extended_global_reference = - | TrueGlobal of global_reference - | SyntacticDef of kernel_name - -let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id) +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_kn kn = +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) - | MPself msid -> - let _,_,dp = repr_msid msid in - let id = id_of_msid msid in - id::(repr_dirpath dp) | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp) in - let mp,sec_dir,l = repr_kn kn 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 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) @@ -225,31 +245,31 @@ let decode_con kn = | _ -> anomaly "Section part should be empty!" (*s qualified names *) -type qualid = section_path +type qualid = full_path let make_qualid = make_path let repr_qualid = repr_path let string_of_qualid = string_of_path -let pr_qualid = pr_sp +let pr_qualid = pr_path let qualid_of_string = path_of_string -let qualid_of_sp sp = sp -let make_short_qualid id = make_qualid empty_dirpath id -let qualid_of_dirpath dir = +let qualid_of_path sp = sp +let qualid_of_ident id = make_qualid empty_dirpath id +let qualid_of_dirpath dir = let (l,a) = split_dirpath dir in make_qualid l a -type object_name = section_path * kernel_name +type object_name = full_path * kernel_name type object_prefix = dir_path * (module_path * dir_path) -let make_oname (dirpath,(mp,dir)) id = +let make_oname (dirpath,(mp,dir)) id = make_path dirpath id, make_kn mp dir (label_of_id id) (* to this type are mapped dir_path's in the nametab *) -type global_dir_reference = +type global_dir_reference = | DirOpenModule of object_prefix | DirOpenModtype of object_prefix | DirOpenSection of object_prefix @@ -265,19 +285,19 @@ type global_dir_reference = ModTypeRef kn' *) -type reference = +type reference = | Qualid of qualid located | Ident of identifier located let qualid_of_reference = function | Qualid (loc,qid) -> loc, qid - | Ident (loc,id) -> loc, make_short_qualid id + | Ident (loc,id) -> loc, qualid_of_ident id let string_of_reference = function | Qualid (loc,qid) -> string_of_qualid qid | Ident (loc,id) -> string_of_id id -let pr_reference = function +let pr_reference = function | Qualid (_,qid) -> pr_qualid qid | Ident (_,id) -> pr_id id @@ -289,14 +309,19 @@ let loc_of_reference = function let pop_con con = let (mp,dir,l) = repr_con con in - Names.make_con mp (dirpath_prefix dir) l + Names.make_con mp (pop_dirpath dir) l let pop_kn kn = - let (mp,dir,l) = repr_kn kn in - Names.make_kn mp (dirpath_prefix dir) l + 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" + +(* Deprecated synonyms *) + +let make_short_qualid = qualid_of_ident +let qualid_of_sp = qualid_of_path |