From 2e91b90e332c473253c2ff91fd65da34eb709572 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 11 Jun 2024 14:06:23 +0200
Subject: Deactivate the use of tuple projectors in the Lean backend

---
 compiler/Config.ml         | 11 +++++++----
 compiler/SymbolicToPure.ml |  2 +-
 2 files changed, 8 insertions(+), 5 deletions(-)

(limited to 'compiler')

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 *)
-- 
cgit v1.2.3