Merge branch 'main' into son/loops2

8 files changed, 206 insertions, 211 deletions

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index ab7eb50c..815e228f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -351,13 +351,13 @@ let unsafe_names_map_add (id : id) (name : string) (nm : unsafe_names_map) :
 
     [append]: function to append an index to a string
  *)
-let basename_to_unique (names_set : StringSet.t)
+let basename_to_unique_aux (collision : string -> bool)
     (append : string -> int -> string) (basename : string) : string =
   let rec gen (i : int) : string =
     let s = append basename i in
-    if StringSet.mem s names_set then gen (i + 1) else s
+    if collision s then gen (i + 1) else s
   in
-  if StringSet.mem basename names_set then gen 1 else basename
+  if collision basename then gen 1 else basename
 
 type names_maps = {
   names_map : names_map;
@@ -1841,13 +1841,22 @@ let trait_self_clause_basename = "self_clause"
 let name_append_index (basename : string) (i : int) : string =
   basename ^ string_of_int i
 
+let basename_to_unique (ctx : extraction_ctx) (name : string) =
+  let collision s =
+    (* Note that we ignore the "unsafe" names which contain in particular
+       field names: we want to allow using field names for variables if
+       the backend allows such collisions *)
+    StringSet.mem s ctx.names_maps.names_map.names_set
+    || StringSet.mem s ctx.names_maps.strict_names_map.names_set
+  in
+
+  basename_to_unique_aux collision name_append_index name
+
 (** Generate a unique type variable name and add it to the context *)
 let ctx_add_type_var (span : Meta.span) (basename : string) (id : TypeVarId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
   let name = ctx_compute_type_var_basename ctx basename in
-  let name =
-    basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
-  in
+  let name = basename_to_unique ctx name in
   let ctx = ctx_add span (TypeVarId id) name ctx in
   (ctx, name)
 
@@ -1856,9 +1865,7 @@ let ctx_add_const_generic_var (span : Meta.span) (basename : string)
     (id : ConstGenericVarId.id) (ctx : extraction_ctx) : extraction_ctx * string
     =
   let name = ctx_compute_const_generic_var_basename ctx basename in
-  let name =
-    basename_to_unique ctx.names_maps.names_map.names_set name_append_index name
-  in
+  let name = basename_to_unique ctx name in
   let ctx = ctx_add span (ConstGenericVarId id) name ctx in
   (ctx, name)
 
@@ -1872,10 +1879,7 @@ let ctx_add_type_vars (span : Meta.span) (vars : (string * TypeVarId.id) list)
 (** Generate a unique variable name and add it to the context *)
 let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id)
     (ctx : extraction_ctx) : extraction_ctx * string =
-  let name =
-    basename_to_unique ctx.names_maps.names_map.names_set name_append_index
-      basename
-  in
+  let name = basename_to_unique ctx basename in
   let ctx = ctx_add span (VarId id) name ctx in
   (ctx, name)
 
@@ -1883,20 +1887,14 @@ let ctx_add_var (span : Meta.span) (basename : string) (id : VarId.id)
 let ctx_add_trait_self_clause (span : Meta.span) (ctx : extraction_ctx) :
     extraction_ctx * string =
   let basename = trait_self_clause_basename in
-  let name =
-    basename_to_unique ctx.names_maps.names_map.names_set name_append_index
-      basename
-  in
+  let name = basename_to_unique ctx basename in
   let ctx = ctx_add span TraitSelfClauseId name ctx in
   (ctx, name)
 
 (** Generate a unique trait clause name and add it to the context *)
 let ctx_add_local_trait_clause (span : Meta.span) (basename : string)
     (id : TraitClauseId.id) (ctx : extraction_ctx) : extraction_ctx * string =
-  let name =
-    basename_to_unique ctx.names_maps.names_map.names_set name_append_index
-      basename
-  in
+  let name = basename_to_unique ctx basename in
   let ctx = ctx_add span (LocalTraitClauseId id) name ctx in
   (ctx, name)
 
diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml
index a7ab6da0..ff936d2f 100644
--- a/compiler/ExtractBuiltin.ml
+++ b/compiler/ExtractBuiltin.ml
@@ -233,7 +233,12 @@ let mk_builtin_types_map () =
 
 let builtin_types_map = mk_memoized mk_builtin_types_map
 
-type builtin_fun_info = { extract_name : string } [@@deriving show]
+type builtin_fun_info = {
+  extract_name : string;
+  can_fail : bool;
+  stateful : bool;
+}
+[@@deriving show]
 
 let int_and_smaller_list : (string * string) list =
   let uint_names = List.rev [ "u8"; "u16"; "u32"; "u64"; "u128" ] in
@@ -257,16 +262,17 @@ let int_and_smaller_list : (string * string) list =
   ]
   @ compute_pairs uint_names @ compute_pairs int_names
 
