From 79af7f999e3a41e3c5f9a30819a7cc43b5397c56 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sat, 29 Jan 2022 20:30:16 +0100 Subject: Make the field names optional and make progress on ExtractToFStar --- src/CfimOfJson.ml | 2 +- src/ExtractToFStar.ml | 22 +++++++++++----------- src/Print.ml | 24 +++++++++++++++++------- src/PrintPure.ml | 10 +++++++--- src/Pure.ml | 2 +- src/PureToExtract.ml | 8 +++++++- src/Types.ml | 2 +- 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] -- cgit v1.2.3