diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/closure.ml | 18 | ||||
| -rw-r--r-- | checker/closure.mli | 5 | ||||
| -rw-r--r-- | checker/reduction.ml | 8 | ||||
| -rw-r--r-- | checker/subtyping.ml | 13 |
4 files changed, 24 insertions, 20 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index bfba6c161..66e69f225 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -135,22 +135,16 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] * instantiations (cbv or lazy) are. *) -type 'a tableKey = - | ConstKey of 'a - | VarKey of Id.t - | RelKey of int - type table_key = Constant.t puniverses tableKey + +let eq_pconstant_key (c,u) (c',u') = + eq_constant_key c c' && Univ.Instance.equal u u' + module KeyHash = struct type t = table_key - let equal k1 k2 = match k1, k2 with - | ConstKey (c1,u1), ConstKey (c2,u2) -> Constant.UserOrd.equal c1 c2 - && Univ.Instance.equal u1 u2 - | VarKey id1, VarKey id2 -> Id.equal id1 id2 - | RelKey i1, RelKey i2 -> Int.equal i1 i2 - | (ConstKey _ | VarKey _ | RelKey _), _ -> false + let equal = Names.eq_table_key eq_pconstant_key open Hashset.Combine @@ -201,8 +195,6 @@ let defined_rels flags env = let mind_equiv_infos info = mind_equiv info.i_env -let eq_table_key = KeyHash.equal - let create mk_cl flgs env = { i_flags = flgs; i_repr = mk_cl; diff --git a/checker/closure.mli b/checker/closure.mli index 4cf02ae2b..49b07f730 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -58,10 +58,6 @@ val betaiotazeta : reds val betadeltaiotanolet : reds (***********************************************************************) -type 'a tableKey = - | ConstKey of 'a - | VarKey of Id.t - | RelKey of int type table_key = Constant.t puniverses tableKey @@ -162,7 +158,6 @@ val unfold_reference : clos_infos -> table_key -> fconstr option (* [mind_equiv] checks whether two inductive types are intentionally equal *) val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool -val eq_table_key : table_key -> table_key -> bool (************************************************************************) (*i This is for lazy debug *) diff --git a/checker/reduction.ml b/checker/reduction.ml index 072dec63f..4e508dc77 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Names open CErrors open Util open Cic @@ -297,6 +298,11 @@ let oracle_order infos l2r k1 k2 = if Int.equal n1 n2 then l2r else n1 < n2 +let eq_table_key univ = + Names.eq_table_key (fun (c1,u1) (c2,u2) -> + Constant.UserOrd.equal c1 c2 && + Univ.Instance.check_eq univ u1 u2) + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) @@ -343,7 +349,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = (* 2 constants, 2 local defined vars or 2 defined rels *) | (FFlex fl1, FFlex fl2) -> (try (* try first intensional equality *) - if eq_table_key fl1 fl2 + if eq_table_key univ fl1 fl2 then convert_stacks univ infos lft1 lft2 v1 v2 else raise NotConvertible with NotConvertible -> diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5cb38cb81..5c672d04a 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -303,7 +303,18 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = | Constant cb1 -> let cb1 = subst_const_body subst1 cb1 in let cb2 = subst_const_body subst2 cb2 in - (*Start by checking types*) + (*Start by checking universes *) + let env = + match cb1.const_universes, cb2.const_universes with + | Monomorphic_const _, Monomorphic_const _ -> env + | Polymorphic_const auctx1, Polymorphic_const auctx2 -> + check_polymorphic_instance error env auctx1 auctx2 + | Monomorphic_const _, Polymorphic_const _ -> + error () + | Polymorphic_const _, Monomorphic_const _ -> + error () + in + (* Now check types *) let typ1 = cb1.const_type in let typ2 = cb2.const_type in check_type env typ1 typ2; |