-(** The assumed functions.
+(** The builtin functions.
 
     The optional list of booleans is filtering information for the type
     parameters. For instance, in the case of the `Vec` functions, there is
     a type parameter for the allocator to use, which we want to filter.
  *)
-let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
+let mk_builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
   (* Small utility *)
-  let mk_fun (rust_name : string) (extract_name : string option)
-      (filter : bool list option) :
+  let mk_fun (rust_name : string) ?(filter : bool list option = None)
+      ?(can_fail = true) ?(stateful = false)
+      ?(extract_name : string option = None) () :
       pattern * bool list option * builtin_fun_info =
     let rust_name =
       try parse_pattern rust_name
@@ -279,124 +285,151 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
       | Some name -> split_on_separator name
     in
     let basename = flatten_name extract_name in
-    let f = { extract_name = basename } in
+    let f = { extract_name = basename; can_fail; stateful } in
     (rust_name, filter, f)
   in
   let mk_scalar_fun (rust_name : string -> string)
-      (extract_name : string -> string) :
+      (extract_name : string -> string) ?(can_fail = true) () :
       (pattern * bool list option * builtin_fun_info) list =
     List.map
-      (fun ty -> mk_fun (rust_name ty) (Some (extract_name ty)) None)
+      (fun ty ->
+        mk_fun (rust_name ty)
+          ~extract_name:(Some (extract_name ty))
+          ~can_fail ())
       all_int_names
   in
   [
-    mk_fun "core::mem::replace" None None;
+    mk_fun "core::mem::replace" ~can_fail:false ();
+    mk_fun "core::mem::take" ~can_fail:false ();
     mk_fun "core::slice::{[@T]}::len"
-      (Some (backend_choice "slice::len" "Slice::len"))
-      None;
+      ~extract_name:(Some (backend_choice "slice::len" "Slice::len"))
+      ~can_fail:false ();
     mk_fun "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new"
-      (Some "alloc::vec::Vec::new") None;
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push" None
-      (Some [ true; false ]);
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert" None
-      (Some [ true; false ]);
-    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len" None
-      (Some [ true; false ]);
+      ~extract_name:(Some "alloc::vec::Vec::new") ~can_fail:false ();
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::push"
+      ~filter:(Some [ true; false ])
+      ();
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::insert"
+      ~filter:(Some [ true; false ])
+      ();
+    mk_fun "alloc::vec::{alloc::vec::Vec<@T, @A>}::len"
+      ~filter:(Some [ true; false ])
+      ~can_fail:false ();
     mk_fun
       "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
        @I>}::index"
-      (Some "alloc.vec.Vec.index")
-      (Some [ true; true; false ]);
+      ~extract_name:(Some "alloc.vec.Vec.index")
+      ~filter:(Some [ true; true; false ])
+      ();
     mk_fun
       "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
        @I>}::index_mut"
-      (Some "alloc.vec.Vec.index_mut")
-      (Some [ true; true; false ]);
+      ~extract_name:(Some "alloc.vec.Vec.index_mut")
+      ~filter:(Some [ true; true; false ])
+      ();
     mk_fun "alloc::boxed::{core::ops::deref::Deref<Box<@T>>}::deref"
