Store function instantiation information within annotations, so we don't

have to recompute it, which can be very expensive for very large
specifications

Also additional flow typing and fixes for boolean type variables

7 files changed, 27 insertions, 19 deletions

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