Flow typing and l-expression changes for ASL parser

1. Experiment with allowing some flow typing on mutable variables for
translating ASL in a more idiomatic way. I realise after updating some
of the test cases that this could have some problematic side effects
for lem translation, where mutable variables are translated into
monadic code. We'd need to ensure that whatever flow typing happens
for mutable variables also works for monadic code, including within
transformed loops. If this doesn't work out some of these changes may
need to be reverted.

2. Make the type inference for l-expressions a bit smarter. Splits the
type checking rules for l-expressions into a inference part and a
checking part like the other bi-directional rules. Should not be able
to type check slightly more l-expresions, such as nested vector slices
that may not have checked previously.

The l-expression rules for vector patterns should be simpler now, but
they are also more strict about bounds checking. Previously the bounds
checks were derived from the corresponding operations that would
appear on the RHS (i.e. LEXP_vector would get it's check from
vector_access). This meant that the l-expression bounds checks could
be weakend by weakening the checks on those operations. Now this is no
longer possible, there is a -no_lexp_bounds_check option which turns
of bounds checking in l-expressions. Currently this is on for the
generated ARM spec, but this should only be temporary.

3. Add a LEXP_vector_concat which mirrors P_vector_concat except in
l-expressions. Previously there was a hack that overloaded LEXP_tup
for this to translate some ASL patterns, but that was fairly
ugly. Adapt the rewriter and other parts of the code to handle
this. The rewriter for lexp tuple vector assignments is now a rewriter
for vector concat assignments.

4. Include a newly generated version of aarch64_no_vector

5. Update the Ocaml test suite to use builtins in lib/

9 files changed, 9 insertions, 315 deletions

diff --git a/test/arm/run_tests.sh b/test/arm/run_tests.sh
index d4e01079..15a45e7c 100755
--- a/test/arm/run_tests.sh
+++ b/test/arm/run_tests.sh
@@ -51,7 +51,7 @@ cd $SAILDIR/aarch64
 
 printf "Compiling specification...\n"
 
-if $SAILDIR/sail -o aarch64_test -ocaml prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null;
+if $SAILDIR/sail -no_lexp_bounds_check -o aarch64_test -ocaml prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null;
 then
     green "compiled no_vector specification" "ok";
     mv aarch64_test $DIR/;
@@ -83,7 +83,7 @@ printf "\nLoading specification into interpreter...\n"
 
 cd $SAILDIR/aarch64
 
-if $SAILDIR/sail -is $DIR/test.isail prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null;
+if $SAILDIR/sail -no_lexp_bounds_check -is $DIR/test.isail prelude.sail no_vector/spec.sail decode_start.sail no_vector/decode.sail decode_end.sail main.sail 1> /dev/null 2> /dev/null;
 then
     green "loaded no_vector specification" "ok";
 