-      (Some "alloc.boxed.Box.deref")
-      (Some [ true; false ]);
+      ~extract_name:(Some "alloc.boxed.Box.deref")
+      ~filter:(Some [ true; false ])
+      ();
     mk_fun "alloc::boxed::{core::ops::deref::DerefMut<Box<@T>>}::deref_mut"
-      (Some "alloc.boxed.Box.deref_mut")
-      (Some [ true; false ]);
+      ~extract_name:(Some "alloc.boxed.Box.deref_mut")
+      ~filter:(Some [ true; false ])
+      ();
     mk_fun "core::slice::index::{core::ops::index::Index<[@T], @I>}::index"
-      (Some "core.slice.index.Slice.index") None;
+      ~extract_name:(Some "core.slice.index.Slice.index") ();
     mk_fun
       "core::slice::index::{core::ops::index::IndexMut<[@T], @I>}::index_mut"
-      (Some "core.slice.index.Slice.index_mut") None;
+      ~extract_name:(Some "core.slice.index.Slice.index_mut") ();
     mk_fun "core::array::{core::ops::index::Index<[@T; @N], @I>}::index"
-      (Some "core.array.Array.index") None;
+      ~extract_name:(Some "core.array.Array.index") ();
     mk_fun "core::array::{core::ops::index::IndexMut<[@T; @N], @I>}::index_mut"
-      (Some "core.array.Array.index_mut") None;
+      ~extract_name:(Some "core.array.Array.index_mut") ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T]>}::get"
-      (Some "core::slice::index::RangeUsize::get") None;
+      ~extract_name:(Some "core::slice::index::RangeUsize::get") ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T]>}::get_mut"
-      (Some "core::slice::index::RangeUsize::get_mut") None;
+      ~extract_name:(Some "core::slice::index::RangeUsize::get_mut") ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T]>}::index"
-      (Some "core::slice::index::RangeUsize::index") None;
+      ~extract_name:(Some "core::slice::index::RangeUsize::index") ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T]>}::index_mut"
-      (Some "core::slice::index::RangeUsize::index_mut") None;
+      ~extract_name:(Some "core::slice::index::RangeUsize::index_mut") ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T]>}::get_unchecked"
-      (Some "core::slice::index::RangeUsize::get_unchecked") None;
+      ~extract_name:(Some "core::slice::index::RangeUsize::get_unchecked") ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::Range<usize>, \
        [@T]>}::get_unchecked_mut"
-      (Some "core::slice::index::RangeUsize::get_unchecked_mut") None;
+      ~extract_name:(Some "core::slice::index::RangeUsize::get_unchecked_mut")
+      ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, [@T]>}::get"
-      None None;
+      ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, \
        [@T]>}::get_mut"
-      None None;
+      ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, \
        [@T]>}::get_unchecked"
-      None None;
+      ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, \
        [@T]>}::get_unchecked_mut"
-      None None;
+      ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, [@T]>}::index"
-      (Some "core_slice_index_Slice_index") None;
+      ~extract_name:(Some "core_slice_index_Slice_index") ();
     mk_fun
       "core::slice::index::{core::slice::index::SliceIndex<usize, \
        [@T]>}::index_mut"
-      (Some "core_slice_index_Slice_index_mut") None;
-    mk_fun "alloc::slice::{[@T]}::to_vec" (Some "alloc.slice.Slice.to_vec") None;
+      ~extract_name:(Some "core_slice_index_Slice_index_mut") ();
+    mk_fun "alloc::slice::{[@T]}::to_vec"
+      ~extract_name:(Some "alloc.slice.Slice.to_vec") ();
     mk_fun
       "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity"
-      (Some "alloc.vec.Vec.with_capacity") None;
-    mk_fun "core::slice::{[@T]}::reverse" (Some "core.slice.Slice.reverse") None;
+      ~extract_name:(Some "alloc.vec.Vec.with_capacity") ~can_fail:false ();
+    mk_fun "core::slice::{[@T]}::reverse"
+      ~extract_name:(Some "core.slice.Slice.reverse") ~can_fail:false ();
     mk_fun
       "alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref"
