Added support for set constraints

Also added some additional tests in test/typecheck

9 files changed, 83 insertions, 2 deletions

diff --git a/test/typecheck/fail/bv_simple_index_no_cast.sail b/test/typecheck/fail/bv_simple_index_no_cast.sail
new file mode 100644
index 00000000..74f46ab7
--- /dev/null
+++ b/test/typecheck/fail/bv_simple_index_no_cast.sail
@@ -0,0 +1,9 @@
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+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_inc; vector_access_dec]
+
+function bool bv ((bit[64]) x) =
+{
+  x[32]
+}
diff --git a/test/typecheck/fail/nat_set.sail b/test/typecheck/fail/nat_set.sail
new file mode 100644
index 00000000..036183c5
--- /dev/null
+++ b/test/typecheck/fail/nat_set.sail
@@ -0,0 +1,9 @@
+
+function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) =
+{
+  true
+}
+
+let x = test(1)
+let y = test(3)
+let z = test(4)
\ No newline at end of file
diff --git a/test/typecheck/fail/word_width_bytes_mips.sail b/test/typecheck/fail/word_width_bytes_mips.sail
new file mode 100644
index 00000000..91f3e787
--- /dev/null
+++ b/test/typecheck/fail/word_width_bytes_mips.sail
@@ -0,0 +1,11 @@
+typedef WordType = enumerate {B; H; W; D}
+
+(* This fails because it's not true for all combinations of 'r and WordType *)
+(* Needs existential types, i.e. return type should be exists Nat 'r, 'r in {1,2,4,8}. [:'r:] *)
+function forall Nat 'r, 'r IN {1,2,4,8}. wordWidthBytes((WordType) w) =
+  switch(w) {
+    case B -> 1
+    case H -> 2
+    case W -> 4
+    case D -> 8
+  }
diff --git a/test/typecheck/pass/bv_simple_index.sail b/test/typecheck/pass/bv_simple_index.sail
new file mode 100644
index 00000000..72e1b094
--- /dev/null
+++ b/test/typecheck/pass/bv_simple_index.sail
@@ -0,0 +1,11 @@
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+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_inc; vector_access_dec]
+
+val cast bit -> bool effect pure cast_bit_bool
+
+function bool bv ((bit[64]) x) =
+{
+  x[32]
+}
diff --git a/test/typecheck/pass/bv_simple_index_bit.sail b/test/typecheck/pass/bv_simple_index_bit.sail
new file mode 100644
index 00000000..2ba5b928
--- /dev/null
+++ b/test/typecheck/pass/bv_simple_index_bit.sail
@@ -0,0 +1,9 @@
+val forall Nat 'n, Nat 'l, Type 'a, 'l >= 0. (vector<'n,'l,dec,'a>, [|'n - 'l + 1:'n|]) -> 'a effect pure vector_access_dec
+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_inc; vector_access_dec]
+
+function bit bv ((bit[64]) x) =
+{
+  x[32]
+}
diff --git a/test/typecheck/pass/nat_set.sail b/test/typecheck/pass/nat_set.sail
new file mode 100644
index 00000000..46338353
--- /dev/null
+++ b/test/typecheck/pass/nat_set.sail
@@ -0,0 +1,8 @@
+
+function forall Nat 'n, 'n IN {1,2,3}. bool test (([:'n:]) x) =
+{
+  true
+}
+
+let x = test(1)
+let y = test(3)
\ No newline at end of file
diff --git a/test/typecheck/pass/set_mark.sail b/test/typecheck/pass/set_mark.sail
new file mode 100644
index 00000000..59710c46
--- /dev/null
+++ b/test/typecheck/pass/set_mark.sail
@@ -0,0 +1,6 @@
+
+val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv
+
+function forall Num 'N, 'N IN {32}. bit['N] Foo32( (bit['N]) x) = x
+
+let x = Foo32( (bit[32]) 0)
diff --git a/test/typecheck/pass/set_mark2.sail b/test/typecheck/pass/set_mark2.sail
new file mode 100644
index 00000000..c1433058
--- /dev/null
+++ b/test/typecheck/pass/set_mark2.sail
@@ -0,0 +1,5 @@
+val cast forall Num 'n, Num 'm, Order 'ord. [:0:] -> vector<'n,'m,'ord,bit> effect pure cast_zero_bv
+
+function forall Nat 'N, 'N IN {32, 64}. bit['N] Foo32( (bit['N]) x) = x
+
+let x = Foo32( (bit[64]) 0)
diff --git a/test/typecheck/run_tests.sh b/test/typecheck/run_tests.sh
index 7fca4770..f33f21ac 100755
--- a/test/typecheck/run_tests.sh
+++ b/test/typecheck/run_tests.sh
@@ -11,6 +11,9 @@ NC='\033[0m'
 mkdir -p $DIR/rtpass
 mkdir -p $DIR/rtfail
 
+pass=0
+fail=0
+
 for i in `ls $DIR/pass/`;
 do
     printf "testing $i expecting pass: "
@@ -18,11 +21,15 @@ do
     then
 	if $DIR/../../sail -dno_cast -just_check $DIR/rtpass/$i 2> /dev/null;
 	then
+	    (( pass += 2))
 	    printf "${GREEN}pass${NC}\n"
 	else
-	    printf "${YELLOW}pass${NC}\n"
+	    (( fail += 1 ))
+	    (( pass += 1 ))
+	    printf "${YELLOW}pass but failed re-check${NC}\n"
 	fi
     else
+	(( fail += 2 ))
 	printf "${RED}fail${NC}\n"
     fi
 done
@@ -32,13 +39,19 @@ do
     printf "testing $i expecting fail: "
     if $DIR/../../sail -ddump_tc_ast -just_check $DIR/fail/$i 2> /dev/null 1> $DIR/rtfail/$i;
     then
+	(( fail += 2 ))
 	printf "${RED}pass${NC}\n"
     else
 	if $DIR/../../sail -dno_cast -just_check $DIR/rtfail/$i 2> /dev/null;
 	then
-	    printf "${YELLOW}fail${NC}\n"
+	    (( fail += 1 ))
+	    (( pass += 1 ))
+	    printf "${YELLOW}fail but passed re-check${NC}\n"
 	else
+	    (( pass += 2 ))
 	    printf "${GREEN}fail${NC}\n"
 	fi
     fi
 done
+
+printf "Passed ${pass} out of $(( pass + fail ))\n"