Extend constraint checking, and add casts for base of a vector shifts (i.e. from 0 to 32 etc, doesn't change order yet.).

1 files changed, 9 insertions, 1 deletions

diff --git a/src/test/pattern.sail b/src/test/pattern.sail
index bc04590d..7bbfebf9 100644
--- a/src/test/pattern.sail
+++ b/src/test/pattern.sail
@@ -3,6 +3,9 @@ register nat n
 register nat x
 register nat y
 
+typedef wordsize = forall Nat 'n, 'n IN {8,16,32}. [|'n|]
+let forall Nat 'n. (wordsize<'n>) word = 8
+
 function nat main _ = {
 
   (* works - x and y are set to 42 *)
@@ -14,7 +17,12 @@ function nat main _ = {
     case z -> { x := 99; x }
   }); 
 
-  (* doesn't work - main returns 1 instead of 99 *)
+  switch word {
+    case 8 -> { x:= 32; }
+    case 16 -> { x:= 64; }
+    case 32 -> { x:= 128; }
+  };
+
   n := 3;
   switch n {
     case 0 -> { 21 }