diff options
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 61 |
1 files changed, 25 insertions, 36 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 16f5a917..536a382d 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -6,13 +6,14 @@ (* * 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*) +(*i $Id: libnames.ml 7052 2005-05-20 15:54:50Z herbelin $ i*) open Pp open Util open Names open Nameops open Term +open Mod_subst type global_reference = | VarRef of variable @@ -21,30 +22,34 @@ type global_reference = | ConstructRef of constructor let subst_global subst ref = match ref with - | VarRef _ -> ref + | VarRef var -> ref, mkVar var | ConstRef kn -> - let kn' = subst_kn subst kn in if kn==kn' then ref else - 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 if kn==kn' then ref else - IndRef(kn',i) + let kn' = subst_kn subst kn in + if kn==kn' then ref, mkInd (kn,i) else IndRef(kn',i), mkInd (kn',i) | ConstructRef ((kn,i),j) -> - let kn' = subst_kn subst kn in if kn==kn' then ref else - ConstructRef ((kn',i),j) + let kn' = subst_kn subst kn in + if kn==kn' then ref, mkConstruct ((kn,i),j) + else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j) -let reference_of_constr c = match kind_of_term c with +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_reference = function +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 + module RefOrdered = struct type t = global_reference @@ -54,24 +59,8 @@ module RefOrdered = 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)) @@ -188,18 +177,10 @@ 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 encode_con dir id = make_con (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 @@ -207,6 +188,13 @@ let decode_kn kn = | _ , [] -> anomaly "MPfile expected!" | _ -> 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!" + (*s qualified names *) type qualid = section_path @@ -267,3 +255,4 @@ let pr_reference = function let loc_of_reference = function | Qualid (loc,qid) -> loc | Ident (loc,id) -> loc + |