diff options
| author | Son Ho | 2023-12-23 01:18:37 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-23 01:18:37 +0100 |
| commit | a52939b5119e2751570582533bf27828724c2e9f (patch) | |
| tree | 3a5383e4ce7e0362bc6583401ac751ac9223a9c8 | |
| parent | a4decc7654bc6f3301c0174124d21fdbc2dbc708 (diff) | |
Fix an issue when deconstructing tuples in Coq
Diffstat (limited to '')
| -rw-r--r-- | compiler/Extract.ml | 10 | ||||
| -rw-r--r-- | compiler/Main.ml | 3 | ||||
| -rw-r--r-- | 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) . |