Merge branch 'sail2' into rmem_interpreter

17 files changed, 85 insertions, 21 deletions

diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail
index 03954a9f..291b7e16 100644
--- a/test/typecheck/pass/Replicate.sail
+++ b/test/typecheck/pass/Replicate.sail
@@ -3,6 +3,9 @@ default Order dec
 $include <smt.sail>
 $include <prelude.sail>
 
+overload operator / = {ediv_int}
+overload operator % = {emod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
index 92c6d7cd..c40aa5ec 100644
--- a/test/typecheck/pass/Replicate/v1.expect
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -1,8 +1,8 @@
 Type error:
-[Replicate/v1.sail]:11:4-30
-11 |    replicate_bits(x, 'N / 'M)
+[Replicate/v1.sail]:14:4-30
+14 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail
index 69f2bb6f..55627db5 100644
--- a/test/typecheck/pass/Replicate/v1.sail
+++ b/test/typecheck/pass/Replicate/v1.sail
@@ -3,6 +3,9 @@ default Order dec
 $include <smt.sail>
 $include <prelude.sail>
 
+overload operator / = {ediv_int}
+overload operator % = {emod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 0.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index 62992f2c..c2c15c12 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -1,8 +1,8 @@
 Type error:
-[Replicate/v2.sail]:10:4-30
-10 |    replicate_bits(x, 'N / 'M)
+[Replicate/v2.sail]:13:4-30
+13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex80# : Int), true. vector(('M * 'ex80#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail
index e54b0af4..436ef24b 100644
--- a/test/typecheck/pass/Replicate/v2.sail
+++ b/test/typecheck/pass/Replicate/v2.sail
@@ -2,6 +2,9 @@ default Order dec
 
 $include <prelude.sail>
 
+overload operator / = {tdiv_int}
+overload operator % = {tmod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/anon_rec.sail b/test/typecheck/pass/anon_rec.sail
new file mode 100644
index 00000000..17dd1e07
--- /dev/null
+++ b/test/typecheck/pass/anon_rec.sail
@@ -0,0 +1,12 @@
+default Order dec
+
+union Foo ('a : Type) = {
+  MkFoo : { field1 : 'a, field2 : int }
+}
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  let _: Foo(unit) = MkFoo(struct { field1 = (), field2 = 22 });
+  print_endline("ok")
+}
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index af2cf65f..7bbd59ad 100644
--- a/test/typecheck/pass/existential_ast/v3.expect
+++ b/test/typecheck/pass/existential_ast/v3.expect
@@ -3,5 +3,5 @@ Type error:
 26 |  Some(Ctor1(a, x, c))
    |       ^------------^
    | Could not resolve quantifiers for Ctor1
-   | * datasize('ex157#)
+   | * datasize('ex195#)
    | 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index e904aa61..24b927a5 100644
--- a/test/typecheck/pass/existential_ast3/v1.expect
+++ b/test/typecheck/pass/existential_ast3/v1.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(33), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (33, unsigned(a))
    | Coercion failed because:
-   | (int(33), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))
+   | (int(33), int('ex157#)) is not a subtype of (int('ex152#), int('ex153#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex114# bound here
+   |    | 'ex152# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex115# bound here
+   |    | 'ex153# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex119# bound here
+   |    | 'ex157# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index fdd13607..a2c08583 100644
--- a/test/typecheck/pass/existential_ast3/v2.expect
+++ b/test/typecheck/pass/existential_ast3/v2.expect
@@ -4,17 +4,17 @@ Type error:
    |                                                ^---------------^
    | Tried performing type coercion from (int(31), range(0, (2 ^ 5 - 1))) to {('d : Int) ('n : Int), (datasize('d) & (0 <= 'n & ('n + 1) <= 'd)). (int('d), int('n))} on (31, unsigned(a))
    | Coercion failed because:
-   | (int(31), int('ex119#)) is not a subtype of (int('ex114#), int('ex115#))
+   | (int(31), int('ex157#)) is not a subtype of (int('ex152#), int('ex153#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex114# bound here
+   |    | 'ex152# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex115# bound here
+   |    | 'ex153# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex119# bound here
+   |    | 'ex157# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index 2432e632..cf86b765 100644
--- a/test/typecheck/pass/existential_ast3/v3.expect
+++ b/test/typecheck/pass/existential_ast3/v3.expect
@@ -3,5 +3,5 @@ Type error:
 25 |    Some(Ctor(64, unsigned(0b0 @ b @ a)))
    |         ^-----------------------------^
    | Could not resolve quantifiers for Ctor
-   | * (datasize(64) & (0 <= 'ex158# & ('ex158# + 1) <= 64))
+   | * (datasize(64) & (0 <= 'ex196# & ('ex196# + 1) <= 64))
    | 
diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail
index 4aac2bed..594130a8 100644
--- a/test/typecheck/pass/guards.sail
+++ b/test/typecheck/pass/guards.sail
@@ -1,8 +1,9 @@
 default Order dec
 
 $include <prelude.sail>
+$include <smt.sail>
 
-overload operator / = {quotient}
+overload operator / = {ediv_int}
 
 union T = {C1 : int, C2 : int}
 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index a63f28f1..80526204 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -5,8 +5,8 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex76# & ('ex76# + 1) <= 3)
+   |    * (0 <= 'ex114# & ('ex114# + 1) <= 3)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex79# & ('ex79# + 1) <= 3)
+   |    * (0 <= 'ex117# & ('ex117# + 1) <= 3)
    | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index f37d215f..0b705b50 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -5,8 +5,8 @@ Type error:
    | No overloading for vector_access, tried:
    | * bitvector_access
    |    Could not resolve quantifiers for bitvector_access
-   |    * (0 <= 'ex76# & ('ex76# + 1) <= 4)
+   |    * (0 <= 'ex114# & ('ex114# + 1) <= 4)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex79# & ('ex79# + 1) <= 4)
+   |    * (0 <= 'ex117# & ('ex117# + 1) <= 4)
    | 
diff --git a/test/typecheck/pass/recursion.sail b/test/typecheck/pass/recursion.sail
index 5ca85f53..cd3ca46c 100644
--- a/test/typecheck/pass/recursion.sail
+++ b/test/typecheck/pass/recursion.sail
@@ -2,6 +2,8 @@ default Order dec
 
 $include <prelude.sail>
 
+overload operator / = {tdiv_int}
+
 val log2 : int -> int
 
 function log2(n) =
diff --git a/test/typecheck/pass/shadow_let.sail b/test/typecheck/pass/shadow_let.sail
new file mode 100644
index 00000000..8a30744c
--- /dev/null
+++ b/test/typecheck/pass/shadow_let.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+register R : int
+
+val foo : int(1) -> unit
+val bar : int(2) -> unit
+
+function main((): unit) -> unit = {
+  let 'x : {'z, 'z == 1. int('z)} = 1;
+  let 'y = x;
+  foo(x);
+  let 'x : {'z, 'z == 2. int('z)} = 2;
+  foo(y);
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/shadow_let/v1.expect b/test/typecheck/pass/shadow_let/v1.expect
new file mode 100644
index 00000000..3cd21dc0
--- /dev/null
+++ b/test/typecheck/pass/shadow_let/v1.expect
@@ -0,0 +1,12 @@
+Type error:
+[shadow_let/v1.sail]:13:6-7
+13 |  bar(y);
+   |      ^
+   | Tried performing type coercion from int('_x#1) to int(2) on y
+   | Coercion failed because:
+   | int('_x#1) is not a subtype of int(2)
+   | [shadow_let/v1.sail]:9:6-8
+   | 9 |  let 'x : {'z, 'z == 1. int('z)} = 1;
+   |   |      ^^
+   |   | '_x#1 bound here
+   | 
diff --git a/test/typecheck/pass/shadow_let/v1.sail b/test/typecheck/pass/shadow_let/v1.sail
new file mode 100644
index 00000000..d7dc20a5
--- /dev/null
+++ b/test/typecheck/pass/shadow_let/v1.sail
@@ -0,0 +1,14 @@
+default Order dec
+
+register R : int
+
+val foo : int(1) -> unit
+val bar : int(2) -> unit
+
+function main((): unit) -> unit = {
+  let 'x : {'z, 'z == 1. int('z)} = 1;
+  let 'y = x;
+  foo(x);
+  let 'x : {'z, 'z == 2. int('z)} = 2;
+  bar(y);
+}
\ No newline at end of file