summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-22 11:47:48 +0100
committerSon Ho2023-11-22 11:47:48 +0100
commit5c3a7986a818446cbf008a87f57b2eb51e0bf861 (patch)
tree75335911ce6afcb7aa78e0a8da3e0697f41347c3
parent4caed6d6e7c4eb85762da373a2e8ab599cb1b440 (diff)
Cleanup a bit
-rw-r--r--compiler/ExtractName.ml87
1 files changed, 0 insertions, 87 deletions
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index 94222ae1..41c81207 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -103,90 +103,3 @@ let name_with_generics_to_simple_name (ctx : ctx) (is_trait_impl : bool)
name
in
pattern_to_extract_name is_trait_impl name
-
-(*
- (* Prepare a name.
- The first id elem is always the crate: if it is the local crate,
- we remove it. We ignore disambiguators (there may be collisions, but we
- check if there are).
- *)
- let rec name_to_simple_name (name : llbc_name) : string list =
- (* Rmk.: initially we only filtered the disambiguators equal to 0 *)
- match name with
- | (PeIdent (crate, _) as id) :: name ->
- let name = if crate = crate_name then name else id :: name in
- let open Types in
- let name =
- List.map
- (function
- | PeIdent (s, _) -> s
- | PeImpl impl -> impl_elem_to_simple_name impl)
- name
- in
- name
- | _ ->
- raise
- (Failure
- ("Unexpected name shape: " ^ TranslateCore.name_to_string ctx name))
- and impl_elem_to_simple_name (impl : Types.impl_elem) : string =
- (* We do something simple for now.
- TODO: we might want to do something different for impl elements which are
- actually trait implementations, in order to prevent name collisions (it
- is possible to define several times the same trait for the same type,
- but with different instantiations of the type, or different trait
- requirements *)
- ty_to_simple_name impl.generics impl.ty
- and ty_to_simple_name (generics : Types.generic_params) (ty : Types.ty) :
- string =
- (* We do something simple for now.
- TODO: find a more principled way of converting types to names.
- In particular, we might want to do something different for impl elements which are
- actually trait implementations, in order to prevent name collisions (it
- is possible to define several times the same trait for the same type,
- but with different instantiations of the type, or different trait
- requirements *)
- match ty with
- | TAdt (id, args) -> (
- match id with
- | TAdtId id ->
- let def = TypeDeclId.Map.find id ctx.type_ctx.type_decls in
- name_last_elem_as_ident def.name
- | TTuple ->
- (* TODO *)
- "Tuple"
- ^ String.concat ""
- (List.map (ty_to_simple_name generics) args.types)
- | TAssumed id -> (
- match id with
- | Types.TBox -> "Box"
- | Types.TArray -> "Array"
- | Types.TSlice -> "Slice"
- | Types.TStr -> "Str"))
- | TVar vid ->
- (* Use the variable name *)
- (List.find (fun (v : type_var) -> v.index = vid) generics.types).name
- | TLiteral lty ->
- StringUtils.capitalize_first_letter
- (Print.Types.literal_type_to_string lty)
- | TNever -> raise (Failure "Unreachable")
- | TRef (_, rty, rk) -> (
- let rty = ty_to_simple_name generics rty in
- match rk with
- | RMut -> "MutBorrow" ^ rty
- | RShared -> "SharedBorrow" ^ rty)
- | TRawPtr (rty, rk) -> (
- let rty = ty_to_simple_name generics rty in
- match rk with RMut -> "MutPtr" ^ rty | RShared -> "ConstPtr" ^ rty)
- | TTraitType (tr, _, name) ->
- (* TODO: this is way too simple *)
- let trait_decl =
- TraitDeclId.Map.find tr.trait_decl_ref.trait_decl_id
- ctx.trait_decls_ctx.trait_decls
- in
- name_last_elem_as_ident trait_decl.name ^ name
- | TArrow (inputs, output) ->
- "Arrow"
- ^ String.concat ""
- (List.map (ty_to_simple_name generics) (inputs @ [ output ]))
- in
-*)