Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13

1 files changed, 44 insertions, 60 deletions

diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index aac66be..56ac458 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -275,14 +275,18 @@ Module Typ.
     Fixpoint interp_compdec_aux (t:type) : {ty: Type & CompDec ty} :=
       match t with
       | TFArray ti te =>
+        let iti := interp_compdec_aux ti in
+        let ite := interp_compdec_aux te in
+        let cti := projT2 iti in
+        let cte := projT2 ite in
+        let tti := type_compdec cti in
+        let tte := type_compdec cte in
         existT (fun ty : Type => CompDec ty)
-               (@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
-                  (type_compdec (projT2 (interp_compdec_aux ti)))
-                  (type_compdec (projT2 (interp_compdec_aux te))))
+               (@farray tti
+                        tte
+                        (@ord_of_compdec tti cti)
+                        (@inh_of_compdec tte cte))
+               (FArray_compdec tti tte)
       | Tindex i =>
         existT (fun ty : Type => CompDec ty)
                (te_carrier (t_i .[of_Z (Z.of_N i)])) (te_compdec (t_i .[of_Z (Z.of_N i)]))
@@ -292,10 +296,10 @@ Module Typ.
       | TBV n => existT (fun ty : Type => CompDec ty) (BITVECTOR_LIST.bitvector n) (BV_compdec n)
       end.
 
-    Definition interp_compdec (t:type) : CompDec (projT1 (interp_compdec_aux t)) :=
-      projT2 (interp_compdec_aux t).
+    Definition interp (t:type) : Type := type_compdec (projT2 (interp_compdec_aux t)).
 
-    Definition interp (t:type) : Type := type_compdec (interp_compdec t).
+    Definition interp_compdec (t:type) : CompDec (interp t) :=
+      projT2 (interp_compdec_aux t).
 
 
     Definition interp_ftype (t:ftype) :=
@@ -303,40 +307,17 @@ Module Typ.
       (interp (snd t)) (fst t).
 
 
-    Definition dec_interp (t:type) : DecType (interp t).
-    Proof.
-      unfold interp.
-      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 t) as [x c]. simpl.
-      apply Ordered.
-    Defined.
-
-    Instance comp_interp (t:type) : Comparable (interp t).
-    Proof.
-      unfold interp, ord_interp.
-      destruct (interp_compdec t) as [x c]. simpl.
-      apply Comp.
-    Defined.
-
-
-    Definition inh_interp (t:type) : Inhabited (interp t).
-      unfold interp.
-      destruct (interp_compdec t).
-      apply Inh.
-    Defined.
+    Global Instance dec_interp (t:type) : DecType (interp t) :=
+      (@EqbToDecType _ (@eqbtype_of_compdec (interp t) (interp_compdec t))).
 
-    Definition inhabitant_interp (t:type) : interp t := @default_value _ (inh_interp _).
+    Global Instance ord_interp (t:type) : OrdType (interp t) :=
+      @ord_of_compdec (interp t) (interp_compdec t).
 
+    Global Instance comp_interp (t:type) : Comparable (interp t) :=
+      @comp_of_compdec (interp t) (interp_compdec t).
 
-    Hint Resolve
-         dec_interp comp_interp ord_interp
-         inh_interp interp_compdec : typeclass_instances.
+    Global Instance inh_interp (t:type) : Inhabited (interp t) :=
+      @inh_of_compdec (interp t) (interp_compdec t).
 
 
     (* Boolean equality over interpretation of a btype *)
@@ -1525,13 +1506,25 @@ Qed.
            apply_binop (Typ.TBV s) (Typ.TBV s) (Typ.TBV s) (@BITVECTOR_LIST.bv_shr s)
          | BO_select ti te => apply_binop (Typ.TFArray ti te) ti te FArray.select
          | BO_diffarray ti te =>
-           apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te))
+           let iti := Typ.interp_compdec_aux t_i ti in
+           let ite := Typ.interp_compdec_aux t_i te in
+           let cti := projT2 iti in
+           let cte := projT2 ite in
+           let tti := type_compdec cti in
+           let tte := type_compdec cte in
+           apply_binop (Typ.TFArray ti te) (Typ.TFArray ti te) ti (@FArray.diff tti tte (@EqbToDecType _ (@eqbtype_of_compdec tti cti)) (@ord_of_compdec tti cti) (@comp_of_compdec tti cti) (@EqbToDecType _ (@eqbtype_of_compdec tte cte)) (@ord_of_compdec tte cte) (@comp_of_compdec tte cte) (@inh_of_compdec tti cti) (@inh_of_compdec tte cte))
          end.
 
       Definition interp_top o :=
          match o with
          | TO_store ti te =>
