summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorSon Ho2023-11-29 17:33:52 +0100
committerSon Ho2023-11-29 17:33:52 +0100
commit054d7256ed90f752ae6b39ebba608f89076d38e7 (patch)
tree4e1732cdf01891fbf564644f73789365a68ce3d1 /compiler
parent789ba1473acd287814a0d659b5f5a0e480e4e9d7 (diff)
Update the code following changes in the NameMatcher
Diffstat (limited to '')
-rw-r--r--compiler/ExtractName.ml17
-rw-r--r--compiler/FunsAnalysis.ml2
-rw-r--r--compiler/LlbcAstUtils.ml2
-rw-r--r--compiler/TranslateCore.ml8
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