Skip to content

Commit b3e7fcd

Browse files
W95PspW95Psp
authored
Merge pull request #1487 from N1ark/fun-ty
Add `Ty::FnDef`
2 parents 254fd5a + 1ee3921 commit b3e7fcd

File tree

5 files changed

+39
-19
lines changed

5 files changed

+39
-19
lines changed

‎engine/lib/import_thir.ml‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1023,7 +1023,9 @@ end) : EXPR = struct
10231023
| Float k ->
10241024
TFloat
10251025
(match k with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128)
1026-
| Arrow signature | Closure (_, { untupled_sig = signature; _ }) ->
1026+
| Arrow signature
1027+
| Closure (_, { untupled_sig = signature; _ })
1028+
| FnDef { fn_sig = signature; _ } ->
10271029
let ({ inputs; output; _ } : Thir.ty_fn_sig) = signature.value in
10281030
let inputs =
10291031
if List.is_empty inputs then [ U.unit_typ ]

‎frontend/exporter/src/types/mir.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -424,6 +424,7 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO
424424
let hax_ty: crate::Ty = ty.sinto(s);
425425
let sig = match hax_ty.kind() {
426426
TyKind::Arrow(sig) => sig,
427+
TyKind::FnDef { fn_sig, .. } => fn_sig,
427428
TyKind::Closure(_, args) => &args.untupled_sig,
428429
_ => supposely_unreachable_fatal!(
429430
s,

‎frontend/exporter/src/types/ty.rs‎

Lines changed: 23 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -796,6 +796,28 @@ pub enum TyKind {
796796
Uint(UintTy),
797797
Float(FloatTy),
798798

799+
#[custom_arm(
800+
ty::TyKind::FnDef(fun_id, generics) => {
801+
let tcx = s.base().tcx;
802+
let def_id = fun_id.sinto(s);
803+
let generic_args: Vec<GenericArg> = generics.sinto(s);
804+
let trait_refs = solve_item_required_traits(s, *fun_id, generics);
805+
let fn_sig = tcx.fn_sig(*fun_id).instantiate(tcx, generics);
806+
let fn_sig = Box::new(fn_sig.sinto(s));
807+
TyKind::FnDef { def_id, generic_args, trait_refs, fn_sig }
808+
},
809+
)]
810+
/// Reflects [`ty::TyKind::FnDef`]
811+
FnDef {
812+
/// Reflects [`ty::TyKind::FnDef`]'s substitutions
813+
generic_args: Vec<GenericArg>,
814+
/// Predicates required by the function, e.g. `T: Sized` for `Option<T>` or `B: 'a + ToOwned`
815+
/// for `Cow<'a, B>`.
816+
trait_refs: Vec<ImplExpr>,
817+
def_id: DefId,
818+
fn_sig: Box<PolyFnSig>,
819+
},
820+
799821
#[custom_arm(
800822
ty::TyKind::FnPtr(tys, header) => {
801823
let sig = tys.map_bound(|tys| ty::FnSig {
@@ -806,13 +828,8 @@ pub enum TyKind {
806828
});
807829
TyKind::Arrow(Box::new(sig.sinto(s)))
808830
},
809-
ty::TyKind::FnDef(def, generics) => {
810-
let tcx = s.base().tcx;
811-
let sig = tcx.fn_sig(*def).instantiate(tcx, generics);
812-
TyKind::Arrow(Box::new(sig.sinto(s)))
813-
},
814831
)]
815-
/// Reflects [`ty::TyKind::FnPtr`] and [`ty::TyKind::FnDef`]
832+
/// Reflects [`ty::TyKind::FnPtr`]
816833
Arrow(Box<PolyFnSig>),
817834

818835
#[custom_arm(

‎test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -133,7 +133,7 @@ class t_T (v_Self: Type0) = {
133133
val impl_T_for_u8:t_T u8
134134

135135
class t_TrGeneric (v_Self: Type0) (v_U: Type0) = {
136-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_13225137425257751668:Core.Clone.t_Clone v_U;
136+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_1848985618546216515:Core.Clone.t_Clone v_U;
137137
f_f_pre:v_U -> Type0;
138138
f_f_post:v_U -> v_Self -> Type0;
139139
f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result)

‎test-harness/src/snapshots/toolchain__traits into-fstar.snap‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -35,11 +35,11 @@ open FStar.Mul
3535
class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }
3636

