From 71834958a958523a4881d822e729af1ddd78c9df Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 10:56:28 +0200
Subject: Add printing of projectors for recursive structs in Lean backend

---
 compiler/ExtractTypes.ml | 133 +++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 130 insertions(+), 3 deletions(-)

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 6a6067de..4272e7a9 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1662,6 +1662,127 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
         (* Add breaks to insert new lines between definitions *)
         F.pp_print_break fmt 0 0
 
+(** Auxiliary function.
+
+    Generate field projectors in Lean.
+
+    Recursive structs are defined as inductives in Lean.
+    Field projectors allow to retrieve the facilities provided by
+    Lean structures.
+ *)
+let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
+    (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
+  sanity_check __FILE__ __LINE__ (!backend = Lean) decl.meta;
+  match decl.kind with
+  | Opaque | Enum _ -> ()
+  | Struct fields ->
+      (* Records are extracted as inductives only if they are recursive *)
+      let is_rec = decl_is_from_rec_group kind in
+      if is_rec then
+        (* Add the type params *)
+        let ctx, type_params, cg_params, trait_clauses =
+          ctx_add_generic_params decl.meta decl.llbc_name decl.llbc_generics
+            decl.generics ctx
+        in
+        (* Record_var will be the ADT argument to the projector *)
+        let ctx, record_var = ctx_add_var decl.meta "x" (VarId.of_int 0) ctx in
+        (* Field_var will be the variable in the constructor that is returned by the projector *)
+        let ctx, field_var = ctx_add_var decl.meta "x" (VarId.of_int 1) ctx in
+        (* Name of the ADT *)
+        let def_name = ctx_get_local_type decl.meta decl.def_id ctx in
+        (* Name of the ADT constructor. As we are in the struct case, we only have
+           one constructor *)
+        let cons_name = ctx_get_struct decl.meta (TAdtId decl.def_id) ctx in
+
+        let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
+          F.pp_print_space fmt ();
+          (* Box for the projector definition *)
+          F.pp_open_hvbox fmt 0;
+          (* Box for the [def ADT.proj ... :=] *)
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          F.pp_print_string fmt "def";
+          F.pp_print_space fmt ();
+
+          (* Print the function name. In Lean, the syntax ADT.proj will
+             allow us to call x.proj for any x of type ADT *)
+          let field_name =
+            ctx_get_field decl.meta (TAdtId decl.def_id) field_id ctx
+          in
+          F.pp_print_string fmt def_name;
+          F.pp_print_string fmt ".";
+          F.pp_print_string fmt field_name;
+
+          (* Print the generics *)
+          let as_implicits = true in
+          extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty
+            ~as_implicits decl.generics type_params cg_params trait_clauses;
+
+          (* Print the record parameter as "(x : ADT)" *)
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "(";
+          F.pp_print_string fmt record_var;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt def_name;
+          List.iter
+            (fun p ->
+              F.pp_print_space fmt ();
+              F.pp_print_string fmt p)
+            type_params;
+          F.pp_print_string fmt ")";
+
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt ":=";
+
+          (* Close the box for the [def ADT.proj ... :=] *)
+          F.pp_close_box fmt ();
+          F.pp_print_space fmt ();
+
+          (* Open a box for the whole match *)
+          F.pp_open_hvbox fmt 0;
+
+          (* Open a box for the [match ... with] *)
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          F.pp_print_string fmt "match";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt record_var;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "with";
+          (* Close the box for the [match ... with] *)
+          F.pp_close_box fmt ();
+
+          (* Open a box for the branch *)
+          F.pp_open_hovbox fmt ctx.indent_incr;
+          (* Print the match branch *)
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "|";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt cons_name;
+          FieldId.iteri
+            (fun id _ ->
+              F.pp_print_space fmt ();
+              if field_id = id then F.pp_print_string fmt field_var
+              else F.pp_print_string fmt "_")
+            fields;
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt "=>";
+          F.pp_print_space fmt ();
+          F.pp_print_string fmt field_var;
+          (* Close the box for the branch *)
+          F.pp_close_box fmt ();
+
+          (* Close the box for the whole match *)
+          F.pp_close_box fmt ();
+
+          (* Close the box for projector definition *)
+          F.pp_close_box fmt ();
+          (* Add breaks to insert new lines between definitions *)
+          F.pp_print_break fmt 0 0
+        in
+
+        FieldId.iteri extract_field_proj fields
+
 (** Auxiliary function.
 
     Generate field projectors in Coq.
@@ -1669,7 +1790,7 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
     Sometimes we extract records as inductives in Coq: when this happens we
     have to define the field projectors afterwards.
  *)
-let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
+let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx)
     (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
   sanity_check __FILE__ __LINE__ (!backend = Coq) decl.meta;
   match decl.kind with
@@ -1826,7 +1947,13 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
 let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (decl : type_decl) : unit =
   match !backend with
-  | FStar | Lean | HOL4 -> ()
+  | FStar | HOL4 -> ()
+  | Lean ->
+      if
+        not
+          (TypesUtils.type_decl_from_decl_id_is_tuple_struct
+             ctx.trans_ctx.type_ctx.type_infos decl.def_id)
+      then extract_type_decl_lean_record_field_projectors ctx fmt kind decl
   | Coq ->
       if
         not
@@ -1834,7 +1961,7 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
              ctx.trans_ctx.type_ctx.type_infos decl.def_id)
       then (
         extract_type_decl_coq_arguments ctx fmt kind decl;
-        extract_type_decl_record_field_projectors ctx fmt kind decl)
+        extract_type_decl_coq_record_field_projectors ctx fmt kind decl)
 
 (** Extract the state type declaration. *)
 let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
