Typecheck: Improve typechecking for constructors with tuple types

1 files changed, 27 insertions, 28 deletions

diff --git a/src/value.ml b/src/value.ml
index 8f8e651a..d1b945a7 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -93,6 +93,33 @@ type value =
      with a direct register read. *)
   | V_attempted_read of string
 
+let coerce_bit = function
+  | V_bit b -> b
+  | _ -> assert false
+
+let is_bit = function
+  | V_bit _ -> true
+  | _ -> false
+       
+let rec string_of_value = function
+  | 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 Sail_lib.B0 -> "bitzero"
+  | V_bit Sail_lib.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_unit -> "()"
+  | V_string str -> "\"" ^ str ^ "\""
+  | V_ref str -> "ref " ^ str
+  | V_real r -> Sail_lib.string_of_real r
+  | 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) ^ "}"
+  | V_attempted_read _ -> assert false
+
 let rec eq_value v1 v2 =
   match v1, v2 with
   | V_vector v1s, V_vector v2s when List.length v1s = List.length v2s -> List.for_all2 eq_value v1s v2s
@@ -111,12 +138,7 @@ let rec eq_value v1 v2 =
      StringMap.equal eq_value fields1 fields2
   | _, _ -> false
 
-let coerce_bit = function
-  | V_bit b -> b
-  | _ -> assert false
-
 let coerce_ctor = function
-  | V_ctor (str, [V_tuple vals]) -> (str, vals)
   | V_ctor (str, vals) -> (str, vals)
   | _ -> assert false
 
@@ -371,33 +393,10 @@ 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 is_ctor = function
   | V_ctor _ -> true
   | _ -> false
 
-let rec string_of_value = function
-  | 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 Sail_lib.B0 -> "bitzero"
-  | V_bit Sail_lib.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_unit -> "()"
-  | V_string str -> "\"" ^ str ^ "\""
-  | V_ref str -> "ref " ^ str
-  | V_real r -> Sail_lib.string_of_real r
-  | 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) ^ "}"
-  | V_attempted_read _ -> assert false
-
 let value_sign_extend = function
   | [v1; v2] -> mk_vector (Sail_lib.sign_extend (coerce_bv v1, coerce_int v2))
   | _ -> failwith "value sign_extend"