Merge changes to type_check.ml

14 files changed, 185 insertions, 0 deletions

diff --git a/test/typecheck/pass/arm_types.sail b/test/typecheck/pass/arm_types.sail
index 83cc8687..af0bcba9 100644
--- a/test/typecheck/pass/arm_types.sail
+++ b/test/typecheck/pass/arm_types.sail
@@ -1,3 +1,5 @@
+$include <flow.sail>
+
 enum boolean = {FALSE, TRUE}
 
 enum signal = {LOW, HIGH}
diff --git a/test/typecheck/pass/decode_patterns.sail b/test/typecheck/pass/decode_patterns.sail
new file mode 100644
index 00000000..d8b17f5b
--- /dev/null
+++ b/test/typecheck/pass/decode_patterns.sail
@@ -0,0 +1,47 @@
+$include <flow.sail>
+
+default Order dec
+
+type bits ('n : Int) = vector('n, dec, bit)
+
+val eq_anything = "eq" : forall ('a : Type). ('a, 'a) -> bool
+
+overload operator == = {eq_anything}
+
+val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_dec"} : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+  (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+
+val vector_access = {ocaml: "access", lem: "access_vec_dec"} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n.
+  (bits('n), atom('m)) -> bit
+
+val decode : vector(16, dec, bit) -> unit
+
+scattered function decode
+
+function clause decode 0x00 @ 0b000 @ _ : bits(1) @ 0x0 as op_code =
+  if op_code[5 .. 5] == 0b0 then {
+    ()
+  } else {
+    ()
+  }
+
+function clause decode 0x00 @ 0b001 @ [b : bit] @ 0x0 =
+  if b == bitone then {
+    ()
+  } else {
+    ()
+  }
+
+end decode
+
+val decode2 : vector(16, dec, bit) -> unit
+
+function decode2 x =
+  match x {
+    0x00 @ 0b000 @ [b : bit]  @ 0x0 =>
+      if b == bitone then {
+        ()
+      } else {
+        ()
+      }
+  }
diff --git a/test/typecheck/pass/exist_tlb.sail b/test/typecheck/pass/exist_tlb.sail
index f1b79b3d..de15edf8 100644
--- a/test/typecheck/pass/exist_tlb.sail
+++ b/test/typecheck/pass/exist_tlb.sail
@@ -1,3 +1,5 @@
+$include <flow.sail>
+
 val extz : forall ('n : Int) ('m : Int) ('ord : Order).
   vector('n, 'ord, bit) -> vector('m, 'ord, bit)
 
diff --git a/test/typecheck/pass/function_namespace.sail b/test/typecheck/pass/function_namespace.sail
new file mode 100644
index 00000000..1e79f051
--- /dev/null
+++ b/test/typecheck/pass/function_namespace.sail
@@ -0,0 +1,11 @@
+
+val test : bool -> unit
+
+function test _ = ()
+
+val main: unit -> unit
+
+function main _ = {
+  let test2 = true;
+  test(test2)
+}
diff --git a/test/typecheck/pass/function_namespace/v1.expect b/test/typecheck/pass/function_namespace/v1.expect
new file mode 100644
index 00000000..d01c3adb
--- /dev/null
+++ b/test/typecheck/pass/function_namespace/v1.expect
@@ -0,0 +1,5 @@
+Type error at file "function_namespace/v1.sail", line 9, character 7 to line 9, character 10
+
+  let test = true;
+
+Local variable test is already bound as a function name
diff --git a/test/typecheck/pass/function_namespace/v1.sail b/test/typecheck/pass/function_namespace/v1.sail
new file mode 100644
index 00000000..a72dcc11
--- /dev/null
+++ b/test/typecheck/pass/function_namespace/v1.sail
@@ -0,0 +1,11 @@
+
+val test : bool -> unit
+
+function test _ = ()
+
+val main: unit -> unit
+
+function main _ = {
+  let test = true;
+  test(test)
+}
diff --git a/test/typecheck/pass/global_type_var.sail b/test/typecheck/pass/global_type_var.sail
new file mode 100644
index 00000000..215907b4
--- /dev/null
+++ b/test/typecheck/pass/global_type_var.sail
@@ -0,0 +1,21 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
diff --git a/test/typecheck/pass/global_type_var/v1.expect b/test/typecheck/pass/global_type_var/v1.expect
new file mode 100644
index 00000000..67355f59
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v1.expect
@@ -0,0 +1,6 @@
+Type error at file "global_type_var/v1.sail", line 23, character 14 to line 23, character 15
+
+let _ = test(32)
+
+Tried performing type coercion on 32
+Failed because atom<32> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
diff --git a/test/typecheck/pass/global_type_var/v1.sail b/test/typecheck/pass/global_type_var/v1.sail
new file mode 100644
index 00000000..f2b2f89a
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v1.sail
@@ -0,0 +1,23 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
+
+let _ = test(32)
\ No newline at end of file
diff --git a/test/typecheck/pass/global_type_var/v2.expect b/test/typecheck/pass/global_type_var/v2.expect
new file mode 100644
index 00000000..fb31fbed
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v2.expect
@@ -0,0 +1,6 @@
+Type error at file "global_type_var/v2.sail", line 23, character 14 to line 23, character 15
+
+let _ = test(64)
+
+Tried performing type coercion on 64
+Failed because atom<64> is not a subtype of atom<'size> in context ('size = 32 | 'size = 64)
diff --git a/test/typecheck/pass/global_type_var/v2.sail b/test/typecheck/pass/global_type_var/v2.sail
new file mode 100644
index 00000000..e8340978
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v2.sail
@@ -0,0 +1,23 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
+
+let _ = test(64)
\ No newline at end of file
diff --git a/test/typecheck/pass/global_type_var/v3.expect b/test/typecheck/pass/global_type_var/v3.expect
new file mode 100644
index 00000000..a01f3eec
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v3.expect
@@ -0,0 +1,5 @@
+Type error at file "global_type_var/v3.sail", line 9, character 19 to line 9, character 23
+
+val test : forall 'size. atom('size) -> unit
+
+Kind identifier 'size is already bound
diff --git a/test/typecheck/pass/global_type_var/v3.sail b/test/typecheck/pass/global_type_var/v3.sail
new file mode 100644
index 00000000..274490ff
--- /dev/null
+++ b/test/typecheck/pass/global_type_var/v3.sail
@@ -0,0 +1,21 @@
+$include <flow.sail>
+
+overload operator == = {eq_atom}
+
+let (size as 'size) : {|32, 64|} = 32
+
+val zeros : forall 'n. atom('n) -> vector ('n, dec, bit)
+
+val test : forall 'size. atom('size) -> unit
+
+function test x =
+  if x == 32 then {
+    ()
+  } else {
+    let y : atom(64) = size in
+    ()
+  }
+
+val test2 : unit -> atom('size)
+
+function test2 () = size
diff --git a/test/typecheck/pass/simple_record_access.sail b/test/typecheck/pass/simple_record_access.sail
index b1eab652..a6e34c8b 100644
--- a/test/typecheck/pass/simple_record_access.sail
+++ b/test/typecheck/pass/simple_record_access.sail
@@ -1,3 +1,5 @@
+$include <flow.sail>
+
 enum signal = {LOW, HIGH}
 
 type Bit32 = vector(32, inc, bit)