summaryrefslogtreecommitdiff
path: root/checker/subtyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/subtyping.ml')
-rw-r--r--checker/subtyping.ml252
1 files changed, 119 insertions, 133 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 7a6868fe..3a100c01 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -19,29 +19,28 @@ open Reduction
open Inductive
open Modops
(*i*)
-open Pp
+open Pp
(* 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 *)
-type namedobject =
+type namedobject =
| Constant of constant_body
| IndType of inductive * mutual_inductive_body
| 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 *)
-let add_nameobjects_of_mib ln mib map =
+let add_nameobjects_of_mib ln mib map =
let add_nameobjects_of_one j oib map =
let ip = (ln,j) in
- let map =
- array_fold_right_i
+ let map =
+ array_fold_right_i
(fun i id map ->
Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map)
oib.mind_consnames
@@ -54,19 +53,19 @@ let add_nameobjects_of_mib ln mib map =
(* creates namedobject map for the whole signature *)
-let make_label_map mp list =
- let add_one (l,e) map =
+let make_label_map 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_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,t,cst) -> add_map (Alias (mp,t))
in
List.fold_right add_one list Labmap.empty
+
let check_conv_error error f env a1 a2 =
try
f env a1 a2
@@ -74,20 +73,21 @@ let check_conv_error error f env a1 a2 =
NotConvertible -> error ()
(* for now we do not allow reorderings *)
-let check_inductive env msid1 l info1 mib2 spec2 =
- let kn = make_kn (MPself msid1) empty_dirpath l in
+let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
+ let kn = make_mind mp1 empty_dirpath l in
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
- let mib1 =
+ let mib1 =
match info1 with
| IndType ((_,0), mib) -> mib
| _ -> error ()
in
+ let mib2 = subst_mind subst2 mib2 in
let check_inductive_type 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
- of the types of the constructors.
+ of the types of the constructors.
By monotonicity of the infered l.u.b. wrt subtyping (i.e. if X:U
|- T(X):s and |- M:U' and U'<=U then infer_type(T(M))<=s), each
@@ -114,7 +114,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
| Type _, Type _ -> (* shortcut here *) Prop Null, Prop Null
| (Prop _, Type _) | (Type _,Prop _) -> error ()
| _ -> (s1, s2) in
- check_conv conv_leq env
+ check_conv conv_leq env
(mkArity (ctx1,s1)) (mkArity (ctx2,s2))
in
@@ -145,7 +145,7 @@ let check_inductive env msid1 l info1 mib2 spec2 =
check (fun mib -> mib.mind_finite);
check (fun mib -> mib.mind_ntypes);
assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
- assert (Array.length mib1.mind_packets >= 1
+ assert (Array.length mib1.mind_packets >= 1
&& Array.length mib2.mind_packets >= 1);
(* Check that the expected numbers of uniform parameters are the same *)
@@ -155,30 +155,30 @@ let check_inductive env msid1 l info1 mib2 spec2 =
(* the inductive types and constructors types have to be convertible *)
check (fun mib -> mib.mind_nparams);
- begin
+ (*begin
match mib2.mind_equiv with
| None -> ()
- | Some kn2' ->
+ | 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 ()
- end;
+ end;*)
(* we check that records and their field names are preserved. *)
check (fun mib -> mib.mind_record);
- if mib1.mind_record then begin
- let rec names_prod_letin t = match t with
+ if mib1.mind_record then begin
+ let rec names_prod_letin t = match 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
+ 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 (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));
end;
(* we first check simple things *)
@@ -187,10 +187,10 @@ let check_inductive env msid1 l info1 mib2 spec2 =
let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets
in ()
-let check_constant env msid1 l info1 cb2 spec2 =
+let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
- let check_type env t1 t2 =
+ let check_type env t1 t2 =
(* If the type of a constant is generated, it may mention
non-variable algebraic universes that the general conversion
@@ -201,7 +201,7 @@ let check_constant env msid1 l info1 cb2 spec2 =
Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
Hence they don't have to be checked again *)
- let t1,t2 =
+ let t1,t2 =
if isArity t2 then
let (ctx2,s2) = destArity t2 in
match s2 with
@@ -236,30 +236,31 @@ let check_constant env msid1 l info1 cb2 spec2 =
(t1,t2) in
check_conv conv_leq env t1 t2
in
-
- match info1 with
- | Constant cb1 ->
- assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
- (*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
- check_type env typ1 typ2;
- let con = make_con (MPself msid1) empty_dirpath l in
- (match cb2 with
- | {const_body=Some lc2;const_opaque=false} ->
- let c2 = force_constr lc2 in
- let c1 = match cb1.const_body with
- | Some lc1 -> force_constr lc1
- | None -> Const con
- in
- check_conv conv env c1 c2
- | _ -> ())
- | IndType ((kn,i),mind1) ->
- ignore (Util.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."));
+ 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
+ let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+ let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+ check_type env typ1 typ2;
+ let con = make_con mp1 empty_dirpath l in
+ (match cb2 with
+ | {const_body=Some lc2;const_opaque=false} ->
+ let c2 = force_constr lc2 in
+ let c1 = match cb1.const_body with
+ | Some lc1 -> force_constr lc1
+ | None -> Const con
+ in
+ check_conv conv env c1 c2
+ | _ -> ())
+ | IndType ((kn,i),mind1) ->
+ ignore (Util.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 cb2.const_body <> None then error () ;
let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
@@ -278,111 +279,96 @@ let check_constant env msid1 l info1 cb2 spec2 =
check_conv conv env ty1 ty2
| _ -> error ()
-let rec check_modules env msid1 l msb1 msb2 =
- let mp = (MPdot(MPself msid1,l)) in
- let mty1 = module_type_of_module (Some mp) msb1 in
- let mty2 = module_type_of_module None msb2 in
- check_modtypes env mty1 mty2 false
-
+let rec check_modules 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
+ check_modtypes env mty1 mty2 subst1 subst2 false;
+
-and check_signatures env (msid1,sig1) alias (msid2,sig2') =
- let mp1 = MPself msid1 in
- let env = add_signature mp1 sig1 env in
- let alias = update_subst_alias alias (map_msid msid2 mp1) in
- let sig2 = subst_structure alias sig2' in
- let sig2 = subst_signature_msid msid2 mp1 sig2 in
+and check_signatures env mp1 sig1 sig2 subst1 subst2 =
let map1 = make_label_map mp1 sig1 in
- let check_one_body (l,spec2) =
- let info1 =
- try
- Labmap.find l map1
- with
- Not_found -> error_no_such_label_sub l msid1 msid2
+ let check_one_body (l,spec2) =
+ let info1 =
+ try
+ Labmap.find l map1
+ with
+ Not_found -> error_no_such_label_sub l mp1
in
match spec2 with
| SFBconst cb2 ->
- check_constant env msid1 l info1 cb2 spec2
- | SFBmind mib2 ->
- check_inductive env msid1 l info1 mib2 spec2
- | SFBmodule msb2 ->
+ check_constant env mp1 l info1 cb2 spec2 subst1 subst2
+ | SFBmind mib2 ->
+ check_inductive env mp1 l info1 mib2 spec2 subst1 subst2
+ | SFBmodule msb2 ->
begin
match info1 with
- | Module msb -> check_modules env msid1 l msb msb2
- | 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 env msid1 l msb msb2
- | _ -> error_not_match l spec2
- end
- | SFBalias (mp,typ_opt,_) ->
- begin
- match info1 with
- | Alias (mp1,_) -> check_modpath_equiv env mp mp1
- | 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 env msid1 l msb msb1
+ | Module msb -> check_modules env msb msb2
+ subst1 subst2
| _ -> error_not_match l spec2
end
| SFBmodtype mtb2 ->
- let mtb1 =
+ let mtb1 =
match info1 with
| Modtype mtb -> mtb
| _ -> error_not_match l spec2
in
- check_modtypes 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 env mtb1 mtb2 subst1 subst2 true
in
List.iter check_one_body sig2
-and check_modtypes env mtb1 mtb2 equiv =
- if mtb1==mtb2 then () 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 env str1 str2 equiv =
- match str1, str2 with
- | SEBstruct (msid1,list1),
- SEBstruct (msid2,list2) ->
- check_signatures env
- (msid1,list1) mtb1.typ_alias (msid2,list2);
- if equiv then
- check_signatures env
- (msid2,list2) mtb2.typ_alias (msid1,list1)
- | SEBfunctor (arg_id1,arg_t1,body_t1),
+and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
+ if mtb1==mtb2 then () else
+ let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
+ let rec check_structure env str1 str2 equiv subst1 subst2 =
+ match str1,str2 with
+ | SEBstruct (list1),
+ SEBstruct (list2) ->
+ check_signatures env
+ mtb1.typ_mp list1 list2 subst1 subst2;
+ if equiv then
+ check_signatures env
+ mtb2.typ_mp list2 list1 subst1 subst2
+ else
+ ()
+ | SEBfunctor (arg_id1,arg_t1,body_t1),
SEBfunctor (arg_id2,arg_t2,body_t2) ->
- check_modtypes env arg_t2 arg_t1 equiv;
+ check_modtypes env
+ arg_t2 arg_t1
+ (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
+ equiv ;
(* 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))
- body_t1
+ let env = match body_t1 with
+ SEBstruct str ->
+ add_module {mod_mp = mtb1.typ_mp;
+ mod_expr = None;
+ mod_type = body_t1;
+ mod_type_alg= None;
+ mod_constraints=mtb1.typ_constraints;
+ mod_retroknowledge = [];
+ mod_delta = mtb1.typ_delta} env
+ | _ -> env
in
- check_structure env (eval_struct env body_t1')
- (eval_struct env body_t2) equiv
+ check_structure env body_t1 body_t2 equiv
+ (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
+ subst2
| _ , _ -> error_incompatible_modtypes mtb1 mtb2
- in
+ in
if mtb1'== mtb2' then ()
- else check_structure env mtb1' mtb2' equiv
+ else check_structure env mtb1' mtb2' equiv subst1 subst2
-let check_subtypes env sup super =
+let check_subtypes env sup super =
(*if sup<>super then*)
- check_modtypes env sup super false
-
-let check_equal env sup super =
+ let env = add_module
+ (module_body_of_type sup.typ_mp sup) env in
+ check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst
+ (map_mp super.typ_mp sup.typ_mp) false
+
+let check_equal env sup super =
(*if sup<>super then*)
- check_modtypes env sup super true
+ check_modtypes env sup super empty_subst
+ (map_mp super.typ_mp sup.typ_mp) true
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-19 06:50:57 +0000