From f2fa48b95a789fdeca777ea1cb932a3657faeed3 Mon Sep 17 00:00:00 2001
From: Gabriel Kerneis
Date: Wed, 11 Jun 2014 17:46:41 +0100
Subject: power.sail: store mode64bit in a bool register

This is now possible because we handle coercions better.
---
 src/test/power.sail   | 5 +----
 src/test/run_power.ml | 1 +
 2 files changed, 2 insertions(+), 4 deletions(-)

(limited to 'src/test')

diff --git a/src/test/power.sail b/src/test/power.sail
index 6fe84602..a9e56c7f 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -1,5 +1,3 @@
-(* XXX sign extension --- note that this produces a signed integer,
-   the constraints on the range of the result is TODO *)
 val extern forall Nat 'n. bit['n] -> bit[64] effect pure exts
 (* XXX binary coded decimal *)
 function forall Type 'a . 'a dec_to_bcd ( x ) = x
@@ -99,8 +97,7 @@ val extern forall Nat 'n. ( nat , [|'n|] ) -> (bit[8 * 'n]) effect { wmem , rmem
 (* XXX effect for trap? *)
 val extern unit -> unit effect pure trap
 
-(* XXX should be register<bool>, this is a workaround for limitations in coercions *)
-let (bit) mode64bit = bitone
+register (bool) mode64bit
 
 scattered function unit execute
 scattered typedef ast = const union
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index ca4dbc97..61f60ef3 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -74,6 +74,7 @@ let init_reg () =
     init "CTR" Big_int.zero_big_int 64;
     init "CR" Big_int.zero_big_int 32;
     init "LR" lr_init_value 64;
+    Id_aux(Id "mode64bit", Unknown), V_lit (L_aux (L_true, Unknown));
   ]
 ;;
 
-- 
cgit v1.2.3