diff --git a/test/ocaml/bitfield/bitfield.sail b/test/ocaml/bitfield/bitfield.sail
index 2a53ab3c..342b3d08 100644
--- a/test/ocaml/bitfield/bitfield.sail
+++ b/test/ocaml/bitfield/bitfield.sail
@@ -11,13 +11,6 @@ bitfield cr : bits(8) = {
 
 register CR : cr
 
-bitfield dr : vector(4, inc, bit) = {
-  DR0 : 2 .. 3,
-  LT : 2
-}
-
-register DR : dr
-
 val main : unit -> unit effect {rreg, wreg}
 
 function main () = {
diff --git a/test/ocaml/lsl/lsl.sail b/test/ocaml/lsl/lsl.sail
index fab04306..74d2b8e5 100644
--- a/test/ocaml/lsl/lsl.sail
+++ b/test/ocaml/lsl/lsl.sail
@@ -1,6 +1,3 @@
-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 >= 1.
   (bits('n), atom('shift)) -> (bits('n), bit) effect {escape}
diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail
index 83178aea..6a8c703f 100644
--- a/test/ocaml/prelude.sail
+++ b/test/ocaml/prelude.sail
@@ -1,18 +1,6 @@
 default Order dec
 
-type bits ('n : Int) = vector('n, dec, bit)
-
-infix 4 ==
-
-val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val lt_atom = "lt" : forall 'n 'm. (atom('n), atom('m)) -> bool
-val gt_atom = "gt" : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-val eq_int = "eq_int" : (int, int) -> bool
-
-val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool
+$include <prelude.sail>
 
 val eq_string = "eq_string" : (string, string) -> bool
 
@@ -25,282 +13,8 @@ val eq_anything = {
 
 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_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_dec, vector_subrange_inc}
-
-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_dec}
-
-val vector_update = "update" : forall 'n ('a : Type).
-  (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a)
-
-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)
-
-val append = "append" : forall ('n : Int) ('m : Int) ('a : Type).
-  (vector('n, dec, 'a), vector('m, dec, 'a)) -> vector('n + 'm, dec, 'a)
-
-val not_bool = "not" : bool -> bool
-
-val not_vec = "not_vec" : forall 'n. bits('n) -> bits('n)
+overload operator == = {eq_string, eq_real, eq_anything}
 
 overload ~ = {not_bool, not_vec}
 
-val neq_atom : forall 'n 'm. (atom('n), atom('m)) -> bool
-
-function neq_atom (x, y) = not_bool(eq_atom(x, y))
-
-val neq_int : (int, int) -> bool
-
-function neq_int (x, y) = not_bool(eq_int(x, y))
-
-val neq_vec : forall 'n. (bits('n), bits('n)) -> bool
-
-function neq_vec (x, y) = not_bool(eq_vec(x, y))
-
-val neq_anything : forall ('a : Type). ('a, 'a) -> bool
-
-function neq_anything (x, y) = not_bool(x == y)
-
-overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
-
-val and_bool = "and_bool" : (bool, bool) -> bool
-
-val builtin_and_vec = "and_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val and_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-function and_vec (xs, ys) = builtin_and_vec(xs, ys)
-
-overload operator & = {and_bool, and_vec}
-
-val or_bool = "or_bool" : (bool, bool) -> bool
-
-val builtin_or_vec = "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val or_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-function or_vec (xs, ys) = builtin_or_vec(xs, ys)
-
-overload operator | = {or_bool, or_vec}
-
-val UInt = "uint" : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1)
-
-val SInt = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1)
-
-val hex_slice = "hex_slice" : forall 'n 'm. (string, atom('n), atom('m)) -> bits('n - 'm)
-
-val __SetSlice_bits = "set_slice" : forall 'n 'm.
-  (atom('n), atom('m), bits('n), int, bits('m)) -> bits('n)
-
-val __SetSlice_int = "set_slice_int" : forall 'w. (atom('w), int, int, bits('w)) -> int
-
-val __raw_SetSlice_int : forall 'w. (atom('w), int, int, bits('w)) -> int
-
-val __raw_GetSlice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> bits('w)
-
-val __GetSlice_int : forall 'n. (atom('n), int, int) -> bits('n)
-
-function __GetSlice_int (n, m, o) = __raw_GetSlice_int(n, m, o)
-
-val __raw_SetSlice_bits : forall 'n 'w.
-  (atom('n), atom('w), bits('n), int, bits('w)) -> bits('n)
-
-val __raw_GetSlice_bits : forall 'n 'w.
-  (atom('n), atom('w), bits('n), int) -> bits('w)
-
-val __ShiftLeft : forall 'm. (bits('m), int) -> bits('m)
-
-val __SignExtendSlice : forall 'm. (bits('m), int, int) -> bits('m)
-
-val __ZeroExtendSlice : forall 'm. (bits('m), int, int) -> bits('m)
-
-val cast cast_unit_vec : bit -> bits(1)
-
-function cast_unit_vec bitone = 0b1
-and cast_unit_vec bitzero = 0b0
-
 val print = "print_endline" : string -> unit
-
-val putchar = "putchar" : forall ('a : Type). 'a -> unit
-
-val concat_str = "concat_str" : (string, string) -> string
-
-val DecStr : int -> string
-
-val HexStr : int -> string
-
-val BitStr = "string_of_bits" : forall 'n. bits('n) -> string
-
-val xor_vec = "xor_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val int_power : (int, int) -> int
-
-val real_power = "real_power" : (real, int) -> real
-
-overload operator ^ = {xor_vec, int_power, real_power}
-
-val add_range = "add_int" : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val add_int = "add_int" : (int, int) -> int
-
-val add_vec = "add_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val add_vec_int = "add_vec_int" : forall 'n. (bits('n), int) -> bits('n)
-
-val add_real = "add_real" : (real, real) -> real
-
-overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
-
-val sub_range = "sub_int" : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val sub_int = "sub_int" : (int, int) -> int
-
-val sub_vec : forall 'n. (bits('n), bits('n)) -> bits('n)
-
-val sub_vec_int = "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n)
-
-val sub_real = "sub_real" : (real, real) -> real
-
-val negate_range = "negate" : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
-
-val negate_int = "negate" : int -> int
-
-val negate_real = "negate_real" : real -> real
-
-overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real}
-
-overload negate = {negate_range, negate_int, negate_real}
-
-val mult_range = "mult" : forall 'n 'm 'o 'p.
-  (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p)
-
-val mult_int = "mult" : (int, int) -> int
-
-val mult_real = "mult_real" : (real, real) -> real
-
-overload operator * = {mult_range, mult_int, mult_real}
-
-val Sqrt = "sqrt_real" : real -> real
-
-val gteq_int = "gteq" : (int, int) -> bool
-
-val gteq_real = "gteq_real" : (real, real) -> bool
-
-overload operator >= = {gteq_atom, gteq_int, gteq_real}
-
-val lteq_int = "lteq" : (int, int) -> bool
-
-val lteq_real = "lteq_real" : (real, real) -> bool
-
-overload operator <= = {lteq_atom, lteq_int, lteq_real}
-
-val gt_int = "gt" : (int, int) -> bool
-
-val gt_real = "gt_real" : (real, real) -> bool
-
-overload operator > = {gt_atom, gt_int, gt_real}
-
-val lt_int = "lt" : (int, int) -> bool
-
-val lt_real = "lt_real" : (real, real) -> bool
-
-overload operator < = {lt_atom, lt_int, lt_real}
-
-val RoundDown = "round_down" : real -> int
-
-val RoundUp = "round_up" : real -> int
-
-val abs = "abs_num" : real -> real
-
-val quotient_nat = "quotient" : (nat, nat) -> nat
-
-val quotient_real = "quotient_real" : (real, real) -> real
-
-val quotient = "quotient" : (int, int) -> int
-
-infixl 7 /
-
-overload operator / = {quotient_nat, quotient, quotient_real}
-
-val modulus = "modulus" : (int, int) -> int
-
-infixl 7 %
-
-overload operator % = {modulus}
-
-val Real = "to_real" : int -> real
-
-val shl_int = "shl_int" : (int, int) -> int
-
-val shr_int = "shr_int" : (int, int) -> int
-
-val min_nat = "min_int" : (nat, nat) -> nat
-
-val min_int = "min_int" : (int, int) -> int
-
-val max_nat = "max_int" : (nat, nat) -> nat
-
-val max_int = "max_int" : (int, int) -> int
-
-overload min = {min_nat, min_int}
-
-overload max = {max_nat, max_int}
-
-val replicate_bits = "replicate_bits" : forall 'n 'm. (bits('n), atom('m)) -> bits('n * 'm)
-
-val cast ex_nat : nat -> {'n, 'n >= 0. atom('n)}
-
-function ex_nat 'n = n
-
-val cast ex_int : int -> {'n, true. atom('n)}
-
-function ex_int 'n = n
-
-val ex_range : forall 'n 'm.
-  range('n, 'm) -> {'o, 'n <= 'o & 'o <= 'm. atom('o)}
-
-val coerce_int_nat : int -> nat effect {escape}
-
-function coerce_int_nat 'x = {
-  assert(constraint('x >= 0));
-  x
-}
-
-val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
-  (bits('m), int, atom('n)) -> bits('n)
-
-val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
-
-val "print_int" : (string, int) -> unit
-
-val "print_bits" : forall 'n. (string, bits('n)) -> unit
\ No newline at end of file
diff --git a/test/ocaml/string_of_struct/sos.sail b/test/ocaml/string_of_struct/sos.sail
index 69a17e6c..ecef0e36 100644
--- a/test/ocaml/string_of_struct/sos.sail
+++ b/test/ocaml/string_of_struct/sos.sail
@@ -2,11 +2,6 @@
 struct would cause the ocaml backend to generate a bad string_of
 function for the struct */
 