3737
class t_ParBlocksSizeUser (v_Self: Type0) = {
38-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_17750095326162477464:t_BlockSizeUser v_Self
38+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_3159012011946225137:t_BlockSizeUser v_Self
3939
}
4040

4141
class t_BlockBackend (v_Self: Type0) = {
42-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_7661532914804666209:t_ParBlocksSizeUser v_Self;
42+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_16388660322355014604:t_ParBlocksSizeUser v_Self;
4343
f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
4444
f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
4545
f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global
@@ -55,7 +55,7 @@ open FStar.Mul
5555
class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit }
5656

5757
class t_Foo (v_Self: Type0) = {
58-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_11535804821030867870:t_Bar v_Self f_U;
58+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_5411500213814698936:t_Bar v_Self f_U;
5959
f_U:Type0
6060
}
6161
'''
@@ -425,11 +425,11 @@ let associated_function_caller
425425
()
426426

427427
class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
428-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_1779568480311729828:t_Trait v_Self
428+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_11151200176018912690:t_Trait v_Self
429429
v_TypeArg
430430
v_ConstArg;
431431
f_AssocType:Type0;
432-
f_AssocType_5410402773016444014:t_Trait f_AssocType v_TypeArg v_ConstArg
432+
f_AssocType_119499091631403638:t_Trait f_AssocType v_TypeArg v_ConstArg
433433
}
434434
'''
435435
"Traits.Interlaced_consts_types.fst" = '''
@@ -506,11 +506,11 @@ open FStar.Mul
506506

507507
class t_Trait1 (v_Self: Type0) = {
508508
f_T:Type0;
509-
f_T_16400978309441275701:t_Trait1 f_T
509+
f_T_4710375119464455744:t_Trait1 f_T
510510
}
511511

512512
class t_Trait2 (v_Self: Type0) = {
513-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_4351024728553910126:t_Trait1 v_Self;
513+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_1575596395930652292:t_Trait1 v_Self;
514514
f_U:Type0
515515
}
516516
'''
@@ -567,7 +567,7 @@ open Core
567567
open FStar.Mul
568568

569569
class t_SuperTrait (v_Self: Type0) = {
570-
[@@@ FStar.Tactics.Typeclasses.no_method]_super_9529721400157967266:Core.Clone.t_Clone v_Self;
570+
[@@@ FStar.Tactics.Typeclasses.no_method]_super_13802182059387893012:Core.Clone.t_Clone v_Self;
571571
f_function_of_super_trait_pre:v_Self -> Type0;
572572
f_function_of_super_trait_post:v_Self -> u32 -> Type0;
573573
f_function_of_super_trait:x0: v_Self
@@ -579,7 +579,7 @@ class t_SuperTrait (v_Self: Type0) = {
579579
[@@ FStar.Tactics.Typeclasses.tcinstance]
580580
let impl: t_SuperTrait i32 =
581581
{
582-
_super_9529721400157967266 = FStar.Tactics.Typeclasses.solve;
582+
_super_13802182059387893012 = FStar.Tactics.Typeclasses.solve;
583583
f_function_of_super_trait_pre = (fun (self: i32) -> true);
584584
f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true);
585585
f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl_i32__abs self <: i32) <: u32
@@ -651,7 +651,7 @@ let uuse_iimpl_trait (_: Prims.unit) : Prims.unit =
651651

652652
class t_Foo (v_Self: Type0) = {
653653
f_AssocType:Type0;
654-
f_AssocType_8652799156911219446:t_SuperTrait f_AssocType;
654+
f_AssocType_2403979284550981955:t_SuperTrait f_AssocType;
655655
f_N:usize;
656656
f_assoc_f_pre:Prims.unit -> Type0;
657657
f_assoc_f_post:Prims.unit -> Prims.unit -> Type0;
@@ -688,7 +688,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x
688688
let impl_Foo_for_tuple_: t_Foo Prims.unit =
689689
{
690690
f_AssocType = i32;
691-
f_AssocType_8652799156911219446 = FStar.Tactics.Typeclasses.solve;
691+
f_AssocType_2403979284550981955 = FStar.Tactics.Typeclasses.solve;
692692
f_N = mk_usize 32;
693693
f_assoc_f_pre = (fun (_: Prims.unit) -> true);
694694
f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);

0 commit comments

Comments
 (0)