diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 427 |
1 files changed, 94 insertions, 333 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index dc3ed452..998e23c6 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -2,8 +2,8 @@ open Pp open Util open Names +open Cic open Term -open Inductive open Reduction open Typeops open Indtypes @@ -12,371 +12,132 @@ open Subtyping open Declarations open Environ -(************************************************************************) -(* Checking constants *) +(** {6 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.empty_constraint + let u' = Univ.Universe.make (Univ.Level.make empty_dirpath 1) in + mkArity (ctxt,Prop Null), + Univ.enforce_leq u u' Univ.empty_constraint | _ -> ar, Univ.empty_constraint 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 + Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); pp_flush (); + let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in + let envty, ty = + match cb.const_type with + RegularArity ty -> + let ty', cu = refresh_arity ty in let envty = add_constraints cu env' in - let _ = infer_type envty ty in - (match body_of_constant cb 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 *) - - -exception Not_path - -let path_of_mexpr = function - | SEBident mp -> mp - | _ -> raise Not_path - -let is_modular = function - | SFBmodule _ | SFBmodtype _ -> true - | SFBconst _ | SFBmind _ -> false - -let rec list_split_assoc ((k,m) as km) rev_before = function - | [] -> raise Not_found - | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after - | h::tail -> list_split_assoc km (h::rev_before) tail - -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 + let _ = infer_type envty ty' in envty, ty + | TemplateArity(ctxt,par) -> + let _ = check_ctxt env' ctxt in + check_polymorphic_arity env' ctxt par; + env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt + in + let () = + match body_of_constant cb with + | Some bd -> + (match cb.const_proj with + | None -> let j = infer envty bd in + conv_leq envty j ty + | Some pb -> + let env' = add_constant kn cb env' in + let j = infer env' bd in + conv_leq envty j ty) + | None -> () 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; - (* In the spirit of subtyping.check_constant, we accept - any implementations of parameters and opaques terms, - as long as they have the right type *) - (match cb2.const_body with - | Undef _ | OpaqueDef _ -> () - | Def lc2 -> - (match cb1.const_body with - | Def lc1 -> - let c1 = force_constr lc1 in - let c2 = force_constr lc2 in - Reduction.conv env c1 c2 - (* Coq only places transparent cb in With_definition_body *) - | _ -> assert false)) + if cb.const_polymorphic then add_constant kn cb env + else add_constant kn cb env' -let lookup_modtype mp env = - try Environ.lookup_modtype mp env - with Not_found -> - failwith ("Unknown module type: "^string_of_mp mp) +(** {6 Checking modules } *) + +(** We currently ignore the [mod_type_alg] and [typ_expr_alg] fields. + The only delicate part is when [mod_expr] is an algebraic expression : + we need to expand it before checking it is indeed a subtype of [mod_type]. + Fortunately, [mod_expr] cannot contain any [MEwith]. *) let lookup_module mp env = try Environ.lookup_module mp env with Not_found -> failwith ("Unknown module: "^string_of_mp mp) -let rec check_with env mtb with_decl mp= - match with_decl with - | With_definition_body (idl,c) -> - check_with_def env mtb (idl,c) mp; - mtb - | With_module_body (idl,mp1) -> - check_with_mod env mtb (idl,mp1) mp; - mtb - -and check_with_def env mtb (idl,c) mp = - let sig_b = match mtb with - | SEBstruct(sig_b) -> - sig_b - | _ -> error_signature_expected mtb - in - let id,idl = match idl with - | [] -> assert false - | id::idl -> id,idl +let mk_mtb mp sign delta = + { mod_mp = mp; + mod_expr = Abstract; + mod_type = sign; + mod_type_alg = None; + mod_constraints = Univ.Constraint.empty; + mod_delta = delta; + mod_retroknowledge = []; } + +let rec check_module env mp mb = + let (_:module_signature) = + check_signature env mb.mod_type mb.mod_mp mb.mod_delta in - let l = label_of_id id in - try - let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in - let before = List.rev rev_before in - let env' = Modops.add_signature mp before empty_delta_resolver env in - if idl = [] then - let cb = match spec with - SFBconst cb -> cb - | _ -> error_not_a_constant l - in - check_definition_sub env' c cb - else - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module l - in - begin - match old.mod_expr with - | None -> - check_with_def env' old.mod_type (idl,c) (MPdot(mp,l)) - | Some msb -> - error_a_generative_module_expected l - end - with - Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_with_incorrect l - -and check_with_mod env mtb (idl,mp1) mp = - let sig_b = - match mtb with - | SEBstruct(sig_b) -> - sig_b - | _ -> error_signature_expected mtb in - let id,idl = match idl with - | [] -> assert false - | id::idl -> id,idl + let optsign = match mb.mod_expr with + |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta) + |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta) + |Abstract|FullStruct -> None in - let l = label_of_id id in - try - let rev_before,spec,after = list_split_assoc (l,false) [] sig_b in - let before = List.rev rev_before in - let env' = Modops.add_signature mp before empty_delta_resolver env in - if idl = [] then - let _ = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module l - in - let (_:module_body) = (Environ.lookup_module mp1 env) in () - else - let old = match spec with - SFBmodule msb -> msb - | _ -> error_not_a_module l - in - begin - match old.mod_expr with - None -> - check_with_mod env' - old.mod_type (idl,mp1) (MPdot(mp,l)) - | Some msb -> - error_a_generative_module_expected l - end - with - Not_found -> error_no_such_label l - | Reduction.NotConvertible -> error_with_incorrect l + match optsign with + |None -> () + |Some sign -> + let mtb1 = mk_mtb mp sign mb.mod_delta + and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in + let env = add_module_type mp mtb1 env in + Subtyping.check_subtypes env mtb1 mtb2 and check_module_type env mty = - let (_:struct_expr_body) = - check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in + let (_:module_signature) = + check_signature env mty.mod_type mty.mod_mp mty.mod_delta in () - -and check_module env mp mb = - match mb.mod_expr, mb.mod_type with - | None,mtb -> - let (_:struct_expr_body) = - check_modtype env mtb mb.mod_mp mb.mod_delta in () - | Some mexpr, mtb when mtb==mexpr -> - let (_:struct_expr_body) = - check_modtype env mtb mb.mod_mp mb.mod_delta in () - | Some mexpr, _ -> - let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in - let (_:struct_expr_body) = - check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in - let mtb1 = - {typ_mp=mp; - typ_expr=sign; - typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; - typ_delta = mb.mod_delta;} - and mtb2 = - {typ_mp=mp; - typ_expr=mb.mod_type; - typ_expr_alg=None; - typ_constraints=Univ.empty_constraint; - typ_delta = mb.mod_delta;} - in - let env = add_module (module_body_of_type mp mtb1) env in - check_subtypes env mtb1 mtb2 - and check_structure_field env mp lab res = function | SFBconst cb -> - let c = make_con mp empty_dirpath lab in - check_constant_declaration env c cb + let c = Constant.make2 mp lab in + check_constant_declaration env c cb | SFBmind mib -> - let kn = make_mind mp empty_dirpath lab in + let kn = MutInd.make2 mp lab in let kn = mind_of_delta res kn in - Indtypes.check_inductive env kn mib + Indtypes.check_inductive env kn mib | SFBmodule msb -> - let (_:unit) = check_module env (MPdot(mp,lab)) msb in - Modops.add_module msb env + let () = check_module env (MPdot(mp,lab)) msb in + Modops.add_module msb env | SFBmodtype mty -> check_module_type env mty; add_modtype (MPdot(mp,lab)) mty env - -and check_modexpr env mse mp_mse res = match mse with - | SEBident mp -> + +and check_mexpr env mse mp_mse res = match mse with + | MEident mp -> let mb = lookup_module mp env in (subst_and_strengthen mb mp_mse).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 + | MEapply (f,mp) -> + let sign = check_mexpr env f mp_mse res in + let farg_id, farg_b, fbody_b = destr_functor sign in let mtb = module_type_of_module (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 (_:env) = 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 mtb = lookup_modtype mp env in - mtb.typ_expr - | 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 body = check_modtype env' body mp_mse res in - SEBfunctor(arg_id,mtb,body) - | SEBapply (f,m,cst) -> - 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 (path_of_mexpr m) - with Not_path -> error_application_to_not_path m - (* place for nondep_supertype *) in - let mtb = module_type_of_module (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_modtype env mte mp_mse res in - let sign = check_with env sign with_decl mp_mse in - sign - | SEBstruct(msb) -> - let (_:env) = 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 - | 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 + check_subtypes env mtb farg_b; + subst_signature (map_mbid farg_id mp) fbody_b + | MEwith _ -> error_with_module () - | 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 check_mexpression env sign mp_mse res = match sign with + | MoreFunctor (arg_id, mtb, body) -> + check_module_type env mtb; + let env' = add_module_type (MPbound arg_id) mtb env in + let body = check_mexpression env' body mp_mse res in + MoreFunctor(arg_id,mtb,body) + | NoFunctor me -> check_mexpr env me mp_mse res -and add_modtype_constraints env mtb = - add_struct_expr_constraints env mtb.typ_expr -*) +and check_signature env sign mp_mse res = match sign with + | MoreFunctor (arg_id, mtb, body) -> + check_module_type env mtb; + let env' = add_module_type (MPbound arg_id) mtb env in + let body = check_signature env' body mp_mse res in + MoreFunctor(arg_id,mtb,body) + | NoFunctor struc -> + let (_:env) = List.fold_left (fun env (lab,mb) -> + check_structure_field env mp_mse lab res mb) env struc + in + NoFunctor struc |