diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Config.ml | 11 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 2 | ||||
| -rw-r--r-- | tests/lean/NoNestedBorrows.lean | 6 |
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 -/ |