-union option ('a : Type) = {
-  None : unit,
-  Some : 'a
-}
-
 struct test = {
   test1 : int,
   test2 : option(int)
diff --git a/test/ocaml/types/types.sail b/test/ocaml/types/types.sail
index d13b527c..6790140e 100644
--- a/test/ocaml/types/types.sail
+++ b/test/ocaml/types/types.sail
@@ -24,8 +24,6 @@ struct TestStruct = {
 
 register SREG : TestStruct
 
-union option ('a : Type) = {None : unit, Some : 'a}
-
 register OREG : option(byte)
 
 val main : unit -> unit effect {rreg, wreg}
diff --git a/test/ocaml/vec_32_64/vec_32_64.sail b/test/ocaml/vec_32_64/vec_32_64.sail
index 5afd421d..ac44d9ae 100644
--- a/test/ocaml/vec_32_64/vec_32_64.sail
+++ b/test/ocaml/vec_32_64/vec_32_64.sail
@@ -8,11 +8,6 @@ function get_size () = 32
 
 val only64 = { ocaml: "(fun _ -> ())" } : bits(64) -> unit
 
-val zeros : forall 'n. atom('n) -> vector('n, dec, bit)
-
-function zeros n =
-  if (n == 1 + 0) then 0b0 else 0b0 @ zeros('n - 1)
-
 val main : unit -> unit
 
 function main () = {
diff --git a/test/typecheck/pass/nzcv.sail b/test/typecheck/pass/nzcv.sail
index 6763922a..dc625084 100644
--- a/test/typecheck/pass/nzcv.sail
+++ b/test/typecheck/pass/nzcv.sail
@@ -10,6 +10,6 @@ function test nzcv = {
   Z = 0b0;
   C = 0b0;
   V = 0b0;
-  (N, Z, C, V) = nzcv;
+  (N @ Z @ C @ V) = nzcv;
   ()
 }
diff --git a/test/typecheck/pass/while_PM.sail b/test/typecheck/pass/while_PM.sail
index c148e6da..84b4f7b4 100644
--- a/test/typecheck/pass/while_PM.sail
+++ b/test/typecheck/pass/while_PM.sail
@@ -22,10 +22,12 @@ val vector_update = {ocaml: "update", lem: "update_vec_dec"} : forall 'n.
 
 register GPR00 : vector(64, dec, bit)
 
+/* FIXME: Currently this doesn't work in lem
 function test b : bit -> unit = {
-  i : int = 0;
+  i : range(0, 64) = 0;
   while i < 64 do {
     GPR00[i] = b;
-    i = i + 1
+    i = i + 1;
   }
 }
+*/
\ No newline at end of file