summaryrefslogtreecommitdiff
path: root/kernel/subtyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/subtyping.ml')
-rw-r--r--kernel/subtyping.ml168
1 files changed, 76 insertions, 92 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 447e062a..c141a02a 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -1,12 +1,15 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: subtyping.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+ the Coq module system *)
+
+(* This module checks subtyping of module types *)
(*i*)
open Util
@@ -22,8 +25,6 @@ open Mod_subst
open Entries
(*i*)
-
-
(* This local type is used to subtype a constant with a constructor or
an inductive type. It can also be useful to allow reorderings in
inductive types *)
@@ -66,26 +67,26 @@ let make_label_map mp list =
in
List.fold_right add_one list Labmap.empty
-let check_conv_error error cst f env a1 a2 =
+let check_conv_error error why cst f env a1 a2 =
try
- Constraint.union cst (f env a1 a2)
+ union_constraints cst (f env a1 a2)
with
- NotConvertible -> error ()
+ 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 error () = error_not_match l spec2 in
- let check_conv cst f = check_conv_error error cst f 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 mib1 =
match info1 with
| IndType ((_,0), mib) -> subst_mind subst1 mib
- | _ -> error ()
+ | _ -> error (InductiveFieldExpected mib2)
in
let mib2 = subst_mind subst2 mib2 in
- let check_inductive_type cst env t1 t2 =
+ let check_inductive_type cst name env t1 t2 =
(* Due to sort-polymorphism in inductive types, the conclusions of
t1 and t2, if in Type, are generated as the least upper bounds
@@ -114,40 +115,43 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
let s1,s2 =
match s1, s2 with
| Type _, Type _ -> (* shortcut here *) prop_sort, prop_sort
- | (Prop _, Type _) | (Type _,Prop _) -> error ()
+ | (Prop _, Type _) | (Type _,Prop _) ->
+ error (NotConvertibleInductiveField name)
| _ -> (s1, s2) in
- check_conv cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+ check_conv (NotConvertibleInductiveField name)
+ cst conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
in
let check_packet cst p1 p2 =
- let check f = if f p1 <> f p2 then error () in
- check (fun p -> p.mind_consnames);
- check (fun p -> p.mind_typename);
+ 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;
(* nf_lc later *)
(* nf_arity later *)
(* user_lc ignored *)
(* user_arity ignored *)
- check (fun p -> p.mind_nrealargs);
+ check (fun p -> p.mind_nrealargs) (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 env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
+ let cst = check_inductive_type cst p2.mind_typename env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
in
cst
in
let check_cons_types i cst p1 p2 =
- array_fold_left2
- (fun cst t1 t2 -> check_conv cst conv env t1 t2)
+ array_fold_left3
+ (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst conv env t1 t2)
cst
+ p2.mind_consnames
(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);
- check (fun mib -> mib.mind_ntypes);
+ 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=[]);
assert (Array.length mib1.mind_packets >= 1
&& Array.length mib2.mind_packets >= 1);
@@ -157,17 +161,17 @@ 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);
+ check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x);
- begin
+ 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 ()
+ error NotEqualInductiveAliases
end;
(* we check that records and their field names are preserved. *)
- check (fun mib -> mib.mind_record);
+ check (fun mib -> mib.mind_record) (fun x -> RecordFieldExpected x);
if mib1.mind_record then begin
let rec names_prod_letin t = match kind_of_term t with
| Prod(n,_,t) -> n::(names_prod_letin t)
@@ -179,7 +183,11 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
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);
- check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
+ 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))
+ (fun x -> RecordProjectionsExpected x);
end;
(* we first check simple things *)
let cst =
@@ -193,7 +201,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
- let error () = error_not_match l spec2 in
+ 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 =
@@ -233,66 +241,42 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
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 *)
- error ()
- with UserError _ (* "not an arity" *) ->
- error () end
- | _ -> t1,t2
+ error NoTypeConstraintExpected
+ with NotArity ->
+ error NotConvertibleTypeField end
+ | _ ->
+ t1,t2
else
(t1,t2) in
- check_conv cst conv_leq env t1 t2
+ check_conv NotConvertibleTypeField cst conv_leq env t1 t2
in
match info1 with
| 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
+ 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 con = make_con mp1 empty_dirpath l in
- let cst =
- if cb2.const_opaque then
- (* In this case we compare opaque definitions, we need to bypass
- the opacity and do a delta step*)
- match cb2.const_body with
- | None -> cst
- | Some lc2 ->
- let c2 = Declarations.force lc2 in
- let c1 = match cb1.const_body with
- | Some lc1 ->
- let c = Declarations.force lc1 in
- begin
- match (kind_of_term c),(kind_of_term c2) with
- Const n1,Const n2 when (eq_constant n1 n2) -> c
- (* c1 may have been strenghtened
- we need to unfold it*)
- | Const n,_ ->
- let cb = subst_const_body subst1
- (lookup_constant n env) in
- (match cb.const_opaque,
- cb.const_body with
- | true, Some lc1 ->
- Declarations.force lc1
- | _,_ -> c)
- | _ ,_-> c
- end
- | None -> mkConst con
- in
- check_conv cst conv env c1 c2
- else
- match cb2.const_body with
- | None -> cst
- | Some lc2 ->
- let c2 = Declarations.force lc2 in
- let c1 = match cb1.const_body with
- | Some lc1 -> Declarations.force lc1
- | None -> mkConst con
- in
- check_conv cst conv env c1 c2
- in
- cst
+ (* Now we check the bodies:
+ - A transparent constant can only be implemented by a compatible
+ transparent constant.
+ - In the signature, an opaque is handled just as a parameter:
+ anything of the right type can implement it, even if bodies differ.
+ *)
+ (match cb2.const_body with
+ | Undef _ | OpaqueDef _ -> cst
+ | Def lc2 ->
+ (match cb1.const_body with
+ | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField
+ | 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))
| IndType ((kn,i),mind1) ->
ignore (Util.error (
"The kernel does not recognize yet that a parameter can be " ^
@@ -300,10 +284,10 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
"inductive type and give a definition to map the old name to the new " ^
"name."));
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
- if cb2.const_body <> None then error () ;
+ if constant_has_body cb2 then error DefinitionFieldExpected;
let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
- check_conv cst conv_leq env arity1 typ2
+ check_conv NotConvertibleTypeField cst conv_leq env arity1 typ2
| IndConstr (((kn,i),j) as cstr,mind1) ->
ignore (Util.error (
"The kernel does not recognize yet that a parameter can be " ^
@@ -311,15 +295,15 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
"constructor and give a definition to map the old name to the new " ^
"name."));
assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
- if cb2.const_body <> None then error () ;
+ if constant_has_body cb2 then error DefinitionFieldExpected;
let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
- check_conv cst conv env ty1 ty2
- | _ -> error ()
+ check_conv NotConvertibleTypeField cst conv env ty1 ty2
+ | _ -> error DefinitionFieldExpected
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 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
@@ -344,13 +328,13 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
match info1 with
| Module msb -> check_modules cst env msb msb2
subst1 subst2
- | _ -> error_not_match l spec2
+ | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
end
| SFBmodtype mtb2 ->
let mtb1 =
match info1 with
| Modtype mtb -> mtb
- | _ -> error_not_match l spec2
+ | _ -> 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
@@ -368,7 +352,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
if equiv then
let subst2 =
add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
- Univ.Constraint.union
+ Univ.union_constraints
(check_signatures cst env
mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
mtb1.typ_delta mtb2.typ_delta)
@@ -412,7 +396,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
let check_subtypes env sup super =
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
+ 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