From ace279c20bcf46f2c298dce9479decfc09d14084 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 22 Jun 2017 19:40:39 +0100
Subject: Added vector subrange support, and tests

---
 src/type_check_new.ml                         |  1 +
 test/typecheck/fail/vector_subrange_gen1.sail | 20 ++++++++++++++++++++
 test/typecheck/pass/vector_subrange_gen.sail  | 20 ++++++++++++++++++++
 3 files changed, 41 insertions(+)
 create mode 100644 test/typecheck/fail/vector_subrange_gen1.sail
 create mode 100644 test/typecheck/pass/vector_subrange_gen.sail

diff --git a/src/type_check_new.ml b/src/type_check_new.ml
index 65227d5e..593b633d 100644
--- a/src/type_check_new.ml
+++ b/src/type_check_new.ml
@@ -1153,6 +1153,7 @@ and infer_exp env (E_aux (exp_aux, (l, _)) as exp : 'a exp) : tannot exp =
   | E_app (f, xs) -> infer_funapp l env f xs None
   | E_vector_access (v, n) -> infer_funapp l env (mk_id "vector_access") [v; n] None
   | E_vector_append (v1, v2) -> infer_funapp l env (mk_id "vector_append") [v1; v2] None
+  | E_vector_subrange (v, n, m) -> infer_funapp l env (mk_id "vector_subrange") [v; n; m] None
   | _ -> typ_error l "Unimplemented"
                    
 and infer_funapp l env f xs ret_ctx_typ =
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
-- 
cgit v1.2.3