summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-06 18:47:38 +0100
committerSon Ho2023-11-06 18:47:38 +0100
commit16c094457d0b23f5a9e1ea60e3195cc452ed7c43 (patch)
treec70441669ad628d6c2c8aee18fc02d8fa813a5b4
parent4ba7d73fa3bfbf9ef41b2d9d5595f28fb67b8e47 (diff)
Fix some issues when extracting references to Self
Diffstat (limited to '')
-rw-r--r--compiler/ExtractTypes.ml87
1 files changed, 57 insertions, 30 deletions
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 56290ab4..f4be9006 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1242,29 +1242,24 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
| TraitType (trait_ref, generics, type_name) -> (
if !parameterize_trait_types then raise (Failure "Unimplemented")
else
- (* There may be a special treatment depending on the instance id *)
+ let type_name =
+ ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id type_name
+ ctx
+ in
+ (* There may be a special treatment depending on the instance id.
+ See the comments for {!extract_trait_instance_id_with_dot}.
+ TODO: there should be a cleaner way to do. The annoying thing
+ here is that if we project directly over the self clause, then
+ we have to be careful (we may not have to print the "Self.").
+ Otherwise, we can directly call {!extract_trait_ref}.
+ *)
match trait_ref.trait_id with
| Self ->
- (* There are two situations:
- - we are extracting a declared item (typically a function signature)
- for a trait declaration. We directly refer to the item (we extract
- trait declarations as structures, so we can refer to their fields)
- - we are extracting a provided method for a trait declaration. We
- refer to the item in the self trait clause (see {!SelfTraitClauseId}).
-
- Remark: we can't get there for trait *implementations* because then the
- types should have been normalized.
- *)
- let trait_decl_id = Option.get ctx.trait_decl_id in
- let item_name = ctx_get_trait_type trait_decl_id type_name ctx in
assert (generics = empty_generic_args);
- if ctx.is_provided_method then
- (* Provided method: use the trait self clause *)
- let self_clause = ctx_get_trait_self_clause ctx in
- F.pp_print_string fmt (self_clause ^ "." ^ item_name)
- else
- (* Declaration: directly refer to the item *)
- F.pp_print_string fmt item_name
+ assert (trait_ref.generics = empty_generic_args);
+ extract_trait_instance_id_with_dot ctx fmt no_params_tys false
+ trait_ref.trait_id;
+ F.pp_print_string fmt type_name
| _ ->
(* HOL4 doesn't have 1st class types *)
assert (!backend <> HOL4);
@@ -1272,12 +1267,8 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter)
if use_brackets then F.pp_print_string fmt "(";
extract_trait_ref ctx fmt no_params_tys false trait_ref;
extract_generic_args ctx fmt no_params_tys generics;
- let name =
- ctx_get_trait_type trait_ref.trait_decl_ref.trait_decl_id
- type_name ctx
- in
if use_brackets then F.pp_print_string fmt ")";
- F.pp_print_string fmt ("." ^ name))
+ F.pp_print_string fmt ("." ^ type_name))
and extract_trait_ref (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (tr : trait_ref) : unit =
@@ -1338,12 +1329,48 @@ and extract_generic_args (ctx : extraction_ctx) (fmt : F.formatter)
(extract_trait_ref ctx fmt no_params_tys true)
trait_refs)
+(** We sometimes need to ignore references to `Self` when generating the
+ code, espcially when we project associated items. For this reason we
+ have a special function for the cases where we project from an instance
+ id (e.g., `<Self as Foo>::foo` - note that in the extracted code, the
+ projections are often written with a dot '.').
+ *)
+and extract_trait_instance_id_with_dot (ctx : extraction_ctx)
+ (fmt : F.formatter) (no_params_tys : TypeDeclId.Set.t) (inside : bool)
+ (id : trait_instance_id) : unit =
+ match id with
+ | Self ->
+ (* There are two situations:
+ - we are extracting a declared item and need to refer to another
+ item (for instance, we are extracting a method signature and
+ need to refer to an associated type).
+ We directly refer to the other item (we extract trait declarations
+ as structures, so we can refer to their fields)
+ - we are extracting a provided method for a trait declaration. We
+ refer to the item in the self trait clause (see {!SelfTraitClauseId}).
+
+ Remark: we can't get there for trait *implementations* because then the
+ types should have been normalized.
+ *)
+ if ctx.is_provided_method then
+ (* Provided method: use the trait self clause *)
+ let self_clause = ctx_get_trait_self_clause ctx in
+ F.pp_print_string fmt (self_clause ^ ".")
+ else
+ (* Declaration: nothing to print, we will directly refer to
+ the item. *)
+ ()
+ | _ ->
+ (* Other cases *)
+ extract_trait_instance_id ctx fmt no_params_tys inside id;
+ F.pp_print_string fmt "."
+
and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
(no_params_tys : TypeDeclId.Set.t) (inside : bool) (id : trait_instance_id)
: unit =
match id with
| Self ->
- (* This has specific treatment depending on the item we're extracting
+ (* This has a specific treatment depending on the item we're extracting
(associated type, etc.). We should have caught this elsewhere. *)
if !Config.extract_fail_hard then
raise (Failure "Unexpected occurrence of `Self`")
@@ -1357,13 +1384,13 @@ and extract_trait_instance_id (ctx : extraction_ctx) (fmt : F.formatter)
| ParentClause (inst_id, decl_id, clause_id) ->
(* Use the trait decl id to lookup the name *)
let name = ctx_get_trait_parent_clause decl_id clause_id ctx in
- extract_trait_instance_id ctx fmt no_params_tys true inst_id;
- F.pp_print_string fmt ("." ^ name)
+ extract_trait_instance_id_with_dot ctx fmt no_params_tys true inst_id;
+ F.pp_print_string fmt name
| ItemClause (inst_id, decl_id, item_name, clause_id) ->
(* Use the trait decl id to lookup the name *)
let name = ctx_get_trait_item_clause decl_id item_name clause_id ctx in
- extract_trait_instance_id ctx fmt no_params_tys true inst_id;
- F.pp_print_string fmt ("." ^ name)
+ extract_trait_instance_id_with_dot ctx fmt no_params_tys true inst_id;
+ F.pp_print_string fmt name
| TraitRef trait_ref ->
extract_trait_ref ctx fmt no_params_tys inside trait_ref
| UnknownTrait _ ->