diff --git a/src/PrePasses.ml b/src/PrePasses.ml index 5b9b7627..245da018 100644 --- a/src/PrePasses.ml +++ b/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] *) diff --git a/src/extract/Extract.ml b/src/extract/Extract.ml index 827abdd2..74796b5d 100644 --- a/src/extract/Extract.ml +++ b/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 diff --git a/src/extract/ExtractBase.ml b/src/extract/ExtractBase.ml index 8a6edb32..78d8a948 100644 --- a/src/extract/ExtractBase.ml +++ b/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 diff --git a/tests/coq/rename_attribute/RenameAttribute.v b/tests/coq/rename_attribute/RenameAttribute.v index a5eaf441..dee95439 100644 --- a/tests/coq/rename_attribute/RenameAttribute.v +++ b/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 . diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v index dea5c5bc..cd965669 100644 --- a/tests/coq/traits/Traits.v +++ b/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 := diff --git a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst b/tests/fstar/rename_attribute/RenameAttribute.Funs.fst index 7aa7c249..7325409d 100644 --- a/tests/fstar/rename_attribute/RenameAttribute.Funs.fst +++ b/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 = diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst index 9e65fd25..c9505fb0 100644 --- a/tests/fstar/traits/Traits.fst +++ b/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) : diff --git a/tests/lean/RenameAttribute.lean b/tests/lean/RenameAttribute.lean index d67b1885..ae9432e4 100644 --- a/tests/lean/RenameAttribute.lean +++ b/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 diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index a7cf2a2d..ac612e3e 100644 --- a/tests/lean/Traits.lean +++ b/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 :=