diff options
Diffstat (limited to 'src/jib/jib_util.ml')
| -rw-r--r-- | src/jib/jib_util.ml | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml index bec4ce75..821cdabc 100644 --- a/src/jib/jib_util.ml +++ b/src/jib/jib_util.ml @@ -167,8 +167,6 @@ let name id = Name (id, -1) let rec cval_rename from_id to_id = function | V_id (id, ctyp) when Name.compare id from_id = 0 -> V_id (to_id, ctyp) | V_id (id, ctyp) -> V_id (id, ctyp) - | V_ref (id, ctyp) when Name.compare id from_id = 0 -> V_ref (to_id, ctyp) - | V_ref (id, ctyp) -> V_ref (id, ctyp) | V_lit (vl, ctyp) -> V_lit (vl, ctyp) | V_call (call, cvals) -> V_call (call, List.map (cval_rename from_id to_id) cvals) | V_field (f, field) -> V_field (cval_rename from_id to_id f, field) @@ -351,24 +349,28 @@ and full_string_of_ctyp = function | CT_ref ctyp -> "ref(" ^ full_string_of_ctyp ctyp ^ ")" | ctyp -> string_of_ctyp ctyp -let string_of_value = function - | VL_bits ([], _) -> "empty" - | VL_bits (bs, true) -> Sail2_values.show_bitlist bs - | VL_bits (bs, false) -> Sail2_values.show_bitlist (List.rev bs) - | VL_int i -> Big_int.to_string i +let rec string_of_value = function + | VL_bits ([], _) -> "UINT64_C(0)" + | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")" + | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")" + | VL_int i -> Big_int.to_string i ^ "l" | VL_bool true -> "true" | VL_bool false -> "false" - | VL_null -> "NULL" - | VL_unit -> "()" - | VL_bit Sail2_values.B0 -> "bitzero" - | VL_bit Sail2_values.B1 -> "bitone" - | VL_bit Sail2_values.BU -> "bitundef" + | VL_unit -> "UNIT" + | VL_bit Sail2_values.B0 -> "UINT64_C(0)" + | VL_bit Sail2_values.B1 -> "UINT64_C(1)" + | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value" | VL_real str -> str | VL_string str -> "\"" ^ str ^ "\"" + | VL_matcher (n, uid) -> Printf.sprintf "matcher(%d, %d)" n uid + | VL_tuple values -> "(" ^ Util.string_of_list ", " string_of_value values ^ ")" + | VL_list [] -> "NULL" + | VL_list values -> "[|" ^ Util.string_of_list ", " string_of_value values ^ "|]" + | VL_enum element -> Util.zencode_string element + | VL_ref r -> "&" ^ Util.zencode_string r let rec string_of_cval = function | V_id (id, ctyp) -> string_of_name id - | V_ref (id, _) -> "&" ^ string_of_name id | V_lit (vl, ctyp) -> string_of_value vl | V_call (op, cvals) -> Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " string_of_cval cvals) @@ -585,7 +587,7 @@ let rec is_polymorphic = function | CT_poly -> true let rec cval_deps = function - | V_id (id, _) | V_ref (id, _) -> NameSet.singleton id + | V_id (id, _) -> NameSet.singleton id | V_lit _ -> NameSet.empty | V_field (cval, _) | V_poly (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval | V_call (_, cvals) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals) @@ -659,7 +661,6 @@ let rec map_clexp_ctyp f = function let rec map_cval_ctyp f = function | V_id (id, ctyp) -> V_id (id, f ctyp) - | V_ref (id, ctyp) -> V_ref (id, f ctyp) | V_lit (vl, ctyp) -> V_lit (vl, f ctyp) | V_ctor_kind (cval, id, unifiers, ctyp) -> V_ctor_kind (map_cval_ctyp f cval, id, List.map f unifiers, f ctyp) @@ -893,7 +894,6 @@ let rec infer_call op vs = and cval_ctyp = function | V_id (_, ctyp) -> ctyp - | V_ref (_, ctyp) -> CT_ref ctyp | V_lit (vl, ctyp) -> ctyp | V_ctor_kind _ -> CT_bool | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> ctyp |