-- 
cgit v1.2.3


From e660a4d575ba55bd23c64b5bd7b4e435be82d7ed Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 10:58:47 +0200
Subject: Improve formatting of Lean struct projectors

---
 compiler/ExtractTypes.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 4272e7a9..8520b0fb 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1696,8 +1696,11 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
 
         let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
           F.pp_print_space fmt ();
-          (* Box for the projector definition *)
+          (* Outer box for the projector definition *)
           F.pp_open_hvbox fmt 0;
+          (* Inner box for the projector definition *)
+          F.pp_open_hvbox fmt ctx.indent_incr;
+
           (* Box for the [def ADT.proj ... :=] *)
           F.pp_open_hovbox fmt ctx.indent_incr;
           F.pp_print_string fmt "def";
@@ -1775,7 +1778,8 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
           (* Close the box for the whole match *)
           F.pp_close_box fmt ();
 
-          (* Close the box for projector definition *)
+          F.pp_close_box fmt ();
+          (* Close the outer box for projector definition *)
           F.pp_close_box fmt ();
           (* Add breaks to insert new lines between definitions *)
           F.pp_print_break fmt 0 0
-- 
cgit v1.2.3


From 7238177f5c7cff15f924e13c01d5b3b4802daf77 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 11:33:46 +0200
Subject: Do not expand field projector for recursive structs to a let binding
 in Lean

---
 compiler/SymbolicToPure.ml | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 6c925bcd..351f5cf2 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2902,14 +2902,9 @@ and translate_ExpandAdt_one_branch (sv : V.symbolic_value)
          - if the ADT is an enumeration (which must have exactly one branch)
          - if we forbid using field projectors.
       *)
-      let is_rec_def =
-        T.TypeDeclId.Set.mem adt_id ctx.type_ctx.recursive_decls
-      in
       let use_let_with_cons =
         is_enum
         || !Config.dont_use_field_projectors
