From b9f33bdd871a1bd7a1bd29f148dd05bd7990548b Mon Sep 17 00:00:00 2001 From: Son Ho Date: Sun, 12 Nov 2023 19:28:56 +0100 Subject: Remove the 'r type variable from the ty type definition --- compiler/LlbcAstUtils.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 0ab4ed94..46b36851 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -4,14 +4,14 @@ include Charon.LlbcAstUtils let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = match fun_id with - | Regular id -> (FunDeclId.Map.find id fun_decls).signature - | Assumed aid -> Assumed.get_assumed_fun_sig aid + | FRegular id -> (FunDeclId.Map.find id fun_decls).signature + | FAssumed aid -> Assumed.get_assumed_fun_sig aid let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : Names.fun_name = match fun_id with - | Regular id -> (FunDeclId.Map.find id fun_decls).name - | Assumed aid -> Assumed.get_assumed_fun_name aid + | FRegular id -> (FunDeclId.Map.find id fun_decls).name + | FAssumed aid -> Assumed.get_assumed_fun_name aid (** Return the opaque declarations found in the crate, which are also *not builtin*. -- cgit v1.2.3 From 6c88d30031255c0ac612b67bb5b3c20c2f07e563 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 13 Nov 2023 13:27:02 +0100 Subject: Add RegionsHierarchy.ml --- compiler/LlbcAstUtils.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 46b36851..de46320b 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -1,5 +1,18 @@ open LlbcAst include Charon.LlbcAstUtils +open Collections + +module FunIdOrderedType : OrderedType with type t = fun_id = struct + type t = fun_id + + let compare = compare_fun_id + let to_string = show_fun_id + let pp_t = pp_fun_id + let show_t = show_fun_id +end + +module FunIdMap = Collections.MakeMap (FunIdOrderedType) +module FunIdSet = Collections.MakeSet (FunIdOrderedType) let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : fun_sig = -- cgit v1.2.3 From 21e3b719f2338f4d4a65c91edc0eb83d0b22393e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 15 Nov 2023 22:03:21 +0100 Subject: Start updating the name type, cleanup the names and the module abbrevs --- compiler/LlbcAstUtils.ml | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index de46320b..01216157 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -1,3 +1,4 @@ +open Types open LlbcAst include Charon.LlbcAstUtils open Collections @@ -20,12 +21,6 @@ let lookup_fun_sig (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : | FRegular id -> (FunDeclId.Map.find id fun_decls).signature | FAssumed aid -> Assumed.get_assumed_fun_sig aid -let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : - Names.fun_name = - match fun_id with - | FRegular id -> (FunDeclId.Map.find id fun_decls).name - | FAssumed aid -> Assumed.get_assumed_fun_name aid - (** Return the opaque declarations found in the crate, which are also *not builtin*. [filter_assumed]: if [true], do not consider as opaque the external definitions @@ -34,7 +29,7 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : Remark: the list of functions also contains the list of opaque global bodies. *) let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : - T.type_decl list * fun_decl list = + type_decl list * fun_decl list = let open ExtractBuiltin in let is_opaque_fun (d : fun_decl) : bool = let sname = name_to_simple_name d.name in @@ -46,15 +41,15 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : || (not (SimpleNameMap.mem sname builtin_globals_map)) && not (SimpleNameMap.mem sname (builtin_funs_map ()))) in - let is_opaque_type (d : T.type_decl) : bool = + let is_opaque_type (d : type_decl) : bool = let sname = name_to_simple_name d.name in - d.kind = T.Opaque + d.kind = Opaque && ((not filter_assumed) || not (SimpleNameMap.mem sname (builtin_types_map ()))) in (* Note that by checking the function bodies we also the globals *) - ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types), - List.filter is_opaque_fun (FunDeclId.Map.values k.functions) ) + ( List.filter is_opaque_type (TypeDeclId.Map.values k.type_decls), + List.filter is_opaque_fun (FunDeclId.Map.values k.fun_decls) ) (** Return true if the crate contains opaque declarations, ignoring the assumed definitions. *) -- cgit v1.2.3 From 672ceef25203ebd5fcf5a55e294a4ebfe65648d6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 20 Nov 2023 21:58:25 +0100 Subject: Use the name matcher implemented in Charon --- compiler/LlbcAstUtils.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) (limited to 'compiler/LlbcAstUtils.ml') 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), -- cgit v1.2.3