diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 254 |
1 files changed, 116 insertions, 138 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 99babe632..e95109fc5 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -65,10 +65,6 @@ 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 check_alias (s1:substitution) s2 = - if s1 <> s2 then failwith "Incorrect alias" - let check_definition_sub env cb1 cb2 = let check_type env t1 t2 = @@ -135,31 +131,31 @@ let lookup_modtype mp env = with Not_found -> failwith ("Unknown module type: "^string_of_mp mp) - -let rec check_with env mtb with_decl = +let rec check_with env mtb with_decl mp= match with_decl with | With_definition_body _ -> - check_with_aux_def env mtb with_decl; - empty_subst + check_with_aux_def env mtb with_decl mp; + mtb | With_module_body _ -> - check_with_aux_mod env mtb with_decl + check_with_aux_mod env mtb with_decl mp; + mtb -and check_with_aux_def env mtb with_decl = - let msid,sig_b = match (eval_struct env mtb) with - | SEBstruct(msid,sig_b) -> - msid,sig_b +and check_with_aux_def env mtb with_decl mp = + let sig_b = match mtb with + | SEBstruct(sig_b) -> + 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 let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in - let env' = Modops.add_signature (MPself msid) before env in + let env' = Modops.add_signature mp before empty_delta_resolver env in match with_decl with | With_definition_body ([],_) -> assert false | With_definition_body ([id],c) -> @@ -179,9 +175,9 @@ 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,t,cst) -> - With_module_body (idl,c,t,cst) in - check_with_aux_def env' (type_of_mb env old) new_with_decl + | With_module_body (_,c) -> + With_module_body (idl,c) in + check_with_aux_def env' old.mod_type new_with_decl (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end @@ -190,46 +186,35 @@ and check_with_aux_def env mtb with_decl = Not_found -> error_no_such_label l | Reduction.NotConvertible -> error_with_incorrect l -and check_with_aux_mod env mtb with_decl = - let initmsid,msid,sig_b = - match eval_struct env mtb with - | SEBstruct(msid,sig_b) -> - let msid'=(refresh_msid msid) in - msid,msid',(subst_signature_msid msid (MPself(msid')) sig_b) +and check_with_aux_mod env mtb with_decl mp = + let sig_b = + match mtb with + | SEBstruct(sig_b) -> + 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 let rev_before,spec,after = list_split_assoc l [] sig_b in let before = List.rev rev_before in let rec mp_rec = function - | [] -> MPself initmsid + | [] -> mp | i::r -> MPdot(mp_rec r,label_of_id i) in - let env' = Modops.add_signature (MPself msid) before env in + let env' = Modops.add_signature mp before empty_delta_resolver env in match with_decl with - | 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' + | With_module_body ([],_) -> assert false + | With_module_body ([id], mp1) -> + let _ = match spec with + SFBmodule msb -> msb | _ -> error_not_a_module l in - let mtb' = lookup_modtype mp env' in - let _ = - match old,alias with - Some msb,None -> () - | None,Some mp' -> - check_modpath_equiv env' mp mp' - | _,_ -> - anomaly "Mod_typing:no implementation and no alias" - in - join (map_mp (mp_rec [id]) mp) mtb'.typ_alias - | With_module_body (_::_,mp,_,_) -> + let _ = (lookup_module mp1 env) in () + | With_module_body (_::_,mp) -> let old = match spec with SFBmodule msb -> msb | _ -> error_not_a_module l @@ -240,12 +225,10 @@ 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,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 - join (map_mp (mp_rec idl) mp) sub + | With_module_body (_,c) -> + With_module_body (idl,c) in + check_with_aux_mod env' + old.mod_type new_with_decl (MPdot(mp,l)) | Some msb -> error_a_generative_module_expected l end @@ -255,110 +238,105 @@ and check_with_aux_mod env mtb with_decl = | Reduction.NotConvertible -> error_with_incorrect l and check_module_type env mty = - if mty.typ_strength <> None then - failwith "strengthening of module types not supported"; - let sub = check_modexpr env mty.typ_expr in - check_alias mty.typ_alias sub - -and check_module env mb = - let sub = - match mb.mod_expr, mb.mod_type with - | None, None -> - anomaly "Mod_typing.translate_module: empty type and expr in module entry" - | None, Some mtb -> check_modexpr env mtb - - | Some mexpr, _ -> - let sub1 = check_modexpr env mexpr in - (match mb.mod_type with - | None -> sub1 - | Some mte -> - let sub2 = check_modexpr env mte in - check_subtypes env - {typ_expr = mexpr; - typ_strength = None; - typ_alias = sub1;} - {typ_expr = mte; - typ_strength = None; - typ_alias = sub2;}; - sub2) in - check_alias mb.mod_alias sub - -and check_structure_field (s,env) mp lab = function + let _ = check_modtype env mty.typ_expr mty.typ_mp in () + + +and check_module env mp mb = + match mb.mod_expr, mb.mod_type with + | None,mtb -> + let _ = check_modtype env mtb mb.mod_mp in () + | Some mexpr, _ -> + let sign = check_modexpr env mexpr mb.mod_mp in + let _ = check_modtype env mb.mod_type mb.mod_mp in + check_subtypes env + {typ_mp=mp; + typ_expr=sign; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = empty_delta_resolver;} + {typ_mp=mp; + typ_expr=mb.mod_type; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = empty_delta_resolver;}; + +and check_structure_field env mp lab = function | SFBconst cb -> let c = make_con mp empty_dirpath lab in - (s,check_constant_declaration env c cb) + check_constant_declaration env c cb | SFBmind mib -> - let kn = make_kn mp empty_dirpath lab in - (s,Indtypes.check_inductive env kn mib) + let kn = make_mind mp empty_dirpath lab in + Indtypes.check_inductive env kn mib | SFBmodule msb -> - check_module env msb; - let mp1 = MPdot(mp,lab) in - 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) -> - (* cf Safe_typing.add_alias *) - (try - let mp' = MPdot(mp,lab) in - let mp2' = scrape_alias mp2 env in - let _,sub = Modops.update_subst env (lookup_module mp2' env) mp2' in - let sub = update_subst sub (map_mp mp' mp2') in - let sub = join_alias sub (map_mp mp' mp2') in - let sub = add_mp mp' mp2' sub in - (join s sub, register_alias mp' mp2 env) - with Not_found -> failwith "unkown aliased module") + let _= check_module env (MPdot(mp,lab)) msb in + Modops.add_module msb env | SFBmodtype mty -> - let kn = MPdot(mp, lab) in check_module_type env mty; - (join s mty.typ_alias, add_modtype kn mty env) - -and check_modexpr env mse = match mse with + add_modtype (MPdot(mp,lab)) mty env + +and check_modexpr env mse mp_mse = match mse with + | SEBident mp -> + let mb = lookup_module mp env in + (subst_and_strengthen mb mp_mse env).mod_type + | SEBfunctor (arg_id, mtb, body) -> + check_module_type env mtb ; + let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in + let sign = check_modexpr env' body mp_mse in + SEBfunctor (arg_id, mtb, sign) + | SEBapply (f,m,cst) -> + let sign = check_modexpr env f mp_mse in + let farg_id, farg_b, fbody_b = destr_functor env sign in + let mp = + try (path_of_mexpr m) + with Not_path -> error_application_to_not_path m + (* place for nondep_supertype *) in + let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in + check_subtypes env mtb farg_b; + (subst_struct_expr (map_mbid farg_id mp) fbody_b) + | SEBwith(mte, with_decl) -> + let sign = check_modexpr env mte mp_mse in + let sign = check_with env sign with_decl mp_mse in + sign + | SEBstruct(msb) -> + let _ = List.fold_left (fun env (lab,mb) -> + check_structure_field env mp_mse lab mb) env msb in + SEBstruct(msb) + +and check_modtype env mse mp_mse= match mse with | SEBident mp -> - let mp = scrape_alias mp env in let mtb = lookup_modtype mp env in - mtb.typ_alias + mtb.typ_expr | SEBfunctor (arg_id, mtb, body) -> check_module_type env mtb; - let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in - let sub = check_modexpr env' body in - sub + let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in + let body = check_modtype env' body mp_mse in + SEBfunctor(arg_id,mtb,body) | SEBapply (f,m,cst) -> - let sub1 = check_modexpr env f in - let f'= eval_struct env f in - let farg_id, farg_b, fbody_b = destr_functor env f' in + let sign = check_modtype env f mp_mse in + let farg_id, farg_b, fbody_b = destr_functor env sign in let mp = - try scrape_alias (path_of_mexpr m) env + try (path_of_mexpr m) with Not_path -> error_application_to_not_path m - (* place for nondep_supertype *) in - let mtb = lookup_modtype mp env in - check_subtypes env mtb farg_b; - let sub2 = match eval_struct env m with - | SEBstruct (msid,sign) -> - join_alias - (subst_key (map_msid msid mp) mtb.typ_alias) - (map_msid msid mp) - | _ -> mtb.typ_alias in - let sub3 = join_alias sub1 (map_mbid farg_id mp) in - let sub4 = update_subst sub2 sub3 in - join sub3 sub4 + (* place for nondep_supertype *) in + let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in + check_subtypes env mtb farg_b; + subst_struct_expr (map_mbid farg_id mp) fbody_b | SEBwith(mte, with_decl) -> - let sub1 = check_modexpr env mte in - let sub2 = check_with env mte with_decl in - join sub1 sub2 - | SEBstruct(msid,msb) -> - let mp = MPself msid in - let (sub,_) = - List.fold_left (fun env (lab,mb) -> - check_structure_field env mp lab mb) (empty_subst,env) msb in - sub - + let sign = check_modtype env mte mp_mse in + let sign = check_with env sign with_decl mp_mse in + sign + | SEBstruct(msb) -> + let _ = List.fold_left (fun env (lab,mb) -> + check_structure_field env mp_mse lab mb) env msb in + SEBstruct(msb) + (* -let rec add_struct_expr_constraints env = function + let rec add_struct_expr_constraints env = function | SEBident _ -> env - + | SEBfunctor (_,mtb,meb) -> - add_struct_expr_constraints - (add_modtype_constraints env mtb) meb + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb | SEBstruct (_,structure_body) -> List.fold_left |