charon_driver/hax/types/
ty.rs

1//! Copies of the relevant type-level types. These are semantically-rich representations of
2//! type-level concepts such as types and trait references.
3use crate::hax::prelude::*;
4use crate::hax::sinto_as_usize;
5use crate::hax::sinto_todo;
6
7use charon_lib::ast::HashConsed;
8use rustc_middle::ty;
9use rustc_span::def_id::DefId as RDefId;
10use rustc_type_ir::inherent::IntoKind;
11
12sinto_reexport!(rustc_abi::ExternAbi);
13
14/// Generic container for decorating items with a type, a span,
15/// attributes and other meta-data.
16
17#[derive(Clone, Debug, Hash, PartialEq, Eq)]
18pub struct Decorated<T> {
19    pub ty: Ty,
20    pub contents: Box<T>,
21}
22
23/// Reflects [`ty::ParamTy`]
24
25#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
26#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::ParamTy, state: S as gstate)]
27pub struct ParamTy {
28    pub index: u32,
29    pub name: Symbol,
30}
31
32/// Reflects [`ty::ParamConst`]
33
34#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
35#[args(<S>, from: ty::ParamConst, state: S as gstate)]
36pub struct ParamConst {
37    pub index: u32,
38    pub name: Symbol,
39}
40
41/// A predicate without `Self`, for use in `dyn Trait`.
42///
43/// Reflects [`ty::ExistentialPredicate`]
44#[derive(AdtInto)]
45#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::ExistentialPredicate<'tcx>, state: S as state)]
46#[derive(Clone, Debug, Hash, PartialEq, Eq)]
47pub enum ExistentialPredicate {
48    /// E.g. `From<u64>`. Note that this isn't `T: From<u64>` with a given `T`, this is just
49    /// `From<u64>`. Could be written `?: From<u64>`.
50    Trait(ExistentialTraitRef),
51    /// E.g. `Iterator::Item = u64`. Could be written `<? as Iterator>::Item = u64`.
52    Projection(ExistentialProjection),
53    /// E.g. `Send`.
54    AutoTrait(DefId),
55}
56
57/// Reflects [`rustc_type_ir::ExistentialTraitRef`]
58#[derive(AdtInto)]
59#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_type_ir::ExistentialTraitRef<ty::TyCtxt<'tcx>>, state: S as state)]
60#[derive(Clone, Debug, Hash, PartialEq, Eq)]
61pub struct ExistentialTraitRef {
62    pub def_id: DefId,
63    pub args: Vec<GenericArg>,
64}
65
66/// Reflects [`rustc_type_ir::ExistentialProjection`]
67#[derive(AdtInto)]
68#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_type_ir::ExistentialProjection<ty::TyCtxt<'tcx>>, state: S as state)]
69#[derive(Clone, Debug, Hash, PartialEq, Eq)]
70pub struct ExistentialProjection {
71    pub def_id: DefId,
72    pub args: Vec<GenericArg>,
73    pub term: Term,
74}
75
76/// Reflects [`ty::BoundTyKind`]
77
78#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
79#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTyKind<'tcx>, state: S as s)]
80pub enum BoundTyKind {
81    Anon,
82    #[custom_arm(&FROM_TYPE::Param(def_id) => TO_TYPE::Param(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
83    Param(DefId, Symbol),
84}
85
86/// Reflects [`ty::BoundTy`]
87
88#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
89#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundTy<'tcx>, state: S as s)]
90pub struct BoundTy {
91    pub var: BoundVar,
92    pub kind: BoundTyKind,
93}
94
95sinto_as_usize!(rustc_middle::ty, BoundVar);
96
97/// Reflects [`ty::BoundRegionKind`]
98
99#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
100#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegionKind<'tcx>, state: S as s)]
101pub enum BoundRegionKind {
102    Anon,
103    NamedForPrinting(Symbol),
104    #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
105    Named(DefId, Symbol),
106    ClosureEnv,
107}
108
109/// Reflects [`ty::BoundRegion`]
110
111#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
112#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundRegion<'tcx>, state: S as s)]
113pub struct BoundRegion {
114    pub var: BoundVar,
115    pub kind: BoundRegionKind,
116}
117
118/// Reflects [`ty::PlaceholderRegion`]
119pub type PlaceholderRegion = Placeholder<BoundRegion>;
120/// Reflects [`ty::PlaceholderConst`]
121pub type PlaceholderConst = Placeholder<BoundVar>;
122/// Reflects [`ty::PlaceholderType`]
123pub type PlaceholderType = Placeholder<BoundTy>;
124
125/// Reflects [`ty::Placeholder`]
126
127#[derive(Clone, Debug, Hash, PartialEq, Eq)]
128pub struct Placeholder<T> {
129    pub bound: T,
130}
131
132impl<'tcx, S: UnderOwnerState<'tcx>, T: SInto<S, U>, U> SInto<S, Placeholder<U>>
133    for ty::Placeholder<ty::TyCtxt<'tcx>, T>
134{
135    fn sinto(&self, s: &S) -> Placeholder<U> {
136        Placeholder {
137            bound: self.bound.sinto(s),
138        }
139    }
140}
141
142/// Reflects [`rustc_middle::infer::canonical::Canonical`]
143
144#[derive(Clone, Debug)]
145pub struct Canonical<T> {
146    pub value: T,
147}
148/// Reflects [`ty::CanonicalUserType`]
149pub type CanonicalUserType = Canonical<UserType>;
150
151impl<'tcx, S: UnderOwnerState<'tcx>, T: SInto<S, U>, U> SInto<S, Canonical<U>>
152    for rustc_middle::infer::canonical::Canonical<'tcx, T>
153{
154    fn sinto(&self, s: &S) -> Canonical<U> {
155        Canonical {
156            value: self.value.sinto(s),
157        }
158    }
159}
160
161/// Reflects [`ty::UserSelfTy`]
162
163#[derive(AdtInto, Clone, Debug)]
164#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::UserSelfTy<'tcx>, state: S as gstate)]
165pub struct UserSelfTy {
166    pub impl_def_id: DefId,
167    pub self_ty: Ty,
168}
169
170/// Reflects [`ty::UserArgs`]
171
172#[derive(AdtInto, Clone, Debug)]
173#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::UserArgs<'tcx>, state: S as gstate)]
174pub struct UserArgs {
175    pub args: Vec<GenericArg>,
176    pub user_self_ty: Option<UserSelfTy>,
177}
178
179/// Reflects [`ty::UserType`]: this is currently
180/// disabled, and everything is printed as debug in the
181/// [`UserType::Todo`] variant.
182
183#[derive(AdtInto, Clone, Debug)]
184#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::UserType<'tcx>, state: S as _s)]
185pub enum UserType {
186    // TODO: for now, we don't use user types at all.
187    // We disable it for now, since it cause the following to fail:
188    //
189    //    pub const MY_VAL: u16 = 5;
190    //    pub type Alias = MyStruct<MY_VAL>; // Using the literal 5, it goes through
191    //
192    //    pub struct MyStruct<const VAL: u16> {}
193    //
194    //    impl<const VAL: u16> MyStruct<VAL> {
195    //        pub const MY_CONST: u16 = VAL;
196    //    }
197    //
198    //    pub fn do_something() -> u32 {
199    //        u32::from(Alias::MY_CONST)
200    //    }
201    //
202    // In this case, we get a [ty::ConstKind::Bound] in
203    // [do_something], which we are not able to translate.
204    // See: https://github.com/hacspec/hax/pull/209
205
206    // Ty(Ty),
207    // TypeOf(DefId, UserArgs),
208    #[todo]
209    Todo(String),
210}
211
212/// Reflects [`ty::VariantDiscr`]
213
214#[derive(AdtInto, Clone, Debug)]
215#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::VariantDiscr, state: S as gstate)]
216pub enum DiscriminantDefinition {
217    Explicit(DefId),
218    Relative(u32),
219}
220
221/// Reflects [`ty::util::Discr`]
222
223#[derive(AdtInto, Clone, Debug)]
224#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::util::Discr<'tcx>, state: S as gstate)]
225pub struct DiscriminantValue {
226    pub val: u128,
227    pub ty: Ty,
228}
229
230/// Reflects [`ty::Visibility`]
231
232#[derive(Clone, Debug)]
233pub enum Visibility<Id> {
234    Public,
235    Restricted(Id),
236}
237
238impl<S, T: SInto<S, U>, U> SInto<S, Visibility<U>> for ty::Visibility<T> {
239    fn sinto(&self, s: &S) -> Visibility<U> {
240        use ty::Visibility as T;
241        match self {
242            T::Public => Visibility::Public,
243            T::Restricted(id) => Visibility::Restricted(id.sinto(s)),
244        }
245    }
246}
247
248/// Reflects [`ty::FieldDef`]
249
250#[derive(Clone, Debug)]
251pub struct FieldDef {
252    pub did: DefId,
253    /// Field definition of [tuple
254    /// structs](https://doc.rust-lang.org/book/ch05-01-defining-structs.html#using-tuple-structs-without-named-fields-to-create-different-types)
255    /// are anonymous, in that case `name` is [`None`].
256    pub name: Option<Symbol>,
257    pub vis: Visibility<DefId>,
258    pub ty: Ty,
259    pub span: Span,
260}
261
262impl FieldDef {
263    pub fn sfrom<'tcx, S: UnderOwnerState<'tcx>>(
264        s: &S,
265        fdef: &ty::FieldDef,
266        instantiate: ty::GenericArgsRef<'tcx>,
267    ) -> FieldDef {
268        let tcx = s.base().tcx;
269        let ty = normalize(tcx, s.typing_env(), fdef.ty(tcx, instantiate)).sinto(s);
270        let name = {
271            let name = fdef.name.sinto(s);
272            let is_user_provided = {
273                // SH: Note that the only way I found of checking if the user wrote the name or if it
274                // is just an integer generated by rustc is by checking if it is just made of
275                // numerals...
276                name.to_string().parse::<usize>().is_err()
277            };
278            is_user_provided.then_some(name)
279        };
280
281        FieldDef {
282            did: fdef.did.sinto(s),
283            name,
284            vis: fdef.vis.sinto(s),
285            ty,
286            span: tcx.def_span(fdef.did).sinto(s),
287        }
288    }
289}
290
291/// Reflects [`ty::VariantDef`]
292
293#[derive(Clone, Debug)]
294pub struct VariantDef {
295    pub def_id: DefId,
296    pub ctor: Option<(CtorKind, DefId)>,
297    pub name: Symbol,
298    pub discr_def: DiscriminantDefinition,
299    pub discr_val: DiscriminantValue,
300    /// The definitions of the fields on this variant. In case of [tuple
301    /// structs/variants](https://doc.rust-lang.org/book/ch05-01-defining-structs.html#using-tuple-structs-without-named-fields-to-create-different-types),
302    /// the fields are anonymous, otherwise fields are named.
303    pub fields: IndexVec<FieldIdx, FieldDef>,
304    /// Span of the definition of the variant
305    pub span: Span,
306}
307
308impl VariantDef {
309    pub(crate) fn sfrom<'tcx, S: UnderOwnerState<'tcx>>(
310        s: &S,
311        def: &ty::VariantDef,
312        discr_val: ty::util::Discr<'tcx>,
313        instantiate: Option<ty::GenericArgsRef<'tcx>>,
314    ) -> Self {
315        let def_id = def.def_id.sinto(s);
316        let instantiate = instantiate.unwrap_or_else(|| def_id.identity_args(s));
317        VariantDef {
318            def_id,
319            ctor: def.ctor.sinto(s),
320            name: def.name.sinto(s),
321            discr_def: def.discr.sinto(s),
322            discr_val: discr_val.sinto(s),
323            fields: def
324                .fields
325                .iter()
326                .map(|f| FieldDef::sfrom(s, f, instantiate))
327                .collect(),
328            span: s.base().tcx.def_span(def.def_id).sinto(s),
329        }
330    }
331}
332
333/// Reflects [`ty::EarlyParamRegion`]
334
335#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
336#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::EarlyParamRegion, state: S as s)]
337pub struct EarlyParamRegion {
338    pub index: u32,
339    pub name: Symbol,
340}
341
342/// Reflects [`ty::LateParamRegion`]
343
344#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
345#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegion, state: S as s)]
346pub struct LateParamRegion {
347    pub scope: DefId,
348    pub kind: LateParamRegionKind,
349}
350
351/// Reflects [`ty::LateParamRegionKind`]
352
353#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
354#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::LateParamRegionKind, state: S as s)]
355pub enum LateParamRegionKind {
356    Anon(u32),
357    NamedAnon(u32, Symbol),
358    #[custom_arm(&FROM_TYPE::Named(def_id) => TO_TYPE::Named(def_id.sinto(s), s.base().tcx.item_name(def_id).sinto(s)),)]
359    Named(DefId, Symbol),
360    ClosureEnv,
361}
362
363/// Reflects [`ty::RegionKind`]
364
365#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
366#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::RegionKind<'tcx>, state: S as gstate)]
367pub enum RegionKind {
368    ReEarlyParam(EarlyParamRegion),
369    ReBound(BoundVarIndexKind, BoundRegion),
370    ReLateParam(LateParamRegion),
371    ReStatic,
372    ReVar(RegionVid),
373    RePlaceholder(PlaceholderRegion),
374    ReErased,
375    ReError(ErrorGuaranteed),
376}
377
378/// Reflects [`ty::BoundVarIndexKind`]
379
380#[derive(AdtInto, Clone, Copy, Debug, Hash, PartialEq, Eq)]
381#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundVarIndexKind, state: S as gstate)]
382pub enum BoundVarIndexKind {
383    Bound(DebruijnIndex),
384    Canonical,
385}
386
387sinto_as_usize!(rustc_middle::ty, DebruijnIndex);
388sinto_as_usize!(rustc_middle::ty, RegionVid);
389
390/// Reflects [`ty::Region`]
391
392#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
393#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::Region<'tcx>, state: S as s)]
394pub struct Region {
395    #[value(self.kind().sinto(s))]
396    pub kind: RegionKind,
397}
398
399/// Reflects both [`ty::GenericArg`] and [`ty::GenericArgKind`]
400
401#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
402#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::GenericArgKind<'tcx>, state: S as s)]
403pub enum GenericArg {
404    Lifetime(Region),
405    Type(Ty),
406    Const(ConstantExpr),
407}
408
409impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, GenericArg> for ty::GenericArg<'tcx> {
410    fn sinto(&self, s: &S) -> GenericArg {
411        self.kind().sinto(s)
412    }
413}
414
415impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Vec<GenericArg>> for ty::GenericArgsRef<'tcx> {
416    fn sinto(&self, s: &S) -> Vec<GenericArg> {
417        self.iter().map(|v| v.kind().sinto(s)).collect()
418    }
419}
420
421/// Reflects both [`ty::GenericArg`] and [`ty::GenericArgKind`]
422#[derive(AdtInto)]
423#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
424#[derive(Clone, Debug, Hash, PartialEq, Eq)]
425pub enum LitIntType {
426    Signed(IntTy),
427    Unsigned(UintTy),
428    Unsuffixed,
429}
430
431/// Reflects partially [`ty::InferTy`]
432
433#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
434#[args(<'tcx, S>, from: ty::InferTy, state: S as gstate)]
435pub enum InferTy {
436    #[custom_arm(FROM_TYPE::TyVar(..) => TO_TYPE::TyVar,)]
437    TyVar, /*TODO?*/
438    #[custom_arm(FROM_TYPE::IntVar(..) => TO_TYPE::IntVar,)]
439    IntVar, /*TODO?*/
440    #[custom_arm(FROM_TYPE::FloatVar(..) => TO_TYPE::FloatVar,)]
441    FloatVar, /*TODO?*/
442    FreshTy(u32),
443    FreshIntTy(u32),
444    FreshFloatTy(u32),
445}
446
447/// Reflects [`rustc_type_ir::IntTy`]
448#[derive(AdtInto)]
449#[args(<S>, from: rustc_type_ir::IntTy, state: S as _s)]
450#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
451pub enum IntTy {
452    Isize,
453    I8,
454    I16,
455    I32,
456    I64,
457    I128,
458}
459
460/// Reflects [`rustc_type_ir::FloatTy`]
461#[derive(AdtInto)]
462#[args(<S>, from: rustc_type_ir::FloatTy, state: S as _s)]
463#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
464pub enum FloatTy {
465    F16,
466    F32,
467    F64,
468    F128,
469}
470
471/// Reflects [`rustc_type_ir::UintTy`]
472#[derive(AdtInto)]
473#[args(<S>, from: rustc_type_ir::UintTy, state: S as _s)]
474#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
475pub enum UintTy {
476    Usize,
477    U8,
478    U16,
479    U32,
480    U64,
481    U128,
482}
483
484#[allow(clippy::to_string_trait_impl)]
485impl ToString for IntTy {
486    fn to_string(&self) -> String {
487        use IntTy::*;
488        match self {
489            Isize => "isize".to_string(),
490            I8 => "i8".to_string(),
491            I16 => "i16".to_string(),
492            I32 => "i32".to_string(),
493            I64 => "i64".to_string(),
494            I128 => "i128".to_string(),
495        }
496    }
497}
498
499#[allow(clippy::to_string_trait_impl)]
500impl ToString for UintTy {
501    fn to_string(&self) -> String {
502        use UintTy::*;
503        match self {
504            Usize => "usize".to_string(),
505            U8 => "u8".to_string(),
506            U16 => "u16".to_string(),
507            U32 => "u32".to_string(),
508            U64 => "u64".to_string(),
509            U128 => "u128".to_string(),
510        }
511    }
512}
513
514/// Reflects [`ty::TypeAndMut`]
515#[derive(AdtInto)]
516#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::TypeAndMut<'tcx>, state: S as gstate)]
517#[derive(Clone, Debug, Hash, PartialEq, Eq)]
518pub struct TypeAndMut {
519    pub ty: Box<Ty>,
520    pub mutbl: Mutability,
521}
522
523impl<S, U, T: SInto<S, U>> SInto<S, Vec<U>> for ty::List<T> {
524    fn sinto(&self, s: &S) -> Vec<U> {
525        self.iter().map(|x| x.sinto(s)).collect()
526    }
527}
528
529/// Reflects [`ty::Variance`]
530#[derive(AdtInto)]
531#[args(<S>, from: ty::Variance, state: S as _s)]
532#[derive(Clone, Debug)]
533pub enum Variance {
534    Covariant,
535    Invariant,
536    Contravariant,
537    Bivariant,
538}
539
540/// Reflects [`ty::GenericParamDef`]
541#[derive(AdtInto)]
542#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::GenericParamDef, state: S as s)]
543#[derive(Clone, Debug)]
544pub struct GenericParamDef {
545    pub name: Symbol,
546    pub def_id: DefId,
547    pub index: u32,
548    pub pure_wrt_drop: bool,
549    #[value(
550        match self.kind {
551            ty::GenericParamDefKind::Lifetime => GenericParamDefKind::Lifetime,
552            ty::GenericParamDefKind::Type { has_default, synthetic } => GenericParamDefKind::Type { has_default, synthetic },
553            ty::GenericParamDefKind::Const { has_default, .. } => {
554                let tcx = s.base().tcx;
555                let ty = tcx.type_of(self.def_id).instantiate_identity();
556                let ty = normalize(tcx, s.typing_env(), ty).sinto(s);
557                GenericParamDefKind::Const { has_default, ty }
558            },
559        }
560    )]
561    pub kind: GenericParamDefKind,
562    /// Variance of this type parameter, if sensible.
563    #[value({
564        use rustc_hir::def::DefKind::*;
565        let tcx = s.base().tcx;
566        let parent = tcx.parent(self.def_id);
567        match tcx.def_kind(parent) {
568            Fn | AssocFn | Enum | Struct | Union | Ctor(..) | OpaqueTy => {
569                tcx.variances_of(parent).get(self.index as usize).sinto(s)
570            }
571            _ => None
572        }
573    })]
574    pub variance: Option<Variance>,
575}
576
577/// Reflects [`ty::GenericParamDefKind`]
578
579#[derive(Clone, Debug)]
580pub enum GenericParamDefKind {
581    Lifetime,
582    Type { has_default: bool, synthetic: bool },
583    Const { has_default: bool, ty: Ty },
584}
585
586/// Reflects [`ty::Generics`]
587#[derive(AdtInto)]
588#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::Generics, state: S as state)]
589#[derive(Clone, Debug)]
590pub struct TyGenerics {
591    pub parent: Option<DefId>,
592    pub parent_count: usize,
593    #[from(own_params)]
594    pub params: Vec<GenericParamDef>,
595    // pub param_def_id_to_index: FxHashMap<DefId, u32>,
596    pub has_self: bool,
597    pub has_late_bound_regions: Option<Span>,
598}
599
600/// This type merges the information from
601/// [`ty::AliasTyKind`] and [`ty::AliasTy`].
602#[derive(Clone, Debug, Hash, PartialEq, Eq)]
603pub struct Alias {
604    pub kind: AliasKind,
605    pub args: Vec<GenericArg>,
606    pub def_id: DefId,
607}
608
609/// Reflects [`rustc_middle::ty::AliasTyKind`].
610#[derive(Clone, Debug, Hash, PartialEq, Eq)]
611pub enum AliasKind {
612    /// The projection of a trait type: `<Ty as Trait<...>>::Type<...>`
613    Projection(ItemRef),
614    /// An associated type in an inherent impl.
615    Inherent,
616    /// An `impl Trait` opaque type.
617    Opaque {
618        /// The real type hidden inside this opaque type.
619        hidden_ty: Ty,
620    },
621    /// A type alias that references opaque types. Likely to always be normalized away.
622    Free,
623}
624
625impl Alias {
626    #[tracing::instrument(level = "trace", skip(s))]
627    fn from<'tcx, S: UnderOwnerState<'tcx>>(s: &S, alias_ty: &ty::AliasTy<'tcx>) -> TyKind {
628        let tcx = s.base().tcx;
629        let typing_env = s.typing_env();
630        use rustc_type_ir::AliasTyKind as RustAliasKind;
631
632        // Try to normalize the alias first.
633        let ty = ty::Ty::new_alias(tcx, *alias_ty);
634        let ty = normalize(tcx, typing_env, ty::Unnormalized::new(ty));
635        let ty::Alias(alias_ty) = ty.kind() else {
636            let ty: Ty = ty.sinto(s);
637            return ty.kind().clone();
638        };
639
640        let kind = match alias_ty.kind {
641            RustAliasKind::Projection { def_id } => {
642                AliasKind::Projection(ItemRef::translate_projection(s, def_id, alias_ty.args))
643            }
644            RustAliasKind::Inherent { .. } => AliasKind::Inherent,
645            RustAliasKind::Opaque { def_id } => {
646                // Reveal the underlying `impl Trait` type.
647                let ty = tcx.type_of(def_id).instantiate(tcx, alias_ty.args);
648                let ty = normalize(tcx, s.typing_env(), ty);
649                AliasKind::Opaque {
650                    hidden_ty: ty.sinto(s),
651                }
652            }
653            RustAliasKind::Free { .. } => AliasKind::Free,
654        };
655        TyKind::Alias(Alias {
656            kind,
657            args: alias_ty.args.sinto(s),
658            def_id: alias_ty.kind.def_id().sinto(s),
659        })
660    }
661}
662
663impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Box<Ty>> for ty::Ty<'tcx> {
664    fn sinto(&self, s: &S) -> Box<Ty> {
665        Box::new(self.sinto(s))
666    }
667}
668
669/// Reflects [`rustc_middle::ty::Ty`]
670
671#[derive(Clone, Debug, Hash, PartialEq, Eq)]
672pub struct Ty {
673    pub(crate) kind: HashConsed<TyKind>,
674}
675
676impl Ty {
677    pub fn new<'tcx, S: BaseState<'tcx>>(_s: &S, kind: TyKind) -> Self {
678        let kind = HashConsed::new(kind);
679        Ty { kind }
680    }
681
682    pub fn kind(&self) -> &TyKind {
683        self.kind.inner()
684    }
685}
686
687impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Ty> for rustc_middle::ty::Ty<'tcx> {
688    fn sinto(&self, s: &S) -> Ty {
689        if let Some(ty) = s.with_cache(|cache| cache.tys.get(self).cloned()) {
690            return ty;
691        }
692        let kind: TyKind = self.kind().sinto(s);
693        let ty = Ty::new(s, kind);
694        s.with_cache(|cache| {
695            cache.tys.insert(*self, ty.clone());
696        });
697        ty
698    }
699}
700
701/// Reflects [`ty::TyKind`]
702#[derive(AdtInto)]
703#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::TyKind<'tcx>, state: S as s)]
704#[derive(Clone, Debug, Hash, PartialEq, Eq)]
705pub enum TyKind {
706    Bool,
707    Char,
708    Int(IntTy),
709    Uint(UintTy),
710    Float(FloatTy),
711
712    #[custom_arm(
713        ty::TyKind::FnDef(fun_id, generics) => {
714            let item = translate_item_ref(s, *fun_id, generics);
715            let tcx = s.base().tcx;
716            let fn_sig = tcx.fn_sig(*fun_id).instantiate(tcx, generics);
717            let fn_sig = Box::new(normalize(tcx, s.typing_env(), fn_sig).sinto(s));
718            TyKind::FnDef { item, fn_sig }
719        },
720    )]
721    /// Reflects [`ty::TyKind::FnDef`]
722    FnDef {
723        item: ItemRef,
724        fn_sig: Box<PolyFnSig>,
725    },
726
727    #[custom_arm(
728        ty::TyKind::FnPtr(tys, header) => {
729            let fn_sig_kind = ty::FnSigKind::new(header.abi(), header.safety(), header.c_variadic());
730            let sig = tys.map_bound(|tys| ty::FnSig {
731                inputs_and_output: tys.inputs_and_output,
732                fn_sig_kind,
733            });
734            TyKind::Arrow(Box::new(sig.sinto(s)))
735        },
736    )]
737    /// Reflects [`ty::TyKind::FnPtr`]
738    Arrow(Box<PolyFnSig>),
739
740    #[custom_arm(
741        ty::TyKind::Closure (def_id, generics) => {
742            TyKind::Closure(ClosureArgs::sfrom(s, *def_id, generics))
743        },
744    )]
745    Closure(ClosureArgs),
746
747    #[custom_arm(FROM_TYPE::Adt(adt_def, generics) => TO_TYPE::Adt(translate_item_ref(s, adt_def.did(), generics)),)]
748    Adt(ItemRef),
749    #[custom_arm(FROM_TYPE::Foreign(def_id) => TO_TYPE::Foreign(translate_item_ref(s, *def_id, Default::default())),)]
750    Foreign(ItemRef),
751    /// The `ItemRef` uses the fake `Array` def_id.
752    #[custom_arm(FROM_TYPE::Array(ty, len) => TO_TYPE::Array({
753        let args = s.base().tcx.mk_args(&[(*ty).into(), (*len).into()]);
754        ItemRef::translate_synthetic(s, SyntheticItem::Array, args)
755    }),)]
756    Array(ItemRef),
757    Pat(Ty, Pattern),
758    /// The `ItemRef` uses the fake `Slice` def_id.
759    #[custom_arm(FROM_TYPE::Slice(ty) => TO_TYPE::Slice({
760        let args = s.base().tcx.mk_args(&[(*ty).into()]);
761        ItemRef::translate_synthetic(s, SyntheticItem::Slice, args)
762    }),)]
763    Slice(ItemRef),
764    /// The `ItemRef` uses the fake `Tuple` def_id.
765    #[custom_arm(FROM_TYPE::Tuple(tys) => TO_TYPE::Tuple({
766        let args = s.base().tcx.mk_args_from_iter(tys.into_iter().map(ty::GenericArg::from));
767        ItemRef::translate_synthetic(s, SyntheticItem::Tuple(tys.len()), args)
768    }),)]
769    Tuple(ItemRef),
770    Str,
771    RawPtr(Box<Ty>, Mutability),
772    Ref(Region, Box<Ty>, Mutability),
773    #[custom_arm(FROM_TYPE::Dynamic(preds, region) => TyKind::Dynamic(resolve_for_dyn(s, preds, |_, _| ()), region.sinto(s)),)]
774    Dynamic(DynBinder<()>, Region),
775    #[custom_arm(FROM_TYPE::Coroutine(def_id, generics) => TO_TYPE::Coroutine(translate_item_ref(s, *def_id, generics)),)]
776    Coroutine(ItemRef),
777    Never,
778    #[custom_arm(FROM_TYPE::Alias(alias_ty) => Alias::from(s, alias_ty),)]
779    Alias(Alias),
780    Param(ParamTy),
781    Bound(BoundVarIndexKind, BoundTy),
782    Placeholder(PlaceholderType),
783    Infer(InferTy),
784    #[custom_arm(FROM_TYPE::Error(..) => TO_TYPE::Error,)]
785    Error,
786    #[todo]
787    Todo(String),
788}
789
790/// A representation of `exists<T: Trait1 + Trait2>(value)`: we create a fresh type id and the
791/// appropriate trait clauses. The contained value may refer to the fresh ty and the in-scope trait
792/// clauses. This is used to represent types related to `dyn Trait`.
793
794#[derive(Clone, Debug, Hash, PartialEq, Eq)]
795pub struct DynBinder<T> {
796    /// Fresh type parameter that we use as the `Self` type in the prediates below.
797    pub existential_ty: ParamTy,
798    /// Clauses that define the trait object. These clauses use the fresh type parameter above
799    /// as `Self` type.
800    pub predicates: GenericPredicates,
801    /// The value inside the binder.
802    pub val: T,
803}
804
805/// Do trait resolution in the context of the clauses of a `dyn Trait` type.
806fn resolve_for_dyn<'tcx, S: UnderOwnerState<'tcx>, R>(
807    s: &S,
808    // The predicates in the context.
809    epreds: &'tcx ty::List<ty::Binder<'tcx, ty::ExistentialPredicate<'tcx>>>,
810    f: impl FnOnce(&mut PredicateSearcher<'tcx>, ty::Ty<'tcx>) -> R,
811) -> DynBinder<R> {
812    fn searcher_for_traits<'tcx, S: UnderOwnerState<'tcx>>(
813        s: &S,
814        preds: &ItemPredicates<'tcx, DefId>,
815    ) -> PredicateSearcher<'tcx> {
816        let tcx = s.base().tcx;
817        // Populate a predicate searcher that knows about the `dyn` clauses.
818        let mut predicate_searcher = s.with_predicate_searcher(|ps, _| ps.clone());
819        predicate_searcher.insert_bound_predicates(&s.base_state(), preds.iter());
820        predicate_searcher.set_param_env(param_env_from_clauses(
821            tcx,
822            s.param_env()
823                .caller_bounds()
824                .iter()
825                .chain(preds.iter().map(|pred| pred.clause)),
826        ));
827        predicate_searcher
828    }
829
830    fn fresh_param_ty<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> ty::ParamTy {
831        let generics = s.owner().generics_of(s);
832        let param_count = generics.count();
833        ty::ParamTy::new(param_count as u32 + 1, rustc_span::Symbol::intern("_dyn"))
834    }
835
836    let tcx = s.base().tcx;
837    let span = rustc_span::DUMMY_SP.sinto(s);
838
839    // Pretend there's an extra type in the environment.
840    let new_param_ty = fresh_param_ty(s);
841    let new_ty = new_param_ty.to_ty(tcx);
842
843    // Set the new type as the `Self` parameter of our predicates.
844    let predicates = epreds.iter().map(|epred| epred.with_self_ty(tcx, new_ty));
845    let predicates: ItemPredicates<'_, DefId> = ItemPredicates::new_unmapped(span, predicates);
846
847    // Populate a predicate searcher that knows about the `dyn` clauses.
848    let mut predicate_searcher = searcher_for_traits(s, &predicates);
849    let val = f(&mut predicate_searcher, new_ty);
850
851    // Using the predicate searcher, translate the predicates. Only the projection predicates need
852    // to be handled specially.
853    let predicates = predicates
854        .iter()
855        .map(|pred| {
856            match pred.clause.as_projection_clause() {
857                // Translate normally
858                None => pred.sinto(s),
859                // Translate by hand using our predicate searcher. This does the same as
860                // `clause.sinto(s)` except that it uses our predicate searcher to resolve the
861                // projection `TraitProof`.
862                Some(proj) => {
863                    let bound_vars = proj.bound_vars().sinto(s);
864                    let proj = {
865                        let alias_ty = &proj.skip_binder().projection_term.expect_ty(tcx);
866                        let trait_proof = {
867                            let poly_trait_ref = proj.rebind(alias_ty.trait_ref(tcx));
868                            predicate_searcher
869                                .resolve(&s.base_state(), &poly_trait_ref)
870                                .sinto(s)
871                        };
872                        let Term::Ty(ty) = proj.skip_binder().term.sinto(s) else {
873                            unreachable!()
874                        };
875                        let item = tcx.associated_item(alias_ty.kind.def_id());
876                        ProjectionPredicate {
877                            trait_proof,
878                            assoc_item: AssocItem::sfrom(s, &item),
879                            ty,
880                        }
881                    };
882                    let kind = Binder {
883                        value: ClauseKind::Projection(proj),
884                        bound_vars,
885                    };
886                    let clause = Clause { kind };
887                    GenericPredicate {
888                        id: pred.id.sinto(s),
889                        clause,
890                        span,
891                    }
892                }
893            }
894        })
895        .collect();
896
897    let predicates = GenericPredicates { predicates };
898    DynBinder {
899        existential_ty: new_param_ty.sinto(s),
900        predicates,
901        val,
902    }
903}
904
905#[derive(AdtInto)]
906#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::pattern::PatternKind<'tcx>, state: S as gstate)]
907#[derive(Clone, Debug, Hash, PartialEq, Eq)]
908pub enum Pattern {
909    Range {
910        start: ConstantExpr,
911        end: ConstantExpr,
912    },
913    Or(Vec<Pattern>),
914    NotNull,
915}
916
917impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Pattern> for ty::Pattern<'tcx> {
918    fn sinto(&self, s: &S) -> Pattern {
919        self.kind().sinto(s)
920    }
921}
922/// Reflects [`ty::CanonicalUserTypeAnnotation`]
923#[derive(AdtInto)]
924#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::CanonicalUserTypeAnnotation<'tcx>, state: S as gstate)]
925#[derive(Clone, Debug)]
926pub struct CanonicalUserTypeAnnotation {
927    pub user_ty: CanonicalUserType,
928    pub span: Span,
929    pub inferred_ty: Ty,
930}
931
932/// Reflects [`ty::AdtKind`]
933
934#[derive(Copy, Clone, Debug)]
935pub enum AdtKind {
936    Struct,
937    Union,
938    Enum,
939    /// We sometimes pretend arrays are an ADT and generate a `FullDef` for them.
940    Array,
941    /// We sometimes pretend slices are an ADT and generate a `FullDef` for them.
942    Slice,
943    /// We sometimes pretend tuples are an ADT and generate a `FullDef` for them.
944    Tuple,
945}
946
947impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, AdtKind> for ty::AdtKind {
948    fn sinto(&self, _s: &S) -> AdtKind {
949        match self {
950            ty::AdtKind::Struct => AdtKind::Struct,
951            ty::AdtKind::Union => AdtKind::Union,
952            ty::AdtKind::Enum => AdtKind::Enum,
953        }
954    }
955}
956
957sinto_todo!(rustc_middle::ty, AdtFlags);
958
959/// Reflects [`rustc_abi::ReprOptions`].
960
961#[derive(AdtInto, Clone, Debug)]
962#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_abi::ReprOptions, state: S as s)]
963pub struct ReprOptions {
964    /// Whether an explicit integer representation was specified.
965    #[value(self.int.is_some())]
966    pub int_specified: bool,
967    /// The actual discriminant type resulting from the representation options.
968    #[value({
969        use rustc_middle::ty::util::IntTypeExt;
970        self.discr_type().to_ty(s.base().tcx).sinto(s)
971    })]
972    pub typ: Ty,
973    pub align: Option<Align>,
974    pub pack: Option<Align>,
975    #[value(ReprFlags { is_c: self.c(), is_transparent: self.transparent(), is_simd: self.simd() })]
976    pub flags: ReprFlags,
977}
978
979/// The representation flags without the ones irrelevant outside of rustc.
980
981#[derive(Default, Clone, Debug)]
982pub struct ReprFlags {
983    pub is_c: bool,
984    pub is_transparent: bool,
985    pub is_simd: bool,
986}
987
988/// Reflects [`rustc_abi::Align`], but directly stores the number of bytes as a u64.
989
990#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
991#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_abi::Align, state: S as _s)]
992pub struct Align {
993    #[value({
994        self.bytes()
995    })]
996    pub bytes: u64,
997}
998
999/// The metadata to attach to the newly-unsized ptr.
1000#[derive(Clone, Debug)]
1001pub enum UnsizingMetadata {
1002    /// Unsize an array to a slice, storing the length as metadata.
1003    Length(ConstantExpr),
1004    /// Unsize a non-dyn type to a dyn type, adding a vtable pointer as metadata.
1005    DirectVTable(TraitProof),
1006    /// Unsize a dyn-type to another dyn-type, (optionally) indexing within the current vtable.
1007    NestedVTable(DynBinder<TraitProof>),
1008    /// Couldn't compute
1009    Unknown,
1010}
1011
1012pub fn compute_unsizing_metadata<'tcx, S: UnderOwnerState<'tcx>>(
1013    s: &S,
1014    src_ty: ty::Ty<'tcx>,
1015    tgt_ty: ty::Ty<'tcx>,
1016) -> UnsizingMetadata {
1017    // TODO: to properly find out what field we want, we should use the query
1018    // `coerce_unsized_info`, which we call recursively to get the list of fields
1019    // to go into until we reach a pointer/reference.
1020    // We should also pass this list of field IDs in the unsizing metadata.
1021
1022    let (Some(src_ty), Some(tgt_ty)) = (src_ty.builtin_deref(true), tgt_ty.builtin_deref(true))
1023    else {
1024        return UnsizingMetadata::Unknown;
1025    };
1026
1027    let tcx = s.base().tcx;
1028    let typing_env = s.typing_env();
1029    let (src_ty, tgt_ty) =
1030        tcx.struct_lockstep_tails_raw(src_ty, tgt_ty, |ty| normalize(tcx, typing_env, ty));
1031
1032    match (&src_ty.kind(), &tgt_ty.kind()) {
1033        (ty::Array(_, len), ty::Slice(_)) => {
1034            let len = len.sinto(s);
1035            UnsizingMetadata::Length(len)
1036        }
1037        (ty::Dynamic(from_preds, _), ty::Dynamic(to_preds, ..)) => {
1038            let trait_proof = resolve_for_dyn(s, from_preds, |searcher, fresh_ty| {
1039                let to_pred = if let Some(to_principal) = to_preds.principal() {
1040                    to_principal.with_self_ty(tcx, fresh_ty)
1041                } else {
1042                    let def_id = to_preds
1043                        .iter()
1044                        .find_map(|pred| match pred.skip_binder() {
1045                            ty::ExistentialPredicate::AutoTrait(def_id) => Some(def_id),
1046                            _ => None,
1047                        })
1048                        .expect("expected a trait predicate in dyn upcast target");
1049                    ty::Binder::dummy(ty::TraitRef::new(tcx, def_id, [fresh_ty]))
1050                };
1051                searcher.resolve(&s.base_state(), &to_pred).sinto(s)
1052            });
1053            UnsizingMetadata::NestedVTable(trait_proof)
1054        }
1055        (_, ty::Dynamic(preds, ..)) => {
1056            let pred = preds[0].with_self_ty(tcx, src_ty);
1057            let clause = pred.as_trait_clause().expect(
1058                "the first `ExistentialPredicate` of `TyKind::Dynamic` \\
1059                                        should be a trait clause",
1060            );
1061            let tref = clause.rebind(clause.skip_binder().trait_ref);
1062            let trait_proof = solve_trait(s, tref);
1063
1064            UnsizingMetadata::DirectVTable(trait_proof)
1065        }
1066        _ => UnsizingMetadata::Unknown,
1067    }
1068}
1069
1070/// Reflects [`ty::FnSig`]
1071#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
1072#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::FnSig<'tcx>, state: S as s)]
1073pub struct TyFnSig {
1074    #[value(self.inputs().sinto(s))]
1075    pub inputs: Vec<Ty>,
1076    #[value(self.output().sinto(s))]
1077    pub output: Ty,
1078    #[value(self.c_variadic())]
1079    pub c_variadic: bool,
1080    #[value(self.safety())]
1081    pub safety: Safety,
1082    #[value(self.abi())]
1083    pub abi: ExternAbi,
1084}
1085
1086/// Reflects [`ty::PolyFnSig`]
1087pub type PolyFnSig = Binder<TyFnSig>;
1088
1089/// Reflects [`ty::TraitRef`]
1090/// Contains the def_id and arguments passed to the trait. The first type argument is the `Self`
1091/// type. The trait proofs are the _required_ predicate for this trait; currently they are always
1092/// empty because we consider all trait predicates as implied.
1093/// `self.in_trait` is always `None` because a trait can't be associated to another one.
1094pub type TraitRef = ItemRef;
1095
1096impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, TraitRef> for ty::TraitRef<'tcx> {
1097    fn sinto(&self, s: &S) -> TraitRef {
1098        translate_item_ref(s, self.def_id, self.args)
1099    }
1100}
1101
1102/// Reflects [`ty::TraitPredicate`]
1103#[derive(AdtInto)]
1104#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::TraitPredicate<'tcx>, state: S as tcx)]
1105#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1106pub struct TraitPredicate {
1107    pub trait_ref: TraitRef,
1108    #[map(*x == ty::PredicatePolarity::Positive)]
1109    #[from(polarity)]
1110    pub is_positive: bool,
1111}
1112
1113/// Reflects [`ty::OutlivesPredicate`] as a named struct
1114/// instead of a tuple struct. This is because the script converting
1115/// JSONSchema types to OCaml doesn't support tuple structs, and this
1116/// is the only tuple struct in the whole AST.
1117
1118#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1119pub struct OutlivesPredicate<T> {
1120    pub lhs: T,
1121    pub rhs: Region,
1122}
1123
1124impl<'tcx, S: UnderOwnerState<'tcx>, T, U> SInto<S, OutlivesPredicate<U>>
1125    for ty::OutlivesPredicate<'tcx, T>
1126where
1127    T: SInto<S, U>,
1128{
1129    fn sinto(&self, s: &S) -> OutlivesPredicate<U> where {
1130        OutlivesPredicate {
1131            lhs: self.0.sinto(s),
1132            rhs: self.1.sinto(s),
1133        }
1134    }
1135}
1136
1137/// Reflects [`ty::RegionOutlivesPredicate`]
1138pub type RegionOutlivesPredicate = OutlivesPredicate<Region>;
1139/// Reflects [`ty::TypeOutlivesPredicate`]
1140pub type TypeOutlivesPredicate = OutlivesPredicate<Ty>;
1141
1142/// Reflects [`ty::Term`]
1143
1144#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1145pub enum Term {
1146    Ty(Ty),
1147    Const(ConstantExpr),
1148}
1149
1150impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Term> for ty::Term<'tcx> {
1151    fn sinto(&self, s: &S) -> Term {
1152        use ty::TermKind;
1153        match self.kind() {
1154            TermKind::Ty(ty) => Term::Ty(ty.sinto(s)),
1155            TermKind::Const(c) => Term::Const(c.sinto(s)),
1156        }
1157    }
1158}
1159
1160/// Expresses a constraints over an associated type.
1161///
1162/// For instance:
1163/// ```text
1164/// fn f<T : Foo<S = String>>(...)
1165///              ^^^^^^^^^^
1166/// ```
1167/// (provided the trait `Foo` has an associated type `S`).
1168
1169#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1170pub struct ProjectionPredicate {
1171    /// The `impl Trait for Ty` in `Ty: Trait<..., Type = U>`.
1172    pub trait_proof: TraitProof,
1173    /// The `Type` in `Ty: Trait<..., Type = U>`.
1174    pub assoc_item: AssocItem,
1175    /// The type `U` in `Ty: Trait<..., Type = U>`.
1176    pub ty: Ty,
1177}
1178
1179impl<'tcx, S: UnderBinderState<'tcx>> SInto<S, ProjectionPredicate>
1180    for ty::ProjectionPredicate<'tcx>
1181{
1182    fn sinto(&self, s: &S) -> ProjectionPredicate {
1183        let tcx = s.base().tcx;
1184        let alias_ty = &self.projection_term.expect_ty(tcx);
1185        let poly_trait_ref = s.binder().rebind(alias_ty.trait_ref(tcx));
1186        let Term::Ty(ty) = self.term.sinto(s) else {
1187            unreachable!()
1188        };
1189        let item = tcx.associated_item(alias_ty.kind.def_id());
1190        ProjectionPredicate {
1191            trait_proof: solve_trait(s, poly_trait_ref),
1192            assoc_item: AssocItem::sfrom(s, &item),
1193            ty,
1194        }
1195    }
1196}
1197
1198/// Reflects [`ty::ClauseKind`]
1199#[derive(AdtInto)]
1200#[args(<'tcx, S: UnderBinderState<'tcx>>, from: ty::ClauseKind<'tcx>, state: S as tcx)]
1201#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1202pub enum ClauseKind {
1203    Trait(TraitPredicate),
1204    RegionOutlives(RegionOutlivesPredicate),
1205    TypeOutlives(TypeOutlivesPredicate),
1206    Projection(ProjectionPredicate),
1207    ConstArgHasType(ConstantExpr, Ty),
1208    WellFormed(Term),
1209    ConstEvaluatable(ConstantExpr),
1210    HostEffect(HostEffectPredicate),
1211    UnstableFeature(Symbol),
1212}
1213
1214sinto_todo!(rustc_middle::ty, HostEffectPredicate<'tcx>);
1215
1216/// Reflects [`ty::Clause`] and adds a hash-consed predicate identifier.
1217
1218#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1219pub struct Clause {
1220    pub kind: Binder<ClauseKind>,
1221}
1222
1223impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for ty::Clause<'tcx> {
1224    fn sinto(&self, s: &S) -> Clause {
1225        let kind = self.kind().sinto(s);
1226        Clause { kind }
1227    }
1228}
1229
1230impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for ty::PolyTraitPredicate<'tcx> {
1231    fn sinto(&self, s: &S) -> Clause {
1232        let kind: Binder<_> = self.sinto(s);
1233        let kind: Binder<ClauseKind> = kind.map(ClauseKind::Trait);
1234        Clause { kind }
1235    }
1236}
1237
1238/// Reflects [`ty::Predicate`] and adds a hash-consed predicate identifier.
1239
1240#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1241pub struct Predicate {
1242    pub kind: Binder<PredicateKind>,
1243}
1244
1245impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Predicate> for ty::Predicate<'tcx> {
1246    fn sinto(&self, s: &S) -> Predicate {
1247        let kind = self.kind().sinto(s);
1248        Predicate { kind }
1249    }
1250}
1251
1252/// Reflects [`ty::BoundVariableKind`]
1253#[derive(AdtInto)]
1254#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundVariableKind<'tcx>, state: S as tcx)]
1255#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1256pub enum BoundVariableKind {
1257    Ty(BoundTyKind),
1258    Region(BoundRegionKind),
1259    Const,
1260}
1261
1262/// Reflects [`ty::Binder`]
1263
1264#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1265pub struct Binder<T> {
1266    pub value: T,
1267    pub bound_vars: Vec<BoundVariableKind>,
1268}
1269
1270impl Binder<()> {
1271    pub fn empty() -> Self {
1272        Binder {
1273            value: (),
1274            bound_vars: vec![],
1275        }
1276    }
1277}
1278
1279impl<T> Binder<T> {
1280    pub fn as_ref(&self) -> Binder<&T> {
1281        Binder {
1282            value: &self.value,
1283            bound_vars: self.bound_vars.clone(),
1284        }
1285    }
1286
1287    pub fn hax_skip_binder(self) -> T {
1288        self.value
1289    }
1290
1291    pub fn hax_skip_binder_ref(&self) -> &T {
1292        &self.value
1293    }
1294
1295    pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Binder<U> {
1296        Binder {
1297            value: f(self.value),
1298            bound_vars: self.bound_vars,
1299        }
1300    }
1301
1302    pub fn inner_mut(&mut self) -> &mut T {
1303        &mut self.value
1304    }
1305
1306    pub fn rebind<U>(&self, value: U) -> Binder<U> {
1307        self.as_ref().map(|_| value)
1308    }
1309}
1310
1311/// Uniquely identifies a predicate.
1312#[derive(AdtInto)]
1313#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: traits::ItemPredicateId<DefId>, state: S as s)]
1314#[derive(Debug, Clone, Hash, PartialEq, Eq)]
1315pub enum GenericPredicateId {
1316    /// A predicate that counts as "input" for an item, e.g. `where` clauses on a function or impl.
1317    /// Numbered in some arbitrary but consistent order.
1318    Required(DefId, u32),
1319    /// A predicate that counts as "output" of an item, e.g. supertrait clauses in a trait. Note
1320    /// that we count `where` clauses on a trait as implied.
1321    /// Numbered in some arbitrary but consistent order.
1322    Implied(DefId, u32),
1323    /// Predicate inside a non-item binder, e.g. within a `dyn Trait`.
1324    /// Numbered in some arbitrary but consistent order.
1325    Unmapped(u32),
1326    /// The special `Self: Trait` clause available within trait `Trait`.
1327    TraitSelf,
1328}
1329
1330#[derive(AdtInto)]
1331#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: traits::ItemPredicate<'tcx, DefId>, state: S as s)]
1332#[derive(Debug, Clone, Hash, PartialEq, Eq)]
1333pub struct GenericPredicate {
1334    pub id: GenericPredicateId,
1335    pub clause: Clause,
1336    pub span: Span,
1337}
1338
1339/// Reflects [`ty::GenericPredicates`]
1340#[derive(AdtInto)]
1341#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: traits::ItemPredicates<'tcx, DefId>, state: S as s)]
1342#[derive(Clone, Debug, Default, Hash, PartialEq, Eq)]
1343pub struct GenericPredicates {
1344    pub predicates: Vec<GenericPredicate>,
1345}
1346
1347impl GenericPredicates {
1348    pub fn iter(&self) -> impl Iterator<Item = &GenericPredicate> {
1349        self.predicates.iter()
1350    }
1351    /// Iter only on trait clauses.
1352    pub fn iter_trait_clauses(&self) -> impl Iterator<Item = &GenericPredicate> {
1353        self.iter()
1354            .filter(|pred| matches!(pred.clause.kind.hax_skip_binder_ref(), ClauseKind::Trait(_)))
1355    }
1356}
1357
1358impl<'tcx, S: UnderOwnerState<'tcx>, T1, T2> SInto<S, Binder<T2>> for ty::Binder<'tcx, T1>
1359where
1360    T1: SInto<StateWithBinder<'tcx>, T2>,
1361{
1362    fn sinto(&self, s: &S) -> Binder<T2> {
1363        let bound_vars = self.bound_vars().sinto(s);
1364        let value = {
1365            let under_binder_s = &s.with_binder(self.as_ref().map_bound(|_| ()));
1366            self.as_ref().skip_binder().sinto(under_binder_s)
1367        };
1368        Binder { value, bound_vars }
1369    }
1370}
1371
1372/// Reflects [`ty::SubtypePredicate`]
1373#[derive(AdtInto)]
1374#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::SubtypePredicate<'tcx>, state: S as tcx)]
1375#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1376pub struct SubtypePredicate {
1377    pub a_is_expected: bool,
1378    pub a: Ty,
1379    pub b: Ty,
1380}
1381
1382/// Reflects [`ty::CoercePredicate`]
1383#[derive(AdtInto)]
1384#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::CoercePredicate<'tcx>, state: S as tcx)]
1385#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1386pub struct CoercePredicate {
1387    pub a: Ty,
1388    pub b: Ty,
1389}
1390
1391/// Reflects [`ty::AliasRelationDirection`]
1392#[derive(AdtInto)]
1393#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::AliasRelationDirection, state: S as _tcx)]
1394#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1395pub enum AliasRelationDirection {
1396    Equate,
1397    Subtype,
1398}
1399
1400/// Reflects [`ty::ClosureArgs`]
1401#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1402
1403pub struct ClosureArgs {
1404    pub item: ItemRef,
1405    /// The base kind of this closure. The kinds are ordered by inclusion: any `Fn` works as an
1406    /// `FnMut`, and any `FnMut` works as an `FnOnce`.
1407    pub kind: ClosureKind,
1408    /// The signature of the function that the closure implements, e.g. `fn(A, B, C) -> D`.
1409    pub fn_sig: PolyFnSig,
1410    /// The set of captured variables. Together they form the state of the closure.
1411    pub upvar_tys: Vec<Ty>,
1412}
1413
1414impl ClosureArgs {
1415    /// Iterate over the upvars that are borrows with erased regions. These may require allocating
1416    /// fresh regions.
1417    pub fn iter_upvar_borrows(&self) -> impl Iterator<Item = &Ty> {
1418        self.upvar_tys.iter().filter(|ty| {
1419            matches!(
1420                ty.kind(),
1421                TyKind::Ref(
1422                    Region {
1423                        kind: RegionKind::ReErased
1424                    },
1425                    ..
1426                )
1427            )
1428        })
1429    }
1430}
1431
1432impl ClosureArgs {
1433    // Manual implementation because we need the `def_id` of the closure.
1434    pub fn sfrom<'tcx, S>(s: &S, def_id: RDefId, from: ty::GenericArgsRef<'tcx>) -> Self
1435    where
1436        S: UnderOwnerState<'tcx>,
1437    {
1438        use rustc_middle::ty;
1439        use rustc_type_ir::TypeFoldable;
1440        use rustc_type_ir::TypeSuperFoldable;
1441
1442        struct RegionUnEraserVisitor<'tcx> {
1443            tcx: ty::TyCtxt<'tcx>,
1444            depth: u32,
1445            bound_vars: Vec<ty::BoundVariableKind<'tcx>>,
1446        }
1447
1448        impl<'tcx> ty::TypeFolder<ty::TyCtxt<'tcx>> for RegionUnEraserVisitor<'tcx> {
1449            fn cx(&self) -> ty::TyCtxt<'tcx> {
1450                self.tcx
1451            }
1452
1453            fn fold_ty(&mut self, ty: ty::Ty<'tcx>) -> ty::Ty<'tcx> {
1454                ty.super_fold_with(self)
1455            }
1456
1457            fn fold_binder<T>(&mut self, t: ty::Binder<'tcx, T>) -> ty::Binder<'tcx, T>
1458            where
1459                T: ty::TypeFoldable<ty::TyCtxt<'tcx>>,
1460            {
1461                self.depth += 1;
1462                let t = t.super_fold_with(self);
1463                self.depth -= 1;
1464                t
1465            }
1466
1467            fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
1468                // Replace erased regions with fresh bound regions.
1469                if r.is_erased() {
1470                    let bound_region = ty::BoundRegion {
1471                        var: ty::BoundVar::from_usize(self.bound_vars.len()),
1472                        kind: ty::BoundRegionKind::Anon,
1473                    };
1474                    self.bound_vars
1475                        .push(ty::BoundVariableKind::Region(bound_region.kind));
1476                    ty::Region::new_bound(
1477                        self.tcx,
1478                        ty::DebruijnIndex::from(self.depth),
1479                        bound_region,
1480                    )
1481                } else {
1482                    r
1483                }
1484            }
1485        }
1486
1487        let tcx = s.base().tcx;
1488        let closure = from.as_closure();
1489        let item = {
1490            // The closure has no generics of its own: it inherits its parent generics and could
1491            // have late-bound args but these are part of the signature.
1492            let parent_args = tcx.mk_args(closure.parent_args());
1493            translate_item_ref(s, def_id, parent_args)
1494        };
1495        let sig = closure.sig();
1496        let sig = tcx.signature_unclosure(sig, rustc_hir::Safety::Safe);
1497        // Add bound variables for each erased region in the signature.
1498        let sig = {
1499            let mut visitor = RegionUnEraserVisitor {
1500                tcx,
1501                depth: 0,
1502                bound_vars: sig.bound_vars().iter().collect(),
1503            };
1504            let unbound_sig = sig.skip_binder().fold_with(&mut visitor);
1505            let bound_vars = tcx.mk_bound_variable_kinds(&visitor.bound_vars);
1506            ty::Binder::bind_with_vars(unbound_sig, bound_vars)
1507        };
1508        ClosureArgs {
1509            item,
1510            kind: closure.kind().sinto(s),
1511            fn_sig: sig.sinto(s),
1512            upvar_tys: closure.upvar_tys().sinto(s),
1513        }
1514    }
1515}
1516
1517/// Reflects [`ty::ClosureKind`]
1518#[derive(AdtInto)]
1519#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::ClosureKind, state: S as _tcx)]
1520#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1521pub enum ClosureKind {
1522    Fn,
1523    FnMut,
1524    FnOnce,
1525}
1526
1527sinto_todo!(rustc_middle::ty, NormalizesTo<'tcx>);
1528
1529/// Reflects [`ty::PredicateKind`]
1530#[derive(AdtInto)]
1531#[args(<'tcx, S: UnderBinderState<'tcx>>, from: ty::PredicateKind<'tcx>, state: S as tcx)]
1532#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1533pub enum PredicateKind {
1534    Clause(ClauseKind),
1535    DynCompatible(DefId),
1536    Subtype(SubtypePredicate),
1537    Coerce(CoercePredicate),
1538    ConstEquate(ConstantExpr, ConstantExpr),
1539    Ambiguous,
1540    AliasRelate(Term, Term, AliasRelationDirection),
1541    NormalizesTo(NormalizesTo),
1542}
1543
1544/// Reflects [`ty::AssocItem`]
1545
1546#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1547pub struct AssocItem {
1548    pub def_id: DefId,
1549    /// This is `None` for RPTITs.
1550    pub name: Option<Symbol>,
1551    pub kind: AssocKind,
1552    pub container: AssocItemContainer,
1553    /// Whether this item has a value (e.g. this is `false` for trait methods without default
1554    /// implementations).
1555    pub has_value: bool,
1556}
1557
1558impl AssocItem {
1559    pub fn sfrom<'tcx, S: BaseState<'tcx>>(s: &S, item: &ty::AssocItem) -> AssocItem {
1560        Self::sfrom_instantiated(s, item, None)
1561    }
1562
1563    /// Translate an `AssocItem` and optionally instantiate it with the provided arguments.
1564    pub fn sfrom_instantiated<'tcx, S: BaseState<'tcx>>(
1565        s: &S,
1566        item: &ty::AssocItem,
1567        item_args: Option<ty::GenericArgsRef<'tcx>>,
1568    ) -> AssocItem {
1569        let tcx = s.base().tcx;
1570        // We want to solve traits in the context of this item.
1571        let item_def_id = item.def_id.sinto(s);
1572        let s = &s.with_hax_owner(&item_def_id);
1573        let item_args = item_args.unwrap_or_else(|| item_def_id.identity_args(s));
1574        let container_id = item.container_id(tcx);
1575        let container_args = item_args.truncate_to(tcx, tcx.generics_of(container_id));
1576        let container = match item.container {
1577            ty::AssocContainer::Trait => {
1578                let trait_ref =
1579                    ty::TraitRef::new_from_args(tcx, container_id, container_args).sinto(s);
1580                AssocItemContainer::TraitContainer { trait_ref }
1581            }
1582            ty::AssocContainer::TraitImpl(implemented_item_id) => {
1583                let implemented_item_id = implemented_item_id.unwrap();
1584                let item = translate_item_ref(s, container_id, container_args);
1585                let implemented_trait_ref = tcx
1586                    .impl_trait_ref(container_id)
1587                    .instantiate(tcx, container_args);
1588                let implemented_trait_ref = normalize(tcx, s.typing_env(), implemented_trait_ref);
1589                let implemented_trait_item = {
1590                    let implemented_item_id = implemented_item_id.sinto(s);
1591                    let generics =
1592                        item_args.rebase_onto(tcx, container_id, implemented_trait_ref.args);
1593                    // Don't resolve, otherwise we'll always get the impl item id back.
1594                    ItemRef::translate_from_hax_def_id_maybe_resolve(
1595                        s,
1596                        implemented_item_id,
1597                        generics,
1598                        AssocItemResolution::None,
1599                    )
1600                };
1601                AssocItemContainer::TraitImplContainer {
1602                    impl_: item,
1603                    implemented_trait_ref: implemented_trait_ref.sinto(s),
1604                    implemented_trait_item,
1605                    overrides_default: tcx.defaultness(implemented_item_id).has_value(),
1606                }
1607            }
1608            ty::AssocContainer::InherentImpl => AssocItemContainer::InherentImplContainer {
1609                impl_id: container_id.sinto(s),
1610            },
1611        };
1612        let name = match item.opt_name() {
1613            None if let ty::AssocKind::Type { data } = item.kind
1614                && let ty::AssocTypeData::Rpitit(rpitit) = data =>
1615            {
1616                let (ty::ImplTraitInTraitData::Trait { fn_def_id, .. }
1617                | ty::ImplTraitInTraitData::Impl { fn_def_id, .. }) = rpitit;
1618                let fn_name = tcx.item_name(fn_def_id);
1619                let name = Symbol::intern(&format!("{fn_name}_ty"));
1620                Some(name)
1621            }
1622            opt_name => opt_name,
1623        };
1624        AssocItem {
1625            def_id: item.def_id.sinto(s),
1626            name,
1627            kind: item.kind.sinto(s),
1628            container,
1629            has_value: item.defaultness(tcx).has_value(),
1630        }
1631    }
1632
1633    /// The `DefId` of the item being implemented.
1634    pub fn implemented_trait_item_id(&self) -> &DefId {
1635        match &self.container {
1636            AssocItemContainer::TraitImplContainer {
1637                implemented_trait_item,
1638                ..
1639            } => &implemented_trait_item.def_id,
1640            _ => &self.def_id,
1641        }
1642    }
1643}
1644
1645/// Reflects [`ty::AssocKind`]
1646#[derive(AdtInto)]
1647#[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocKind, state: S as _tcx)]
1648#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1649pub enum AssocKind {
1650    Const { name: Symbol },
1651    Fn { name: Symbol, has_self: bool },
1652    Type { data: AssocTypeData },
1653}
1654
1655/// Reflects [`ty::AssocTypeData`]
1656#[derive(AdtInto)]
1657#[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocTypeData, state: S as _tcx)]
1658#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1659pub enum AssocTypeData {
1660    Normal(Symbol),
1661    Rpitit(ImplTraitInTraitData),
1662}
1663
1664#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1665pub enum AssocItemContainer {
1666    TraitContainer {
1667        trait_ref: TraitRef,
1668    },
1669    TraitImplContainer {
1670        /// Reference to the def_id of the impl block.
1671        impl_: ItemRef,
1672        /// The trait ref implemented by the impl block.
1673        implemented_trait_ref: TraitRef,
1674        /// The the associated item (in the trait declaration) that is being implemented.
1675        implemented_trait_item: ItemRef,
1676        /// Whether the corresponding trait item had a default (and therefore this one overrides
1677        /// it).
1678        overrides_default: bool,
1679    },
1680    InherentImplContainer {
1681        impl_id: DefId,
1682    },
1683}
1684
1685/// Reflects [`ty::ImplTraitInTraitData`]
1686#[derive(AdtInto)]
1687#[args(<'tcx, S: BaseState<'tcx>>, from: ty::ImplTraitInTraitData, state: S as _s)]
1688#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1689pub enum ImplTraitInTraitData {
1690    Trait {
1691        fn_def_id: DefId,
1692        opaque_def_id: DefId,
1693    },
1694    Impl {
1695        fn_def_id: DefId,
1696    },
1697}
charon_driver/hax/types/ty.rs

charon_driver/hax/types/
ty.rs
