Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix generics handling for function calls #1215

Merged
merged 7 commits into from
Jan 6, 2025
Merged

Fix generics handling for function calls #1215

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
d976f64
Clarify method call generics
Nadrieril Dec 30, 2024
64e1730
Provide late bound generics to function calls
Nadrieril Dec 30, 2024
6a71603
Improve `ClosureArgs` for use in `AggregateKind`
Nadrieril Dec 12, 2024
4e62c29
Split off `TyKind::Closure` from `TyKind::Arrow`
Nadrieril Dec 12, 2024
eafd535
Properly account for predicates on ADT constructors
Nadrieril Dec 30, 2024
79e2da0
Discard more-precise implemented method signatures
Nadrieril Dec 31, 2024
63422f3
Use `supposely_unreachable!` to get better errors
Nadrieril Jan 6, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions engine/lib/import_thir.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1004,8 +1004,8 @@ end) : EXPR = struct
| Float k ->
TFloat
(match k with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128)
| Arrow value ->
let ({ inputs; output; _ } : Thir.ty_fn_sig) = value.value in
| Arrow signature | Closure (_, { untupled_sig = signature; _ }) ->
let ({ inputs; output; _ } : Thir.ty_fn_sig) = signature.value in
let inputs =
if List.is_empty inputs then [ U.unit_typ ]
else List.map ~f:(c_ty span) inputs
Expand Down
6 changes: 4 additions & 2 deletions frontend/exporter/src/types/mir.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -433,8 +433,10 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO

let ty = func.ty(&s.mir().local_decls, tcx);
let hax_ty: crate::Ty = ty.sinto(s);
let TyKind::Arrow(sig) = hax_ty.kind() else {
unreachable!("Attempting to call non-function type: {ty:?}")
let sig = match hax_ty.kind() {
TyKind::Arrow(sig) => sig,
TyKind::Closure(_, args) => &args.untupled_sig,
_ => unreachable!("Attempting to call non-function type: {ty:?}"),
Nadrieril marked this conversation as resolved.
Show resolved Hide resolved
};
let fun_op = if let ty::TyKind::FnDef(def_id, generics) = ty.kind() {
// The type of the value is one of the singleton types that corresponds to each function,
Expand Down
18 changes: 12 additions & 6 deletions frontend/exporter/src/types/ty.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -802,15 +802,21 @@ pub enum TyKind {
let sig = tcx.fn_sig(*def).instantiate(tcx, generics);
TyKind::Arrow(Box::new(sig.sinto(s)))
},
ty::TyKind::Closure (_def_id, generics) => {
let sig = generics.as_closure().sig();
let sig = s.base().tcx.signature_unclosure(sig, rustc_hir::Safety::Safe);
TyKind::Arrow(Box::new(sig.sinto(s)))
},
)]
/// Reflects [`ty::TyKind::FnPtr`], [`ty::TyKind::FnDef`] and [`ty::TyKind::Closure`]
/// Reflects [`ty::TyKind::FnPtr`] and [`ty::TyKind::FnDef`]
Arrow(Box<PolyFnSig>),

#[custom_arm(
ty::TyKind::Closure (def_id, generics) => {
let closure = generics.as_closure();
TyKind::Closure(
def_id.sinto(s),
ClosureArgs::sfrom(s, *def_id, closure),
)
},
)]
Closure(DefId, ClosureArgs),

#[custom_arm(
ty::TyKind::Adt(adt_def, generics) => {
let def_id = adt_def.did().sinto(s);
Expand Down
2 changes: 1 addition & 1 deletion test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -110,7 +110,7 @@ val t_OpaqueEnum (v_X: usize) (v_T v_U: Type0) : eqtype
val t_OpaqueStruct (v_X: usize) (v_T v_U: Type0) : eqtype

class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_6168282666194871449:Core.Clone.t_Clone v_U;
[@@@ FStar.Tactics.Typeclasses.no_method]_super_13225137425257751668:Core.Clone.t_Clone v_U;
f_f_pre:v_U -> Type0;
f_f_post:v_U -> v_Self -> Type0;
f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)
Expand Down
22 changes: 11 additions & 11 deletions test-harness/src/snapshots/toolchain__traits into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,11 +35,11 @@ open FStar.Mul
class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }

