diff options
| -rw-r--r-- | compiler/ExtractBase.ml | 23 | ||||
| -rw-r--r-- | compiler/ExtractName.ml | 24 | ||||
| -rw-r--r-- | compiler/TranslateCore.ml | 9 |
3 files changed, 45 insertions, 11 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 6f227003..cfba7324 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1495,8 +1495,8 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) in let params = trait_impl.generics in let args = trait_impl.impl_trait.decl_generics in - name_with_generics_to_simple_name ctx.trans_ctx trait_decl.llbc_name params - args + trait_name_with_generics_to_simple_name ctx.trans_ctx trait_decl.llbc_name + params args in let name = flatten_name name in match !backend with @@ -1516,6 +1516,21 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx) *) (* We need to lookup the LLBC definitions, to have the original instantiation *) let clause = + (* If the current trait decl and the trait decl referenced by the clause + are in the same namespace, we try to simplify the names. We do so by + removing the common prefixes in their names. + + For instance, if we have: + {[ + // This is file traits.rs + trait Parent {} + + trait Child : Parent {} + ]} + For the parent clause of trait [Child] we would like to generate + the name: "ParentInst", rather than "traitParentInst". + *) + let prefix = Some trait_decl.llbc_name in let trait_decl = TraitDeclId.Map.find trait_decl.def_id ctx.crate.trait_decls in @@ -1528,8 +1543,8 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx) let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in let params = trait_decl.generics in let args = clause.clause_generics in - name_with_generics_to_simple_name ctx.trans_ctx impl_trait_decl.name params - args + trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix + impl_trait_decl.name params args in let clause = String.concat "" clause in let clause = diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index 6d50ed73..f7177223 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -82,14 +82,30 @@ let pattern_to_trait_impl_extract_name = pattern_to_extract_name true (* TODO: this is provisional. We just want to make sure that the extraction names we derive from the patterns (for the builtin definitions) are consistent with the extraction names we derive from the Rust names *) -let name_to_simple_name (ctx : ctx) (n : Types.name) : string list = +let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) : + string list = let c : to_pat_config = { tgt = TkName } in - pattern_to_extract_name false (name_to_pattern ctx c n) + pattern_to_extract_name is_trait_impl (name_to_pattern ctx c n) -let name_with_generics_to_simple_name (ctx : ctx) (n : Types.name) +(** If the [prefix] is Some, we attempt to remove the common prefix + between [prefix] and [name] from [name] *) +let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool) + ?(prefix : Types.name option = None) (name : Types.name) (p : Types.generic_params) (g : Types.generic_args) : string list = let c : to_pat_config = { tgt = TkName } in - pattern_to_extract_name true (name_with_generics_to_pattern ctx c n p g) + let name = name_with_generics_to_pattern ctx c name p g in + let name = + match prefix with + | None -> name + | Some prefix -> + let prefix = + name_with_generics_to_pattern ctx c prefix + TypesUtils.empty_generic_params TypesUtils.empty_generic_args + in + let _, _, name = pattern_common_prefix prefix name in + name + in + pattern_to_extract_name is_trait_impl name (* (* Prepare a name. diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index f251e169..abf4fcf7 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -65,9 +65,11 @@ let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list = trait_decls = ctx.trait_decls_ctx.trait_decls; } in - name_to_simple_name mctx n + let is_trait_impl = false in + name_to_simple_name mctx is_trait_impl n -let name_with_generics_to_simple_name (ctx : trans_ctx) (n : Types.name) +let trait_name_with_generics_to_simple_name (ctx : trans_ctx) + ?(prefix : Types.name option = None) (n : Types.name) (p : Types.generic_params) (g : Types.generic_args) : string list = let mctx : Charon.NameMatcher.ctx = { @@ -76,4 +78,5 @@ let name_with_generics_to_simple_name (ctx : trans_ctx) (n : Types.name) trait_decls = ctx.trait_decls_ctx.trait_decls; } in - name_with_generics_to_simple_name mctx n p g + let is_trait_impl = true in + name_with_generics_to_simple_name mctx is_trait_impl ~prefix n p g |