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.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, 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
627impl Alias {
628    #[tracing::instrument(level = "trace", skip(s))]
629    fn from<'tcx, S: UnderOwnerState<'tcx>>(s: &S, alias_ty: &ty::AliasTy<'tcx>) -> TyKind {
630        let tcx = s.base().tcx;
631        let typing_env = s.typing_env();
632        use rustc_type_ir::AliasTyKind as RustAliasKind;
633
634        // Try to normalize the alias first.
635        let ty = ty::Ty::new_alias(tcx, *alias_ty);
636        let ty = normalize(tcx, typing_env, ty::Unnormalized::new(ty));
637        let ty::Alias(alias_ty) = ty.kind() else {
638            let ty: Ty = ty.sinto(s);
639            return ty.kind().clone();
640        };
641
642        let kind = match alias_ty.kind {
643            RustAliasKind::Projection { def_id } => {
644                AliasKind::Projection(ItemRef::translate_projection(s, def_id, alias_ty.args))
645            }
646            RustAliasKind::Inherent { .. } => AliasKind::Inherent,
647            RustAliasKind::Opaque { def_id } => {
648                // Reveal the underlying `impl Trait` type.
649                let ty = tcx.type_of(def_id).instantiate(tcx, alias_ty.args);
650                let ty = normalize(tcx, s.typing_env(), ty);
651                AliasKind::Opaque {
652                    hidden_ty: ty.sinto(s),
653                }
654            }
655            RustAliasKind::Free { .. } => AliasKind::Free,
656        };
657        TyKind::Alias(Alias {
658            kind,
659            args: alias_ty.args.sinto(s),
660            def_id: alias_ty.kind.def_id().sinto(s),
661        })
662    }
663}
664
665impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Box<Ty>> for ty::Ty<'tcx> {
666    fn sinto(&self, s: &S) -> Box<Ty> {
667        Box::new(self.sinto(s))
668    }
669}
670
671/// Reflects [`rustc_middle::ty::Ty`]
672
673#[derive(Clone, Debug, Hash, PartialEq, Eq)]
674pub struct Ty {
675    pub(crate) kind: HashConsed<TyKind>,
676}
677
678impl Ty {
679    pub fn new<'tcx, S: BaseState<'tcx>>(_s: &S, kind: TyKind) -> Self {
680        let kind = HashConsed::new(kind);
681        Ty { kind }
682    }
683
684    pub fn kind(&self) -> &TyKind {
685        self.kind.inner()
686    }
687}
688
689impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Ty> for rustc_middle::ty::Ty<'tcx> {
690    fn sinto(&self, s: &S) -> Ty {
691        if let Some(ty) = s.with_cache(|cache| cache.tys.get(self).cloned()) {
692            return ty;
693        }
694        let kind: TyKind = self.kind().sinto(s);
695        let ty = Ty::new(s, kind);
696        s.with_cache(|cache| {
697            cache.tys.insert(*self, ty.clone());
698        });
699        ty
700    }
701}
702
703/// Reflects [`ty::TyKind`]
704#[derive(AdtInto)]
705#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::TyKind<'tcx>, state: S as s)]
706#[derive(Clone, Debug, Hash, PartialEq, Eq)]
707pub enum TyKind {
708    Bool,
709    Char,
710    Int(IntTy),
711    Uint(UintTy),
712    Float(FloatTy),
713
714    #[custom_arm(
715        ty::TyKind::FnDef(fun_id, generics) => {
716            let item = translate_item_ref(s, *fun_id, generics);
717            let tcx = s.base().tcx;
718            let fn_sig = tcx.fn_sig(*fun_id).instantiate(tcx, generics);
719            let fn_sig = Box::new(normalize(tcx, s.typing_env(), fn_sig).sinto(s));
720            TyKind::FnDef { item, fn_sig }
721        },
722    )]
723    /// Reflects [`ty::TyKind::FnDef`]
724    FnDef {
725        item: ItemRef,
726        fn_sig: Box<PolyFnSig>,
727    },
728
729    #[custom_arm(
730        ty::TyKind::FnPtr(tys, header) => {
731            let fn_sig_kind = ty::FnSigKind::new(header.abi(), header.safety(), header.c_variadic());
732            let sig = tys.map_bound(|tys| ty::FnSig {
733                inputs_and_output: tys.inputs_and_output,
734                fn_sig_kind,
735            });
736            TyKind::Arrow(Box::new(sig.sinto(s)))
737        },
738    )]
739    /// Reflects [`ty::TyKind::FnPtr`]
740    Arrow(Box<PolyFnSig>),
741
742    #[custom_arm(
743        ty::TyKind::Closure (def_id, generics) => {
744            TyKind::Closure(ClosureArgs::sfrom(s, *def_id, generics))
745        },
746    )]
747    Closure(ClosureArgs),
748
749    #[custom_arm(FROM_TYPE::Adt(adt_def, generics) => TO_TYPE::Adt(translate_item_ref(s, adt_def.did(), generics)),)]
750    Adt(ItemRef),
751    #[custom_arm(FROM_TYPE::Foreign(def_id) => TO_TYPE::Foreign(translate_item_ref(s, *def_id, Default::default())),)]
752    Foreign(ItemRef),
753    /// The `ItemRef` uses the fake `Array` def_id.
754    #[custom_arm(FROM_TYPE::Array(ty, len) => TO_TYPE::Array({
755        let args = s.base().tcx.mk_args(&[(*ty).into(), (*len).into()]);
756        ItemRef::translate_synthetic(s, SyntheticItem::Array, args)
757    }),)]
758    Array(ItemRef),
759    Pat(Ty, Pattern),
760    /// The `ItemRef` uses the fake `Slice` def_id.
761    #[custom_arm(FROM_TYPE::Slice(ty) => TO_TYPE::Slice({
762        let args = s.base().tcx.mk_args(&[(*ty).into()]);
763        ItemRef::translate_synthetic(s, SyntheticItem::Slice, args)
764    }),)]
765    Slice(ItemRef),
766    /// The `ItemRef` uses the fake `Tuple` def_id.
767    #[custom_arm(FROM_TYPE::Tuple(tys) => TO_TYPE::Tuple({
768        let args = s.base().tcx.mk_args_from_iter(tys.into_iter().map(ty::GenericArg::from));
769        ItemRef::translate_synthetic(s, SyntheticItem::Tuple(tys.len()), args)
770    }),)]
771    Tuple(ItemRef),
772    Str,
773    RawPtr(Box<Ty>, Mutability),
774    Ref(Region, Box<Ty>, Mutability),
775    #[custom_arm(FROM_TYPE::Dynamic(preds, region) => TyKind::Dynamic(resolve_for_dyn(s, preds, |_, _| ()), region.sinto(s)),)]
776    Dynamic(DynBinder<()>, Region),
777    #[custom_arm(FROM_TYPE::Coroutine(def_id, generics) => TO_TYPE::Coroutine(translate_item_ref(s, *def_id, generics)),)]
778    Coroutine(ItemRef),
779    Never,
780    #[custom_arm(FROM_TYPE::Alias(alias_ty) => Alias::from(s, alias_ty),)]
781    Alias(Alias),
782    Param(ParamTy),
783    Bound(BoundVarIndexKind, BoundTy),
784    Placeholder(PlaceholderType),
785    Infer(InferTy),
786    #[custom_arm(FROM_TYPE::Error(..) => TO_TYPE::Error,)]
787    Error,
788    #[todo]
789    Todo(String),
790}
791
792/// A representation of `exists<T: Trait1 + Trait2>(value)`: we create a fresh type id and the
793/// appropriate trait clauses. The contained value may refer to the fresh ty and the in-scope trait
794/// clauses. This is used to represent types related to `dyn Trait`.
795
796#[derive(Clone, Debug, Hash, PartialEq, Eq)]
797pub struct DynBinder<T> {
798    /// Fresh type parameter that we use as the `Self` type in the prediates below.
799    pub existential_ty: ParamTy,
800    /// Clauses that define the trait object. These clauses use the fresh type parameter above
801    /// as `Self` type.
802    pub predicates: GenericPredicates,
803    /// The value inside the binder.
804    pub val: T,
805}
806
807/// Do trait resolution in the context of the clauses of a `dyn Trait` type.
808fn resolve_for_dyn<'tcx, S: UnderOwnerState<'tcx>, R>(
809    s: &S,
810    // The predicates in the context.
811    epreds: &'tcx ty::List<ty::Binder<'tcx, ty::ExistentialPredicate<'tcx>>>,
812    f: impl FnOnce(&mut PredicateSearcher<'tcx>, ty::Ty<'tcx>) -> R,
813) -> DynBinder<R> {
814    fn searcher_for_traits<'tcx, S: UnderOwnerState<'tcx>>(
815        s: &S,
816        preds: &ItemPredicates<'tcx, DefId>,
817    ) -> PredicateSearcher<'tcx> {
818        let tcx = s.base().tcx;
819        // Populate a predicate searcher that knows about the `dyn` clauses.
820        let mut predicate_searcher = s.with_predicate_searcher(|ps, _| ps.clone());
821        predicate_searcher.insert_bound_predicates(&s.base_state(), preds.iter());
822        predicate_searcher.set_param_env(param_env_from_clauses(
823            tcx,
824            s.param_env()
825                .caller_bounds()
826                .iter()
827                .chain(preds.iter().map(|pred| pred.clause)),
828        ));
829        predicate_searcher
830    }
831
832    fn fresh_param_ty<'tcx, S: UnderOwnerState<'tcx>>(s: &S) -> ty::ParamTy {
833        let generics = s.owner().generics_of(s);
834        let param_count = generics.count();
835        ty::ParamTy::new(param_count as u32 + 1, rustc_span::Symbol::intern("_dyn"))
836    }
837
838    let tcx = s.base().tcx;
839    let span = rustc_span::DUMMY_SP.sinto(s);
840
841    // Pretend there's an extra type in the environment.
842    let new_param_ty = fresh_param_ty(s);
843    let new_ty = new_param_ty.to_ty(tcx);
844
845    // Set the new type as the `Self` parameter of our predicates.
846    let predicates = epreds.iter().map(|epred| epred.with_self_ty(tcx, new_ty));
847    let predicates: ItemPredicates<'_, DefId> = ItemPredicates::new_unmapped(span, predicates);
848
849    // Populate a predicate searcher that knows about the `dyn` clauses.
850    let mut predicate_searcher = searcher_for_traits(s, &predicates);
851    let val = f(&mut predicate_searcher, new_ty);
852
853    // Using the predicate searcher, translate the predicates. Only the projection predicates need
854    // to be handled specially.
855    let predicates = predicates
856        .iter()
857        .map(|pred| {
858            match pred.clause.as_projection_clause() {
859                // Translate normally
860                None => pred.sinto(s),
861                // Translate by hand using our predicate searcher. This does the same as
862                // `clause.sinto(s)` except that it uses our predicate searcher to resolve the
863                // projection `TraitProof`.
864                Some(proj) => {
865                    let bound_vars = proj.bound_vars().sinto(s);
866                    let proj = {
867                        let alias_ty = &proj.skip_binder().projection_term.expect_ty(tcx);
868                        let trait_proof = {
869                            let poly_trait_ref = proj.rebind(alias_ty.trait_ref(tcx));
870                            predicate_searcher
871                                .resolve(&s.base_state(), &poly_trait_ref)
872                                .sinto(s)
873                        };
874                        let Term::Ty(ty) = proj.skip_binder().term.sinto(s) else {
875                            unreachable!()
876                        };
877                        let item = tcx.associated_item(alias_ty.kind.def_id());
878                        ProjectionPredicate {
879                            trait_proof,
880                            assoc_item: AssocItem::sfrom(s, &item),
881                            ty,
882                        }
883                    };
884                    let kind = Binder {
885                        value: ClauseKind::Projection(proj),
886                        bound_vars,
887                    };
888                    let clause = Clause { kind };
889                    GenericPredicate {
890                        id: pred.id.sinto(s),
891                        clause,
892                        span,
893                    }
894                }
895            }
896        })
897        .collect();
898
899    let predicates = GenericPredicates { predicates };
900    DynBinder {
901        existential_ty: new_param_ty.sinto(s),
902        predicates,
903        val,
904    }
905}
906
907#[derive(AdtInto)]
908#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::pattern::PatternKind<'tcx>, state: S as gstate)]
909#[derive(Clone, Debug, Hash, PartialEq, Eq)]
910pub enum Pattern {
911    Range {
912        start: ConstantExpr,
913        end: ConstantExpr,
914    },
915    Or(Vec<Pattern>),
916    NotNull,
917}
918
919impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Pattern> for ty::Pattern<'tcx> {
920    fn sinto(&self, s: &S) -> Pattern {
921        self.kind().sinto(s)
922    }
923}
924/// Reflects [`ty::CanonicalUserTypeAnnotation`]
925#[derive(AdtInto)]
926#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::CanonicalUserTypeAnnotation<'tcx>, state: S as gstate)]
927#[derive(Clone, Debug)]
928pub struct CanonicalUserTypeAnnotation {
929    pub user_ty: CanonicalUserType,
930    pub span: Span,
931    pub inferred_ty: Ty,
932}
933
934/// Reflects [`ty::AdtKind`]
935
936#[derive(Copy, Clone, Debug)]
937pub enum AdtKind {
938    Struct,
939    Union,
940    Enum,
941    /// We sometimes pretend arrays are an ADT and generate a `FullDef` for them.
942    Array,
943    /// We sometimes pretend slices are an ADT and generate a `FullDef` for them.
944    Slice,
945    /// We sometimes pretend tuples are an ADT and generate a `FullDef` for them.
946    Tuple,
947}
948
949impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, AdtKind> for ty::AdtKind {
950    fn sinto(&self, _s: &S) -> AdtKind {
951        match self {
952            ty::AdtKind::Struct => AdtKind::Struct,
953            ty::AdtKind::Union => AdtKind::Union,
954            ty::AdtKind::Enum => AdtKind::Enum,
955        }
956    }
957}
958
959sinto_todo!(rustc_middle::ty, AdtFlags);
960
961/// Reflects [`rustc_abi::ReprOptions`].
962
963#[derive(AdtInto, Clone, Debug)]
964#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: rustc_abi::ReprOptions, state: S as s)]
965pub struct ReprOptions {
966    /// Whether an explicit integer representation was specified.
967    #[value(self.int.is_some())]
968    pub int_specified: bool,
969    /// The actual discriminant type resulting from the representation options.
970    #[value({
971        use rustc_middle::ty::util::IntTypeExt;
972        self.discr_type().to_ty(s.base().tcx).sinto(s)
973    })]
974    pub typ: Ty,
975    pub align: Option<Align>,
976    pub pack: Option<Align>,
977    #[value(ReprFlags { is_c: self.c(), is_transparent: self.transparent(), is_simd: self.simd() })]
978    pub flags: ReprFlags,
979}
980
981/// The representation flags without the ones irrelevant outside of rustc.
982
983#[derive(Default, Clone, Debug)]
984pub struct ReprFlags {
985    pub is_c: bool,
986    pub is_transparent: bool,
987    pub is_simd: bool,
988}
989
990/// Reflects [`rustc_abi::Align`], but directly stores the number of bytes as a u64.
991
992#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
993#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_abi::Align, state: S as _s)]
994pub struct Align {
995    #[value({
996        self.bytes()
997    })]
998    pub bytes: u64,
999}
1000
1001/// The metadata to attach to the newly-unsized ptr.
1002#[derive(Clone, Debug)]
1003pub enum UnsizingMetadata {
1004    /// Unsize an array to a slice, storing the length as metadata.
1005    Length(ConstantExpr),
1006    /// Unsize a non-dyn type to a dyn type, adding a vtable pointer as metadata.
1007    DirectVTable(TraitProof),
1008    /// Unsize a dyn-type to another dyn-type, (optionally) indexing within the current vtable.
1009    NestedVTable(DynBinder<TraitProof>),
1010    /// Couldn't compute
1011    Unknown,
1012}
1013
1014pub fn compute_unsizing_metadata<'tcx, S: UnderOwnerState<'tcx>>(
1015    s: &S,
1016    src_ty: ty::Ty<'tcx>,
1017    tgt_ty: ty::Ty<'tcx>,
1018) -> UnsizingMetadata {
1019    // TODO: to properly find out what field we want, we should use the query
1020    // `coerce_unsized_info`, which we call recursively to get the list of fields
1021    // to go into until we reach a pointer/reference.
1022    // We should also pass this list of field IDs in the unsizing metadata.
1023
1024    let (Some(src_ty), Some(tgt_ty)) = (src_ty.builtin_deref(true), tgt_ty.builtin_deref(true))
1025    else {
1026        return UnsizingMetadata::Unknown;
1027    };
1028
1029    let tcx = s.base().tcx;
1030    let typing_env = s.typing_env();
1031    let (src_ty, tgt_ty) =
1032        tcx.struct_lockstep_tails_raw(src_ty, tgt_ty, |ty| normalize(tcx, typing_env, ty));
1033
1034    match (&src_ty.kind(), &tgt_ty.kind()) {
1035        (ty::Array(_, len), ty::Slice(_)) => {
1036            let len = len.sinto(s);
1037            UnsizingMetadata::Length(len)
1038        }
1039        (ty::Dynamic(from_preds, _), ty::Dynamic(to_preds, ..)) => {
1040            let trait_proof = resolve_for_dyn(s, from_preds, |searcher, fresh_ty| {
1041                let to_pred = if let Some(to_principal) = to_preds.principal() {
1042                    to_principal.with_self_ty(tcx, fresh_ty)
1043                } else {
1044                    let def_id = to_preds
1045                        .iter()
1046                        .find_map(|pred| match pred.skip_binder() {
1047                            ty::ExistentialPredicate::AutoTrait(def_id) => Some(def_id),
1048                            _ => None,
1049                        })
1050                        .expect("expected a trait predicate in dyn upcast target");
1051                    ty::Binder::dummy(ty::TraitRef::new(tcx, def_id, [fresh_ty]))
1052                };
1053                searcher.resolve(&s.base_state(), &to_pred).sinto(s)
1054            });
1055            UnsizingMetadata::NestedVTable(trait_proof)
1056        }
1057        (_, ty::Dynamic(preds, ..)) => {
1058            let pred = preds[0].with_self_ty(tcx, src_ty);
1059            let clause = pred.as_trait_clause().expect(
1060                "the first `ExistentialPredicate` of `TyKind::Dynamic` \\
1061                                        should be a trait clause",
1062            );
1063            let tref = clause.rebind(clause.skip_binder().trait_ref);
1064            let trait_proof = solve_trait(s, tref);
1065
1066            UnsizingMetadata::DirectVTable(trait_proof)
1067        }
1068        _ => UnsizingMetadata::Unknown,
1069    }
1070}
1071
1072/// Reflects [`ty::FnSig`]
1073#[derive(AdtInto, Clone, Debug, Hash, PartialEq, Eq)]
1074#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::FnSig<'tcx>, state: S as s)]
1075pub struct TyFnSig {
1076    #[value(self.inputs().sinto(s))]
1077    pub inputs: Vec<Ty>,
1078    #[value(self.output().sinto(s))]
1079    pub output: Ty,
1080    #[value(self.c_variadic())]
1081    pub c_variadic: bool,
1082    #[value(self.safety())]
1083    pub safety: Safety,
1084    #[value(self.abi())]
1085    pub abi: ExternAbi,
1086}
1087
1088/// Reflects [`ty::PolyFnSig`]
1089pub type PolyFnSig = Binder<TyFnSig>;
1090
1091/// Reflects [`ty::TraitRef`]
1092/// Contains the def_id and arguments passed to the trait. The first type argument is the `Self`
1093/// type. The trait proofs are the _required_ predicate for this trait; currently they are always
1094/// empty because we consider all trait predicates as implied.
1095/// `self.in_trait` is always `None` because a trait can't be associated to another one.
1096pub type TraitRef = ItemRef;
1097
1098impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, TraitRef> for ty::TraitRef<'tcx> {
1099    fn sinto(&self, s: &S) -> TraitRef {
1100        translate_item_ref(s, self.def_id, self.args)
1101    }
1102}
1103
1104/// Reflects [`ty::TraitPredicate`]
1105#[derive(AdtInto)]
1106#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::TraitPredicate<'tcx>, state: S as tcx)]
1107#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1108pub struct TraitPredicate {
1109    pub trait_ref: TraitRef,
1110    #[map(*x == ty::PredicatePolarity::Positive)]
1111    #[from(polarity)]
1112    pub is_positive: bool,
1113}
1114
1115/// Reflects [`ty::OutlivesPredicate`] as a named struct
1116/// instead of a tuple struct. This is because the script converting
1117/// JSONSchema types to OCaml doesn't support tuple structs, and this
1118/// is the only tuple struct in the whole AST.
1119
1120#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1121pub struct OutlivesPredicate<T> {
1122    pub lhs: T,
1123    pub rhs: Region,
1124}
1125
1126impl<'tcx, S: UnderOwnerState<'tcx>, T, U> SInto<S, OutlivesPredicate<U>>
1127    for ty::OutlivesPredicate<'tcx, T>
1128where
1129    T: SInto<S, U>,
1130{
1131    fn sinto(&self, s: &S) -> OutlivesPredicate<U> where {
1132        OutlivesPredicate {
1133            lhs: self.0.sinto(s),
1134            rhs: self.1.sinto(s),
1135        }
1136    }
1137}
1138
1139/// Reflects [`ty::RegionOutlivesPredicate`]
1140pub type RegionOutlivesPredicate = OutlivesPredicate<Region>;
1141/// Reflects [`ty::TypeOutlivesPredicate`]
1142pub type TypeOutlivesPredicate = OutlivesPredicate<Ty>;
1143
1144/// Reflects [`ty::Term`]
1145
1146#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1147pub enum Term {
1148    Ty(Ty),
1149    Const(ConstantExpr),
1150}
1151
1152impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Term> for ty::Term<'tcx> {
1153    fn sinto(&self, s: &S) -> Term {
1154        use ty::TermKind;
1155        match self.kind() {
1156            TermKind::Ty(ty) => Term::Ty(ty.sinto(s)),
1157            TermKind::Const(c) => Term::Const(c.sinto(s)),
1158        }
1159    }
1160}
1161
1162/// Expresses a constraints over an associated type.
1163///
1164/// For instance:
1165/// ```text
1166/// fn f<T : Foo<S = String>>(...)
1167///              ^^^^^^^^^^
1168/// ```
1169/// (provided the trait `Foo` has an associated type `S`).
1170
1171#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1172pub struct ProjectionPredicate {
1173    /// The `impl Trait for Ty` in `Ty: Trait<..., Type = U>`.
1174    pub trait_proof: TraitProof,
1175    /// The `Type` in `Ty: Trait<..., Type = U>`.
1176    pub assoc_item: AssocItem,
1177    /// The type `U` in `Ty: Trait<..., Type = U>`.
1178    pub ty: Ty,
1179}
1180
1181impl<'tcx, S: UnderBinderState<'tcx>> SInto<S, ProjectionPredicate>
1182    for ty::ProjectionPredicate<'tcx>
1183{
1184    fn sinto(&self, s: &S) -> ProjectionPredicate {
1185        let tcx = s.base().tcx;
1186        let alias_ty = &self.projection_term.expect_ty(tcx);
1187        let poly_trait_ref = s.binder().rebind(alias_ty.trait_ref(tcx));
1188        let Term::Ty(ty) = self.term.sinto(s) else {
1189            unreachable!()
1190        };
1191        let item = tcx.associated_item(alias_ty.kind.def_id());
1192        ProjectionPredicate {
1193            trait_proof: solve_trait(s, poly_trait_ref),
1194            assoc_item: AssocItem::sfrom(s, &item),
1195            ty,
1196        }
1197    }
1198}
1199
1200/// Reflects [`ty::ClauseKind`]
1201#[derive(AdtInto)]
1202#[args(<'tcx, S: UnderBinderState<'tcx>>, from: ty::ClauseKind<'tcx>, state: S as tcx)]
1203#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1204pub enum ClauseKind {
1205    Trait(TraitPredicate),
1206    RegionOutlives(RegionOutlivesPredicate),
1207    TypeOutlives(TypeOutlivesPredicate),
1208    Projection(ProjectionPredicate),
1209    ConstArgHasType(ConstantExpr, Ty),
1210    WellFormed(Term),
1211    ConstEvaluatable(ConstantExpr),
1212    HostEffect(HostEffectPredicate),
1213    UnstableFeature(Symbol),
1214}
1215
1216sinto_todo!(rustc_middle::ty, HostEffectPredicate<'tcx>);
1217
1218/// Reflects [`ty::Clause`] and adds a hash-consed predicate identifier.
1219
1220#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1221pub struct Clause {
1222    pub kind: Binder<ClauseKind>,
1223}
1224
1225impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for ty::Clause<'tcx> {
1226    fn sinto(&self, s: &S) -> Clause {
1227        let kind = self.kind().sinto(s);
1228        Clause { kind }
1229    }
1230}
1231
1232impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause> for ty::PolyTraitPredicate<'tcx> {
1233    fn sinto(&self, s: &S) -> Clause {
1234        let kind: Binder<_> = self.sinto(s);
1235        let kind: Binder<ClauseKind> = kind.map(ClauseKind::Trait);
1236        Clause { kind }
1237    }
1238}
1239
1240/// Reflects [`ty::Predicate`] and adds a hash-consed predicate identifier.
1241
1242#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1243pub struct Predicate {
1244    pub kind: Binder<PredicateKind>,
1245}
1246
1247impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Predicate> for ty::Predicate<'tcx> {
1248    fn sinto(&self, s: &S) -> Predicate {
1249        let kind = self.kind().sinto(s);
1250        Predicate { kind }
1251    }
1252}
1253
1254/// Reflects [`ty::BoundVariableKind`]
1255#[derive(AdtInto)]
1256#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::BoundVariableKind<'tcx>, state: S as tcx)]
1257#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1258pub enum BoundVariableKind {
1259    Ty(BoundTyKind),
1260    #[custom_arm(
1261        &FROM_TYPE::Region(region) => TO_TYPE::Region(region.sinto(tcx), None),
1262    )]
1263    Region(BoundRegionKind, Option<Variance>),
1264    Const,
1265}
1266
1267/// Reflects [`ty::Binder`]
1268
1269#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1270pub struct Binder<T> {
1271    pub value: T,
1272    pub bound_vars: Vec<BoundVariableKind>,
1273}
1274
1275impl Binder<()> {
1276    pub fn empty() -> Self {
1277        Binder {
1278            value: (),
1279            bound_vars: vec![],
1280        }
1281    }
1282}
1283
1284impl<T> Binder<T> {
1285    pub fn as_ref(&self) -> Binder<&T> {
1286        Binder {
1287            value: &self.value,
1288            bound_vars: self.bound_vars.clone(),
1289        }
1290    }
1291
1292    pub fn hax_skip_binder(self) -> T {
1293        self.value
1294    }
1295
1296    pub fn hax_skip_binder_ref(&self) -> &T {
1297        &self.value
1298    }
1299
1300    pub fn map<U>(self, f: impl FnOnce(T) -> U) -> Binder<U> {
1301        Binder {
1302            value: f(self.value),
1303            bound_vars: self.bound_vars,
1304        }
1305    }
1306
1307    pub fn inner_mut(&mut self) -> &mut T {
1308        &mut self.value
1309    }
1310
1311    pub fn rebind<U>(&self, value: U) -> Binder<U> {
1312        self.as_ref().map(|_| value)
1313    }
1314}
1315
1316/// Uniquely identifies a predicate.
1317#[derive(AdtInto)]
1318#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: traits::ItemPredicateId<DefId>, state: S as s)]
1319#[derive(Debug, Clone, Hash, PartialEq, Eq)]
1320pub enum GenericPredicateId {
1321    /// A predicate that counts as "input" for an item, e.g. `where` clauses on a function or impl.
1322    /// Numbered in some arbitrary but consistent order.
1323    Required(DefId, u32),
1324    /// A predicate that counts as "output" of an item, e.g. supertrait clauses in a trait. Note
1325    /// that we count `where` clauses on a trait as implied.
1326    /// Numbered in some arbitrary but consistent order.
1327    Implied(DefId, u32),
1328    /// Predicate inside a non-item binder, e.g. within a `dyn Trait`.
1329    /// Numbered in some arbitrary but consistent order.
1330    Unmapped(u32),
1331    /// The special `Self: Trait` clause available within trait `Trait`.
1332    TraitSelf,
1333}
1334
1335#[derive(AdtInto)]
1336#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: traits::ItemPredicate<'tcx, DefId>, state: S as s)]
1337#[derive(Debug, Clone, Hash, PartialEq, Eq)]
1338pub struct GenericPredicate {
1339    pub id: GenericPredicateId,
1340    pub clause: Clause,
1341    pub span: Span,
1342}
1343
1344/// Reflects [`ty::GenericPredicates`]
1345#[derive(AdtInto)]
1346#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: traits::ItemPredicates<'tcx, DefId>, state: S as s)]
1347#[derive(Clone, Debug, Default, Hash, PartialEq, Eq)]
1348pub struct GenericPredicates {
1349    pub predicates: Vec<GenericPredicate>,
1350}
1351
1352impl GenericPredicates {
1353    pub fn iter(&self) -> impl Iterator<Item = &GenericPredicate> {
1354        self.predicates.iter()
1355    }
1356    /// Iter only on trait clauses.
1357    pub fn iter_trait_clauses(&self) -> impl Iterator<Item = &GenericPredicate> {
1358        self.iter()
1359            .filter(|pred| matches!(pred.clause.kind.hax_skip_binder_ref(), ClauseKind::Trait(_)))
1360    }
1361}
1362
1363/// Lets types declare how to compute the variance of bound parameters.
1364trait BinderVariances<'tcx>: Sized {
1365    fn variances(
1366        _tcx: ty::TyCtxt<'tcx>,
1367        _binder: &ty::Binder<'tcx, Self>,
1368    ) -> HashMap<ty::BoundVar, ty::Variance> {
1369        HashMap::new()
1370    }
1371}
1372
1373impl<'tcx> BinderVariances<'tcx> for ty::FnSig<'tcx> {
1374    fn variances(
1375        tcx: ty::TyCtxt<'tcx>,
1376        binder: &ty::Binder<'tcx, Self>,
1377    ) -> HashMap<ty::BoundVar, ty::Variance> {
1378        fn_sig_bound_region_variances(tcx, *binder)
1379    }
1380}
1381
1382impl<'tcx> BinderVariances<'tcx> for ty::ClauseKind<'tcx> {}
1383impl<'tcx> BinderVariances<'tcx> for ty::PredicateKind<'tcx> {}
1384impl<'tcx> BinderVariances<'tcx> for ty::TraitRef<'tcx> {}
1385impl<'tcx> BinderVariances<'tcx> for ty::TraitPredicate<'tcx> {}
1386
1387impl<'tcx, S: UnderOwnerState<'tcx>, T1, T2> SInto<S, Binder<T2>> for ty::Binder<'tcx, T1>
1388where
1389    T1: SInto<StateWithBinder<'tcx>, T2> + BinderVariances<'tcx>,
1390{
1391    fn sinto(&self, s: &S) -> Binder<T2> {
1392        let variances = T1::variances(s.base().tcx, self);
1393        let mut bound_vars = self.bound_vars().sinto(s);
1394        for (index, var) in bound_vars.iter_mut().enumerate() {
1395            if let BoundVariableKind::Region(_, variance) = var {
1396                *variance = variances
1397                    .get(&ty::BoundVar::from_usize(index))
1398                    .copied()
1399                    .sinto(s);
1400            }
1401        }
1402        let value = {
1403            let under_binder_s = &s.with_binder(self.as_ref().map_bound(|_| ()));
1404            self.as_ref().skip_binder().sinto(under_binder_s)
1405        };
1406        Binder { value, bound_vars }
1407    }
1408}
1409
1410/// Reflects [`ty::SubtypePredicate`]
1411#[derive(AdtInto)]
1412#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::SubtypePredicate<'tcx>, state: S as tcx)]
1413#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1414pub struct SubtypePredicate {
1415    pub a_is_expected: bool,
1416    pub a: Ty,
1417    pub b: Ty,
1418}
1419
1420/// Reflects [`ty::CoercePredicate`]
1421#[derive(AdtInto)]
1422#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::CoercePredicate<'tcx>, state: S as tcx)]
1423#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1424pub struct CoercePredicate {
1425    pub a: Ty,
1426    pub b: Ty,
1427}
1428
1429/// Reflects [`ty::AliasRelationDirection`]
1430#[derive(AdtInto)]
1431#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::AliasRelationDirection, state: S as _tcx)]
1432#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1433pub enum AliasRelationDirection {
1434    Equate,
1435    Subtype,
1436}
1437
1438/// Reflects [`ty::ClosureArgs`]
1439#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1440
1441pub struct ClosureArgs {
1442    pub item: ItemRef,
1443    /// The base kind of this closure. The kinds are ordered by inclusion: any `Fn` works as an
1444    /// `FnMut`, and any `FnMut` works as an `FnOnce`.
1445    pub kind: ClosureKind,
1446    /// The signature of the function that the closure implements, e.g. `fn(A, B, C) -> D`.
1447    pub fn_sig: PolyFnSig,
1448    /// The set of captured variables. Together they form the state of the closure.
1449    pub upvar_tys: Vec<Ty>,
1450}
1451
1452impl ClosureArgs {
1453    /// Iterate over the upvars that are borrows with erased regions. These may require allocating
1454    /// fresh regions.
1455    pub fn iter_upvar_borrows(&self) -> impl Iterator<Item = &Ty> {
1456        self.upvar_tys.iter().filter(|ty| {
1457            matches!(
1458                ty.kind(),
1459                TyKind::Ref(
1460                    Region {
1461                        kind: RegionKind::ReErased
1462                    },
1463                    ..
1464                )
1465            )
1466        })
1467    }
1468}
1469
1470impl ClosureArgs {
1471    // Manual implementation because we need the `def_id` of the closure.
1472    pub fn sfrom<'tcx, S>(s: &S, def_id: RDefId, from: ty::GenericArgsRef<'tcx>) -> Self
1473    where
1474        S: UnderOwnerState<'tcx>,
1475    {
1476        use rustc_middle::ty;
1477        use rustc_type_ir::TypeFoldable;
1478        use rustc_type_ir::TypeSuperFoldable;
1479
1480        struct RegionUnEraserVisitor<'tcx> {
1481            tcx: ty::TyCtxt<'tcx>,
1482            depth: u32,
1483            bound_vars: Vec<ty::BoundVariableKind<'tcx>>,
1484        }
1485
1486        impl<'tcx> ty::TypeFolder<ty::TyCtxt<'tcx>> for RegionUnEraserVisitor<'tcx> {
1487            fn cx(&self) -> ty::TyCtxt<'tcx> {
1488                self.tcx
1489            }
1490
1491            fn fold_ty(&mut self, ty: ty::Ty<'tcx>) -> ty::Ty<'tcx> {
1492                ty.super_fold_with(self)
1493            }
1494
1495            fn fold_binder<T>(&mut self, t: ty::Binder<'tcx, T>) -> ty::Binder<'tcx, T>
1496            where
1497                T: ty::TypeFoldable<ty::TyCtxt<'tcx>>,
1498            {
1499                self.depth += 1;
1500                let t = t.super_fold_with(self);
1501                self.depth -= 1;
1502                t
1503            }
1504
1505            fn fold_region(&mut self, r: ty::Region<'tcx>) -> ty::Region<'tcx> {
1506                // Replace erased regions with fresh bound regions.
1507                if r.is_erased() {
1508                    let bound_region = ty::BoundRegion {
1509                        var: ty::BoundVar::from_usize(self.bound_vars.len()),
1510                        kind: ty::BoundRegionKind::Anon,
1511                    };
1512                    self.bound_vars
1513                        .push(ty::BoundVariableKind::Region(bound_region.kind));
1514                    ty::Region::new_bound(
1515                        self.tcx,
1516                        ty::DebruijnIndex::from(self.depth),
1517                        bound_region,
1518                    )
1519                } else {
1520                    r
1521                }
1522            }
1523        }
1524
1525        let tcx = s.base().tcx;
1526        let closure = from.as_closure();
1527        let item = {
1528            // The closure has no generics of its own: it inherits its parent generics and could
1529            // have late-bound args but these are part of the signature.
1530            let parent_args = tcx.mk_args(closure.parent_args());
1531            translate_item_ref(s, def_id, parent_args)
1532        };
1533        let sig = closure.sig();
1534        let sig = tcx.signature_unclosure(sig, rustc_hir::Safety::Safe);
1535        // Add bound variables for each erased region in the signature.
1536        let sig = {
1537            let mut visitor = RegionUnEraserVisitor {
1538                tcx,
1539                depth: 0,
1540                bound_vars: sig.bound_vars().iter().collect(),
1541            };
1542            let unbound_sig = sig.skip_binder().fold_with(&mut visitor);
1543            let bound_vars = tcx.mk_bound_variable_kinds(&visitor.bound_vars);
1544            ty::Binder::bind_with_vars(unbound_sig, bound_vars)
1545        };
1546        ClosureArgs {
1547            item,
1548            kind: closure.kind().sinto(s),
1549            fn_sig: sig.sinto(s),
1550            upvar_tys: closure.upvar_tys().sinto(s),
1551        }
1552    }
1553}
1554
1555/// Reflects [`ty::ClosureKind`]
1556#[derive(AdtInto)]
1557#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::ClosureKind, state: S as _tcx)]
1558#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1559pub enum ClosureKind {
1560    Fn,
1561    FnMut,
1562    FnOnce,
1563}
1564
1565sinto_todo!(rustc_middle::ty, NormalizesTo<'tcx>);
1566
1567/// Reflects [`ty::PredicateKind`]
1568#[derive(AdtInto)]
1569#[args(<'tcx, S: UnderBinderState<'tcx>>, from: ty::PredicateKind<'tcx>, state: S as tcx)]
1570#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1571pub enum PredicateKind {
1572    Clause(ClauseKind),
1573    DynCompatible(DefId),
1574    Subtype(SubtypePredicate),
1575    Coerce(CoercePredicate),
1576    ConstEquate(ConstantExpr, ConstantExpr),
1577    Ambiguous,
1578    AliasRelate(Term, Term, AliasRelationDirection),
1579    NormalizesTo(NormalizesTo),
1580}
1581
1582/// Reflects [`ty::AssocItem`]
1583
1584#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1585pub struct AssocItem {
1586    pub def_id: DefId,
1587    /// This is `None` for RPTITs.
1588    pub name: Option<Symbol>,
1589    pub kind: AssocKind,
1590    pub container: AssocItemContainer,
1591    /// Whether this item has a value (e.g. this is `false` for trait methods without default
1592    /// implementations).
1593    pub has_value: bool,
1594}
1595
1596impl AssocItem {
1597    pub fn sfrom<'tcx, S: BaseState<'tcx>>(s: &S, item: &ty::AssocItem) -> AssocItem {
1598        Self::sfrom_instantiated(s, item, None)
1599    }
1600
1601    /// Translate an `AssocItem` and optionally instantiate it with the provided arguments.
1602    pub fn sfrom_instantiated<'tcx, S: BaseState<'tcx>>(
1603        s: &S,
1604        item: &ty::AssocItem,
1605        item_args: Option<ty::GenericArgsRef<'tcx>>,
1606    ) -> AssocItem {
1607        let tcx = s.base().tcx;
1608        // We want to solve traits in the context of this item.
1609        let item_def_id = item.def_id.sinto(s);
1610        let s = &s.with_hax_owner(&item_def_id);
1611        let item_args = item_args.unwrap_or_else(|| item_def_id.identity_args(s));
1612        let container_id = item.container_id(tcx);
1613        let container_args = item_args.truncate_to(tcx, tcx.generics_of(container_id));
1614        let container = match item.container {
1615            ty::AssocContainer::Trait => {
1616                let trait_ref =
1617                    ty::TraitRef::new_from_args(tcx, container_id, container_args).sinto(s);
1618                AssocItemContainer::TraitContainer { trait_ref }
1619            }
1620            ty::AssocContainer::TraitImpl(implemented_item_id) => {
1621                let implemented_item_id = implemented_item_id.unwrap();
1622                let item = translate_item_ref(s, container_id, container_args);
1623                let implemented_trait_ref = tcx
1624                    .impl_trait_ref(container_id)
1625                    .instantiate(tcx, container_args);
1626                let implemented_trait_ref = normalize(tcx, s.typing_env(), implemented_trait_ref);
1627                let implemented_trait_item = {
1628                    let implemented_item_id = implemented_item_id.sinto(s);
1629                    let generics =
1630                        item_args.rebase_onto(tcx, container_id, implemented_trait_ref.args);
1631                    // Don't resolve, otherwise we'll always get the impl item id back.
1632                    ItemRef::translate_from_hax_def_id_maybe_resolve(
1633                        s,
1634                        implemented_item_id,
1635                        generics,
1636                        AssocItemResolution::None,
1637                    )
1638                };
1639                AssocItemContainer::TraitImplContainer {
1640                    impl_: item,
1641                    implemented_trait_ref: implemented_trait_ref.sinto(s),
1642                    implemented_trait_item,
1643                    overrides_default: tcx.defaultness(implemented_item_id).has_value(),
1644                }
1645            }
1646            ty::AssocContainer::InherentImpl => AssocItemContainer::InherentImplContainer {
1647                impl_id: container_id.sinto(s),
1648            },
1649        };
1650        let name = match item.opt_name() {
1651            None if let ty::AssocKind::Type { data } = item.kind
1652                && let ty::AssocTypeData::Rpitit(rpitit) = data =>
1653            {
1654                let (ty::ImplTraitInTraitData::Trait { fn_def_id, .. }
1655                | ty::ImplTraitInTraitData::Impl { fn_def_id, .. }) = rpitit;
1656                let fn_name = tcx.item_name(fn_def_id);
1657                let name = Symbol::intern(&format!("{fn_name}_ty"));
1658                Some(name)
1659            }
1660            opt_name => opt_name,
1661        };
1662        AssocItem {
1663            def_id: item.def_id.sinto(s),
1664            name,
1665            kind: item.kind.sinto(s),
1666            container,
1667            has_value: item.defaultness(tcx).has_value(),
1668        }
1669    }
1670
1671    /// The `DefId` of the item being implemented.
1672    pub fn implemented_trait_item_id(&self) -> &DefId {
1673        match &self.container {
1674            AssocItemContainer::TraitImplContainer {
1675                implemented_trait_item,
1676                ..
1677            } => &implemented_trait_item.def_id,
1678            _ => &self.def_id,
1679        }
1680    }
1681}
1682
1683/// Reflects [`ty::AssocKind`]
1684#[derive(AdtInto)]
1685#[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocKind, state: S as _tcx)]
1686#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1687pub enum AssocKind {
1688    Const { name: Symbol },
1689    Fn { name: Symbol, has_self: bool },
1690    Type { data: AssocTypeData },
1691}
1692
1693/// Reflects [`ty::AssocTypeData`]
1694#[derive(AdtInto)]
1695#[args(<'tcx, S: BaseState<'tcx>>, from: ty::AssocTypeData, state: S as _tcx)]
1696#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1697pub enum AssocTypeData {
1698    Normal(Symbol),
1699    Rpitit(ImplTraitInTraitData),
1700}
1701
1702#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1703pub enum AssocItemContainer {
1704    TraitContainer {
1705        trait_ref: TraitRef,
1706    },
1707    TraitImplContainer {
1708        /// Reference to the def_id of the impl block.
1709        impl_: ItemRef,
1710        /// The trait ref implemented by the impl block.
1711        implemented_trait_ref: TraitRef,
1712        /// The the associated item (in the trait declaration) that is being implemented.
1713        implemented_trait_item: ItemRef,
1714        /// Whether the corresponding trait item had a default (and therefore this one overrides
1715        /// it).
1716        overrides_default: bool,
1717    },
1718    InherentImplContainer {
1719        impl_id: DefId,
1720    },
1721}
1722
1723/// Reflects [`ty::ImplTraitInTraitData`]
1724#[derive(AdtInto)]
1725#[args(<'tcx, S: BaseState<'tcx>>, from: ty::ImplTraitInTraitData, state: S as _s)]
1726#[derive(Clone, Debug, Hash, PartialEq, Eq)]
1727pub enum ImplTraitInTraitData {
1728    Trait {
1729        fn_def_id: DefId,
1730        opaque_def_id: DefId,
1731    },
1732    Impl {
1733        fn_def_id: DefId,
1734    },
1735}
charon_driver/hax/types/ty.rs

charon_driver/hax/types/
ty.rs
