charon_driver/hax/types/
predicates.rs

1use crate::hax::prelude::*;
2use crate::hax::sinto_todo;
3
4use rustc_middle::ty;
5
6/// A predicate without `Self`, for use in `dyn Trait`.
7///
8/// Reflects [`ty::ExistentialPredicate`]
9#[derive(AdtInto)]
10#[args(< S: UnderOwnerState<'tcx>>, from: ty::ExistentialPredicate<'tcx>, state: S as state)]
11#[derive(Debug, Clone, PartialEq, Eq, Hash)]
12pub enum ExistentialPredicate<'tcx> {
13    /// E.g. `From<u64>`. Note that this isn't `T: From<u64>` with a given `T`, this is just
14    /// `From<u64>`. Could be written `?: From<u64>`.
15    Trait(ExistentialTraitRef<'tcx>),
16    /// E.g. `Iterator::Item = u64`. Could be written `<? as Iterator>::Item = u64`.
17    Projection(ExistentialProjection<'tcx>),
18    /// E.g. `Send`.
19    AutoTrait(DefId),
20}
21
22/// Reflects [`ty::ExistentialTraitRef`]
23#[derive(AdtInto)]
24#[args(< S: UnderOwnerState<'tcx>>, from: ty::ExistentialTraitRef<'tcx>, state: S as state)]
25#[derive(Debug, Clone, PartialEq, Eq, Hash)]
26pub struct ExistentialTraitRef<'tcx> {
27    pub def_id: DefId,
28    pub args: Vec<GenericArg<'tcx>>,
29}
30
31/// Reflects [`ty::ExistentialProjection`]
32#[derive(AdtInto)]
33#[args(< S: UnderOwnerState<'tcx>>, from: ty::ExistentialProjection<'tcx>, state: S as state)]
34#[derive(Debug, Clone, PartialEq, Eq, Hash)]
35pub struct ExistentialProjection<'tcx> {
36    pub def_id: DefId,
37    pub args: Vec<GenericArg<'tcx>>,
38    pub term: Term<'tcx>,
39}
40
41impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, GenericPredicate<'tcx>>
42    for rustc_trait_elaboration::DynPredicate<'tcx, DefId>
43{
44    fn sinto(&self, s: &S) -> GenericPredicate<'tcx> {
45        let tcx = s.base().tcx;
46        let pred = &self.predicate;
47        if let Some(projection) = pred.clause.as_projection_clause() {
48            let trait_proof = self
49                .projection_trait_proof
50                .expect("projection predicates should have a trait proof")
51                .sinto(s);
52            let bound_vars = projection.bound_vars().sinto(s);
53            let projection = projection.skip_binder();
54            let alias_ty = projection.projection_term.expect_ty();
55            let Term::Ty(ty) = projection.term.sinto(s) else {
56                unreachable!()
57            };
58            let item = tcx.associated_item(alias_ty_kind_def_id(alias_ty.kind));
59            GenericPredicate {
60                id: pred.id.sinto(s),
61                clause: Clause {
62                    kind: Binder {
63                        value: ClauseKind::Projection(ProjectionPredicate {
64                            trait_proof,
65                            assoc_item: AssocItem::sfrom(s, &item),
66                            ty,
67                        }),
68                        bound_vars,
69                    },
70                },
71                span: pred.span.sinto(s),
72            }
73        } else {
74            assert!(self.projection_trait_proof.is_none());
75            pred.sinto(s)
76        }
77    }
78}
79
80pub(super) fn resolve_for_dyn<'tcx, S, T, U>(
81    s: &S,
82    epreds: &'tcx ty::List<ty::Binder<'tcx, ty::ExistentialPredicate<'tcx>>>,
83    f: impl FnOnce(&mut PredicateSearcher<'tcx>, ty::Ty<'tcx>) -> T,
84) -> DynBinder<'tcx, U>
85where
86    S: UnderOwnerState<'tcx>,
87    T: SInto<S, U>,
88{
89    s.with_predicate_searcher(|searcher, state| searcher.resolve_for_dyn(state, epreds, f))
90        .sinto(s)
91}
92
93/// Reflects [`ty::TraitClause`]
94#[derive(AdtInto)]
95#[args(< S: UnderOwnerState<'tcx>>, from: ty::TraitClause<'tcx>, state: S as tcx)]
96#[derive(Debug, Clone, PartialEq, Eq, Hash)]
97pub struct TraitPredicate<'tcx> {
98    pub trait_ref: TraitRef<'tcx>,
99    #[map(*x == ty::ClausePolarity::Positive)]
100    #[from(polarity)]
101    pub is_positive: bool,
102}
103
104/// Reflects [`ty::OutlivesPredicate`] as a named struct
105/// instead of a tuple struct. This is because the script converting
106/// JSONSchema types to OCaml doesn't support tuple structs, and this
107/// is the only tuple struct in the whole AST.
108#[derive(Debug, Clone, PartialEq, Eq, Hash)]
109pub struct OutlivesPredicate<T> {
110    pub lhs: T,
111    pub rhs: Region,
112}
113
114impl<'tcx, S: UnderOwnerState<'tcx>, T, U> SInto<S, OutlivesPredicate<U>>
115    for ty::OutlivesClause<'tcx, T>
116where
117    T: SInto<S, U>,
118{
119    fn sinto(&self, s: &S) -> OutlivesPredicate<U> where {
120        OutlivesPredicate {
121            lhs: self.0.sinto(s),
122            rhs: self.1.sinto(s),
123        }
124    }
125}
126
127/// Reflects [`ty::RegionOutlivesPredicate`]
128pub type RegionOutlivesPredicate = OutlivesPredicate<Region>;
129/// Reflects [`ty::TypeOutlivesPredicate`]
130pub type TypeOutlivesPredicate<'tcx> = OutlivesPredicate<Ty<'tcx>>;
131
132/// Reflects [`ty::Term`]
133#[derive(Debug, Clone, PartialEq, Eq, Hash)]
134pub enum Term<'tcx> {
135    Ty(Ty<'tcx>),
136    Const(ConstantExpr<'tcx>),
137}
138
139impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Term<'tcx>> for ty::Term<'tcx> {
140    fn sinto(&self, s: &S) -> Term<'tcx> {
141        use ty::TermKind;
142        match self.kind() {
143            TermKind::Ty(ty) => Term::Ty(ty.sinto(s)),
144            TermKind::Const(c) => Term::Const(c.sinto(s)),
145        }
146    }
147}
148
149/// Expresses a constraints over an associated type.
150///
151/// For instance:
152/// ```text
153/// fn f<T : Foo<S = String>>(...)
154///              ^^^^^^^^^^
155/// ```
156/// (provided the trait `Foo` has an associated type `S`).
157#[derive(Debug, Clone, PartialEq, Eq, Hash)]
158pub struct ProjectionPredicate<'tcx> {
159    /// The `impl Trait for Ty` in `Ty: Trait<..., Type = U>`.
160    pub trait_proof: TraitProof<'tcx>,
161    /// The `Type` in `Ty: Trait<..., Type = U>`.
162    pub assoc_item: AssocItem<'tcx>,
163    /// The type `U` in `Ty: Trait<..., Type = U>`.
164    pub ty: Ty<'tcx>,
165}
166
167impl<'tcx, S: UnderOwnerState<'tcx>> SInto<(S, UnitBinder<'tcx>), ProjectionPredicate<'tcx>>
168    for ty::ProjectionClause<'tcx>
169{
170    fn sinto(&self, s: &(S, UnitBinder<'tcx>)) -> ProjectionPredicate<'tcx> {
171        let tcx = s.base().tcx;
172        let alias_ty = &self.projection_term.expect_ty();
173        let poly_trait_ref = s.1.rebind(alias_ty.trait_ref(tcx));
174        let Term::Ty(ty) = self.term.sinto(s) else {
175            unreachable!()
176        };
177        let item = tcx.associated_item(alias_ty_kind_def_id(alias_ty.kind));
178        ProjectionPredicate {
179            trait_proof: solve_trait(s, poly_trait_ref),
180            assoc_item: AssocItem::sfrom(s, &item),
181            ty,
182        }
183    }
184}
185
186/// Reflects [`ty::ClauseKind`]
187#[derive(AdtInto)]
188#[args(< S: UnderOwnerState<'tcx>>, from: ty::ClauseKind<'tcx>, state: (S, UnitBinder<'tcx>) as tcx)]
189#[derive(Debug, Clone, PartialEq, Eq, Hash)]
190pub enum ClauseKind<'tcx> {
191    Trait(TraitPredicate<'tcx>),
192    RegionOutlives(RegionOutlivesPredicate),
193    TypeOutlives(TypeOutlivesPredicate<'tcx>),
194    Projection(ProjectionPredicate<'tcx>),
195    ConstArgHasType(ConstantExpr<'tcx>, Ty<'tcx>),
196    WellFormed(Term<'tcx>),
197    ConstEvaluatable(ConstantExpr<'tcx>),
198    HostEffect(HostEffectClause),
199    UnstableFeature(Symbol),
200}
201
202sinto_todo!(rustc_middle::ty, HostEffectClause<'tcx>);
203
204/// Reflects [`ty::Clause`] and adds a hash-consed predicate identifier.
205#[derive(Debug, Clone, PartialEq, Eq, Hash)]
206pub struct Clause<'tcx> {
207    pub kind: Binder<ClauseKind<'tcx>>,
208}
209
210impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause<'tcx>> for ty::Clause<'tcx> {
211    fn sinto(&self, s: &S) -> Clause<'tcx> {
212        let kind = self.kind().sinto(s);
213        Clause { kind }
214    }
215}
216
217impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Clause<'tcx>> for ty::PolyTraitClause<'tcx> {
218    fn sinto(&self, s: &S) -> Clause<'tcx> {
219        let kind: Binder<_> = self.sinto(s);
220        let kind: Binder<ClauseKind> = kind.map(ClauseKind::Trait);
221        Clause { kind }
222    }
223}
224
225/// Reflects [`ty::Predicate`] and adds a hash-consed predicate identifier.
226#[derive(Debug, Clone, PartialEq, Eq, Hash)]
227pub struct Predicate<'tcx> {
228    pub kind: Binder<PredicateKind<'tcx>>,
229}
230
231impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Predicate<'tcx>> for ty::Predicate<'tcx> {
232    fn sinto(&self, s: &S) -> Predicate<'tcx> {
233        let kind = self.kind().sinto(s);
234        Predicate { kind }
235    }
236}
237
238/// Uniquely identifies a predicate.
239#[derive(AdtInto)]
240#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: traits::ItemPredicateId<DefId>, state: S as s)]
241#[derive(Debug, Clone, PartialEq, Eq, Hash)]
242pub enum GenericPredicateId {
243    /// A predicate that counts as "input" for an item, e.g. `where` clauses on a function or impl.
244    /// Numbered in some arbitrary but consistent order.
245    Required(DefId, u32),
246    /// A predicate that counts as "output" of an item, e.g. supertrait clauses in a trait. Note
247    /// that we count `where` clauses on a trait as implied.
248    /// Numbered in some arbitrary but consistent order.
249    Implied(DefId, u32),
250    /// Predicate inside a non-item binder, e.g. within a `dyn Trait`.
251    /// Numbered in some arbitrary but consistent order.
252    Unmapped(u32),
253    /// The special `Self: Trait` clause available within trait `Trait`.
254    TraitSelf,
255}
256
257#[derive(AdtInto)]
258#[args(< S: UnderOwnerState<'tcx>>, from: traits::ItemPredicate<'tcx, DefId>, state: S as s)]
259#[derive(Debug, Clone, PartialEq, Eq, Hash)]
260pub struct GenericPredicate<'tcx> {
261    pub id: GenericPredicateId,
262    pub clause: Clause<'tcx>,
263    pub span: Span,
264}
265
266/// Reflects [`ty::GenericPredicates`]
267#[derive(AdtInto)]
268#[args(< S: UnderOwnerState<'tcx>>, from: traits::ItemPredicates<'tcx, DefId>, state: S as s)]
269#[derive(Debug, Default, Clone, PartialEq, Eq, Hash)]
270pub struct GenericPredicates<'tcx> {
271    pub predicates: Vec<GenericPredicate<'tcx>>,
272}
273
274impl<'tcx> GenericPredicates<'tcx> {
275    pub fn iter(&self) -> impl Iterator<Item = &GenericPredicate<'tcx>> {
276        self.predicates.iter()
277    }
278    /// Iter only on trait clauses.
279    pub fn iter_trait_clauses(&self) -> impl Iterator<Item = &GenericPredicate<'tcx>> {
280        self.iter().filter(move |pred| {
281            matches!(pred.clause.kind.hax_skip_binder_ref(), ClauseKind::Trait(_))
282        })
283    }
284}
285
286/// Reflects [`ty::SubtypePredicate`]
287#[derive(AdtInto)]
288#[args(< S: UnderOwnerState<'tcx>>, from: ty::SubtypePredicate<'tcx>, state: S as tcx)]
289#[derive(Debug, Clone, PartialEq, Eq, Hash)]
290pub struct SubtypePredicate<'tcx> {
291    pub a_is_expected: bool,
292    pub a: Ty<'tcx>,
293    pub b: Ty<'tcx>,
294}
295
296/// Reflects [`ty::CoercePredicate`]
297#[derive(AdtInto)]
298#[args(< S: UnderOwnerState<'tcx>>, from: ty::CoercePredicate<'tcx>, state: S as tcx)]
299#[derive(Debug, Clone, PartialEq, Eq, Hash)]
300pub struct CoercePredicate<'tcx> {
301    pub a: Ty<'tcx>,
302    pub b: Ty<'tcx>,
303}
304
305sinto_todo!(rustc_middle::ty, NormalizesTo<'tcx>);
306
307/// Reflects [`ty::PredicateKind`]
308#[derive(AdtInto)]
309#[args(< S: UnderOwnerState<'tcx>>, from: ty::PredicateKind<'tcx>, state: (S, UnitBinder<'tcx>) as tcx)]
310#[derive(Debug, Clone, PartialEq, Eq, Hash)]
311pub enum PredicateKind<'tcx> {
312    Clause(ClauseKind<'tcx>),
313    DynCompatible(DefId),
314    Subtype(SubtypePredicate<'tcx>),
315    Coerce(CoercePredicate<'tcx>),
316    ConstEquate(ConstantExpr<'tcx>, ConstantExpr<'tcx>),
317    Ambiguous,
318    NormalizesTo(NormalizesTo),
319}
charon_driver/hax/types/predicates.rs

charon_driver/hax/types/
predicates.rs
