From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- kernel/mod_typing.ml | 303 +++++++++++++++++++++++---------------------------- 1 file changed, 137 insertions(+), 166 deletions(-) (limited to 'kernel/mod_typing.ml') diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index e366bc97..a384c836 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,12 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* mp | _ -> raise Not_path +let rec mp_from_mexpr = function + | MSEident mp -> mp + | MSEapply (expr,_) -> mp_from_mexpr expr + | MSEfunctor (_,_,expr) -> mp_from_mexpr expr + | MSEwith (expr,_) -> mp_from_mexpr expr + 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 discr_resolver env mtb = match mtb.typ_expr with SEBstruct _ -> @@ -81,40 +84,41 @@ and check_with_aux_def env sign with_decl mp equiv = | With_Definition ([],_) -> assert false | With_Definition ([id],c) -> let cb = match spec with - SFBconst cb -> cb + | SFBconst cb -> cb | _ -> error_not_a_constant l in - begin - match cb.const_body with - | None -> - let (j,cst1) = Typeops.infer env' c in - let typ = Typeops.type_of_constant_type env' cb.const_type in - let cst2 = Reduction.conv_leq env' j.uj_type typ in - let cst = - Constraint.union - (Constraint.union cb.const_constraints cst1) - cst2 in - let body = Some (Declarations.from_val j.uj_val) in - let cb' = {cb with - const_body = body; - const_body_code = Cemitcodes.from_val - (compile_constant_body env' body false false); - const_constraints = cst} in - SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst - | Some b -> - let cst1 = Reduction.conv env' c (Declarations.force b) in - let cst = Constraint.union cb.const_constraints cst1 in - let body = Some (Declarations.from_val c) in - let cb' = {cb with - const_body = body; - const_body_code = Cemitcodes.from_val - (compile_constant_body env' body false false); - const_constraints = cst} in - SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst - end + (* In the spirit of subtyping.check_constant, we accept + any implementations of parameters and opaques terms, + as long as they have the right type *) + let def,cst = match cb.const_body with + | Undef _ | OpaqueDef _ -> + let (j,cst1) = Typeops.infer env' c in + let typ = Typeops.type_of_constant_type env' cb.const_type in + let cst2 = Reduction.conv_leq env' j.uj_type typ in + let cst = + union_constraints + (union_constraints cb.const_constraints cst1) + cst2 + in + let def = Def (Declarations.from_val j.uj_val) in + def,cst + | Def cs -> + let cst1 = Reduction.conv env' c (Declarations.force cs) in + let cst = union_constraints cb.const_constraints cst1 in + let def = Def (Declarations.from_val c) in + def,cst + in + let cb' = + { cb with + const_body = def; + const_body_code = + Cemitcodes.from_val (compile_constant_body env' def); + const_constraints = cst } + in + SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst | With_Definition (_::_,c) -> let old = match spec with - SFBmodule msb -> msb + | SFBmodule msb -> msb | _ -> error_not_a_module (string_of_label l) in begin @@ -129,12 +133,12 @@ and check_with_aux_def env sign with_decl mp equiv = mod_type_alg = None}) in SEBstruct(before@((l,new_spec)::after)),cb,cst | Some msb -> - error_a_generative_module_expected l + error_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 + | Not_found -> error_no_such_label l + | Reduction.NotConvertible -> error_incorrect_with_constraint l and check_with_aux_mod env sign with_decl mp equiv = let sig_b = match sign with @@ -163,24 +167,24 @@ and check_with_aux_mod env sign with_decl mp equiv = in let mb_mp1 = (lookup_module mp1 env) in let mtb_mp1 = - module_type_of_module env' None mb_mp1 in + module_type_of_module None mb_mp1 in let cst = match old.mod_expr with None -> begin - try Constraint.union + try union_constraints (check_subtypes env' mtb_mp1 - (module_type_of_module env' None old)) + (module_type_of_module None old)) old.mod_constraints - with Failure _ -> error_with_incorrect (label_of_id id) + with Failure _ -> error_incorrect_with_constraint (label_of_id id) end | Some (SEBident(mp')) -> check_modpath_equiv env' mp1 mp'; old.mod_constraints - | _ -> error_a_generative_module_expected l + | _ -> error_generative_module_expected l + in + let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false in - let new_mb = strengthen_and_subst_mb mb_mp1 - (MPdot(mp,l)) env false in let new_spec = SFBmodule {new_mb with mod_mp = MPdot(mp,l); mod_expr = Some (SEBident mp1); @@ -215,14 +219,14 @@ and check_with_aux_mod env sign with_decl mp equiv = let mpnew = rebuild_mp mp' (List.map label_of_id idl) in check_modpath_equiv env' mpnew mp; SEBstruct(before@(l,spec)::after) - ,equiv,Constraint.empty + ,equiv,empty_constraint | _ -> - error_a_generative_module_expected l + error_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 + | Reduction.NotConvertible -> error_incorrect_with_constraint l and translate_module env mp inl me = match me.mod_entry_expr, me.mod_entry_type with @@ -243,14 +247,14 @@ and translate_module env mp inl me = let sign,alg1,resolver,cst2 = match me.mod_entry_type with | None -> - sign,None,resolver,Constraint.empty + sign,None,resolver,empty_constraint | Some mte -> let mtb = translate_module_type env mp inl mte in let cst = check_subtypes env {typ_mp = mp; typ_expr = sign; typ_expr_alg = None; - typ_constraints = Constraint.empty; + typ_constraints = empty_constraint; typ_delta = resolver;} mtb in @@ -258,9 +262,9 @@ and translate_module env mp inl me = in { mod_mp = mp; mod_type = sign; - mod_expr = Some alg_implem; + mod_expr = alg_implem; mod_type_alg = alg1; - mod_constraints = Univ.Constraint.union cst1 cst2; + mod_constraints = Univ.union_constraints cst1 cst2; mod_delta = resolver; mod_retroknowledge = []} (* spiwack: not so sure about that. It may @@ -268,125 +272,92 @@ and translate_module env mp inl me = If it does, I don't really know how to fix the bug.*) +and translate_apply env inl ftrans mexpr mkalg = + let sign,alg,resolver,cst1 = ftrans in + let farg_id, farg_b, fbody_b = destr_functor env sign in + let mp1 = + try path_of_mexpr mexpr + with Not_path -> error_application_to_not_path mexpr + in + let mtb = module_type_of_module None (lookup_module mp1 env) in + let cst2 = check_subtypes env mtb farg_b in + let mp_delta = discr_resolver env mtb in + let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in + let subst = map_mbid farg_id mp1 mp_delta + in + subst_struct_expr subst fbody_b, + mkalg alg mp1 cst2, + subst_codom_delta_resolver subst resolver, + Univ.union_constraints cst1 cst2 + +and translate_functor env inl arg_id arg_e trans mkalg = + let mtb = translate_module_type env (MPbound arg_id) inl arg_e in + let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in + let sign,alg,resolver,cst = trans env' + in + SEBfunctor (arg_id, mtb, sign), + mkalg alg arg_id mtb, + resolver, + Univ.union_constraints cst mtb.typ_constraints -and translate_struct_module_entry env mp inl mse = match mse with +and translate_struct_module_entry env mp inl = function | MSEident mp1 -> - let mb = lookup_module mp1 env in - let mb' = strengthen_and_subst_mb mb mp env false in - mb'.mod_type, SEBident mp1, mb'.mod_delta,Univ.Constraint.empty + let mb = lookup_module mp1 env in + let mb' = strengthen_and_subst_mb mb mp false in + mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint | MSEfunctor (arg_id, arg_e, body_expr) -> - let mtb = translate_module_type env (MPbound arg_id) inl arg_e in - let env' = add_module (module_body_of_type (MPbound arg_id) mtb) - env in - let sign,alg,resolver,cst = - translate_struct_module_entry env' mp inl body_expr in - SEBfunctor (arg_id, mtb, sign),SEBfunctor (arg_id, mtb, alg),resolver, - Univ.Constraint.union cst mtb.typ_constraints + let trans env' = translate_struct_module_entry env' mp inl body_expr in + let mkalg a id m = Option.map (fun a -> SEBfunctor (id,m,a)) a in + translate_functor env inl arg_id arg_e trans mkalg | MSEapply (fexpr,mexpr) -> - let sign,alg,resolver,cst1 = - translate_struct_module_entry env mp inl fexpr - in - let farg_id, farg_b, fbody_b = destr_functor env sign in - let mtb,mp1 = - try - let mp1 = path_of_mexpr mexpr in - let mtb = module_type_of_module env None (lookup_module mp1 env) in - mtb,mp1 - with - | Not_path -> error_application_to_not_path mexpr - (* place for nondep_supertype *) in - let cst = check_subtypes env mtb farg_b in - let mp_delta = discr_resolver env mtb in - let mp_delta = if not inl then mp_delta else - complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta - in - let subst = map_mbid farg_id mp1 mp_delta in - (subst_struct_expr subst fbody_b),SEBapply(alg,SEBident mp1,cst), - (subst_codom_delta_resolver subst resolver), - Univ.Constraint.union cst1 cst + let trans = translate_struct_module_entry env mp inl fexpr in + let mkalg a mp c = Option.map (fun a -> SEBapply(a,SEBident mp,c)) a in + translate_apply env inl trans mexpr mkalg | MSEwith(mte, with_decl) -> - let sign,alg,resolve,cst1 = translate_struct_module_entry env mp inl mte in - let sign,alg,resolve,cst2 = check_with env sign with_decl (Some alg) mp resolve in - sign,Option.get alg,resolve,Univ.Constraint.union cst1 cst2 - -and translate_struct_type_entry env inl mse = match mse with + let sign,alg,resolve,cst1 = + translate_struct_module_entry env mp inl mte in + let sign,alg,resolve,cst2 = + check_with env sign with_decl alg mp resolve in + sign,alg,resolve,Univ.union_constraints cst1 cst2 + +and translate_struct_type_entry env inl = function | MSEident mp1 -> - let mtb = lookup_modtype mp1 env in - mtb.typ_expr, - Some (SEBident mp1),mtb.typ_delta,mp1,Univ.Constraint.empty + let mtb = lookup_modtype mp1 env in + mtb.typ_expr,Some (SEBident mp1),mtb.typ_delta,Univ.empty_constraint | MSEfunctor (arg_id, arg_e, body_expr) -> - let mtb = translate_module_type env (MPbound arg_id) inl arg_e in - let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in - let sign,alg,resolve,mp_from,cst = - translate_struct_type_entry env' inl body_expr in - SEBfunctor (arg_id, mtb, sign),None,resolve,mp_from, - Univ.Constraint.union cst mtb.typ_constraints + let trans env' = translate_struct_type_entry env' inl body_expr in + translate_functor env inl arg_id arg_e trans (fun _ _ _ -> None) | MSEapply (fexpr,mexpr) -> - let sign,alg,resolve,mp_from,cst1 = - translate_struct_type_entry env inl fexpr - in - let farg_id, farg_b, fbody_b = destr_functor env sign in - let mtb,mp1 = - try - let mp1 = path_of_mexpr mexpr in - let mtb = module_type_of_module env None (lookup_module mp1 env) in - mtb,mp1 - with - | Not_path -> error_application_to_not_path mexpr - (* place for nondep_supertype *) in - let cst2 = check_subtypes env mtb farg_b in - let mp_delta = discr_resolver env mtb in - let mp_delta = if not inl then mp_delta else - complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta - in - let subst = map_mbid farg_id mp1 mp_delta in - (subst_struct_expr subst fbody_b),None, - (subst_codom_delta_resolver subst resolve),mp_from,Univ.Constraint.union cst1 cst2 + let trans = translate_struct_type_entry env inl fexpr in + translate_apply env inl trans mexpr (fun _ _ _ -> None) | MSEwith(mte, with_decl) -> - let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in - let sign,alg,resolve,cst1 = - check_with env sign with_decl alg mp_from resolve in - sign,alg,resolve,mp_from,Univ.Constraint.union cst cst1 + let sign,alg,resolve,cst1 = translate_struct_type_entry env inl mte in + let sign,alg,resolve,cst2 = + check_with env sign with_decl alg (mp_from_mexpr mte) resolve + in + sign,alg,resolve,Univ.union_constraints cst1 cst2 and translate_module_type env mp inl mte = - let sign,alg,resolve,mp_from,cst = translate_struct_type_entry env inl mte in - let mtb = subst_modtype_and_resolver - {typ_mp = mp_from; - typ_expr = sign; - typ_expr_alg = None; - typ_constraints = cst; - typ_delta = resolve} mp env - in {mtb with typ_expr_alg = alg} + let mp_from = mp_from_mexpr mte in + let sign,alg,resolve,cst = translate_struct_type_entry env inl mte in + let mtb = subst_modtype_and_resolver + {typ_mp = mp_from; + typ_expr = sign; + typ_expr_alg = None; + typ_constraints = cst; + typ_delta = resolve} mp + in {mtb with typ_expr_alg = alg} -let rec translate_struct_include_module_entry env mp inl mse = match mse with +let rec translate_struct_include_module_entry env mp inl = function | MSEident mp1 -> - let mb = lookup_module mp1 env in - let mb' = strengthen_and_subst_mb mb mp env true in - let mb_typ = clean_bounded_mod_expr mb'.mod_type in - mb_typ, mb'.mod_delta,Univ.Constraint.empty + let mb = lookup_module mp1 env in + let mb' = strengthen_and_subst_mb mb mp true in + let mb_typ = clean_bounded_mod_expr mb'.mod_type in + mb_typ,None,mb'.mod_delta,Univ.empty_constraint | MSEapply (fexpr,mexpr) -> - let sign,resolver,cst1 = - translate_struct_include_module_entry env mp inl fexpr in - let farg_id, farg_b, fbody_b = destr_functor env sign in - let mtb,mp1 = - try - let mp1 = path_of_mexpr mexpr in - let mtb = module_type_of_module env None (lookup_module mp1 env) in - mtb,mp1 - with - | Not_path -> error_application_to_not_path mexpr - (* place for nondep_supertype *) in - let cst = check_subtypes env mtb farg_b in - let mp_delta = discr_resolver env mtb in - let mp_delta = if not inl then mp_delta else - complete_inline_delta_resolver env mp1 farg_id farg_b mp_delta - in - let subst = map_mbid farg_id mp1 mp_delta in - (subst_struct_expr subst fbody_b), - (subst_codom_delta_resolver subst resolver), - Univ.Constraint.union cst1 cst + let ftrans = translate_struct_include_module_entry env mp inl fexpr in + translate_apply env inl ftrans mexpr (fun _ _ _ -> None) | _ -> error ("You cannot Include a high-order structure.") - let rec add_struct_expr_constraints env = function | SEBident _ -> env @@ -448,11 +419,11 @@ let rec struct_expr_constraints cst = function | SEBapply (meb1,meb2,cst1) -> struct_expr_constraints - (struct_expr_constraints (Univ.Constraint.union cst1 cst) meb1) + (struct_expr_constraints (Univ.union_constraints cst1 cst) meb1) meb2 | SEBwith(meb,With_definition_body(_,cb))-> struct_expr_constraints - (Univ.Constraint.union cb.const_constraints cst) meb + (Univ.union_constraints cb.const_constraints cst) meb | SEBwith(meb,With_module_body(_,_))-> struct_expr_constraints cst meb @@ -468,11 +439,11 @@ and module_constraints cst mb = | Some meb -> struct_expr_constraints cst meb in let cst = struct_expr_constraints cst mb.mod_type in - Univ.Constraint.union mb.mod_constraints cst + Univ.union_constraints mb.mod_constraints cst and modtype_constraints cst mtb = - struct_expr_constraints (Univ.Constraint.union mtb.typ_constraints cst) mtb.typ_expr + struct_expr_constraints (Univ.union_constraints mtb.typ_constraints cst) mtb.typ_expr -let struct_expr_constraints = struct_expr_constraints Univ.Constraint.empty -let module_constraints = module_constraints Univ.Constraint.empty +let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint +let module_constraints = module_constraints Univ.empty_constraint -- cgit v1.2.3