summaryrefslogtreecommitdiff
path: root/kernel/subtyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/subtyping.ml')
-rw-r--r--kernel/subtyping.ml240
1 files changed, 116 insertions, 124 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 447e062a..c809572a 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-2012 *)
(* \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 *)
@@ -31,15 +32,18 @@ type namedobject =
| Constant of constant_body
| IndType of inductive * mutual_inductive_body
| IndConstr of constructor * mutual_inductive_body
+
+type namedmodule =
| Module of module_body
| Modtype of module_type_body
(* adds above information about one mutual inductive: all types and
constructors *)
-let add_nameobjects_of_mib ln mib map =
- let add_nameobjects_of_one j oib map =
- let ip = (ln,j) in
+let add_mib_nameobjects mp l mib map =
+ let ind = make_mind mp empty_dirpath l in
+ let add_mip_nameobjects j oib map =
+ let ip = (ind,j) in
let map =
array_fold_right_i
(fun i id map ->
@@ -49,43 +53,54 @@ let add_nameobjects_of_mib ln mib map =
in
Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
in
- array_fold_right_i add_nameobjects_of_one 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 }
+let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
-(* creates namedobject map for the whole signature *)
+let get_obj mp map l =
+ try Labmap.find l map.objs
+ with Not_found -> error_no_such_label_sub l (string_of_mp mp)
-let make_label_map mp list =
+let get_mod mp map l =
+ try Labmap.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 =
- let add_map obj = Labmap.add l obj map in
match e with
- | SFBconst cb -> add_map (Constant cb)
- | SFBmind mib ->
- add_nameobjects_of_mib (make_mind mp empty_dirpath l) mib map
- | SFBmodule mb -> add_map (Module mb)
- | SFBmodtype mtb -> add_map (Modtype mtb)
+ | SFBconst cb -> { map with objs = Labmap.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 }
in
- List.fold_right add_one list Labmap.empty
+ List.fold_right add_one list empty_labmap
+
-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 +129,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 +175,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 +197,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,10 +215,12 @@ 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 =
+ let err = NotConvertibleTypeField (env, t1, t2) in
+
(* 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
@@ -233,66 +257,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 err end
+ | _ ->
+ t1,t2
else
(t1,t2) in
- check_conv cst conv_leq env t1 t2
+ check_conv err 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 +300,11 @@ 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
+ let error = NotConvertibleTypeField (env, arity1, typ2) in
+ check_conv error 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,46 +312,37 @@ 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 ()
+ let error = NotConvertibleTypeField (env, ty1, ty2) in
+ check_conv error cst conv env ty1 ty2
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
and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
- let map1 = make_label_map mp1 sig1 in
+ let map1 = make_labmap mp1 sig1 in
let check_one_body cst (l,spec2) =
- let info1 =
- try
- Labmap.find l map1
- with
- Not_found -> error_no_such_label_sub l
- (string_of_mp mp1)
- in
- match spec2 with
+ match spec2 with
| SFBconst cb2 ->
- check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2
+ check_constant cst env mp1 l (get_obj mp1 map1 l)
+ cb2 spec2 subst1 subst2
| SFBmind mib2 ->
- check_inductive cst env
- mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
+ check_inductive cst env mp1 l (get_obj mp1 map1 l)
+ mp2 mib2 spec2 subst1 subst2 reso1 reso2
| SFBmodule msb2 ->
- begin
- match info1 with
- | Module msb -> check_modules cst env msb msb2
- subst1 subst2
- | _ -> error_not_match l spec2
+ begin match get_mod mp1 map1 l with
+ | Module msb -> check_modules cst env msb msb2 subst1 subst2
+ | _ -> error_signature_mismatch l spec2 ModuleFieldExpected
end
| SFBmodtype mtb2 ->
- let mtb1 =
- match info1 with
- | Modtype mtb -> mtb
- | _ -> error_not_match l spec2
+ let mtb1 = match get_mod mp1 map1 l with
+ | 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
@@ -368,7 +360,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 +404,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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 03:48:54 +0000