diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-06-02 18:36:25 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-06-02 18:36:25 +0200 |
commit | 2c3b041073910c7d84d7995992e014e56aaed1fb (patch) | |
tree | e8d2f41ab1dd81ac715e814b10645df37de328d9 /src/array/Array_checker.v | |
parent | 92f2a211fb112fef44f7b5b86fc70a2e5a9e639b (diff) | |
parent | 6a209bbc1bf5c90adb5f576093129fc62ce84780 (diff) | |
download | smtcoq-2c3b041073910c7d84d7995992e014e56aaed1fb.tar.gz smtcoq-2c3b041073910c7d84d7995992e014e56aaed1fb.zip |
Merge remote-tracking branch 'remotes/origin/coq-8.10' into coq-8.11
Diffstat (limited to 'src/array/Array_checker.v')
-rw-r--r-- | src/array/Array_checker.v | 112 |
1 files changed, 97 insertions, 15 deletions
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)). |