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

charon_driver/hax/types/
ty.rs