class t_ParBlocksSizeUser (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_10960599340086055385:t_BlockSizeUser v_Self
[@@@ FStar.Tactics.Typeclasses.no_method]_super_17750095326162477464:t_BlockSizeUser v_Self
}

class t_BlockBackend (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_15949286759387124191:t_ParBlocksSizeUser v_Self;
[@@@ FStar.Tactics.Typeclasses.no_method]_super_7661532914804666209:t_ParBlocksSizeUser v_Self;
f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global
Expand All @@ -55,7 +55,7 @@ open FStar.Mul
class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }

class t_Foo (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_5461126672499050919:t_Bar v_Self f_U;
[@@@ FStar.Tactics.Typeclasses.no_method]_super_16210070100893052778:t_Bar v_Self f_U;
f_U:Type0
}
'''
Expand Down Expand Up @@ -387,11 +387,11 @@ let method_caller
()

class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_11748868061750783190:t_Trait v_Self
[@@@ FStar.Tactics.Typeclasses.no_method]_super_1779568480311729828:t_Trait v_Self
v_TypeArg
v_ConstArg;
f_AssocType:Type0;
f_AssocType_5566993444404141271:t_Trait f_AssocType v_TypeArg v_ConstArg
f_AssocType_7414800425644916102:t_Trait f_AssocType v_TypeArg v_ConstArg
}
'''
"Traits.Interlaced_consts_types.fst" = '''
Expand Down Expand Up @@ -468,11 +468,11 @@ open FStar.Mul

class t_Trait1 (v_Self: Type0) = {
f_T:Type0;
f_T_7805326132379548775:t_Trait1 f_T
f_T_2328060197809802853:t_Trait1 f_T
}

class t_Trait2 (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_4567617955834163411:t_Trait1 v_Self;
[@@@ FStar.Tactics.Typeclasses.no_method]_super_4351024728553910126:t_Trait1 v_Self;
f_U:Type0
}
'''
Expand Down Expand Up @@ -549,7 +549,7 @@ let t_Error_cast_to_repr (x: t_Error) : isize = match x <: t_Error with | Error_
type t_Struct = | Struct : t_Struct

class t_SuperTrait (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self;
[@@@ FStar.Tactics.Typeclasses.no_method]_super_9529721400157967266:Core.Clone.t_Clone v_Self;
f_function_of_super_trait_pre:v_Self -> Type0;
f_function_of_super_trait_post:v_Self -> u32 -> Type0;
f_function_of_super_trait:x0: v_Self
Expand All @@ -561,7 +561,7 @@ class t_SuperTrait (v_Self: Type0) = {
[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_SuperTrait_for_i32: t_SuperTrait i32 =
{
_super_9442900250278684536 = FStar.Tactics.Typeclasses.solve;
_super_9529721400157967266 = FStar.Tactics.Typeclasses.solve;
f_function_of_super_trait_pre = (fun (self: i32) -> true);
f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true);
f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
Expand Down Expand Up @@ -613,7 +613,7 @@ let use_impl_trait (_: Prims.unit) : Prims.unit =

class t_Foo (v_Self: Type0) = {
f_AssocType:Type0;
f_AssocType_15012754260415912210:t_SuperTrait f_AssocType;
f_AssocType_12248650268031145847:t_SuperTrait f_AssocType;
f_N:usize;
f_assoc_f_pre:Prims.unit -> Type0;
f_assoc_f_post:Prims.unit -> Prims.unit -> Type0;
Expand Down Expand Up @@ -650,7 +650,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x
let impl_Foo_for_tuple_: t_Foo Prims.unit =
{
f_AssocType = i32;
f_AssocType_15012754260415912210 = FStar.Tactics.Typeclasses.solve;
f_AssocType_12248650268031145847 = FStar.Tactics.Typeclasses.solve;
f_N = sz 32;
f_assoc_f_pre = (fun (_: Prims.unit) -> true);
f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);
Expand Down