-      (Some "alloc.vec.DerefVec.deref")
-      (Some [ true; false ]);
+      ~extract_name:(Some "alloc.vec.DerefVec.deref")
+      ~filter:(Some [ true; false ])
+      ~can_fail:false ();
     mk_fun
       "alloc::vec::{core::ops::deref::DerefMut<alloc::vec::Vec<@T, \
        @A>>}::deref_mut"
-      (Some "alloc.vec.DerefMutVec.deref_mut")
-      (Some [ true; false ]);
+      ~extract_name:(Some "alloc.vec.DerefMutVec.deref_mut")
+      ~filter:(Some [ true; false ])
+      ();
     mk_fun "core::option::{core::option::Option<@T>}::unwrap"
-      (Some "core.option.Option.unwrap") None;
+      ~extract_name:(Some "core.option.Option.unwrap") ();
   ]
   @ List.flatten
       (List.map
+         (fun int_name ->
+           List.map
+             (fun op ->
+               mk_fun
+                 ("core::num::" ^ "{" ^ int_name ^ "}::" ^ op)
+                 ~can_fail:false ())
+             [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ])
+         all_int_names)
+  @ List.flatten
+      (List.map
          (fun op ->
            mk_scalar_fun
              (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op)
              (fun ty ->
-               StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op))
+               StringUtils.capitalize_first_letter ty ^ ".checked_" ^ op)
+             ~can_fail:false ())
          [ "add"; "sub"; "mul"; "div"; "rem" ])
   (* From<INT, bool> *)
   @ mk_scalar_fun
@@ -406,44 +439,50 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
         "core.convert.num.From"
         ^ StringUtils.capitalize_first_letter ty
         ^ "Bool.from")
