diff options
| -rw-r--r-- | compiler/ExtractName.ml | 17 | ||||
| -rw-r--r-- | compiler/FunsAnalysis.ml | 2 | ||||
| -rw-r--r-- | compiler/LlbcAstUtils.ml | 2 | ||||
| -rw-r--r-- | compiler/TranslateCore.ml | 8 |
4 files changed, 23 insertions, 6 deletions
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml index a916bffb..2ccd4af6 100644 --- a/compiler/ExtractName.ml +++ b/compiler/ExtractName.ml @@ -3,13 +3,14 @@ open Charon.NameMatcher let log = Logging.extract_log +let match_with_trait_decl_refs = true module NameMatcherMap = struct module NMM = NameMatcherMap type 'a t = 'a NMM.t - let config = { map_vars_to_vars = true } + let config = { map_vars_to_vars = true; match_with_trait_decl_refs } let find_opt (ctx : ctx) (name : Types.name) (m : 'a t) : 'a option = NMM.find_opt ctx config name m @@ -85,7 +86,9 @@ let pattern_to_trait_impl_extract_name = pattern_to_extract_name true consistent with the extraction names we derive from the Rust names *) let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.name) : string list = - let c : to_pat_config = { tgt = TkName } in + let c : to_pat_config = + { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs } + in pattern_to_extract_name is_trait_impl (name_to_pattern ctx c n) (** If the [prefix] is Some, we attempt to remove the common prefix @@ -93,15 +96,17 @@ let name_to_simple_name (ctx : ctx) (is_trait_impl : bool) (n : Types.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 - let name = name_with_generics_to_pattern ctx c name p g in + let c : to_pat_config = + { tgt = TkName; use_trait_decl_refs = match_with_trait_decl_refs } + in + let name = name_with_generics_to_pattern ctx c p name 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 + name_with_generics_to_pattern ctx c TypesUtils.empty_generic_params + prefix TypesUtils.empty_generic_args in let _, _, name = pattern_common_prefix prefix name in name diff --git a/compiler/FunsAnalysis.ml b/compiler/FunsAnalysis.ml index 9ae6ce86..2f950083 100644 --- a/compiler/FunsAnalysis.ml +++ b/compiler/FunsAnalysis.ml @@ -62,7 +62,9 @@ let analyze_module (m : crate) (funs_map : fun_decl FunDeclId.Map.t) { type_decls = m.type_decls; global_decls = m.global_decls; + fun_decls = m.fun_decls; trait_decls = m.trait_decls; + trait_impls = m.trait_impls; } in diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index ffdce481..d3fac032 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -35,7 +35,9 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : { type_decls = k.type_decls; global_decls = k.global_decls; + fun_decls = k.fun_decls; trait_decls = k.trait_decls; + trait_impls = k.trait_impls; } in let is_opaque_fun (d : fun_decl) : bool = diff --git a/compiler/TranslateCore.ml b/compiler/TranslateCore.ml index abf4fcf7..88438872 100644 --- a/compiler/TranslateCore.ml +++ b/compiler/TranslateCore.ml @@ -39,7 +39,9 @@ let match_name_find_opt (ctx : trans_ctx) (name : Types.name) { type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; } in NameMatcherMap.find_opt mctx name m @@ -52,7 +54,9 @@ let match_name_with_generics_find_opt (ctx : trans_ctx) (name : Types.name) { type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; } in NameMatcherMap.find_with_generics_opt mctx name generics m @@ -62,7 +66,9 @@ let name_to_simple_name (ctx : trans_ctx) (n : Types.name) : string list = { type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; } in let is_trait_impl = false in @@ -75,7 +81,9 @@ let trait_name_with_generics_to_simple_name (ctx : trans_ctx) { type_decls = ctx.type_ctx.type_decls; global_decls = ctx.global_ctx.global_decls; + fun_decls = ctx.fun_ctx.fun_decls; trait_decls = ctx.trait_decls_ctx.trait_decls; + trait_impls = ctx.trait_impls_ctx.trait_impls; } in let is_trait_impl = true in |