Merge pull request #442 from AeneasVerif/son/fix

Fix some naming issues

src/PrePasses.ml

@@ -661,27 +661,12 @@ let decompose_str_borrows (f : fun_decl) : fun_decl =
   in
   { f with body }
 
-(** 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
-    struct. We therefore rename these function items to avoid the name clash.
- *)
-let rename_default_methods (def : fun_decl) : fun_decl =
-  match def.kind with
-  | TraitDeclItem (_, _, true) ->
-      let name =
-        def.item_meta.name @ [ PeIdent ("default", Disambiguator.zero) ]
-      in
-      { def with item_meta = { def.item_meta with name } }
-  | _ -> def
-
 let apply_passes (crate : crate) : crate =
   let function_passes =
     [
       remove_loop_breaks crate;
       remove_shallow_borrows crate;
       decompose_str_borrows;
-      rename_default_methods;
     ]
   in
   (* Attempt to apply a pass: if it fails we replace the body by [None] *)

src/extract/Extract.ml

@@ -24,12 +24,13 @@ let texpression_to_string (ctx : extraction_ctx) =
 let extract_fun_decl_register_names (ctx : extraction_ctx)
     (has_decreases_clause : fun_decl -> bool) (def : pure_fun_translation) :
     extraction_ctx =
-  (* Ignore the trait methods **declarations** (rem.: we do not ignore the trait
-     method implementations): we do not need to refer to them directly. We will
-     only use their type for the fields of the records we generate for the trait
-     declarations *)
   match def.f.kind with
-  | TraitDeclItem (_, _, false) -> ctx
+  | TraitDeclItem (_, _, false) ->
+      (* Ignore the trait methods **declarations** (rem.: we do not ignore the trait
+         method implementations): we do not need to refer to them directly. We will
+         only use their type for the fields of the records we generate for the trait
+         declarations *)
+      ctx
   | _ -> (
       (* Check if the function is builtin *)
       let builtin =
@@ -2328,7 +2329,7 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
           let f =
             { f with item_meta = { f.item_meta with name = llbc_name } }
           in
-          let name = ctx_compute_fun_name f ctx in
+          let name = ctx_compute_fun_name f true ctx in
           (* Add a prefix if necessary *)
           let name =
             if !record_fields_short_names then name

src/extract/ExtractBase.ml

@@ -2158,7 +2158,12 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) :
       let ctx = ctx_add def.item_meta.span body (name ^ suffix ^ "_body") ctx in
       ctx
 
-let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
+(** - [is_trait_decl_field]: [true] if we are computing the name of a field
+      in a trait declaration, [false] if we are computing the name of a function
+      declaration.
+ *)
+let ctx_compute_fun_name (def : fun_decl) (is_trait_decl_field : bool)
+    (ctx : extraction_ctx) : string =
   (* Rename the function, if the user added a [rename] attribute.
 
      We have to do something peculiar for the implementation of trait
@@ -2197,6 +2202,20 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
     | _ -> def.item_meta
   in
   let llbc_name = rename_llbc_name item_meta.attr_info def.item_meta.name in
+  (* 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
+     struct. We therefore rename these function items to avoid the name clash by
+     adding the "default" suffix.
+  *)
+  let llbc_name =
+    if is_trait_decl_field then llbc_name
+    else
+      match def.kind with
+      | TraitDeclItem (_, _, true) ->
+          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
 
@@ -2209,7 +2228,7 @@ let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
     def.item_meta.span;
   let def_id = def.def_id in
   (* Add the function name *)
-  let def_name = ctx_compute_fun_name def ctx in
+  let def_name = ctx_compute_fun_name def false ctx in
   let fun_id = (Pure.FunId (FRegular def_id), def.loop_id) in
   ctx_add def.item_meta.span (FunId (FromLlbc fun_id)) def_name ctx
 

tests/coq/rename_attribute/RenameAttribute.v

@@ -100,9 +100,9 @@ Definition no_borrows_sum (n : nat) (max : u32) : result u32 :=
   no_borrows_sum_loop n max 0%u32 0%u32
 .
 
-(** [rename_attribute::BoolTrait::ret_true::default]:
+(** [rename_attribute::BoolTrait::ret_true]:
     Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-Definition boolTrait_ret_true_retTest
+Definition boolTrait_retTest_default
   {Self : Type} (self_clause : BoolTest_t Self) (self : Self) : result bool :=
   Ok true
 .

tests/coq/traits/Traits.v

@@ -705,7 +705,7 @@ Definition use_foo2
   Ok (foo_foo T traitInst)
 .
 
-(** [traits::BoolTrait::ret_true::default]:
+(** [traits::BoolTrait::ret_true]:
     Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
 Definition boolTrait_ret_true_default
   {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool :=

tests/fstar/rename_attribute/RenameAttribute.Funs.fst

@@ -65,9 +65,9 @@ let rec no_borrows_sum_loop
 let no_borrows_sum (max : u32) : result u32 =
   no_borrows_sum_loop max 0 0
 
-(** [rename_attribute::BoolTrait::ret_true::default]:
+(** [rename_attribute::BoolTrait::ret_true]:
     Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 *)
-let boolTrait_ret_true_retTest
+let boolTrait_retTest_default
   (#self : Type0) (self_clause : boolTest_t self) (self1 : self) :
   result bool
   =

tests/fstar/traits/Traits.fst

@@ -531,7 +531,7 @@ let use_foo2
   =
   Ok (foo_foo t traitInst)
 
-(** [traits::BoolTrait::ret_true::default]:
+(** [traits::BoolTrait::ret_true]:
     Source: 'tests/src/traits.rs', lines 8:4-10:5 *)
 let boolTrait_ret_true_default
   (#self : Type0) (self_clause : boolTrait_t self) (self1 : self) :

tests/lean/RenameAttribute.lean

@@ -91,9 +91,9 @@ divergent def No_borrows_sum_loop
 def No_borrows_sum (max : U32) : Result U32 :=
   No_borrows_sum_loop max 0#u32 0#u32
 
-/- [rename_attribute::BoolTrait::ret_true::default]:
+/- [rename_attribute::BoolTrait::ret_true]:
    Source: 'tests/src/rename_attribute.rs', lines 15:4-17:5 -/
-def BoolTrait.ret_true.retTest
+def BoolTrait.retTest.default
   {Self : Type} (self_clause : BoolTest Self) (self : Self) : Result Bool :=
   Result.ok true
 

tests/lean/Traits.lean

@@ -550,7 +550,7 @@ def use_foo2
   :=
   Result.ok (Foo.FOO T TraitInst)
 
-/- [traits::BoolTrait::ret_true::default]:
+/- [traits::BoolTrait::ret_true]:
    Source: 'tests/src/traits.rs', lines 8:4-10:5 -/
 def BoolTrait.ret_true.default
   {Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=