summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Print.ml64
-rw-r--r--src/Substitute.ml18
-rw-r--r--src/Types.ml15
3 files changed, 64 insertions, 33 deletions
diff --git a/src/Print.ml b/src/Print.ml
index 30a7453a..24e038f9 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -161,7 +161,8 @@ module Values = struct
type_def_id_to_string : T.TypeDefId.id -> string;
adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
var_id_to_string : V.VarId.id -> string;
- (* TODO: add and use an adt_field_names : ... -> (string list) option *)
+ adt_field_names :
+ T.TypeDefId.id -> T.VariantId.id option -> string list option;
}
let value_to_etype_formatter (fmt : value_formatter) : PT.etype_formatter =
@@ -223,12 +224,21 @@ module Values = struct
| None -> fmt.type_def_id_to_string av.def_id
in
let field_values = T.FieldId.vector_to_list av.field_values in
+ let field_values = List.map (typed_value_to_string fmt) field_values in
if List.length field_values > 0 then
- let field_values =
- String.concat " "
- (List.map (typed_value_to_string fmt) field_values)
- in
- adt_ident ^ " " ^ field_values
+ match fmt.adt_field_names av.V.def_id av.V.variant_id with
+ | None ->
+ let field_values = String.concat ", " field_values in
+ adt_ident ^ " (" ^ field_values ^ ")"
+ | Some field_names ->
+ let field_values = List.combine field_names field_values in
+ let field_values =
+ List.map
+ (fun (field, value) -> field ^ " = " ^ value ^ ";")
+ field_values
+ in
+ let field_values = String.concat "; " field_values in
+ adt_ident ^ " { " ^ field_values ^ " }"
else adt_ident
| Tuple values ->
let values = T.FieldId.vector_to_list values in
@@ -436,12 +446,21 @@ module Contexts = struct
let var = C.ctx_lookup_var ctx vid in
PV.var_to_string var
in
+ let adt_field_names (def_id : T.TypeDefId.id)
+ (opt_variant_id : T.VariantId.id option) =
+ let def = C.ctx_lookup_type_def ctx def_id in
+ let fields = T.type_def_get_fields def opt_variant_id in
+ (* TODO: the field name should be optional?? *)
+ let fields = T.FieldId.map (fun f -> f.T.field_name) fields in
+ Some (T.FieldId.vector_to_list fields)
+ in
{
r_to_string;
type_var_id_to_string;
type_def_id_to_string;
adt_variant_to_string;
var_id_to_string;
+ adt_field_names;
}
(** Split an [env] at every occurrence of [Frame], eliminating those elements.
@@ -484,6 +503,8 @@ module CfimAst = struct
adt_field_to_string :
T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string;
var_id_to_string : V.VarId.id -> string;
+ adt_field_names :
+ T.TypeDefId.id -> T.VariantId.id option -> string list option;
fun_def_id_to_string : A.FunDefId.id -> string;
}
@@ -494,6 +515,7 @@ module CfimAst = struct
PV.type_def_id_to_string = fmt.type_def_id_to_string;
PV.adt_variant_to_string = fmt.adt_variant_to_string;
PV.var_id_to_string = fmt.var_id_to_string;
+ PV.adt_field_names = fmt.adt_field_names;
}
let ast_to_etype_formatter (fmt : ast_formatter) : PT.etype_formatter =
@@ -584,16 +606,28 @@ module CfimAst = struct
let ops = List.map (operand_to_string fmt) ops in
match akind with
| E.AggregatedTuple -> "(" ^ String.concat ", " ops ^ ")"
- | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) -> (
+ | E.AggregatedAdt (def_id, opt_variant_id, _regions, _types) ->
let adt_name = fmt.type_def_id_to_string def_id in
- match opt_variant_id with
- | None -> adt_name ^ "{ " ^ String.concat ", " ops ^ " }"
- | Some variant_id ->
- let variant_name =
- fmt.adt_variant_to_string def_id variant_id
- in
- adt_name ^ "::" ^ variant_name ^ "(" ^ String.concat ", " ops
- ^ ")"))
+ let variant_name =
+ match opt_variant_id with
+ | None -> adt_name
+ | Some variant_id ->
+ adt_name ^ "::" ^ fmt.adt_variant_to_string def_id variant_id
+ in
+ let fields =
+ match fmt.adt_field_names def_id opt_variant_id with
+ | None -> "(" ^ String.concat ", " ops ^ ")"
+ | Some field_names ->
+ let fields = List.combine field_names ops in
+ let fields =
+ List.map
+ (fun (field, value) -> field ^ " = " ^ value ^ ";")
+ fields
+ in
+ let fields = String.concat " " fields in
+ "{ " ^ fields ^ " }"
+ in
+ variant_name ^ " " ^ fields)
let statement_to_string (fmt : ast_formatter) (st : A.statement) : string =
match st with
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 8cb92587..cad61595 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -51,24 +51,6 @@ let make_type_subst (var_ids : T.TypeVarId.id list) (tys : 'r T.ty list) :
in
fun id -> T.TypeVarId.Map.find id mp
-(** Retrieve the list of fields for the given variant of a [type_def].
-
- Raises [Invalid_argument] if the arguments are incorrect.
-
- TODO: move
- *)
-let type_def_get_fields (def : T.type_def)
- (opt_variant_id : T.VariantId.id option) : T.field T.FieldId.vector =
- match (def.kind, opt_variant_id) with
- | Enum variants, Some variant_id ->
- (T.VariantId.nth variants variant_id).fields
- | Struct fields, None -> fields
- | _ ->
- raise
- (Invalid_argument
- "The variant id should be [Some] if and only if the definition is \
- an enumeration")
-
(** Instantiate the type variables in an ADT definition, and return the list
of types of the fields for the chosen variant *)
let type_def_get_instantiated_field_type (def : T.type_def)
diff --git a/src/Types.ml b/src/Types.ml
index abcd0e28..ae2f0958 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -123,3 +123,18 @@ let rec erase_regions (ty : rty) : ety =
let regions = List.map (fun _ -> Erased) regions in
let tys = List.map erase_regions tys in
Assumed (aty, regions, tys)
+
+(** Retrieve the list of fields for the given variant of a [type_def].
+
+ Raises [Invalid_argument] if the arguments are incorrect.
+ *)
+let type_def_get_fields (def : type_def) (opt_variant_id : VariantId.id option)
+ : field FieldId.vector =
+ match (def.kind, opt_variant_id) with
+ | Enum variants, Some variant_id -> (VariantId.nth variants variant_id).fields
+ | Struct fields, None -> fields
+ | _ ->
+ raise
+ (Invalid_argument
+ "The variant id should be [Some] if and only if the definition is \
+ an enumeration")