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/array/Array_checker.v | 112 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 97 insertions(+), 15 deletions(-) (limited to 'src/array/Array_checker.v') 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)). -- cgit