diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 305 |
1 files changed, 143 insertions, 162 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 24000591..23ba4893 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -31,7 +31,7 @@ let check_constant_declaration env kn cb = (match cb.const_type with NonPolymorphicType ty -> let ty, cu = refresh_arity ty in - let envty = add_constraints cu env' in + let envty = add_constraints cu env' in let _ = infer_type envty ty in (match cb.const_body with | Some bd -> @@ -58,19 +58,15 @@ let rec list_split_assoc k rev_before = function | (k',b)::after when k=k' -> rev_before,b,after | h::tail -> list_split_assoc k (h::rev_before) tail -let rec list_fold_map2 f e = function +let rec list_fold_map2 f e = function | [] -> (e,[],[]) - | h::t -> + | h::t -> let e',h1',h2' = f e h in 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 = + let check_type env t1 t2 = (* If the type of a constant is generated, it may mention non-variable algebraic universes that the general conversion @@ -81,7 +77,7 @@ let check_definition_sub env cb1 cb2 = Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T'). Hence they don't have to be checked again *) - let t1,t2 = + let t1,t2 = if isArity t2 then let (ctx2,s2) = destArity t2 in match s2 with @@ -135,38 +131,38 @@ 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 - | With_module_body _ -> - check_with_aux_mod env mtb with_decl + | With_definition_body _ -> + check_with_aux_def env mtb with_decl mp; + mtb + | With_module_body _ -> + 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,_,_,_) -> + 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 ([],_) | 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) -> + | With_definition_body ([id],c) -> let cb = match spec with SFBconst cb -> cb | _ -> error_not_a_constant l - in + in check_definition_sub env' c cb | With_definition_body (_::_,_) -> let old = match spec with @@ -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,_,_,_) -> + 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 ([],_) | 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 + 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 @@ -238,14 +223,12 @@ and check_with_aux_mod env mtb with_decl = match old.mod_expr with None -> let new_with_decl = match with_decl with - With_definition_body (_,c) -> + 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,113 +238,111 @@ 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 + let _ = check_modtype env mty.typ_expr mty.typ_mp in () -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 + +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, mtb when mtb==mexpr -> + let _ = check_modtype env mtb mb.mod_mp in () + | Some mexpr, _ -> + let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in + let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in + check_subtypes env + {typ_mp=mp; + typ_expr=sign; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = mb.mod_delta;} + {typ_mp=mp; + typ_expr=mb.mod_type; + typ_expr_alg=None; + typ_constraints=Univ.Constraint.empty; + typ_delta = mb.mod_delta;}; + +and check_structure_field env mp lab res = 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 + let kn = mind_of_delta res kn 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 "unknown 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 res = 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 res in + SEBfunctor (arg_id, mtb, sign) + | SEBapply (f,m,cst) -> + let sign = check_modexpr env f mp_mse res 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 res 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 res mb) env msb in + SEBstruct(msb) + +and check_modtype env mse mp_mse res = 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 res 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 res 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 res 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 res 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 + + | SEBfunctor (_,mtb,meb) -> + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb | SEBstruct (_,structure_body) -> - List.fold_left + List.fold_left (fun env (l,item) -> add_struct_elem_constraints env item) env structure_body @@ -369,20 +350,20 @@ let rec add_struct_expr_constraints env = function | SEBapply (meb1,meb2,cst) -> (* let g = Univ.merge_constraints cst Univ.initial_universes in msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++ - Univ.pr_universes g++str"============="++fnl()); + Univ.pr_universes g++str"============="++fnl()); *) - Environ.add_constraints cst - (add_struct_expr_constraints - (add_struct_expr_constraints env meb1) + Environ.add_constraints cst + (add_struct_expr_constraints + (add_struct_expr_constraints env meb1) meb2) | SEBwith(meb,With_definition_body(_,cb))-> Environ.add_constraints cb.const_constraints (add_struct_expr_constraints env meb) | SEBwith(meb,With_module_body(_,_,cst))-> Environ.add_constraints cst - (add_struct_expr_constraints env meb) - -and add_struct_elem_constraints env = function + (add_struct_expr_constraints env meb) + +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 @@ -390,18 +371,18 @@ and add_struct_elem_constraints env = function | SFBalias (mp,None) -> env | SFBmodtype mtb -> add_modtype_constraints env mtb -and add_module_constraints env mb = +and add_module_constraints env mb = let env = match mb.mod_expr with | None -> env | Some meb -> add_struct_expr_constraints env meb in let env = match mb.mod_type with | None -> env - | Some mtb -> + | Some mtb -> add_struct_expr_constraints env mtb in Environ.add_constraints mb.mod_constraints env -and add_modtype_constraints env mtb = +and add_modtype_constraints env mtb = add_struct_expr_constraints env mtb.typ_expr *) |