diff options
author | Guillaume Boisseau | 2024-06-28 10:58:44 +0200 |
---|---|---|
committer | GitHub | 2024-06-28 10:58:44 +0200 |
commit | 5590dc87a5426cbcb32a2387701d179e107a9792 (patch) | |
tree | 57f062f6243ae878b3fbc0df5abb9b7a938cb7f7 | |
parent | 2e9d264566d32a9ee2a12d005851434cd8390975 (diff) | |
parent | 617941a779baab199aa69bf2e8578a1ee7877289 (diff) |
Merge pull request #272 from Nadrieril/remove-llbc_name
Diffstat (limited to '')
-rw-r--r-- | compiler/Extract.ml | 61 | ||||
-rw-r--r-- | compiler/ExtractBase.ml | 17 | ||||
-rw-r--r-- | compiler/ExtractTypes.ml | 16 | ||||
-rw-r--r-- | compiler/Pure.ml | 6 | ||||
-rw-r--r-- | compiler/PureMicroPasses.ml | 1 | ||||
-rw-r--r-- | compiler/PureUtils.ml | 2 | ||||
-rw-r--r-- | compiler/SymbolicToPure.ml | 18 | ||||
-rw-r--r-- | compiler/Translate.ml | 9 | ||||
-rw-r--r-- | tests/src/mutually-recursive-traits.lean.out | 12 |
9 files changed, 65 insertions, 77 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 diff --git a/tests/src/mutually-recursive-traits.lean.out b/tests/src/mutually-recursive-traits.lean.out index bd281a82..a7e81535 100644 --- a/tests/src/mutually-recursive-traits.lean.out +++ b/tests/src/mutually-recursive-traits.lean.out @@ -1,17 +1,17 @@ [[92mInfo[39m ] Imported: tests/llbc/mutually_recursive_traits.llbc -[[91mError[39m] In file Translate.ml, line 826: +[[91mError[39m] In file Translate.ml, line 827: Mutually recursive trait declarations are not supported Uncaught exception: (Failure - "In file Translate.ml, line 826:\ - \nIn file Translate.ml, line 826:\ + "In file Translate.ml, line 827:\ + \nIn file Translate.ml, line 827:\ \nMutually recursive trait declarations are not supported") Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 47, characters 4-76 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 -Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 852, characters 2-52 -Called from Aeneas__Translate.extract_file in file "Translate.ml", line 979, characters 2-36 -Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1528, characters 5-42 +Called from Aeneas__Translate.extract_definitions in file "Translate.ml", line 853, characters 2-52 +Called from Aeneas__Translate.extract_file in file "Translate.ml", line 980, characters 2-36 +Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 1529, characters 5-42 Called from Dune__exe__Main in file "Main.ml", line 317, characters 14-66 |