flux_middle/rty/
mod.rs

1//! Defines how flux represents refinement types internally. Definitions in this module are used
2//! during refinement type checking. A couple of important differences between definitions in this
3//! module and in [`crate::fhir`] are:
4//!
5//! * Types in this module use debruijn indices to represent local binders.
6//! * Data structures are interned so they can be cheaply cloned.
7mod binder;
8pub mod canonicalize;
9mod expr;
10pub mod fold;
11pub mod normalize;
12mod pretty;
13pub mod refining;
14pub mod region_matching;
15pub mod subst;
16use std::{borrow::Cow, cmp::Ordering, fmt, hash::Hash, sync::LazyLock};
17
18pub use SortInfer::*;
19pub use binder::{Binder, BoundReftKind, BoundVariableKind, BoundVariableKinds, EarlyBinder};
20pub use expr::{
21    AggregateKind, AliasReft, BinOp, BoundReft, Constant, Ctor, ESpan, EVid, EarlyReftParam, Expr,
22    ExprKind, FieldProj, HoleKind, InternalFuncKind, KVar, KVid, Lambda, Loc, Name, Path, Real,
23    SpecFuncKind, UnOp, Var,
24};
25pub use flux_arc_interner::List;
26use flux_arc_interner::{Interned, impl_internable, impl_slice_internable};
27use flux_common::{bug, tracked_span_assert_eq, tracked_span_bug};
28use flux_config::OverflowMode;
29use flux_macros::{TypeFoldable, TypeVisitable};
30pub use flux_rustc_bridge::ty::{
31    AliasKind, BoundRegion, BoundRegionKind, BoundVar, Const, ConstKind, ConstVid, DebruijnIndex,
32    EarlyParamRegion, LateParamRegion, LateParamRegionKind,
33    Region::{self, *},
34    RegionVid,
35};
36use flux_rustc_bridge::{
37    ToRustc,
38    mir::{Place, RawPtrKind},
39    ty::{self, GenericArgsExt as _, VariantDef},
40};
41use itertools::Itertools;
42pub use normalize::{NormalizeInfo, NormalizedDefns, local_deps};
43use refining::{Refine as _, Refiner};
44use rustc_abi;
45pub use rustc_abi::{FIRST_VARIANT, VariantIdx};
46use rustc_data_structures::{fx::FxIndexMap, snapshot_map::SnapshotMap, unord::UnordMap};
47use rustc_hir::{LangItem, Safety, def_id::DefId};
48use rustc_index::{IndexSlice, IndexVec, newtype_index};
49use rustc_macros::{Decodable, Encodable, TyDecodable, TyEncodable, extension};
50use rustc_middle::ty::TyCtxt;
51pub use rustc_middle::{
52    mir::Mutability,
53    ty::{AdtFlags, ClosureKind, FloatTy, IntTy, ParamConst, ParamTy, ScalarInt, UintTy},
54};
55use rustc_span::{DUMMY_SP, Span, Symbol, sym, symbol::kw};
56use rustc_type_ir::Upcast as _;
57pub use rustc_type_ir::{INNERMOST, TyVid};
58
59use self::fold::TypeFoldable;
60pub use crate::fhir::InferMode;
61use crate::{
62    LocalDefId,
63    def_id::{FluxDefId, FluxLocalDefId},
64    fhir::{self, FhirId, FluxOwnerId},
65    global_env::GlobalEnv,
66    pretty::{Pretty, PrettyCx},
67    queries::{QueryErr, QueryResult},
68    rty::subst::SortSubst,
69};
70
71/// The definition of the data sort automatically generated for a struct or enum.
72#[derive(Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
73pub struct AdtSortDef(Interned<AdtSortDefData>);
74
75#[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
76pub struct AdtSortVariant {
77    /// The list of field names as declared in the `#[flux::refined_by(...)]` annotation
78    field_names: Vec<Symbol>,
79    /// The sort of each of the fields. Note that these can contain [sort variables]. Methods used
80    /// to access these sorts guarantee they are properly instantiated.
81    ///
82    /// [sort variables]: Sort::Var
83    sorts: List<Sort>,
84}
85
86impl AdtSortVariant {
87    pub fn new(fields: Vec<(Symbol, Sort)>) -> Self {
88        let (field_names, sorts) = fields.into_iter().unzip();
89        AdtSortVariant { field_names, sorts: List::from_vec(sorts) }
90    }
91
92    pub fn fields(&self) -> usize {
93        self.sorts.len()
94    }
95
96    pub fn field_names(&self) -> &Vec<Symbol> {
97        &self.field_names
98    }
99
100    pub fn sort_by_field_name(&self, args: &[Sort]) -> FxIndexMap<Symbol, Sort> {
101        std::iter::zip(&self.field_names, &self.sorts.fold_with(&mut SortSubst::new(args)))
102            .map(|(name, sort)| (*name, sort.clone()))
103            .collect()
104    }
105
106    pub fn field_by_name(
107        &self,
108        def_id: DefId,
109        args: &[Sort],
110        name: Symbol,
111    ) -> Option<(FieldProj, Sort)> {
112        let idx = self.field_names.iter().position(|it| name == *it)?;
113        let proj = FieldProj::Adt { def_id, field: idx as u32 };
114        let sort = self.sorts[idx].fold_with(&mut SortSubst::new(args));
115        Some((proj, sort))
116    }
117
118    pub fn field_sorts(&self, args: &[Sort]) -> List<Sort> {
119        self.sorts.fold_with(&mut SortSubst::new(args))
120    }
121
122    pub fn projections(&self, def_id: DefId) -> impl Iterator<Item = FieldProj> {
123        (0..self.fields()).map(move |i| FieldProj::Adt { def_id, field: i as u32 })
124    }
125}
126
127#[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
128struct AdtSortDefData {
129    /// [`DefId`] of the struct or enum this data sort is associated to.
130    def_id: DefId,
131    /// The list of the type parameters used in the `#[flux::refined_by(..)]` annotation.
132    ///
133    /// See [`fhir::RefinedBy::sort_params`] for more details. This is a version of that but using
134    /// [`ParamTy`] instead of [`DefId`].
135    ///
136    /// The length of this list corresponds to the number of sort variables bound by this definition.
137    params: Vec<ParamTy>,
138    /// A vec of variants of the ADT;
139    /// - a `struct` sort -- used for types with a `refined_by` has a single variant;
140    /// - a `reflected` sort -- used for `reflected` enums have multiple variants
141    variants: IndexVec<VariantIdx, AdtSortVariant>,
142    is_reflected: bool,
143    is_struct: bool,
144}
145
146impl AdtSortDef {
147    pub fn new(
148        def_id: DefId,
149        params: Vec<ParamTy>,
150        variants: IndexVec<VariantIdx, AdtSortVariant>,
151        is_reflected: bool,
152        is_struct: bool,
153    ) -> Self {
154        Self(Interned::new(AdtSortDefData { def_id, params, variants, is_reflected, is_struct }))
155    }
156
157    pub fn did(&self) -> DefId {
158        self.0.def_id
159    }
160
161    pub fn variant(&self, idx: VariantIdx) -> &AdtSortVariant {
162        &self.0.variants[idx]
163    }
164
165    pub fn variants(&self) -> &IndexSlice<VariantIdx, AdtSortVariant> {
166        &self.0.variants
167    }
168
169    pub fn opt_struct_variant(&self) -> Option<&AdtSortVariant> {
170        if self.is_struct() { Some(self.struct_variant()) } else { None }
171    }
172
173    #[track_caller]
174    pub fn struct_variant(&self) -> &AdtSortVariant {
175        tracked_span_assert_eq!(self.0.is_struct, true);
176        &self.0.variants[FIRST_VARIANT]
177    }
178
179    pub fn is_reflected(&self) -> bool {
180        self.0.is_reflected
181    }
182
183    pub fn is_struct(&self) -> bool {
184        self.0.is_struct
185    }
186
187    pub fn to_sort(&self, args: &[GenericArg]) -> Sort {
188        let sorts = self
189            .filter_generic_args(args)
190            .map(|arg| arg.expect_base().sort())
191            .collect();
192
193        Sort::App(SortCtor::Adt(self.clone()), sorts)
194    }
195
196    /// Given a list of generic args, returns an iterator of the generic arguments that should be
197    /// mapped to sorts for instantiation.
198    pub fn filter_generic_args<'a, A>(&'a self, args: &'a [A]) -> impl Iterator<Item = &'a A> + 'a {
199        self.0.params.iter().map(|p| &args[p.index as usize])
200    }
201
202    pub fn identity_args(&self) -> List<Sort> {
203        (0..self.0.params.len())
204            .map(|i| Sort::Var(ParamSort::from(i)))
205            .collect()
206    }
207
208    /// Gives the number of sort variables bound by this definition.
209    pub fn param_count(&self) -> usize {
210        self.0.params.len()
211    }
212}
213
214#[derive(Debug, Clone, Default, Encodable, Decodable)]
215pub struct Generics {
216    pub parent: Option<DefId>,
217    pub parent_count: usize,
218    pub own_params: List<GenericParamDef>,
219    pub has_self: bool,
220}
221
222impl Generics {
223    pub fn count(&self) -> usize {
224        self.parent_count + self.own_params.len()
225    }
226
227    pub fn own_default_count(&self) -> usize {
228        self.own_params
229            .iter()
230            .filter(|param| {
231                match param.kind {
232                    GenericParamDefKind::Type { has_default }
233                    | GenericParamDefKind::Const { has_default }
234                    | GenericParamDefKind::Base { has_default } => has_default,
235                    GenericParamDefKind::Lifetime => false,
236                }
237            })
238            .count()
239    }
240
241    pub fn param_at(&self, param_index: usize, genv: GlobalEnv) -> QueryResult<GenericParamDef> {
242        if let Some(index) = param_index.checked_sub(self.parent_count) {
243            Ok(self.own_params[index].clone())
244        } else {
245            let parent = self.parent.expect("parent_count > 0 but no parent?");
246            genv.generics_of(parent)?.param_at(param_index, genv)
247        }
248    }
249
250    pub fn const_params(&self, genv: GlobalEnv) -> QueryResult<Vec<(ParamConst, Sort)>> {
251        // FIXME(nilehmann) this shouldn't use the methods in `flux_middle::sort_of` to get the sort
252        let mut res = vec![];
253        for i in 0..self.count() {
254            let param = self.param_at(i, genv)?;
255            if let GenericParamDefKind::Const { .. } = param.kind
256                && let Some(sort) = genv.sort_of_generic_param(param.def_id)?
257            {
258                let param_const = ParamConst { name: param.name, index: param.index };
259                res.push((param_const, sort));
260            }
261        }
262        Ok(res)
263    }
264}
265
266#[derive(Debug, Clone, TyEncodable, TyDecodable)]
267pub struct RefinementGenerics {
268    pub parent: Option<DefId>,
269    pub parent_count: usize,
270    pub own_params: List<RefineParam>,
271}
272
273#[derive(
274    PartialEq, Eq, Debug, Clone, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
275)]
276pub struct RefineParam {
277    pub sort: Sort,
278    pub name: Symbol,
279    pub mode: InferMode,
280}
281
282#[derive(Debug, Clone, PartialEq, Eq, Hash, Encodable, Decodable)]
283pub struct GenericParamDef {
284    pub kind: GenericParamDefKind,
285    pub def_id: DefId,
286    pub index: u32,
287    pub name: Symbol,
288}
289
290#[derive(Copy, Debug, Clone, PartialEq, Eq, Hash, Encodable, Decodable)]
291pub enum GenericParamDefKind {
292    Type { has_default: bool },
293    Base { has_default: bool },
294    Lifetime,
295    Const { has_default: bool },
296}
297
298pub const SELF_PARAM_TY: ParamTy = ParamTy { index: 0, name: kw::SelfUpper };
299
300#[derive(Debug, Clone, TyEncodable, TyDecodable)]
301pub struct GenericPredicates {
302    pub parent: Option<DefId>,
303    pub predicates: List<Clause>,
304}
305
306#[derive(
307    Debug, PartialEq, Eq, Hash, Clone, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
308)]
309pub struct Clause {
310    kind: Binder<ClauseKind>,
311}
312
313impl Clause {
314    pub fn new(vars: impl Into<List<BoundVariableKind>>, kind: ClauseKind) -> Self {
315        Clause { kind: Binder::bind_with_vars(kind, vars.into()) }
316    }
317
318    pub fn kind(&self) -> Binder<ClauseKind> {
319        self.kind.clone()
320    }
321
322    fn as_trait_clause(&self) -> Option<Binder<TraitPredicate>> {
323        let clause = self.kind();
324        if let ClauseKind::Trait(trait_clause) = clause.skip_binder_ref() {
325            Some(clause.rebind(trait_clause.clone()))
326        } else {
327            None
328        }
329    }
330
331    pub fn as_projection_clause(&self) -> Option<Binder<ProjectionPredicate>> {
332        let clause = self.kind();
333        if let ClauseKind::Projection(proj_clause) = clause.skip_binder_ref() {
334            Some(clause.rebind(proj_clause.clone()))
335        } else {
336            None
337        }
338    }
339
340    // FIXME(nilehmann) we should deal with the binder in all the places this is used instead of
341    // blindly skipping it here
342    pub fn kind_skipping_binder(&self) -> ClauseKind {
343        self.kind.clone().skip_binder()
344    }
345
346    /// Group `Fn` trait clauses with their corresponding `FnOnce::Output` projection
347    /// predicate. This assumes there's exactly one corresponding projection predicate and will
348    /// crash otherwise.
349    pub fn split_off_fn_trait_clauses(
350        genv: GlobalEnv,
351        clauses: &Clauses,
352    ) -> (Vec<Clause>, Vec<Binder<FnTraitPredicate>>) {
353        let mut fn_trait_clauses = vec![];
354        let mut fn_trait_output_clauses = vec![];
355        let mut rest = vec![];
356        for clause in clauses {
357            if let Some(trait_clause) = clause.as_trait_clause()
358                && let Some(kind) = genv.tcx().fn_trait_kind_from_def_id(trait_clause.def_id())
359            {
360                fn_trait_clauses.push((kind, trait_clause));
361            } else if let Some(proj_clause) = clause.as_projection_clause()
362                && genv.is_fn_output(proj_clause.projection_def_id())
363            {
364                fn_trait_output_clauses.push(proj_clause);
365            } else {
366                rest.push(clause.clone());
367            }
368        }
369        let fn_trait_clauses = fn_trait_clauses
370            .into_iter()
371            .map(|(kind, fn_trait_clause)| {
372                let mut candidates = vec![];
373                for fn_trait_output_clause in &fn_trait_output_clauses {
374                    if fn_trait_output_clause.self_ty() == fn_trait_clause.self_ty() {
375                        candidates.push(fn_trait_output_clause.clone());
376                    }
377                }
378                tracked_span_assert_eq!(candidates.len(), 1);
379                let proj_pred = candidates.pop().unwrap().skip_binder();
380                fn_trait_clause.map(|fn_trait_clause| {
381                    FnTraitPredicate {
382                        kind,
383                        self_ty: fn_trait_clause.self_ty().to_ty(),
384                        tupled_args: fn_trait_clause.trait_ref.args[1].expect_base().to_ty(),
385                        output: proj_pred.term.to_ty(),
386                    }
387                })
388            })
389            .collect_vec();
390        (rest, fn_trait_clauses)
391    }
392}
393
394impl<'tcx> ToRustc<'tcx> for Clause {
395    type T = rustc_middle::ty::Clause<'tcx>;
396
397    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
398        self.kind.to_rustc(tcx).upcast(tcx)
399    }
400}
401
402impl From<Binder<ClauseKind>> for Clause {
403    fn from(kind: Binder<ClauseKind>) -> Self {
404        Clause { kind }
405    }
406}
407
408pub type Clauses = List<Clause>;
409
410#[derive(
411    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
412)]
413pub enum ClauseKind {
414    Trait(TraitPredicate),
415    Projection(ProjectionPredicate),
416    RegionOutlives(RegionOutlivesPredicate),
417    TypeOutlives(TypeOutlivesPredicate),
418    ConstArgHasType(Const, Ty),
419}
420
421impl<'tcx> ToRustc<'tcx> for ClauseKind {
422    type T = rustc_middle::ty::ClauseKind<'tcx>;
423
424    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
425        match self {
426            ClauseKind::Trait(trait_predicate) => {
427                rustc_middle::ty::ClauseKind::Trait(trait_predicate.to_rustc(tcx))
428            }
429            ClauseKind::Projection(projection_predicate) => {
430                rustc_middle::ty::ClauseKind::Projection(projection_predicate.to_rustc(tcx))
431            }
432            ClauseKind::RegionOutlives(outlives_predicate) => {
433                rustc_middle::ty::ClauseKind::RegionOutlives(outlives_predicate.to_rustc(tcx))
434            }
435            ClauseKind::TypeOutlives(outlives_predicate) => {
436                rustc_middle::ty::ClauseKind::TypeOutlives(outlives_predicate.to_rustc(tcx))
437            }
438            ClauseKind::ConstArgHasType(constant, ty) => {
439                rustc_middle::ty::ClauseKind::ConstArgHasType(
440                    constant.to_rustc(tcx),
441                    ty.to_rustc(tcx),
442                )
443            }
444        }
445    }
446}
447
448#[derive(Eq, PartialEq, Hash, Clone, Debug, TyEncodable, TyDecodable)]
449pub struct OutlivesPredicate<T>(pub T, pub Region);
450
451pub type TypeOutlivesPredicate = OutlivesPredicate<Ty>;
452pub type RegionOutlivesPredicate = OutlivesPredicate<Region>;
453
454impl<'tcx, V: ToRustc<'tcx>> ToRustc<'tcx> for OutlivesPredicate<V> {
455    type T = rustc_middle::ty::OutlivesPredicate<'tcx, V::T>;
456
457    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
458        rustc_middle::ty::OutlivesPredicate(self.0.to_rustc(tcx), self.1.to_rustc(tcx))
459    }
460}
461
462#[derive(
463    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
464)]
465pub struct TraitPredicate {
466    pub trait_ref: TraitRef,
467}
468
469impl TraitPredicate {
470    fn self_ty(&self) -> SubsetTyCtor {
471        self.trait_ref.self_ty()
472    }
473}
474
475impl<'tcx> ToRustc<'tcx> for TraitPredicate {
476    type T = rustc_middle::ty::TraitPredicate<'tcx>;
477
478    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
479        rustc_middle::ty::TraitPredicate {
480            polarity: rustc_middle::ty::PredicatePolarity::Positive,
481            trait_ref: self.trait_ref.to_rustc(tcx),
482        }
483    }
484}
485
486pub type PolyTraitPredicate = Binder<TraitPredicate>;
487
488impl PolyTraitPredicate {
489    fn def_id(&self) -> DefId {
490        self.skip_binder_ref().trait_ref.def_id
491    }
492
493    fn self_ty(&self) -> Binder<SubsetTyCtor> {
494        self.clone().map(|predicate| predicate.self_ty())
495    }
496}
497
498#[derive(
499    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
500)]
501pub struct TraitRef {
502    pub def_id: DefId,
503    pub args: GenericArgs,
504}
505
506impl TraitRef {
507    pub fn self_ty(&self) -> SubsetTyCtor {
508        self.args[0].expect_base().clone()
509    }
510}
511
512impl<'tcx> ToRustc<'tcx> for TraitRef {
513    type T = rustc_middle::ty::TraitRef<'tcx>;
514
515    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
516        rustc_middle::ty::TraitRef::new(tcx, self.def_id, self.args.to_rustc(tcx))
517    }
518}
519
520pub type PolyTraitRef = Binder<TraitRef>;
521
522impl PolyTraitRef {
523    pub fn def_id(&self) -> DefId {
524        self.as_ref().skip_binder().def_id
525    }
526}
527
528#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
529pub enum ExistentialPredicate {
530    Trait(ExistentialTraitRef),
531    Projection(ExistentialProjection),
532    AutoTrait(DefId),
533}
534
535pub type PolyExistentialPredicate = Binder<ExistentialPredicate>;
536
537impl ExistentialPredicate {
538    /// See [`rustc_middle::ty::ExistentialPredicateStableCmpExt`]
539    pub fn stable_cmp(&self, tcx: TyCtxt, other: &Self) -> Ordering {
540        match (self, other) {
541            (ExistentialPredicate::Trait(_), ExistentialPredicate::Trait(_)) => Ordering::Equal,
542            (ExistentialPredicate::Projection(a), ExistentialPredicate::Projection(b)) => {
543                tcx.def_path_hash(a.def_id)
544                    .cmp(&tcx.def_path_hash(b.def_id))
545            }
546            (ExistentialPredicate::AutoTrait(a), ExistentialPredicate::AutoTrait(b)) => {
547                tcx.def_path_hash(*a).cmp(&tcx.def_path_hash(*b))
548            }
549            (ExistentialPredicate::Trait(_), _) => Ordering::Less,
550            (ExistentialPredicate::Projection(_), ExistentialPredicate::Trait(_)) => {
551                Ordering::Greater
552            }
553            (ExistentialPredicate::Projection(_), _) => Ordering::Less,
554            (ExistentialPredicate::AutoTrait(_), _) => Ordering::Greater,
555        }
556    }
557}
558
559impl<'tcx> ToRustc<'tcx> for ExistentialPredicate {
560    type T = rustc_middle::ty::ExistentialPredicate<'tcx>;
561
562    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
563        match self {
564            ExistentialPredicate::Trait(trait_ref) => {
565                let trait_ref = rustc_middle::ty::ExistentialTraitRef::new_from_args(
566                    tcx,
567                    trait_ref.def_id,
568                    trait_ref.args.to_rustc(tcx),
569                );
570                rustc_middle::ty::ExistentialPredicate::Trait(trait_ref)
571            }
572            ExistentialPredicate::Projection(projection) => {
573                rustc_middle::ty::ExistentialPredicate::Projection(
574                    rustc_middle::ty::ExistentialProjection::new_from_args(
575                        tcx,
576                        projection.def_id,
577                        projection.args.to_rustc(tcx),
578                        projection.term.skip_binder_ref().to_rustc(tcx).into(),
579                    ),
580                )
581            }
582            ExistentialPredicate::AutoTrait(def_id) => {
583                rustc_middle::ty::ExistentialPredicate::AutoTrait(*def_id)
584            }
585        }
586    }
587}
588
589#[derive(
590    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
591)]
592pub struct ExistentialTraitRef {
593    pub def_id: DefId,
594    pub args: GenericArgs,
595}
596
597pub type PolyExistentialTraitRef = Binder<ExistentialTraitRef>;
598
599impl PolyExistentialTraitRef {
600    pub fn def_id(&self) -> DefId {
601        self.as_ref().skip_binder().def_id
602    }
603}
604
605#[derive(
606    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
607)]
608pub struct ExistentialProjection {
609    pub def_id: DefId,
610    pub args: GenericArgs,
611    pub term: SubsetTyCtor,
612}
613
614#[derive(
615    PartialEq, Eq, Hash, Debug, Clone, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
616)]
617pub struct ProjectionPredicate {
618    pub projection_ty: AliasTy,
619    pub term: SubsetTyCtor,
620}
621
622impl Pretty for ProjectionPredicate {
623    fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
624        write!(
625            f,
626            "ProjectionPredicate << projection_ty = {:?}, term = {:?} >>",
627            self.projection_ty, self.term
628        )
629    }
630}
631
632impl ProjectionPredicate {
633    pub fn self_ty(&self) -> SubsetTyCtor {
634        self.projection_ty.self_ty().clone()
635    }
636}
637
638impl<'tcx> ToRustc<'tcx> for ProjectionPredicate {
639    type T = rustc_middle::ty::ProjectionPredicate<'tcx>;
640
641    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
642        rustc_middle::ty::ProjectionPredicate {
643            projection_term: rustc_middle::ty::AliasTerm::new_from_args(
644                tcx,
645                self.projection_ty.def_id,
646                self.projection_ty.args.to_rustc(tcx),
647            ),
648            term: self.term.as_bty_skipping_binder().to_rustc(tcx).into(),
649        }
650    }
651}
652
653pub type PolyProjectionPredicate = Binder<ProjectionPredicate>;
654
655impl PolyProjectionPredicate {
656    pub fn projection_def_id(&self) -> DefId {
657        self.skip_binder_ref().projection_ty.def_id
658    }
659
660    pub fn self_ty(&self) -> Binder<SubsetTyCtor> {
661        self.clone().map(|predicate| predicate.self_ty())
662    }
663}
664
665#[derive(
666    Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
667)]
668pub struct FnTraitPredicate {
669    pub self_ty: Ty,
670    pub tupled_args: Ty,
671    pub output: Ty,
672    pub kind: ClosureKind,
673}
674
675impl Pretty for FnTraitPredicate {
676    fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
677        write!(
678            f,
679            "self = {:?}, args = {:?}, output = {:?}, kind = {}",
680            self.self_ty, self.tupled_args, self.output, self.kind
681        )
682    }
683}
684
685impl FnTraitPredicate {
686    pub fn fndef_sig(&self) -> FnSig {
687        let inputs = self.tupled_args.expect_tuple().iter().cloned().collect();
688        let ret = self.output.clone().shift_in_escaping(1);
689        let output = Binder::bind_with_vars(FnOutput::new(ret, vec![]), List::empty());
690        FnSig::new(Safety::Safe, rustc_abi::ExternAbi::Rust, List::empty(), inputs, output)
691    }
692}
693
694pub fn to_closure_sig(
695    tcx: TyCtxt,
696    closure_id: LocalDefId,
697    tys: &[Ty],
698    args: &flux_rustc_bridge::ty::GenericArgs,
699    poly_sig: &PolyFnSig,
700) -> PolyFnSig {
701    let closure_args = args.as_closure();
702    let kind_ty = closure_args.kind_ty().to_rustc(tcx);
703    let Some(kind) = kind_ty.to_opt_closure_kind() else {
704        bug!("to_closure_sig: expected closure kind, found {kind_ty:?}");
705    };
706
707    let mut vars = poly_sig.vars().clone().to_vec();
708    let fn_sig = poly_sig.clone().skip_binder();
709    let closure_ty = Ty::closure(closure_id.into(), tys, args);
710    let env_ty = match kind {
711        ClosureKind::Fn => {
712            vars.push(BoundVariableKind::Region(BoundRegionKind::ClosureEnv));
713            let br = BoundRegion {
714                var: BoundVar::from_usize(vars.len() - 1),
715                kind: BoundRegionKind::ClosureEnv,
716            };
717            Ty::mk_ref(ReBound(INNERMOST, br), closure_ty, Mutability::Not)
718        }
719        ClosureKind::FnMut => {
720            vars.push(BoundVariableKind::Region(BoundRegionKind::ClosureEnv));
721            let br = BoundRegion {
722                var: BoundVar::from_usize(vars.len() - 1),
723                kind: BoundRegionKind::ClosureEnv,
724            };
725            Ty::mk_ref(ReBound(INNERMOST, br), closure_ty, Mutability::Mut)
726        }
727        ClosureKind::FnOnce => closure_ty,
728    };
729
730    let inputs = std::iter::once(env_ty)
731        .chain(fn_sig.inputs().iter().cloned())
732        .collect::<Vec<_>>();
733    let output = fn_sig.output().clone();
734
735    let fn_sig = crate::rty::FnSig::new(
736        fn_sig.safety,
737        fn_sig.abi,
738        fn_sig.requires.clone(), // crate::rty::List::empty(),
739        inputs.into(),
740        output,
741    );
742
743    PolyFnSig::bind_with_vars(fn_sig, List::from(vars))
744}
745
746#[derive(
747    Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
748)]
749pub struct CoroutineObligPredicate {
750    pub def_id: DefId,
751    pub resume_ty: Ty,
752    pub upvar_tys: List<Ty>,
753    pub output: Ty,
754}
755
756#[derive(Copy, Clone, Encodable, Decodable, Hash, PartialEq, Eq)]
757pub struct AssocReft {
758    pub def_id: FluxDefId,
759    // NOTE: Field is used to denote final associated generic refinements on Traits
760    pub final_: bool,
761    pub span: Span,
762}
763
764impl AssocReft {
765    pub fn new(def_id: FluxDefId, final_: bool, span: Span) -> Self {
766        Self { def_id, final_, span }
767    }
768
769    pub fn name(&self) -> Symbol {
770        self.def_id.name()
771    }
772
773    pub fn def_id(&self) -> FluxDefId {
774        self.def_id
775    }
776}
777
778#[derive(Clone, Encodable, Decodable)]
779pub struct AssocRefinements {
780    pub items: List<AssocReft>,
781}
782
783impl Default for AssocRefinements {
784    fn default() -> Self {
785        Self { items: List::empty() }
786    }
787}
788
789impl AssocRefinements {
790    pub fn get(&self, assoc_id: FluxDefId) -> AssocReft {
791        *self
792            .items
793            .into_iter()
794            .find(|it| it.def_id == assoc_id)
795            .unwrap_or_else(|| bug!("caller should guarantee existence of associated refinement"))
796    }
797
798    pub fn find(&self, name: Symbol) -> Option<AssocReft> {
799        Some(*self.items.into_iter().find(|it| it.name() == name)?)
800    }
801}
802
803#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
804pub enum SortCtor {
805    Set,
806    Map,
807    Adt(AdtSortDef),
808    User { name: Symbol },
809}
810
811newtype_index! {
812    /// [`ParamSort`] is used for polymorphic sorts (`Set`, `Map`, etc.) and [bit-vector size parameters].
813    /// They should occur "bound" under a [`PolyFuncSort`] or an [`AdtSortDef`]. We assume there's a
814    /// single binder and a [`ParamSort`] represents a variable as an index into the list of variables
815    /// bound by that binder, i.e., the representation doesnt't support higher-ranked sorts.
816    ///
817    /// [bit-vector size parameters]: BvSize::Param
818    #[debug_format = "?{}s"]
819    #[encodable]
820    pub struct ParamSort {}
821}
822
823newtype_index! {
824    /// A *sort* *v*variable *id*
825    #[debug_format = "?{}s"]
826    #[encodable]
827    pub struct SortVid {}
828}
829
830impl ena::unify::UnifyKey for SortVid {
831    type Value = Option<Sort>;
832
833    #[inline]
834    fn index(&self) -> u32 {
835        self.as_u32()
836    }
837
838    #[inline]
839    fn from_index(u: u32) -> Self {
840        SortVid::from_u32(u)
841    }
842
843    fn tag() -> &'static str {
844        "SortVid"
845    }
846}
847
848impl ena::unify::EqUnifyValue for Sort {}
849
850newtype_index! {
851    /// A *num*eric *v*variable *id*
852    #[debug_format = "?{}n"]
853    #[encodable]
854    pub struct NumVid {}
855}
856
857#[derive(Debug, Clone, Copy, PartialEq, Eq)]
858pub enum NumVarValue {
859    Real,
860    Int,
861    BitVec(BvSize),
862}
863
864impl NumVarValue {
865    pub fn to_sort(self) -> Sort {
866        match self {
867            NumVarValue::Real => Sort::Real,
868            NumVarValue::Int => Sort::Int,
869            NumVarValue::BitVec(size) => Sort::BitVec(size),
870        }
871    }
872}
873
874impl ena::unify::UnifyKey for NumVid {
875    type Value = Option<NumVarValue>;
876
877    #[inline]
878    fn index(&self) -> u32 {
879        self.as_u32()
880    }
881
882    #[inline]
883    fn from_index(u: u32) -> Self {
884        NumVid::from_u32(u)
885    }
886
887    fn tag() -> &'static str {
888        "NumVid"
889    }
890}
891
892impl ena::unify::EqUnifyValue for NumVarValue {}
893
894/// A placeholder for a sort that needs to be inferred
895#[derive(PartialEq, Eq, Clone, Copy, Hash, Encodable, Decodable)]
896pub enum SortInfer {
897    /// A sort variable.
898    SortVar(SortVid),
899    /// A numeric sort variable.
900    NumVar(NumVid),
901}
902
903newtype_index! {
904    /// A *b*it *v*ector *size* *v*variable *id*
905    #[debug_format = "?{}size"]
906    #[encodable]
907    pub struct BvSizeVid {}
908}
909
910impl ena::unify::UnifyKey for BvSizeVid {
911    type Value = Option<BvSize>;
912
913    #[inline]
914    fn index(&self) -> u32 {
915        self.as_u32()
916    }
917
918    #[inline]
919    fn from_index(u: u32) -> Self {
920        BvSizeVid::from_u32(u)
921    }
922
923    fn tag() -> &'static str {
924        "BvSizeVid"
925    }
926}
927
928impl ena::unify::EqUnifyValue for BvSize {}
929
930#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
931pub enum Sort {
932    Int,
933    Bool,
934    Real,
935    BitVec(BvSize),
936    Str,
937    Char,
938    Loc,
939    Param(ParamTy),
940    Tuple(List<Sort>),
941    Alias(AliasKind, AliasTy),
942    Func(PolyFuncSort),
943    App(SortCtor, List<Sort>),
944    Var(ParamSort),
945    Infer(SortInfer),
946    Err,
947}
948
949pub enum CastKind {
950    /// Identity cast, which is erasable (e.g. int -> int, char -> int)
951    Identity,
952    /// From bool to int
953    BoolToInt,
954    /// Casts to unit index, (e.g. int -> float)
955    IntoUnit,
956    /// Uninterpreted casts, only allowed with explicit flag
957    Uninterpreted,
958}
959
960impl Sort {
961    pub fn tuple(sorts: impl Into<List<Sort>>) -> Self {
962        Sort::Tuple(sorts.into())
963    }
964
965    pub fn app(ctor: SortCtor, sorts: List<Sort>) -> Self {
966        Sort::App(ctor, sorts)
967    }
968
969    pub fn unit() -> Self {
970        Self::tuple(vec![])
971    }
972
973    #[track_caller]
974    pub fn expect_func(&self) -> &PolyFuncSort {
975        if let Sort::Func(sort) = self { sort } else { bug!("expected `Sort::Func`") }
976    }
977
978    pub fn is_loc(&self) -> bool {
979        matches!(self, Sort::Loc)
980    }
981
982    pub fn is_unit(&self) -> bool {
983        matches!(self, Sort::Tuple(sorts) if sorts.is_empty())
984    }
985
986    pub fn is_unit_adt(&self) -> Option<DefId> {
987        if let Sort::App(SortCtor::Adt(sort_def), _) = self
988            && let Some(variant) = sort_def.opt_struct_variant()
989            && variant.fields() == 0
990        {
991            Some(sort_def.did())
992        } else {
993            None
994        }
995    }
996
997    /// Whether the sort is a function with return sort bool
998    pub fn is_pred(&self) -> bool {
999        matches!(self, Sort::Func(fsort) if fsort.skip_binders().output().is_bool())
1000    }
1001
1002    /// Returns `true` if the sort is [`Bool`].
1003    ///
1004    /// [`Bool`]: Sort::Bool
1005    #[must_use]
1006    pub fn is_bool(&self) -> bool {
1007        matches!(self, Self::Bool)
1008    }
1009
1010    pub fn is_numeric(&self) -> bool {
1011        matches!(self, Self::Int | Self::Real)
1012    }
1013
1014    pub fn cast_kind(self: &Sort, to: &Sort) -> CastKind {
1015        if self == to
1016            || (matches!(self, Sort::Char | Sort::Int) && matches!(to, Sort::Char | Sort::Int))
1017        {
1018            CastKind::Identity
1019        } else if matches!(self, Sort::Bool) && matches!(to, Sort::Int) {
1020            CastKind::BoolToInt
1021        } else if to.is_unit() {
1022            CastKind::IntoUnit
1023        } else {
1024            CastKind::Uninterpreted
1025        }
1026    }
1027
1028    pub fn walk(&self, mut f: impl FnMut(&Sort, &[FieldProj])) {
1029        fn go(sort: &Sort, f: &mut impl FnMut(&Sort, &[FieldProj]), proj: &mut Vec<FieldProj>) {
1030            match sort {
1031                Sort::Tuple(flds) => {
1032                    for (i, sort) in flds.iter().enumerate() {
1033                        proj.push(FieldProj::Tuple { arity: flds.len(), field: i as u32 });
1034                        go(sort, f, proj);
1035                        proj.pop();
1036                    }
1037                }
1038                Sort::App(SortCtor::Adt(sort_def), args) if sort_def.is_struct() => {
1039                    let field_sorts = sort_def.struct_variant().field_sorts(args);
1040                    for (i, sort) in field_sorts.iter().enumerate() {
1041                        proj.push(FieldProj::Adt { def_id: sort_def.did(), field: i as u32 });
1042                        go(sort, f, proj);
1043                        proj.pop();
1044                    }
1045                }
1046                _ => {
1047                    f(sort, proj);
1048                }
1049            }
1050        }
1051        go(self, &mut f, &mut vec![]);
1052    }
1053}
1054
1055/// The size of a [bit-vector]
1056///
1057/// [bit-vector]: Sort::BitVec
1058#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1059pub enum BvSize {
1060    /// A fixed size
1061    Fixed(u32),
1062    /// A size that has been parameterized, e.g., bound under a [`PolyFuncSort`]
1063    Param(ParamSort),
1064    /// A size that needs to be inferred. Used during sort checking to instantiate bit-vector
1065    /// sizes at call-sites.
1066    Infer(BvSizeVid),
1067}
1068
1069impl rustc_errors::IntoDiagArg for Sort {
1070    fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1071        rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1072    }
1073}
1074
1075impl rustc_errors::IntoDiagArg for FuncSort {
1076    fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1077        rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1078    }
1079}
1080
1081#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
1082pub struct FuncSort {
1083    pub inputs_and_output: List<Sort>,
1084}
1085
1086impl FuncSort {
1087    pub fn new(mut inputs: Vec<Sort>, output: Sort) -> Self {
1088        inputs.push(output);
1089        FuncSort { inputs_and_output: List::from_vec(inputs) }
1090    }
1091
1092    pub fn inputs(&self) -> &[Sort] {
1093        &self.inputs_and_output[0..self.inputs_and_output.len() - 1]
1094    }
1095
1096    pub fn output(&self) -> &Sort {
1097        &self.inputs_and_output[self.inputs_and_output.len() - 1]
1098    }
1099
1100    pub fn to_poly(&self) -> PolyFuncSort {
1101        PolyFuncSort::new(List::empty(), self.clone())
1102    }
1103}
1104
1105/// See [`PolyFuncSort`]
1106#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)]
1107pub enum SortParamKind {
1108    Sort,
1109    BvSize,
1110}
1111
1112/// A polymorphic function sort parametric over [sorts] or [bit-vector sizes].
1113///
1114/// Parameterizing over bit-vector sizes is a bit of a stretch, because smtlib doesn't support full
1115/// parametric reasoning over them. As long as we used functions parameterized over a size monomorphically
1116/// we should be fine. Right now, we can guarantee this, because size parameters are not exposed in
1117/// the surface syntax and they are only used for predefined (interpreted) theory functions.
1118///
1119/// [sorts]: Sort
1120/// [bit-vector sizes]: BvSize::Param
1121#[derive(Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)]
1122pub struct PolyFuncSort {
1123    /// The list of parameters including sorts and bit vector sizes
1124    params: List<SortParamKind>,
1125    fsort: FuncSort,
1126}
1127
1128impl PolyFuncSort {
1129    pub fn new(params: List<SortParamKind>, fsort: FuncSort) -> Self {
1130        PolyFuncSort { params, fsort }
1131    }
1132
1133    pub fn skip_binders(&self) -> FuncSort {
1134        self.fsort.clone()
1135    }
1136
1137    pub fn instantiate_identity(&self) -> FuncSort {
1138        self.fsort.clone()
1139    }
1140
1141    pub fn expect_mono(&self) -> FuncSort {
1142        assert!(self.params.is_empty());
1143        self.fsort.clone()
1144    }
1145
1146    pub fn params(&self) -> impl ExactSizeIterator<Item = SortParamKind> + '_ {
1147        self.params.iter().copied()
1148    }
1149
1150    pub fn instantiate(&self, args: &[SortArg]) -> FuncSort {
1151        self.fsort.fold_with(&mut SortSubst::new(args))
1152    }
1153}
1154
1155/// An argument for a generic parameter in a [`Sort`] which can be either a generic sort or a
1156/// generic bit-vector size.
1157#[derive(
1158    Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
1159)]
1160pub enum SortArg {
1161    Sort(Sort),
1162    BvSize(BvSize),
1163}
1164
1165#[derive(Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1166pub enum ConstantInfo {
1167    /// An uninterpreted constant
1168    Uninterpreted,
1169    /// A non-integral constant whose value is specified by the user
1170    Interpreted(Expr, Sort),
1171}
1172
1173#[derive(Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1174pub struct AdtDef(Interned<AdtDefData>);
1175
1176#[derive(Debug, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1177pub struct AdtDefData {
1178    invariants: Vec<Invariant>,
1179    sort_def: AdtSortDef,
1180    opaque: bool,
1181    rustc: ty::AdtDef,
1182}
1183
1184/// Option-like enum to explicitly mark that we don't have information about an ADT because it was
1185/// annotated with `#[flux::opaque]`. Note that only structs can be marked as opaque.
1186#[derive(Clone, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
1187pub enum Opaqueness<T> {
1188    Opaque,
1189    Transparent(T),
1190}
1191
1192impl<T> Opaqueness<T> {
1193    pub fn map<S>(self, f: impl FnOnce(T) -> S) -> Opaqueness<S> {
1194        match self {
1195            Opaqueness::Opaque => Opaqueness::Opaque,
1196            Opaqueness::Transparent(value) => Opaqueness::Transparent(f(value)),
1197        }
1198    }
1199
1200    pub fn as_ref(&self) -> Opaqueness<&T> {
1201        match self {
1202            Opaqueness::Opaque => Opaqueness::Opaque,
1203            Opaqueness::Transparent(value) => Opaqueness::Transparent(value),
1204        }
1205    }
1206
1207    pub fn as_deref(&self) -> Opaqueness<&T::Target>
1208    where
1209        T: std::ops::Deref,
1210    {
1211        match self {
1212            Opaqueness::Opaque => Opaqueness::Opaque,
1213            Opaqueness::Transparent(value) => Opaqueness::Transparent(value.deref()),
1214        }
1215    }
1216
1217    pub fn ok_or_else<E>(self, err: impl FnOnce() -> E) -> Result<T, E> {
1218        match self {
1219            Opaqueness::Transparent(v) => Ok(v),
1220            Opaqueness::Opaque => Err(err()),
1221        }
1222    }
1223
1224    #[track_caller]
1225    pub fn expect(self, msg: &str) -> T {
1226        match self {
1227            Opaqueness::Transparent(val) => val,
1228            Opaqueness::Opaque => bug!("{}", msg),
1229        }
1230    }
1231
1232    pub fn ok_or_query_err(self, struct_id: DefId) -> Result<T, QueryErr> {
1233        self.ok_or_else(|| QueryErr::OpaqueStruct { struct_id })
1234    }
1235}
1236
1237impl<T, E> Opaqueness<Result<T, E>> {
1238    pub fn transpose(self) -> Result<Opaqueness<T>, E> {
1239        match self {
1240            Opaqueness::Transparent(Ok(x)) => Ok(Opaqueness::Transparent(x)),
1241            Opaqueness::Transparent(Err(e)) => Err(e),
1242            Opaqueness::Opaque => Ok(Opaqueness::Opaque),
1243        }
1244    }
1245}
1246
1247pub static INT_TYS: [IntTy; 6] =
1248    [IntTy::Isize, IntTy::I8, IntTy::I16, IntTy::I32, IntTy::I64, IntTy::I128];
1249pub static UINT_TYS: [UintTy; 6] =
1250    [UintTy::Usize, UintTy::U8, UintTy::U16, UintTy::U32, UintTy::U64, UintTy::U128];
1251
1252#[derive(
1253    Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable,
1254)]
1255pub struct Invariant {
1256    // This predicate may have sort variables, but we don't explicitly mark it like in `PolyFuncSort`.
1257    // See comment on `apply` for details.
1258    pred: Binder<Expr>,
1259}
1260
1261impl Invariant {
1262    pub fn new(pred: Binder<Expr>) -> Self {
1263        Self { pred }
1264    }
1265
1266    pub fn apply(&self, idx: &Expr) -> Expr {
1267        // The predicate may have sort variables but we don't explicitly instantiate them. This
1268        // works because within an expression, sort variables can only appear inside the sort
1269        // annotation for a lambda and invariants cannot have lambdas. It remains to instantiate
1270        // variables in the sort of the binder itself, but since we are removing it, we can avoid
1271        // the explicit instantiation. Ultimately, this works because the expression we generate in
1272        // fixpoint doesn't need sort annotations (sorts are re-inferred).
1273        self.pred.replace_bound_reft(idx)
1274    }
1275}
1276
1277pub type PolyVariants = List<Binder<VariantSig>>;
1278pub type PolyVariant = Binder<VariantSig>;
1279
1280#[derive(Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1281pub struct VariantSig {
1282    pub adt_def: AdtDef,
1283    pub args: GenericArgs,
1284    pub fields: List<Ty>,
1285    pub idx: Expr,
1286    pub requires: List<Expr>,
1287}
1288
1289pub type PolyFnSig = Binder<FnSig>;
1290
1291#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
1292pub struct FnSig {
1293    pub safety: Safety,
1294    pub abi: rustc_abi::ExternAbi,
1295    pub requires: List<Expr>,
1296    pub inputs: List<Ty>,
1297    pub output: Binder<FnOutput>,
1298}
1299
1300#[derive(
1301    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
1302)]
1303pub struct FnOutput {
1304    pub ret: Ty,
1305    pub ensures: List<Ensures>,
1306}
1307
1308#[derive(Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1309pub enum Ensures {
1310    Type(Path, Ty),
1311    Pred(Expr),
1312}
1313
1314#[derive(Debug, TypeVisitable, TypeFoldable)]
1315pub struct Qualifier {
1316    pub def_id: FluxLocalDefId,
1317    pub body: Binder<Expr>,
1318    pub global: bool,
1319}
1320
1321/// A `PrimOpProp` is a single property for a primitive operation which
1322/// can be conjoined to get the definition of the [`PrimRel`] for that
1323/// primitive operation.
1324#[derive(Debug, TypeVisitable, TypeFoldable)]
1325pub struct PrimOpProp {
1326    pub def_id: FluxLocalDefId,
1327    pub op: BinOp,
1328    pub body: Binder<Expr>,
1329}
1330
1331#[derive(Debug, TypeVisitable, TypeFoldable)]
1332pub struct PrimRel {
1333    pub body: Binder<Expr>,
1334}
1335
1336pub type TyCtor = Binder<Ty>;
1337
1338impl TyCtor {
1339    pub fn to_ty(&self) -> Ty {
1340        match &self.vars()[..] {
1341            [] => {
1342                return self.skip_binder_ref().shift_out_escaping(1);
1343            }
1344            [BoundVariableKind::Refine(sort, ..)] => {
1345                if sort.is_unit() {
1346                    return self.replace_bound_reft(&Expr::unit());
1347                }
1348                if let Some(def_id) = sort.is_unit_adt() {
1349                    return self.replace_bound_reft(&Expr::unit_struct(def_id));
1350                }
1351            }
1352            _ => {}
1353        }
1354        Ty::exists(self.clone())
1355    }
1356}
1357
1358#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1359pub struct Ty(Interned<TyKind>);
1360
1361impl Ty {
1362    pub fn kind(&self) -> &TyKind {
1363        &self.0
1364    }
1365
1366    /// Dummy type used for the `Self` of a `TraitRef` created when converting a trait object, and
1367    /// which gets removed in `ExistentialTraitRef`. This type must not appear anywhere in other
1368    /// converted types and must be a valid `rustc` type (i.e., we must be able to call `to_rustc`
1369    /// on it). `TyKind::Infer(TyVid(0))` does the job, with the caveat that we must skip 0 when
1370    /// generating `TyKind::Infer` for "type holes".
1371    pub fn trait_object_dummy_self() -> Ty {
1372        Ty::infer(TyVid::from_u32(0))
1373    }
1374
1375    pub fn dynamic(preds: impl Into<List<Binder<ExistentialPredicate>>>, region: Region) -> Ty {
1376        BaseTy::Dynamic(preds.into(), region).to_ty()
1377    }
1378
1379    pub fn strg_ref(re: Region, path: Path, ty: Ty) -> Ty {
1380        TyKind::StrgRef(re, path, ty).intern()
1381    }
1382
1383    pub fn ptr(pk: impl Into<PtrKind>, path: impl Into<Path>) -> Ty {
1384        TyKind::Ptr(pk.into(), path.into()).intern()
1385    }
1386
1387    pub fn constr(p: impl Into<Expr>, ty: Ty) -> Ty {
1388        TyKind::Constr(p.into(), ty).intern()
1389    }
1390
1391    pub fn uninit() -> Ty {
1392        TyKind::Uninit.intern()
1393    }
1394
1395    pub fn indexed(bty: BaseTy, idx: impl Into<Expr>) -> Ty {
1396        TyKind::Indexed(bty, idx.into()).intern()
1397    }
1398
1399    pub fn exists(ty: Binder<Ty>) -> Ty {
1400        TyKind::Exists(ty).intern()
1401    }
1402
1403    pub fn exists_with_constr(bty: BaseTy, pred: Expr) -> Ty {
1404        let sort = bty.sort();
1405        let ty = Ty::indexed(bty, Expr::nu());
1406        Ty::exists(Binder::bind_with_sort(Ty::constr(pred, ty), sort))
1407    }
1408
1409    pub fn discr(adt_def: AdtDef, place: Place) -> Ty {
1410        TyKind::Discr(adt_def, place).intern()
1411    }
1412
1413    pub fn unit() -> Ty {
1414        Ty::tuple(vec![])
1415    }
1416
1417    pub fn bool() -> Ty {
1418        BaseTy::Bool.to_ty()
1419    }
1420
1421    pub fn int(int_ty: IntTy) -> Ty {
1422        BaseTy::Int(int_ty).to_ty()
1423    }
1424
1425    pub fn uint(uint_ty: UintTy) -> Ty {
1426        BaseTy::Uint(uint_ty).to_ty()
1427    }
1428
1429    pub fn param(param_ty: ParamTy) -> Ty {
1430        TyKind::Param(param_ty).intern()
1431    }
1432
1433    pub fn downcast(
1434        adt: AdtDef,
1435        args: GenericArgs,
1436        ty: Ty,
1437        variant: VariantIdx,
1438        fields: List<Ty>,
1439    ) -> Ty {
1440        TyKind::Downcast(adt, args, ty, variant, fields).intern()
1441    }
1442
1443    pub fn blocked(ty: Ty) -> Ty {
1444        TyKind::Blocked(ty).intern()
1445    }
1446
1447    pub fn str() -> Ty {
1448        BaseTy::Str.to_ty()
1449    }
1450
1451    pub fn char() -> Ty {
1452        BaseTy::Char.to_ty()
1453    }
1454
1455    pub fn float(float_ty: FloatTy) -> Ty {
1456        BaseTy::Float(float_ty).to_ty()
1457    }
1458
1459    pub fn mk_ref(region: Region, ty: Ty, mutbl: Mutability) -> Ty {
1460        BaseTy::Ref(region, ty, mutbl).to_ty()
1461    }
1462
1463    pub fn mk_slice(ty: Ty) -> Ty {
1464        BaseTy::Slice(ty).to_ty()
1465    }
1466
1467    pub fn mk_box(genv: GlobalEnv, deref_ty: Ty, alloc_ty: Ty) -> QueryResult<Ty> {
1468        let def_id = genv.tcx().require_lang_item(LangItem::OwnedBox, DUMMY_SP);
1469        let adt_def = genv.adt_def(def_id)?;
1470
1471        let args = List::from_arr([GenericArg::Ty(deref_ty), GenericArg::Ty(alloc_ty)]);
1472
1473        let bty = BaseTy::adt(adt_def, args);
1474        Ok(Ty::indexed(bty, Expr::unit_struct(def_id)))
1475    }
1476
1477    pub fn mk_box_with_default_alloc(genv: GlobalEnv, deref_ty: Ty) -> QueryResult<Ty> {
1478        let def_id = genv.tcx().require_lang_item(LangItem::OwnedBox, DUMMY_SP);
1479
1480        let generics = genv.generics_of(def_id)?;
1481        let alloc_ty = genv
1482            .lower_type_of(generics.own_params[1].def_id)?
1483            .skip_binder()
1484            .refine(&Refiner::default_for_item(genv, def_id)?)?;
1485
1486        Ty::mk_box(genv, deref_ty, alloc_ty)
1487    }
1488
1489    pub fn tuple(tys: impl Into<List<Ty>>) -> Ty {
1490        BaseTy::Tuple(tys.into()).to_ty()
1491    }
1492
1493    pub fn array(ty: Ty, c: Const) -> Ty {
1494        BaseTy::Array(ty, c).to_ty()
1495    }
1496
1497    pub fn closure(
1498        did: DefId,
1499        tys: impl Into<List<Ty>>,
1500        args: &flux_rustc_bridge::ty::GenericArgs,
1501    ) -> Ty {
1502        BaseTy::Closure(did, tys.into(), args.clone()).to_ty()
1503    }
1504
1505    pub fn coroutine(did: DefId, resume_ty: Ty, upvar_tys: List<Ty>) -> Ty {
1506        BaseTy::Coroutine(did, resume_ty, upvar_tys).to_ty()
1507    }
1508
1509    pub fn never() -> Ty {
1510        BaseTy::Never.to_ty()
1511    }
1512
1513    pub fn infer(vid: TyVid) -> Ty {
1514        TyKind::Infer(vid).intern()
1515    }
1516
1517    pub fn unconstr(&self) -> (Ty, Expr) {
1518        fn go(this: &Ty, preds: &mut Vec<Expr>) -> Ty {
1519            if let TyKind::Constr(pred, ty) = this.kind() {
1520                preds.push(pred.clone());
1521                go(ty, preds)
1522            } else {
1523                this.clone()
1524            }
1525        }
1526        let mut preds = vec![];
1527        (go(self, &mut preds), Expr::and_from_iter(preds))
1528    }
1529
1530    pub fn unblocked(&self) -> Ty {
1531        match self.kind() {
1532            TyKind::Blocked(ty) => ty.clone(),
1533            _ => self.clone(),
1534        }
1535    }
1536
1537    /// Whether the type is an `int` or a `uint`
1538    pub fn is_integral(&self) -> bool {
1539        self.as_bty_skipping_existentials()
1540            .map(BaseTy::is_integral)
1541            .unwrap_or_default()
1542    }
1543
1544    /// Whether the type is a `bool`
1545    pub fn is_bool(&self) -> bool {
1546        self.as_bty_skipping_existentials()
1547            .map(BaseTy::is_bool)
1548            .unwrap_or_default()
1549    }
1550
1551    /// Whether the type is a `char`
1552    pub fn is_char(&self) -> bool {
1553        self.as_bty_skipping_existentials()
1554            .map(BaseTy::is_char)
1555            .unwrap_or_default()
1556    }
1557
1558    pub fn is_uninit(&self) -> bool {
1559        matches!(self.kind(), TyKind::Uninit)
1560    }
1561
1562    pub fn is_box(&self) -> bool {
1563        self.as_bty_skipping_existentials()
1564            .map(BaseTy::is_box)
1565            .unwrap_or_default()
1566    }
1567
1568    pub fn is_struct(&self) -> bool {
1569        self.as_bty_skipping_existentials()
1570            .map(BaseTy::is_struct)
1571            .unwrap_or_default()
1572    }
1573
1574    pub fn is_array(&self) -> bool {
1575        self.as_bty_skipping_existentials()
1576            .map(BaseTy::is_array)
1577            .unwrap_or_default()
1578    }
1579
1580    pub fn is_slice(&self) -> bool {
1581        self.as_bty_skipping_existentials()
1582            .map(BaseTy::is_slice)
1583            .unwrap_or_default()
1584    }
1585
1586    pub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy> {
1587        match self.kind() {
1588            TyKind::Indexed(bty, _) => Some(bty),
1589            TyKind::Exists(ty) => Some(ty.skip_binder_ref().as_bty_skipping_existentials()?),
1590            TyKind::Constr(_, ty) => ty.as_bty_skipping_existentials(),
1591            _ => None,
1592        }
1593    }
1594
1595    #[track_caller]
1596    pub fn expect_discr(&self) -> (&AdtDef, &Place) {
1597        if let TyKind::Discr(adt_def, place) = self.kind() {
1598            (adt_def, place)
1599        } else {
1600            tracked_span_bug!("expected discr")
1601        }
1602    }
1603
1604    #[track_caller]
1605    pub fn expect_adt(&self) -> (&AdtDef, &[GenericArg], &Expr) {
1606        if let TyKind::Indexed(BaseTy::Adt(adt_def, args), idx) = self.kind() {
1607            (adt_def, args, idx)
1608        } else {
1609            tracked_span_bug!("expected adt `{self:?}`")
1610        }
1611    }
1612
1613    #[track_caller]
1614    pub fn expect_tuple(&self) -> &[Ty] {
1615        if let TyKind::Indexed(BaseTy::Tuple(tys), _) = self.kind() {
1616            tys
1617        } else {
1618            tracked_span_bug!("expected tuple found `{self:?}` (kind: `{:?}`)", self.kind())
1619        }
1620    }
1621}
1622
1623impl<'tcx> ToRustc<'tcx> for Ty {
1624    type T = rustc_middle::ty::Ty<'tcx>;
1625
1626    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
1627        match self.kind() {
1628            TyKind::Indexed(bty, _) => bty.to_rustc(tcx),
1629            TyKind::Exists(ty) => ty.skip_binder_ref().to_rustc(tcx),
1630            TyKind::Constr(_, ty) => ty.to_rustc(tcx),
1631            TyKind::Param(pty) => pty.to_ty(tcx),
1632            TyKind::StrgRef(re, _, ty) => {
1633                rustc_middle::ty::Ty::new_ref(
1634                    tcx,
1635                    re.to_rustc(tcx),
1636                    ty.to_rustc(tcx),
1637                    Mutability::Mut,
1638                )
1639            }
1640            TyKind::Infer(vid) => rustc_middle::ty::Ty::new_var(tcx, *vid),
1641            TyKind::Uninit
1642            | TyKind::Ptr(_, _)
1643            | TyKind::Discr(_, _)
1644            | TyKind::Downcast(_, _, _, _, _)
1645            | TyKind::Blocked(_) => bug!("TODO: to_rustc for `{self:?}`"),
1646        }
1647    }
1648}
1649
1650#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
1651pub enum TyKind {
1652    Indexed(BaseTy, Expr),
1653    Exists(Binder<Ty>),
1654    Constr(Expr, Ty),
1655    Uninit,
1656    StrgRef(Region, Path, Ty),
1657    Ptr(PtrKind, Path),
1658    /// This is a bit of a hack. We use this type internally to represent the result of
1659    /// [`Rvalue::Discriminant`] in a way that we can recover the necessary control information
1660    /// when checking a [`match`]. The hack is that we assume the dicriminant remains the same from
1661    /// the creation of this type until we use it in a [`match`].
1662    ///
1663    ///
1664    /// [`Rvalue::Discriminant`]: flux_rustc_bridge::mir::Rvalue::Discriminant
1665    /// [`match`]: flux_rustc_bridge::mir::TerminatorKind::SwitchInt
1666    Discr(AdtDef, Place),
1667    Param(ParamTy),
1668    Downcast(AdtDef, GenericArgs, Ty, VariantIdx, List<Ty>),
1669    Blocked(Ty),
1670    /// A type that needs to be inferred by matching the signature against a rust signature.
1671    /// [`TyKind::Infer`] appear as an intermediate step during `conv` and should not be present in
1672    /// the final signature.
1673    Infer(TyVid),
1674}
1675
1676#[derive(Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1677pub enum PtrKind {
1678    Mut(Region),
1679    Box,
1680}
1681
1682#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1683pub enum BaseTy {
1684    Int(IntTy),
1685    Uint(UintTy),
1686    Bool,
1687    Str,
1688    Char,
1689    Slice(Ty),
1690    Adt(AdtDef, GenericArgs),
1691    Float(FloatTy),
1692    RawPtr(Ty, Mutability),
1693    RawPtrMetadata(Ty),
1694    Ref(Region, Ty, Mutability),
1695    FnPtr(PolyFnSig),
1696    FnDef(DefId, GenericArgs),
1697    Tuple(List<Ty>),
1698    Alias(AliasKind, AliasTy),
1699    Array(Ty, Const),
1700    Never,
1701    Closure(DefId, /* upvar_tys */ List<Ty>, flux_rustc_bridge::ty::GenericArgs),
1702    Coroutine(DefId, /*resume_ty: */ Ty, /* upvar_tys: */ List<Ty>),
1703    Dynamic(List<Binder<ExistentialPredicate>>, Region),
1704    Param(ParamTy),
1705    Infer(TyVid),
1706    Foreign(DefId),
1707}
1708
1709impl BaseTy {
1710    pub fn opaque(alias_ty: AliasTy) -> BaseTy {
1711        BaseTy::Alias(AliasKind::Opaque, alias_ty)
1712    }
1713
1714    pub fn projection(alias_ty: AliasTy) -> BaseTy {
1715        BaseTy::Alias(AliasKind::Projection, alias_ty)
1716    }
1717
1718    pub fn adt(adt_def: AdtDef, args: GenericArgs) -> BaseTy {
1719        BaseTy::Adt(adt_def, args)
1720    }
1721
1722    pub fn fn_def(def_id: DefId, args: impl Into<GenericArgs>) -> BaseTy {
1723        BaseTy::FnDef(def_id, args.into())
1724    }
1725
1726    pub fn from_primitive_str(s: &str) -> Option<BaseTy> {
1727        match s {
1728            "i8" => Some(BaseTy::Int(IntTy::I8)),
1729            "i16" => Some(BaseTy::Int(IntTy::I16)),
1730            "i32" => Some(BaseTy::Int(IntTy::I32)),
1731            "i64" => Some(BaseTy::Int(IntTy::I64)),
1732            "i128" => Some(BaseTy::Int(IntTy::I128)),
1733            "u8" => Some(BaseTy::Uint(UintTy::U8)),
1734            "u16" => Some(BaseTy::Uint(UintTy::U16)),
1735            "u32" => Some(BaseTy::Uint(UintTy::U32)),
1736            "u64" => Some(BaseTy::Uint(UintTy::U64)),
1737            "u128" => Some(BaseTy::Uint(UintTy::U128)),
1738            "f16" => Some(BaseTy::Float(FloatTy::F16)),
1739            "f32" => Some(BaseTy::Float(FloatTy::F32)),
1740            "f64" => Some(BaseTy::Float(FloatTy::F64)),
1741            "f128" => Some(BaseTy::Float(FloatTy::F128)),
1742            "isize" => Some(BaseTy::Int(IntTy::Isize)),
1743            "usize" => Some(BaseTy::Uint(UintTy::Usize)),
1744            "bool" => Some(BaseTy::Bool),
1745            "char" => Some(BaseTy::Char),
1746            "str" => Some(BaseTy::Str),
1747            _ => None,
1748        }
1749    }
1750
1751    /// If `self` is a primitive, return its [`Symbol`].
1752    pub fn primitive_symbol(&self) -> Option<Symbol> {
1753        match self {
1754            BaseTy::Bool => Some(sym::bool),
1755            BaseTy::Char => Some(sym::char),
1756            BaseTy::Float(f) => {
1757                match f {
1758                    FloatTy::F16 => Some(sym::f16),
1759                    FloatTy::F32 => Some(sym::f32),
1760                    FloatTy::F64 => Some(sym::f64),
1761                    FloatTy::F128 => Some(sym::f128),
1762                }
1763            }
1764            BaseTy::Int(f) => {
1765                match f {
1766                    IntTy::Isize => Some(sym::isize),
1767                    IntTy::I8 => Some(sym::i8),
1768                    IntTy::I16 => Some(sym::i16),
1769                    IntTy::I32 => Some(sym::i32),
1770                    IntTy::I64 => Some(sym::i64),
1771                    IntTy::I128 => Some(sym::i128),
1772                }
1773            }
1774            BaseTy::Uint(f) => {
1775                match f {
1776                    UintTy::Usize => Some(sym::usize),
1777                    UintTy::U8 => Some(sym::u8),
1778                    UintTy::U16 => Some(sym::u16),
1779                    UintTy::U32 => Some(sym::u32),
1780                    UintTy::U64 => Some(sym::u64),
1781                    UintTy::U128 => Some(sym::u128),
1782                }
1783            }
1784            BaseTy::Str => Some(sym::str),
1785            _ => None,
1786        }
1787    }
1788
1789    pub fn is_integral(&self) -> bool {
1790        matches!(self, BaseTy::Int(_) | BaseTy::Uint(_))
1791    }
1792
1793    pub fn is_numeric(&self) -> bool {
1794        matches!(self, BaseTy::Int(_) | BaseTy::Uint(_) | BaseTy::Float(_))
1795    }
1796
1797    pub fn is_signed(&self) -> bool {
1798        matches!(self, BaseTy::Int(_))
1799    }
1800
1801    pub fn is_unsigned(&self) -> bool {
1802        matches!(self, BaseTy::Uint(_))
1803    }
1804
1805    pub fn is_float(&self) -> bool {
1806        matches!(self, BaseTy::Float(_))
1807    }
1808
1809    pub fn is_bool(&self) -> bool {
1810        matches!(self, BaseTy::Bool)
1811    }
1812
1813    fn is_struct(&self) -> bool {
1814        matches!(self, BaseTy::Adt(adt_def, _) if adt_def.is_struct())
1815    }
1816
1817    fn is_array(&self) -> bool {
1818        matches!(self, BaseTy::Array(..))
1819    }
1820
1821    fn is_slice(&self) -> bool {
1822        matches!(self, BaseTy::Slice(..))
1823    }
1824
1825    pub fn is_box(&self) -> bool {
1826        matches!(self, BaseTy::Adt(adt_def, _) if adt_def.is_box())
1827    }
1828
1829    pub fn is_char(&self) -> bool {
1830        matches!(self, BaseTy::Char)
1831    }
1832
1833    pub fn is_str(&self) -> bool {
1834        matches!(self, BaseTy::Str)
1835    }
1836
1837    pub fn unpack_box(&self) -> Option<(&Ty, &Ty)> {
1838        if let BaseTy::Adt(adt_def, args) = self
1839            && adt_def.is_box()
1840        {
1841            Some(args.box_args())
1842        } else {
1843            None
1844        }
1845    }
1846
1847    pub fn invariants(
1848        &self,
1849        tcx: TyCtxt,
1850        overflow_mode: OverflowMode,
1851    ) -> impl Iterator<Item = Invariant> {
1852        let (invariants, args) = match self {
1853            BaseTy::Adt(adt_def, args) => (adt_def.invariants().skip_binder(), &args[..]),
1854            BaseTy::Uint(uint_ty) => (uint_invariants(*uint_ty, overflow_mode), &[][..]),
1855            BaseTy::Int(int_ty) => (int_invariants(*int_ty, overflow_mode), &[][..]),
1856            BaseTy::Slice(_) => (slice_invariants(overflow_mode), &[][..]),
1857            _ => (&[][..], &[][..]),
1858        };
1859        invariants
1860            .iter()
1861            .map(move |inv| EarlyBinder(inv).instantiate_ref(tcx, args, &[]))
1862    }
1863
1864    pub fn to_ty(&self) -> Ty {
1865        let sort = self.sort();
1866        if sort.is_unit() {
1867            Ty::indexed(self.clone(), Expr::unit())
1868        } else {
1869            Ty::exists(Binder::bind_with_sort(Ty::indexed(self.clone(), Expr::nu()), sort))
1870        }
1871    }
1872
1873    pub fn to_subset_ty_ctor(&self) -> SubsetTyCtor {
1874        let sort = self.sort();
1875        Binder::bind_with_sort(SubsetTy::trivial(self.clone(), Expr::nu()), sort)
1876    }
1877
1878    #[track_caller]
1879    pub fn expect_adt(&self) -> (&AdtDef, &[GenericArg]) {
1880        if let BaseTy::Adt(adt_def, args) = self {
1881            (adt_def, args)
1882        } else {
1883            tracked_span_bug!("expected adt `{self:?}`")
1884        }
1885    }
1886
1887    /// A type is an *atom* if it is "self-delimiting", i.e., it has a clear boundary
1888    /// when printed. This is used to avoid unnecessary parenthesis when pretty printing.
1889    pub fn is_atom(&self) -> bool {
1890        // (nilehmann) I'm not sure about this list, please adjust if you get any odd behavior
1891        matches!(
1892            self,
1893            BaseTy::Int(_)
1894                | BaseTy::Uint(_)
1895                | BaseTy::Slice(_)
1896                | BaseTy::Bool
1897                | BaseTy::Char
1898                | BaseTy::Str
1899                | BaseTy::Adt(..)
1900                | BaseTy::Tuple(..)
1901                | BaseTy::Param(_)
1902                | BaseTy::Array(..)
1903                | BaseTy::Never
1904                | BaseTy::Closure(..)
1905                | BaseTy::Coroutine(..)
1906                // opaque alias are atoms the way we print them now, but they won't
1907                // be if we print them as `impl Trait`
1908                | BaseTy::Alias(..)
1909        )
1910    }
1911}
1912
1913impl<'tcx> ToRustc<'tcx> for BaseTy {
1914    type T = rustc_middle::ty::Ty<'tcx>;
1915
1916    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
1917        use rustc_middle::ty;
1918        match self {
1919            BaseTy::Int(i) => ty::Ty::new_int(tcx, *i),
1920            BaseTy::Uint(i) => ty::Ty::new_uint(tcx, *i),
1921            BaseTy::Param(pty) => pty.to_ty(tcx),
1922            BaseTy::Slice(ty) => ty::Ty::new_slice(tcx, ty.to_rustc(tcx)),
1923            BaseTy::Bool => tcx.types.bool,
1924            BaseTy::Char => tcx.types.char,
1925            BaseTy::Str => tcx.types.str_,
1926            BaseTy::Adt(adt_def, args) => {
1927                let did = adt_def.did();
1928                let adt_def = tcx.adt_def(did);
1929                let args = args.to_rustc(tcx);
1930                ty::Ty::new_adt(tcx, adt_def, args)
1931            }
1932            BaseTy::FnDef(def_id, args) => {
1933                let args = args.to_rustc(tcx);
1934                ty::Ty::new_fn_def(tcx, *def_id, args)
1935            }
1936            BaseTy::Float(f) => ty::Ty::new_float(tcx, *f),
1937            BaseTy::RawPtr(ty, mutbl) => ty::Ty::new_ptr(tcx, ty.to_rustc(tcx), *mutbl),
1938            BaseTy::Ref(re, ty, mutbl) => {
1939                ty::Ty::new_ref(tcx, re.to_rustc(tcx), ty.to_rustc(tcx), *mutbl)
1940            }
1941            BaseTy::FnPtr(poly_sig) => ty::Ty::new_fn_ptr(tcx, poly_sig.to_rustc(tcx)),
1942            BaseTy::Tuple(tys) => {
1943                let ts = tys.iter().map(|ty| ty.to_rustc(tcx)).collect_vec();
1944                ty::Ty::new_tup(tcx, &ts)
1945            }
1946            BaseTy::Alias(kind, alias_ty) => {
1947                ty::Ty::new_alias(tcx, kind.to_rustc(tcx), alias_ty.to_rustc(tcx))
1948            }
1949            BaseTy::Array(ty, n) => {
1950                let ty = ty.to_rustc(tcx);
1951                let n = n.to_rustc(tcx);
1952                ty::Ty::new_array_with_const_len(tcx, ty, n)
1953            }
1954            BaseTy::Never => tcx.types.never,
1955            BaseTy::Closure(did, _, args) => ty::Ty::new_closure(tcx, *did, args.to_rustc(tcx)),
1956            BaseTy::Dynamic(exi_preds, re) => {
1957                let preds: Vec<_> = exi_preds
1958                    .iter()
1959                    .map(|pred| pred.to_rustc(tcx))
1960                    .collect_vec();
1961                let preds = tcx.mk_poly_existential_predicates(&preds);
1962                ty::Ty::new_dynamic(tcx, preds, re.to_rustc(tcx), rustc_middle::ty::DynKind::Dyn)
1963            }
1964            BaseTy::Coroutine(def_id, resume_ty, upvars) => {
1965                bug!("TODO: Generator {def_id:?} {resume_ty:?} {upvars:?}")
1966                // let args = args.iter().map(|arg| into_rustc_generic_arg(tcx, arg));
1967                // let args = tcx.mk_args_from_iter(args);
1968                // ty::Ty::new_generator(*tcx, *def_id, args, mov)
1969            }
1970            BaseTy::Infer(ty_vid) => ty::Ty::new_var(tcx, *ty_vid),
1971            BaseTy::Foreign(def_id) => ty::Ty::new_foreign(tcx, *def_id),
1972            BaseTy::RawPtrMetadata(ty) => {
1973                ty::Ty::new_ptr(
1974                    tcx,
1975                    ty.to_rustc(tcx),
1976                    RawPtrKind::FakeForPtrMetadata.to_mutbl_lossy(),
1977                )
1978            }
1979        }
1980    }
1981}
1982
1983#[derive(
1984    Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
1985)]
1986pub struct AliasTy {
1987    pub def_id: DefId,
1988    pub args: GenericArgs,
1989    /// Holds the refinement-arguments for opaque-types; empty for projections
1990    pub refine_args: RefineArgs,
1991}
1992
1993impl AliasTy {
1994    pub fn new(def_id: DefId, args: GenericArgs, refine_args: RefineArgs) -> Self {
1995        AliasTy { args, refine_args, def_id }
1996    }
1997}
1998
1999/// This methods work only with associated type projections (i.e., no opaque types)
2000impl AliasTy {
2001    pub fn self_ty(&self) -> SubsetTyCtor {
2002        self.args[0].expect_base().clone()
2003    }
2004
2005    pub fn with_self_ty(&self, self_ty: SubsetTyCtor) -> Self {
2006        Self {
2007            def_id: self.def_id,
2008            args: [GenericArg::Base(self_ty)]
2009                .into_iter()
2010                .chain(self.args.iter().skip(1).cloned())
2011                .collect(),
2012            refine_args: self.refine_args.clone(),
2013        }
2014    }
2015}
2016
2017impl<'tcx> ToRustc<'tcx> for AliasTy {
2018    type T = rustc_middle::ty::AliasTy<'tcx>;
2019
2020    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2021        rustc_middle::ty::AliasTy::new(tcx, self.def_id, self.args.to_rustc(tcx))
2022    }
2023}
2024
2025pub type RefineArgs = List<Expr>;
2026
2027#[extension(pub trait RefineArgsExt)]
2028impl RefineArgs {
2029    fn identity_for_item(genv: GlobalEnv, def_id: DefId) -> QueryResult<RefineArgs> {
2030        Self::for_item(genv, def_id, |param, index| {
2031            Ok(Expr::var(Var::EarlyParam(EarlyReftParam {
2032                index: index as u32,
2033                name: param.name(),
2034            })))
2035        })
2036    }
2037
2038    fn for_item<F>(genv: GlobalEnv, def_id: DefId, mut mk: F) -> QueryResult<RefineArgs>
2039    where
2040        F: FnMut(EarlyBinder<RefineParam>, usize) -> QueryResult<Expr>,
2041    {
2042        let reft_generics = genv.refinement_generics_of(def_id)?;
2043        let count = reft_generics.count();
2044        let mut args = Vec::with_capacity(count);
2045        reft_generics.fill_item(genv, &mut args, &mut mk)?;
2046        Ok(List::from_vec(args))
2047    }
2048}
2049
2050/// A type constructor meant to be used as generic a argument of [kind base]. This is just an alias
2051/// to [`Binder<SubsetTy>`], but we expect the binder to have a single bound variable of the sort of
2052/// the underlying [base type].
2053///
2054/// [kind base]: GenericParamDefKind::Base
2055/// [base type]: SubsetTy::bty
2056pub type SubsetTyCtor = Binder<SubsetTy>;
2057
2058impl SubsetTyCtor {
2059    pub fn as_bty_skipping_binder(&self) -> &BaseTy {
2060        &self.as_ref().skip_binder().bty
2061    }
2062
2063    pub fn to_ty(&self) -> Ty {
2064        let sort = self.sort();
2065        if sort.is_unit() {
2066            self.replace_bound_reft(&Expr::unit()).to_ty()
2067        } else if let Some(def_id) = sort.is_unit_adt() {
2068            self.replace_bound_reft(&Expr::unit_struct(def_id)).to_ty()
2069        } else {
2070            Ty::exists(self.as_ref().map(SubsetTy::to_ty))
2071        }
2072    }
2073
2074    pub fn to_ty_ctor(&self) -> TyCtor {
2075        self.as_ref().map(SubsetTy::to_ty)
2076    }
2077}
2078
2079/// A subset type is a simplified version of a type that has the form `{b[e] | p}` where `b` is a
2080/// [`BaseTy`], `e` a refinement index, and `p` a predicate.
2081///
2082/// These are mainly found under a [`Binder`] with a single variable of the base type's sort. This
2083/// can be interpreted as a type constructor or an existential type. For example, under a binder with a
2084/// variable `v` of sort `int`, we can interpret `{i32[v] | v > 0}` as:
2085/// - A lambda `λv:int. {i32[v] | v > 0}` that "constructs" types when applied to ints, or
2086/// - An existential type `∃v:int. {i32[v] | v > 0}`.
2087///
2088/// This second interpretation is the reason we call this a subset type, i.e., the type `∃v. {b[v] | p}`
2089/// corresponds to the subset of values of  type `b` whose index satisfies `p`. These are the types
2090/// written as `B{v: p}` in the surface syntax and correspond to the types supported in other
2091/// refinement type systems like Liquid Haskell (with the difference that we are explicit
2092/// about separating refinements from program values via an index).
2093///
2094/// The main purpose for subset types is to be used as generic arguments of [kind base] when
2095/// interpreted as type constructors. They have two key properties that makes them suitable
2096/// for this:
2097///
2098/// 1. **Syntactic Restriction**: Subset types are syntactically restricted, making it easier to
2099///    relate them structurally (e.g., for subtyping). For instance, given two types `S<λv. T1>` and
2100///    `S<λ. T2>`, if `T1` and `T2` are subset types, we know they match structurally (at least
2101///    shallowly). In particularly, the syntactic restriction rules out complex types like
2102///    `S<λv. (i32[v], i32[v])>` simplifying some operations.
2103///
2104/// 2. **Eager Canonicalization**: Subset types can be eagerly canonicalized via [*strengthening*]
2105///    during substitution. For example, suppose we have a function:
2106///    ```text
2107///    fn foo<T>(x: T[@a], y: { T[@b] | b == a }) { }
2108///    ```
2109///    If we instantiate `T` with `λv. { i32[v] | v > 0}`, after substitution and applying the
2110///    lambda (the indexing syntax `T[a]` corresponds to an application of the lambda), we get:
2111///    ```text
2112///    fn foo(x: {i32[@a] | a > 0}, y: { { i32[@b] | b > 0 } | b == a }) { }
2113///    ```
2114///    Via *strengthening* we can canonicalize this to
2115///    ```text
2116///    fn foo(x: {i32[@a] | a > 0}, y: { i32[@b] | b == a && b > 0 }) { }
2117///    ```
2118///    As a result, we can guarantee the syntactic restriction through substitution.
2119///
2120/// [kind base]: GenericParamDefKind::Base
2121/// [*strengthening*]: https://arxiv.org/pdf/2010.07763.pdf
2122#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)]
2123pub struct SubsetTy {
2124    /// The base type `b` in the subset type `{b[e] | p}`.
2125    ///
2126    /// **NOTE:** This is mostly going to be under a [`Binder`]. It is not yet clear to me whether
2127    /// this [`BaseTy`] should be able to mention variables in the binder. In general, in a type
2128    /// `∃v. {b[e] | p}`, it's fine to mention `v` inside `b`, but since [`SubsetTy`] is meant to
2129    /// facilitate syntactic manipulation we may want to restrict this.
2130    pub bty: BaseTy,
2131    /// The refinement index `e` in the subset type `{b[e] | p}`. This can be an arbitrary expression,
2132    /// which makes manipulation easier. However, since this is mostly found under a binder, we expect
2133    /// it to be [`Expr::nu()`].
2134    pub idx: Expr,
2135    /// The predicate `p` in the subset type `{b[e] | p}`.
2136    pub pred: Expr,
2137}
2138
2139impl SubsetTy {
2140    pub fn new(bty: BaseTy, idx: impl Into<Expr>, pred: impl Into<Expr>) -> Self {
2141        Self { bty, idx: idx.into(), pred: pred.into() }
2142    }
2143
2144    pub fn trivial(bty: BaseTy, idx: impl Into<Expr>) -> Self {
2145        Self::new(bty, idx, Expr::tt())
2146    }
2147
2148    pub fn strengthen(&self, pred: impl Into<Expr>) -> Self {
2149        let this = self.clone();
2150        let pred = Expr::and(this.pred, pred).simplify(&SnapshotMap::default());
2151        Self { bty: this.bty, idx: this.idx, pred }
2152    }
2153
2154    pub fn to_ty(&self) -> Ty {
2155        let bty = self.bty.clone();
2156        if self.pred.is_trivially_true() {
2157            Ty::indexed(bty, &self.idx)
2158        } else {
2159            Ty::constr(&self.pred, Ty::indexed(bty, &self.idx))
2160        }
2161    }
2162}
2163
2164impl<'tcx> ToRustc<'tcx> for SubsetTy {
2165    type T = rustc_middle::ty::Ty<'tcx>;
2166
2167    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::Ty<'tcx> {
2168        self.bty.to_rustc(tcx)
2169    }
2170}
2171
2172#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)]
2173pub enum GenericArg {
2174    Ty(Ty),
2175    Base(SubsetTyCtor),
2176    Lifetime(Region),
2177    Const(Const),
2178}
2179
2180impl GenericArg {
2181    #[track_caller]
2182    pub fn expect_type(&self) -> &Ty {
2183        if let GenericArg::Ty(ty) = self {
2184            ty
2185        } else {
2186            bug!("expected `rty::GenericArg::Ty`, found `{self:?}`")
2187        }
2188    }
2189
2190    #[track_caller]
2191    pub fn expect_base(&self) -> &SubsetTyCtor {
2192        if let GenericArg::Base(ctor) = self {
2193            ctor
2194        } else {
2195            bug!("expected `rty::GenericArg::Base`, found `{self:?}`")
2196        }
2197    }
2198
2199    pub fn from_param_def(param: &GenericParamDef) -> Self {
2200        match param.kind {
2201            GenericParamDefKind::Type { .. } => {
2202                let param_ty = ParamTy { index: param.index, name: param.name };
2203                GenericArg::Ty(Ty::param(param_ty))
2204            }
2205            GenericParamDefKind::Base { .. } => {
2206                // λv. T[v]
2207                let param_ty = ParamTy { index: param.index, name: param.name };
2208                GenericArg::Base(Binder::bind_with_sort(
2209                    SubsetTy::trivial(BaseTy::Param(param_ty), Expr::nu()),
2210                    Sort::Param(param_ty),
2211                ))
2212            }
2213            GenericParamDefKind::Lifetime => {
2214                let region = EarlyParamRegion { index: param.index, name: param.name };
2215                GenericArg::Lifetime(Region::ReEarlyParam(region))
2216            }
2217            GenericParamDefKind::Const { .. } => {
2218                let param_const = ParamConst { index: param.index, name: param.name };
2219                let kind = ConstKind::Param(param_const);
2220                GenericArg::Const(Const { kind })
2221            }
2222        }
2223    }
2224
2225    /// Creates a `GenericArgs` from the definition of generic parameters, by calling a closure to
2226    /// obtain arg. The closures get to observe the `GenericArgs` as they're being built, which can
2227    /// be used to correctly replace defaults of generic parameters.
2228    pub fn for_item<F>(genv: GlobalEnv, def_id: DefId, mut mk_kind: F) -> QueryResult<GenericArgs>
2229    where
2230        F: FnMut(&GenericParamDef, &[GenericArg]) -> GenericArg,
2231    {
2232        let defs = genv.generics_of(def_id)?;
2233        let count = defs.count();
2234        let mut args = Vec::with_capacity(count);
2235        Self::fill_item(genv, &mut args, &defs, &mut mk_kind)?;
2236        Ok(List::from_vec(args))
2237    }
2238
2239    pub fn identity_for_item(genv: GlobalEnv, def_id: DefId) -> QueryResult<GenericArgs> {
2240        Self::for_item(genv, def_id, |param, _| GenericArg::from_param_def(param))
2241    }
2242
2243    fn fill_item<F>(
2244        genv: GlobalEnv,
2245        args: &mut Vec<GenericArg>,
2246        generics: &Generics,
2247        mk_kind: &mut F,
2248    ) -> QueryResult<()>
2249    where
2250        F: FnMut(&GenericParamDef, &[GenericArg]) -> GenericArg,
2251    {
2252        if let Some(def_id) = generics.parent {
2253            let parent_generics = genv.generics_of(def_id)?;
2254            Self::fill_item(genv, args, &parent_generics, mk_kind)?;
2255        }
2256        for param in &generics.own_params {
2257            let kind = mk_kind(param, args);
2258            tracked_span_assert_eq!(param.index as usize, args.len());
2259            args.push(kind);
2260        }
2261        Ok(())
2262    }
2263}
2264
2265impl From<TyOrBase> for GenericArg {
2266    fn from(v: TyOrBase) -> Self {
2267        match v {
2268            TyOrBase::Ty(ty) => GenericArg::Ty(ty),
2269            TyOrBase::Base(ctor) => GenericArg::Base(ctor),
2270        }
2271    }
2272}
2273
2274impl<'tcx> ToRustc<'tcx> for GenericArg {
2275    type T = rustc_middle::ty::GenericArg<'tcx>;
2276
2277    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2278        use rustc_middle::ty;
2279        match self {
2280            GenericArg::Ty(ty) => ty::GenericArg::from(ty.to_rustc(tcx)),
2281            GenericArg::Base(ctor) => ty::GenericArg::from(ctor.skip_binder_ref().to_rustc(tcx)),
2282            GenericArg::Lifetime(re) => ty::GenericArg::from(re.to_rustc(tcx)),
2283            GenericArg::Const(c) => ty::GenericArg::from(c.to_rustc(tcx)),
2284        }
2285    }
2286}
2287
2288pub type GenericArgs = List<GenericArg>;
2289
2290#[extension(pub trait GenericArgsExt)]
2291impl GenericArgs {
2292    #[track_caller]
2293    fn box_args(&self) -> (&Ty, &Ty) {
2294        if let [GenericArg::Ty(deref), GenericArg::Ty(alloc)] = &self[..] {
2295            (deref, alloc)
2296        } else {
2297            bug!("invalid generic arguments for box");
2298        }
2299    }
2300
2301    // We can't implement [`ToRustc`] because of coherence so we add it here
2302    fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::GenericArgsRef<'tcx> {
2303        tcx.mk_args_from_iter(self.iter().map(|arg| arg.to_rustc(tcx)))
2304    }
2305
2306    fn rebase_onto(
2307        &self,
2308        tcx: &TyCtxt,
2309        source_ancestor: DefId,
2310        target_args: &GenericArgs,
2311    ) -> List<GenericArg> {
2312        let defs = tcx.generics_of(source_ancestor);
2313        target_args
2314            .iter()
2315            .chain(self.iter().skip(defs.count()))
2316            .cloned()
2317            .collect()
2318    }
2319}
2320
2321#[derive(Debug)]
2322pub enum TyOrBase {
2323    Ty(Ty),
2324    Base(SubsetTyCtor),
2325}
2326
2327impl TyOrBase {
2328    pub fn into_ty(self) -> Ty {
2329        match self {
2330            TyOrBase::Ty(ty) => ty,
2331            TyOrBase::Base(ctor) => ctor.to_ty(),
2332        }
2333    }
2334
2335    #[track_caller]
2336    pub fn expect_base(self) -> SubsetTyCtor {
2337        match self {
2338            TyOrBase::Base(ctor) => ctor,
2339            TyOrBase::Ty(_) => tracked_span_bug!("expected `TyOrBase::Base`"),
2340        }
2341    }
2342
2343    pub fn as_base(self) -> Option<SubsetTyCtor> {
2344        match self {
2345            TyOrBase::Base(ctor) => Some(ctor),
2346            TyOrBase::Ty(_) => None,
2347        }
2348    }
2349}
2350
2351#[derive(Debug, Clone, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
2352pub enum TyOrCtor {
2353    Ty(Ty),
2354    Ctor(TyCtor),
2355}
2356
2357impl TyOrCtor {
2358    #[track_caller]
2359    pub fn expect_ctor(self) -> TyCtor {
2360        match self {
2361            TyOrCtor::Ctor(ctor) => ctor,
2362            TyOrCtor::Ty(_) => tracked_span_bug!("expected `TyOrCtor::Ctor`"),
2363        }
2364    }
2365
2366    pub fn expect_subset_ty_ctor(self) -> SubsetTyCtor {
2367        self.expect_ctor().map(|ty| {
2368            if let canonicalize::CanonicalTy::Constr(constr_ty) = ty.shallow_canonicalize()
2369                && let TyKind::Indexed(bty, idx) = constr_ty.ty().kind()
2370                && idx.is_nu()
2371            {
2372                SubsetTy::new(bty.clone(), Expr::nu(), constr_ty.pred())
2373            } else {
2374                tracked_span_bug!()
2375            }
2376        })
2377    }
2378
2379    pub fn to_ty(&self) -> Ty {
2380        match self {
2381            TyOrCtor::Ctor(ctor) => ctor.to_ty(),
2382            TyOrCtor::Ty(ty) => ty.clone(),
2383        }
2384    }
2385}
2386
2387impl From<TyOrBase> for TyOrCtor {
2388    fn from(v: TyOrBase) -> Self {
2389        match v {
2390            TyOrBase::Ty(ty) => TyOrCtor::Ty(ty),
2391            TyOrBase::Base(ctor) => TyOrCtor::Ctor(ctor.to_ty_ctor()),
2392        }
2393    }
2394}
2395
2396impl CoroutineObligPredicate {
2397    pub fn to_poly_fn_sig(&self) -> PolyFnSig {
2398        let vars = vec![];
2399
2400        let resume_ty = &self.resume_ty;
2401        let env_ty = Ty::coroutine(self.def_id, resume_ty.clone(), self.upvar_tys.clone());
2402
2403        let inputs = List::from_arr([env_ty, resume_ty.clone()]);
2404        let output =
2405            Binder::bind_with_vars(FnOutput::new(self.output.clone(), vec![]), List::empty());
2406
2407        PolyFnSig::bind_with_vars(
2408            FnSig::new(Safety::Safe, rustc_abi::ExternAbi::RustCall, List::empty(), inputs, output),
2409            List::from(vars),
2410        )
2411    }
2412}
2413
2414impl RefinementGenerics {
2415    pub fn count(&self) -> usize {
2416        self.parent_count + self.own_params.len()
2417    }
2418
2419    pub fn own_count(&self) -> usize {
2420        self.own_params.len()
2421    }
2422
2423    // /// Iterate and collect all parameters in this item including parents
2424    // pub fn collect_all_params<T, S>(
2425    //     &self,
2426    //     genv: GlobalEnv,
2427    //     mut f: impl FnMut(RefineParam) -> T,
2428    // ) -> QueryResult<S>
2429    // where
2430    //     S: FromIterator<T>,
2431    // {
2432    //     (0..self.count())
2433    //         .map(|i| Ok(f(self.param_at(i, genv)?)))
2434    //         .try_collect()
2435    // }
2436}
2437
2438impl EarlyBinder<RefinementGenerics> {
2439    pub fn parent(&self) -> Option<DefId> {
2440        self.skip_binder_ref().parent
2441    }
2442
2443    pub fn parent_count(&self) -> usize {
2444        self.skip_binder_ref().parent_count
2445    }
2446
2447    pub fn count(&self) -> usize {
2448        self.skip_binder_ref().count()
2449    }
2450
2451    pub fn own_count(&self) -> usize {
2452        self.skip_binder_ref().own_count()
2453    }
2454
2455    pub fn own_param_at(&self, index: usize) -> EarlyBinder<RefineParam> {
2456        self.as_ref().map(|this| this.own_params[index].clone())
2457    }
2458
2459    pub fn param_at(
2460        &self,
2461        param_index: usize,
2462        genv: GlobalEnv,
2463    ) -> QueryResult<EarlyBinder<RefineParam>> {
2464        if let Some(index) = param_index.checked_sub(self.parent_count()) {
2465            Ok(self.own_param_at(index))
2466        } else {
2467            let parent = self.parent().expect("parent_count > 0 but no parent?");
2468            genv.refinement_generics_of(parent)?
2469                .param_at(param_index, genv)
2470        }
2471    }
2472
2473    pub fn iter_own_params(&self) -> impl Iterator<Item = EarlyBinder<RefineParam>> + use<'_> {
2474        self.skip_binder_ref()
2475            .own_params
2476            .iter()
2477            .cloned()
2478            .map(EarlyBinder)
2479    }
2480
2481    pub fn fill_item<F, R>(&self, genv: GlobalEnv, vec: &mut Vec<R>, mk: &mut F) -> QueryResult
2482    where
2483        F: FnMut(EarlyBinder<RefineParam>, usize) -> QueryResult<R>,
2484    {
2485        if let Some(def_id) = self.parent() {
2486            genv.refinement_generics_of(def_id)?
2487                .fill_item(genv, vec, mk)?;
2488        }
2489        for param in self.iter_own_params() {
2490            vec.push(mk(param, vec.len())?);
2491        }
2492        Ok(())
2493    }
2494}
2495
2496impl EarlyBinder<GenericPredicates> {
2497    pub fn predicates(&self) -> EarlyBinder<List<Clause>> {
2498        EarlyBinder(self.0.predicates.clone())
2499    }
2500}
2501
2502impl EarlyBinder<FuncSort> {
2503    /// See [`subst::GenericsSubstForSort`]
2504    pub fn instantiate_func_sort<E>(
2505        self,
2506        sort_for_param: impl FnMut(ParamTy) -> Result<Sort, E>,
2507    ) -> Result<FuncSort, E> {
2508        self.0.try_fold_with(&mut subst::GenericsSubstFolder::new(
2509            subst::GenericsSubstForSort { sort_for_param },
2510            &[],
2511        ))
2512    }
2513}
2514
2515impl VariantSig {
2516    pub fn new(
2517        adt_def: AdtDef,
2518        args: GenericArgs,
2519        fields: List<Ty>,
2520        idx: Expr,
2521        requires: List<Expr>,
2522    ) -> Self {
2523        VariantSig { adt_def, args, fields, idx, requires }
2524    }
2525
2526    pub fn fields(&self) -> &[Ty] {
2527        &self.fields
2528    }
2529
2530    pub fn ret(&self) -> Ty {
2531        let bty = BaseTy::Adt(self.adt_def.clone(), self.args.clone());
2532        let idx = self.idx.clone();
2533        Ty::indexed(bty, idx)
2534    }
2535}
2536
2537impl FnSig {
2538    pub fn new(
2539        safety: Safety,
2540        abi: rustc_abi::ExternAbi,
2541        requires: List<Expr>,
2542        inputs: List<Ty>,
2543        output: Binder<FnOutput>,
2544    ) -> Self {
2545        FnSig { safety, abi, requires, inputs, output }
2546    }
2547
2548    pub fn requires(&self) -> &[Expr] {
2549        &self.requires
2550    }
2551
2552    pub fn inputs(&self) -> &[Ty] {
2553        &self.inputs
2554    }
2555
2556    pub fn output(&self) -> Binder<FnOutput> {
2557        self.output.clone()
2558    }
2559}
2560
2561impl<'tcx> ToRustc<'tcx> for FnSig {
2562    type T = rustc_middle::ty::FnSig<'tcx>;
2563
2564    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2565        tcx.mk_fn_sig(
2566            self.inputs().iter().map(|ty| ty.to_rustc(tcx)),
2567            self.output().as_ref().skip_binder().to_rustc(tcx),
2568            false,
2569            self.safety,
2570            self.abi,
2571        )
2572    }
2573}
2574
2575impl FnOutput {
2576    pub fn new(ret: Ty, ensures: impl Into<List<Ensures>>) -> Self {
2577        Self { ret, ensures: ensures.into() }
2578    }
2579}
2580
2581impl<'tcx> ToRustc<'tcx> for FnOutput {
2582    type T = rustc_middle::ty::Ty<'tcx>;
2583
2584    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2585        self.ret.to_rustc(tcx)
2586    }
2587}
2588
2589impl AdtDef {
2590    pub fn new(
2591        rustc: ty::AdtDef,
2592        sort_def: AdtSortDef,
2593        invariants: Vec<Invariant>,
2594        opaque: bool,
2595    ) -> Self {
2596        AdtDef(Interned::new(AdtDefData { invariants, sort_def, opaque, rustc }))
2597    }
2598
2599    pub fn did(&self) -> DefId {
2600        self.0.rustc.did()
2601    }
2602
2603    pub fn sort_def(&self) -> &AdtSortDef {
2604        &self.0.sort_def
2605    }
2606
2607    pub fn sort(&self, args: &[GenericArg]) -> Sort {
2608        self.sort_def().to_sort(args)
2609    }
2610
2611    pub fn is_box(&self) -> bool {
2612        self.0.rustc.is_box()
2613    }
2614
2615    pub fn is_enum(&self) -> bool {
2616        self.0.rustc.is_enum()
2617    }
2618
2619    pub fn is_struct(&self) -> bool {
2620        self.0.rustc.is_struct()
2621    }
2622
2623    pub fn is_union(&self) -> bool {
2624        self.0.rustc.is_union()
2625    }
2626
2627    pub fn variants(&self) -> &IndexSlice<VariantIdx, VariantDef> {
2628        self.0.rustc.variants()
2629    }
2630
2631    pub fn variant(&self, idx: VariantIdx) -> &VariantDef {
2632        self.0.rustc.variant(idx)
2633    }
2634
2635    pub fn invariants(&self) -> EarlyBinder<&[Invariant]> {
2636        EarlyBinder(&self.0.invariants)
2637    }
2638
2639    pub fn discriminants(&self) -> impl Iterator<Item = (VariantIdx, u128)> + '_ {
2640        self.0.rustc.discriminants()
2641    }
2642
2643    pub fn is_opaque(&self) -> bool {
2644        self.0.opaque
2645    }
2646}
2647
2648impl EarlyBinder<PolyVariant> {
2649    // The field_idx is `Some(i)` when we have the `i`-th field of a `union`, in which case,
2650    // the `inputs` are _just_ the `i`-th type (and not all the types...)
2651    pub fn to_poly_fn_sig(&self, field_idx: Option<crate::FieldIdx>) -> EarlyBinder<PolyFnSig> {
2652        self.as_ref().map(|poly_variant| {
2653            poly_variant.as_ref().map(|variant| {
2654                let ret = variant.ret().shift_in_escaping(1);
2655                let output = Binder::bind_with_vars(FnOutput::new(ret, vec![]), List::empty());
2656                let inputs = match field_idx {
2657                    None => variant.fields.clone(),
2658                    Some(i) => List::singleton(variant.fields[i.index()].clone()),
2659                };
2660                FnSig::new(
2661                    Safety::Safe,
2662                    rustc_abi::ExternAbi::Rust,
2663                    variant.requires.clone(),
2664                    inputs,
2665                    output,
2666                )
2667            })
2668        })
2669    }
2670}
2671
2672impl TyKind {
2673    fn intern(self) -> Ty {
2674        Ty(Interned::new(self))
2675    }
2676}
2677
2678/// returns the same invariants as for `usize` which is the length of a slice
2679fn slice_invariants(overflow_mode: OverflowMode) -> &'static [Invariant] {
2680    static DEFAULT: LazyLock<[Invariant; 1]> = LazyLock::new(|| {
2681        [Invariant { pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int) }]
2682    });
2683    static OVERFLOW: LazyLock<[Invariant; 2]> = LazyLock::new(|| {
2684        [
2685            Invariant {
2686                pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int),
2687            },
2688            Invariant {
2689                pred: Binder::bind_with_sort(
2690                    Expr::le(Expr::nu(), Expr::uint_max(UintTy::Usize)),
2691                    Sort::Int,
2692                ),
2693            },
2694        ]
2695    });
2696    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2697        &*OVERFLOW
2698    } else {
2699        &*DEFAULT
2700    }
2701}
2702
2703fn uint_invariants(uint_ty: UintTy, overflow_mode: OverflowMode) -> &'static [Invariant] {
2704    static DEFAULT: LazyLock<[Invariant; 1]> = LazyLock::new(|| {
2705        [Invariant { pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int) }]
2706    });
2707
2708    static OVERFLOW: LazyLock<UnordMap<UintTy, [Invariant; 2]>> = LazyLock::new(|| {
2709        UINT_TYS
2710            .into_iter()
2711            .map(|uint_ty| {
2712                let invariants = [
2713                    Invariant {
2714                        pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int),
2715                    },
2716                    Invariant {
2717                        pred: Binder::bind_with_sort(
2718                            Expr::le(Expr::nu(), Expr::uint_max(uint_ty)),
2719                            Sort::Int,
2720                        ),
2721                    },
2722                ];
2723                (uint_ty, invariants)
2724            })
2725            .collect()
2726    });
2727    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2728        &OVERFLOW[&uint_ty]
2729    } else {
2730        &*DEFAULT
2731    }
2732}
2733
2734fn int_invariants(int_ty: IntTy, overflow_mode: OverflowMode) -> &'static [Invariant] {
2735    static DEFAULT: [Invariant; 0] = [];
2736
2737    static OVERFLOW: LazyLock<UnordMap<IntTy, [Invariant; 2]>> = LazyLock::new(|| {
2738        INT_TYS
2739            .into_iter()
2740            .map(|int_ty| {
2741                let invariants = [
2742                    Invariant {
2743                        pred: Binder::bind_with_sort(
2744                            Expr::ge(Expr::nu(), Expr::int_min(int_ty)),
2745                            Sort::Int,
2746                        ),
2747                    },
2748                    Invariant {
2749                        pred: Binder::bind_with_sort(
2750                            Expr::le(Expr::nu(), Expr::int_max(int_ty)),
2751                            Sort::Int,
2752                        ),
2753                    },
2754                ];
2755                (int_ty, invariants)
2756            })
2757            .collect()
2758    });
2759    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2760        &OVERFLOW[&int_ty]
2761    } else {
2762        &DEFAULT
2763    }
2764}
2765
2766impl_internable!(AdtDefData, AdtSortDefData, TyKind);
2767impl_slice_internable!(
2768    Ty,
2769    GenericArg,
2770    Ensures,
2771    InferMode,
2772    Sort,
2773    SortArg,
2774    GenericParamDef,
2775    TraitRef,
2776    Binder<ExistentialPredicate>,
2777    Clause,
2778    PolyVariant,
2779    Invariant,
2780    RefineParam,
2781    FluxDefId,
2782    SortParamKind,
2783    AssocReft
2784);
2785
2786#[macro_export]
2787macro_rules! _Int {
2788    ($int_ty:pat, $idxs:pat) => {
2789        TyKind::Indexed(BaseTy::Int($int_ty), $idxs)
2790    };
2791}
2792pub use crate::_Int as Int;
2793
2794#[macro_export]
2795macro_rules! _Uint {
2796    ($uint_ty:pat, $idxs:pat) => {
2797        TyKind::Indexed(BaseTy::Uint($uint_ty), $idxs)
2798    };
2799}
2800pub use crate::_Uint as Uint;
2801
2802#[macro_export]
2803macro_rules! _Bool {
2804    ($idxs:pat) => {
2805        TyKind::Indexed(BaseTy::Bool, $idxs)
2806    };
2807}
2808pub use crate::_Bool as Bool;
2809
2810#[macro_export]
2811macro_rules! _Char {
2812    ($idxs:pat) => {
2813        TyKind::Indexed(BaseTy::Char, $idxs)
2814    };
2815}
2816pub use crate::_Char as Char;
2817
2818#[macro_export]
2819macro_rules! _Ref {
2820    ($($pats:pat),+ $(,)?) => {
2821        $crate::rty::TyKind::Indexed($crate::rty::BaseTy::Ref($($pats),+), _)
2822    };
2823}
2824pub use crate::_Ref as Ref;
2825
2826pub struct WfckResults {
2827    pub owner: FluxOwnerId,
2828    param_sorts: UnordMap<fhir::ParamId, Sort>,
2829    bin_op_sorts: ItemLocalMap<Sort>,
2830    fn_app_sorts: ItemLocalMap<List<SortArg>>,
2831    coercions: ItemLocalMap<Vec<Coercion>>,
2832    field_projs: ItemLocalMap<FieldProj>,
2833    node_sorts: ItemLocalMap<Sort>,
2834    record_ctors: ItemLocalMap<DefId>,
2835}
2836
2837#[derive(Clone, Copy, Debug)]
2838pub enum Coercion {
2839    Inject(DefId),
2840    Project(DefId),
2841}
2842
2843pub type ItemLocalMap<T> = UnordMap<fhir::ItemLocalId, T>;
2844
2845#[derive(Debug)]
2846pub struct LocalTableInContext<'a, T> {
2847    owner: FluxOwnerId,
2848    data: &'a ItemLocalMap<T>,
2849}
2850
2851pub struct LocalTableInContextMut<'a, T> {
2852    owner: FluxOwnerId,
2853    data: &'a mut ItemLocalMap<T>,
2854}
2855
2856impl WfckResults {
2857    pub fn new(owner: impl Into<FluxOwnerId>) -> Self {
2858        Self {
2859            owner: owner.into(),
2860            param_sorts: UnordMap::default(),
2861            bin_op_sorts: ItemLocalMap::default(),
2862            coercions: ItemLocalMap::default(),
2863            field_projs: ItemLocalMap::default(),
2864            node_sorts: ItemLocalMap::default(),
2865            record_ctors: ItemLocalMap::default(),
2866            fn_app_sorts: ItemLocalMap::default(),
2867        }
2868    }
2869
2870    pub fn param_sorts_mut(&mut self) -> &mut UnordMap<fhir::ParamId, Sort> {
2871        &mut self.param_sorts
2872    }
2873
2874    pub fn param_sorts(&self) -> &UnordMap<fhir::ParamId, Sort> {
2875        &self.param_sorts
2876    }
2877
2878    pub fn bin_op_sorts_mut(&mut self) -> LocalTableInContextMut<'_, Sort> {
2879        LocalTableInContextMut { owner: self.owner, data: &mut self.bin_op_sorts }
2880    }
2881
2882    pub fn fn_app_sorts_mut(&mut self) -> LocalTableInContextMut<'_, List<SortArg>> {
2883        LocalTableInContextMut { owner: self.owner, data: &mut self.fn_app_sorts }
2884    }
2885
2886    pub fn fn_app_sorts(&self) -> LocalTableInContext<'_, List<SortArg>> {
2887        LocalTableInContext { owner: self.owner, data: &self.fn_app_sorts }
2888    }
2889
2890    pub fn bin_op_sorts(&self) -> LocalTableInContext<'_, Sort> {
2891        LocalTableInContext { owner: self.owner, data: &self.bin_op_sorts }
2892    }
2893
2894    pub fn coercions_mut(&mut self) -> LocalTableInContextMut<'_, Vec<Coercion>> {
2895        LocalTableInContextMut { owner: self.owner, data: &mut self.coercions }
2896    }
2897
2898    pub fn coercions(&self) -> LocalTableInContext<'_, Vec<Coercion>> {
2899        LocalTableInContext { owner: self.owner, data: &self.coercions }
2900    }
2901
2902    pub fn field_projs_mut(&mut self) -> LocalTableInContextMut<'_, FieldProj> {
2903        LocalTableInContextMut { owner: self.owner, data: &mut self.field_projs }
2904    }
2905
2906    pub fn field_projs(&self) -> LocalTableInContext<'_, FieldProj> {
2907        LocalTableInContext { owner: self.owner, data: &self.field_projs }
2908    }
2909
2910    pub fn node_sorts_mut(&mut self) -> LocalTableInContextMut<'_, Sort> {
2911        LocalTableInContextMut { owner: self.owner, data: &mut self.node_sorts }
2912    }
2913
2914    pub fn node_sorts(&self) -> LocalTableInContext<'_, Sort> {
2915        LocalTableInContext { owner: self.owner, data: &self.node_sorts }
2916    }
2917
2918    pub fn record_ctors_mut(&mut self) -> LocalTableInContextMut<'_, DefId> {
2919        LocalTableInContextMut { owner: self.owner, data: &mut self.record_ctors }
2920    }
2921
2922    pub fn record_ctors(&self) -> LocalTableInContext<'_, DefId> {
2923        LocalTableInContext { owner: self.owner, data: &self.record_ctors }
2924    }
2925}
2926
2927impl<T> LocalTableInContextMut<'_, T> {
2928    pub fn insert(&mut self, fhir_id: FhirId, value: T) {
2929        tracked_span_assert_eq!(self.owner, fhir_id.owner);
2930        self.data.insert(fhir_id.local_id, value);
2931    }
2932}
2933
2934impl<'a, T> LocalTableInContext<'a, T> {
2935    pub fn get(&self, fhir_id: FhirId) -> Option<&'a T> {
2936        tracked_span_assert_eq!(self.owner, fhir_id.owner);
2937        self.data.get(&fhir_id.local_id)
2938    }
2939}