From a52939b5119e2751570582533bf27828724c2e9f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 01:18:37 +0100
Subject: Fix an issue when deconstructing tuples in Coq

---
 compiler/Extract.ml    | 10 ++++++++--
 compiler/Main.ml       |  3 ---
 tests/coq/misc/Loops.v |  4 ++--
 3 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 30b76ceb..87dcb1fd 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -132,9 +132,15 @@ let extract_adt_g_value
       F.pp_print_string fmt "tt";
       ctx)
     else
-      (* If there is exactly one value, we don't print the parentheses *)
+      (* If there is exactly one value, we don't print the parentheses.
+         Also, for Coq, we need the special syntax ['(...)] if we destruct
+         a tuple pattern in a let-binding and the tuple has > 2 values.
+      *)
       let lb, rb =
-        if List.length field_values = 1 then ("", "") else ("(", ")")
+        if List.length field_values = 1 then ("", "")
+        else if !backend = Coq && is_single_pat && List.length field_values > 2
+        then ("'(", ")")
+        else ("(", ")")
       in
       F.pp_print_string fmt lb;
       let ctx =
diff --git a/compiler/Main.ml b/compiler/Main.ml
index abc27b46..0b8ec439 100644
--- a/compiler/Main.ml
+++ b/compiler/Main.ml
@@ -196,9 +196,6 @@ let () =
   let _ =
     match !backend with
     | FStar ->
-        (* Some patterns are not supported *)
-        decompose_monadic_let_bindings := false;
-        decompose_nested_let_patterns := false;
         (* F* can disambiguate the field names *)
         record_fields_short_names := true
     | Coq ->
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index cc76f359..af920d41 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -358,7 +358,7 @@ Fixpoint list_nth_mut_loop_pair_loop
         else (
           i1 <- u32_sub i 1%u32;
           t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
-          let (p, back_'a, back_'b) := t in
+          let '(p, back_'a, back_'b) := t in
           let back_'a1 :=
             fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
           let back_'b1 :=
@@ -378,7 +378,7 @@ Definition list_nth_mut_loop_pair
   result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
   :=
   t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i;
-  let (p, back_'a, back_'b) := t in
+  let '(p, back_'a, back_'b) := t in
   Return (p, back_'a, back_'b)
 .
 
-- 
cgit v1.2.3