Added support for bitvectors

Added basic support for vector types, and fixed various bugs. Also
added some basic tests for these features in test/typecheck.

7 files changed, 46 insertions, 1 deletions

diff --git a/test/typecheck/fail/assignment_simple1.sail b/test/typecheck/fail/assignment_simple1.sail
index 3778d84a..1ad9f8bf 100644
--- a/test/typecheck/fail/assignment_simple1.sail
+++ b/test/typecheck/fail/assignment_simple1.sail
@@ -8,7 +8,6 @@ val unit -> [:10:] effect pure test
 function [:10:] test () =
 {
   z := 9;
-  z := 10;
   z
 }
 
diff --git a/test/typecheck/fail/bitwise_not_gen1.sail b/test/typecheck/fail/bitwise_not_gen1.sail
new file mode 100644
index 00000000..272b1a65
--- /dev/null
+++ b/test/typecheck/fail/bitwise_not_gen1.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not
+
+default Order dec
+    
+val forall 'n. bit['n] -> bit['n - 1] effect pure test
+    
+function forall 'n. bit['n - 1] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file
diff --git a/test/typecheck/fail/bitwise_not_gen2.sail b/test/typecheck/fail/bitwise_not_gen2.sail
new file mode 100644
index 00000000..fdf17244
--- /dev/null
+++ b/test/typecheck/fail/bitwise_not_gen2.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not
+
+default Order dec
+    
+val forall 'n. bit['n] -> bit['n + 1] effect pure test
+    
+function forall 'n. bit['n + 1] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file
diff --git a/test/typecheck/fail/fun_simple_constraints9.sail b/test/typecheck/fail/fun_simple_constraints9.sail
new file mode 100644
index 00000000..3563ae2d
--- /dev/null
+++ b/test/typecheck/fail/fun_simple_constraints9.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'n, Nat 'm. ([:'n + 20:], [:'m:]) -> [:'n + 20 + 'm:] effect pure plus
+
+val forall Nat 'n, 'n >= 10. [:'n:] -> [:'n:] effect pure ten_id
+
+val forall Nat 'N, 'N >= 63. [|10:'N|] -> [|10:'N|] effect pure branch
+
+function forall Nat 'N, 'N >= 63. [|10:'N|] branch x = ten_id(plus(sizeof 'N, 1))
diff --git a/test/typecheck/pass/bitwise_not.sail b/test/typecheck/pass/bitwise_not.sail
new file mode 100644
index 00000000..1c4f8d3b
--- /dev/null
+++ b/test/typecheck/pass/bitwise_not.sail
@@ -0,0 +1,7 @@
+val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not
+
+default Order dec
+    
+val bit[5] -> bit[5] effect pure test
+    
+function bit[5] test ((bit[5]) x) = bitwise_not(x)
\ No newline at end of file
diff --git a/test/typecheck/pass/bitwise_not_gen.sail b/test/typecheck/pass/bitwise_not_gen.sail
new file mode 100644
index 00000000..8be3ea5c
--- /dev/null
+++ b/test/typecheck/pass/bitwise_not_gen.sail
@@ -0,0 +1,8 @@
+
+val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not
+
+default Order dec
+    
+val forall 'n. bit['n] -> bit['n] effect pure test
+    
+function forall 'n. bit['n] test ((bit['n]) x) = bitwise_not(bitwise_not(x))
\ No newline at end of file
diff --git a/test/typecheck/pass/bitwise_not_x3.sail b/test/typecheck/pass/bitwise_not_x3.sail
new file mode 100644
index 00000000..49d962a6
--- /dev/null
+++ b/test/typecheck/pass/bitwise_not_x3.sail
@@ -0,0 +1,7 @@
+val forall Nat 'n, Nat 'm, Order 'o. vector<'n,'m,'o,bit> -> vector<'n,'m,'o,bit> effect pure bitwise_not
+
+default Order dec
+    
+val bit[5] -> bit[5] effect pure test
+    
+function bit[5] test ((bit[5]) x) = bitwise_not(bitwise_not(bitwise_not(x)))
\ No newline at end of file