diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 398 |
1 files changed, 398 insertions, 0 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml new file mode 100644 index 00000000..ecf8d633 --- /dev/null +++ b/checker/mod_checking.ml @@ -0,0 +1,398 @@ + +open Pp +open Util +open Names +open Term +open Inductive +open Reduction +open Typeops +open Indtypes +open Modops +open Subtyping +open Declarations +open Environ + +(************************************************************************) +(* Checking constants *) + +let refresh_arity ar = + let ctxt, hd = decompose_prod_assum ar in + match hd with + Sort (Type u) when not (Univ.is_univ_variable u) -> + let u' = Univ.fresh_local_univ() in + mkArity (ctxt,Type u'), + Univ.enforce_geq u' u Univ.Constraint.empty + | _ -> ar, Univ.Constraint.empty + +let check_constant_declaration env kn cb = + Flags.if_verbose msgnl (str " checking cst: " ++ prcon kn); + let env = add_constraints cb.const_constraints env in + let env' = check_named_ctxt env cb.const_hyps in + (match cb.const_type with + NonPolymorphicType ty -> + let ty, cu = refresh_arity ty in + let envty = add_constraints cu env' in + let _ = infer_type envty ty in + (match cb.const_body with + | Some bd -> + let j = infer env' (force_constr bd) in + conv_leq envty j ty + | None -> ()) + | PolymorphicArity(ctxt,par) -> + let _ = check_ctxt env ctxt in + check_polymorphic_arity env ctxt par); + add_constant kn cb env + +(************************************************************************) +(* Checking modules *) + + +let rec add_struct_expr_constraints env = function + | SEBident _ -> env + + | SEBfunctor (_,mtb,meb) -> + add_struct_expr_constraints + (add_modtype_constraints env mtb) meb + + | SEBstruct (_,structure_body) -> + List.fold_left + (fun env (l,item) -> add_struct_elem_constraints env item) + env + structure_body + + | 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()); +*) + 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 + | 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 + | SFBmodtype mtb -> add_modtype_constraints env mtb + +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 -> + add_struct_expr_constraints env mtb + in + Environ.add_constraints mb.mod_constraints env + +and add_modtype_constraints env mtb = + add_struct_expr_constraints env mtb.typ_expr + +exception Not_path + +let path_of_mexpr = function + | SEBident mp -> mp + | _ -> raise Not_path + +let rec list_split_assoc k rev_before = function + | [] -> raise Not_found + | (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 + | [] -> (e,[],[]) + | 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 = + + (* If the type of a constant is generated, it may mention + non-variable algebraic universes that the general conversion + algorithm is not ready to handle. Anyway, generated types of + constants are functions of the body of the constant. If the + bodies are the same in environments that are subtypes one of + the other, the types are subtypes too (i.e. if Gamma <= Gamma', + 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 = + if isArity t2 then + let (ctx2,s2) = destArity t2 in + match s2 with + | Type v when not (Univ.is_univ_variable v) -> + (* The type in the interface is inferred and is made of algebraic + universes *) + begin try + let (ctx1,s1) = dest_arity env t1 in + match s1 with + | Type u when not (Univ.is_univ_variable u) -> + (* Both types are inferred, no need to recheck them. We + cheat and collapse the types to Prop *) + mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) + | Prop _ -> + (* The type in the interface is inferred, it may be the case + that the type in the implementation is smaller because + the body is more reduced. We safely collapse the upper + type to Prop *) + mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null) + | Type _ -> + (* The type in the interface is inferred and the type in the + implementation is not inferred or is inferred but from a + more reduced body so that it is just a variable. Since + constraints of the form "univ <= max(...)" are not + expressible in the system of algebraic universes: we fail + (the user has to use an explicit type in the interface *) + raise Reduction.NotConvertible + with UserError _ (* "not an arity" *) -> + raise Reduction.NotConvertible end + | _ -> t1,t2 + else + (t1,t2) in + Reduction.conv_leq env t1 t2 + in + assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; + (*Start by checking types*) + let typ1 = Typeops.type_of_constant_type env cb1.const_type in + let typ2 = Typeops.type_of_constant_type env cb2.const_type in + check_type env typ1 typ2; + (match cb2 with + | {const_body=Some lc2;const_opaque=false} -> + let c2 = force_constr lc2 in + let c1 = match cb1.const_body with + | Some lc1 -> force_constr lc1 + | None -> assert false in + Reduction.conv env c1 c2 + | _ -> ()) + +let rec check_with env mtb with_decl = + 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 + +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 + | _ -> 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 + 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 + match with_decl with + | With_definition_body ([],_) -> assert false + | With_definition_body ([id],c) -> + let cb = match spec with + SFBconst cb -> cb + | _ -> error_not_a_constant l + in + check_definition_sub env' c cb + | With_definition_body (_::_,_) -> + let old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module l + in + begin + match old.mod_expr with + | None -> + 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 + check_with_aux_def env' (type_of_mb env old) new_with_decl + | Some msb -> + error_a_generative_module_expected l + end + | _ -> anomaly "Modtyping:incorrect use of with" + with + 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) + | _ -> 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 + 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 + | i::r -> MPdot(mp_rec r,label_of_id i) + 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,_) -> + let old,alias = match spec with + SFBmodule msb -> Some msb,None + | SFBalias (mp',_) -> None,Some mp' + | _ -> 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 old = match spec with + SFBmodule msb -> msb + | _ -> error_not_a_module l + in + begin + match old.mod_expr with + None -> + 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 + let sub = + check_with_aux_mod env' + (type_of_mb env old) new_with_decl in + join (map_mp (mp_rec idl) mp) sub + | Some msb -> + error_a_generative_module_expected l + end + | _ -> anomaly "Modtyping:incorrect use of with" + with + Not_found -> error_no_such_label l + | 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 env' = add_module_constraints env mb in + 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 + | SFBconst cb -> + let c = make_con mp empty_dirpath lab in + (s,check_constant_declaration env c cb) + | SFBmind mib -> + let kn = make_kn mp empty_dirpath lab in + (s,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 + (add_module_constraints env msb)) + | SFBalias(mp2,cst) -> + (try + let mp2' = scrape_alias mp2 env in + let msb = lookup_module mp2' env in + (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias), + Option.fold_right add_constraints cst + (register_alias (MPdot(mp,lab)) mp2 env)) + with Not_found -> failwith "unkown aliased module") + | SFBmodtype mty -> + let kn = MPdot(mp, lab) in + check_module_type env mty; + (join s mty.typ_alias, + add_modtype kn mty (add_modtype_constraints env mty)) + +and check_modexpr env mse = match mse with + | SEBident mp -> + let mtb = lookup_modtype mp env in + mtb.typ_alias + | 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 + | 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 mp = + try scrape_alias (path_of_mexpr m) env + 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 + | 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 |