Merge branch 'sail2' into smt_experiments

11 files changed, 94 insertions, 16 deletions

diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index c2c15c12..acadd4e2 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -2,7 +2,7 @@ Type error:
 [Replicate/v2.sail]:13:4-30
 13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | 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)))
+   | Tried performing type coercion from {('ex119# : Int), true. vector(('M * 'ex119#), 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/complex_exist_sat/v1.expect b/test/typecheck/pass/complex_exist_sat/v1.expect
index b1937f47..4090165a 100644
--- a/test/typecheck/pass/complex_exist_sat/v1.expect
+++ b/test/typecheck/pass/complex_exist_sat/v1.expect
@@ -4,5 +4,5 @@ Type error:
   |                  ^
   | Tried performing type coercion from int(3) to {('q : Int), 'q in {0, 1}. int((2 * 'q))} on 3
   | Coercion failed because:
-  | Constraint 3 == (2 * 'ex1#) is not satisfiable
+  | Constraint 3 == (2 * 'ex2#) is not satisfiable
   | 
diff --git a/test/typecheck/pass/existential_ast/v3.expect b/test/typecheck/pass/existential_ast/v3.expect
index 7bbd59ad..7bb8a4ab 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('ex195#)
+   | * datasize('ex196#)
    | 
diff --git a/test/typecheck/pass/existential_ast3/v1.expect b/test/typecheck/pass/existential_ast3/v1.expect
index 24b927a5..4b9bd7cc 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('ex157#)) is not a subtype of (int('ex152#), int('ex153#))
+   | (int(33), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex152# 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));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex154# bound here
    | [existential_ast3/v1.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (33, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex157# bound here
+   |    | 'ex158# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v2.expect b/test/typecheck/pass/existential_ast3/v2.expect
index a2c08583..52eb2f13 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('ex157#)) is not a subtype of (int('ex152#), int('ex153#))
+   | (int(31), int('ex158#)) is not a subtype of (int('ex153#), int('ex154#))
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex152# 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));
    |    |                                                ^---------------^
-   |    | 'ex153# bound here
+   |    | 'ex154# bound here
    | [existential_ast3/v2.sail]:17:48-65
    | 17 |    if b == 0b0 then (64, unsigned(b @ a)) else (31, unsigned(a));
    |    |                                                ^---------------^
-   |    | 'ex157# bound here
+   |    | 'ex158# bound here
    | 
diff --git a/test/typecheck/pass/existential_ast3/v3.expect b/test/typecheck/pass/existential_ast3/v3.expect
index cf86b765..0e43cd52 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 <= 'ex196# & ('ex196# + 1) <= 64))
+   | * (datasize(64) & (0 <= 'ex197# & ('ex197# + 1) <= 64))
    | 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 80526204..011ecbdf 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 <= 'ex114# & ('ex114# + 1) <= 3)
+   |    * (0 <= 'ex115# & ('ex115# + 1) <= 3)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex117# & ('ex117# + 1) <= 3)
+   |    * (0 <= 'ex118# & ('ex118# + 1) <= 3)
    | 
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 0b705b50..9a34f688 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 <= 'ex114# & ('ex114# + 1) <= 4)
+   |    * (0 <= 'ex115# & ('ex115# + 1) <= 4)
    | * plain_vector_access
    |    Could not resolve quantifiers for plain_vector_access
-   |    * (0 <= 'ex117# & ('ex117# + 1) <= 4)
+   |    * (0 <= 'ex118# & ('ex118# + 1) <= 4)
    | 
diff --git a/test/typecheck/pass/short_circuit_bool_ex.sail b/test/typecheck/pass/short_circuit_bool_ex.sail
new file mode 100644
index 00000000..5cfdc1dc
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex.sail
@@ -0,0 +1,36 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+
+val assertive : forall 'n. int('n) -> range(0,'n) effect {escape}
+
+function assertive(n) = {
+  assert(n > 0);
+  0
+}
+
+val ok : unit -> bool(0 == 1) effect {escape}
+
+function ok() = {
+  let n = -1;
+  let a = assertive(n) > 0 in
+  if (true | a) then true else true
+}
+
+/*
+val bad : unit -> bool(0 == 1) effect {escape}
+
+function bad() = {
+  let n = -1;
+  if (true | assertive(n) > 0) then true else true
+}
+*/
+
+val main : unit -> unit effect {escape}
+
+function main() =
+  if ok() then
+    print_endline("0 = 1")
+  else
+    print_endline("0 != 1")
\ No newline at end of file
diff --git a/test/typecheck/pass/short_circuit_bool_ex/v1.expect b/test/typecheck/pass/short_circuit_bool_ex/v1.expect
new file mode 100644
index 00000000..fc98db1b
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex/v1.expect
@@ -0,0 +1,8 @@
+Type error:
+[short_circuit_bool_ex/v1.sail]:25:36-40
+25 |  if (true | assertive(n) > 0) then true else true
+   |                                    ^--^
+   | Tried performing type coercion from bool(true) to bool(0 == 1) on true
+   | Coercion failed because:
+   | Mismatched argument types in subtype check
+   | 
diff --git a/test/typecheck/pass/short_circuit_bool_ex/v1.sail b/test/typecheck/pass/short_circuit_bool_ex/v1.sail
new file mode 100644
index 00000000..2faf12af
--- /dev/null
+++ b/test/typecheck/pass/short_circuit_bool_ex/v1.sail
@@ -0,0 +1,34 @@
+default Order dec
+
+$include <prelude.sail>
+$include <string.sail>
+
+val assertive : forall 'n. int('n) -> range(0,'n) effect {escape}
+
+function assertive(n) = {
+  assert(n > 0);
+  0
+}
+
+val ok : unit -> bool(0 == 1) effect {escape}
+
+function ok() = {
+  let n = -1;
+  let a = assertive(n) > 0 in
+  if (true | a) then true else true
+}
+
+val bad : unit -> bool(0 == 1) effect {escape}
+
+function bad() = {
+  let n = -1;
+  if (true | assertive(n) > 0) then true else true
+}
+
+val main : unit -> unit effect {escape}
+
+function main() =
+  if bad() then
+    print_endline("0 = 1")
+  else
+    print_endline("0 != 1")
\ No newline at end of file