Lots of experimental changes on this branch

* Changed comment syntax to C-style /* */ and //

* References to registers and mutable variables are never created
implicitly - a reference to a register or variable R is now created
via the expression "ref R". References are assigned like "(*Y) = X",
with "(*ref R) = X" being equivalent to "R = X". Everything is always
explicit now, which simplifies the logic in the typechecker. There's
also now an invariant that every id directly in a LEXP is mutable,
which is actually required for our rewriter steps to be sound.

* More flexible syntax for L-expressions to better support wierd
power-idioms, some syntax sugar means that:

X.GET(a, b, c)  ==>  _mod_GET(X, a, b, c)
X->GET(a, b, c)  ==>  _mod_GET(ref X, a, b, c)

for setters, this can be combined with the (still somewhat poorly
named) LEXP_memory construct, such that:

X->SET(a, b, c) = Y  ==>  _mod_SET(ref X, a, b, c, Y)

Currently I use the _mod_ prefix for these 'modifier' functions, but
we could omit that a la rust.

* The register bits typedef construct no longer exists in the
typechecker. This construct never worked consistently between backends
and inc/dec vectors, and it can be easily replaced by structs with
fancy setters/getters if need be. One can also use custom type operators to mimic the syntax, i.e.

type operator ... ('n : Int) ('m : Int) = slice('n, 'm)

struct cr = {
  CR0 : 32 ... 35,
  /* 32 : LT; 33 : GT; 34 : EQ; 35 : SO; */
  CR1 : 36 ... 39,
  /* 36 : FX; 37 : FEX; 38 : VX; 39 : OX; */
  CR2 : 40 ... 43,
  CR3 : 44 ... 47,
  CR4 : 48 ... 51,
  CR5 : 52 ... 55,
  CR6 : 56 ... 59,
  CR7 : 60 ... 63,
}

This greatly simplifies a lot of the logic in the typechecker, as it
means that E_field is no longer ambiguously overloaded between records
and register bit typedefs. This also makes writing semantics for these
constructs much simpler.

1 files changed, 13 insertions, 2 deletions

diff --git a/src/value.ml b/src/value.ml
index 59dadafe..d9690899 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -61,6 +61,7 @@ type value =
   | V_tuple of value list
   | V_unit
   | V_string of string
+  | V_ref of string
   | V_ctor of string * value list
   | V_record of value StringMap.t
 
@@ -127,6 +128,10 @@ let coerce_string = function
   | V_string str -> str
   | _ -> assert false
 
+let coerce_ref = function
+  | V_ref str -> str
+  | _ -> assert false
+
 let unit_value = V_unit
 
 let value_eq_int = function
@@ -221,17 +226,23 @@ let value_replicate_bits = function
   | [v1; v2] -> mk_vector (Sail_lib.replicate_bits (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value replicate_bits"
 
+let is_bit = function
+  | V_bit _ -> true
+  | _ -> false
+
 let rec string_of_value = function
-  | V_vector vs -> Sail_lib.string_of_bits (List.map coerce_bit vs)
+  | V_vector vs when List.for_all is_bit vs -> Sail_lib.string_of_bits (List.map coerce_bit vs)
+  | V_vector vs -> "[" ^ Util.string_of_list ", " string_of_value vs ^ "]"
   | V_bool true -> "true"
   | V_bool false -> "false"
   | V_bit B0 -> "bitzero"
   | V_bit B1 -> "bitone"
   | V_int n -> Big_int.to_string n
   | V_tuple vals -> "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
-  | V_list vals -> "[" ^ Util.string_of_list ", " string_of_value vals ^ "]"
+  | V_list vals -> "[|" ^ Util.string_of_list ", " string_of_value vals ^ "|]"
   | V_unit -> "()"
   | V_string str -> "\"" ^ str ^ "\""
+  | V_ref str -> "ref " ^ str
   | V_ctor (str, vals) -> str ^ "(" ^ Util.string_of_list ", " string_of_value vals ^ ")"
   | V_record record ->
      "{" ^ Util.string_of_list ", " (fun (field, v) -> field ^ "=" ^ string_of_value v) (StringMap.bindings record) ^ "}"