Fix a naming issue at extraction and add Box::as_mut

backends/lean/Aeneas/Std/Alloc.lean

@@ -1,6 +1,5 @@
 import Lean
 import Aeneas.Std.Core
-import Aeneas.Std.Core
 
 namespace Aeneas
 

backends/lean/Aeneas/Std/Core.lean

@@ -7,6 +7,10 @@ namespace Std
 
 open Result
 
+/- [alloc::boxed::{core::convert::AsMut<T> for alloc::boxed::Box<T>}::as_mut] -/
+def alloc.boxed.AsMutBoxT.as_mut {T : Type} (x : T) : T × (T → T) :=
+  (x, fun x => x)
+
 namespace core
 
 /- Trait declaration: [core::convert::From] -/
@@ -143,6 +147,15 @@ def core.convert.TryIntoFrom {T U : Type} (fromInst : core.convert.TryFrom U T)
   try_into := core.convert.TryIntoFrom.try_into fromInst
 }
 
+structure core.convert.AsMut (Self : Type) (T : Type) where
+  as_mut : Self → Result (T × (T → Self))
+
+/- [alloc::boxed::{core::convert::AsMut<T> for alloc::boxed::Box<T>}] -/
+@[reducible]
+def core.convert.AsMutBoxT (T : Type) : core.convert.AsMut T T := {
+  as_mut := fun x => ok (alloc.boxed.AsMutBoxT.as_mut x)
+}
+
 /- TODO: -/
 axiom Formatter : Type
 
@@ -159,7 +172,6 @@ def core.result.Result.unwrap {T E : Type}
 structure core.ops.range.RangeFrom (Idx : Type) where
   start : Idx
 
-
 end Std
 
 end Aeneas

src/Logging.ml

@@ -46,7 +46,7 @@ let simplify_aggregates_unchanged_fields_log =
   create_logger "PureMicroPasses.simplify_aggregates_unchanged_fields"
 
 (** Logger for ExtractBase *)
-let extract_log = create_logger "ExtractBase"
+let extract_log = create_logger "Extract"
 
 (** Logger for ExtractBuiltin *)
 let builtin_log = create_logger "Builtin"

src/extract/Extract.ml

@@ -2321,6 +2321,7 @@ let extract_trait_decl_type_names (ctx : extraction_ctx)
 let extract_trait_decl_method_names (ctx : extraction_ctx)
     (trait_decl : trait_decl)
     (builtin_info : Pure.builtin_trait_decl_info option) : extraction_ctx =
+  log#ltrace (lazy (__FUNCTION__ ^ ": " ^ trait_decl.name));
   let methods = trait_decl.methods in
   (* Compute the names *)
   let method_names =
@@ -2329,6 +2330,10 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
         (* Not a builtin function *)
         let compute_item_name (item_name : string) (id : fun_decl_id) :
             string * string =
+          log#ldebug
+            (lazy
+              (__FUNCTION__ ^ "(" ^ trait_decl.name ^ "): compute_item_name: "
+             ^ item_name));
           let trans : pure_fun_translation =
             match FunDeclId.Map.find_opt id ctx.trans_funs with
             | Some decl -> decl
@@ -2348,6 +2353,10 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
           let f =
             { f with item_meta = { f.item_meta with name = llbc_name } }
           in
+          log#ldebug
+            (lazy
+              (__FUNCTION__ ^ ": compute_item_name: llbc_name="
+              ^ name_to_string ctx f.item_meta.name));
           let name = ctx_compute_fun_name f true ctx in
           (* Add a prefix if necessary *)
           let name =

src/extract/ExtractBase.ml

@@ -1452,22 +1452,22 @@ let name_last_elem_as_ident (span : Meta.span) (n : llbc_name) : string =
     we remove it. We ignore disambiguators (there may be collisions, but we
     check if there are).
  *)
