From 6d961ac24305f26e896b602bdabe0e9c3c7cbf05 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:09:15 +0000 Subject: global_reference migrated from Libnames to new Globnames, less deps in grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/libnames.ml | 169 +--------------------------------------------------- 1 file changed, 1 insertion(+), 168 deletions(-) (limited to 'library/libnames.ml') diff --git a/library/libnames.ml b/library/libnames.ml index 24f083887..37ae97ace 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -10,123 +10,6 @@ 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 (**********************************************) @@ -236,32 +119,6 @@ let restrict_path n sp = 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!" - (*s qualified names *) type qualid = full_path @@ -295,14 +152,6 @@ type global_dir_reference = | 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 @@ -317,28 +166,12 @@ let string_of_reference = function let pr_reference = function | Qualid (_,qid) -> pr_qualid qid - | Ident (_,id) -> pr_id id + | Ident (_,id) -> str (string_of_id 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" - (* Deprecated synonyms *) let make_short_qualid = qualid_of_ident -- cgit v1.2.3