Merge pull request #49 from AeneasVerif/son_merge_back

Allow the extraction of structures as tuples

1 files changed, 75 insertions, 40 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index e48e6ae6..20cdb20b 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -111,7 +111,7 @@ let extract_global_decl_register_names (ctx : extraction_ctx)
     context updated with new bindings.
 
     [is_single_pat]: are we extracting a single pattern (a pattern for a let-binding
-    or a lambda).
+    or a lambda)?
 
     TODO: we don't need something very generic anymore (some definitions used
     to be polymorphic).
@@ -121,38 +121,53 @@ let extract_adt_g_value
     (fmt : F.formatter) (ctx : extraction_ctx) (is_single_pat : bool)
     (inside : bool) (variant_id : VariantId.id option) (field_values : 'v list)
     (ty : ty) : extraction_ctx =
+  let extract_as_tuple () =
+    (* This is very annoying: in Coq, we can't write [()] for the value of
+       type [unit], we have to write [tt]. *)
+    if !backend = Coq && field_values = [] then (
+      F.pp_print_string fmt "tt";
+      ctx)
+    else
+      (* If there is exactly one value, we don't print the parentheses *)
+      let lb, rb =
+        if List.length field_values = 1 then ("", "") else ("(", ")")
+      in
+      F.pp_print_string fmt lb;
+      let ctx =
+        Collections.List.fold_left_link
+          (fun () ->
+            F.pp_print_string fmt ",";
+            F.pp_print_space fmt ())
+          (fun ctx v -> extract_value ctx false v)
+          ctx field_values
+      in
+      F.pp_print_string fmt rb;
+      ctx
+  in
   match ty with
   | TAdt (TTuple, generics) ->
       (* Tuple *)
       (* For now, we only support fully applied tuple constructors *)
       assert (List.length generics.types = List.length field_values);
       assert (generics.const_generics = [] && generics.trait_refs = []);
-      (* This is very annoying: in Coq, we can't write [()] for the value of
-         type [unit], we have to write [tt]. *)
-      if !backend = Coq && field_values = [] then (
-        F.pp_print_string fmt "tt";
-        ctx)
-      else (
-        F.pp_print_string fmt "(";
-        let ctx =
-          Collections.List.fold_left_link
-            (fun () ->
-              F.pp_print_string fmt ",";
-              F.pp_print_space fmt ())
-            (fun ctx v -> extract_value ctx false v)
-            ctx field_values
-        in
-        F.pp_print_string fmt ")";
-        ctx)
+      extract_as_tuple ()
   | TAdt (adt_id, _) ->
       (* "Regular" ADT *)
-
-      (* If we are generating a pattern for a let-binding and we target Lean,
-         the syntax is: `let ⟨ x0, ..., xn ⟩ := ...`.
-
-         Otherwise, it is: `let Cons x0 ... xn = ...`
-      *)
-      if is_single_pat && !Config.backend = Lean then (
+      (* We may still extract the ADT as a tuple, if none of the fields are
+         named *)
+      if
+        PureUtils.type_decl_from_type_id_is_tuple_struct
+          ctx.trans_ctx.type_ctx.type_infos adt_id
+      then (* Extract as a tuple *)
+        extract_as_tuple ()
+      else if
+        (* If we are generating a pattern for a let-binding and we target Lean,
+           the syntax is: `let ⟨ x0, ..., xn ⟩ := ...`.
+
+           Otherwise, it is: `let Cons x0 ... xn = ...`
+        *)
+        is_single_pat && !Config.backend = Lean
+      then (
         F.pp_print_string fmt "⟨";
         F.pp_print_space fmt ();
         let ctx =
@@ -516,21 +531,41 @@ and extract_field_projector (ctx : extraction_ctx) (fmt : F.formatter)
    * projection ([x.field] instead of [MkAdt?.field x] *)
   match args with
   | [ arg ] ->
-      (* Exactly one argument: pretty-print *)
-      let field_name = ctx_get_field proj.adt_id proj.field_id ctx in
-      (* Open a box *)
-      F.pp_open_hovbox fmt ctx.indent_incr;
-      (* Extract the expression *)
-      extract_texpression ctx fmt true arg;
-      (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
-      if !backend <> Lean then F.pp_print_break fmt 0 0;
-      F.pp_print_string fmt ".";
-      (* If in Coq, the field projection has to be parenthesized *)
-      (match !backend with
-      | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
-      | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
-      (* Close the box *)
-      F.pp_close_box fmt ()
+      let is_tuple_struct =
+        PureUtils.type_decl_from_type_id_is_tuple_struct
+          ctx.trans_ctx.type_ctx.type_infos proj.adt_id
+      in
+      (* Check if we extract the type as a tuple, and it only has one field.
+         In this case, there is no projection. *)
+      let has_one_field =
+        match proj.adt_id with
+        | TAdtId id -> (
+            let d = TypeDeclId.Map.find id ctx.trans_types in
+            match d.kind with Struct [ _ ] -> true | _ -> false)
+        | _ -> false
+      in
+      if is_tuple_struct && has_one_field then
+        extract_texpression ctx fmt inside arg
+      else
+        (* Exactly one argument: pretty-print *)
+        let field_name =
+          (* Check if we need to extract the type as a tuple *)
+          if is_tuple_struct then FieldId.to_string proj.field_id
+          else ctx_get_field proj.adt_id proj.field_id ctx
+        in
+        (* Open a box *)
+        F.pp_open_hovbox fmt ctx.indent_incr;
+        (* Extract the expression *)
+        extract_texpression ctx fmt true arg;
+        (* We allow to break where the "." appears (except Lean, it's a syntax error) *)
+        if !backend <> Lean then F.pp_print_break fmt 0 0;
+        F.pp_print_string fmt ".";
+        (* If in Coq, the field projection has to be parenthesized *)
+        (match !backend with
+        | FStar | Lean | HOL4 -> F.pp_print_string fmt field_name
+        | Coq -> F.pp_print_string fmt ("(" ^ field_name ^ ")"));
+        (* Close the box *)
+        F.pp_close_box fmt ()
   | arg :: args ->
       (* Call extract_App again, but in such a way that the first argument is
        * isolated *)