From 1bc81fa6dcafcfe24fce3685c2eb61f882e6b65c Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 19 Nov 2018 14:44:42 +0000
Subject: Add missing constraints on bitvector_access, with regression
 test.Fixes #24.

---
 lib/vector_dec.sail                      |  2 +-
 lib/vector_inc.sail                      |  2 +-
 test/typecheck/pass/vec_length.sail      |  8 ++++++++
 test/typecheck/pass/vec_length/v1.expect | 13 +++++++++++++
 test/typecheck/pass/vec_length/v1.sail   |  8 ++++++++
 5 files changed, 31 insertions(+), 2 deletions(-)
 create mode 100644 test/typecheck/pass/vec_length.sail
 create mode 100644 test/typecheck/pass/vec_length/v1.expect
 create mode 100644 test/typecheck/pass/vec_length/v1.sail

diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index 8abcd218..7011a55c 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -63,7 +63,7 @@ val bitvector_access = {
   lem: "access_vec_dec",
   coq: "access_vec_dec",
   c: "vector_access"
-} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit
+} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit
 
 val plain_vector_access = {
   ocaml: "access",
diff --git a/lib/vector_inc.sail b/lib/vector_inc.sail
index b295c92c..042a6324 100644
--- a/lib/vector_inc.sail
+++ b/lib/vector_inc.sail
@@ -61,7 +61,7 @@ val bitvector_access = {
   lem: "access_vec_inc",
   coq: "access_vec_inc",
   c: "vector_access"
-} : forall ('n : Int), 'n >= 0. (bits('n), int) -> bit
+} : forall ('n : Int) ('m : Int), 0 <= 'm < 'n . (bits('n), int('m)) -> bit
 
 val plain_vector_access = {
   ocaml: "access",
diff --git a/test/typecheck/pass/vec_length.sail b/test/typecheck/pass/vec_length.sail
new file mode 100644
index 00000000..078e266b
--- /dev/null
+++ b/test/typecheck/pass/vec_length.sail
@@ -0,0 +1,8 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[3];
+  ()
+}
\ No newline at end of file
diff --git a/test/typecheck/pass/vec_length/v1.expect b/test/typecheck/pass/vec_length/v1.expect
new file mode 100644
index 00000000..68a4ca70
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1.expect
@@ -0,0 +1,13 @@
+Type error at file "vec_length/v1.sail", line 6, character 11 to line 6, character 15
+
+  let y = x[10];
+
+No overloadings for vector_access, tried:
+  bitvector_access:
+    Could not resolve quantifiers for bitvector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
+  plain_vector_access:
+    Could not resolve quantifiers for plain_vector_access (0 <= 10 & (10 + 1) <= 8)
+    
+    Try adding the constraint: (0 <= 10 & (10 + 1) <= 8)
diff --git a/test/typecheck/pass/vec_length/v1.sail b/test/typecheck/pass/vec_length/v1.sail
new file mode 100644
index 00000000..735da89c
--- /dev/null
+++ b/test/typecheck/pass/vec_length/v1.sail
@@ -0,0 +1,8 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  let x : bits(8) = 0xff;
+  let y = x[10];
+  ()
+}
\ No newline at end of file
-- 
cgit v1.2.3