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

charon_driver/hax/types/
ty.rs
