diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /library/libnames.ml |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'library/libnames.ml')
-rw-r--r-- | library/libnames.ml | 269 |
1 files changed, 269 insertions, 0 deletions
diff --git a/library/libnames.ml b/library/libnames.ml new file mode 100644 index 00000000..16f5a917 --- /dev/null +++ b/library/libnames.ml @@ -0,0 +1,269 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: libnames.ml,v 1.11.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) + +open Pp +open Util +open Names +open Nameops +open Term + +type global_reference = + | VarRef of variable + | ConstRef of constant + | IndRef of inductive + | ConstructRef of constructor + +let subst_global subst ref = match ref with + | VarRef _ -> ref + | ConstRef kn -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + ConstRef kn' + | IndRef (kn,i) -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + IndRef(kn',i) + | ConstructRef ((kn,i),j) -> + let kn' = subst_kn subst kn in if kn==kn' then ref else + ConstructRef ((kn',i),j) + +let reference_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_reference = function + | VarRef id -> mkVar id + | ConstRef sp -> mkConst sp + | ConstructRef sp -> mkConstruct sp + | IndRef sp -> mkInd sp + +module RefOrdered = + struct + type t = global_reference + let compare = Pervasives.compare + end + +module Refset = Set.Make(RefOrdered) +module Refmap = Map.Make(RefOrdered) + +module InductiveOrdered = struct + type t = inductive + let compare (spx,ix) (spy,iy) = + let c = ix - iy in if c = 0 then compare spx spy else c +end + +module Indmap = Map.Make(InductiveOrdered) + +let inductives_table = ref Indmap.empty + +module ConstructorOrdered = struct + type t = constructor + let compare (indx,ix) (indy,iy) = + let c = ix - iy in if c = 0 then InductiveOrdered.compare indx indy else c +end + +module Constrmap = Map.Make(ConstructorOrdered) + +(**********************************************) + +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 = + make_dirpath (list_skipn n (repr_dirpath dir)) + +let dirpath_prefix p = match repr_dirpath p with + | [] -> anomaly "dirpath_prefix: empty dirpath" + | _::l -> make_dirpath l + +let is_dirpath_prefix_of d1 d2 = + list_prefix_of (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) + +(* 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 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 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 + let rec decoupe_dirs dirs n = + if n>=len then dirs else + let pos = + try + String.index_from s n '.' + with Not_found -> len + in + let dir = String.sub s n (pos-n) in + decoupe_dirs ((id_of_string dir)::dirs) (pos+1) + in + decoupe_dirs [] 0 + +let dirpath_of_string s = + match parse_dir s with + [] -> invalid_arg "dirpath_of_string" + | dir -> make_dirpath dir + +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 = { + dirpath : dir_path ; + basename : identifier } + +let make_path pa id = { dirpath = pa; basename = id } +let repr_path { dirpath = pa; basename = id } = (pa,id) + +(* 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) + +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 + +module SpOrdered = + struct + type t = section_path + let compare = sp_ord + end + +module Spset = Set.Make(SpOrdered) +module Sppred = Predicate.Make(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 + make_path dir id + with + | Invalid_argument _ -> invalid_arg "path_of_string" + +let pr_sp 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 subst_ext subst glref = match glref with + | TrueGlobal ref -> + let ref' = subst_global subst ref in + if ref' == ref then glref else + TrueGlobal ref' + | SyntacticDef kn -> + let kn' = subst_kn subst kn in + if kn' == kn then glref else + SyntacticDef kn' + +let encode_kn dir id = make_kn (MPfile dir) empty_dirpath (label_of_id id) + +let decode_kn kn = + let mp,sec_dir,l = repr_kn 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!" + +(*s qualified names *) +type qualid = section_path + +let make_qualid = make_path +let repr_qualid = repr_path + +let string_of_qualid = string_of_path +let pr_qualid = pr_sp + +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 (l,a) = split_dirpath dir in + make_qualid l a + +type object_name = section_path * kernel_name + +type object_prefix = dir_path * (module_path * dir_path) + +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 = + | DirOpenModule of object_prefix + | DirOpenModtype of object_prefix + | DirOpenSection of object_prefix + | DirModule of object_prefix + | DirClosedSection of dir_path + (* 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' +*) + +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 + +let string_of_reference = function + | Qualid (loc,qid) -> string_of_qualid qid + | Ident (loc,id) -> string_of_id id + +let pr_reference = function + | Qualid (_,qid) -> pr_qualid qid + | Ident (_,id) -> pr_id id + +let loc_of_reference = function + | Qualid (loc,qid) -> loc + | Ident (loc,id) -> loc |