diff options
author | Son Ho | 2023-11-20 21:58:25 +0100 |
---|---|---|
committer | Son Ho | 2023-11-20 21:58:25 +0100 |
commit | 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 (patch) | |
tree | ed1f2e69fe173e25b6c137c350e87a855b513e46 /compiler/LlbcAstUtils.ml | |
parent | 4a3779de578cebe01143bb18d295457107be1e3a (diff) |
Use the name matcher implemented in Charon
Diffstat (limited to 'compiler/LlbcAstUtils.ml')
-rw-r--r-- | compiler/LlbcAstUtils.ml | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 01216157..ffdce481 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -31,21 +31,26 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : type_decl list * fun_decl list = let open ExtractBuiltin in + let ctx : Charon.NameMatcher.ctx = + { + type_decls = k.type_decls; + global_decls = k.global_decls; + trait_decls = k.trait_decls; + } + in let is_opaque_fun (d : fun_decl) : bool = - let sname = name_to_simple_name d.name in d.body = None (* Something to pay attention to: we must ignore trait method *declarations* (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitMethodDecl _ -> false | _ -> true) && ((not filter_assumed) - || (not (SimpleNameMap.mem sname builtin_globals_map)) - && not (SimpleNameMap.mem sname (builtin_funs_map ()))) + || (not (NameMatcherMap.mem ctx d.name builtin_globals_map)) + && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ()))) in let is_opaque_type (d : type_decl) : bool = - let sname = name_to_simple_name d.name in d.kind = Opaque && ((not filter_assumed) - || not (SimpleNameMap.mem sname (builtin_types_map ()))) + || not (NameMatcherMap.mem ctx d.name (builtin_types_map ()))) in (* Note that by checking the function bodies we also the globals *) ( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls), |