diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/AssociatedTypes.ml | 39 | ||||
| -rw-r--r-- | compiler/SymbolicToPure.ml | 21 |
2 files changed, 44 insertions, 16 deletions
diff --git a/compiler/AssociatedTypes.ml b/compiler/AssociatedTypes.ml index 022aad2f..94e08996 100644 --- a/compiler/AssociatedTypes.ml +++ b/compiler/AssociatedTypes.ml @@ -171,6 +171,8 @@ type 'r norm_ctx = { convert_ety : T.ety -> 'r T.ty; convert_etrait_ref : T.etrait_ref -> 'r T.trait_ref; ty_to_string : 'r T.ty -> string; + generic_params_to_string : T.generic_params -> string; + generic_args_to_string : 'r T.generic_args -> string; trait_ref_to_string : 'r T.trait_ref -> string; trait_instance_id_to_string : 'r T.trait_instance_id -> string; pp_r : Format.formatter -> 'r -> unit; @@ -188,6 +190,9 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty = | Ref (r, ty, rkind) -> let ty = ctx_normalize_ty ctx ty in T.Ref (r, ty, rkind) + | RawPtr (ty, rkind) -> + let ty = ctx_normalize_ty ctx ty in + RawPtr (ty, rkind) | Arrow (inputs, output) -> let inputs = List.map (ctx_normalize_ty ctx) inputs in let output = ctx_normalize_ty ctx output in @@ -195,14 +200,18 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty = | TraitType (trait_ref, generics, type_name) -> ( log#ldebug (lazy - ("ctx_normalize_ty: trait type: " ^ ctx.ty_to_string ty + ("ctx_normalize_ty:\n- trait type: " ^ ctx.ty_to_string ty ^ "\n- trait_ref: " ^ ctx.trait_ref_to_string trait_ref ^ "\n- raw trait ref:\n" - ^ T.show_trait_ref ctx.pp_r trait_ref)); + ^ T.show_trait_ref ctx.pp_r trait_ref + ^ "\n- generics:\n" + ^ ctx.generic_args_to_string generics)); (* Normalize and attempt to project the type from the trait ref *) let trait_ref = ctx_normalize_trait_ref ctx trait_ref in let generics = ctx_normalize_generic_args ctx generics in + (* For now, we don't support higher order types *) + assert (generics = TypesUtils.mk_empty_generic_args); let ty : 'r T.ty = match trait_ref.trait_id with | T.TraitRef @@ -216,13 +225,13 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty = let trait_impl = C.ctx_lookup_trait_impl ctx.ctx impl_id in (* Lookup the type *) let ty = snd (List.assoc type_name trait_impl.types) in - (* Annoying: convert etype to an stype - TODO: hwo to avoid that? *) + (* Annoying: convert etype to an stype - TODO: how to avoid that? *) let ty : T.sty = TypesUtils.ety_no_regions_to_gr_ty ty in (* Substitute *) let tr_self = T.UnknownTrait __FUNCTION__ in let subst = Subst.make_subst_from_generics_no_regions trait_impl.generics - generics tr_self + trait_ref.generics tr_self in let ty = Subst.ty_substitute subst ty in (* Reconvert *) @@ -230,7 +239,14 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty = (* Normalize *) ctx_normalize_ty ctx ty | T.TraitImpl impl_id -> - (* This happens. This doesn't come from the substituations + log#ldebug + (lazy + ("ctx_normalize_ty (trait impl):\n- trait type: " + ^ ctx.ty_to_string ty ^ "\n- trait_ref: " + ^ ctx.trait_ref_to_string trait_ref + ^ "\n- raw trait ref:\n" + ^ T.show_trait_ref ctx.pp_r trait_ref)); + (* This happens. This doesn't come from the substitutions performed by Aeneas (the [TraitImpl] would be wrapped in a [TraitRef] but from non-normalized traits translated from the Rustc AST. @@ -240,13 +256,13 @@ let rec ctx_normalize_ty : 'r. 'r norm_ctx -> 'r T.ty -> 'r T.ty = let trait_impl = C.ctx_lookup_trait_impl ctx.ctx impl_id in (* Lookup the type *) let ty = snd (List.assoc type_name trait_impl.types) in - (* Annoying: convert etype to an stype - TODO: hwo to avoid that? *) + (* Annoying: convert etype to an stype - TODO: how to avoid that? *) let ty : T.sty = TypesUtils.ety_no_regions_to_gr_ty ty in (* Substitute *) let tr_self = T.UnknownTrait __FUNCTION__ in let subst = Subst.make_subst_from_generics_no_regions trait_impl.generics - generics tr_self + trait_ref.generics tr_self in let ty = Subst.ty_substitute subst ty in (* Reconvert *) @@ -465,6 +481,9 @@ let ctx_normalize_trait_type_constraint (ctx : 'r norm_ctx) let ty = ctx_normalize_ty ctx ty in { T.trait_ref; generics; type_name; ty } +let generic_params_to_string ctx x = + "<" ^ String.concat ", " (fst (PA.generic_params_to_strings ctx x)) ^ ">" + let mk_snorm_ctx (ctx : C.eval_ctx) : T.RegionVarId.id T.region norm_ctx = let get_ty_repr x = C.STraitTypeRefMap.find_opt x ctx.norm_trait_stypes in { @@ -473,6 +492,8 @@ let mk_snorm_ctx (ctx : C.eval_ctx) : T.RegionVarId.id T.region norm_ctx = convert_ety = TypesUtils.ety_no_regions_to_sty; convert_etrait_ref = TypesUtils.etrait_ref_no_regions_to_gr_trait_ref; ty_to_string = PA.sty_to_string ctx; + generic_params_to_string = generic_params_to_string ctx; + generic_args_to_string = PA.sgeneric_args_to_string ctx; trait_ref_to_string = PA.strait_ref_to_string ctx; trait_instance_id_to_string = PA.strait_instance_id_to_string ctx; pp_r = T.pp_region T.pp_region_var_id; @@ -486,6 +507,8 @@ let mk_rnorm_ctx (ctx : C.eval_ctx) : T.RegionId.id T.region norm_ctx = convert_ety = TypesUtils.ety_no_regions_to_rty; convert_etrait_ref = TypesUtils.etrait_ref_no_regions_to_gr_trait_ref; ty_to_string = PA.rty_to_string ctx; + generic_params_to_string = generic_params_to_string ctx; + generic_args_to_string = PA.rgeneric_args_to_string ctx; trait_ref_to_string = PA.rtrait_ref_to_string ctx; trait_instance_id_to_string = PA.rtrait_instance_id_to_string ctx; pp_r = T.pp_region T.pp_region_id; @@ -499,6 +522,8 @@ let mk_enorm_ctx (ctx : C.eval_ctx) : T.erased_region norm_ctx = convert_ety = (fun x -> x); convert_etrait_ref = (fun x -> x); ty_to_string = PA.ety_to_string ctx; + generic_params_to_string = generic_params_to_string ctx; + generic_args_to_string = PA.egeneric_args_to_string ctx; trait_ref_to_string = PA.etrait_ref_to_string ctx; trait_instance_id_to_string = PA.etrait_instance_id_to_string ctx; pp_r = T.pp_erased_region; diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 4ba5296f..885d2ba5 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -534,12 +534,6 @@ let rec translate_fwd_ty (type_infos : TA.type_infos) (ty : 'r T.ty) : ty = (* Eliminate boxes and simplify tuples *) match type_id with | AdtId _ | T.Assumed (T.Array | T.Slice | T.Str) -> - (* No general parametricity for now *) - assert ( - not - (List.exists - (TypesUtils.ty_has_borrows type_infos) - generics.types)); let type_id = translate_type_id type_id in Adt (type_id, t_generics) | Tuple -> @@ -614,15 +608,24 @@ let rec translate_back_ty (type_infos : TA.type_infos) | T.Adt (type_id, generics) -> ( match type_id with | T.AdtId _ | Assumed (T.Array | T.Slice | T.Str) -> - (* Don't accept ADTs (which are not tuples) with borrows for now *) - assert (not (TypesUtils.ty_has_borrows type_infos ty)); let type_id = translate_type_id type_id in if inside_mut then (* We do not want to filter anything, so we translate the generics as "forward" types *) let generics = translate_fwd_generic_args type_infos generics in Some (Adt (type_id, generics)) - else None + else + (* If not inside a mutable reference: check if at least one + of the generics contains a mutable reference (i.e., is not + translated to `None`. If yes, keep the whole type, and + translate all the generics as "forward" types (the backward + function will extract the proper information from the ADT value) + *) + let types = List.filter_map translate generics.types in + if types <> [] then + let generics = translate_fwd_generic_args type_infos generics in + Some (Adt (type_id, generics)) + else None | Assumed T.Box -> ( (* Don't accept ADTs (which are not tuples) with borrows for now *) assert (not (TypesUtils.ty_has_borrows type_infos ty)); |