From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 1 Feb 2009 00:54:40 +0100 Subject: Imported Upstream version 8.2~rc2+dfsg --- kernel/declarations.ml | 8 ++-- kernel/declarations.mli | 8 ++-- kernel/indtypes.ml | 5 ++- kernel/indtypes.mli | 3 +- kernel/inductive.ml | 5 ++- kernel/mod_typing.ml | 115 ++++++++++++++++++++++++++++++++++-------------- kernel/modops.ml | 115 ++++++++++++++++++++++++++---------------------- kernel/names.ml | 14 ++++-- kernel/names.mli | 5 ++- kernel/safe_typing.ml | 15 +++++-- kernel/subtyping.ml | 16 +++---- kernel/univ.ml | 23 +++++++--- 12 files changed, 214 insertions(+), 118 deletions(-) (limited to 'kernel') diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 6e99bf79..f4827029 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.ml 10664 2008-03-14 11:27:37Z soubiran $ i*) +(*i $Id: declarations.ml 11417 2008-09-17 15:06:57Z soubiran $ i*) (*i*) open Util @@ -251,7 +251,8 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * constraints option + | SFBalias of module_path * struct_expr_body option + * constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -265,7 +266,8 @@ and struct_expr_body = | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * constraints + With_module_body of identifier list * module_path + * struct_expr_body option * constraints | With_definition_body of identifier list * constant_body and module_body = diff --git a/kernel/declarations.mli b/kernel/declarations.mli index fa03a338..b4f5f1f7 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.mli 10664 2008-03-14 11:27:37Z soubiran $ i*) +(*i $Id: declarations.mli 11417 2008-09-17 15:06:57Z soubiran $ i*) (*i*) open Names @@ -181,7 +181,8 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * constraints option + | SFBalias of module_path * struct_expr_body option + *constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -195,7 +196,8 @@ and struct_expr_body = | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * constraints + With_module_body of identifier list * module_path + * struct_expr_body option * constraints | With_definition_body of identifier list * constant_body and module_body = diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 01b8aca1..06764834 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: indtypes.ml 11784 2009-01-14 11:36:32Z herbelin $ *) open Util open Names @@ -46,6 +46,7 @@ type inductive_error = | SameNamesOverlap of identifier list | NotAnArity of identifier | BadEntry + | LargeNonPropInductiveNotInType exception InductiveError of inductive_error @@ -266,7 +267,7 @@ let typecheck_inductive env mie = | Prop Pos when engagement env <> Some ImpredicativeSet -> (* Predicative set: check that the content is indeed predicative *) if not (is_type0m_univ lev) & not (is_type0_univ lev) then - error "Large non-propositional inductive types must be in Type."; + raise (InductiveError LargeNonPropInductiveNotInType); Inl (info,full_arity,s), cst | Prop _ -> Inl (info,full_arity,s), cst in diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 0477df82..90ae70c3 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: indtypes.mli 10425 2008-01-05 17:04:16Z herbelin $ i*) +(*i $Id: indtypes.mli 11784 2009-01-14 11:36:32Z herbelin $ i*) (*i*) open Names @@ -33,6 +33,7 @@ type inductive_error = | SameNamesOverlap of identifier list | NotAnArity of identifier | BadEntry + | LargeNonPropInductiveNotInType exception InductiveError of inductive_error diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 4bb8e9d6..99ec1650 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: inductive.ml 11647 2008-12-02 10:40:11Z barras $ *) open Util open Names @@ -683,7 +683,8 @@ let check_one_fix renv recpos def = List.iter (check_rec_call renv) l | Some c -> try List.iter (check_rec_call renv) l - with FixGuardError _ -> check_rec_call renv (applist(c,l)) + with FixGuardError _ -> + check_rec_call renv (applist(lift p c,l)) end | Case (ci,p,c_0,lrest) -> diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 6840febd..4a9fb606 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_typing.ml 11170 2008-06-25 08:31:04Z soubiran $ i*) +(*i $Id: mod_typing.ml 11514 2008-10-28 13:39:02Z soubiran $ i*) open Util open Names @@ -37,14 +37,46 @@ let rec list_fold_map2 f e = function let e'',t1',t2' = list_fold_map2 f e' t in e'',h1'::t1',h2'::t2' +let rec rebuild_mp mp l = + match l with + []-> mp + | i::r -> rebuild_mp (MPdot(mp,i)) r + +let type_of_struct env b meb = + let rec aux env = function + | SEBfunctor (mp,mtb,body) -> + let env = add_module (MPbound mp) (module_body_of_type mtb) env in + SEBfunctor(mp,mtb, aux env body) + | SEBident mp -> + strengthen env (lookup_modtype mp env).typ_expr mp + | SEBapply _ as mtb -> eval_struct env mtb + | str -> str + in + if b then + Some (aux env meb) + else + None + +let rec bounded_str_expr = function + | SEBfunctor (mp,mtb,body) -> bounded_str_expr body + | SEBident mp -> (check_bound_mp mp) + | SEBapply (f,a,_)->(bounded_str_expr f) + | _ -> false + +let return_opt_type mp env mtb = + if (check_bound_mp mp) then + Some (strengthen env mtb.typ_expr mp) + else + None + let rec check_with env mtb with_decl = match with_decl with | With_Definition (id,_) -> let cb = check_with_aux_def env mtb with_decl in SEBwith(mtb,With_definition_body(id,cb)),empty_subst | With_Module (id,mp) -> - let cst,sub = check_with_aux_mod env mtb with_decl true in - SEBwith(mtb,With_module_body(id,mp,cst)),sub + let cst,sub,typ_opt = check_with_aux_mod env mtb with_decl true in + SEBwith(mtb,With_module_body(id,mp,typ_opt,cst)),sub and check_with_aux_def env mtb with_decl = let msid,sig_b = match (eval_struct env mtb) with @@ -140,7 +172,7 @@ and check_with_aux_mod env mtb with_decl now = | With_Module ([id], mp) -> let old,alias = match spec with SFBmodule msb -> Some msb,None - | SFBalias (mp',cst) -> None,Some (mp',cst) + | SFBalias (mp',_,cst) -> None,Some (mp',cst) | _ -> error_not_a_module (string_of_label l) in let mtb' = lookup_modtype mp env' in @@ -164,35 +196,48 @@ and check_with_aux_mod env mtb with_decl now = in if now then let mp' = scrape_alias mp env' in - let up_subst = update_subst mtb'.typ_alias (map_mp (mp_rec [id]) mp') in - cst, (join (map_mp (mp_rec [id]) mp') up_subst) + let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in + let up_subst = update_subst sub (map_mp (mp_rec [id]) mp') in + cst, (join (map_mp (mp_rec [id]) mp') up_subst),(return_opt_type mp env' mtb') else - cst,empty_subst + cst,empty_subst,(return_opt_type mp env' mtb') | With_Module (_::_,mp) -> - let old = match spec with - SFBmodule msb -> msb + let old,alias = match spec with + SFBmodule msb -> Some msb, None + | SFBalias (mpold,typ_opt,cst)->None, Some mpold | _ -> error_not_a_module (string_of_label l) in begin - match old.mod_expr with - None -> - let new_with_decl = match with_decl with - With_Definition (_,c) -> - With_Definition (idl,c) - | With_Module (_,c) -> With_Module (idl,c) in - let cst,_ = - check_with_aux_mod env' - (type_of_mb env old) new_with_decl false in - if now then - let mtb' = lookup_modtype mp env' in - let mp' = scrape_alias mp env' in - let up_subst = update_subst - mtb'.typ_alias (map_mp (mp_rec (List.rev (id::idl))) mp') in - cst, (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst) + if alias = None then + let old = Option.get old in + match old.mod_expr with + None -> + let new_with_decl = match with_decl with + With_Definition (_,c) -> + With_Definition (idl,c) + | With_Module (_,c) -> With_Module (idl,c) in + let cst,_,typ_opt = + check_with_aux_mod env' + (type_of_mb env' old) new_with_decl false in + if now then + let mtb' = lookup_modtype mp env' in + let mp' = scrape_alias mp env' in + let _,sub = Modops.update_subst env' (module_body_of_type mtb') mp' in + let up_subst = update_subst + sub (map_mp (mp_rec (List.rev (id::idl))) mp') in + cst, + (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst), + typ_opt + else + cst,empty_subst,typ_opt + | Some msb -> + error_a_generative_module_expected l else - cst,empty_subst - | Some msb -> - error_a_generative_module_expected l + let mpold = Option.get alias in + let mpnew = rebuild_mp mpold (List.map label_of_id idl) in + check_modpath_equiv env' mpnew mp; + let mtb' = lookup_modtype mp env' in + Constraint.empty,empty_subst,(return_opt_type mp env' mtb') end | _ -> anomaly "Modtyping:incorrect use of with" with @@ -214,7 +259,9 @@ and translate_module env me = let meb,sub1 = translate_struct_entry env mexpr in let mod_typ,sub,cst = match me.mod_entry_type with - | None -> None,sub1,Constraint.empty + | None -> + (type_of_struct env (bounded_str_expr meb) meb) + ,sub1,Constraint.empty | Some mte -> let mtb2,sub2 = translate_struct_entry env mte in let cst = check_subtypes env @@ -304,7 +351,7 @@ let rec add_struct_expr_constraints env = function | SEBwith(meb,With_definition_body(_,cb))-> Environ.add_constraints cb.const_constraints (add_struct_expr_constraints env meb) - | SEBwith(meb,With_module_body(_,_,cst))-> + | SEBwith(meb,With_module_body(_,_,_,cst))-> Environ.add_constraints cst (add_struct_expr_constraints env meb) @@ -312,8 +359,8 @@ and add_struct_elem_constraints env = function | SFBconst cb -> Environ.add_constraints cb.const_constraints env | SFBmind mib -> Environ.add_constraints mib.mind_constraints env | SFBmodule mb -> add_module_constraints env mb - | SFBalias (mp,Some cst) -> Environ.add_constraints cst env - | SFBalias (mp,None) -> env + | SFBalias (mp,_,Some cst) -> Environ.add_constraints cst env + | SFBalias (mp,_,None) -> env | SFBmodtype mtb -> add_modtype_constraints env mtb and add_module_constraints env mb = @@ -352,15 +399,15 @@ let rec struct_expr_constraints cst = function | SEBwith(meb,With_definition_body(_,cb))-> struct_expr_constraints (Univ.Constraint.union cb.const_constraints cst) meb - | SEBwith(meb,With_module_body(_,_,cst1))-> + | SEBwith(meb,With_module_body(_,_,_,cst1))-> struct_expr_constraints (Univ.Constraint.union cst1 cst) meb and struct_elem_constraints cst = function | SFBconst cb -> cst | SFBmind mib -> cst | SFBmodule mb -> module_constraints cst mb - | SFBalias (mp,Some cst1) -> Univ.Constraint.union cst1 cst - | SFBalias (mp,None) -> cst + | SFBalias (mp,_,Some cst1) -> Univ.Constraint.union cst1 cst + | SFBalias (mp,_,None) -> cst | SFBmodtype mtb -> modtype_constraints cst mtb and module_constraints cst mb = diff --git a/kernel/modops.ml b/kernel/modops.ml index 7bed3254..25a11c69 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id: modops.ml 11514 2008-10-28 13:39:02Z soubiran $ i*) (*i*) open Util @@ -113,16 +113,18 @@ let module_body_of_type mtb = mod_retroknowledge = []} let module_type_of_module mp mb = - {typ_expr = + let mp1,expr = (match mb.mod_type with - | Some expr -> expr + | Some expr -> mp,expr | None -> (match mb.mod_expr with - | Some expr -> expr + | Some (SEBident mp') ->(Some mp'),(SEBident mp') + | Some expr -> mp,expr | None -> - anomaly "Modops: empty expr and type")); - typ_alias = mb.mod_alias; - typ_strength = mp - } + anomaly "Modops: empty expr and type")) in + {typ_expr = expr; + typ_alias = mb.mod_alias; + typ_strength = mp1 + } let rec check_modpath_equiv env mp1 mp2 = if mp1=mp2 then () else @@ -132,13 +134,14 @@ let rec check_modpath_equiv env mp1 mp2 = else error_not_equal mp1 mp2 -let subst_with_body sub = function - | With_module_body(id,mp,cst) -> - With_module_body(id,subst_mp sub mp,cst) +let rec subst_with_body sub = function + | With_module_body(id,mp,typ_opt,cst) -> + With_module_body(id,subst_mp sub mp,Option.smartmap + (subst_struct_expr sub) typ_opt,cst) | With_definition_body(id,cb) -> With_definition_body( id,subst_const_body sub cb) -let rec subst_modtype sub mtb = +and subst_modtype sub mtb = let typ_expr' = subst_struct_expr sub mtb.typ_expr in if typ_expr'==mtb.typ_expr then mtb @@ -156,8 +159,9 @@ and subst_structure sub sign = SFBmodule (subst_module sub mb) | SFBmodtype mtb -> SFBmodtype (subst_modtype sub mtb) - | SFBalias (mp,cst) -> - SFBalias (subst_mp sub mp,cst) + | SFBalias (mp,typ_opt,cst) -> + SFBalias (subst_mp sub mp,Option.smartmap + (subst_struct_expr sub) typ_opt,cst) in List.map (fun (l,b) -> (l,subst_body b)) sign @@ -277,7 +281,7 @@ let rec eval_struct env = function | SEBwith (mtb,(With_definition_body _ as wdb)) -> let mtb',_ = merge_with env mtb wdb empty_subst in mtb' - | SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) -> + | SEBwith (mtb, (With_module_body (_,mp,_,_) as wdb)) -> let alias_in_mp = (lookup_modtype mp env).typ_alias in let alias_in_mp = match eval_struct env (SEBident mp) with @@ -303,8 +307,8 @@ and merge_with env mtb with_decl alias= | _ -> error_signature_expected mtb in let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) -> id,idl - | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false + | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl + | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false in let l = label_of_id id in try @@ -314,47 +318,54 @@ and merge_with env mtb with_decl alias= | [] -> MPself msid | i::r -> MPdot(mp_rec r,label_of_id i) in + let env' = add_signature (MPself msid) before env in let new_spec,subst = match with_decl with | With_definition_body ([],_) - | With_module_body ([],_,_) -> assert false + | With_module_body ([],_,_,_) -> assert false | With_definition_body ([id],c) -> SFBconst c,None - | With_module_body ([id], mp,cst) -> - let mp' = scrape_alias mp env in + | With_module_body ([id], mp,typ_opt,cst) -> + let mp' = scrape_alias mp env' in let new_alias = update_subst alias (map_mp (mp_rec [id]) mp') in - SFBalias (mp,Some cst), + SFBalias (mp,typ_opt,Some cst), Some(join (map_mp (mp_rec [id]) mp') new_alias) | With_definition_body (_::_,_) - | With_module_body (_::_,_,_) -> - let old = match spec with - SFBmodule msb -> msb + | With_module_body (_::_,_,_,_) -> + let old,aliasold = match spec with + SFBmodule msb -> Some msb, None + | SFBalias (mpold,typ_opt,cst) ->None, Some (mpold,typ_opt,cst) | _ -> error_not_a_module (string_of_label l) in - let new_with_decl,subst1 = - match with_decl with - With_definition_body (_,c) -> With_definition_body (idl,c),None - | With_module_body (idc,mp,cst) -> - let mp' = scrape_alias mp env in - With_module_body (idl,mp,cst), - Some(map_mp (mp_rec (List.rev idc)) mp') - in - let subst = match subst1 with - | None -> None - | Some s -> Some (join s (update_subst alias s)) in - let modtype,subst_msb = - merge_with env (type_of_mb env old) new_with_decl alias in - let msb = - { mod_expr = None; - mod_type = Some modtype; - mod_constraints = old.mod_constraints; - mod_alias = begin - match subst_msb with - |None -> empty_subst - |Some s -> s - end; - mod_retroknowledge = old.mod_retroknowledge} - in - (SFBmodule msb),subst + if aliasold = None then + let old = Option.get old in + let new_with_decl,subst1 = + match with_decl with + With_definition_body (_,c) -> With_definition_body (idl,c),None + | With_module_body (idc,mp,typ_opt,cst) -> + let mp' = scrape_alias mp env' in + With_module_body (idl,mp,typ_opt,cst), + Some(map_mp (mp_rec (List.rev idc)) mp') + in + let subst = match subst1 with + | None -> None + | Some s -> Some (join s (update_subst alias s)) in + let modtype,subst_msb = + merge_with env' (type_of_mb env' old) new_with_decl alias in + let msb = + { mod_expr = None; + mod_type = Some modtype; + mod_constraints = old.mod_constraints; + mod_alias = begin + match subst_msb with + |None -> empty_subst + |Some s -> s + end; + mod_retroknowledge = old.mod_retroknowledge} + in + (SFBmodule msb),subst + else + let mpold,typ_opt,cst = Option.get aliasold in + SFBalias (mpold,typ_opt,cst),None in SEBstruct(msid, before@(l,new_spec):: (Option.fold_right subst_structure subst after)),subst @@ -371,7 +382,7 @@ and add_signature mp sign env = | SFBmodule mb -> add_module (MPdot (mp,l)) mb env (* adds components as well *) - | SFBalias (mp1,cst) -> + | SFBalias (mp1,_,cst) -> Environ.register_alias (MPdot(mp,l)) mp1 env | SFBmodtype mtb -> Environ.add_modtype (MPdot(mp,l)) mtb env @@ -402,7 +413,7 @@ and constants_of_specification env mp sign = let new_env = add_module (MPdot (mp,l)) mb env in new_env,(constants_of_modtype env (MPdot (mp,l)) (type_of_mb env mb)) @ res - | SFBalias (mp1,cst) -> + | SFBalias (mp1,typ_opt,cst) -> let new_env = register_alias (MPdot (mp,l)) mp1 env in new_env,(constants_of_modtype env (MPdot (mp,l)) (eval_struct env (SEBident mp1))) @ res @@ -494,7 +505,7 @@ and strengthen_sig env msid sign mp = match sign with (MPdot (MPself msid,l)) mb env in let rest' = strengthen_sig env' msid rest mp in item':: rest' - | ((l,SFBalias (mp1,cst)) as item) :: rest -> + | ((l,SFBalias (mp1,_,cst)) as item) :: rest -> let env' = register_alias (MPdot(MPself msid,l)) mp1 env in let rest' = strengthen_sig env' msid rest mp in item::rest' diff --git a/kernel/names.ml b/kernel/names.ml index 25f03495..b4dcd7c8 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: names.ml 11238 2008-07-19 09:34:03Z herbelin $ *) +(* $Id: names.ml 11750 2009-01-05 20:47:34Z herbelin $ *) open Pp open Util @@ -17,7 +17,7 @@ type identifier = string let id_ord = Pervasives.compare -let id_of_string s = check_ident s; String.copy s +let id_of_string s = check_ident_soft s; String.copy s let string_of_id id = String.copy id @@ -86,6 +86,7 @@ type label = string type mod_self_id = uniq_ident let make_msid = make_uid +let repr_msid (n, id, dp) = (n, id, dp) let debug_string_of_msid = debug_string_of_uid let refresh_msid (_,s,dir) = make_uid dir s let string_of_msid = string_of_uid @@ -94,6 +95,7 @@ let label_of_msid (_,s,_) = s type mod_bound_id = uniq_ident let make_mbid = make_uid +let repr_mbid (n, id, dp) = (n, id, dp) let debug_string_of_mbid = debug_string_of_uid let string_of_mbid = string_of_uid let id_of_mbid (_,s,_) = s @@ -115,8 +117,14 @@ type module_path = | MPself of mod_self_id | MPdot of module_path * label + +let rec check_bound_mp = function + | MPbound _ -> true + | MPdot(mp,_) ->check_bound_mp mp + | _ -> false + let rec string_of_mp = function - | MPfile sl -> string_of_dirpath sl + | MPfile sl -> "MPfile (" ^ string_of_dirpath sl ^ ")" | MPbound uid -> string_of_uid uid | MPself uid -> string_of_uid uid | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l diff --git a/kernel/names.mli b/kernel/names.mli index c6f59048..49b10bfe 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: names.mli 10919 2008-05-11 22:04:26Z msozeau $ i*) +(*i $Id: names.mli 11582 2008-11-12 19:49:57Z notin $ i*) (*s Identifiers *) @@ -48,6 +48,7 @@ type mod_self_id (* The first argument is a file name - to prevent conflict between different files *) val make_msid : dir_path -> string -> mod_self_id +val repr_msid : mod_self_id -> int * string * dir_path val id_of_msid : mod_self_id -> identifier val label_of_msid : mod_self_id -> label val refresh_msid : mod_self_id -> mod_self_id @@ -58,6 +59,7 @@ val string_of_msid : mod_self_id -> string type mod_bound_id val make_mbid : dir_path -> string -> mod_bound_id +val repr_mbid : mod_bound_id -> int * string * dir_path val id_of_mbid : mod_bound_id -> identifier val label_of_mbid : mod_bound_id -> label val debug_string_of_mbid : mod_bound_id -> string @@ -82,6 +84,7 @@ type module_path = | MPdot of module_path * label (*i | MPapply of module_path * module_path in the future (maybe) i*) +val check_bound_mp : module_path -> bool val string_of_mp : module_path -> string diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 3c7461b2..fbb05a2d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: safe_typing.ml 11453 2008-10-15 14:42:34Z soubiran $ *) open Util open Names @@ -312,6 +312,13 @@ let add_alias l mp senv = check_label l senv.labset; let mp' = MPdot(senv.modinfo.modpath, l) in let mp1 = scrape_alias mp senv.env in + let typ_opt = + if check_bound_mp mp then + Some (strengthen senv.env + (lookup_modtype mp senv.env).typ_expr mp) + else + None + in (* we get all updated alias substitution {mp1.K\M} that comes from mp1 *) let _,sub = Modops.update_subst senv.env (lookup_module mp1 senv.env) mp1 in (* transformation of {mp1.K\M} to {mp.K\M}*) @@ -327,7 +334,7 @@ let add_alias l mp senv = alias_subst = join senv.modinfo.alias_subst sub}; labset = Labset.add l senv.labset; - revstruct = (l,SFBalias (mp,None))::senv.revstruct; + revstruct = (l,SFBalias (mp,typ_opt,None))::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; @@ -502,7 +509,7 @@ let end_module l restype senv = imports = senv'.imports; loads = senv'.loads; local_retroknowledge = senv'.local_retroknowledge } - | SFBalias (mp',cst) -> + | SFBalias (mp',typ_opt,cst) -> let env' = Option.fold_right Environ.add_constraints cst senv.env in let mp = MPdot(senv.modinfo.modpath, l) in @@ -518,7 +525,7 @@ let end_module l restype senv = alias_subst = join senv.modinfo.alias_subst sub}; labset = Labset.add l senv.labset; - revstruct = (l,SFBalias (mp',cst))::senv.revstruct; + revstruct = (l,SFBalias (mp',typ_opt,cst))::senv.revstruct; univ = senv.univ; engagement = senv.engagement; imports = senv.imports; diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 14020c0b..98ee1dbb 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtyping.ml 11142 2008-06-18 15:37:31Z soubiran $ i*) +(*i $Id: subtyping.ml 11453 2008-10-15 14:42:34Z soubiran $ i*) (*i*) open Util @@ -33,7 +33,7 @@ type namedobject = | IndConstr of constructor * mutual_inductive_body | Module of module_body | Modtype of module_type_body - | Alias of module_path + | Alias of module_path * struct_expr_body option (* adds above information about one mutual inductive: all types and constructors *) @@ -64,7 +64,7 @@ let make_label_map mp list = add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map | SFBmodule mb -> add_map (Module mb) | SFBmodtype mtb -> add_map (Modtype mtb) - | SFBalias (mp,cst) -> add_map (Alias mp) + | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt)) in List.fold_right add_one list Labmap.empty @@ -352,23 +352,23 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = begin match info1 with | Module msb -> check_modules cst env msid1 l msb msb2 alias - | Alias mp ->let msb = + | Alias (mp,typ_opt) ->let msb = {mod_expr = Some (SEBident mp); - mod_type = Some (eval_struct env (SEBident mp)); + mod_type = typ_opt; mod_constraints = Constraint.empty; mod_alias = (lookup_modtype mp env).typ_alias; mod_retroknowledge = []} in check_modules cst env msid1 l msb msb2 alias | _ -> error_not_match l spec2 end - | SFBalias (mp,_) -> + | SFBalias (mp,typ_opt,_) -> begin match info1 with - | Alias mp1 -> check_modpath_equiv env mp mp1; cst + | Alias (mp1,_) -> check_modpath_equiv env mp mp1; cst | Module msb -> let msb1 = {mod_expr = Some (SEBident mp); - mod_type = Some (eval_struct env (SEBident mp)); + mod_type = typ_opt; mod_constraints = Constraint.empty; mod_alias = (lookup_modtype mp env).typ_alias; mod_retroknowledge = []} in diff --git a/kernel/univ.ml b/kernel/univ.ml index 11a5452c..3d254ce6 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml 11301 2008-08-04 19:41:18Z herbelin $ *) +(* $Id: univ.ml 11596 2008-11-16 15:34:06Z letouzey $ *) (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) @@ -43,13 +43,25 @@ type universe_level = | Set | Level of Names.dir_path * int +(* A specialized comparison function: we compare the [int] part first. + This way, most of the time, the [dir_path] part is not considered. *) + +let cmp_univ_level u v = match u,v with + | Set, Set -> 0 + | Set, _ -> -1 + | _, Set -> 1 + | Level (dp1,i1), Level (dp2,i2) -> + if i1 < i2 then -1 + else if i1 > i2 then 1 + else compare dp1 dp2 + type universe = | Atom of universe_level | Max of universe_level list * universe_level list module UniverseOrdered = struct type t = universe_level - let compare = Pervasives.compare + let compare = cmp_univ_level end let string_of_univ_level = function @@ -86,7 +98,8 @@ let super = function Used to type the products. *) let sup u v = match u,v with - | Atom u, Atom v -> if u = v then Atom u else Max ([u;v],[]) + | Atom u, Atom v -> + if cmp_univ_level u v = 0 then Atom u else Max ([u;v],[]) | u, Max ([],[]) -> u | Max ([],[]), v -> v | Atom u, Max (gel,gtl) -> Max (list_add_set u gel,gtl) @@ -601,12 +614,12 @@ let dump_universes output g = let u_str = string_of_univ_level u in List.iter (fun v -> - Printf.fprintf output "%s > %s ;\n" u_str + Printf.fprintf output "%s < %s ;\n" u_str (string_of_univ_level v)) lt; List.iter (fun v -> - Printf.fprintf output "%s >= %s ;\n" u_str + Printf.fprintf output "%s <= %s ;\n" u_str (string_of_univ_level v)) le | Equiv (u,v) -> -- cgit v1.2.3