diff options
| -rw-r--r-- | compiler/Extract.ml | 13 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 2 |
2 files changed, 7 insertions, 8 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 60455cd9..ecfb47c7 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -732,21 +732,20 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) in let trait_decl_name (trait_decl : trait_decl) : string = - type_name_to_snake_case trait_decl.name + type_name trait_decl.name in let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) : string = (* TODO: provisional: we concatenate the trait impl name (which is its type) with the trait decl name *) - let inst_keyword = + let trait_decl = + let name = trait_decl.name in match !backend with - | HOL4 | FStar | Coq -> "_instance" - | Lean -> "Instance" + | FStar | Coq | HOL4 -> type_name_to_snake_case name ^ "_instance" + | Lean -> String.concat "" (get_type_name name) ^ "Instance" in - flatten_name - (get_type_name trait_impl.name - @ [ trait_decl_name trait_decl ^ inst_keyword ]) + flatten_name (get_type_name trait_impl.name @ [ trait_decl ]) in let trait_parent_clause_name (trait_decl : trait_decl) (clause : trait_clause) diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 1996d38f..28928325 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1339,7 +1339,7 @@ let ctx_add_trait_method (d : trait_decl) (item_name : string) (f : fun_decl) (* Add a prefix if necessary *) let name = if !Config.record_fields_short_names then name - else ctx.fmt.trait_decl_name d ^ name + else ctx.fmt.trait_decl_name d ^ "_" ^ name in let is_opaque = false in ctx_add is_opaque (TraitMethodId (d.def_id, item_name, f.back_id)) name ctx |