summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2024-06-11 14:06:23 +0200
committerSon Ho2024-06-11 14:06:23 +0200
commit2e91b90e332c473253c2ff91fd65da34eb709572 (patch)
treed7b06e270fd6a1cf69717f98db7c30e43788dad1
parentbf883726d771988c838bc6a6e1c012dfb008769c (diff)
Deactivate the use of tuple projectors in the Lean backend
Diffstat (limited to '')
-rw-r--r--compiler/Config.ml11
-rw-r--r--compiler/SymbolicToPure.ml2
-rw-r--r--tests/lean/NoNestedBorrows.lean6
3 files changed, 12 insertions, 7 deletions
diff --git a/compiler/Config.ml b/compiler/Config.ml
index cb2c86ad..584635bc 100644
--- a/compiler/Config.ml
+++ b/compiler/Config.ml
@@ -362,16 +362,19 @@ let variant_concatenate_type_name = ref true
ex.:
{[
// Rust
- struct Foo(u32)
+ struct Foo(u32, u32)
// OCaml
- type Foo = (u32)
+ type Foo = u32 * u32
]}
*)
let use_tuple_structs = ref true
-let backend_has_tuple_projectors () =
- match backend () with Lean -> true | Coq | FStar | HOL4 -> false
+let backend_has_tuple_projectors backend =
+ match backend with Lean -> true | Coq | FStar | HOL4 -> false
+
+(** Toggle the use of tuple projectors *)
+let use_tuple_projectors = ref false
(** We we use nested projectors for tuple (like: [(0, 1).snd.fst]) or do
we use better projector syntax? *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 3975107a..87f1128d 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2916,7 +2916,7 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
at once (`let (a, b, c) = x in`) *)
|| TypesUtils.type_decl_from_type_id_is_tuple_struct
ctx.type_ctx.type_infos type_id
- && not (Config.backend_has_tuple_projectors ())
+ && not !Config.use_tuple_projectors
in
if use_let_with_cons then
(* Introduce a let binding which expands the ADT *)
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 262fc79e..f0438050 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -553,12 +553,14 @@ def update_tuple (x : (U32 × U32)) : Result (U32 × U32) :=
/- [no_nested_borrows::read_tuple_struct]:
Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/
def read_tuple_struct (x : Tuple U32 U32) : Result U32 :=
- Result.ok x.#0
+ let (i, _) := x
+ Result.ok i
/- [no_nested_borrows::update_tuple_struct]:
Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/
def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
- Result.ok (1#u32, x.#1)
+ let (_, i) := x
+ Result.ok (1#u32, i)
/- [no_nested_borrows::create_tuple_struct]:
Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/