Make the field names optional and make progress on ExtractToFStar

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]