-        (* TODO: for now, we don't have field projectors over recursive ADTs in Lean. *)
-        || (!Config.backend = Lean && is_rec_def)
         (* Also, there is a special case when the ADT is to be extracted as
            a tuple, because it is a structure with unnamed fields. Some backends
            like Lean have projectors for tuples (like so: `x.3`), but others
-- 
cgit v1.2.3


From b4cc9c908935eb95c761b664e75ce065fb97d85c Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 12:04:09 +0200
Subject: Regenerate Lean files for betree following extraction changes

---
 tests/lean/BetreeMain/Funs.lean  | 81 +++++++++++++++++-----------------------
 tests/lean/BetreeMain/Types.lean | 12 ++++++
 2 files changed, 46 insertions(+), 47 deletions(-)

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 7cc52159..f6fda6db 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -250,16 +250,15 @@ mutual divergent def betree.Internal.lookup_in_children
   (self : betree.Internal) (key : U64) (st : State) :
   Result (State × ((Option U64) × betree.Internal))
   :=
-  let ⟨ i, i1, n, n1 ⟩ := self
-  if key < i1
+  if key < self.pivot
   then
     do
-    let (st1, (o, n2)) ← betree.Node.lookup n key st
-    Result.ok (st1, (o, betree.Internal.mk i i1 n2 n1))
+    let (st1, (o, n)) ← betree.Node.lookup self.left key st
+    Result.ok (st1, (o, betree.Internal.mk self.id self.pivot n self.right))
   else
     do
-    let (st1, (o, n2)) ← betree.Node.lookup n1 key st
-    Result.ok (st1, (o, betree.Internal.mk i i1 n n2))
+    let (st1, (o, n)) ← betree.Node.lookup self.right key st
+    Result.ok (st1, (o, betree.Internal.mk self.id self.pivot self.left n))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
    Source: 'src/betree.rs', lines 709:4-709:58 -/
@@ -270,8 +269,7 @@ divergent def betree.Node.lookup
   match self with
   | betree.Node.Internal node =>
     do
-    let ⟨ i, i1, n, n1 ⟩ := node
-    let (st1, msgs) ← betree.load_internal_node i st
+    let (st1, msgs) ← betree.load_internal_node node.id st
     let (pending, lookup_first_message_for_key_back) ←
       betree.Node.lookup_first_message_for_key key msgs
     match pending with
@@ -281,8 +279,7 @@ divergent def betree.Node.lookup
       then
         do
         let (st2, (o, node1)) ←
-          betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
-            st1
+          betree.Internal.lookup_in_children node key st1
         let _ ←
           lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
         Result.ok (st2, (o, betree.Node.Internal node1))
@@ -293,33 +290,26 @@ divergent def betree.Node.lookup
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Insert v) l)
-          Result.ok (st1, (some v, betree.Node.Internal (betree.Internal.mk i
-            i1 n n1)))
+          Result.ok (st1, (some v, betree.Node.Internal node))
         | betree.Message.Delete =>
           do
           let _ ←
             lookup_first_message_for_key_back (betree.List.Cons (k,
               betree.Message.Delete) l)
-          Result.ok (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
-            n n1)))
+          Result.ok (st1, (none, betree.Node.Internal node))
         | betree.Message.Upsert ufs =>
           do
           let (st2, (v, node1)) ←
-            betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1)
-              key st1
+            betree.Internal.lookup_in_children node key st1
           let (v1, pending1) ←
             betree.Node.apply_upserts (betree.List.Cons (k,
               betree.Message.Upsert ufs) l) v key
-          let ⟨ i2, i3, n2, n3 ⟩ := node1
           let msgs1 ← lookup_first_message_for_key_back pending1
-          let (st3, _) ← betree.store_internal_node i2 msgs1 st2
-          Result.ok (st3, (some v1, betree.Node.Internal (betree.Internal.mk i2
-            i3 n2 n3)))
+          let (st3, _) ← betree.store_internal_node node1.id msgs1 st2
+          Result.ok (st3, (some v1, betree.Node.Internal node1))
     | betree.List.Nil =>
       do
-      let (st2, (o, node1)) ←
-        betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
-          st1
+      let (st2, (o, node1)) ← betree.Internal.lookup_in_children node key st1
       let _ ← lookup_first_message_for_key_back betree.List.Nil
       Result.ok (st2, (o, betree.Node.Internal node1))
   | betree.Node.Leaf node =>
@@ -541,34 +531,36 @@ mutual divergent def betree.Internal.flush
     × betree.NodeIdCounter)))
   :=
   do
-  let ⟨ i, i1, n, n1 ⟩ := self
-  let p ← betree.ListPairU64T.partition_at_pivot betree.Message content i1
+  let p ←
+    betree.ListPairU64T.partition_at_pivot betree.Message content self.pivot
   let (msgs_left, msgs_right) := p
   let len_left ← betree.List.len (U64 × betree.Message) msgs_left
   if len_left >= params.min_flush_size
   then
     do
     let (st1, p1) ←
-      betree.Node.apply_messages n params node_id_cnt msgs_left st
-    let (n2, node_id_cnt1) := p1
+      betree.Node.apply_messages self.left params node_id_cnt msgs_left st
+    let (n, node_id_cnt1) := p1
     let len_right ← betree.List.len (U64 × betree.Message) msgs_right
     if len_right >= params.min_flush_size
     then
       do
       let (st2, p2) ←
