Improve interpreter value printing

Some interpreter values printed in a slightly odd way, particularly enums
which were treated like constructors and therefore got printed as `X()` for
an enumeration member `X` which is not valid syntax.

This means that SMT counterexamples should be pasteable into the interpreter
more easily now

src/lib/constant_fold.ml

@@ -90,7 +90,7 @@ and exp_of_value =
   | V_bool true -> mk_lit_exp L_true
   | V_bool false -> mk_lit_exp L_false
   | V_string str -> mk_lit_exp (L_string str)
-  | V_record ctors -> mk_exp (E_struct (List.map fexp_of_ctor (StringMap.bindings ctors)))
+  | V_record fields -> mk_exp (E_struct (List.map fexp_of_ctor (StringMap.bindings fields)))
   | V_vector vs -> mk_exp (E_vector (List.map exp_of_value vs))
   | V_tuple vs -> mk_exp (E_tuple (List.map exp_of_value vs))
   | V_unit -> mk_lit_exp L_unit
@@ -103,7 +103,7 @@ and exp_of_value =
 let rec is_too_large =
   let open Value in
   function
-  | V_int _ | V_bit _ | V_bool _ | V_string _ | V_unit | V_attempted_read _ | V_real _ | V_ref _ -> false
+  | V_int _ | V_bit _ | V_bool _ | V_string _ | V_unit | V_attempted_read _ | V_real _ | V_ref _ | V_member _ -> false
   | V_vector vs | V_tuple vs | V_list vs -> List.compare_length_with vs 256 > 0
   | V_record fields -> StringMap.exists (fun _ v -> is_too_large v) fields
   | V_ctor (_, vs) -> List.exists is_too_large vs

src/lib/interpreter.ml

@@ -468,7 +468,7 @@ let rec step (E_aux (e_aux, annot) as orig_exp) =
           get_global_letbinds () >>= fun lbs ->
           let chain = build_letchain id lbs orig_exp in
           return chain
-      | Enum _ -> return (exp_of_value (V_ctor (string_of_id id, [])))
+      | Enum _ -> return (exp_of_value (V_member (string_of_id id)))
       | _ -> fail ("Couldn't find id " ^ string_of_id id)
     end
   | E_struct fexps ->
@@ -651,7 +651,7 @@ and pattern_match env (P_aux (p_aux, (l, _))) value =
       begin
         match Env.lookup_id id env with
         | Enum _ ->
-            if is_ctor value && string_of_id id = fst (coerce_ctor value) then (true, Bindings.empty)
+            if is_member value && string_of_id id = coerce_member value then (true, Bindings.empty)
             else (false, Bindings.empty)
         | _ -> (true, Bindings.singleton id (Complete_binding value))
       end

src/lib/value.ml

@@ -97,6 +97,7 @@ type value =
   | V_unit
   | V_string of string
   | V_ref of string
+  | V_member of string
   | V_ctor of string * value list
   | V_record of value StringMap.t
   (* When constant folding we disable reading registers, so a register
@@ -124,10 +125,11 @@ let rec string_of_value = function
   | V_string str -> "\"" ^ str ^ "\""
   | V_ref str -> "ref " ^ str
   | V_real r -> Sail_lib.string_of_real r
+  | V_member str -> 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)
+      "struct {"
+      ^ Util.string_of_list ", " (fun (field, v) -> field ^ " = " ^ string_of_value v) (StringMap.bindings record)
       ^ "}"
   | V_attempted_read _ -> assert false
 
@@ -143,11 +145,14 @@ let rec eq_value v1 v2 =
   | V_unit, V_unit -> true
   | V_string str1, V_string str2 -> str1 = str2
   | V_ref str1, V_ref str2 -> str1 = str2
+  | V_member name1, V_member name2 -> name1 = name2
   | V_ctor (name1, fields1), V_ctor (name2, fields2) when List.length fields1 = List.length fields2 ->
       name1 = name2 && List.for_all2 eq_value fields1 fields2
   | V_record fields1, V_record fields2 -> StringMap.equal eq_value fields1 fields2
   | _, _ -> false
 
+let coerce_member = function V_member str -> str | _ -> assert false
+
 let coerce_ctor = function V_ctor (str, vals) -> (str, vals) | _ -> assert false
 
 let coerce_bool = function V_bool b -> b | _ -> assert false
@@ -399,6 +404,8 @@ let value_count_leading_zeros = function
   | [v1] -> V_int (Sail_lib.count_leading_zeros (coerce_bv v1))
   | _ -> failwith "value count_leading_zeros"
 
+let is_member = function V_member _ -> true | _ -> false
+
 let is_ctor = function V_ctor _ -> true | _ -> false
 
 let value_sign_extend = function

src/sail_smt_backend/smtlib.ml

@@ -655,7 +655,7 @@ let rec value_of_sexpr sexpr =
       match sexpr with
       | Atom name -> begin
           match List.find_opt (fun member -> Util.zencode_string (string_of_id member) = name) members with
-          | Some member -> V_ctor (string_of_id member, [])
+          | Some member -> V_member (string_of_id member)
           | None ->
               failwith
                 ("Could not find enum member for " ^ name ^ " in " ^ Util.string_of_list ", " string_of_id members)