From 6dbe9e153043e5091a4d17da9bc7c3ed7d4093b1 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Dec 2023 12:23:57 +0100
Subject: Fix minor issues when extracting a structure with one field as a
 tuple

---
 compiler/Extract.ml      | 55 ++++++++++++++++++++++++++++++------------------
 compiler/ExtractTypes.ml | 11 ++++++++++
 2 files changed, 45 insertions(+), 21 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 85bdd929..20cdb20b 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -531,28 +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 =
-        (* Check if we need to extract the type as a structure *)
-        if
-          PureUtils.type_decl_from_type_id_is_tuple_struct
-            ctx.trans_ctx.type_ctx.type_infos proj.adt_id
-        then FieldId.to_string proj.field_id
-        else ctx_get_field proj.adt_id proj.field_id ctx
+      let is_tuple_struct =
+        PureUtils.type_decl_from_type_id_is_tuple_struct
+          ctx.trans_ctx.type_ctx.type_infos proj.adt_id
       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 ()
+      (* 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 *)
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 22243a4a..08064a06 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1287,6 +1287,9 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
     TypesUtils.type_decl_from_decl_id_is_tuple_struct
       ctx.trans_ctx.type_ctx.type_infos def.def_id
   in
+  let is_tuple_struct_one_field =
+    is_tuple_struct && match def.kind with Struct [ _ ] -> true | _ -> false
+  in
   let type_kind =
     if extract_body then
       if is_tuple_struct then Some Tuple
@@ -1329,6 +1332,14 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
       if is_tuple_struct then F.pp_open_hvbox fmt 0 else F.pp_open_vbox fmt 0);
   (* Open a box for "type TYPE_NAME (TYPE_PARAMS CONST_GEN_PARAMS) =" *)
   F.pp_open_hovbox fmt ctx.indent_incr;
+  (* > "@[reducible]"
+     We need this annotation, otherwise Lean sometimes doesn't manage to typecheck
+     the expressions when it needs to coerce the type.
+  *)
+  if is_tuple_struct_one_field && !backend = Lean then (
+    F.pp_print_string fmt "@[reducible]";
+    F.pp_print_space fmt ())
+  else ();
   (* > "type TYPE_NAME" *)
   let qualif = type_decl_kind_to_qualif kind type_kind in
   (match qualif with
-- 
cgit v1.2.3