6 files changed, 59 insertions, 10 deletions
diff --git a/test/ocaml/bitfield/bitfield.sail b/test/ocaml/bitfield/bitfield.sail
new file mode 100644
index 00000000..5a70d52e
--- /dev/null
+++ b/test/ocaml/bitfield/bitfield.sail
@@ -0,0 +1,32 @@
+
+val _reg_deref = "reg_deref" : forall ('a : Type). register('a) -> 'a
+
+bitfield cr : bits(8) = {
+  CR0 : 7 .. 4,
+  LT : 7,
+  CR1 : 3 .. 2,
+  CR2 : 1,
+  CR3 : 0,
+}
+
+register CR : cr
+
+bitfield dr : vector(4, inc, bit) = {
+  DR0 : 2 .. 3
+}
+
+register DR : dr
+
+val main : unit -> unit effect {rreg, wreg}
+
+function main () = {
+  CR->bits() = 0xFF;
+  print_bits("CR: ", CR.bits());
+  ref CR.CR0() = 0x0;
+  print_bits("CR: ", CR.bits());
+  CR->LT() = 0b1;
+  print_bits("CR.CR0: ", CR.CR0());
+  print_bits("CR: ", CR.bits());
+  CR->CR3() = 0b0;
+  print_bits("CR: ", CR.bits())
+}
diff --git a/test/ocaml/bitfield/expect b/test/ocaml/bitfield/expect
new file mode 100644
index 00000000..63247dfd
--- /dev/null
+++ b/test/ocaml/bitfield/expect
@@ -0,0 +1,5 @@
+CR: 0xFF
+CR: 0x0F
+CR.CR0: 0x8
+CR: 0x8F
+CR: 0x8E
diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail
index 8c3e9700..fab04306 100644
--- a/test/ocaml/lsl/lsl.sail
+++ b/test/ocaml/lsl/lsl.sail
@@ -2,7 +2,7 @@ val zeros : forall ('n : Int), 'n >= 0. atom('n) -> bits('n)
 
 function zeros n = replicate_bits(0b0, 'n)
 
-val lslc : forall ('n : Int) ('shift : Int), 'n >= 0.
+val lslc : forall ('n : Int) ('shift : Int), 'n >= 1.
   (bits('n), atom('shift)) -> (bits('n), bit) effect {escape}
 
 function lslc (vec, shift) = {
@@ -13,7 +13,7 @@ function lslc (vec, shift) = {
   return((result, c))
 }
 
-val lsl : forall ('n : Int) ('shift : Int), 'n >= 0.
+val lsl : forall ('n : Int) ('shift : Int), 'n >= 1.
   (bits('n), atom('shift)) -> bits('n) effect {escape}
 
 function lsl (vec, shift) = if shift == 0 then vec else let (result, _) = lslc(vec, shift) in result
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
index 9bdfdc33..add43eec 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -24,28 +24,40 @@ val length = "length" : forall 'n ('a : Type). vector('n, dec, 'a) -> atom('n)
 
 overload operator == = {eq_atom, eq_int, eq_vec, eq_string, eq_real, eq_anything}
 
-val vector_subrange_A = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
+val vector_subrange_dec = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'o <= 'm <= 'n.
   (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
 
+val vector_subrange_inc = "subrange" : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n.
+  (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit)
+
+/*
 val vector_subrange_B = "subrange" : forall ('n : Int) ('m : Int) ('o : Int).
   (bits('n), atom('m), atom('o)) -> bits('m - ('o - 1))
+*/
 
-overload vector_subrange = {vector_subrange_A, vector_subrange_B}
+overload vector_subrange = {vector_subrange_dec, vector_subrange_inc}
 
-val vector_access_A = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
+val vector_access_dec = "access" : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n.
   (vector('n, dec, 'a), atom('m)) -> 'a
 
+/*
 val vector_access_B = "access" : forall ('n : Int) ('a : Type).
   (vector('n, dec, 'a), int) -> 'a
+*/
 
-overload vector_access = {vector_access_A, vector_access_B}
+overload vector_access = {vector_access_dec}
 
 val vector_update = "update" : forall 'n ('a : Type).
   (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
 
-val vector_update_subrange = "update_subrange" : forall 'n 'm 'o.
+val vector_update_subrange_dec = "update_subrange" : forall 'n 'm 'o.
   (bits('n), atom('m), atom('o), bits('m - ('o - 1))) -> bits('n)
 
+val vector_update_subrange_inc = "update_subrange" : forall 'n 'm 'o.
+  (vector('n, inc, bit), atom('m), atom('o), vector('o - ('m - 1), inc, bit)) -> vector('n, inc, bit)
+
+overload vector_update_subrange = {vector_update_subrange_dec, vector_update_subrange_inc}
+
 val vcons : forall ('n : Int) ('a : Type).
   ('a, vector('n, dec, 'a)) -> vector('n + 1, dec, 'a)
 
diff --git a/test/ocaml/reg_ref/rr.sail b/test/ocaml/reg_ref/rr.sail
index 3c11dcb8..f6d40a08 100644
--- a/test/ocaml/reg_ref/rr.sail
+++ b/test/ocaml/reg_ref/rr.sail
@@ -47,7 +47,7 @@ val vector_slice : forall 'n 'm 'o, 0 <= 'm <= 'o <= 'n.
 
 function vector_slice (v, to, from) = MkSlice(from, v[to .. from])
 
-val slice_slice : forall 'n 'm 'o 'p.
+val slice_slice : forall 'n 'm 'o 'p, 'm <= 'o & 'o - 'p <= 'n.
   (slice('p, 'n), atom('o), atom('m)) -> slice('m, 'o - ('m - 1))
 
 function slice_slice (MkSlice(start, v), to, from) = MkSlice(from, v[to - start .. from - start])
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh
index 9ed00494..aad3aa39 100755
--- a/test/ocaml/run_tests.sh
+++ b/test/ocaml/run_tests.sh
@@ -50,7 +50,7 @@ printf "<testsuites>\n" >> $DIR/tests.xml
 for i in `ls -d */`;
 do
     cd $DIR/$i;
-    if $SAILDIR/sail -new_parser -o out -ocaml ../prelude.sail `ls *.sail` 1> /dev/null;
+    if $SAILDIR/sail -o out -ocaml ../prelude.sail `ls *.sail` 1> /dev/null;
     then
 	./out > result;
 	if diff expect result;
@@ -74,7 +74,7 @@ cd $DIR
 for i in `ls -d */`;
 do
     cd $DIR/$i;
-    if $SAILDIR/sail -new_parser -o out -ocaml_trace ../prelude.sail `ls *.sail` 1> /dev/null;
+    if $SAILDIR/sail -o out -ocaml_trace ../prelude.sail `ls *.sail` 1> /dev/null;
     then
 	./out > result 2> /dev/null;
 	if diff expect result;