charon_driver/hax/types/
ty.rs

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

charon_driver/hax/types/
ty.rs