+      ~can_fail:false ()
   (* From<INT, INT> *)
   @ List.map
       (fun (big, small) ->
         mk_fun
           ("core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
          ^ ">}::from")
-          (Some
-             ("core.convert.num.From"
-             ^ StringUtils.capitalize_first_letter big
-             ^ StringUtils.capitalize_first_letter small
-             ^ ".from"))
-          None)
+          ~extract_name:
+            (Some
+               ("core.convert.num.From"
+               ^ StringUtils.capitalize_first_letter big
+               ^ StringUtils.capitalize_first_letter small
+               ^ ".from"))
+          ~can_fail:false ())
       int_and_smaller_list
   (* Leading zeros *)
   @ mk_scalar_fun
       (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
       (fun ty ->
         "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".leading_zeros")
+      ~can_fail:false ()
   (* to_le_bytes *)
   @ mk_scalar_fun
       (fun ty -> "core::num::{" ^ ty ^ "}::to_le_bytes")
       (fun ty ->
         "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_le_bytes")
+      ~can_fail:false ()
   (* to_be_bytes *)
   @ mk_scalar_fun
       (fun ty -> "core::num::{" ^ ty ^ "}::to_be_bytes")
       (fun ty ->
         "core.num." ^ StringUtils.capitalize_first_letter ty ^ ".to_be_bytes")
+      ~can_fail:false ()
   (* Clone<bool> *)
   @ [
       mk_fun "core::clone::impls::{core::clone::Clone<bool>}::clone"
-        (Some "core.clone.CloneBool.clone") None;
+        ~extract_name:(Some "core.clone.CloneBool.clone") ~can_fail:false ();
     ]
   (* Clone<INT> *)
   @ mk_scalar_fun
       (fun ty -> "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone")
       (fun ty ->
         "core.clone.Clone" ^ StringUtils.capitalize_first_letter ty ^ ".clone")
+      ~can_fail:false ()
   (* Lean-only definitions *)
   @ mk_lean_only
       [
@@ -451,15 +490,19 @@ let builtin_funs () : (pattern * bool list option * builtin_fun_info) list =
             By construction, we cannot write down that parameter in the output
             in this list
         *)
-        mk_fun "core::mem::swap" None None;
+        mk_fun "core::mem::swap" ~can_fail:false ();
         mk_fun "core::option::{core::option::Option<@T>}::take"
-          (Some (backend_choice "" "Option::take"))
-          None;
+          ~extract_name:(Some (backend_choice "" "Option::take"))
+          ~can_fail:false ();
         mk_fun "core::option::{core::option::Option<@T>}::is_none"
-          (Some (backend_choice "" "Option::isNone"))
-          (Some [ false ]);
+          ~extract_name:(Some (backend_choice "" "Option::isNone"))
+          ~filter:(Some [ false ]) ~can_fail:false ();
       ]
 
+let builtin_funs : unit -> (pattern * bool list option * builtin_fun_info) list
+    =
+  mk_memoized mk_builtin_funs
+
 let mk_builtin_funs_map () =
   let m =
     NameMatcherMap.of_list
@@ -475,106 +518,20 @@ let builtin_funs_map = mk_memoized mk_builtin_funs_map
 
 type effect_info = { can_fail : bool; stateful : bool }
 
-let builtin_fun_effects =
-  let int_ops =
-    [ "wrapping_add"; "wrapping_sub"; "rotate_left"; "rotate_right" ]
-  in
-  let int_funs =
-    List.map
-      (fun int_name ->
-        List.map (fun op -> "core::num::" ^ "{" ^ int_name ^ "}::" ^ op) int_ops)
-      all_int_names
-    @ List.map
-        (fun op ->
-          List.map
-            (fun ty -> "core::num::{" ^ ty ^ "}::checked_" ^ op)
-            all_int_names)
-        [ "add"; "sub"; "mul"; "div"; "rem" ]
-    (* From<INT, bool> *)
-    @ [
-        List.map
-          (fun int_name ->
-            "core::convert::num::{core::convert::From<" ^ int_name
-            ^ ", bool>}::from")
-          all_int_names;
-      ]
-    (* From<INT, INT> *)
-    @ [
-        List.map
-          (fun (big, small) ->
-            "core::convert::num::{core::convert::From<" ^ big ^ ", " ^ small
-            ^ ">}::from")
-          int_and_smaller_list;
-      ]
-    (* Leading zeros *)
-    @ [
-        List.map
-          (fun ty -> "core::num::{" ^ ty ^ "}::leading_zeros")
-          all_int_names;
-      ]
-    (* to_{le,be}_bytes *)
-    @ List.map
-        (fun ty ->
-          let pre = "core::num::{" ^ ty ^ "}::" in
-          [ pre ^ "to_le_bytes"; pre ^ "to_be_bytes" ])
-        all_int_names
-    (* clone *)
-    @ [
-        List.map
-          (fun ty ->
-            "core::clone::impls::{core::clone::Clone<" ^ ty ^ ">}::clone")
-          all_int_names;
-      ]
+let mk_builtin_fun_effects () : (pattern * effect_info) list =
+  let builtin_funs : (pattern * bool list option * builtin_fun_info) list =
+    builtin_funs ()
   in
+  List.map
+    (fun ((pattern, _, info) : _ * _ * builtin_fun_info) ->
+      let info = { can_fail = info.can_fail; stateful = info.stateful } in
+      (pattern, info))
+    builtin_funs
 
-  let int_funs = List.concat int_funs in
-  let no_fail_no_state_funs =
-    [
-      (* TODO: redundancy with the funs information above *)
-      "core::slice::{[@T]}::len";
-      "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::new";
-      "alloc::vec::{alloc::vec::Vec<@T, @A>}::len";
-      "core::mem::replace";
-      "core::mem::take";
-      "core::clone::impls::{core::clone::Clone<bool>}::clone";
-      "alloc::vec::{alloc::vec::Vec<@T, alloc::alloc::Global>}::with_capacity";
-      "core::slice::{[@T]}::reverse";
-      "alloc::vec::{core::ops::deref::Deref<alloc::vec::Vec<@T, @A>>}::deref";
-    ]
-    @ int_funs
-    @ mk_lean_only
-        [
-          "core::mem::swap";
-          "core::option::{core::option::Option<@T>}::take";
-          "core::option::{core::option::Option<@T>}::is_none";
-        ]
-  in
-  let no_fail_no_state_funs =
-    List.map
-      (fun n -> (n, { can_fail = false; stateful = false }))
-      no_fail_no_state_funs
-  in
-  (* TODO: all the functions registered in the [builtin_funs] above should
-     be considered as not using a state. There is a lot of redundancy
-     right now. *)
-  let no_state_funs =
-    [
-      "alloc::vec::{alloc::vec::Vec<@T, @A>}::push";
-      "alloc::vec::{core::ops::index::Index<alloc::vec::Vec<@T, @A>, \
-       @I>}::index";
-      "alloc::vec::{core::ops::index::IndexMut<alloc::vec::Vec<@T, @A>, \
-       @I>}::index_mut";
-      "core::option::{core::option::Option<@T>}::unwrap";
-    ]
-  in
-  let no_state_funs =
-    List.map (fun n -> (n, { can_fail = true; stateful = false })) no_state_funs
-  in
-  no_fail_no_state_funs @ no_state_funs
+let mk_builtin_fun_effects_map () =
+  NameMatcherMap.of_list (mk_builtin_fun_effects ())
 
-let builtin_fun_effects_map =
-  NameMatcherMap.of_list
-    (List.map (fun (n, x) -> (parse_pattern n, x)) builtin_fun_effects)
+let builtin_fun_effects_map = mk_memoized mk_builtin_fun_effects_map
 
 type builtin_trait_decl_info = {
   rust_name : pattern;
@@ -632,13 +589,16 @@ let builtin_trait_decls_info () =
               if !record_fields_short_names then item_name
               else extract_name ^ "_" ^ item_name
             in
-            let fwd = { extract_name = basename } in
+            let fwd =
+              { extract_name = basename; can_fail = true; stateful = false }
+            in
             (item_name, fwd)
           in
           List.map mk_method methods
       | Some methods ->
           List.map
-            (fun (item_name, extract_name) -> (item_name, { extract_name }))
+            (fun (item_name, extract_name) ->
+              (item_name, { extract_name; can_fail = true; stateful = false }))
             methods
     in
     {
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index a2d4758b..cc0c351d 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1666,14 +1666,15 @@ let extract_type_decl_coq_arguments (ctx : extraction_ctx) (fmt : F.formatter)
 
 (** Auxiliary function.
 
-    Generate field projectors in Coq.
+    Generate field projectors for Lean and Coq.
 
-    Sometimes we extract records as inductives in Coq: when this happens we
-    have to define the field projectors afterwards.
+    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_record_field_projectors (ctx : extraction_ctx)
     (fmt : F.formatter) (kind : decl_kind) (decl : type_decl) : unit =
-  sanity_check __FILE__ __LINE__ (!backend = Coq) decl.span;
+  sanity_check __FILE__ __LINE__ (!backend = Coq || !backend = Lean) decl.span;
   match decl.kind with
   | Opaque | Enum _ -> ()
   | Struct fields ->
@@ -1685,29 +1686,60 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           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.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.span "x" (VarId.of_int 1) ctx in
+        (* Name of the ADT *)
         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.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 ... :=] *)
+
+          (* 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 "Definition";
+          (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. In Coq,
+             we will have to introduce a notation for the projector. *)
           let field_name =
             ctx_get_field decl.span (TAdtId decl.def_id) field_id ctx
           in
+          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.span ctx fmt TypeDeclId.Set.empty
             ~as_implicits decl.generics type_params cg_params trait_clauses;
-          (* Print the record parameter *)
+
+          (* Print the record parameter as "(x : ADT)" *)
           F.pp_print_space fmt ();
           F.pp_print_string fmt "(";
           F.pp_print_string fmt record_var;
@@ -1721,14 +1753,17 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
               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 ... :=] *)
+
+          (* 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";
@@ -1758,9 +1793,12 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
           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 *)
@@ -1769,12 +1807,13 @@ let extract_type_decl_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 *)
@@ -1815,7 +1854,7 @@ let extract_type_decl_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
@@ -1828,14 +1867,14 @@ 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 -> ()
-  | Coq ->
+  | FStar | HOL4 -> ()
+  | 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;
+        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. *)
diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml
index a11eab87..815c470f 100644
--- a/compiler/FunsAnalysis.ml
+++ b/compiler/FunsAnalysis.ml
@@ -74,7 +74,8 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
        way. *)
     let get_builtin_info (f : fun_decl) : ExtractBuiltin.effect_info option =
       let open ExtractBuiltin in
