Check simple constraints (i.e. ones using only constants).

Changes syntax of tuple type from * to , so that nexps of the form 8 * 'n can be supported in the parser, which was apparently not true before.

4 files changed, 10 insertions, 10 deletions

diff --git a/src/test/regbits.sail b/src/test/regbits.sail
index 0a41280d..ed2a95e0 100644
--- a/src/test/regbits.sail
+++ b/src/test/regbits.sail
@@ -9,7 +9,7 @@ register (xer) XER
 register (bit) query
 
 function (bit[64]) main _ = {
-  XER := 0b010101010101010101010101010101010101010101010101010101010101001;
+  XER := 0b0101010101010101010101010101010101010101010101010101010101010010;
   f := XER;
   (bit[7]) foo := XER[57..63];
   query := XER.SO;
diff --git a/src/test/test1.sail b/src/test/test1.sail
index 0050a257..64722089 100644
--- a/src/test/test1.sail
+++ b/src/test/test1.sail
@@ -2,8 +2,8 @@ default Nat 'i
 default Order 'o
 default bool b
 default forall 'a. list<'a> b
-val forall 'a, 'b . ('a * 'b) -> 'b effect pure snd
-val forall Type 'i, 'b. ('i * 'b) -> 'i effect pure fst
+val forall 'a, 'b . ('a, 'b) -> 'b effect pure snd
+val forall Type 'i, 'b. ('i, 'b) -> 'i effect pure fst
 typedef int_list [name = "il"] = list<nat>
 typedef reco = const struct forall 'i, 'a, 'b. { 'a['i] v; 'b w; }
 typedef maybe = const union forall 'a. { Nne; 'a Sme; }
@@ -23,10 +23,10 @@ function unit ignore(x) = ()
 scattered typedef ast = const union
 scattered function ast f
 
-union ast member  bit * bit * bit A
+union ast member  (bit, bit, bit) A
 function clause f (  A (a,b,c) ) = C(a)
 
-union ast member  bit * bit B
+union ast member  (bit, bit) B
 function clause f (  B (a,b) ) = C(a)
 
 union ast member  bit C
diff --git a/src/test/test3.sail b/src/test/test3.sail
index 778d323a..78d60513 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -6,7 +6,7 @@ register (bit[8]) dummy_reg2
    memory-writing functions are figured out syntactically. *)
 val extern nat -> nat effect { wmem , rmem }  MEM
 val extern nat -> nat effect { wmem , rmem }  MEM_GPU
-val extern ( nat * nat ) -> (bit[8]) effect { wmem , rmem }  MEM_SIZE
+val extern forall Nat 'n . ( nat, [|'n|] ) -> (bit['n * 8]) effect { wmem , rmem }  MEM_SIZE
 val extern nat -> (bit[8]) effect { wmem , rmem }  MEM_WORD
 
 (* XXX types are wrong *)
@@ -18,8 +18,8 @@ val extern forall Type 'a . nat -> 'a effect pure to_vec_dec = "to_vec_dec"
 function unit ignore(x) = ()
 
 (* extern functions *)
-val extern ( nat * nat ) -> nat effect pure add = "add"
-val extern ( nat * nat ) -> nat effect pure (deinfix + ) = "add"   (* infix plus *)
+val extern ( nat, nat ) -> nat effect pure add = "add"
+val extern ( nat, nat ) -> nat effect pure (deinfix + ) = "add"   (* infix plus *)
 
 function nat (deinfix * ) ( (nat) x, (nat) y ) = 42
 
diff --git a/src/test/vectors.sail b/src/test/vectors.sail
index f1af224b..de610a39 100644
--- a/src/test/vectors.sail
+++ b/src/test/vectors.sail
@@ -1,6 +1,6 @@
-let (bit[32]) v = 0b101
+let (bit[3]) v = 0b101
 let (bit[4]) v2 = [0,1,0,0]
-register (bit[32]) i
+register (bit[4]) i
 
 let (bit[10]) v3 = 0b0101010111
 register (bit[10]) slice_check