diff options
| -rw-r--r-- | checker/declarations.ml | 19 | ||||
| -rw-r--r-- | checker/declarations.mli | 5 | ||||
| -rw-r--r-- | checker/mod_checking.ml | 26 | ||||
| -rw-r--r-- | checker/modops.ml | 24 | ||||
| -rw-r--r-- | checker/subtyping.ml | 14 | ||||
| -rw-r--r-- | contrib/extraction/extract_env.ml | 10 | ||||
| -rw-r--r-- | kernel/declarations.ml | 6 | ||||
| -rw-r--r-- | kernel/declarations.mli | 6 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 61 | ||||
| -rw-r--r-- | kernel/modops.ml | 39 | ||||
| -rw-r--r-- | kernel/names.ml | 5 | ||||
| -rw-r--r-- | kernel/names.mli | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 15 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 14 | ||||
| -rw-r--r-- | library/declaremods.ml | 8 | ||||
| -rw-r--r-- | parsing/printmod.ml | 6 |
16 files changed, 159 insertions, 101 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 71b6c9ca0b..ea41c64894 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -562,7 +562,7 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * Univ.constraints option + | SFBalias of module_path * struct_expr_body option * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -576,7 +576,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 * Univ.constraints + With_module_body of identifier list * module_path * + struct_expr_body option * Univ.constraints | With_definition_body of identifier list * constant_body and module_body = @@ -592,13 +593,14 @@ and module_type_body = typ_alias : substitution} -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 @@ -616,8 +618,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 diff --git a/checker/declarations.mli b/checker/declarations.mli index fdea3383b4..225f91604f 100644 --- a/checker/declarations.mli +++ b/checker/declarations.mli @@ -150,7 +150,7 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * Univ.constraints option + | SFBalias of module_path * struct_expr_body option * Univ.constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -164,7 +164,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 * Univ.constraints + With_module_body of identifier list * module_path * + struct_expr_body option * Univ.constraints | With_definition_body of identifier list * constant_body and module_body = diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 379273af91..af5e4f469a 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -145,9 +145,9 @@ and check_with_aux_def env mtb with_decl = | _ -> error_signature_expected mtb in let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) -> + | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl - | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false + | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false in let l = label_of_id id in try @@ -173,8 +173,8 @@ and check_with_aux_def env mtb with_decl = let new_with_decl = match with_decl with With_definition_body (_,c) -> With_definition_body (idl,c) - | With_module_body (_,c,cst) -> - With_module_body (idl,c,cst) in + | With_module_body (_,c,t,cst) -> + With_module_body (idl,c,t,cst) in check_with_aux_def env' (type_of_mb env old) new_with_decl | Some msb -> error_a_generative_module_expected l @@ -192,9 +192,9 @@ and check_with_aux_mod env mtb with_decl = msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b) | _ -> error_signature_expected mtb in let id,idl = match with_decl with - | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_) -> + | With_definition_body (id::idl,_) | With_module_body (id::idl,_,_,_) -> id,idl - | With_definition_body ([],_) | With_module_body ([],_,_) -> assert false + | With_definition_body ([],_) | With_module_body ([],_,_,_) -> assert false in let l = label_of_id id in try @@ -206,11 +206,11 @@ and check_with_aux_mod env mtb with_decl = in let env' = Modops.add_signature (MPself msid) before env in match with_decl with - | With_module_body ([],_,_) -> assert false - | With_module_body ([id], mp,_) -> + | With_module_body ([],_,_,_) -> assert false + | With_module_body ([id], mp,_,_) -> let old,alias = match spec with SFBmodule msb -> Some msb,None - | SFBalias (mp',_) -> None,Some mp' + | SFBalias (mp',_,_) -> None,Some mp' | _ -> error_not_a_module l in let mtb' = lookup_modtype mp env' in @@ -223,7 +223,7 @@ and check_with_aux_mod env mtb with_decl = anomaly "Mod_typing:no implementation and no alias" in join (map_mp (mp_rec [id]) mp) mtb'.typ_alias - | With_module_body (_::_,mp,_) -> + | With_module_body (_::_,mp,_,_) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -234,8 +234,8 @@ and check_with_aux_mod env mtb with_decl = let new_with_decl = match with_decl with With_definition_body (_,c) -> With_definition_body (idl,c) - | With_module_body (_,c,cst) -> - With_module_body (idl,c,cst) in + | With_module_body (_,c,t,cst) -> + With_module_body (idl,c,t,cst) in let sub = check_with_aux_mod env' (type_of_mb env old) new_with_decl in @@ -290,7 +290,7 @@ and check_structure_field (s,env) mp lab = function let is_fun, sub = Modops.update_subst env msb mp1 in ((if is_fun then s else join s sub), Modops.add_module (MPdot(mp,lab)) msb env) - | SFBalias(mp2,cst) -> + | SFBalias(mp2,_,cst) -> (* cf Safe_typing.add_alias *) (try let mp' = MPdot(mp,lab) in diff --git a/checker/modops.ml b/checker/modops.ml index f79e52c2e4..27ea4d55be 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -145,7 +145,7 @@ let rec eval_struct env = function (join sub_alias (map_mbid farg_id mp)) fbody_b) | SEBwith (mtb,(With_definition_body _ as wdb)) -> merge_with env mtb wdb empty_subst - | 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 merge_with env mtb wdb alias_in_mp @@ -167,8 +167,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 @@ -180,15 +180,15 @@ and merge_with env mtb with_decl alias= 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) -> + | With_module_body ([id], mp,typ_opt,cst) -> let mp' = scrape_alias mp env in - SFBalias (mp,Some cst), + SFBalias (mp,typ_opt,Some cst), Some(join (map_mp (mp_rec [id]) mp') alias) | With_definition_body (_::_,_) - | With_module_body (_::_,_,_) -> + | With_module_body (_::_,_,_,_) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -196,8 +196,8 @@ and merge_with env mtb with_decl alias= 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) -> - With_module_body (idl,mp,cst), + | With_module_body (idc,mp,t,cst) -> + With_module_body (idl,mp,t,cst), Some(map_mp (mp_rec idc) mp) in let subst = Option.fold_right join subst1 alias in @@ -227,7 +227,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 @@ -257,7 +257,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,_,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 @@ -323,7 +323,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/checker/subtyping.ml b/checker/subtyping.ml index fb95b606a8..edf119c664 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -32,7 +32,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 *) @@ -63,7 +63,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 @@ -308,23 +308,23 @@ and check_signatures env (msid1,sig1) alias (msid2,sig2') = begin match info1 with | Module msb -> check_modules env msid1 l msb msb2 - | 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 env msid1 l msb msb2 | _ -> error_not_match l spec2 end - | SFBalias (mp,_) -> + | SFBalias (mp,typ_opt,_) -> begin match info1 with - | Alias mp1 -> check_modpath_equiv env mp mp1 + | Alias (mp1,_) -> check_modpath_equiv env mp mp1 | 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/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index e52571aadb..edfdfb13ea 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -165,10 +165,10 @@ let rec extract_sfb_spec env mp = function | (l,SFBmodtype mtb) :: msig -> let specs = extract_sfb_spec env mp msig in (l,Smodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: specs - | (l,SFBalias(mp1,_))::msig -> + | (l,SFBalias(mp1,typ_opt,_))::msig -> extract_sfb_spec env mp ((l,SFBmodule {mod_expr = Some (SEBident mp1); - mod_type = None; + mod_type = typ_opt; mod_constraints = Univ.Constraint.empty; mod_alias = Mod_subst.empty_subst; mod_retroknowledge = []})::msig) @@ -183,7 +183,7 @@ and extract_seb_spec env truetype = function (match extract_with_type env cb with (* cb peut contenir des kn *) | None -> mtb'' | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ))) - | SEBwith(mtb',With_module_body(idl,mp,_))-> + | SEBwith(mtb',With_module_body(idl,mp,_,_))-> Visit.add_mp mp; MTwith(extract_seb_spec env truetype mtb', ML_With_module(idl,mp)) @@ -250,13 +250,13 @@ let rec extract_sfb env mp all = function if all || Visit.needed_mp mp then (l,SEmodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: ms else ms - | (l,SFBalias (mp1,cst)) :: msb -> + | (l,SFBalias (mp1,typ_opt,cst)) :: msb -> let ms = extract_sfb env mp all msb in let mp = MPdot (mp,l) in if all || Visit.needed_mp mp then (l,SEmodule (extract_module env mp true {mod_expr = Some (SEBident mp1); - mod_type = None; + mod_type = typ_opt; mod_constraints= Univ.Constraint.empty; mod_alias = empty_subst; mod_retroknowledge = []})) :: ms diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 475ef042d1..725859321c 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -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 e98cb379c2..fb8317cdcb 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -182,7 +182,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 @@ -196,7 +197,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/mod_typing.ml b/kernel/mod_typing.ml index 907b8a8fe9..941d219ba7 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -37,14 +37,41 @@ 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 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 +167,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 @@ -165,9 +192,9 @@ and check_with_aux_mod env mtb with_decl now = 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) + 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 @@ -180,7 +207,7 @@ and check_with_aux_mod env mtb with_decl now = With_Definition (_,c) -> With_Definition (idl,c) | With_Module (_,c) -> With_Module (idl,c) in - let cst,_ = + let cst,_,typ_opt = check_with_aux_mod env' (type_of_mb env old) new_with_decl false in if now then @@ -188,9 +215,11 @@ and check_with_aux_mod env mtb with_decl now = 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) + cst, + (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst), + typ_opt else - cst,empty_subst + cst,empty_subst,typ_opt | Some msb -> error_a_generative_module_expected l end @@ -214,7 +243,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 +335,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 +343,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 +383,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 d903d4b328..750d393cb3 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -21,6 +21,7 @@ open Mod_subst (*i*) + let error_existing_label l = error ("The label "^string_of_label l^" is already declared.") @@ -132,13 +133,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 +158,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 +280,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 +306,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 @@ -316,16 +319,16 @@ and merge_with env mtb with_decl alias= 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) -> + | 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 (_::_,_,_) -> + | With_module_body (_::_,_,_,_) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) @@ -333,9 +336,9 @@ and merge_with env mtb with_decl alias= 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) -> + | With_module_body (idc,mp,typ_opt,cst) -> let mp' = scrape_alias mp env in - With_module_body (idl,mp,cst), + With_module_body (idl,mp,typ_opt,cst), Some(map_mp (mp_rec (List.rev idc)) mp') in let subst = match subst1 with @@ -371,7 +374,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 +405,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 +497,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 0191880d16..e75900cfa1 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -117,6 +117,11 @@ 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 -> "MPfile (" ^ string_of_dirpath sl ^ ")" | MPbound uid -> string_of_uid uid diff --git a/kernel/names.mli b/kernel/names.mli index 177768cf43..d0efe2380e 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -84,6 +84,8 @@ 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 module MPset : Set.S with type elt = module_path diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index eef2d675ce..09b2f918f0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -27,6 +27,7 @@ open Subtyping open Mod_typing open Mod_subst + type modvariant = | NONE | SIG of (* funsig params *) (mod_bound_id * module_type_body) list @@ -312,6 +313,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 +335,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 +510,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 +526,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; @@ -817,4 +825,3 @@ let j_type j = j.uj_type let safe_infer senv = infer (env_of_senv senv) let typing senv = Typeops.typing (env_of_senv senv) - diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 918a2f51ba..387d97de97 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -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/library/declaremods.ml b/library/declaremods.ml index ac5636b58e..72f199efb5 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -434,10 +434,12 @@ and subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) = mod_entry_expr = Some (MSEident mp')},sub), substobjs, match mbids with - | [] -> + | [] -> let subst = update_subst subst' (map_mp mp' mp) in Some (subst_objects (dir,(mp',empty_dirpath)) - (join subst' (join (map_msid msid mp') - (map_mp mp mp'))) objs) + (join (join subst' subst) (join (map_msid msid mp') + (map_mp mp mp'))) + objs) + | _ -> None) | _ -> anomaly "Modops: Not an alias" diff --git a/parsing/printmod.ml b/parsing/printmod.ml index be73f573b5..596ce6b24b 100644 --- a/parsing/printmod.ml +++ b/parsing/printmod.ml @@ -90,7 +90,7 @@ and print_modtype locals mty = let s = (String.concat "." (List.map string_of_id idl)) in hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ str "Definition"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) - | SEBwith(seb,With_module_body(idl,mp,_))-> + | SEBwith(seb,With_module_body(idl,mp,_,_))-> let s =(String.concat "." (List.map string_of_id idl)) in hov 2 (print_modtype locals seb ++ spc() ++ str "with" ++ spc() ++ str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc()) @@ -102,7 +102,7 @@ and print_sig locals msid sign = | SFBconst {const_opaque=true} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " - | SFBalias (mp,_) -> str "Module " + | SFBalias (mp,_,_) -> str "Module " | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_spec sign @@ -114,7 +114,7 @@ and print_struct locals msid struc = | SFBconst {const_body=None} -> str "Parameter " | SFBmind _ -> str "Inductive " | SFBmodule _ -> str "Module " - | SFBalias (mp,_) -> str "Module " + | SFBalias (mp,_,_) -> str "Module " | SFBmodtype _ -> str "Module Type ") ++ str (string_of_label l) in prlist_with_sep spc print_body struc |