-           apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te) (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti))) (ord_of_compdec _) _ (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i te))
+           let iti := Typ.interp_compdec_aux t_i ti in
+           let ite := Typ.interp_compdec_aux t_i te in
+           let cti := projT2 iti in
+           let cte := projT2 ite in
+           let tti := type_compdec cti in
+           let tte := type_compdec cte in
+           apply_terop (Typ.TFArray ti te) ti te (Typ.TFArray ti te) (@FArray.store tti tte (@EqbToDecType _ (@eqbtype_of_compdec tti cti)) (@ord_of_compdec tti cti) (@comp_of_compdec tti cti) (@ord_of_compdec tte cte) (@comp_of_compdec tte cte) (@inh_of_compdec tte cte))
          end.
 
       Fixpoint compute_interp ty acc l :=
@@ -1966,9 +1959,9 @@ Qed.
         rewrite !Typ.cast_refl.
         intros.
         exists ((@FArray.diff (Typ.interp t_i t') (Typ.interp t_i te)
-             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i t')))
-             (ord_of_compdec _)
-             (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te)
+             (Typ.dec_interp t_i t')
+             (Typ.ord_interp t_i t')
+             (Typ.comp_interp t_i t') (Typ.dec_interp t_i te) (Typ.ord_interp t_i te)
              (Typ.comp_interp t_i te) (Typ.inh_interp t_i t') (Typ.inh_interp t_i te) x1 x2)); auto.
 
         (* Ternary operatores *)
@@ -1990,11 +1983,7 @@ Qed.
         intros.
         rewrite !Typ.cast_refl.
         intros.
-        exists ((@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te')
-             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti')))
-             (ord_of_compdec _)
-             (comp_of_compdec _) (Typ.ord_interp t_i te') (Typ.comp_interp t_i te')
-             (Typ.inh_interp t_i te') x1 x2 x3)); auto.
+        exists (@FArray.store (Typ.interp t_i ti') (Typ.interp t_i te') (Typ.dec_interp t_i ti') (Typ.ord_interp t_i ti') (Typ.comp_interp t_i ti') (Typ.ord_interp t_i te') (Typ.comp_interp t_i te') (Typ.inh_interp t_i te') x1 x2 x3); auto.
 
         (* N-ary operators *)
         destruct op as [A]; simpl; intros [ | | | | | ]; try discriminate; simpl; intros _; case (compute_interp A nil ha).
@@ -2475,12 +2464,7 @@ Qed.
           simpl; try (exists true; auto); intro k1;
             case (Typ.cast (v_type Typ.type interp_t (a .[ h2])) (Typ.TFArray ti te)) as [k2| ];
             simpl; try (exists true; reflexivity).
-        exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te)
-             (@EqbToDecType _ (@eqbtype_of_compdec _(Typ.interp_compdec t_i ti)))
-             (ord_of_compdec _)
-             (comp_of_compdec _) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te)
-             (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te)
-             (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto.
+        exists ((@FArray.diff (Typ.interp t_i ti) (Typ.interp t_i te) (Typ.dec_interp t_i ti) (Typ.ord_interp t_i ti) (Typ.comp_interp t_i ti) (Typ.dec_interp t_i te) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te) (Typ.inh_interp t_i ti) (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y))); auto.
 
         (* Ternary operators *)
         intros [ti te] h1 h2 h3; simpl; rewrite !andb_true_iff; intros [[H1 H2] H3];
@@ -2494,9 +2478,9 @@ Qed.
             case (Typ.cast (v_type Typ.type interp_t (a .[ h3])) te) as [k3| ];
             simpl; try (exists true; reflexivity).
          exists (@FArray.store (Typ.interp t_i ti) (Typ.interp t_i te)
-             (@EqbToDecType _ (@eqbtype_of_compdec _ (Typ.interp_compdec t_i ti)))
-             (ord_of_compdec _)
-             (comp_of_compdec _) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te)
+             (Typ.dec_interp t_i ti)
+             (Typ.ord_interp t_i ti)
+             (Typ.comp_interp t_i ti) (Typ.ord_interp t_i te) (Typ.comp_interp t_i te)
              (Typ.inh_interp t_i te) (k1 (Typ.interp t_i) x) (k2 (Typ.interp t_i) y)
              (k3 (Typ.interp t_i) z)); auto.