Added support for vector append and indexing

11 files changed, 156 insertions, 0 deletions

diff --git a/test/typecheck/fail/vector_access1.sail b/test/typecheck/fail/vector_access1.sail
new file mode 100644
index 00000000..1eef5250
--- /dev/null
+++ b/test/typecheck/fail/vector_access1.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[4] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,0);
+  z := v[4]
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_access2.sail b/test/typecheck/fail/vector_access2.sail
new file mode 100644
index 00000000..0b4ba7c2
--- /dev/null
+++ b/test/typecheck/fail/vector_access2.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[4] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,-1);
+  z := v[3]
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_access3.sail b/test/typecheck/fail/vector_access3.sail
new file mode 100644
index 00000000..dd43cfea
--- /dev/null
+++ b/test/typecheck/fail/vector_access3.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[0] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,0);
+  z := v[0]
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_access4.sail b/test/typecheck/fail/vector_access4.sail
new file mode 100644
index 00000000..31d34eae
--- /dev/null
+++ b/test/typecheck/fail/vector_access4.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[-5] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,([|0:-5|]) -1);
+  z := v[-1]
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_append1.sail b/test/typecheck/fail/vector_append1.sail
new file mode 100644
index 00000000..e2429380
--- /dev/null
+++ b/test/typecheck/fail/vector_append1.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val (bit[4], bit[4]) -> bit[7] effect pure test
+    
+function bit[7] test (v1, v2) =
+{
+  z := vector_access(v1, 3);
+  z := v1[0];
+  zv := vector_append(v1, v2);
+  zv := v1 : v2;
+  zv
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_append2.sail b/test/typecheck/fail/vector_append2.sail
new file mode 100644
index 00000000..acaeb0b0
--- /dev/null
+++ b/test/typecheck/fail/vector_append2.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val (bit[4], bit[4]) -> bit[9] effect pure test
+    
+function bit[9] test (v1, v2) =
+{
+  z := vector_access(v1, 3);
+  z := v1[0];
+  zv := vector_append(v1, v2);
+  zv := v1 : v2;
+  zv
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_append_gen1.sail b/test/typecheck/fail/vector_append_gen1.sail
new file mode 100644
index 00000000..727d5c14
--- /dev/null
+++ b/test/typecheck/fail/vector_append_gen1.sail
@@ -0,0 +1,14 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val forall 'n, 'm. (bit['n], bit['m]) -> bit['n + 'm] effect pure test
+    
+function forall 'n, 'm. bit['n + 'm] test (v1, v2) =
+{
+  v1 : v2;
+}
\ No newline at end of file
diff --git a/test/typecheck/fail/vector_append_gen2.sail b/test/typecheck/fail/vector_append_gen2.sail
new file mode 100644
index 00000000..8e534253
--- /dev/null
+++ b/test/typecheck/fail/vector_append_gen2.sail
@@ -0,0 +1,14 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val forall 'n, 'm. (bit['n], bit['m]) -> bit['n + 'm] effect pure test
+    
+function forall 'n, 'm. bit['n + 'm] test (v1, v2) =
+{
+  vector_append(v1, v2);
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vector_access.sail b/test/typecheck/pass/vector_access.sail
new file mode 100644
index 00000000..9346f5fe
--- /dev/null
+++ b/test/typecheck/pass/vector_access.sail
@@ -0,0 +1,12 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+default Order inc
+
+val bit[4] -> unit effect pure test
+    
+function unit test v =
+{
+  z := vector_access(v,3);
+  z := v[3]
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vector_append.sail b/test/typecheck/pass/vector_append.sail
new file mode 100644
index 00000000..d2f1ca47
--- /dev/null
+++ b/test/typecheck/pass/vector_append.sail
@@ -0,0 +1,18 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val (bit[4], bit[4]) -> bit[8] effect pure test
+    
+function bit[8] test (v1, v2) =
+{
+  z := vector_access(v1, 3);
+  z := v1[0];
+  zv := vector_append(v1, v2);
+  zv := v1 : v2;
+  zv
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vector_append_gen.sail b/test/typecheck/pass/vector_append_gen.sail
new file mode 100644
index 00000000..ddb027ee
--- /dev/null
+++ b/test/typecheck/pass/vector_append_gen.sail
@@ -0,0 +1,14 @@
+
+val forall Nat 'n, Nat 'l, Order 'o, Type 'a, 'l >= 0. (vector<'n,'l,'o,'a>, [|'n:'n + 'l - 1|]) -> 'a effect pure vector_access
+
+val forall Nat 'n1, Nat 'l1, Nat 'n2, Nat 'l2, Order 'o, Type 'a, 'l1 >= 0, 'l2 >= 0.
+  (vector<'n1,'l1,'o,'a>, vector<'n2,'l2,'o,'a>) -> vector<'n1,'l1 + 'l2,'o,'a> effect pure vector_append
+
+default Order inc
+
+val forall 'n, 'm, 'n >= 0, 'm >= 0. (bit['n], bit['m]) -> bit['n + 'm] effect pure test
+    
+function forall 'n, 'm. bit['n + 'm] test (v1, v2) =
+{
+  vector_append(v1, v2);
+}
\ No newline at end of file