diff options
Diffstat (limited to 'compiler/ExtractBase.ml')
| -rw-r--r-- | compiler/ExtractBase.ml | 43 |
1 files changed, 24 insertions, 19 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index fb65bd5e..57131dad 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -253,8 +253,9 @@ let empty_names_map : names_map = } (** Small helper to update an LLBC name if the rename attribute has been set *) -let rename_llbc_name (item_meta : Meta.item_meta) (llbc_name : llbc_name) = - match item_meta.rename with +let rename_llbc_name (attr_info : Meta.attr_info) (llbc_name : llbc_name) : + llbc_name = + match attr_info.rename with | Some rename -> let name_prefix = List.tl (List.rev llbc_name) in List.rev (T.PeIdent (rename, Disambiguator.zero) :: name_prefix) @@ -1393,8 +1394,8 @@ let ctx_compute_simple_type_name = ctx_compute_simple_name (** Helper *) let ctx_compute_type_name_no_suffix (ctx : extraction_ctx) - (item_meta : Meta.item_meta) (name : llbc_name) : string = - let name = rename_llbc_name item_meta name in + (item_meta : Types.item_meta) (name : llbc_name) : string = + let name = rename_llbc_name item_meta.attr_info name in flatten_name (ctx_compute_simple_type_name item_meta.span ctx name) (** Provided a basename, compute a type name. @@ -1403,7 +1404,7 @@ let ctx_compute_type_name_no_suffix (ctx : extraction_ctx) for instance field and variant names when we need to add the name of the type as a prefix. *) -let ctx_compute_type_name (item_meta : Meta.item_meta) (ctx : extraction_ctx) +let ctx_compute_type_name (item_meta : Types.item_meta) (ctx : extraction_ctx) (name : llbc_name) = let name = ctx_compute_type_name_no_suffix ctx item_meta name in match backend () with @@ -1424,7 +1425,7 @@ let ctx_compute_type_name (item_meta : Meta.item_meta) (ctx : extraction_ctx) to tuples, meaning generating names by using indices shouldn't be too much of a problem. *) -let ctx_compute_field_name (def : type_decl) (field_meta : Meta.item_meta) +let ctx_compute_field_name (def : type_decl) (field_meta : Meta.attr_info) (ctx : extraction_ctx) (def_name : llbc_name) (field_id : FieldId.id) (field_name : string option) : string = (* If the user did not provide a name, use the field index. *) @@ -1435,7 +1436,7 @@ let ctx_compute_field_name (def : type_decl) (field_meta : Meta.item_meta) let field_name_s = Option.value field_meta.rename ~default:field_name_s in (* Prefix the name with the name of the type, if necessary (some backends don't support field name collisions) *) - let def_name = rename_llbc_name def.item_meta def_name in + let def_name = rename_llbc_name def.item_meta.attr_info def_name in let name = if !Config.record_fields_short_names then if field_name = None then (* TODO: this is a bit ugly *) @@ -1457,7 +1458,7 @@ let ctx_compute_variant_name (ctx : extraction_ctx) (def : type_decl) (variant : variant) : string = (* Replace the name of the variant if the user annotated it with the [rename] attribute. *) let variant = - Option.value variant.item_meta.rename ~default:variant.variant_name + Option.value variant.attr_info.rename ~default:variant.variant_name in match backend () with | FStar | Coq | HOL4 -> @@ -1547,7 +1548,9 @@ 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 trait_decl.llbc_name in + let llbc_name = + rename_llbc_name trait_decl.item_meta.attr_info trait_decl.llbc_name + in ctx_compute_type_name trait_decl.item_meta ctx llbc_name let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) @@ -1561,7 +1564,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) Note that if the user provided a [rename] attribute, we simply use that. *) let name = - match trait_impl.item_meta.rename with + match trait_impl.item_meta.attr_info.rename with | None -> let name = let params = trait_impl.llbc_generics in @@ -1569,7 +1572,7 @@ let ctx_compute_trait_impl_name (ctx : extraction_ctx) (trait_decl : trait_decl) let name = ctx_prepare_name trait_impl.item_meta.span ctx trait_decl.llbc_name in - let name = rename_llbc_name trait_impl.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 in flatten_name name @@ -1631,7 +1634,7 @@ let ctx_compute_trait_clause_name (ctx : extraction_ctx) let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in let args = clause.clause_generics in trait_name_with_generics_to_simple_name ctx.trans_ctx ~prefix - impl_trait_decl.name params args + impl_trait_decl.item_meta.name params args in String.concat "" clause @@ -1814,7 +1817,7 @@ let ctx_compute_var_basename (span : Meta.span) (ctx : extraction_ctx) *) (* The name shouldn't be empty, and its last element should * be an ident *) - let cl = Collections.List.last def.name in + let cl = Collections.List.last def.item_meta.name in name_from_type_ident (TypesUtils.as_ident cl)) | TVar _ -> ( (* TODO: use "t" also for F* *) @@ -2006,7 +2009,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 def.llbc_name in + let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in let name = ctx_compute_decreases_proof_name def.item_meta.span ctx def.def_id name def.num_loops def.loop_id @@ -2017,7 +2020,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 def.llbc_name in + let name = rename_llbc_name def.item_meta.attr_info def.llbc_name in let name = ctx_compute_termination_measure_name def.item_meta.span ctx def.def_id name def.num_loops def.loop_id @@ -2034,13 +2037,15 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : (* Check if the global corresponds to an assumed global that we should map to a custom definition in our standard library (for instance, happens with "core::num::usize::MAX") *) - match match_name_find_opt ctx.trans_ctx def.name builtin_globals_map with + match + match_name_find_opt ctx.trans_ctx def.item_meta.name builtin_globals_map + with | Some name -> (* Yes: register the custom binding *) ctx_add def.item_meta.span decl name ctx | None -> (* Not the case: "standard" registration *) - let name = rename_llbc_name def.item_meta def.name in + let name = rename_llbc_name def.item_meta.attr_info def.item_meta.name in let name = ctx_compute_global_name def.item_meta.span ctx name in let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in @@ -2068,7 +2073,7 @@ let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = let item_meta = match def.kind with | TraitItemImpl (_, trait_decl_id, item_name, _) -> ( - if Option.is_some def.item_meta.rename then def.item_meta + if Option.is_some def.item_meta.attr_info.rename then def.item_meta else (* Lookup the declaration. TODO: the trait item impl info should directly give us the id of the method declaration. *) @@ -2099,7 +2104,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 def.llbc_name in + let llbc_name = rename_llbc_name item_meta.attr_info def.llbc_name in ctx_compute_fun_name def.item_meta.span ctx llbc_name def.num_loops def.loop_id |