-let ctx_prepare_name (span : Meta.span) (ctx : extraction_ctx)
+let ctx_prepare_name (meta : T.item_meta) (ctx : extraction_ctx)
     (name : llbc_name) : llbc_name =
   (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
   match name with
   | (PeIdent (crate, _) as id) :: name ->
       if crate = ctx.crate.name then name else id :: name
   | _ ->
-      craise __FILE__ __LINE__ span
+      craise __FILE__ __LINE__ meta.span
         ("Unexpected name shape: "
         ^ TranslateCore.name_to_string ctx.trans_ctx name)
 
 (** Helper *)
-let ctx_compute_simple_name (span : Meta.span) (ctx : extraction_ctx)
+let ctx_compute_simple_name (meta : T.item_meta) (ctx : extraction_ctx)
     (name : llbc_name) : string list =
   (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
-  let name = ctx_prepare_name span ctx name in
+  let name = if meta.is_local then ctx_prepare_name meta ctx name else name in
   name_to_simple_name ctx.trans_ctx name
 
 (** Helper *)
@@ -1477,7 +1477,7 @@ let ctx_compute_simple_type_name = ctx_compute_simple_name
 let ctx_compute_type_name_no_suffix (ctx : extraction_ctx)
     (item_meta : Types.item_meta) (name : llbc_name) : string =
   let name = rename_llbc_name item_meta.attr_info name in
-  flatten_name (ctx_compute_simple_type_name item_meta.span ctx name)
+  flatten_name (ctx_compute_simple_type_name item_meta ctx name)
 
 (** Provided a basename, compute a type name.
 
@@ -1569,25 +1569,24 @@ let ctx_compute_struct_constructor (def : type_decl) (ctx : extraction_ctx)
   let tname = ctx_compute_type_name def.item_meta ctx basename in
   ExtractBuiltin.mk_struct_constructor tname
 
-let ctx_compute_fun_name_no_suffix (span : Meta.span) (ctx : extraction_ctx)
+let ctx_compute_fun_name_no_suffix (meta : T.item_meta) (ctx : extraction_ctx)
     (fname : llbc_name) : string =
-  let fname = ctx_compute_simple_name span ctx fname in
+  let fname = ctx_compute_simple_name meta ctx fname in
   (* TODO: don't convert to snake case for Coq, HOL4, F* *)
   let fname = flatten_name fname in
   match backend () with
   | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
   | Lean -> fname
 
 (** Provided a basename, compute the name of a global declaration. *)
-let ctx_compute_global_name (span : Meta.span) (ctx : extraction_ctx)
+let ctx_compute_global_name (meta : T.item_meta) (ctx : extraction_ctx)
     (name : llbc_name) : string =
+  let name = ctx_compute_simple_name meta ctx name in
   match Config.backend () with
   | Coq | FStar | HOL4 ->
-      let parts =
-        List.map to_snake_case (ctx_compute_simple_name span ctx name)
-      in
+      let parts = List.map to_snake_case name in
       String.concat "_" parts
-  | Lean -> flatten_name (ctx_compute_simple_name span ctx name)
+  | Lean -> flatten_name name
 
 (** Helper function: generate a suffix for a function name, i.e., generates
     a suffix like "_loop", "loop1", etc. to append to a function name.
@@ -1618,10 +1617,10 @@ let default_fun_suffix (num_loops : int) (loop_id : LoopId.id option) : string =
     - loop id (if pertinent)
     TODO: use the fun id for the builtin functions.
  *)
-let ctx_compute_fun_name (span : Meta.span) (ctx : extraction_ctx)
+let ctx_compute_fun_name (meta : T.item_meta) (ctx : extraction_ctx)
     (fname : llbc_name) (num_loops : int) (loop_id : LoopId.id option) : string
     =
-  let fname = ctx_compute_fun_name_no_suffix span ctx fname in
+  let fname = ctx_compute_fun_name_no_suffix meta ctx fname in
   (* Compute the suffix *)
   let suffix = default_fun_suffix num_loops loop_id in
   (* Concatenate *)
@@ -1651,8 +1650,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
           let params = trait_impl.llbc_generics in
           let args = trait_impl.llbc_impl_trait.decl_generics in
           let name =
-            ctx_prepare_name trait_impl.item_meta.span ctx
-              trait_decl.item_meta.name
+            ctx_prepare_name trait_impl.item_meta ctx trait_decl.item_meta.name
           in
           let name = rename_llbc_name trait_impl.item_meta.attr_info name in
           trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
@@ -1804,17 +1802,17 @@ let ctx_compute_trait_type_clause_name (ctx : extraction_ctx)
       the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
-let ctx_compute_termination_measure_name (span : Meta.span)
+let ctx_compute_termination_measure_name (meta : T.item_meta)
     (ctx : extraction_ctx) (_fid : A.FunDeclId.id) (fname : llbc_name)
     (num_loops : int) (loop_id : LoopId.id option) : string =
-  let fname = ctx_compute_fun_name_no_suffix span ctx fname in
+  let fname = ctx_compute_fun_name_no_suffix meta ctx fname in
   let lp_suffix = default_fun_loop_suffix num_loops loop_id in
   (* Compute the suffix *)
   let suffix =
     match Config.backend () with
     | FStar -> "_decreases"
     | Lean -> "_terminates"
-    | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
+    | Coq | HOL4 -> craise __FILE__ __LINE__ meta.span "Unexpected"
   in
   (* Concatenate *)
   fname ^ lp_suffix ^ suffix
@@ -1833,16 +1831,16 @@ let ctx_compute_termination_measure_name (span : Meta.span)
       the same purpose as in [llbc_name].
     - loop identifier, if this is for a loop
  *)
-let ctx_compute_decreases_proof_name (span : Meta.span) (ctx : extraction_ctx)
+let ctx_compute_decreases_proof_name (meta : T.item_meta) (ctx : extraction_ctx)
     (_fid : A.FunDeclId.id) (fname : llbc_name) (num_loops : int)
     (loop_id : LoopId.id option) : string =
-  let fname = ctx_compute_fun_name_no_suffix span ctx fname in
+  let fname = ctx_compute_fun_name_no_suffix meta ctx fname in
   let lp_suffix = default_fun_loop_suffix num_loops loop_id in
   (* Compute the suffix *)
   let suffix =
     match Config.backend () with
     | Lean -> "_decreases"
-    | FStar | Coq | HOL4 -> craise __FILE__ __LINE__ span "Unexpected"
+    | FStar | Coq | HOL4 -> craise __FILE__ __LINE__ meta.span "Unexpected"
   in
   (* Concatenate *)
   fname ^ lp_suffix ^ suffix
@@ -2112,7 +2110,7 @@ let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in
   let name =
-    ctx_compute_decreases_proof_name def.item_meta.span ctx def.def_id name
+    ctx_compute_decreases_proof_name def.item_meta ctx def.def_id name
       def.num_loops def.loop_id
   in
   ctx_add def.item_meta.span
@@ -2123,7 +2121,7 @@ let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
     extraction_ctx =
   let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in
   let name =
-    ctx_compute_termination_measure_name def.item_meta.span ctx def.def_id name
+    ctx_compute_termination_measure_name def.item_meta ctx def.def_id name
       def.num_loops def.loop_id
   in
   ctx_add def.item_meta.span
@@ -2145,7 +2143,7 @@ let ctx_add_global_decl_and_body (def : global_decl) (ctx : extraction_ctx) :
   | None ->
       (* Not the case: "standard" registration *)
       let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in
-      let name = ctx_compute_global_name def.item_meta.span ctx name in
+      let name = ctx_compute_global_name def.item_meta ctx name in
 
       let body = FunId (FromLlbc (FunId (FRegular def.body_id), None)) in
       (* If this is a provided constant (i.e., the default value for a constant
@@ -2205,6 +2203,10 @@ let ctx_compute_fun_name (def : fun_decl) (is_trait_decl_field : bool)
     | _ -> def.item_meta
   in
   let llbc_name = rename_llbc_name item_meta.attr_info def.item_meta.name in
+  log#ldebug
+    (lazy
+      (__FUNCTION__ ^ ": llbc_name after renaming: "
+      ^ name_to_string ctx llbc_name));
   (* When a trait method has a default implementation, this becomes a [fun_decl]
      that we may want to extract. By default, its name is [Trait::method], which
      for lean creates a name clash with the method name as a field in the trait
@@ -2219,8 +2221,12 @@ let ctx_compute_fun_name (def : fun_decl) (is_trait_decl_field : bool)
           llbc_name @ [ PeIdent ("default", Disambiguator.zero) ]
       | _ -> llbc_name
   in
-  ctx_compute_fun_name def.item_meta.span ctx llbc_name def.num_loops
-    def.loop_id
+  log#ldebug
+    (lazy
+      (__FUNCTION__
+     ^ ": llbc_name after adding 'default' suffix (for default methods): "
+      ^ name_to_string ctx llbc_name));
+  ctx_compute_fun_name def.item_meta ctx llbc_name def.num_loops def.loop_id
 
 (* TODO: move to Extract *)
 let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =

src/extract/ExtractBuiltin.ml

@@ -545,6 +545,11 @@ let mk_builtin_funs () : (pattern * Pure.builtin_fun_info) list =
            "core::slice::index::{core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
             [@T]>}::index_mut"
            ();
+         (* *)
+         mk_fun "alloc::boxed::{core::convert::AsMut<Box<@T>, @T>}::as_mut"
+           ~can_fail:false
+           ~filter:(Some [ true; false ])
+           ();
        ]
       @ List.flatten
           (List.map
@@ -719,8 +724,10 @@ let builtin_trait_decls_info () =
           ();
         (* Debug *)
         mk_trait "core::fmt::Debug" ~types:[ "T" ] ~methods:[ "fmt" ] ();
+        (* *)
         mk_trait "core::convert::TryFrom" ~methods:[ "try_from" ] ();
         mk_trait "core::convert::TryInto" ~methods:[ "try_into" ] ();
+        mk_trait "core::convert::AsMut" ~methods:[ "as_mut" ] ();
       ]
 
 let mk_builtin_trait_decls_map () =
@@ -822,6 +829,9 @@ let builtin_trait_impls_info () : (pattern * Pure.builtin_trait_impl_info) list
           "core::slice::index::SliceIndex<core::ops::range::RangeFrom<usize>, \
            [@Self]>"
           ();
+        fmt "core::convert::AsMut<Box<@Self>, @Self>"
+          ~filter:(Some [ true; false ])
+          ();
       ]
   (* From<INT, bool> *)
   @ List.map

tests/lean/AsMut.lean

@@ -0,0 +1,25 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [as_mut]
+import Aeneas
+open Aeneas.Std Result Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+namespace as_mut
+
+/- [as_mut::use_box_as_mut]:
+   Source: 'tests/src/as_mut.rs', lines 2:0-4:1 -/
+def use_box_as_mut {T : Type} (x : T) : Result (T × (T → T)) :=
+  ok (alloc.boxed.AsMutBoxT.as_mut x)
+
+/- [as_mut::use_as_mut]:
+   Source: 'tests/src/as_mut.rs', lines 6:0-8:1 -/
+def use_as_mut
+  {S : Type} {T : Type} (coreconvertAsMutInst : core.convert.AsMut T S) 
+  (x : T) :
+  Result (S × (S → T))
+  :=
+  coreconvertAsMutInst.as_mut x
+
+end as_mut

tests/src/as_mut.rs

@@ -0,0 +1,8 @@
+//@ [!lean] skip
+fn use_box_as_mut<T>(mut x : &mut Box<T>) -> &mut T{
+    x.as_mut()
+}
+
+fn use_as_mut<S, T : core::convert::AsMut<S>>(mut x : &mut T) -> &mut S {
+    x.as_mut()
+}