summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml61
-rw-r--r--compiler/ExtractBase.ml17
-rw-r--r--compiler/ExtractTypes.ml16
-rw-r--r--compiler/Pure.ml6
-rw-r--r--compiler/PureMicroPasses.ml1
-rw-r--r--compiler/PureUtils.ml2
-rw-r--r--compiler/SymbolicToPure.ml18
-rw-r--r--compiler/Translate.ml9
8 files changed, 59 insertions, 71 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 1fbce7fd..cf632388 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -26,7 +26,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx)
let builtin =
let open ExtractBuiltin in
let funs_map = builtin_funs_map () in
- match_name_find_opt ctx.trans_ctx def.f.llbc_name funs_map
+ match_name_find_opt ctx.trans_ctx def.f.item_meta.name funs_map
in
(* Use the builtin names if necessary *)
match builtin with
@@ -214,7 +214,7 @@ let fun_builtin_filter_types (id : FunDeclId.id) (types : 'a list)
let decl = FunDeclId.Map.find id ctx.trans_funs in
let err =
"Ill-formed builtin information for function "
- ^ name_to_string ctx decl.f.llbc_name
+ ^ name_to_string ctx decl.f.item_meta.name
^ ": "
^ string_of_int (List.length filter)
^ " filtering arguments provided for "
@@ -1158,7 +1158,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx)
(* Add the type parameters - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params def.item_meta.span def.llbc_name
+ ctx_add_generic_params def.item_meta.span def.item_meta.name
def.signature.llbc_generics def.signature.generics ctx
in
(* Print the generics *)
@@ -1259,11 +1259,11 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
(* Print a comment to link the extracted type to its original rust definition *)
(let name =
if !extract_external_name_patterns && not def.item_meta.is_local then
- Some def.llbc_name
+ Some def.item_meta.name
else None
in
extract_comment_with_raw_span ctx fmt
- [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
+ [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: decreases clause" ]
name def.item_meta.span.span);
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
@@ -1332,7 +1332,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
F.pp_print_break fmt 0 0;
(* Print a comment to link the extracted type to its original rust definition *)
extract_comment_with_raw_span ctx fmt
- [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
+ [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: termination measure" ]
None def.item_meta.span.span;
F.pp_print_space fmt ();
(* Open a box for the definition, so that whenever possible it gets printed on
@@ -1391,7 +1391,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
(* syntax <def_name> term ... term : tactic *)
F.pp_print_break fmt 0 0;
extract_comment_with_raw_span ctx fmt
- [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
+ [ "[" ^ name_to_string ctx def.item_meta.name ^ "]: decreases_by tactic" ]
None def.item_meta.span.span;
F.pp_print_space fmt ();
F.pp_open_hvbox fmt 0;
@@ -1423,7 +1423,7 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
(def : fun_decl) : unit =
- let comment_pre = "[" ^ name_to_string ctx def.llbc_name ^ "]:" in
+ let comment_pre = "[" ^ name_to_string ctx def.item_meta.name ^ "]:" in
let comment =
let loop_comment =
match def.loop_id with
@@ -1434,7 +1434,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
in
let name =
if !extract_external_name_patterns && not def.item_meta.is_local then
- Some def.llbc_name
+ Some def.item_meta.name
else None
in
extract_comment_with_raw_span ctx fmt comment name def.item_meta.span.span
@@ -1722,7 +1722,7 @@ let extract_fun_decl_hol4_opaque (ctx : extraction_ctx) (fmt : F.formatter)
(* Add the type/const gen parameters - note that we need those bindings
only for the generation of the type (they are not top-level) *)
let ctx, _, _, _ =
- ctx_add_generic_params def.item_meta.span def.llbc_name
+ ctx_add_generic_params def.item_meta.span def.item_meta.name
def.signature.llbc_generics def.signature.generics ctx
in
(* Add breaks to insert new lines between definitions *)
@@ -1925,11 +1925,11 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
let name =
if !extract_external_name_patterns && not global.item_meta.is_local then
- Some global.llbc_name
+ Some global.item_meta.name
else None
in
extract_comment_with_raw_span ctx fmt
- [ "[" ^ name_to_string ctx global.llbc_name ^ "]" ]
+ [ "[" ^ name_to_string ctx global.item_meta.name ^ "]" ]
name global.span.span;
F.pp_print_space fmt ();
@@ -1947,7 +1947,7 @@ let extract_global_decl_aux (ctx : extraction_ctx) (fmt : F.formatter)
in
(* Add the type parameters *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params span global.llbc_name global.llbc_generics
+ ctx_add_generic_params span global.item_meta.name global.llbc_generics
global.generics ctx
in
match body.body with
@@ -2173,7 +2173,9 @@ let extract_trait_decl_method_names (ctx : extraction_ctx)
let llbc_name : Types.name =
[ Types.PeIdent (item_name, Disambiguator.zero) ]
in
- let f = { f with llbc_name } in
+ let f =
+ { f with item_meta = { f.item_meta with name = llbc_name } }
+ in
let name = ctx_compute_fun_name f ctx in
(* Add a prefix if necessary *)
let name =
@@ -2208,7 +2210,7 @@ let extract_trait_decl_register_names (ctx : extraction_ctx)
(* Lookup the information if this is a builtin trait *)
let open ExtractBuiltin in
let builtin_info =
- match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+ match_name_find_opt ctx.trans_ctx trait_decl.item_meta.name
(builtin_trait_decls_map ())
in
let ctx =
@@ -2254,7 +2256,7 @@ let extract_trait_impl_register_names (ctx : extraction_ctx)
TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
in
let decl_ref = trait_impl.impl_trait in
- match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+ match_name_with_generics_find_opt ctx.trans_ctx trait_decl.item_meta.name
decl_ref.decl_generics
(builtin_trait_impls_map ())
in
@@ -2360,7 +2362,7 @@ let extract_trait_decl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
- we only generate trait clauses for the clauses we find in the
pure generics *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.item_meta.span f.llbc_name
+ ctx_add_generic_params decl.item_meta.span f.item_meta.name
f.signature.llbc_generics generics ctx
in
let backend_uses_forall =
@@ -2390,11 +2392,11 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Print a comment to link the extracted type to its original rust definition *)
(let name =
if !extract_external_name_patterns && not decl.item_meta.is_local then
- Some decl.llbc_name
+ Some decl.item_meta.name
else None
in
extract_comment_with_raw_span ctx fmt
- [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
+ [ "Trait declaration: [" ^ name_to_string ctx decl.item_meta.name ^ "]" ]
name decl.item_meta.span.span);
F.pp_print_break fmt 0 0;
(* Open two outer boxes for the definition, so that whenever possible it gets printed on
@@ -2429,8 +2431,8 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add the type and const generic params - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.item_meta.span decl.llbc_name decl.llbc_generics
- generics ctx
+ ctx_add_generic_params decl.item_meta.span decl.item_meta.name
+ decl.llbc_generics generics ctx
in
extract_generic_params decl.item_meta.span ctx fmt TypeDeclId.Set.empty
generics type_params cg_params trait_clauses;
@@ -2666,7 +2668,7 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
- we only generate trait clauses for the clauses we find in the
pure generics *)
let ctx, f_tys, f_cgs, f_tcs =
- ctx_add_generic_params impl.item_meta.span f.llbc_name
+ ctx_add_generic_params impl.item_meta.span f.item_meta.name
f.signature.llbc_generics f_generics ctx
in
let use_forall = f_generics <> empty_generic_params in
@@ -2696,7 +2698,8 @@ let extract_trait_impl_method_items (ctx : extraction_ctx) (fmt : F.formatter)
(** Extract a trait implementation *)
let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(impl : trait_impl) : unit =
- log#ldebug (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.llbc_name));
+ log#ldebug
+ (lazy ("extract_trait_impl: " ^ name_to_string ctx impl.item_meta.name));
(* Retrieve the impl name *)
let impl_name = ctx_get_trait_impl impl.item_meta.span impl.def_id ctx in
(* Add a break before *)
@@ -2707,12 +2710,14 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
let decl_id = impl.impl_trait.trait_decl_id in
let trait_decl = TraitDeclId.Map.find decl_id ctx.trans_trait_decls in
let decl_ref = impl.llbc_impl_trait in
- ( Some trait_decl.llbc_name,
+ ( Some trait_decl.item_meta.name,
Some (trait_decl.llbc_generics, decl_ref.decl_generics) )
else (None, None)
in
extract_comment_with_raw_span ctx fmt
- [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
+ [
+ "Trait implementation: [" ^ name_to_string ctx impl.item_meta.name ^ "]";
+ ]
(* TODO: why option option for the generics? Looks like a bug in OCaml!? *)
name ?generics:(Some generics) impl.item_meta.span.span);
F.pp_print_break fmt 0 0;
@@ -2744,8 +2749,8 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
(* Add the type and const generic params - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params impl.item_meta.span impl.llbc_name impl.llbc_generics
- impl.generics ctx
+ ctx_add_generic_params impl.item_meta.span impl.item_meta.name
+ impl.llbc_generics impl.generics ctx
in
let all_generics = (type_params, cg_params, trait_clauses) in
extract_generic_params impl.item_meta.span ctx fmt TypeDeclId.Set.empty
@@ -2913,7 +2918,7 @@ let extract_unit_test_if_unit_fun (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_break fmt 0 0;
(* Print a comment *)
extract_comment fmt
- [ "Unit test for [" ^ name_to_string ctx def.llbc_name ^ "]" ];
+ [ "Unit test for [" ^ name_to_string ctx def.item_meta.name ^ "]" ];
F.pp_print_space fmt ();
(* Open a box for the test *)
F.pp_open_hovbox fmt ctx.indent_incr;
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 57131dad..4d05f0d0 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1467,7 +1467,7 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl)
(some backends don't support collision of variant names) *)
if !variant_concatenate_type_name then
StringUtils.capitalize_first_letter
- (ctx_compute_type_name_no_suffix ctx def.item_meta def.llbc_name
+ (ctx_compute_type_name_no_suffix ctx def.item_meta def.item_meta.name
^ "_" ^ variant)
else variant
| Lean -> variant
@@ -1549,7 +1549,7 @@ let ctx_compute_fun_name (span : Meta.span) (ctx : extraction_ctx)
let ctx_compute_trait_decl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
: string =
let llbc_name =
- rename_llbc_name trait_decl.item_meta.attr_info trait_decl.llbc_name
+ rename_llbc_name trait_decl.item_meta.attr_info trait_decl.item_meta.name
in
ctx_compute_type_name trait_decl.item_meta ctx llbc_name
@@ -1570,7 +1570,8 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl)
let params = trait_impl.llbc_generics in
let args = trait_impl.llbc_impl_trait.decl_generics in
let name =
- ctx_prepare_name trait_impl.item_meta.span ctx trait_decl.llbc_name
+ ctx_prepare_name trait_impl.item_meta.span ctx
+ trait_decl.item_meta.name
in
let name = rename_llbc_name trait_impl.item_meta.attr_info name in
trait_name_with_generics_to_simple_name ctx.trans_ctx name params args
@@ -1646,7 +1647,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
*)
(* We need to lookup the LLBC definitions, to have the original instantiation *)
let clause =
- let current_def_name = trait_decl.llbc_name in
+ let current_def_name = trait_decl.item_meta.name in
let params = trait_decl.llbc_generics in
ctx_compute_trait_clause_name ctx current_def_name params
trait_decl.llbc_parent_clauses clause.clause_id
@@ -2009,7 +2010,7 @@ let ctx_add_generic_params (span : Meta.span) (current_def_name : Types.name)
let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
- let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in
+ let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in
let name =
ctx_compute_decreases_proof_name def.item_meta.span ctx def.def_id name
def.num_loops def.loop_id
@@ -2020,7 +2021,7 @@ let ctx_add_decreases_proof (def : fun_decl) (ctx : extraction_ctx) :
let ctx_add_termination_measure (def : fun_decl) (ctx : extraction_ctx) :
extraction_ctx =
- let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in
+ let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in
let name =
ctx_compute_termination_measure_name def.item_meta.span ctx def.def_id name
def.num_loops def.loop_id
@@ -2104,7 +2105,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string =
~default:def.item_meta))
| _ -> def.item_meta
in
- let llbc_name = rename_llbc_name item_meta.attr_info def.llbc_name in
+ let llbc_name = rename_llbc_name item_meta.attr_info def.item_meta.name in
ctx_compute_fun_name def.item_meta.span ctx llbc_name def.num_loops
def.loop_id
@@ -2123,4 +2124,4 @@ let ctx_add_fun_decl (def : fun_decl) (ctx : extraction_ctx) : extraction_ctx =
let ctx_compute_type_decl_name (ctx : extraction_ctx) (def : type_decl) : string
=
- ctx_compute_type_name def.item_meta ctx def.llbc_name
+ ctx_compute_type_name def.item_meta ctx def.item_meta.name
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 129fdd78..78382179 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -739,7 +739,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
(* Lookup the builtin information, if there is *)
let open ExtractBuiltin in
let info =
- match_name_find_opt ctx.trans_ctx def.llbc_name (builtin_types_map ())
+ match_name_find_opt ctx.trans_ctx def.item_meta.name (builtin_types_map ())
in
(* Register the filtering information, if there is *)
let ctx =
@@ -783,11 +783,11 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) :
(fun fid (field : field) ->
( fid,
ctx_compute_field_name def field.attr_info ctx
- def.llbc_name fid field.field_name ))
+ def.item_meta.name fid field.field_name ))
fields
in
let cons_name =
- ctx_compute_struct_constructor def ctx def.llbc_name
+ ctx_compute_struct_constructor def ctx def.item_meta.name
in
(field_names, cons_name)
| Some { body_info = Some (Struct (cons_name, field_names)); _ } ->
@@ -1417,8 +1417,8 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Add the type and const generic params - note that we need those bindings only for the
* body translation (they are not top-level) *)
let ctx_body, type_params, cg_params, trait_clauses =
- ctx_add_generic_params def.item_meta.span def.llbc_name def.llbc_generics
- def.generics ctx
+ ctx_add_generic_params def.item_meta.span def.item_meta.name
+ def.llbc_generics def.generics ctx
in
(* Add a break before *)
if backend () <> HOL4 || not (decl_is_first_from_group kind) then
@@ -1426,11 +1426,11 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
(* Print a comment to link the extracted type to its original rust definition *)
(let name =
if !Config.extract_external_name_patterns && not def.item_meta.is_local
- then Some def.llbc_name
+ then Some def.item_meta.name
else None
in
extract_comment_with_raw_span ctx fmt
- [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
+ [ "[" ^ name_to_string ctx def.item_meta.name ^ "]" ]
name def.item_meta.span.span);
F.pp_print_break fmt 0 0;
(* Open a box for the definition, so that whenever possible it gets printed on
@@ -1703,7 +1703,7 @@ let extract_type_decl_record_field_projectors (ctx : extraction_ctx)
if is_rec then
(* Add the type params *)
let ctx, type_params, cg_params, trait_clauses =
- ctx_add_generic_params decl.item_meta.span decl.llbc_name
+ ctx_add_generic_params decl.item_meta.span decl.item_meta.name
decl.llbc_generics decl.generics ctx
in
(* Record_var will be the ADT argument to the projector *)
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index d273546a..2754eaac 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -397,8 +397,6 @@ type predicates = { trait_type_constraints : trait_type_constraint list }
type type_decl = {
def_id : TypeDeclId.id;
- llbc_name : llbc_name;
- (** The original name coming from the LLBC declaration *)
name : string;
(** We use the name only for printing purposes (for debugging):
the name used at extraction time will be derived from the
@@ -1106,7 +1104,6 @@ type fun_decl = {
*)
loop_id : LoopId.id option;
(** [Some] if this definition was generated for a loop *)
- llbc_name : llbc_name; (** The original LLBC name. *)
name : string;
(** We use the name only for printing purposes (for debugging):
the name used at extraction time will be derived from the
@@ -1122,7 +1119,6 @@ type global_decl = {
def_id : GlobalDeclId.id;
span : span;
item_meta : T.item_meta;
- llbc_name : llbc_name; (** The original LLBC name. *)
name : string;
(** We use the name only for printing purposes (for debugging):
the name used at extraction time will be derived from the
@@ -1140,7 +1136,6 @@ type global_decl = {
type trait_decl = {
def_id : trait_decl_id;
- llbc_name : llbc_name;
name : string;
item_meta : T.item_meta;
generics : generic_params;
@@ -1162,7 +1157,6 @@ type trait_decl = {
type trait_impl = {
def_id : trait_impl_id;
- llbc_name : llbc_name;
name : string;
item_meta : T.item_meta;
impl_trait : trait_decl_ref;
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index dda6a611..3476df5f 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -1504,7 +1504,6 @@ let decompose_loops (_ctx : trans_ctx) (def : fun_decl) :
backend_attributes = def.backend_attributes;
num_loops;
loop_id = Some loop.loop_id;
- llbc_name = def.llbc_name;
name = def.name;
signature = loop_sig;
is_global_decl_body = def.is_global_decl_body;
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index d38644c1..9673f542 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -690,7 +690,6 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
let {
def_id = _;
name = _;
- llbc_name = _;
item_meta = _;
generics = _;
llbc_generics = _;
@@ -711,7 +710,6 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
let {
def_id = _;
name = _;
- llbc_name = _;
item_meta = _;
impl_trait = _;
llbc_impl_trait = _;
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 13c94bdf..e829ed30 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -583,7 +583,6 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
^ "\n"));
let env = Print.Contexts.decls_ctx_to_fmt_env ctx in
let def_id = def.T.def_id in
- let llbc_name = def.item_meta.name in
let name = Print.Types.name_to_string env def.item_meta.name in
(* Can't translate types with regions for now *)
cassert __FILE__ __LINE__
@@ -596,7 +595,6 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
let item_meta = def.item_meta in
{
def_id;
- llbc_name;
name;
item_meta;
generics;
@@ -3772,8 +3770,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
(* Translate the declaration *)
let def_id = def.def_id in
- let llbc_name = def.item_meta.name in
- let name = name_to_string ctx llbc_name in
+ let name = name_to_string ctx def.item_meta.name in
(* Translate the signature *)
let signature = translate_fun_sig_from_decomposed ctx.sg in
(* Translate the body, if there is *)
@@ -3898,7 +3895,6 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
backend_attributes;
num_loops;
loop_id;
- llbc_name;
name;
signature;
is_global_decl_body = def.is_global_decl_body;
@@ -3943,12 +3939,11 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
} : A.trait_decl =
trait_decl
in
- let llbc_name = item_meta.name in
let type_infos = ctx.type_ctx.type_infos in
let name =
Print.Types.name_to_string
(Print.Contexts.decls_ctx_to_fmt_env ctx)
- llbc_name
+ item_meta.name
in
let generics, preds =
translate_generic_params trait_decl.item_meta.span llbc_generics
@@ -3978,7 +3973,6 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
in
{
def_id;
- llbc_name;
name;
item_meta;
generics;
@@ -4007,7 +4001,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
} =
trait_impl
in
- let llbc_name = item_meta.name in
let type_infos = ctx.type_ctx.type_infos in
let impl_trait =
translate_trait_decl_ref trait_impl.item_meta.span
@@ -4017,7 +4010,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
let name =
Print.Types.name_to_string
(Print.Contexts.decls_ctx_to_fmt_env ctx)
- llbc_name
+ item_meta.name
in
let generics, preds =
translate_generic_params trait_impl.item_meta.span llbc_generics
@@ -4043,7 +4036,6 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
in
{
def_id;
- llbc_name;
name;
item_meta;
impl_trait;
@@ -4070,11 +4062,10 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
} =
decl
in
- let llbc_name = item_meta.name in
let name =
Print.Types.name_to_string
(Print.Contexts.decls_ctx_to_fmt_env ctx)
- llbc_name
+ item_meta.name
in
let generics, preds =
translate_generic_params decl.item_meta.span llbc_generics
@@ -4084,7 +4075,6 @@ let translate_global (ctx : Contexts.decls_ctx) (decl : A.global_decl) :
span = item_meta.span;
def_id;
item_meta;
- llbc_name;
name;
llbc_generics;
generics;
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index cadf8cbd..672fb22f 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -442,7 +442,7 @@ let export_types_group (fmt : Format.formatter) (config : gen_config)
let types_map = builtin_types_map () in
List.map
(fun (def : Pure.type_decl) ->
- match_name_find_opt ctx.trans_ctx def.llbc_name types_map <> None)
+ match_name_find_opt ctx.trans_ctx def.item_meta.name types_map <> None)
defs
in
@@ -648,7 +648,8 @@ let export_functions_group (fmt : Format.formatter) (config : gen_config)
let funs_map = builtin_funs_map () in
List.map
(fun (trans : pure_fun_translation) ->
- match_name_find_opt ctx.trans_ctx trans.f.llbc_name funs_map <> None)
+ match_name_find_opt ctx.trans_ctx trans.f.item_meta.name funs_map
+ <> None)
pure_ls
in
@@ -727,7 +728,7 @@ let export_trait_decl (fmt : Format.formatter) (_config : gen_config)
(* Check if the trait declaration is builtin, in which case we ignore it *)
let open ExtractBuiltin in
if
- match_name_find_opt ctx.trans_ctx trait_decl.llbc_name
+ match_name_find_opt ctx.trans_ctx trait_decl.item_meta.name
(builtin_trait_decls_map ())
= None
then (
@@ -752,7 +753,7 @@ let export_trait_impl (fmt : Format.formatter) (_config : gen_config)
let trait_impl =
TraitImplId.Map.find trait_impl.def_id ctx.crate.trait_impls
in
- match_name_with_generics_find_opt ctx.trans_ctx trait_decl.llbc_name
+ match_name_with_generics_find_opt ctx.trans_ctx trait_decl.item_meta.name
trait_impl.impl_trait.decl_generics
(builtin_trait_impls_map ())
in
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-18 15:24:44 +0000