summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/CfimOfJson.ml2
-rw-r--r--src/ExtractToFStar.ml22
-rw-r--r--src/Print.ml24
-rw-r--r--src/PrintPure.ml10
-rw-r--r--src/Pure.ml2
-rw-r--r--src/PureToExtract.ml8
-rw-r--r--src/Types.ml2
7 files changed, 45 insertions, 25 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 82f9d95a..3378f548 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -134,7 +134,7 @@ let field_of_json (js : json) : (T.field, string) result =
combine_error_msgs js "field_of_json"
(match js with
| `Assoc [ ("name", name); ("ty", ty) ] ->
- let* name = string_of_json name in
+ let* name = option_of_json string_of_json name in
let* ty = sty_of_json ty in
Ok { T.field_name = name; field_ty = ty }
| _ -> Error "")
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 35d15607..4491a722 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -89,7 +89,7 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_close_box fmt ()
let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
- (def : type_def) (type_name : string) (type_params : string list)
+ (def : type_def) (def_name : string) (type_params : string list)
(variants : variant list) : unit =
(* We want to generate a definition which looks like this:
* ```
@@ -151,17 +151,17 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
let var_id = VarId.of_int (FieldId.to_int fid) in
let ctx, field_name = ctx_add_var field_name var_id ctx in
F.pp_print_string fmt (field_name ^ " :");
- F.pp_space fmt ();
+ F.pp_print_space fmt ();
ctx
in
(* Print the field type *)
extract_ty ctx fmt false f.field_ty;
(* Print the arrow `->`*)
- F.pp_space fmt ();
- F.pp_print_string "->";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "->";
(* Close the field box *)
F.pp_close_box fmt ();
- F.pp_space fmt ();
+ F.pp_print_space fmt ();
(* Return *)
ctx
in
@@ -171,14 +171,14 @@ let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
List.fold_left (fun ctx (fid, f) -> print_field fid f ctx) ctx fields
in
(* Print the final type *)
- F.pp_open_hovbox fmt ();
- F.pp_string fmt def_name;
+ F.pp_open_hovbox fmt 0;
+ F.pp_print_string fmt def_name;
List.iter
(fun type_param ->
- F.pp_space fmt ();
- F.pp_string fmt type_param)
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt type_param)
type_params;
- F.pp_close_hovbox fmt ();
+ F.pp_close_box fmt ();
(* Close the variant box *)
F.pp_close_box fmt ()
in
@@ -216,7 +216,7 @@ let rec extract_type_def (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt def_name;
(match def.kind with
- | Struct fields -> extract_type_def_struct_body ctx_body fmt fields
+ | Struct fields -> extract_type_def_struct_body ctx_body fmt def fields
| Enum variants ->
extract_type_def_enum_body ctx_body fmt def def_name type_params variants);
ctx
diff --git a/src/Print.ml b/src/Print.ml
index 78a826bf..8124df52 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -110,7 +110,9 @@ module Types = struct
ty_to_string fmt ty
let field_to_string fmt (f : T.field) : string =
- f.field_name ^ " : " ^ ty_to_string fmt f.field_ty
+ match f.field_name with
+ | Some field_name -> field_name ^ " : " ^ ty_to_string fmt f.field_ty
+ | None -> ty_to_string fmt f.field_ty
let variant_to_string fmt (v : T.variant) : string =
v.variant_name ^ "("
@@ -511,9 +513,15 @@ module Contexts = struct
fun def_id opt_variant_id ->
let def = T.TypeDefId.Map.find def_id ctx in
let fields = TU.type_def_get_fields def opt_variant_id in
- (* TODO: the field name should be optional?? *)
- let fields = List.map (fun f -> f.T.field_name) fields in
- Some fields
+ (* There are two cases: either all the fields have names, or none of them
+ * has names *)
+ let has_names =
+ List.exists (fun f -> Option.is_some f.T.field_name) fields
+ in
+ if has_names then
+ let fields = List.map (fun f -> Option.get f.T.field_name) fields in
+ Some fields
+ else None
let eval_ctx_to_ctx_formatter (ctx : C.eval_ctx) : ctx_formatter =
(* We shouldn't use rvar_to_string *)
@@ -596,7 +604,7 @@ module CfimAst = struct
type_def_id_to_string : T.TypeDefId.id -> string;
adt_variant_to_string : T.TypeDefId.id -> T.VariantId.id -> string;
adt_field_to_string :
- T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string;
+ T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string option;
var_id_to_string : V.VarId.id -> string;
adt_field_names :
T.TypeDefId.id -> T.VariantId.id option -> string list option;
@@ -639,7 +647,7 @@ module CfimAst = struct
}
let type_ctx_to_adt_field_to_string_fun (ctx : T.type_def T.TypeDefId.Map.t) :
- T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string =
+ T.TypeDefId.id -> T.VariantId.id option -> T.FieldId.id -> string option =
fun def_id opt_variant_id field_id ->
let def = T.TypeDefId.Map.find def_id ctx in
let fields = TU.type_def_get_fields def opt_variant_id in
@@ -722,7 +730,9 @@ module CfimAst = struct
"(" ^ s ^ ")." ^ T.FieldId.to_string fid
| E.Field (E.ProjAdt (adt_id, opt_variant_id), fid) -> (
let field_name =
- fmt.adt_field_to_string adt_id opt_variant_id fid
+ match fmt.adt_field_to_string adt_id opt_variant_id fid with
+ | Some field_name -> field_name
+ | None -> T.FieldId.to_string fid
in
match opt_variant_id with
| None -> "(" ^ s ^ ")." ^ field_name
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index b4816e14..0325e60c 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -41,7 +41,7 @@ type ast_formatter = {
adt_variant_to_string : TypeDefId.id -> VariantId.id -> string;
var_id_to_string : VarId.id -> string;
adt_field_to_string :
- TypeDefId.id -> VariantId.id option -> FieldId.id -> string;
+ TypeDefId.id -> VariantId.id option -> FieldId.id -> string option;
adt_field_names : TypeDefId.id -> VariantId.id option -> string list option;
fun_def_id_to_string : A.FunDefId.id -> string;
}
@@ -149,7 +149,9 @@ let rec ty_to_string (fmt : type_formatter) (ty : ty) : string =
| Slice sty -> "[" ^ ty_to_string fmt sty ^ "]"
let field_to_string fmt (f : field) : string =
- f.field_name ^ " : " ^ ty_to_string fmt f.field_ty
+ match f.field_name with
+ | None -> ty_to_string fmt f.field_ty
+ | Some field_name -> field_name ^ " : " ^ ty_to_string fmt f.field_ty
let variant_to_string fmt (v : variant) : string =
v.variant_name ^ "("
@@ -202,7 +204,9 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)
| E.ProjTuple _ -> "(" ^ s ^ ")." ^ T.FieldId.to_string pe.field_id
| E.ProjAdt (adt_id, opt_variant_id) -> (
let field_name =
- fmt.adt_field_to_string adt_id opt_variant_id pe.field_id
+ match fmt.adt_field_to_string adt_id opt_variant_id pe.field_id with
+ | Some field_name -> field_name
+ | None -> T.FieldId.to_string pe.field_id
in
match opt_variant_id with
| None -> "(" ^ s ^ ")." ^ field_name
diff --git a/src/Pure.ml b/src/Pure.ml
index 139b4c58..53c053b0 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -100,7 +100,7 @@ type ty =
polymorphic = false;
}]
-type field = { field_name : string; field_ty : ty } [@@deriving show]
+type field = { field_name : string option; field_ty : ty } [@@deriving show]
type variant = { variant_name : string; fields : field list } [@@deriving show]
diff --git a/src/PureToExtract.ml b/src/PureToExtract.ml
index f2c03b90..5313569a 100644
--- a/src/PureToExtract.ml
+++ b/src/PureToExtract.ml
@@ -35,10 +35,16 @@ type name_formatter = {
char_name : string;
int_name : integer_type -> string;
str_name : string;
- field_name : name -> string -> string;
+ field_name : name -> string option -> string;
(** Inputs:
- type name
- field name
+
+ Note that fields don't always have names, but we still need to
+ generate some names if we want to extract the structures to records...
+ We might want to extract such structures to tuples, later, but field
+ access then causes trouble because not all provers accept syntax like
+ `x.3` where `x` is a tuple.
*)
variant_name : name -> string -> string;
(** Inputs:
diff --git a/src/Types.ml b/src/Types.ml
index 4e9c69c8..70ab3978 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -182,7 +182,7 @@ type ety = erased_region ty [@@deriving show, ord]
Used in function bodies, "regular" value types, etc.
*)
-type field = { field_name : string; field_ty : sty } [@@deriving show]
+type field = { field_name : string option; field_ty : sty } [@@deriving show]
type variant = { variant_name : string; fields : field list } [@@deriving show]
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 14:18:42 +0000