Added vector subrange support, and tests

2 files changed, 40 insertions, 0 deletions

diff --git a/test/typecheck/fail/vector_subrange_gen1.sail b/test/typecheck/fail/vector_subrange_gen1.sail
new file mode 100644
index 00000000..0ae6f9f9
--- /dev/null
+++ b/test/typecheck/fail/vector_subrange_gen1.sail
@@ -0,0 +1,20 @@
+
+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
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'u, Order 'o, Type 'a, 'l >= 0, 'm <= 'u, 'u <= 'l. (vector<'n,'l,'o,'a>, [:'m:], [:'u:]) -> vector<'m,'u - 'm,'o,'a> effect pure vector_subrange
+
+val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure minus
+
+default Order inc
+
+val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 2] effect pure test
+    
+function forall 'n, 'n >= 5. bit['n - 3] test v =
+{
+  z := vector_subrange(v, 0, minus(sizeof 'n, 3));
+  z := v[0 .. minus(sizeof 'n, 2)];
+  z
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vector_subrange_gen.sail b/test/typecheck/pass/vector_subrange_gen.sail
new file mode 100644
index 00000000..5c48db77
--- /dev/null
+++ b/test/typecheck/pass/vector_subrange_gen.sail
@@ -0,0 +1,20 @@
+
+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
+
+val forall Nat 'n, Nat 'l, Nat 'm, Nat 'u, Order 'o, Type 'a, 'l >= 0, 'm <= 'u, 'u <= 'l. (vector<'n,'l,'o,'a>, [:'m:], [:'u:]) -> vector<'m,'u - 'm,'o,'a> effect pure vector_subrange
+
+val forall Nat 'n, Nat 'm. ([:'n:], [:'m:]) -> [:'n - 'm:] effect pure minus
+
+default Order inc
+
+val forall 'n, 'm, 'n >= 5. bit['n] -> bit['n - 2] effect pure test
+    
+function forall 'n, 'n >= 5. bit['n - 2] test v =
+{
+  z := vector_subrange(v, 0, minus(sizeof 'n, 2));
+  z := v[0 .. minus(sizeof 'n, 2)];
+  z
+}
\ No newline at end of file