introduce if_opt_bool_val.

1 files changed, 12 insertions, 7 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 193941aa..2d0eeb11 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -1229,14 +1229,16 @@ Definition arith_eval_p (i : arith_p) : val :=
   | Pfmovimmd f => Vfloat f
   end.
 
+Definition if_opt_bool_val (c: option bool) v1 v2: val :=
+   match c with
+   | Some true => v1
+   | Some false =>  v2
+   | None => Vundef
+   end.
+
 Definition arith_eval_c_p (i : arith_c_p) (c : option bool) : val :=
   match i with
-  | Pcset =>
-    (match c with
-    | Some true => Vint Int.one
-    | Some false =>  Vint Int.zero
-    | None => Vundef
-    end)
+  | Pcset => if_opt_bool_val c (Vint Int.one) (Vint Int.zero)
   end.
 
 Definition arith_eval_pp i v :=
@@ -1311,8 +1313,10 @@ Definition arith_eval_ppp i v1 v2 :=
   end.
 
 Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) :=
+  if_opt_bool_val c v1 v2.
+ (*
   match i with
-  | Pcsel =>
+  | Pcsel => 
     (match c with
     | Some true => v1
     | Some false => v2
@@ -1325,6 +1329,7 @@ Definition arith_eval_c_ppp (i : arith_c_ppp) (v1 v2 : val) (c : option bool) :=
     | None => Vundef
     end)
   end.
+ *)
 
 Definition arith_rr0r_isize (i: arith_rr0r) :=
   match i with