diff options
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 32 |
1 files changed, 12 insertions, 20 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 31dab0c9..0916d98d 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -12,7 +12,6 @@ open Util open Names open Cic -open Term open Declarations open Environ open Reduction @@ -123,16 +122,6 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= env, Univ.make_abstract_instance auctx' | _ -> error () in - let eq_projection_body p1 p2 = - let check eq f = if not (eq (f p1) (f p2)) then error () in - check MutInd.equal (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 t1 t2 = check_conv conv_leq env t1 t2 in let check_packet p1 p2 = @@ -186,16 +175,19 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= (* we check that records and their field names are preserved. *) 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 Constant.UserOrd.equal p1 p2 && - Array.for_all2 eq_projection_body pb1 pb2 + | NotRecord, NotRecord -> true + | FakeRecord, FakeRecord -> true + | PrimRecord info1, PrimRecord info2 -> + let check (id1, p1, pb1) (id2, p2, pb2) = + (* we don't care about the id, the types are inferred from the inductive + (ie checked before now) *) + Array.for_all2 Label.equal p1 p2 + in + Array.equal check info1 info2 | _, _ -> false in check record_equal (fun mib -> mib.mind_record); - if mib1.mind_record != None then begin + if mib1.mind_record != NotRecord 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) @@ -216,7 +208,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= 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 = +let check_constant env 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 = check_conv conv_leq env t1 t2 in @@ -280,7 +272,7 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 = let check_one_body (l,spec2) = match spec2 with | SFBconst cb2 -> - check_constant env mp1 l (get_obj mp1 map1 l) + check_constant env l (get_obj mp1 map1 l) cb2 spec2 subst1 subst2 | SFBmind mib2 -> check_inductive env mp1 l (get_obj mp1 map1 l) |