-        betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1
-      let (n3, node_id_cnt2) := p2
-      Result.ok (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
-        node_id_cnt2)))
+        betree.Node.apply_messages self.right params node_id_cnt1 msgs_right
+          st1
+      let (n1, node_id_cnt2) := p2
+      Result.ok (st2, (betree.List.Nil, (betree.Internal.mk self.id self.pivot
+        n n1, node_id_cnt2)))
     else
-      Result.ok (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
-        node_id_cnt1)))
+      Result.ok (st1, (msgs_right, (betree.Internal.mk self.id self.pivot n
+        self.right, node_id_cnt1)))
   else
     do
     let (st1, p1) ←
-      betree.Node.apply_messages n1 params node_id_cnt msgs_right st
-    let (n2, node_id_cnt1) := p1
-    Result.ok (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
+      betree.Node.apply_messages self.right params node_id_cnt msgs_right st
+    let (n, node_id_cnt1) := p1
+    Result.ok (st1, (msgs_left, (betree.Internal.mk self.id self.pivot
+      self.left n, node_id_cnt1)))
 
 /- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
    Source: 'src/betree.rs', lines 588:4-593:5 -/
@@ -581,26 +573,21 @@ divergent def betree.Node.apply_messages
   match self with
   | betree.Node.Internal node =>
     do
-    let ⟨ i, i1, n, n1 ⟩ := node
-    let (st1, content) ← betree.load_internal_node i st
+    let (st1, content) ← betree.load_internal_node node.id st
     let content1 ← betree.Node.apply_messages_to_internal content msgs
     let num_msgs ← betree.List.len (U64 × betree.Message) content1
     if num_msgs >= params.min_flush_size
     then
       do
       let (st2, (content2, p)) ←
-        betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt
-          content1 st1
+        betree.Internal.flush node params node_id_cnt content1 st1
       let (node1, node_id_cnt1) := p
-      let ⟨ i2, i3, n2, n3 ⟩ := node1
-      let (st3, _) ← betree.store_internal_node i2 content2 st2
-      Result.ok (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
-        node_id_cnt1))
+      let (st3, _) ← betree.store_internal_node node1.id content2 st2
+      Result.ok (st3, (betree.Node.Internal node1, node_id_cnt1))
     else
       do
-      let (st2, _) ← betree.store_internal_node i content1 st1
-      Result.ok (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
-        node_id_cnt))
+      let (st2, _) ← betree.store_internal_node node.id content1 st1
+      Result.ok (st2, (betree.Node.Internal node, node_id_cnt))
   | betree.Node.Leaf node =>
     do
     let (st1, content) ← betree.load_leaf_node node.id st
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 877508f6..3f115fe4 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -46,6 +46,18 @@ inductive betree.Node :=
 
 end
 