-      NameMatcherMap.find_opt name_matcher_ctx f.name builtin_fun_effects_map
+      NameMatcherMap.find_opt name_matcher_ctx f.name
+        (builtin_fun_effects_map ())
     in
 
     (* JP: Why not use a reduce visitor here with a tuple of the values to be
@@ -102,7 +103,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t)
 
           method! visit_rvalue _env rv =
             match rv with
-            | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ -> ()
+            | Use _ | RvRef _ | Global _ | Discriminant _ | Aggregate _ | Len _
+              ->
+                ()
             | UnaryOp (uop, _) -> can_fail := unop_can_fail uop || !can_fail
             | BinaryOp (bop, _, _) ->
                 can_fail := binop_can_fail bop || !can_fail
diff --git a/compiler/InterpreterExpressions.ml b/compiler/InterpreterExpressions.ml
index 2223897c..56c0ab5f 100644
--- a/compiler/InterpreterExpressions.ml
+++ b/compiler/InterpreterExpressions.ml
@@ -816,6 +816,7 @@ let eval_rvalue_not_global (config : config) (span : Meta.span)
         "Unreachable: discriminant reads should have been eliminated from the \
          AST"
   | Global _ -> craise __FILE__ __LINE__ span "Unreachable"
+  | Len _ -> craise __FILE__ __LINE__ span "Unhandled Len"
 
 let eval_fake_read (config : config) (span : Meta.span) (p : place) : cm_fun =
  fun ctx ->
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 19510c2e..5ddc1ed8 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -951,6 +951,8 @@ and eval_statement_raw (config : config) (st : statement) : stl_cm_fun =
                 let cc =
                   match rvalue with
                   | Global _ -> craise __FILE__ __LINE__ st.span "Unreachable"
