Added effect system to new type checker

9 files changed, 42 insertions, 1 deletions

diff --git a/test/typecheck/fail/eff_escape.sail b/test/typecheck/fail/eff_escape.sail
new file mode 100644
index 00000000..698cf0b1
--- /dev/null
+++ b/test/typecheck/fail/eff_escape.sail
@@ -0,0 +1,7 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+  exit ()
+}
diff --git a/test/typecheck/fail/eff_undef.sail b/test/typecheck/fail/eff_undef.sail
new file mode 100644
index 00000000..d5d98a3f
--- /dev/null
+++ b/test/typecheck/fail/eff_undef.sail
@@ -0,0 +1,7 @@
+
+val unit -> unit effect pure test
+
+function unit test () =
+{
+  undefined
+}
diff --git a/test/typecheck/pass/mips400.sail b/test/typecheck/pass/mips400.sail
index 4b9c5286..38680fcf 100644
--- a/test/typecheck/pass/mips400.sail
+++ b/test/typecheck/pass/mips400.sail
@@ -22,7 +22,7 @@ val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2
   (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
 
 (* Implicit register dereferencing *)
-val cast forall Type 'a. register<'a> -> 'a effect pure reg_deref
+val cast forall Type 'a. register<'a> -> 'a effect {rreg} reg_deref
 
 overload vector_access [vector_access_inc; vector_access_dec]
 
diff --git a/test/typecheck/pass/nondet.sail b/test/typecheck/pass/nondet.sail
index 3c5db152..8a353c66 100644
--- a/test/typecheck/pass/nondet.sail
+++ b/test/typecheck/pass/nondet.sail
@@ -1,6 +1,8 @@
 
 register int z
 
+val unit -> unit effect {wreg} test
+
 function unit test () = {
   nondet {
     z := 0;
diff --git a/test/typecheck/pass/nondet_assert.sail b/test/typecheck/pass/nondet_assert.sail
index 1486c8d4..e90bb6f2 100644
--- a/test/typecheck/pass/nondet_assert.sail
+++ b/test/typecheck/pass/nondet_assert.sail
@@ -1,6 +1,8 @@
 
 register int z
 
+val unit -> int effect {wreg, rreg} test
+
 function int test () = {
   nondet {
     z := 0;
diff --git a/test/typecheck/pass/nondet_return.sail b/test/typecheck/pass/nondet_return.sail
index 2a559e19..56fcfd5a 100644
--- a/test/typecheck/pass/nondet_return.sail
+++ b/test/typecheck/pass/nondet_return.sail
@@ -1,6 +1,8 @@
 
 register int z
 
+val unit -> int effect {wreg, rreg} test
+
 function int test () = {
   nondet {
     z := 0;
diff --git a/test/typecheck/pass/phantom_num.sail b/test/typecheck/pass/phantom_num.sail
new file mode 100644
index 00000000..c4ff8b13
--- /dev/null
+++ b/test/typecheck/pass/phantom_num.sail
@@ -0,0 +1,17 @@
+
+val extern (int, int) -> bool effect pure gt_int
+
+(* val cast forall Num 'n, Num 'm. [|'n:'m|] -> int effect pure cast_range_int *)
+
+overload (deinfix >) [gt_int]
+
+register int z
+
+val forall Nat 'n. unit -> unit effect {wreg} test
+
+function forall Nat 'n. unit test () =
+{
+  if sizeof 'n > 3
+  then z := 0
+  else z := 1
+}
diff --git a/test/typecheck/pass/regtyp_vec.sail b/test/typecheck/pass/regtyp_vec.sail
index 5142208e..c939cce8 100644
--- a/test/typecheck/pass/regtyp_vec.sail
+++ b/test/typecheck/pass/regtyp_vec.sail
@@ -8,6 +8,8 @@ val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l +
 val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,inc,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access_inc
 *)
 
+overload vector_access [vector_access_dec]
+
 default Order dec
 
 typedef CauseReg = register bits [ 31 : 0 ] {
diff --git a/test/typecheck/pass/simple_record_access.sail b/test/typecheck/pass/simple_record_access.sail
index a31dfa83..d4f4d61f 100644
--- a/test/typecheck/pass/simple_record_access.sail
+++ b/test/typecheck/pass/simple_record_access.sail
@@ -8,6 +8,8 @@ typedef Record =
 
 register bit[32] R0
 
+val Record -> unit effect {wreg} test
+
 function unit test ((Record) r) =
 {
   R0 := r.bitfield;