+def betree.Internal.id (x : betree.Internal) :=
+  match x with | betree.Internal.mk x1 _ _ _ => x1
+
+def betree.Internal.pivot (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ x1 _ _ => x1
+
+def betree.Internal.left (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ _ x1 _ => x1
+
+def betree.Internal.right (x : betree.Internal) :=
+  match x with | betree.Internal.mk _ _ _ x1 => x1
+
 /- [betree_main::betree::Params]
    Source: 'src/betree.rs', lines 187:0-187:13 -/
 structure betree.Params where
-- 
cgit v1.2.3


From e76ef95ddda11d4220e1f0fd863b0df568de95bc Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 16:41:54 +0200
Subject: Add simp, reducible attributes to generated Lean projectors

---
 compiler/ExtractTypes.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 8520b0fb..70a4d000 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1701,6 +1701,16 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
           (* Inner box for the projector definition *)
           F.pp_open_hvbox fmt ctx.indent_incr;
 
+          (* Box for the attributes *)
+          F.pp_open_vbox fmt 0;
+          (* Annotate the projectors with both simp and reducible.
+             The first one allows to automatically unfold when calling simp in proofs.
+             The second ensures that projectors will interact well with the unifier *)
+          F.pp_print_string fmt "@[simp, reducible]";
+          F.pp_print_break fmt 0 0;
+          (* Close box for the attributes *)
+          F.pp_close_box fmt ();
+
           (* Box for the [def ADT.proj ... :=] *)
           F.pp_open_hovbox fmt ctx.indent_incr;
           F.pp_print_string fmt "def";
-- 
cgit v1.2.3


From 765cb792916c1c69f864a6cf59a49c504ad603a2 Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 16:46:18 +0200
Subject: Regenerate Lean files for betree

---
 tests/lean/BetreeMain/Types.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 3f115fe4..e79da43f 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -46,15 +46,19 @@ inductive betree.Node :=
 
 end
 
+@[simp, reducible]
 def betree.Internal.id (x : betree.Internal) :=
   match x with | betree.Internal.mk x1 _ _ _ => x1
 
+@[simp, reducible]
 def betree.Internal.pivot (x : betree.Internal) :=
   match x with | betree.Internal.mk _ x1 _ _ => x1
 
+@[simp, reducible]
 def betree.Internal.left (x : betree.Internal) :=
   match x with | betree.Internal.mk _ _ x1 _ => x1
 
+@[simp, reducible]
 def betree.Internal.right (x : betree.Internal) :=
   match x with | betree.Internal.mk _ _ _ x1 => x1
 
-- 
cgit v1.2.3


From 3b4139de5b9bcf5f43213330652ad01383e975d3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 May 2024 16:50:18 +0200
Subject: Factor out the code for Lean and Coq

---
 compiler/ExtractTypes.ml | 184 +++++++++++------------------------------------
 1 file changed, 41 insertions(+), 143 deletions(-)

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 2fc0c117..cc0c351d 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1666,15 +1666,15 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
 
 (** Auxiliary function.
 
-    Generate field projectors in Lean.
+    Generate field projectors for Lean and Coq.
 
-    Recursive structs are defined as inductives in Lean.
+    Recursive structs are defined as inductives in Lean and Coq.
     Field projectors allow to retrieve the facilities provided by
     Lean structures.
  *)
-let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
+let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
     (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
-  sanity_check __FILE__ __LINE__ (!backend = Lean) decl.meta;
+  sanity_check __FILE__ __LINE__ (!backend = Coq || !backend = Lean) decl.span;
   match decl.kind with
   | Opaque | Enum _ -> ()
   | Struct fields ->
@@ -1683,18 +1683,18 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
       if is_rec then
         (* Add the type params *)
         let ctx, type_params, cg_params, trait_clauses =
-          ctx_add_generic_params decl.meta decl.llbc_name decl.llbc_generics
+          ctx_add_generic_params decl.span decl.llbc_name decl.llbc_generics
             decl.generics ctx
         in
         (* Record_var will be the ADT argument to the projector *)
-        let ctx, record_var = ctx_add_var decl.meta "x" (VarId.of_int 0) ctx in
+        let ctx, record_var = ctx_add_var decl.span "x" (VarId.of_int 0) ctx in
         (* Field_var will be the variable in the constructor that is returned by the projector *)
-        let ctx, field_var = ctx_add_var decl.meta "x" (VarId.of_int 1) ctx in
+        let ctx, field_var = ctx_add_var decl.span "x" (VarId.of_int 1) ctx in
         (* Name of the ADT *)
-        let def_name = ctx_get_local_type decl.meta decl.def_id ctx in
+        let def_name = ctx_get_local_type decl.span decl.def_id ctx in
         (* Name of the ADT constructor. As we are in the struct case, we only have
            one constructor *)
-        let cons_name = ctx_get_struct decl.meta (TAdtId decl.def_id) ctx in
+        let cons_name = ctx_get_struct decl.span (TAdtId decl.def_id) ctx in
 
         let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
           F.pp_print_space fmt ();
@@ -1703,33 +1703,40 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
           (* Inner box for the projector definition *)
           F.pp_open_hvbox fmt ctx.indent_incr;
 
-          (* Box for the attributes *)
-          F.pp_open_vbox fmt 0;
-          (* Annotate the projectors with both simp and reducible.
-             The first one allows to automatically unfold when calling simp in proofs.
-             The second ensures that projectors will interact well with the unifier *)
-          F.pp_print_string fmt "@[simp, reducible]";
-          F.pp_print_break fmt 0 0;
-          (* Close box for the attributes *)
-          F.pp_close_box fmt ();
+          (* For Lean: add some attributes *)
+          if !backend = Lean then (
+            (* Box for the attributes *)
+            F.pp_open_vbox fmt 0;
+            (* Annotate the projectors with both simp and reducible.
+               The first one allows to automatically unfold when calling simp in proofs.
+               The second ensures that projectors will interact well with the unifier *)
+            F.pp_print_string fmt "@[simp, reducible]";
+            F.pp_print_break fmt 0 0;
+            (* Close box for the attributes *)
+            F.pp_close_box fmt ());
 
           (* Box for the [def ADT.proj ... :=] *)
           F.pp_open_hovbox fmt ctx.indent_incr;
-          F.pp_print_string fmt "def";
+          (match !backend with
+          | Lean -> F.pp_print_string fmt "def"
+          | Coq -> F.pp_print_string fmt "Definition"
+          | _ -> internal_error __FILE__ __LINE__ decl.span);
           F.pp_print_space fmt ();
 
           (* Print the function name. In Lean, the syntax ADT.proj will
-             allow us to call x.proj for any x of type ADT *)
+             allow us to call x.proj for any x of type ADT. In Coq,
+             we will have to introduce a notation for the projector. *)
           let field_name =
-            ctx_get_field decl.meta (TAdtId decl.def_id) field_id ctx
+            ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
           in
-          F.pp_print_string fmt def_name;
-          F.pp_print_string fmt ".";
+          if !backend = Lean then (
+            F.pp_print_string fmt def_name;
+            F.pp_print_string fmt ".");
           F.pp_print_string fmt field_name;
 
           (* Print the generics *)
           let as_implicits = true in
-          extract_generic_params decl.meta ctx fmt TypeDeclId.Set.empty
+          extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty
             ~as_implicits decl.generics type_params cg_params trait_clauses;
 
           (* Print the record parameter as "(x : ADT)" *)
@@ -1787,115 +1794,11 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
           (* Close the box for the branch *)
           F.pp_close_box fmt ();
 
-          (* Close the box for the whole match *)
-          F.pp_close_box fmt ();
-
-          F.pp_close_box fmt ();
-          (* Close the outer box for projector definition *)
-          F.pp_close_box fmt ();
-          (* Add breaks to insert new lines between definitions *)
-          F.pp_print_break fmt 0 0
-        in
-
-        FieldId.iteri extract_field_proj fields
-
-(** Auxiliary function.
-
-    Generate field projectors in Coq.
-
-    Sometimes we extract records as inductives in Coq: when this happens we
-    have to define the field projectors afterwards.
- *)
-let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx)
-    (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
-  sanity_check __FILE__ __LINE__ (!backend = Coq) decl.span;
-  match decl.kind with
-  | Opaque | Enum _ -> ()
-  | Struct fields ->
-      (* Records are extracted as inductives only if they are recursive *)
-      let is_rec = decl_is_from_rec_group kind in
-      if is_rec then
-        (* Add the type params *)
-        let ctx, type_params, cg_params, trait_clauses =
-          ctx_add_generic_params decl.span decl.llbc_name decl.llbc_generics
-            decl.generics ctx
-        in
-        let ctx, record_var = ctx_add_var decl.span "x" (VarId.of_int 0) ctx in
-        let ctx, field_var = ctx_add_var decl.span "x" (VarId.of_int 1) ctx in
-        let def_name = ctx_get_local_type decl.span decl.def_id ctx in
-        let cons_name = ctx_get_struct decl.span (TAdtId decl.def_id) ctx in
-        let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
-          F.pp_print_space fmt ();
-          (* Outer box for the projector definition *)
-          F.pp_open_hvbox fmt 0;
-          (* Inner box for the projector definition *)
-          F.pp_open_hvbox fmt ctx.indent_incr;
-          (* Open a box for the [Definition PROJ ... :=] *)
-          F.pp_open_hovbox fmt ctx.indent_incr;
-          F.pp_print_string fmt "Definition";
-          F.pp_print_space fmt ();
-          let field_name =
-            ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
-          in
-          F.pp_print_string fmt field_name;
-          (* Print the generics *)
-          let as_implicits = true in
-          extract_generic_params decl.span ctx fmt TypeDeclId.Set.empty
-            ~as_implicits decl.generics type_params cg_params trait_clauses;
-          (* Print the record parameter *)
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "(";
-          F.pp_print_string fmt record_var;
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt ":";
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt def_name;
-          List.iter
-            (fun p ->
-              F.pp_print_space fmt ();
-              F.pp_print_string fmt p)
-            type_params;
-          F.pp_print_string fmt ")";
-          (* *)
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt ":=";
-          (* Close the box for the [Definition PROJ ... :=] *)
-          F.pp_close_box fmt ();
-          F.pp_print_space fmt ();
-          (* Open a box for the whole match *)
-          F.pp_open_hvbox fmt 0;
-          (* Open a box for the [match ... with] *)
-          F.pp_open_hovbox fmt ctx.indent_incr;
-          F.pp_print_string fmt "match";
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt record_var;
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "with";
-          (* Close the box for the [match ... with] *)
-          F.pp_close_box fmt ();
-
-          (* Open a box for the branch *)
-          F.pp_open_hovbox fmt ctx.indent_incr;
-          (* Print the match branch *)
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "|";
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt cons_name;
-          FieldId.iteri
-            (fun id _ ->
-              F.pp_print_space fmt ();
-              if field_id = id then F.pp_print_string fmt field_var
-              else F.pp_print_string fmt "_")
-            fields;
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "=>";
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt field_var;
-          (* Close the box for the branch *)
-          F.pp_close_box fmt ();
           (* Print the [end] *)
-          F.pp_print_space fmt ();
-          F.pp_print_string fmt "end";
+          if !backend = Coq then (
+            F.pp_print_space fmt ();
+            F.pp_print_string fmt "end");
+
           (* Close the box for the whole match *)
           F.pp_close_box fmt ();
           (* Close the inner box projector *)
@@ -1904,12 +1807,13 @@ let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx)
           if !backend = Coq then (
             F.pp_print_cut fmt ();
             F.pp_print_string fmt ".");
-          (* Close the outer box projector  *)
+          (* Close the outer box for projector definition *)
           F.pp_close_box fmt ();
           (* Add breaks to insert new lines between definitions *)
           F.pp_print_break fmt 0 0
         in
 
+        (* Only for Coq: we need to define a notation for the projector *)
         let extract_proj_notation (field_id : FieldId.id) (_ : field) : unit =
           F.pp_print_space fmt ();
           (* Outer box for the projector definition *)
@@ -1950,7 +1854,7 @@ let extract_type_decl_coq_record_field_projectors (ctx : extraction_ctx)
         let extract_field_proj_and_notation (field_id : FieldId.id)
             (field : field) : unit =
           extract_field_proj field_id field;
-          extract_proj_notation field_id field
+          if !backend = Coq then extract_proj_notation field_id field
         in
 
         FieldId.iteri extract_field_proj_and_notation fields
@@ -1964,20 +1868,14 @@ let extract_type_decl_extra_info (ctx : extraction_ctx) (fmt : F.formatter)
     (kind : decl_kind) (decl : type_decl) : unit =
   match !backend with
   | FStar | HOL4 -> ()
-  | Lean ->
-      if
-        not
-          (TypesUtils.type_decl_from_decl_id_is_tuple_struct
-             ctx.trans_ctx.type_ctx.type_infos decl.def_id)
-      then extract_type_decl_lean_record_field_projectors ctx fmt kind decl
-  | Coq ->
+  | Lean | Coq ->
       if
         not
           (TypesUtils.type_decl_from_decl_id_is_tuple_struct
              ctx.trans_ctx.type_ctx.type_infos decl.def_id)
       then (
-        extract_type_decl_coq_arguments ctx fmt kind decl;
-        extract_type_decl_coq_record_field_projectors ctx fmt kind decl)
+        if !backend = Coq then extract_type_decl_coq_arguments ctx fmt kind decl;
+        extract_type_decl_record_field_projectors ctx fmt kind decl)
 
 (** Extract the state type declaration. *)
 let extract_state_type (fmt : F.formatter) (ctx : extraction_ctx)
-- 
cgit v1.2.3


From 169af47945f013e61b14d67e7ebdc9c03636c5a2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 24 May 2024 16:50:25 +0200
Subject: Update an .opam file

---
 tests/test_runner/aeneas_test_runner.opam | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/test_runner/aeneas_test_runner.opam b/tests/test_runner/aeneas_test_runner.opam
index b57cc9f6..1539c521 100644
--- a/tests/test_runner/aeneas_test_runner.opam
+++ b/tests/test_runner/aeneas_test_runner.opam
@@ -7,7 +7,7 @@ homepage: "https://github.com/AeneasVerif/aeneas"
 bug-reports: "https://github.com/AeneasVerif/aeneas/issues"
 depends: [
   "ocaml"
-  "dune" {>= "3.12"}
+  "dune" {>= "3.7"}
   "odoc" {with-doc}
 ]
 build: [
-- 
cgit v1.2.3