diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 192 |
1 files changed, 89 insertions, 103 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 861dc9a3fd..41f4c640ce 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -33,7 +33,6 @@ type namedobject = | IndConstr of constructor * mutual_inductive_body | Module of module_body | Modtype of module_type_body - | Alias of module_path * struct_expr_body option (* adds above information about one mutual inductive: all types and constructors *) @@ -61,10 +60,9 @@ let make_label_map mp list = match e with | SFBconst cb -> add_map (Constant cb) | SFBmind mib -> - add_nameobjects_of_mib (make_kn mp empty_dirpath l) mib map + add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map | SFBmodule mb -> add_map (Module mb) | SFBmodtype mtb -> add_map (Modtype mtb) - | SFBalias (mp,typ_opt,cst) -> add_map (Alias (mp,typ_opt)) in List.fold_right add_one list Labmap.empty @@ -75,15 +73,18 @@ let check_conv_error error cst f env a1 a2 = NotConvertible -> error () (* for now we do not allow reorderings *) -let check_inductive cst env msid1 l info1 mib2 spec2 = - let kn = make_kn (MPself msid1) empty_dirpath l in + +let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= + let kn1 = make_mind mp1 empty_dirpath l in + let kn2 = make_mind mp2 empty_dirpath l in let error () = error_not_match l spec2 in let check_conv cst f = check_conv_error error cst f in let mib1 = match info1 with - | IndType ((_,0), mib) -> mib + | IndType ((_,0), mib) -> subst_mind subst1 mib | _ -> error () in + let mib2 = subst_mind subst2 mib2 in let check_inductive_type cst env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of @@ -141,8 +142,8 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = array_fold_left2 (fun cst t1 t2 -> check_conv cst conv env t1 t2) cst - (arities_of_specif kn (mib1,p1)) - (arities_of_specif kn (mib2,p2)) + (arities_of_specif kn1 (mib1,p1)) + (arities_of_specif kn1 (mib2,p2)) in let check f = if f mib1 <> f mib2 then error () in check (fun mib -> mib.mind_finite); @@ -158,16 +159,12 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = (* the inductive types and constructors types have to be convertible *) check (fun mib -> mib.mind_nparams); - begin - match mib2.mind_equiv with - | None -> () - | Some kn2' -> - let kn2 = scrape_mind env kn2' in - let kn1 = match mib1.mind_equiv with - None -> kn - | Some kn1' -> scrape_mind env kn1' - in - if kn1 <> kn2 then error () + begin + match mind_of_delta reso2 kn2 with + | kn2' when kn2=kn2' -> () + | kn2' -> + if not (eq_mind (mind_of_delta reso1 kn1) kn2') then + error () end; (* we check that records and their field names are preserved. *) check (fun mib -> mib.mind_record); @@ -194,7 +191,8 @@ let check_inductive cst env msid1 l info1 mib2 spec2 = in cst -let check_constant cst env msid1 l info1 cb2 spec2 = + +let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = @@ -245,13 +243,15 @@ let check_constant cst env msid1 l info1 cb2 spec2 = in match info1 with - | Constant cb1 -> - assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; - (*Start by checking types*) + | Constant cb1 -> + assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; + (*Start by checking types*) + let cb1 = subst_const_body subst1 cb1 in + let cb2 = subst_const_body subst2 cb2 in let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in let cst = check_type cst env typ1 typ2 in - let con = make_con (MPself msid1) empty_dirpath l in + let con = make_con mp1 empty_dirpath l in let cst = if cb2.const_opaque then match cb2.const_body with @@ -264,7 +264,8 @@ let check_constant cst env msid1 l info1 cb2 spec2 = begin match (kind_of_term c) with Const n -> - let cb = lookup_constant n env in + let cb = subst_const_body subst1 + (lookup_constant n env) in (match cb.const_opaque, cb.const_body with | true, Some lc1 -> @@ -311,28 +312,13 @@ let check_constant cst env msid1 l info1 cb2 spec2 = check_conv cst conv env ty1 ty2 | _ -> error () -let rec check_modules cst env msid1 l msb1 msb2 alias = - let mp = (MPdot(MPself msid1,l)) in - let mty1 = module_type_of_module (Some mp) msb1 in - let alias1,struct_expr = match eval_struct env mty1.typ_expr with - | SEBstruct (msid,sign) as str -> - update_subst alias (map_msid msid mp),str - | _ as str -> empty_subst,str in - let mty1 = {mty1 with - typ_expr = struct_expr; - typ_alias = join alias1 mty1.typ_alias } in - let mty2 = module_type_of_module None msb2 in - let cst = check_modtypes cst env mty1 mty2 false in +let rec check_modules cst env msb1 msb2 subst1 subst2 = + let mty1 = module_type_of_module env None msb1 in + let mty2 = module_type_of_module env None msb2 in + let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in cst - -and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = - let mp1 = MPself msid1 in - let env = add_signature mp1 sig1 env in - let sig1 = subst_structure alias sig1 in - let alias1 = update_subst alias (map_msid msid2 mp1) in - let sig2 = subst_structure alias1 sig2' in - let sig2 = subst_signature_msid msid2 mp1 sig2 in +and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= let map1 = make_label_map mp1 sig1 in let check_one_body cst (l,spec2) = let info1 = @@ -340,38 +326,19 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = Labmap.find l map1 with Not_found -> error_no_such_label_sub l - (string_of_msid msid1) (string_of_msid msid2) + (string_of_mp mp1) in match spec2 with | SFBconst cb2 -> - check_constant cst env msid1 l info1 cb2 spec2 + check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 | SFBmind mib2 -> - check_inductive cst env msid1 l info1 mib2 spec2 + check_inductive cst env + mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 | SFBmodule msb2 -> begin match info1 with - | Module msb -> check_modules cst env msid1 l msb msb2 alias - | Alias (mp,typ_opt) ->let msb = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules cst env msid1 l msb msb2 alias - | _ -> error_not_match l spec2 - end - | SFBalias (mp,typ_opt,_) -> - begin - match info1 with - | Alias (mp1,_) -> check_modpath_equiv env mp mp1; cst - | Module msb -> - let msb1 = - {mod_expr = Some (SEBident mp); - mod_type = typ_opt; - mod_constraints = Constraint.empty; - mod_alias = (lookup_modtype mp env).typ_alias; - mod_retroknowledge = []} in - check_modules cst env msid1 l msb msb1 alias + | Module msb -> check_modules cst env msb msb2 + subst1 subst2 | _ -> error_not_match l spec2 end | SFBmodtype mtb2 -> @@ -380,50 +347,69 @@ and check_signatures cst env (msid1,sig1) alias (msid2,sig2') = | Modtype mtb -> mtb | _ -> error_not_match l spec2 in - check_modtypes cst env mtb1 mtb2 true + let env = add_module (module_body_of_type mtb2.typ_mp mtb2) + (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in + check_modtypes cst env mtb1 mtb2 subst1 subst2 true in List.fold_left check_one_body cst sig2 - -and check_modtypes cst env mtb1 mtb2 equiv = - if mtb1==mtb2 then cst else (* just in case :) *) - let mtb1',mtb2'= - (match mtb1.typ_strength with - None -> eval_struct env mtb1.typ_expr, - eval_struct env mtb2.typ_expr - | Some mp -> strengthen env mtb1.typ_expr mp, - eval_struct env mtb2.typ_expr) in - let rec check_structure cst env str1 str2 equiv = - match str1, str2 with - | SEBstruct (msid1,list1), - SEBstruct (msid2,list2) -> - let cst = check_signatures cst env - (msid1,list1) mtb1.typ_alias (msid2,list2) in - if equiv then - check_signatures cst env - (msid2,list2) mtb2.typ_alias (msid1,list1) - else - cst +and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 then cst else + let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in + let rec check_structure cst env str1 str2 equiv subst1 subst2 = + match str1,str2 with + | SEBstruct (list1), + SEBstruct (list2) -> + if equiv then + let subst2 = + add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in + Univ.Constraint.union + (check_signatures cst env + mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 + mtb1.typ_delta mtb2.typ_delta) + (check_signatures cst env + mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1 + mtb2.typ_delta mtb1.typ_delta) + else + check_signatures cst env + mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2 + mtb1.typ_delta mtb2.typ_delta | SEBfunctor (arg_id1,arg_t1,body_t1), SEBfunctor (arg_id2,arg_t2,body_t2) -> - let cst = check_modtypes cst env arg_t2 arg_t1 equiv in + let subst1 = + (join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in + let cst = check_modtypes cst env + arg_t2 arg_t1 subst2 subst1 + equiv in (* contravariant *) - let env = - add_module (MPbound arg_id2) (module_body_of_type arg_t2) env + let env = add_module + (module_body_of_type (MPbound arg_id2) arg_t2) env in - let body_t1' = - (* since we are just checking well-typedness we do not need - to expand any constant. Hence the identity resolver. *) - subst_struct_expr - (map_mbid arg_id1 (MPbound arg_id2) None) - body_t1 + let subst1 = + (join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in + let env = match body_t1 with + SEBstruct str -> + add_module {mod_mp = mtb1.typ_mp; + mod_expr = None; + mod_type = subst_struct_expr subst1 body_t1; + mod_type_alg= None; + mod_constraints=mtb1.typ_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.typ_delta} env + | _ -> env in - check_structure cst env (eval_struct env body_t1') - (eval_struct env body_t2) equiv + check_structure cst env body_t1 body_t2 equiv + subst1 + subst2 | _ , _ -> error_incompatible_modtypes mtb1 mtb2 in if mtb1'== mtb2' then cst - else check_structure cst env mtb1' mtb2' equiv + else check_structure cst env mtb1' mtb2' equiv subst1 subst2 let check_subtypes env sup super = - check_modtypes Constraint.empty env sup super false + let env = add_module + (module_body_of_type sup.typ_mp sup) env in + check_modtypes Constraint.empty env + (strengthen env sup sup.typ_mp) super empty_subst + (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false + |