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: Box<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 rustc_hir::def::DefKind::*;
567        let tcx = s.base().tcx;
568        let parent = tcx.parent(self.def_id);
569        match tcx.def_kind(parent) {
570            Fn | AssocFn | Enum | Struct | Union | Ctor(..) | OpaqueTy => {
571                tcx.variances_of(parent).get(self.index as usize).sinto(s)
572            }
573            _ => None
574        }
575    })]
576    pub variance: Option<Variance>,
577}
578
579/// Reflects [`ty::GenericParamDefKind`]
580
581#[derive(Clone, Debug)]
582pub enum GenericParamDefKind {
583    Lifetime,
584    Type { has_default: bool, synthetic: bool },
585    Const { has_default: bool, ty: Ty },
586}
587
588/// Reflects [`ty::Generics`]
589#[derive(AdtInto)]
590#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::Generics, state: S as state)]
591#[derive(Clone, Debug)]
592pub struct TyGenerics {
593    pub parent: Option<DefId>,
594    pub parent_count: usize,
595    #[from(own_params)]
596    pub params: Vec<GenericParamDef>,
597    // pub param_def_id_to_index: FxHashMap<DefId, u32>,
598    pub has_self: bool,
599    pub has_late_bound_regions: Option<Span>,
600}
601
602/// This type merges the information from
603/// [`ty::AliasTyKind`] and [`ty::AliasTy`].
604#[derive(Clone, Debug, Hash, PartialEq, Eq)]
605pub struct Alias {
606    pub kind: AliasKind,
607    pub args: Vec<GenericArg>,
608    pub def_id: DefId,
609}
610
611/// Reflects [`rustc_middle::ty::AliasTyKind`].
612#[derive(Clone, Debug, Hash, PartialEq, Eq)]
613pub enum AliasKind {
614    /// The projection of a trait type: `<Ty as Trait<...>>::Type<...>`
615    Projection(ItemRef),
616    /// An associated type in an inherent impl.
617    Inherent,
618    /// An `impl Trait` opaque type.
619    Opaque {
620        /// The real type hidden inside this opaque type.
621        hidden_ty: Ty,
622    },
623    /// A type alias that references opaque types. Likely to always be normalized away.
624    Free,
625}
626
627pub fn alias_ty_kind_def_id<'tcx>(kind: ty::AliasTyKind<'tcx>) -> RDefId {
628    match kind {
629        ty::AliasTyKind::Projection { def_id }
630        | ty::AliasTyKind::Inherent { def_id }
631        | ty::AliasTyKind::Opaque { def_id }
632        | ty::AliasTyKind::Free { def_id } => def_id,
633    }
634}
635
636impl Alias {
637    #[tracing::instrument(level = "trace", skip(s))]
638    fn from<'tcx, S: UnderOwnerState<'tcx>>(s: &S, alias_ty: &ty::AliasTy<'tcx>) -> TyKind {
639        let tcx = s.base().tcx;
640        let typing_env = s.typing_env();
641        use rustc_type_ir::AliasTyKind as RustAliasKind;
642
643        // Try to normalize the alias first.
644        let ty = ty::Ty::new_alias(tcx, ty::IsRigid::No, *alias_ty);
645        let ty = normalize(tcx, typing_env, ty::Unnormalized::new(ty));
646        let ty::Alias(_is_rigid, alias_ty) = ty.kind() else {
647            let ty: Ty = ty.sinto(s);
648            return ty.kind().clone();
649        };
650
651        let kind = match alias_ty.kind {
652            RustAliasKind::Projection { def_id } => {
653                AliasKind::Projection(ItemRef::translate_projection(s, def_id, alias_ty.args))
654            }
655            RustAliasKind::Inherent { .. } => AliasKind::Inherent,
656            RustAliasKind::Opaque { def_id } => {
657                // Reveal the underlying `impl Trait` type.
658                let ty = tcx.type_of(def_id).instantiate(tcx, alias_ty.args);
659                let ty = normalize(tcx, s.typing_env(), ty);
660                AliasKind::Opaque {
661                    hidden_ty: ty.sinto(s),
662                }
663            }
664            RustAliasKind::Free { .. } => AliasKind::Free,
665        };
666        TyKind::Alias(Alias {
667            kind,
668            args: alias_ty.args.sinto(s),
669            def_id: alias_ty_kind_def_id(alias_ty.kind).sinto(s),
670        })
671    }
672}
673
674impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Box<Ty>> for ty::Ty<'tcx> {
675    fn sinto(&self, s: &S) -> Box<Ty> {
676        Box::new(self.sinto(s))
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    Str,
779    RawPtr(Box<Ty>, Mutability),
780    Ref(Region, Box<Ty>, Mutability),
781    #[custom_arm(FROM_TYPE::Dynamic(preds, region) => TyKind::Dynamic(resolve_for_dyn(s, preds, |_, _| ()), region.sinto(s)),)]
782    Dynamic(DynBinder<()>, Region),
783    #[custom_arm(FROM_TYPE::Coroutine(def_id, generics) => TO_TYPE::Coroutine(translate_item_ref(s, *def_id, generics)),)]
784    Coroutine(ItemRef),
785    Never,
786    #[custom_arm(FROM_TYPE::Alias(_is_rigid, alias_ty) => Alias::from(s, alias_ty),)]
787    Alias(Alias),
788    Param(ParamTy),
789    Bound(BoundVarIndexKind, BoundTy),
790    Placeholder(PlaceholderType),
791    Infer(InferTy),
792    #[custom_arm(FROM_TYPE::Error(..) => TO_TYPE::Error,)]
793    Error,
794    #[todo]
795    Todo(String),
796}
797
798/// A representation of `exists<T: Trait1 + Trait2>(value)`: we create a fresh type id and the
799/// appropriate trait clauses. The contained value may refer to the fresh ty and the in-scope trait
800/// clauses. This is used to represent types related to `dyn Trait`.
801
802#[derive(Clone, Debug, Hash, PartialEq, Eq)]
803pub struct DynBinder<T> {
804    /// Fresh type parameter that we use as the `Self` type in the prediates below.
805    pub existential_ty: ParamTy,
806    /// Clauses that define the trait object. These clauses use the fresh type parameter above
807    /// as `Self` type.
808    pub predicates: GenericPredicates,
809    /// The value inside the binder.
810    pub val: T,
811}
812
813/// Do trait resolution in the context of the clauses of a `dyn Trait` type.
814fn resolve_for_dyn<'tcx, S: UnderOwnerState<'tcx>, R>(
815    s: &S,
816    // The predicates in the context.
817    epreds: &'tcx ty::List<ty::Binder<'tcx, ty::ExistentialPredicate<'tcx>>>,
818    f: impl FnOnce(&mut PredicateSearcher<'tcx>, ty::Ty<'tcx>) -> R,
819) -> DynBinder<R> {
820    fn searcher_for_traits<'tcx, S: UnderOwnerState<'tcx>>(
821        s: &S,
822        preds: &ItemPredicates<'tcx, DefId>,
823    ) -> PredicateSearcher<'tcx> {
824        let tcx = s.base().tcx;
825        // Populate a predicate searcher that knows about the `dyn` clauses.
826        let mut predicate_searcher = s.with_predicate_searcher(|ps, _| ps.clone());
827        predicate_searcher.insert_bound_predicates(&s.base_state(), preds.iter());
828        predicate_searcher.set_param_env(param_env_from_clauses(
829            tcx,
830            s.param_env()
831                .caller_bounds()
832                .iter()
833                .chain(preds.iter().map(|pred| pred.clause)),
834        ));
835        predicate_searcher
836    }
837
838    fn fresh_param_ty<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> ty::ParamTy {
839        let generics = s.owner().generics_of(s);
840        let param_count = generics.count();
841        ty::ParamTy::new(param_count as u32 + 1, rustc_span::Symbol::intern("_dyn"))
842    }
843
844    let tcx = s.base().tcx;
845    let span = rustc_span::DUMMY_SP.sinto(s);
846
847    // Pretend there's an extra type in the environment.
848    let new_param_ty = fresh_param_ty(s);
849    let new_ty = new_param_ty.to_ty(tcx);
850
851    // Set the new type as the `Self` parameter of our predicates.
852    let predicates = epreds.iter().map(|epred| epred.with_self_ty(tcx, new_ty));
853    let predicates: ItemPredicates<'_, DefId> = ItemPredicates::new_unmapped(span, predicates);
854
855    // Populate a predicate searcher that knows about the `dyn` clauses.
856    let mut predicate_searcher = searcher_for_traits(s, &predicates);
857    let val = f(&mut predicate_searcher, new_ty);
858
859    // Using the predicate searcher, translate the predicates. Only the projection predicates need
860    // to be handled specially.
861    let predicates = predicates
862        .iter()
863        .map(|pred| {
864            match pred.clause.as_projection_clause() {
865                // Translate normally
866                None => pred.sinto(s),
867                // Translate by hand using our predicate searcher. This does the same as
868                // `clause.sinto(s)` except that it uses our predicate searcher to resolve the
869                // projection `TraitProof`.
870                Some(proj) => {
871                    let bound_vars = proj.bound_vars().sinto(s);
872                    let proj = {
873                        let alias_ty = &proj.skip_binder().projection_term.expect_ty();
874                        let trait_proof = {
875                            let poly_trait_ref = proj.rebind(alias_ty.trait_ref(tcx));
876                            predicate_searcher
877                                .resolve(&s.base_state(), &poly_trait_ref)
878                                .sinto(s)
879                        };
880                        let Term::Ty(ty) = proj.skip_binder().term.sinto(s) else {
881                            unreachable!()
882                        };
883                        let item = tcx.associated_item(alias_ty_kind_def_id(alias_ty.kind));
884                        ProjectionPredicate {
885                            trait_proof,
886                            assoc_item: AssocItem::sfrom(s, &item),
887                            ty,
888                        }
889                    };
890                    let kind = Binder {
891                        value: ClauseKind::Projection(proj),
892                        bound_vars,
893                    };
894                    let clause = Clause { kind };
895                    GenericPredicate {
896                        id: pred.id.sinto(s),
897                        clause,
898                        span,
899                    }
900                }
901            }
902        })
903        .collect();
904
905    let predicates = GenericPredicates { predicates };
906    DynBinder {
907        existential_ty: new_param_ty.sinto(s),
908        predicates,
909        val,
910    }
911}
912
913#[derive(AdtInto)]
914#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::pattern::PatternKind<'tcx>, state: S as gstate)]
915#[derive(Clone, Debug, Hash, PartialEq, Eq)]
916pub enum Pattern {
917    Range {
918        start: ConstantExpr,
919        end: ConstantExpr,
920    },
921    Or(Vec<Pattern>),
922    NotNull,
923}
924
925impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Pattern> for ty::Pattern<'tcx> {
926    fn sinto(&self, s: &S) -> Pattern {
927        self.kind().sinto(s)
928    }
929}
930/// Reflects [`ty::CanonicalUserTypeAnnotation`]
931#[derive(AdtInto)]
932#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::CanonicalUserTypeAnnotation<'tcx>, state: S as gstate)]
933#[derive(Clone, Debug)]
934pub struct CanonicalUserTypeAnnotation {
935    pub user_ty: CanonicalUserType,
936    pub span: Span,
937    pub inferred_ty: Ty,
938}
939
940/// Reflects [`ty::AdtKind`]
941
942#[derive(Copy, Clone, Debug)]
943pub enum AdtKind {
944    Struct,
945    Union,
946    Enum,
947    /// We sometimes pretend arrays are an ADT and generate a `FullDef` for them.
948    Array,
949    /// We sometimes pretend slices are an ADT and generate a `FullDef` for them.
950    Slice,
951    /// We sometimes pretend tuples are an ADT and generate a `FullDef` for them.
952    Tuple,
953}
954
955impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, AdtKind> for ty::AdtKind {
956    fn sinto(&self, _s: &S) -> AdtKind {
957        match self {
958            ty::AdtKind::Struct => AdtKind::Struct,
959            ty::AdtKind::Union => AdtKind::Union,
960            ty::AdtKind::Enum => AdtKind::Enum,
961        }
962    }
963}
964
965sinto_todo!(rustc_middle::ty, AdtFlags);
966
967/// Reflects [`rustc_abi::ReprOptions`].
968
969#[derive(AdtInto, Clone, Debug)]
970#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_abi::ReprOptions, state: S as s)]
971pub struct ReprOptions {
972    /// Whether an explicit integer representation was specified.
973    #[value(self.int.is_some())]
974    pub int_specified: bool,
975    /// The actual discriminant type resulting from the representation options.
976    #[value({
977        use rustc_middle::ty::util::IntTypeExt;
978        self.discr_type().to_ty(s.base().tcx).sinto(s)
979    })]
980    pub typ: Ty,
981    pub align: Option<Align>,
982    pub pack: Option<Align>,
983    #[value(ReprFlags { is_c: self.c(), is_transparent: self.transparent(), is_simd: self.simd() })]
984    pub flags: ReprFlags,
985}
986
987/// The representation flags without the ones irrelevant outside of rustc.
988
989#[derive(Default, Clone, Debug)]
990pub struct ReprFlags {
991    pub is_c: bool,
992    pub is_transparent: bool,
993    pub is_simd: bool,
994}
995
996/// Reflects [`rustc_abi::Align`], but directly stores the number of bytes as a u64.
997
998#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
999#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_abi::Align, state: S as _s)]
1000pub struct Align {
1001    #[value({
1002        self.bytes()
1003    })]
1004    pub bytes: u64,
1005}
1006
1007/// The metadata to attach to the newly-unsized ptr.
1008#[derive(Clone, Debug)]
1009pub enum UnsizingMetadata {
1010    /// Unsize an array to a slice, storing the length as metadata.
1011    Length(ConstantExpr),
1012    /// Unsize a non-dyn type to a dyn type, adding a vtable pointer as metadata.
1013    DirectVTable(TraitProof),
1014    /// Unsize a dyn-type to another dyn-type, (optionally) indexing within the current vtable.
1015    NestedVTable(DynBinder<TraitProof>),
1016    /// Couldn't compute
1017    Unknown,
1018}
1019
1020pub fn compute_unsizing_metadata<'tcx, S: UnderOwnerState<'tcx>>(
1021    s: &S,
1022    src_ty: ty::Ty<'tcx>,
1023    tgt_ty: ty::Ty<'tcx>,
1024) -> UnsizingMetadata {
1025    // TODO: to properly find out what field we want, we should use the query
1026    // `coerce_unsized_info`, which we call recursively to get the list of fields
1027    // to go into until we reach a pointer/reference.
1028    // We should also pass this list of field IDs in the unsizing metadata.
1029
1030    let (Some(src_ty), Some(tgt_ty)) = (src_ty.builtin_deref(true), tgt_ty.builtin_deref(true))
1031    else {
1032        return UnsizingMetadata::Unknown;
1033    };
1034
1035    let tcx = s.base().tcx;
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).sinto(s)
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::ClauseKind<'tcx> {}
1389impl<'tcx> BinderVariances<'tcx> for ty::PredicateKind<'tcx> {}
1390impl<'tcx> BinderVariances<'tcx> for ty::TraitRef<'tcx> {}
1391impl<'tcx> BinderVariances<'tcx> for ty::TraitPredicate<'tcx> {}
1392
1393impl<'tcx, S: UnderOwnerState<'tcx>, T1, T2> SInto<S, Binder<T2>> for ty::Binder<'tcx, T1>
1394where
1395    T1: SInto<StateWithBinder<'tcx>, T2> + BinderVariances<'tcx>,
1396{
1397    fn sinto(&self, s: &S) -> Binder<T2> {
1398        let variances = T1::variances(s.base().tcx, self);
1399        let mut bound_vars = self.bound_vars().sinto(s);
1400        for (index, var) in bound_vars.iter_mut().enumerate() {
1401            if let BoundVariableKind::Region(_, variance) = var {
1402                *variance = variances
1403                    .get(&ty::BoundVar::from_usize(index))
1404                    .copied()
1405                    .sinto(s);
1406            }
1407        }
1408        let value = {
1409            let under_binder_s = &s.with_binder(self.as_ref().map_bound(|_| ()));
1410            self.as_ref().skip_binder().sinto(under_binder_s)
1411        };
1412        Binder { value, bound_vars }
1413    }
1414}
1415
1416/// Reflects [`ty::SubtypePredicate`]
1417#[derive(AdtInto)]
1418#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::SubtypePredicate<'tcx>, state: S as tcx)]
1419#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1420pub struct SubtypePredicate {
1421    pub a_is_expected: bool,
1422    pub a: Ty,
1423    pub b: Ty,
1424}
1425
1426/// Reflects [`ty::CoercePredicate`]
1427#[derive(AdtInto)]
1428#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::CoercePredicate<'tcx>, state: S as tcx)]
1429#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1430pub struct CoercePredicate {
1431    pub a: Ty,
1432    pub b: Ty,
1433}
1434
1435/// Reflects [`ty::ClosureArgs`]
1436#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1437
1438pub struct ClosureArgs {
1439    pub item: ItemRef,
1440    /// The base kind of this closure. The kinds are ordered by inclusion: any `Fn` works as an
1441    /// `FnMut`, and any `FnMut` works as an `FnOnce`.
1442    pub kind: ClosureKind,
1443    /// The signature of the function that the closure implements, e.g. `fn(A, B, C) -> D`.
1444    pub fn_sig: PolyFnSig,
1445    /// The set of captured variables. Together they form the state of the closure.
1446    pub upvar_tys: Vec<Ty>,
1447}
1448
1449impl ClosureArgs {
1450    /// Iterate over the upvars that are borrows with erased regions. These may require allocating
1451    /// fresh regions.
1452    pub fn iter_upvar_borrows(&self) -> impl Iterator<Item = &Ty> {
1453        self.upvar_tys.iter().filter(|ty| {
1454            matches!(
1455                ty.kind(),
1456                TyKind::Ref(
1457                    Region {
1458                        kind: RegionKind::ReErased
1459                    },
1460                    ..
1461                )
1462            )
1463        })
1464    }
1465}
1466
1467impl ClosureArgs {
1468    // Manual implementation because we need the `def_id` of the closure.
1469    pub fn sfrom<'tcx, S>(s: &S, def_id: RDefId, from: ty::GenericArgsRef<'tcx>) -> Self
1470    where
1471        S: UnderOwnerState<'tcx>,
1472    {
1473        use rustc_middle::ty;
1474        use rustc_type_ir::TypeFoldable;
1475        use rustc_type_ir::TypeSuperFoldable;
1476
1477        struct RegionUnEraserVisitor<'tcx> {
1478            tcx: ty::TyCtxt<'tcx>,
1479            depth: u32,
1480            bound_vars: Vec<ty::BoundVariableKind<'tcx>>,
1481        }
1482
1483        impl<'tcx> ty::TypeFolder<ty::TyCtxt<'tcx>> for RegionUnEraserVisitor<'tcx> {
1484            fn cx(&self) -> ty::TyCtxt<'tcx> {
1485                self.tcx
1486            }
1487
1488            fn fold_ty(&mut self, ty: ty::Ty<'tcx>) -> ty::Ty<'tcx> {
1489                ty.super_fold_with(self)
1490            }
1491
1492            fn fold_binder<T>(&mut self, t: ty::Binder<'tcx, T>) -> ty::Binder<'tcx, T>
1493            where
1494                T: ty::TypeFoldable<ty::TyCtxt<'tcx>>,
1495            {
1496                self.depth += 1;
1497                let t = t.super_fold_with(self);
1498                self.depth -= 1;
1499                t
1500            }
1501
1502            fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
1503                // Replace erased regions with fresh bound regions.
1504                if r.is_erased() {
1505                    let bound_region = ty::BoundRegion {
1506                        var: ty::BoundVar::from_usize(self.bound_vars.len()),
1507                        kind: ty::BoundRegionKind::Anon,
1508                    };
1509                    self.bound_vars
1510                        .push(ty::BoundVariableKind::Region(bound_region.kind));
1511                    ty::Region::new_bound(
1512                        self.tcx,
1513                        ty::DebruijnIndex::from(self.depth),
1514                        bound_region,
1515                    )
1516                } else {
1517                    r
1518                }
1519            }
1520        }
1521
1522        let tcx = s.base().tcx;
1523        let closure = from.as_closure();
1524        let item = {
1525            // The closure has no generics of its own: it inherits its parent generics and could
1526            // have late-bound args but these are part of the signature.
1527            let parent_args = tcx.mk_args(closure.parent_args());
1528            translate_item_ref(s, def_id, parent_args)
1529        };
1530        let sig = closure.sig();
1531        let sig = tcx.signature_unclosure(sig, rustc_hir::Safety::Safe);
1532        // Add bound variables for each erased region in the signature.
1533        let sig = {
1534            let mut visitor = RegionUnEraserVisitor {
1535                tcx,
1536                depth: 0,
1537                bound_vars: sig.bound_vars().iter().collect(),
1538            };
1539            let unbound_sig = sig.skip_binder().fold_with(&mut visitor);
1540            let bound_vars = tcx.mk_bound_variable_kinds(&visitor.bound_vars);
1541            ty::Binder::bind_with_vars(unbound_sig, bound_vars)
1542        };
1543        ClosureArgs {
1544            item,
1545            kind: closure.kind().sinto(s),
1546            fn_sig: sig.sinto(s),
1547            upvar_tys: closure.upvar_tys().sinto(s),
1548        }
1549    }
1550}
1551
1552/// Reflects [`ty::ClosureKind`]
1553#[derive(AdtInto)]
1554#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::ClosureKind, state: S as _tcx)]
1555#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1556pub enum ClosureKind {
1557    Fn,
1558    FnMut,
1559    FnOnce,
1560}
1561
1562sinto_todo!(rustc_middle::ty, NormalizesTo<'tcx>);
1563
1564/// Reflects [`ty::PredicateKind`]
1565#[derive(AdtInto)]
1566#[args(<'tcx, S: UnderBinderState<'tcx>>, from: ty::PredicateKind<'tcx>, state: S as tcx)]
1567#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1568pub enum PredicateKind {
1569    Clause(ClauseKind),
1570    DynCompatible(DefId),
1571    Subtype(SubtypePredicate),
1572    Coerce(CoercePredicate),
1573    ConstEquate(ConstantExpr, ConstantExpr),
1574    Ambiguous,
1575    NormalizesTo(NormalizesTo),
1576}
1577
1578/// Reflects [`ty::AssocItem`]
1579
1580#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1581pub struct AssocItem {
1582    pub def_id: DefId,
1583    /// This is `None` for RPTITs.
1584    pub name: Option<Symbol>,
1585    pub kind: AssocKind,
1586    pub container: AssocItemContainer,
1587    /// Whether this item has a value (e.g. this is `false` for trait methods without default
1588    /// implementations).
1589    pub has_value: bool,
1590}
1591
1592impl AssocItem {
1593    pub fn sfrom<'tcx, S: BaseState<'tcx>>(s: &S, item: &ty::AssocItem) -> AssocItem {
1594        Self::sfrom_instantiated(s, item, None)
1595    }
1596
1597    /// Translate an `AssocItem` and optionally instantiate it with the provided arguments.
1598    pub fn sfrom_instantiated<'tcx, S: BaseState<'tcx>>(
1599        s: &S,
1600        item: &ty::AssocItem,
1601        item_args: Option<ty::GenericArgsRef<'tcx>>,
1602    ) -> AssocItem {
1603        let tcx = s.base().tcx;
1604        // We want to solve traits in the context of this item.
1605        let item_def_id = item.def_id.sinto(s);
1606        let s = &s.with_hax_owner(&item_def_id);
1607        let item_args = item_args.unwrap_or_else(|| item_def_id.identity_args(s));
1608        let container_id = item.container_id(tcx);
1609        let container_args = item_args.truncate_to(tcx, tcx.generics_of(container_id));
1610        let container = match item.container {
1611            ty::AssocContainer::Trait => {
1612                let trait_ref =
1613                    ty::TraitRef::new_from_args(tcx, container_id, container_args).sinto(s);
1614                AssocItemContainer::TraitContainer { trait_ref }
1615            }
1616            ty::AssocContainer::TraitImpl(implemented_item_id) => {
1617                let implemented_item_id = implemented_item_id.unwrap();
1618                let item = translate_item_ref(s, container_id, container_args);
1619                let implemented_trait_ref = tcx
1620                    .impl_trait_ref(container_id)
1621                    .instantiate(tcx, container_args);
1622                let implemented_trait_ref = normalize(tcx, s.typing_env(), implemented_trait_ref);
1623                let implemented_trait_item = {
1624                    let implemented_item_id = implemented_item_id.sinto(s);
1625                    let generics =
1626                        item_args.rebase_onto(tcx, container_id, implemented_trait_ref.args);
1627                    // Don't resolve, otherwise we'll always get the impl item id back.
1628                    ItemRef::translate_from_hax_def_id_maybe_resolve(
1629                        s,
1630                        implemented_item_id,
1631                        generics,
1632                        AssocItemResolution::None,
1633                    )
1634                };
1635                AssocItemContainer::TraitImplContainer {
1636                    impl_: item,
1637                    implemented_trait_ref: implemented_trait_ref.sinto(s),
1638                    implemented_trait_item,
1639                    overrides_default: tcx.defaultness(implemented_item_id).has_value(),
1640                }
1641            }
1642            ty::AssocContainer::InherentImpl => AssocItemContainer::InherentImplContainer {
1643                impl_id: container_id.sinto(s),
1644            },
1645        };
1646        let name = match item.opt_name() {
1647            None if let ty::AssocKind::Type { data } = item.kind
1648                && let ty::AssocTypeData::Rpitit(rpitit) = data =>
1649            {
1650                let (ty::ImplTraitInTraitData::Trait { fn_def_id, .. }
1651                | ty::ImplTraitInTraitData::Impl { fn_def_id, .. }) = rpitit;
1652                let fn_name = tcx.item_name(fn_def_id);
1653                let name = Symbol::intern(&format!("{fn_name}_ty"));
1654                Some(name)
1655            }
1656            opt_name => opt_name,
1657        };
1658        AssocItem {
1659            def_id: item.def_id.sinto(s),
1660            name,
1661            kind: item.kind.sinto(s),
1662            container,
1663            has_value: item.defaultness(tcx).has_value(),
1664        }
1665    }
1666
1667    /// The `DefId` of the item being implemented.
1668    pub fn implemented_trait_item_id(&self) -> &DefId {
1669        match &self.container {
1670            AssocItemContainer::TraitImplContainer {
1671                implemented_trait_item,
1672                ..
1673            } => &implemented_trait_item.def_id,
1674            _ => &self.def_id,
1675        }
1676    }
1677}
1678
1679/// Reflects [`ty::AssocKind`]
1680#[derive(AdtInto)]
1681#[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocKind, state: S as _tcx)]
1682#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1683pub enum AssocKind {
1684    Const { name: Symbol },
1685    Fn { name: Symbol, has_self: bool },
1686    Type { data: AssocTypeData },
1687}
1688
1689/// Reflects [`ty::AssocTypeData`]
1690#[derive(AdtInto)]
1691#[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocTypeData, state: S as _tcx)]
1692#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1693pub enum AssocTypeData {
1694    Normal(Symbol),
1695    Rpitit(ImplTraitInTraitData),
1696}
1697
1698#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1699pub enum AssocItemContainer {
1700    TraitContainer {
1701        trait_ref: TraitRef,
1702    },
1703    TraitImplContainer {
1704        /// Reference to the def_id of the impl block.
1705        impl_: ItemRef,
1706        /// The trait ref implemented by the impl block.
1707        implemented_trait_ref: TraitRef,
1708        /// The the associated item (in the trait declaration) that is being implemented.
1709        implemented_trait_item: ItemRef,
1710        /// Whether the corresponding trait item had a default (and therefore this one overrides
1711        /// it).
1712        overrides_default: bool,
1713    },
1714    InherentImplContainer {
1715        impl_id: DefId,
1716    },
1717}
1718
1719/// Reflects [`ty::ImplTraitInTraitData`]
1720#[derive(AdtInto)]
1721#[args(<'tcx, S: BaseState<'tcx>>, from: ty::ImplTraitInTraitData, state: S as _s)]
1722#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1723pub enum ImplTraitInTraitData {
1724    Trait {
1725        fn_def_id: DefId,
1726        opaque_def_id: DefId,
1727    },
1728    Impl {
1729        fn_def_id: DefId,
1730    },
1731}
charon_driver/hax/types/ty.rs

charon_driver/hax/types/
ty.rs
