summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-12-23 01:18:37 +0100
committerSon Ho2023-12-23 01:18:37 +0100
commita52939b5119e2751570582533bf27828724c2e9f (patch)
tree3a5383e4ce7e0362bc6583401ac751ac9223a9c8
parenta4decc7654bc6f3301c0174124d21fdbc2dbc708 (diff)
Fix an issue when deconstructing tuples in Coq
Diffstat (limited to '')
-rw-r--r--compiler/Extract.ml10
-rw-r--r--compiler/Main.ml3
-rw-r--r--tests/coq/misc/Loops.v4
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)
.