+                  | Len _ ->
+                      craise __FILE__ __LINE__ st.span "Len is not handled yet"
                   | Use _
                   | RvRef (_, (BShared | BMut | BTwoPhaseMut | BShallow))
                   | UnaryOp _ | BinaryOp _ | Discriminant _ | Aggregate _ ->
diff --git a/compiler/InterpreterUtils.ml b/compiler/InterpreterUtils.ml
index 653a0e24..f3f12906 100644
--- a/compiler/InterpreterUtils.ml
+++ b/compiler/InterpreterUtils.ml
@@ -291,7 +291,7 @@ let rvalue_get_place (rv : rvalue) : place option =
   match rv with
   | Use (Copy p | Move p) -> Some p
   | Use (Constant _) -> None
-  | RvRef (p, _) -> Some p
+  | Len (p, _, _) | RvRef (p, _) -> Some p
   | UnaryOp _ | BinaryOp _ | Global _ | Discriminant _ | Aggregate _ -> None
 
 (** See {!ValuesUtils.symbolic_value_has_borrows} *)
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 71f8e4fc..848bfe50 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -2903,14 +2903,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
@@ -3534,10 +3529,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       if effect_info.stateful then mk_simpl_tuple_ty [ mk_state_ty; output ]
       else output
     in
-    let output =
-      if effect_info.can_fail && inputs <> [] then mk_result_ty output
-      else output
-    in
+    let output = if effect_info.can_fail then mk_result_ty output else output in
     (back_info, output)
   in