From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- kernel/subtyping.ml | 334 ++++++++++++++++++++++++++++++---------------------- 1 file changed, 193 insertions(+), 141 deletions(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index d17d7bb0..db155e6c 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) + Label.Map.add (Label.of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames map in - Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map + Label.Map.add (Label.of_id oib.mind_typename) (IndType (ip, mib)) map in - array_fold_right_i add_mip_nameobjects mib.mind_packets map + Array.fold_right_i add_mip_nameobjects mib.mind_packets map (* creates (namedobject/namedmodule) map for the whole signature *) -type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t } +type labmap = { objs : namedobject Label.Map.t; mods : namedmodule Label.Map.t } -let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty } +let empty_labmap = { objs = Label.Map.empty; mods = Label.Map.empty } let get_obj mp map l = - try Labmap.find l map.objs + try Label.Map.find l map.objs with Not_found -> error_no_such_label_sub l (string_of_mp mp) let get_mod mp map l = - try Labmap.find l map.mods + try Label.Map.find l map.mods with Not_found -> error_no_such_label_sub l (string_of_mp mp) let make_labmap mp list = let add_one (l,e) map = match e with - | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs } + | SFBconst cb -> { map with objs = Label.Map.add l (Constant cb) map.objs } | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs } - | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods } - | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods } + | SFBmodule mb -> { map with mods = Label.Map.add l (Module mb) map.mods } + | SFBmodtype mtb -> { map with mods = Label.Map.add l (Modtype mtb) map.mods } in List.fold_right add_one list empty_labmap -let check_conv_error error why cst f env a1 a2 = - try - union_constraints cst (f env a1 a2) - with - NotConvertible -> error why +let check_conv_error error why cst poly u f env a1 a2 = + try + let a1 = Vars.subst_instance_constr u a1 in + let a2 = Vars.subst_instance_constr u a2 in + let cst' = f env (Environ.universes env) a1 a2 in + if poly then + if Constraint.is_empty cst' then cst + else error (IncompatiblePolymorphism (env, a1, a2)) + else Constraint.union cst cst' + with NotConvertible -> error why (* for now we do not allow reorderings *) 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 kn1 = KerName.make2 mp1 l in + let kn2 = KerName.make2 mp2 l in let error why = error_signature_mismatch l spec2 why in - let check_conv why cst f = check_conv_error error why cst f in + let check_conv why cst poly u f = check_conv_error error why cst poly u f in let mib1 = match info1 with - | IndType ((_,0), mib) -> subst_mind subst1 mib + | IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib | _ -> error (InductiveFieldExpected mib2) in - let mib2 = subst_mind subst2 mib2 in + let poly = + if not (mib1.mind_polymorphic == mib2.mind_polymorphic) then + error (PolymorphicStatusExpected mib2.mind_polymorphic) + else mib2.mind_polymorphic + in + let u = + if poly then + Errors.error ("Checking of subtyping of polymorphic" ^ + " inductive types not implemented") + else Instance.empty + in + let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name env t1 t2 = (* Due to sort-polymorphism in inductive types, the conclusions of @@ -133,40 +148,44 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 error (NotConvertibleInductiveField name) | _ -> (s1, s2) in check_conv (NotConvertibleInductiveField name) - cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) + cst poly u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2)) in let check_packet cst p1 p2 = - let check f why = if f p1 <> f p2 then error why in - check (fun p -> p.mind_consnames) NotSameConstructorNamesField; - check (fun p -> p.mind_typename) NotSameInductiveNameInBlockField; + let check f test why = if not (test (f p1) (f p2)) then error why in + check (fun p -> p.mind_consnames) (Array.equal Id.equal) NotSameConstructorNamesField; + check (fun p -> p.mind_typename) Id.equal NotSameInductiveNameInBlockField; (* nf_lc later *) (* nf_arity later *) (* user_lc ignored *) (* user_arity ignored *) - check (fun p -> p.mind_nrealargs) (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *) + check (fun p -> p.mind_nrealargs) Int.equal (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *) (* kelim ignored *) (* listrec ignored *) (* finite done *) (* nparams done *) (* params_ctxt done because part of the inductive types *) (* Don't check the sort of the type if polymorphic *) - let cst = check_inductive_type cst p2.mind_typename env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) - in + let ty1, cst1 = constrained_type_of_inductive env ((mib1,p1),u) in + let ty2, cst2 = constrained_type_of_inductive env ((mib2,p2),u) in + let cst = Constraint.union cst1 (Constraint.union cst2 cst) in + let cst = check_inductive_type cst p2.mind_typename env ty1 ty2 in cst in + let mind = mind_of_kn kn1 in let check_cons_types i cst p1 p2 = - array_fold_left3 - (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst conv env t1 t2) + Array.fold_left3 + (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst + poly u infer_conv env t1 t2) cst p2.mind_consnames - (arities_of_specif kn1 (mib1,p1)) - (arities_of_specif kn1 (mib2,p2)) + (arities_of_specif (mind,u) (mib1,p1)) + (arities_of_specif (mind,u) (mib2,p2)) in - let check f why = if f mib1 <> f mib2 then error (why (f mib2)) in - check (fun mib -> mib.mind_finite) (fun x -> FiniteInductiveFieldExpected x); - check (fun mib -> mib.mind_ntypes) (fun x -> InductiveNumbersFieldExpected x); - assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]); + let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in + check (fun mib -> mib.mind_finite<>Decl_kinds.CoFinite) (==) (fun x -> FiniteInductiveFieldExpected x); + check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x); + assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps); assert (Array.length mib1.mind_packets >= 1 && Array.length mib2.mind_packets >= 1); @@ -175,49 +194,50 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 (* at the time of checking the inductive arities in check_packet. *) (* Notice that we don't expect the local definitions to match: only *) (* the inductive types and constructors types have to be convertible *) - check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x); + check (fun mib -> mib.mind_nparams) Int.equal (fun x -> InductiveParamsNumberField x); begin - match mind_of_delta reso2 kn2 with - | kn2' when kn2=kn2' -> () - | kn2' -> - if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then - error NotEqualInductiveAliases + let kn2' = kn_of_delta reso2 kn2 in + if KerName.equal kn2 kn2' || + MutInd.equal (mind_of_delta_kn reso1 kn1) + (subst_mind subst2 (MutInd.make kn2 kn2')) + then () + else error NotEqualInductiveAliases end; (* we check that records and their field names are preserved. *) - check (fun mib -> mib.mind_record) (fun x -> RecordFieldExpected x); - if mib1.mind_record then begin + check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x); + if mib1.mind_record <> None then begin let rec names_prod_letin t = match kind_of_term t with | Prod(n,_,t) -> n::(names_prod_letin t) | LetIn(n,_,_,t) -> n::(names_prod_letin t) | Cast(t,_,_) -> names_prod_letin t | _ -> [] in - assert (Array.length mib1.mind_packets = 1); - assert (Array.length mib2.mind_packets = 1); - assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1); - assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1); + assert (Int.equal (Array.length mib1.mind_packets) 1); + assert (Int.equal (Array.length mib2.mind_packets) 1); + assert (Int.equal (Array.length mib1.mind_packets.(0).mind_user_lc) 1); + assert (Int.equal (Array.length mib2.mind_packets.(0).mind_user_lc) 1); check (fun mib -> let nparamdecls = List.length mib.mind_params_ctxt in let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in - snd (list_chop nparamdecls names)) + snd (List.chop nparamdecls names)) (List.equal Name.equal) (fun x -> RecordProjectionsExpected x); end; (* we first check simple things *) let cst = - array_fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets + Array.fold_left2 check_packet cst mib1.mind_packets mib2.mind_packets in (* and constructor types in the end *) let cst = - array_fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets + Array.fold_left2_i check_cons_types cst mib1.mind_packets mib2.mind_packets in cst let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let error why = error_signature_mismatch l spec2 why in - let check_conv cst f = check_conv_error error cst f in - let check_type cst env t1 t2 = + let check_conv cst poly u f = check_conv_error error cst poly u f in + let check_type poly u cst env t1 t2 = let err = NotConvertibleTypeField (env, t1, t2) in @@ -264,18 +284,47 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = t1,t2 else (t1,t2) in - check_conv err cst conv_leq env t1 t2 + check_conv err cst poly u infer_conv_leq env t1 t2 in - match info1 with | Constant cb1 -> - assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ; - let cb1 = subst_const_body subst1 cb1 in - let cb2 = subst_const_body subst2 cb2 in - (* 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 - let cst = check_type cst env typ1 typ2 in + let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in + let cb1 = Declareops.subst_const_body subst1 cb1 in + let cb2 = Declareops.subst_const_body subst2 cb2 in + (* Start by checking universes *) + let poly = + if not (cb1.const_polymorphic == cb2.const_polymorphic) then + error (PolymorphicStatusExpected cb2.const_polymorphic) + else cb2.const_polymorphic + in + let cst', env', u = + if poly then + let ctx1 = Univ.instantiate_univ_context cb1.const_universes in + let ctx2 = Univ.instantiate_univ_context cb2.const_universes in + let inst1, ctx1 = Univ.UContext.dest ctx1 in + let inst2, ctx2 = Univ.UContext.dest ctx2 in + if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then + error IncompatibleInstances + else + let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in + let cstrs = Univ.Constraint.union cstrs ctx2 in + try + (* The environment with the expected universes plus equality + of the body instances with the expected instance *) + let env = Environ.add_constraints cstrs env in + (* Check that the given definition does not add any constraint over + the expected ones, so that it can be used in place of the original. *) + if Univ.check_constraints ctx1 (Environ.universes env) then + cstrs, env, inst2 + else error (IncompatibleConstraints ctx1) + with Univ.UniverseInconsistency incon -> + error (IncompatibleUniverses incon) + else cst, env, Univ.Instance.empty + in + (* Now check 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 + let cst = check_type poly u cst env' typ1 typ2 in (* Now we check the bodies: - A transparent constant can only be implemented by a compatible transparent constant. @@ -290,39 +339,47 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = | Def lc1 -> (* NB: cb1 might have been strengthened and appear as transparent. Anyway [check_conv] will handle that afterwards. *) - let c1 = Declarations.force lc1 in - let c2 = Declarations.force lc2 in - check_conv NotConvertibleBodyField cst conv env c1 c2)) + let c1 = Mod_subst.force_constr lc1 in + let c2 = Mod_subst.force_constr lc2 in + check_conv NotConvertibleBodyField cst poly u infer_conv env' c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Util.error ( + ignore (Errors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ "name.")); - assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; - if constant_has_body cb2 then error DefinitionFieldExpected; - let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in + let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in + if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; + let u1 = inductive_instance mind1 in + let arity1,cst1 = constrained_type_of_inductive env + ((mind1,mind1.mind_packets.(i)),u1) in + let cst2 = + Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in let typ2 = Typeops.type_of_constant_type env cb2.const_type in + let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, arity1, typ2) in - check_conv error cst conv_leq env arity1 typ2 + check_conv error cst false Univ.Instance.empty infer_conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Util.error ( + ignore (Errors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ "name.")); - assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ; - if constant_has_body cb2 then error DefinitionFieldExpected; - let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in + let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in + if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; + let u1 = inductive_instance mind1 in + let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in + let cst2 = + Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in let ty2 = Typeops.type_of_constant_type env cb2.const_type in + let cst = Constraint.union cst (Constraint.union cst1 cst2) in let error = NotConvertibleTypeField (env, ty1, ty2) in - check_conv error cst conv env ty1 ty2 + check_conv error cst false Univ.Instance.empty infer_conv env ty1 ty2 let rec check_modules cst env msb1 msb2 subst1 subst2 = - let mty1 = module_type_of_module None msb1 in - let mty2 = module_type_of_module None msb2 in - let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in - cst + let mty1 = module_type_of_module msb1 in + let mty2 = module_type_of_module msb2 in + check_modtypes cst env mty1 mty2 subst1 subst2 false and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= let map1 = make_labmap mp1 sig1 in @@ -344,67 +401,62 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= | Modtype mtb -> mtb | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected in - 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 + let env = + add_module_type mtb2.mod_mp mtb2 + (add_module_type mtb1.mod_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 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.union_constraints - (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 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 - (module_body_of_type (MPbound arg_id2) arg_t2) env - 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 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 subst1 subst2 +and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = + if mtb1==mtb2 || mtb1.mod_type == mtb2.mod_type then cst + else + let rec check_structure cst env str1 str2 equiv subst1 subst2 = + match str1,str2 with + |NoFunctor list1, + NoFunctor list2 -> + if equiv then + let subst2 = add_mp mtb2.mod_mp mtb1.mod_mp mtb1.mod_delta subst2 in + let cst1 = check_signatures cst env + mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2 + mtb1.mod_delta mtb2.mod_delta + in + let cst2 = check_signatures cst env + mtb2.mod_mp list2 mtb1.mod_mp list1 subst2 subst1 + mtb2.mod_delta mtb1.mod_delta + in + Univ.Constraint.union cst1 cst2 + else + check_signatures cst env + mtb1.mod_mp list1 mtb2.mod_mp list2 subst1 subst2 + mtb1.mod_delta mtb2.mod_delta + |MoreFunctor (arg_id1,arg_t1,body_t1), + MoreFunctor (arg_id2,arg_t2,body_t2) -> + let mp2 = MPbound arg_id2 in + let subst1 = join (map_mbid arg_id1 mp2 arg_t2.mod_delta) subst1 in + let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in + (* contravariant *) + let env = add_module_type mp2 arg_t2 env in + let env = + if Modops.is_functor body_t1 then env + else add_module + {mod_mp = mtb1.mod_mp; + mod_expr = Abstract; + mod_type = subst_signature subst1 body_t1; + mod_type_alg = None; + mod_constraints = mtb1.mod_constraints; + mod_retroknowledge = []; + mod_delta = mtb1.mod_delta} env + in + check_structure cst env body_t1 body_t2 equiv subst1 subst2 + | _ , _ -> error_incompatible_modtypes mtb1 mtb2 + in + check_structure cst env mtb1.mod_type mtb2.mod_type equiv subst1 subst2 let check_subtypes env sup super = - let env = add_module - (module_body_of_type sup.typ_mp sup) env in - check_modtypes empty_constraint env - (strengthen sup sup.typ_mp) super empty_subst - (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false + let env = add_module_type sup.mod_mp sup env in + check_modtypes Univ.Constraint.empty env + (strengthen sup sup.mod_mp) super empty_subst + (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false -- cgit v1.2.3