9 files changed, 52 insertions, 19 deletions

diff --git a/test/c/bool_bits_mapping.expect b/test/c/bool_bits_mapping.expect
new file mode 100644
index 00000000..79ebd086
--- /dev/null
+++ b/test/c/bool_bits_mapping.expect
@@ -0,0 +1,2 @@
+ok
+ok
diff --git a/test/c/bool_bits_mapping.sail b/test/c/bool_bits_mapping.sail
new file mode 100644
index 00000000..1a104186
--- /dev/null
+++ b/test/c/bool_bits_mapping.sail
@@ -0,0 +1,23 @@
+default Order dec
+
+$include <prelude.sail>
+
+mapping bool_bits : bool <-> bits(1) = {
+  true   <-> 0b1,
+  false  <-> 0b0
+}
+
+val "print_endline" : string -> unit
+
+function main((): unit) -> unit = {
+  if bool_bits(0b1) then {
+    print_endline("ok")
+  } else {
+    print_endline("fail")
+  };
+  if bool_bits(true) == 0b1 then {
+    print_endline("ok")
+  } else {
+    print_endline("fail")
+  }
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/bool_bits_mapping.sail b/test/typecheck/pass/bool_bits_mapping.sail
new file mode 100644
index 00000000..7fd2bae3
--- /dev/null
+++ b/test/typecheck/pass/bool_bits_mapping.sail
@@ -0,0 +1,8 @@
+default Order dec
+
+$include <prelude.sail>
+
+mapping bool_bits : bool <-> bits(1) = {
+  true   <-> 0b1,
+  false  <-> 0b0
+}
diff --git a/test/typecheck/pass/bool_constraint/v1.expect b/test/typecheck/pass/bool_constraint/v1.expect
index 2ce8f471..8b8e6b24 100644
--- a/test/typecheck/pass/bool_constraint/v1.expect
+++ b/test/typecheck/pass/bool_constraint/v1.expect
@@ -6,7 +6,7 @@ Tried performing type coercion from int(4) to {'m, ('b & 'm == 'n | not('b) & 'm
 Coercion failed because:
   int(4) is not a subtype of {('m : Int), (('b & 'm == 'n) | (not('b) & 'm == 3)). int('m)}
   in context
-  * 4 == 'ex44#m
+  * 4 == 'ex37#m
   * not('b)
   where
   * 'b bound at file "bool_constraint/v1.sail", line 11, character 1 to line 13, character 1
@@ -15,7 +15,7 @@ Coercion failed because:
   if b then n else 4
 }
 
-  * 'ex44#m bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
+  * 'ex37#m bound at file "bool_constraint/v1.sail", line 12, character 20 to line 12, character 20
 
   if b then n else 4
 
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
index 1b159c6c..986e82c0 100644
--- a/test/typecheck/pass/global_type_var/v1.expect
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -6,17 +6,17 @@ Tried performing type coercion from int(32) to int('size) on 32
 Coercion failed because:
   int(32) is not a subtype of int('size)
   in context
-  * 'size == 'ex11#
-  * ('ex11# == 32 | 'ex11# == 64)
+  * 'size == 'ex10#
   * ('ex10# == 32 | 'ex10# == 64)
+  * ('ex9# == 32 | 'ex9# == 64)
   where
-  * 'ex10# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
+  * 'ex10# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
 
-let (size as 'size) : {|32, 64|} = 32
+let (size as 'size) : {|32, 64|} = 32
 
-  * 'ex11# bound at file "global_type_var/v1.sail", line 5, character 6 to line 5, character 18
+  * 'ex9# bound at file "global_type_var/v1.sail", line 5, character 5 to line 5, character 32
 
-let (size as 'size) : {|32, 64|} = 32
+let (size as 'size) : {|32, 64|} = 32
 
   * 'size bound at file "global_type_var/v1.sail", line 5, character 14 to line 5, character 18
 
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
index 1fee46c8..f081d4af 100644
--- a/test/typecheck/pass/global_type_var/v2.expect
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -6,17 +6,17 @@ Tried performing type coercion from int(64) to int('size) on 64
 Coercion failed because:
   int(64) is not a subtype of int('size)
   in context
-  * 'size == 'ex11#
-  * ('ex11# == 32 | 'ex11# == 64)
+  * 'size == 'ex10#
   * ('ex10# == 32 | 'ex10# == 64)
+  * ('ex9# == 32 | 'ex9# == 64)
   where
-  * 'ex10# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
+  * 'ex10# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
 
-let (size as 'size) : {|32, 64|} = 32
+let (size as 'size) : {|32, 64|} = 32
 
-  * 'ex11# bound at file "global_type_var/v2.sail", line 5, character 6 to line 5, character 18
+  * 'ex9# bound at file "global_type_var/v2.sail", line 5, character 5 to line 5, character 32
 
-let (size as 'size) : {|32, 64|} = 32
+let (size as 'size) : {|32, 64|} = 32
 
   * 'size bound at file "global_type_var/v2.sail", line 5, character 14 to line 5, character 18
 
diff --git a/test/typecheck/pass/if_infer/v1.expect b/test/typecheck/pass/if_infer/v1.expect
index 55b39716..e0ffbbb1 100644
--- a/test/typecheck/pass/if_infer/v1.expect
+++ b/test/typecheck/pass/if_infer/v1.expect
@@ -4,13 +4,13 @@ Type error at file "if_infer/v1.sail", line 10, character 11 to line 10, charact
 
 No overloadings for vector_access, tried:
   bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex44#ex43# & ('ex44#ex43# + 1) <= 3)
+    Could not resolve quantifiers for bitvector_access (0 <= 'ex38#ex37# & ('ex38#ex37# + 1) <= 3)
     
     Try adding named type variables for 
     
     
   plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 'ex47#ex46# & ('ex47#ex46# + 1) <= 3)
+    Could not resolve quantifiers for plain_vector_access (0 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 3)
     
     Try adding named type variables for 
     
diff --git a/test/typecheck/pass/if_infer/v2.expect b/test/typecheck/pass/if_infer/v2.expect
index 3518448d..fe377730 100644
--- a/test/typecheck/pass/if_infer/v2.expect
+++ b/test/typecheck/pass/if_infer/v2.expect
@@ -4,13 +4,13 @@ Type error at file "if_infer/v2.sail", line 10, character 11 to line 10, charact
 
 No overloadings for vector_access, tried:
   bitvector_access:
-    Could not resolve quantifiers for bitvector_access (0 <= 'ex44#ex43# & ('ex44#ex43# + 1) <= 4)
+    Could not resolve quantifiers for bitvector_access (0 <= 'ex38#ex37# & ('ex38#ex37# + 1) <= 4)
     
     Try adding named type variables for 
     
     
   plain_vector_access:
-    Could not resolve quantifiers for plain_vector_access (0 <= 'ex47#ex46# & ('ex47#ex46# + 1) <= 4)
+    Could not resolve quantifiers for plain_vector_access (0 <= 'ex41#ex40# & ('ex41#ex40# + 1) <= 4)
     
     Try adding named type variables for 
     
diff --git a/test/typecheck/pass/patternrefinement.sail b/test/typecheck/pass/patternrefinement.sail
index 86294543..4433a2c3 100644
--- a/test/typecheck/pass/patternrefinement.sail
+++ b/test/typecheck/pass/patternrefinement.sail
@@ -12,7 +12,7 @@ val eq_vec = {ocaml: "eq_vec", lem: "eq_vec"}: forall ('m : Int) ('ord : Order).
   (vector('m, 'ord, bit), vector('m, 'ord, bit)) -> bool
 
 val eq_int = {ocaml: "eq_atom", lem: "eq"}: forall ('n : Int) ('m : Int).
-  (int('n), int('m)) -> bool
+  (int('n), int('m)) -> bool('n == 'm)
 
 val eq = {ocaml: "eq", lem: "eq"}: forall ('a : Type). ('a, 'a) -> bool