summaryrefslogtreecommitdiff
path: root/checker/subtyping.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/subtyping.ml')
-rw-r--r--checker/subtyping.ml217
1 files changed, 121 insertions, 96 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 02821c29..372c3142 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -1,15 +1,16 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i*)
+open Errors
open Util
open Names
-open Univ
+open Cic
open Term
open Declarations
open Environ
@@ -17,9 +18,6 @@ open Reduction
open Inductive
open Modops
(*i*)
-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
@@ -37,42 +35,42 @@ type namedmodule =
constructors *)
let add_mib_nameobjects mp l mib map =
- let ind = make_mind mp empty_dirpath l in
+ let ind = MutInd.make2 mp l in
let add_mip_nameobjects j oib map =
let ip = (ind,j) in
let map =
- array_fold_right_i
+ Array.fold_right_i
(fun i id map ->
- 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 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 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
@@ -85,7 +83,7 @@ let check_conv_error error f env a1 a2 =
(* for now we do not allow reorderings *)
let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
- let kn = make_mind mp1 empty_dirpath l in
+ let kn = MutInd.make2 mp1 l in
let error () = error_not_match l spec2 in
let check_conv f = check_conv_error error f in
let mib1 =
@@ -93,7 +91,26 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
| IndType ((_,0), mib) -> mib
| _ -> error ()
in
- let mib2 = subst_mind subst2 mib2 in
+ let mib2 = subst_mind subst2 mib2 in
+ let check eq f = if not (eq (f mib1) (f mib2)) then error () in
+ let bool_equal (x : bool) (y : bool) = x = y in
+ let u =
+ check bool_equal (fun x -> x.mind_polymorphic);
+ if mib1.mind_polymorphic then (
+ check Univ.Instance.equal (fun x -> Univ.UContext.instance x.mind_universes);
+ Univ.UContext.instance mib1.mind_universes)
+ else Univ.Instance.empty
+ in
+ let eq_projection_body p1 p2 =
+ let check eq f = if not (eq (f p1) (f p2)) then error () in
+ check eq_mind (fun x -> x.proj_ind);
+ check (==) (fun x -> x.proj_npars);
+ check (==) (fun x -> x.proj_arg);
+ check (eq_constr) (fun x -> x.proj_type);
+ check (eq_constr) (fun x -> fst x.proj_eta);
+ check (eq_constr) (fun x -> snd x.proj_eta);
+ check (eq_constr) (fun x -> x.proj_body); true
+ in
let check_inductive_type env t1 t2 =
(* Due to sort-polymorphism in inductive types, the conclusions of
@@ -130,14 +147,16 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
in
let check_packet 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 eq f = if not (eq (f p1) (f p2)) then error () in
+ check
+ (fun a1 a2 -> Array.equal Id.equal a1 a2)
+ (fun p -> p.mind_consnames);
+ check Id.equal (fun p -> p.mind_typename);
(* nf_lc later *)
(* nf_arity later *)
(* user_lc ignored *)
(* user_arity ignored *)
- check (fun p -> p.mind_nrealargs);
+ check Int.equal (fun p -> p.mind_nrealargs);
(* kelim ignored *)
(* listrec ignored *)
(* finite done *)
@@ -145,17 +164,15 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
(* params_ctxt done because part of the inductive types *)
(* Don't check the sort of the type if polymorphic *)
check_inductive_type env
- (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
+ (type_of_inductive env ((mib1,p1),u)) (type_of_inductive env ((mib2,p2),u))
in
let check_cons_types i p1 p2 =
- array_iter2 (check_conv conv env)
- (arities_of_specif kn (mib1,p1))
- (arities_of_specif kn (mib2,p2))
+ Array.iter2 (check_conv conv env)
+ (arities_of_specif (kn,u) (mib1,p1))
+ (arities_of_specif (kn,u) (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);
- assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
+ check (==) (fun mib -> mib.mind_finite);
+ check Int.equal (fun mib -> mib.mind_ntypes);
assert (Array.length mib1.mind_packets >= 1
&& Array.length mib2.mind_packets >= 1);
@@ -164,7 +181,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
(* 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 Int.equal (fun mib -> mib.mind_nparams);
(*begin
match mib2.mind_equiv with
@@ -178,8 +195,18 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
if kn1 <> kn2 then error ()
end;*)
(* we check that records and their field names are preserved. *)
- check (fun mib -> mib.mind_record);
- if mib1.mind_record then begin
+ let record_equal x y =
+ match x, y with
+ | None, None -> true
+ | Some None, Some None -> true
+ | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
+ Id.equal id1 id2 &&
+ Array.for_all2 eq_con_chk p1 p2 &&
+ Array.for_all2 eq_projection_body pb1 pb2
+ | _, _ -> false
+ in
+ check record_equal (fun mib -> mib.mind_record);
+ if mib1.mind_record != None 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)
@@ -190,12 +217,14 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2=
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 l1 l2 -> List.equal Name.equal l1 l2)
+ (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
end;
(* we first check simple things *)
- array_iter2 check_packet mib1.mind_packets mib2.mind_packets;
+ Array.iter2 check_packet mib1.mind_packets mib2.mind_packets;
(* and constructor types in the end *)
- let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets
+ let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets
in ()
let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
@@ -216,13 +245,13 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
if isArity t2 then
let (ctx2,s2) = destArity t2 in
match s2 with
- | Type v when not (is_univ_variable v) ->
+ | Type v when not (Univ.is_univ_variable v) ->
(* The type in the interface is inferred and is made of algebraic
universes *)
begin try
let (ctx1,s1) = dest_arity env t1 in
match s1 with
- | Type u when not (is_univ_variable u) ->
+ | Type u when not (Univ.is_univ_variable u) ->
(* Both types are inferred, no need to recheck them. We
cheat and collapse the types to Prop *)
mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
@@ -249,7 +278,6 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
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*)
@@ -274,25 +302,25 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
let c2 = force_constr lc2 in
check_conv 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 () ;
- let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
+ let u = inductive_instance mind1 in
+ let arity1 = type_of_inductive env ((mind1,mind1.mind_packets.(i)),u) in
let typ2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv 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 () ;
- let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
+ let u1 = inductive_instance mind1 in
+ let ty1 = type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
let ty2 = Typeops.type_of_constant_type env cb2.const_type in
check_conv conv env ty1 ty2
@@ -325,56 +353,53 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
| Modtype mtb -> mtb
| _ -> error_not_match l spec2
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 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 env mtb1 mtb2 subst1 subst2 true
in
- List.iter check_one_body sig2
-
-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
- (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
- equiv ;
- (* contravariant *)
- let env = add_module
- (module_body_of_type (MPbound arg_id2) arg_t2) env
- in
- let env = match body_t1 with
- SEBstruct str ->
- let env = shallow_remove_module mtb1.typ_mp env in
- 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 body_t1 body_t2 equiv
- (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
- subst2
- | _ , _ -> error_incompatible_modtypes mtb1 mtb2
- in
- if mtb1'== mtb2' then ()
- else check_structure env mtb1' mtb2' equiv subst1 subst2
+ List.iter check_one_body sig2
+
+and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
+ if mtb1==mtb2 || mtb1.mod_type == mtb2.mod_type then ()
+ else
+ let rec check_structure env str1 str2 equiv subst1 subst2 =
+ match str1,str2 with
+ | NoFunctor (list1),
+ NoFunctor (list2) ->
+ check_signatures env mtb1.mod_mp list1 list2 subst1 subst2;
+ if equiv then
+ check_signatures env mtb2.mod_mp list2 list1 subst1 subst2
+ else
+ ()
+ | MoreFunctor (arg_id1,arg_t1,body_t1),
+ MoreFunctor (arg_id2,arg_t2,body_t2) ->
+ check_modtypes env
+ arg_t2 arg_t1
+ (map_mp arg_t1.mod_mp arg_t2.mod_mp) subst2
+ equiv;
+ (* contravariant *)
+ let env = add_module_type (MPbound arg_id2) arg_t2 env in
+ let env =
+ if is_functor body_t1 then env
+ else
+ let env = shallow_remove_module mtb1.mod_mp env in
+ add_module {mod_mp = mtb1.mod_mp;
+ mod_expr = Abstract;
+ mod_type = body_t1;
+ mod_type_alg = None;
+ mod_constraints = mtb1.mod_constraints;
+ mod_retroknowledge = [];
+ mod_delta = mtb1.mod_delta} env
+ in
+ check_structure env body_t1 body_t2 equiv
+ (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
+ subst2
+ | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+ in
+ check_structure env mtb1.mod_type mtb2.mod_type equiv subst1 subst2
let check_subtypes env sup super =
- check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
- (map_mp super.typ_mp sup.typ_mp) false
+ check_modtypes env (strengthen sup sup.mod_mp) super empty_subst
+ (map_mp super.mod_mp sup.mod_mp) false
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 10:17:19 +0000