Cmov Tsingle

3 files changed, 43 insertions, 33 deletions

diff --git a/riscV/ExtValues.v b/riscV/ExtValues.v
index aebbe5c5..edf359ef 100644
--- a/riscV/ExtValues.v
+++ b/riscV/ExtValues.v
@@ -111,3 +111,13 @@ Proof.
   f_equal.
   apply Float.of_to_bits.
 Qed.
+
+Lemma single_bits_normalize:
+  forall v1,
+  ExtValues.single_of_bits (Val.normalize (ExtValues.bits_of_single v1) AST.Tint) =
+  Val.normalize v1 AST.Tsingle.
+Proof.
+  destruct v1; cbn; trivial.
+  f_equal.
+  apply Float32.of_to_bits.
+Qed.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index b6720e40..bc169006 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -433,6 +433,13 @@ Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr)
                        ((Eop (Ocmp cond) args) :::
 		         (Eop Obits_of_float (e1 ::: Enil)) :::
 			 (Eop Obits_of_float (e2 ::: Enil)) ::: Enil)) ::: Enil))
+      | Tsingle => Some
+         (Eop Osingle_of_bits
+           ((Eop Olowlong ((Eop Oselectl
+             ((Eop (Ocmp cond) args) :::
+         (Eop Ocast32signed ((Eop Obits_of_single (e1 ::: Enil)) ::: Enil)) :::
+	 (Eop Ocast32signed ((Eop Obits_of_single (e2 ::: Enil)) ::: Enil))
+	 ::: Enil)) ::: Enil)) ::: Enil))
       | _ => None
       end
       else None.
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index c313fbaf..1fe4e662 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -943,50 +943,43 @@ Proof.
   destruct Archi.ptr64 eqn:PTR64.
   2: discriminate.
   destruct ty; cbn in *; try discriminate.
-  - inv H. TrivialExists.
-    + cbn. constructor.
-      { econstructor.
-        { constructor.
-          { econstructor. eassumption. cbn. rewrite H3. reflexivity. }
-          constructor. econstructor. constructor. eassumption.
-          constructor. cbn. reflexivity.
-          constructor. econstructor. constructor. eassumption. constructor.
-          cbn. reflexivity. constructor.
-        }
-        constructor.
-      }
-      constructor.
+  - (* Tint *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
     + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      destruct b.
+      rewrite H3. destruct b.
       * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
       * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
-  - inv H. TrivialExists.
-    + cbn. constructor.
-      { econstructor.
-        { constructor.
-          { econstructor. eassumption. cbn. rewrite H3. reflexivity. }
-          constructor. econstructor. constructor. eassumption.
-          constructor. cbn. reflexivity.
-          constructor. econstructor. constructor. eassumption. constructor.
-          cbn. reflexivity. constructor.
-        }
-        constructor.
-      }
-      constructor.
+        
+  - (* Tfloat *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
     + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      destruct b.
+      rewrite H3. destruct b.
       * rewrite ExtValues.select01_long_true.
         apply ExtValues.float_bits_normalize.
       * rewrite ExtValues.select01_long_false.
         apply ExtValues.float_bits_normalize.
-  - inv H. TrivialExists.
-    + cbn. constructor.
-      { econstructor. eassumption. cbn. rewrite H3. cbn. reflexivity. }
-      constructor. eassumption. constructor. eassumption. constructor.
+
+  - (* Tlong *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
     + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      destruct b.
+      rewrite H3. destruct b.
       * rewrite ExtValues.select01_long_true. reflexivity.
       * rewrite ExtValues.select01_long_false. reflexivity.
+
+  - (* Tsingle *)
+    inv H. TrivialExists.
+    + cbn. repeat econstructor; eassumption.
+    + cbn. f_equal. rewrite ExtValues.normalize_select01.
+      rewrite H3. destruct b.
+      * rewrite ExtValues.select01_long_true.
+        rewrite normalize_low_long by assumption.
+        apply ExtValues.single_bits_normalize.
+      * rewrite ExtValues.select01_long_false.
+        rewrite normalize_low_long by assumption.
+        apply ExtValues.single_bits_normalize.
 Qed.
 
 Theorem eval_addressing: