From efb1a48817405c6ad894d2088077f70c3d7eb15b Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 2 Jun 2021 18:31:06 +0200 Subject: Type back in CompDec (for efficiency reasons) --- src/SMT_terms.v | 18 ++++---- src/array/Array_checker.v | 112 +++++++++++++++++++++++++++++++++++++++------- src/classes/SMT_classes.v | 19 ++++---- 3 files changed, 117 insertions(+), 32 deletions(-) diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 33aca50..dc5063f 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -274,13 +274,13 @@ Module Typ. match t with | TFArray ti te => existT (fun ty : Type => CompDec ty) - (@farray (projT1 (interp_compdec_aux ti)) - (projT1 (interp_compdec_aux te)) + (@farray (type_compdec (projT2 (interp_compdec_aux ti))) + (type_compdec (projT2 (interp_compdec_aux te))) (@ord_of_compdec _ (projT2 (interp_compdec_aux ti))) (@inh_of_compdec _ (projT2 (interp_compdec_aux te)))) (FArray_compdec - (projT1 (interp_compdec_aux ti)) - (projT1 (interp_compdec_aux te))) + (type_compdec (projT2 (interp_compdec_aux ti))) + (type_compdec (projT2 (interp_compdec_aux te)))) | Tindex i => existT (fun ty : Type => CompDec ty) (te_carrier (t_i .[ i])) (te_compdec (t_i .[ i])) @@ -293,7 +293,7 @@ Module Typ. Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) := projT2 (interp_compdec_aux t). - Definition interp (t:type) : Type := projT1 (interp_compdec_aux t). + Definition interp (t:type) : Type := type_compdec (interp_compdec t). Definition interp_ftype (t:ftype) := @@ -304,21 +304,21 @@ Module Typ. Definition dec_interp (t:type) : DecType (interp t). Proof. unfold interp. - destruct (interp_compdec_aux t) as [x c]. simpl. + destruct (interp_compdec t) as [x c]. simpl. apply EqbToDecType. Defined. Instance ord_interp (t:type) : OrdType (interp t). Proof. unfold interp. - destruct (interp_compdec_aux t) as [x c]. simpl. + destruct (interp_compdec t) as [x c]. simpl. apply Ordered. Defined. Instance comp_interp (t:type) : Comparable (interp t). Proof. unfold interp, ord_interp. - destruct (interp_compdec_aux t) as [x c]. simpl. + destruct (interp_compdec t) as [x c]. simpl. apply Comp. Defined. @@ -349,7 +349,7 @@ Module Typ. eqb_of_compdec c x y = true <-> x = y. Proof. intros x y. - destruct c as [[E HE] O C I]. + destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE. Qed. diff --git a/src/array/Array_checker.v b/src/array/Array_checker.v index 7d8e994..de20723 100644 --- a/src/array/Array_checker.v +++ b/src/array/Array_checker.v @@ -1227,21 +1227,91 @@ Section certif. subst. specialize (Atom.Bval_inj2 t_i v_typed2' (v_vald2) (@diff (Typ.interp t_i v_typed2') (Typ.interp t_i v_typec1') (@EqbToDecType - _ + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2')) (@eqbtype_of_compdec - _ + (@projT1 Type (fun ty : Type => CompDec ty) + (Typ.interp_compdec_aux t_i v_typed2')) (Typ.interp_compdec t_i v_typed2'))) - _ + (@ord_of_compdec (Typ.interp t_i v_typed2') + (@projT2 Type (fun ty : Type => CompDec ty) + ((fix interp_compdec_aux (t : Typ.type) : + @sigT Type (fun ty : Type => CompDec ty) := + match t return (@sigT Type (fun ty : Type => CompDec ty)) with + | Typ.TFArray ti te => + @existT Type (fun ty : Type => CompDec ty) + (@farray + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti))) + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te))) + (@ord_of_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti))) + (@inh_of_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te)))) + (@SMT_classes_instances.FArray_compdec + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti))) + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te))) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te))) + | Typ.Tindex i => + @existT Type (fun ty : Type => CompDec ty) + (te_carrier (@get typ_compdec t_i i)) + (te_compdec (@get typ_compdec t_i i)) + | Typ.TZ => + @existT Type (fun ty : Type => CompDec ty) BinNums.Z + SMT_classes_instances.Z_compdec + | Typ.Tbool => + @existT Type (fun ty : Type => CompDec ty) bool + SMT_classes_instances.bool_compdec + | Typ.Tpositive => + @existT Type (fun ty : Type => CompDec ty) + BinNums.positive SMT_classes_instances.Positive_compdec + | Typ.TBV n => + @existT Type (fun ty : Type => CompDec ty) + (BVList.BITVECTOR_LIST.bitvector n) + (SMT_classes_instances.BV_compdec n) + end) v_typed2'))) (@comp_of_compdec (Typ.interp t_i v_typed2') - (projT2 + (@projT2 Type (fun ty : Type => CompDec ty) ((fix interp_compdec_aux (t : Typ.type) : @sigT Type (fun ty : Type => CompDec ty) := match t return (@sigT Type (fun ty : Type => CompDec ty)) with | Typ.TFArray ti te => @existT Type (fun ty : Type => CompDec ty) (@farray - (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) - (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te)) + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti))) + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te))) (@ord_of_compdec (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) @@ -1253,10 +1323,20 @@ Section certif. (@projT2 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te)))) (@SMT_classes_instances.FArray_compdec - (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) - (@projT1 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te)) - (@projT2 Type (fun ty : Type => CompDec ty) (interp_compdec_aux ti)) - (@projT2 Type (fun ty : Type => CompDec ty) (interp_compdec_aux te))) + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti))) + (@type_compdec + (@projT1 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te))) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux ti)) + (@projT2 Type (fun ty : Type => CompDec ty) + (interp_compdec_aux te))) | Typ.Tindex i => @existT Type (fun ty : Type => CompDec ty) (te_carrier (@get typ_compdec t_i i)) @@ -1268,14 +1348,16 @@ Section certif. @existT Type (fun ty : Type => CompDec ty) bool SMT_classes_instances.bool_compdec | Typ.Tpositive => - @existT Type (fun ty : Type => CompDec ty) BinNums.positive - SMT_classes_instances.Positive_compdec + @existT Type (fun ty : Type => CompDec ty) + BinNums.positive SMT_classes_instances.Positive_compdec | Typ.TBV n => @existT Type (fun ty : Type => CompDec ty) - (BVList.BITVECTOR_LIST.bitvector n) (SMT_classes_instances.BV_compdec n) + (BVList.BITVECTOR_LIST.bitvector n) + (SMT_classes_instances.BV_compdec n) end) v_typed2'))) (Typ.dec_interp t_i v_typec1') - _ (Typ.comp_interp t_i v_typec1') - (Typ.inh_interp t_i v_typed2') (Typ.inh_interp t_i v_typec1') v_valf1 v_valf2)). + (Typ.ord_interp t_i v_typec1') (Typ.comp_interp t_i v_typec1') + (Typ.inh_interp t_i v_typed2') (Typ.inh_interp t_i v_typec1') v_valf1 + v_valf2)). intros. specialize (H5 Htid2'''). rewrite <- H5. specialize (Atom.Bval_inj2 t_i v_typed2' (v_vale2) (v_vald2)). diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v index d314aa0..53d5dcc 100644 --- a/src/classes/SMT_classes.v +++ b/src/classes/SMT_classes.v @@ -148,27 +148,30 @@ Class Inhabited T := { (** * CompDec: Merging all previous classes *) Class CompDec T := { - Eqb :> EqbType T; (* This is redundant since implied by Comp, but it actually allows us to choose a specific equality function *) - Ordered :> OrdType T; - Comp :> @Comparable T Ordered; - Inh :> Inhabited T + ty := T; (* This is redundant for performance reasons *) + Eqb :> EqbType ty; (* This is redundant since implied by Comp, but it actually allows us to choose a specific equality function *) + Ordered :> OrdType ty; + Comp :> @Comparable ty Ordered; + Inh :> Inhabited ty }. Instance eqbtype_of_compdec t `{c: CompDec t} : (EqbType t) := - let (eqb, _, _, _) := c in eqb. + let (_, eqb, _, _, _) := c in eqb. Instance ord_of_compdec t `{c: CompDec t} : (OrdType t) := - let (_, ord, _, _) := c in ord. + let (_, _, ord, _, _) := c in ord. Instance inh_of_compdec t `{c: CompDec t} : (Inhabited t) := - let (_, _, _, inh) := c in inh. + let (_, _, _, _, inh) := c in inh. Instance comp_of_compdec t `{c: CompDec t} : @Comparable t (ord_of_compdec t). destruct c; trivial. Defined. +Definition type_compdec {ty:Type} (cd : CompDec ty) := ty. + Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool := match eqbtype_of_compdec t with | {| eqb := eqb |} => eqb @@ -178,7 +181,7 @@ Definition eqb_of_compdec {t} (c : CompDec t) : t -> t -> bool := Lemma compdec_eq_eqb {T:Type} {c : CompDec T} : forall x y : T, x = y <-> eqb_of_compdec c x y = true. Proof. - intros x y. destruct c as [[E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE. + intros x y. destruct c as [TY [E HE] O C I]. unfold eqb_of_compdec. simpl. now rewrite HE. Qed. Hint Resolve -- cgit