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, fast_reject::SimplifiedType};
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 field_sorts_instantiate_identity(&self) -> List<Sort> {
123        self.sorts.clone()
124    }
125
126    pub fn projections(&self, def_id: DefId) -> impl Iterator<Item = FieldProj> {
127        (0..self.fields()).map(move |i| FieldProj::Adt { def_id, field: i as u32 })
128    }
129}
130
131#[derive(Debug, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
132struct AdtSortDefData {
133    /// [`DefId`] of the struct or enum this data sort is associated to.
134    def_id: DefId,
135    /// The list of the type parameters used in the `#[flux::refined_by(..)]` annotation.
136    ///
137    /// See [`fhir::RefinedBy::sort_params`] for more details. This is a version of that but using
138    /// [`ParamTy`] instead of [`DefId`].
139    ///
140    /// The length of this list corresponds to the number of sort variables bound by this definition.
141    params: Vec<ParamTy>,
142    /// A vec of variants of the ADT;
143    /// - a `struct` sort -- used for types with a `refined_by` has a single variant;
144    /// - a `reflected` sort -- used for `reflected` enums have multiple variants
145    variants: IndexVec<VariantIdx, AdtSortVariant>,
146    is_reflected: bool,
147    is_struct: bool,
148}
149
150impl AdtSortDef {
151    pub fn new(
152        def_id: DefId,
153        params: Vec<ParamTy>,
154        variants: IndexVec<VariantIdx, AdtSortVariant>,
155        is_reflected: bool,
156        is_struct: bool,
157    ) -> Self {
158        Self(Interned::new(AdtSortDefData { def_id, params, variants, is_reflected, is_struct }))
159    }
160
161    pub fn did(&self) -> DefId {
162        self.0.def_id
163    }
164
165    pub fn variant(&self, idx: VariantIdx) -> &AdtSortVariant {
166        &self.0.variants[idx]
167    }
168
169    pub fn variants(&self) -> &IndexSlice<VariantIdx, AdtSortVariant> {
170        &self.0.variants
171    }
172
173    pub fn opt_struct_variant(&self) -> Option<&AdtSortVariant> {
174        if self.is_struct() { Some(self.struct_variant()) } else { None }
175    }
176
177    #[track_caller]
178    pub fn struct_variant(&self) -> &AdtSortVariant {
179        tracked_span_assert_eq!(self.0.is_struct, true);
180        &self.0.variants[FIRST_VARIANT]
181    }
182
183    pub fn is_reflected(&self) -> bool {
184        self.0.is_reflected
185    }
186
187    pub fn is_struct(&self) -> bool {
188        self.0.is_struct
189    }
190
191    pub fn to_sort(&self, args: &[GenericArg]) -> Sort {
192        let sorts = self
193            .filter_generic_args(args)
194            .map(|arg| arg.expect_base().sort())
195            .collect();
196
197        Sort::App(SortCtor::Adt(self.clone()), sorts)
198    }
199
200    /// Given a list of generic args, returns an iterator of the generic arguments that should be
201    /// mapped to sorts for instantiation.
202    pub fn filter_generic_args<'a, A>(&'a self, args: &'a [A]) -> impl Iterator<Item = &'a A> + 'a {
203        self.0.params.iter().map(|p| &args[p.index as usize])
204    }
205
206    pub fn identity_args(&self) -> List<Sort> {
207        (0..self.0.params.len())
208            .map(|i| Sort::Var(ParamSort::from(i)))
209            .collect()
210    }
211
212    /// Gives the number of sort variables bound by this definition.
213    pub fn param_count(&self) -> usize {
214        self.0.params.len()
215    }
216}
217
218#[derive(Debug, Clone, Default, Encodable, Decodable)]
219pub struct Generics {
220    pub parent: Option<DefId>,
221    pub parent_count: usize,
222    pub own_params: List<GenericParamDef>,
223    pub has_self: bool,
224}
225
226impl Generics {
227    pub fn count(&self) -> usize {
228        self.parent_count + self.own_params.len()
229    }
230
231    pub fn own_default_count(&self) -> usize {
232        self.own_params
233            .iter()
234            .filter(|param| {
235                match param.kind {
236                    GenericParamDefKind::Type { has_default }
237                    | GenericParamDefKind::Const { has_default }
238                    | GenericParamDefKind::Base { has_default } => has_default,
239                    GenericParamDefKind::Lifetime => false,
240                }
241            })
242            .count()
243    }
244
245    pub fn param_at(&self, param_index: usize, genv: GlobalEnv) -> QueryResult<GenericParamDef> {
246        if let Some(index) = param_index.checked_sub(self.parent_count) {
247            Ok(self.own_params[index].clone())
248        } else {
249            let parent = self.parent.expect("parent_count > 0 but no parent?");
250            genv.generics_of(parent)?.param_at(param_index, genv)
251        }
252    }
253
254    pub fn const_params(&self, genv: GlobalEnv) -> QueryResult<Vec<(ParamConst, Sort)>> {
255        // FIXME(nilehmann) this shouldn't use the methods in `flux_middle::sort_of` to get the sort
256        let mut res = vec![];
257        for i in 0..self.count() {
258            let param = self.param_at(i, genv)?;
259            if let GenericParamDefKind::Const { .. } = param.kind
260                && let Some(sort) = genv.sort_of_generic_param(param.def_id)?
261            {
262                let param_const = ParamConst { name: param.name, index: param.index };
263                res.push((param_const, sort));
264            }
265        }
266        Ok(res)
267    }
268}
269
270#[derive(Debug, Clone, TyEncodable, TyDecodable)]
271pub struct RefinementGenerics {
272    pub parent: Option<DefId>,
273    pub parent_count: usize,
274    pub own_params: List<RefineParam>,
275}
276
277#[derive(
278    PartialEq, Eq, Debug, Clone, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
279)]
280pub struct RefineParam {
281    pub sort: Sort,
282    pub name: Symbol,
283    pub mode: InferMode,
284}
285
286#[derive(Debug, Clone, PartialEq, Eq, Hash, Encodable, Decodable)]
287pub struct GenericParamDef {
288    pub kind: GenericParamDefKind,
289    pub def_id: DefId,
290    pub index: u32,
291    pub name: Symbol,
292}
293
294#[derive(Copy, Debug, Clone, PartialEq, Eq, Hash, Encodable, Decodable)]
295pub enum GenericParamDefKind {
296    Type { has_default: bool },
297    Base { has_default: bool },
298    Lifetime,
299    Const { has_default: bool },
300}
301
302pub const SELF_PARAM_TY: ParamTy = ParamTy { index: 0, name: kw::SelfUpper };
303
304#[derive(Debug, Clone, TyEncodable, TyDecodable)]
305pub struct GenericPredicates {
306    pub parent: Option<DefId>,
307    pub predicates: List<Clause>,
308}
309
310#[derive(
311    Debug, PartialEq, Eq, Hash, Clone, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
312)]
313pub struct Clause {
314    kind: Binder<ClauseKind>,
315}
316
317impl Clause {
318    pub fn new(vars: impl Into<List<BoundVariableKind>>, kind: ClauseKind) -> Self {
319        Clause { kind: Binder::bind_with_vars(kind, vars.into()) }
320    }
321
322    pub fn kind(&self) -> Binder<ClauseKind> {
323        self.kind.clone()
324    }
325
326    fn as_trait_clause(&self) -> Option<Binder<TraitPredicate>> {
327        let clause = self.kind();
328        if let ClauseKind::Trait(trait_clause) = clause.skip_binder_ref() {
329            Some(clause.rebind(trait_clause.clone()))
330        } else {
331            None
332        }
333    }
334
335    pub fn as_projection_clause(&self) -> Option<Binder<ProjectionPredicate>> {
336        let clause = self.kind();
337        if let ClauseKind::Projection(proj_clause) = clause.skip_binder_ref() {
338            Some(clause.rebind(proj_clause.clone()))
339        } else {
340            None
341        }
342    }
343
344    // FIXME(nilehmann) we should deal with the binder in all the places this is used instead of
345    // blindly skipping it here
346    pub fn kind_skipping_binder(&self) -> ClauseKind {
347        self.kind.clone().skip_binder()
348    }
349
350    /// Group `Fn` trait clauses with their corresponding `FnOnce::Output` projection
351    /// predicate. This assumes there's exactly one corresponding projection predicate and will
352    /// crash otherwise.
353    pub fn split_off_fn_trait_clauses(
354        genv: GlobalEnv,
355        clauses: &Clauses,
356    ) -> (Vec<Clause>, Vec<Binder<FnTraitPredicate>>) {
357        let mut fn_trait_clauses = vec![];
358        let mut fn_trait_output_clauses = vec![];
359        let mut rest = vec![];
360        for clause in clauses {
361            if let Some(trait_clause) = clause.as_trait_clause()
362                && let Some(kind) = genv.tcx().fn_trait_kind_from_def_id(trait_clause.def_id())
363            {
364                fn_trait_clauses.push((kind, trait_clause));
365            } else if let Some(proj_clause) = clause.as_projection_clause()
366                && genv.is_fn_output(proj_clause.projection_def_id())
367            {
368                fn_trait_output_clauses.push(proj_clause);
369            } else {
370                rest.push(clause.clone());
371            }
372        }
373        let fn_trait_clauses = fn_trait_clauses
374            .into_iter()
375            .map(|(kind, fn_trait_clause)| {
376                let mut candidates = vec![];
377                for fn_trait_output_clause in &fn_trait_output_clauses {
378                    if fn_trait_output_clause.self_ty() == fn_trait_clause.self_ty() {
379                        candidates.push(fn_trait_output_clause.clone());
380                    }
381                }
382                tracked_span_assert_eq!(candidates.len(), 1);
383                let proj_pred = candidates.pop().unwrap().skip_binder();
384                fn_trait_clause.map(|fn_trait_clause| {
385                    FnTraitPredicate {
386                        kind,
387                        self_ty: fn_trait_clause.self_ty().to_ty(),
388                        tupled_args: fn_trait_clause.trait_ref.args[1].expect_base().to_ty(),
389                        output: proj_pred.term.to_ty(),
390                    }
391                })
392            })
393            .collect_vec();
394        (rest, fn_trait_clauses)
395    }
396}
397
398impl<'tcx> ToRustc<'tcx> for Clause {
399    type T = rustc_middle::ty::Clause<'tcx>;
400
401    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
402        self.kind.to_rustc(tcx).upcast(tcx)
403    }
404}
405
406impl From<Binder<ClauseKind>> for Clause {
407    fn from(kind: Binder<ClauseKind>) -> Self {
408        Clause { kind }
409    }
410}
411
412pub type Clauses = List<Clause>;
413
414#[derive(
415    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
416)]
417pub enum ClauseKind {
418    Trait(TraitPredicate),
419    Projection(ProjectionPredicate),
420    RegionOutlives(RegionOutlivesPredicate),
421    TypeOutlives(TypeOutlivesPredicate),
422    ConstArgHasType(Const, Ty),
423}
424
425impl<'tcx> ToRustc<'tcx> for ClauseKind {
426    type T = rustc_middle::ty::ClauseKind<'tcx>;
427
428    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
429        match self {
430            ClauseKind::Trait(trait_predicate) => {
431                rustc_middle::ty::ClauseKind::Trait(trait_predicate.to_rustc(tcx))
432            }
433            ClauseKind::Projection(projection_predicate) => {
434                rustc_middle::ty::ClauseKind::Projection(projection_predicate.to_rustc(tcx))
435            }
436            ClauseKind::RegionOutlives(outlives_predicate) => {
437                rustc_middle::ty::ClauseKind::RegionOutlives(outlives_predicate.to_rustc(tcx))
438            }
439            ClauseKind::TypeOutlives(outlives_predicate) => {
440                rustc_middle::ty::ClauseKind::TypeOutlives(outlives_predicate.to_rustc(tcx))
441            }
442            ClauseKind::ConstArgHasType(constant, ty) => {
443                rustc_middle::ty::ClauseKind::ConstArgHasType(
444                    constant.to_rustc(tcx),
445                    ty.to_rustc(tcx),
446                )
447            }
448        }
449    }
450}
451
452#[derive(Eq, PartialEq, Hash, Clone, Debug, TyEncodable, TyDecodable)]
453pub struct OutlivesPredicate<T>(pub T, pub Region);
454
455pub type TypeOutlivesPredicate = OutlivesPredicate<Ty>;
456pub type RegionOutlivesPredicate = OutlivesPredicate<Region>;
457
458impl<'tcx, V: ToRustc<'tcx>> ToRustc<'tcx> for OutlivesPredicate<V> {
459    type T = rustc_middle::ty::OutlivesPredicate<'tcx, V::T>;
460
461    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
462        rustc_middle::ty::OutlivesPredicate(self.0.to_rustc(tcx), self.1.to_rustc(tcx))
463    }
464}
465
466#[derive(
467    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
468)]
469pub struct TraitPredicate {
470    pub trait_ref: TraitRef,
471}
472
473impl TraitPredicate {
474    fn self_ty(&self) -> SubsetTyCtor {
475        self.trait_ref.self_ty()
476    }
477}
478
479impl<'tcx> ToRustc<'tcx> for TraitPredicate {
480    type T = rustc_middle::ty::TraitPredicate<'tcx>;
481
482    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
483        rustc_middle::ty::TraitPredicate {
484            polarity: rustc_middle::ty::PredicatePolarity::Positive,
485            trait_ref: self.trait_ref.to_rustc(tcx),
486        }
487    }
488}
489
490pub type PolyTraitPredicate = Binder<TraitPredicate>;
491
492impl PolyTraitPredicate {
493    fn def_id(&self) -> DefId {
494        self.skip_binder_ref().trait_ref.def_id
495    }
496
497    fn self_ty(&self) -> Binder<SubsetTyCtor> {
498        self.clone().map(|predicate| predicate.self_ty())
499    }
500}
501
502#[derive(
503    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
504)]
505pub struct TraitRef {
506    pub def_id: DefId,
507    pub args: GenericArgs,
508}
509
510impl TraitRef {
511    pub fn self_ty(&self) -> SubsetTyCtor {
512        self.args[0].expect_base().clone()
513    }
514}
515
516impl<'tcx> ToRustc<'tcx> for TraitRef {
517    type T = rustc_middle::ty::TraitRef<'tcx>;
518
519    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
520        rustc_middle::ty::TraitRef::new(tcx, self.def_id, self.args.to_rustc(tcx))
521    }
522}
523
524pub type PolyTraitRef = Binder<TraitRef>;
525
526impl PolyTraitRef {
527    pub fn def_id(&self) -> DefId {
528        self.as_ref().skip_binder().def_id
529    }
530}
531
532#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
533pub enum ExistentialPredicate {
534    Trait(ExistentialTraitRef),
535    Projection(ExistentialProjection),
536    AutoTrait(DefId),
537}
538
539pub type PolyExistentialPredicate = Binder<ExistentialPredicate>;
540
541impl ExistentialPredicate {
542    /// See [`rustc_middle::ty::ExistentialPredicateStableCmpExt`]
543    pub fn stable_cmp(&self, tcx: TyCtxt, other: &Self) -> Ordering {
544        match (self, other) {
545            (ExistentialPredicate::Trait(_), ExistentialPredicate::Trait(_)) => Ordering::Equal,
546            (ExistentialPredicate::Projection(a), ExistentialPredicate::Projection(b)) => {
547                tcx.def_path_hash(a.def_id)
548                    .cmp(&tcx.def_path_hash(b.def_id))
549            }
550            (ExistentialPredicate::AutoTrait(a), ExistentialPredicate::AutoTrait(b)) => {
551                tcx.def_path_hash(*a).cmp(&tcx.def_path_hash(*b))
552            }
553            (ExistentialPredicate::Trait(_), _) => Ordering::Less,
554            (ExistentialPredicate::Projection(_), ExistentialPredicate::Trait(_)) => {
555                Ordering::Greater
556            }
557            (ExistentialPredicate::Projection(_), _) => Ordering::Less,
558            (ExistentialPredicate::AutoTrait(_), _) => Ordering::Greater,
559        }
560    }
561}
562
563impl<'tcx> ToRustc<'tcx> for ExistentialPredicate {
564    type T = rustc_middle::ty::ExistentialPredicate<'tcx>;
565
566    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
567        match self {
568            ExistentialPredicate::Trait(trait_ref) => {
569                let trait_ref = rustc_middle::ty::ExistentialTraitRef::new_from_args(
570                    tcx,
571                    trait_ref.def_id,
572                    trait_ref.args.to_rustc(tcx),
573                );
574                rustc_middle::ty::ExistentialPredicate::Trait(trait_ref)
575            }
576            ExistentialPredicate::Projection(projection) => {
577                rustc_middle::ty::ExistentialPredicate::Projection(
578                    rustc_middle::ty::ExistentialProjection::new_from_args(
579                        tcx,
580                        projection.def_id,
581                        projection.args.to_rustc(tcx),
582                        projection.term.skip_binder_ref().to_rustc(tcx).into(),
583                    ),
584                )
585            }
586            ExistentialPredicate::AutoTrait(def_id) => {
587                rustc_middle::ty::ExistentialPredicate::AutoTrait(*def_id)
588            }
589        }
590    }
591}
592
593#[derive(
594    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
595)]
596pub struct ExistentialTraitRef {
597    pub def_id: DefId,
598    pub args: GenericArgs,
599}
600
601pub type PolyExistentialTraitRef = Binder<ExistentialTraitRef>;
602
603impl PolyExistentialTraitRef {
604    pub fn def_id(&self) -> DefId {
605        self.as_ref().skip_binder().def_id
606    }
607}
608
609#[derive(
610    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
611)]
612pub struct ExistentialProjection {
613    pub def_id: DefId,
614    pub args: GenericArgs,
615    pub term: SubsetTyCtor,
616}
617
618#[derive(
619    PartialEq, Eq, Hash, Debug, Clone, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
620)]
621pub struct ProjectionPredicate {
622    pub projection_ty: AliasTy,
623    pub term: SubsetTyCtor,
624}
625
626impl Pretty for ProjectionPredicate {
627    fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
628        write!(
629            f,
630            "ProjectionPredicate << projection_ty = {:?}, term = {:?} >>",
631            self.projection_ty, self.term
632        )
633    }
634}
635
636impl ProjectionPredicate {
637    pub fn self_ty(&self) -> SubsetTyCtor {
638        self.projection_ty.self_ty().clone()
639    }
640}
641
642impl<'tcx> ToRustc<'tcx> for ProjectionPredicate {
643    type T = rustc_middle::ty::ProjectionPredicate<'tcx>;
644
645    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
646        rustc_middle::ty::ProjectionPredicate {
647            projection_term: rustc_middle::ty::AliasTerm::new_from_args(
648                tcx,
649                self.projection_ty.def_id,
650                self.projection_ty.args.to_rustc(tcx),
651            ),
652            term: self.term.as_bty_skipping_binder().to_rustc(tcx).into(),
653        }
654    }
655}
656
657pub type PolyProjectionPredicate = Binder<ProjectionPredicate>;
658
659impl PolyProjectionPredicate {
660    pub fn projection_def_id(&self) -> DefId {
661        self.skip_binder_ref().projection_ty.def_id
662    }
663
664    pub fn self_ty(&self) -> Binder<SubsetTyCtor> {
665        self.clone().map(|predicate| predicate.self_ty())
666    }
667}
668
669#[derive(
670    Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
671)]
672pub struct FnTraitPredicate {
673    pub self_ty: Ty,
674    pub tupled_args: Ty,
675    pub output: Ty,
676    pub kind: ClosureKind,
677}
678
679impl Pretty for FnTraitPredicate {
680    fn fmt(&self, _cx: &PrettyCx, f: &mut fmt::Formatter<'_>) -> fmt::Result {
681        write!(
682            f,
683            "self = {:?}, args = {:?}, output = {:?}, kind = {}",
684            self.self_ty, self.tupled_args, self.output, self.kind
685        )
686    }
687}
688
689impl FnTraitPredicate {
690    pub fn fndef_sig(&self) -> FnSig {
691        let inputs = self.tupled_args.expect_tuple().iter().cloned().collect();
692        let ret = self.output.clone().shift_in_escaping(1);
693        let output = Binder::bind_with_vars(FnOutput::new(ret, vec![]), List::empty());
694        FnSig::new(Safety::Safe, rustc_abi::ExternAbi::Rust, List::empty(), inputs, output)
695    }
696}
697
698pub fn to_closure_sig(
699    tcx: TyCtxt,
700    closure_id: LocalDefId,
701    tys: &[Ty],
702    args: &flux_rustc_bridge::ty::GenericArgs,
703    poly_sig: &PolyFnSig,
704) -> PolyFnSig {
705    let closure_args = args.as_closure();
706    let kind_ty = closure_args.kind_ty().to_rustc(tcx);
707    let Some(kind) = kind_ty.to_opt_closure_kind() else {
708        bug!("to_closure_sig: expected closure kind, found {kind_ty:?}");
709    };
710
711    let mut vars = poly_sig.vars().clone().to_vec();
712    let fn_sig = poly_sig.clone().skip_binder();
713    let closure_ty = Ty::closure(closure_id.into(), tys, args);
714    let env_ty = match kind {
715        ClosureKind::Fn => {
716            vars.push(BoundVariableKind::Region(BoundRegionKind::ClosureEnv));
717            let br = BoundRegion {
718                var: BoundVar::from_usize(vars.len() - 1),
719                kind: BoundRegionKind::ClosureEnv,
720            };
721            Ty::mk_ref(ReBound(INNERMOST, br), closure_ty, Mutability::Not)
722        }
723        ClosureKind::FnMut => {
724            vars.push(BoundVariableKind::Region(BoundRegionKind::ClosureEnv));
725            let br = BoundRegion {
726                var: BoundVar::from_usize(vars.len() - 1),
727                kind: BoundRegionKind::ClosureEnv,
728            };
729            Ty::mk_ref(ReBound(INNERMOST, br), closure_ty, Mutability::Mut)
730        }
731        ClosureKind::FnOnce => closure_ty,
732    };
733
734    let inputs = std::iter::once(env_ty)
735        .chain(fn_sig.inputs().iter().cloned())
736        .collect::<Vec<_>>();
737    let output = fn_sig.output().clone();
738
739    let fn_sig = crate::rty::FnSig::new(
740        fn_sig.safety,
741        fn_sig.abi,
742        fn_sig.requires.clone(), // crate::rty::List::empty(),
743        inputs.into(),
744        output,
745    );
746
747    PolyFnSig::bind_with_vars(fn_sig, List::from(vars))
748}
749
750#[derive(
751    Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
752)]
753pub struct CoroutineObligPredicate {
754    pub def_id: DefId,
755    pub resume_ty: Ty,
756    pub upvar_tys: List<Ty>,
757    pub output: Ty,
758}
759
760#[derive(Copy, Clone, Encodable, Decodable, Hash, PartialEq, Eq)]
761pub struct AssocReft {
762    pub def_id: FluxDefId,
763    // NOTE: Field is used to denote final associated generic refinements on Traits
764    pub final_: bool,
765    pub span: Span,
766}
767
768impl AssocReft {
769    pub fn new(def_id: FluxDefId, final_: bool, span: Span) -> Self {
770        Self { def_id, final_, span }
771    }
772
773    pub fn name(&self) -> Symbol {
774        self.def_id.name()
775    }
776
777    pub fn def_id(&self) -> FluxDefId {
778        self.def_id
779    }
780}
781
782#[derive(Clone, Encodable, Decodable)]
783pub struct AssocRefinements {
784    pub items: List<AssocReft>,
785}
786
787impl Default for AssocRefinements {
788    fn default() -> Self {
789        Self { items: List::empty() }
790    }
791}
792
793impl AssocRefinements {
794    pub fn get(&self, assoc_id: FluxDefId) -> AssocReft {
795        *self
796            .items
797            .into_iter()
798            .find(|it| it.def_id == assoc_id)
799            .unwrap_or_else(|| bug!("caller should guarantee existence of associated refinement"))
800    }
801
802    pub fn find(&self, name: Symbol) -> Option<AssocReft> {
803        Some(*self.items.into_iter().find(|it| it.name() == name)?)
804    }
805}
806
807#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
808pub enum SortCtor {
809    Set,
810    Map,
811    Adt(AdtSortDef),
812    User(FluxDefId),
813}
814
815newtype_index! {
816    /// [`ParamSort`] is used for polymorphic sorts (`Set`, `Map`, etc.) and [bit-vector size parameters].
817    /// They should occur "bound" under a [`PolyFuncSort`] or an [`AdtSortDef`]. We assume there's a
818    /// single binder and a [`ParamSort`] represents a variable as an index into the list of variables
819    /// bound by that binder, i.e., the representation doesnt't support higher-ranked sorts.
820    ///
821    /// [bit-vector size parameters]: BvSize::Param
822    #[debug_format = "?{}s"]
823    #[encodable]
824    pub struct ParamSort {}
825}
826
827newtype_index! {
828    /// A *sort* *v*variable *id*
829    #[debug_format = "?{}s"]
830    #[encodable]
831    pub struct SortVid {}
832}
833
834impl ena::unify::UnifyKey for SortVid {
835    type Value = Option<Sort>;
836
837    #[inline]
838    fn index(&self) -> u32 {
839        self.as_u32()
840    }
841
842    #[inline]
843    fn from_index(u: u32) -> Self {
844        SortVid::from_u32(u)
845    }
846
847    fn tag() -> &'static str {
848        "SortVid"
849    }
850}
851
852impl ena::unify::EqUnifyValue for Sort {}
853
854newtype_index! {
855    /// A *num*eric *v*variable *id*
856    #[debug_format = "?{}n"]
857    #[encodable]
858    pub struct NumVid {}
859}
860
861#[derive(Debug, Clone, Copy, PartialEq, Eq)]
862pub enum NumVarValue {
863    Real,
864    Int,
865    BitVec(BvSize),
866}
867
868impl NumVarValue {
869    pub fn to_sort(self) -> Sort {
870        match self {
871            NumVarValue::Real => Sort::Real,
872            NumVarValue::Int => Sort::Int,
873            NumVarValue::BitVec(size) => Sort::BitVec(size),
874        }
875    }
876}
877
878impl ena::unify::UnifyKey for NumVid {
879    type Value = Option<NumVarValue>;
880
881    #[inline]
882    fn index(&self) -> u32 {
883        self.as_u32()
884    }
885
886    #[inline]
887    fn from_index(u: u32) -> Self {
888        NumVid::from_u32(u)
889    }
890
891    fn tag() -> &'static str {
892        "NumVid"
893    }
894}
895
896impl ena::unify::EqUnifyValue for NumVarValue {}
897
898/// A placeholder for a sort that needs to be inferred
899#[derive(PartialEq, Eq, Clone, Copy, Hash, Encodable, Decodable)]
900pub enum SortInfer {
901    /// A sort variable.
902    SortVar(SortVid),
903    /// A numeric sort variable.
904    NumVar(NumVid),
905}
906
907newtype_index! {
908    /// A *b*it *v*ector *size* *v*variable *id*
909    #[debug_format = "?{}size"]
910    #[encodable]
911    pub struct BvSizeVid {}
912}
913
914impl ena::unify::UnifyKey for BvSizeVid {
915    type Value = Option<BvSize>;
916
917    #[inline]
918    fn index(&self) -> u32 {
919        self.as_u32()
920    }
921
922    #[inline]
923    fn from_index(u: u32) -> Self {
924        BvSizeVid::from_u32(u)
925    }
926
927    fn tag() -> &'static str {
928        "BvSizeVid"
929    }
930}
931
932impl ena::unify::EqUnifyValue for BvSize {}
933
934#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
935pub enum Sort {
936    Int,
937    Bool,
938    Real,
939    BitVec(BvSize),
940    Str,
941    Char,
942    Loc,
943    Param(ParamTy),
944    Tuple(List<Sort>),
945    Alias(AliasKind, AliasTy),
946    Func(PolyFuncSort),
947    App(SortCtor, List<Sort>),
948    Var(ParamSort),
949    Infer(SortInfer),
950    Err,
951}
952
953pub enum CastKind {
954    /// Identity cast, which is erasable (e.g. int -> int, char -> int)
955    Identity,
956    /// From bool to int
957    BoolToInt,
958    /// Casts to unit index, (e.g. int -> float)
959    IntoUnit,
960    /// Uninterpreted casts, only allowed with explicit flag
961    Uninterpreted,
962}
963
964impl Sort {
965    pub fn tuple(sorts: impl Into<List<Sort>>) -> Self {
966        Sort::Tuple(sorts.into())
967    }
968
969    pub fn app(ctor: SortCtor, sorts: List<Sort>) -> Self {
970        Sort::App(ctor, sorts)
971    }
972
973    pub fn unit() -> Self {
974        Self::tuple(vec![])
975    }
976
977    #[track_caller]
978    pub fn expect_func(&self) -> &PolyFuncSort {
979        if let Sort::Func(sort) = self { sort } else { bug!("expected `Sort::Func`") }
980    }
981
982    pub fn is_loc(&self) -> bool {
983        matches!(self, Sort::Loc)
984    }
985
986    pub fn is_unit(&self) -> bool {
987        matches!(self, Sort::Tuple(sorts) if sorts.is_empty())
988    }
989
990    pub fn is_unit_adt(&self) -> Option<DefId> {
991        if let Sort::App(SortCtor::Adt(sort_def), _) = self
992            && let Some(variant) = sort_def.opt_struct_variant()
993            && variant.fields() == 0
994        {
995            Some(sort_def.did())
996        } else {
997            None
998        }
999    }
1000
1001    /// Whether the sort is a function with return sort bool
1002    pub fn is_pred(&self) -> bool {
1003        matches!(self, Sort::Func(fsort) if fsort.skip_binders().output().is_bool())
1004    }
1005
1006    /// Returns `true` if the sort is [`Bool`].
1007    ///
1008    /// [`Bool`]: Sort::Bool
1009    #[must_use]
1010    pub fn is_bool(&self) -> bool {
1011        matches!(self, Self::Bool)
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    pub fn simplify_type(&self) -> Option<SimplifiedType> {
1623        self.as_bty_skipping_existentials()
1624            .and_then(BaseTy::simplify_type)
1625    }
1626}
1627
1628impl<'tcx> ToRustc<'tcx> for Ty {
1629    type T = rustc_middle::ty::Ty<'tcx>;
1630
1631    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
1632        match self.kind() {
1633            TyKind::Indexed(bty, _) => bty.to_rustc(tcx),
1634            TyKind::Exists(ty) => ty.skip_binder_ref().to_rustc(tcx),
1635            TyKind::Constr(_, ty) => ty.to_rustc(tcx),
1636            TyKind::Param(pty) => pty.to_ty(tcx),
1637            TyKind::StrgRef(re, _, ty) => {
1638                rustc_middle::ty::Ty::new_ref(
1639                    tcx,
1640                    re.to_rustc(tcx),
1641                    ty.to_rustc(tcx),
1642                    Mutability::Mut,
1643                )
1644            }
1645            TyKind::Infer(vid) => rustc_middle::ty::Ty::new_var(tcx, *vid),
1646            TyKind::Uninit
1647            | TyKind::Ptr(_, _)
1648            | TyKind::Discr(..)
1649            | TyKind::Downcast(..)
1650            | TyKind::Blocked(_) => bug!("TODO: to_rustc for `{self:?}`"),
1651        }
1652    }
1653}
1654
1655#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
1656pub enum TyKind {
1657    Indexed(BaseTy, Expr),
1658    Exists(Binder<Ty>),
1659    Constr(Expr, Ty),
1660    Uninit,
1661    StrgRef(Region, Path, Ty),
1662    Ptr(PtrKind, Path),
1663    /// This is a bit of a hack. We use this type internally to represent the result of
1664    /// [`Rvalue::Discriminant`] in a way that we can recover the necessary control information
1665    /// when checking a [`match`]. The hack is that we assume the dicriminant remains the same from
1666    /// the creation of this type until we use it in a [`match`].
1667    ///
1668    ///
1669    /// [`Rvalue::Discriminant`]: flux_rustc_bridge::mir::Rvalue::Discriminant
1670    /// [`match`]: flux_rustc_bridge::mir::TerminatorKind::SwitchInt
1671    Discr(AdtDef, Place),
1672    Param(ParamTy),
1673    Downcast(AdtDef, GenericArgs, Ty, VariantIdx, List<Ty>),
1674    Blocked(Ty),
1675    /// A type that needs to be inferred by matching the signature against a rust signature.
1676    /// [`TyKind::Infer`] appear as an intermediate step during `conv` and should not be present in
1677    /// the final signature.
1678    Infer(TyVid),
1679}
1680
1681#[derive(Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1682pub enum PtrKind {
1683    Mut(Region),
1684    Box,
1685}
1686
1687#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1688pub enum BaseTy {
1689    Int(IntTy),
1690    Uint(UintTy),
1691    Bool,
1692    Str,
1693    Char,
1694    Slice(Ty),
1695    Adt(AdtDef, GenericArgs),
1696    Float(FloatTy),
1697    RawPtr(Ty, Mutability),
1698    RawPtrMetadata(Ty),
1699    Ref(Region, Ty, Mutability),
1700    FnPtr(PolyFnSig),
1701    FnDef(DefId, GenericArgs),
1702    Tuple(List<Ty>),
1703    Alias(AliasKind, AliasTy),
1704    Array(Ty, Const),
1705    Never,
1706    Closure(DefId, /* upvar_tys */ List<Ty>, flux_rustc_bridge::ty::GenericArgs),
1707    Coroutine(DefId, /*resume_ty: */ Ty, /* upvar_tys: */ List<Ty>),
1708    Dynamic(List<Binder<ExistentialPredicate>>, Region),
1709    Param(ParamTy),
1710    Infer(TyVid),
1711    Foreign(DefId),
1712}
1713
1714impl BaseTy {
1715    pub fn opaque(alias_ty: AliasTy) -> BaseTy {
1716        BaseTy::Alias(AliasKind::Opaque, alias_ty)
1717    }
1718
1719    pub fn projection(alias_ty: AliasTy) -> BaseTy {
1720        BaseTy::Alias(AliasKind::Projection, alias_ty)
1721    }
1722
1723    pub fn adt(adt_def: AdtDef, args: GenericArgs) -> BaseTy {
1724        BaseTy::Adt(adt_def, args)
1725    }
1726
1727    pub fn fn_def(def_id: DefId, args: impl Into<GenericArgs>) -> BaseTy {
1728        BaseTy::FnDef(def_id, args.into())
1729    }
1730
1731    pub fn from_primitive_str(s: &str) -> Option<BaseTy> {
1732        match s {
1733            "i8" => Some(BaseTy::Int(IntTy::I8)),
1734            "i16" => Some(BaseTy::Int(IntTy::I16)),
1735            "i32" => Some(BaseTy::Int(IntTy::I32)),
1736            "i64" => Some(BaseTy::Int(IntTy::I64)),
1737            "i128" => Some(BaseTy::Int(IntTy::I128)),
1738            "u8" => Some(BaseTy::Uint(UintTy::U8)),
1739            "u16" => Some(BaseTy::Uint(UintTy::U16)),
1740            "u32" => Some(BaseTy::Uint(UintTy::U32)),
1741            "u64" => Some(BaseTy::Uint(UintTy::U64)),
1742            "u128" => Some(BaseTy::Uint(UintTy::U128)),
1743            "f16" => Some(BaseTy::Float(FloatTy::F16)),
1744            "f32" => Some(BaseTy::Float(FloatTy::F32)),
1745            "f64" => Some(BaseTy::Float(FloatTy::F64)),
1746            "f128" => Some(BaseTy::Float(FloatTy::F128)),
1747            "isize" => Some(BaseTy::Int(IntTy::Isize)),
1748            "usize" => Some(BaseTy::Uint(UintTy::Usize)),
1749            "bool" => Some(BaseTy::Bool),
1750            "char" => Some(BaseTy::Char),
1751            "str" => Some(BaseTy::Str),
1752            _ => None,
1753        }
1754    }
1755
1756    /// If `self` is a primitive, return its [`Symbol`].
1757    pub fn primitive_symbol(&self) -> Option<Symbol> {
1758        match self {
1759            BaseTy::Bool => Some(sym::bool),
1760            BaseTy::Char => Some(sym::char),
1761            BaseTy::Float(f) => {
1762                match f {
1763                    FloatTy::F16 => Some(sym::f16),
1764                    FloatTy::F32 => Some(sym::f32),
1765                    FloatTy::F64 => Some(sym::f64),
1766                    FloatTy::F128 => Some(sym::f128),
1767                }
1768            }
1769            BaseTy::Int(f) => {
1770                match f {
1771                    IntTy::Isize => Some(sym::isize),
1772                    IntTy::I8 => Some(sym::i8),
1773                    IntTy::I16 => Some(sym::i16),
1774                    IntTy::I32 => Some(sym::i32),
1775                    IntTy::I64 => Some(sym::i64),
1776                    IntTy::I128 => Some(sym::i128),
1777                }
1778            }
1779            BaseTy::Uint(f) => {
1780                match f {
1781                    UintTy::Usize => Some(sym::usize),
1782                    UintTy::U8 => Some(sym::u8),
1783                    UintTy::U16 => Some(sym::u16),
1784                    UintTy::U32 => Some(sym::u32),
1785                    UintTy::U64 => Some(sym::u64),
1786                    UintTy::U128 => Some(sym::u128),
1787                }
1788            }
1789            BaseTy::Str => Some(sym::str),
1790            _ => None,
1791        }
1792    }
1793
1794    pub fn is_integral(&self) -> bool {
1795        matches!(self, BaseTy::Int(_) | BaseTy::Uint(_))
1796    }
1797
1798    pub fn is_signed(&self) -> bool {
1799        matches!(self, BaseTy::Int(_))
1800    }
1801
1802    pub fn is_unsigned(&self) -> bool {
1803        matches!(self, BaseTy::Uint(_))
1804    }
1805
1806    pub fn is_float(&self) -> bool {
1807        matches!(self, BaseTy::Float(_))
1808    }
1809
1810    pub fn is_bool(&self) -> bool {
1811        matches!(self, BaseTy::Bool)
1812    }
1813
1814    fn is_struct(&self) -> bool {
1815        matches!(self, BaseTy::Adt(adt_def, _) if adt_def.is_struct())
1816    }
1817
1818    fn is_array(&self) -> bool {
1819        matches!(self, BaseTy::Array(..))
1820    }
1821
1822    fn is_slice(&self) -> bool {
1823        matches!(self, BaseTy::Slice(..))
1824    }
1825
1826    pub fn is_box(&self) -> bool {
1827        matches!(self, BaseTy::Adt(adt_def, _) if adt_def.is_box())
1828    }
1829
1830    pub fn is_char(&self) -> bool {
1831        matches!(self, BaseTy::Char)
1832    }
1833
1834    pub fn is_str(&self) -> bool {
1835        matches!(self, BaseTy::Str)
1836    }
1837
1838    pub fn invariants(
1839        &self,
1840        tcx: TyCtxt,
1841        overflow_mode: OverflowMode,
1842    ) -> impl Iterator<Item = Invariant> {
1843        let (invariants, args) = match self {
1844            BaseTy::Adt(adt_def, args) => (adt_def.invariants().skip_binder(), &args[..]),
1845            BaseTy::Uint(uint_ty) => (uint_invariants(*uint_ty, overflow_mode), &[][..]),
1846            BaseTy::Int(int_ty) => (int_invariants(*int_ty, overflow_mode), &[][..]),
1847            BaseTy::Slice(_) => (slice_invariants(overflow_mode), &[][..]),
1848            _ => (&[][..], &[][..]),
1849        };
1850        invariants
1851            .iter()
1852            .map(move |inv| EarlyBinder(inv).instantiate_ref(tcx, args, &[]))
1853    }
1854
1855    pub fn to_ty(&self) -> Ty {
1856        let sort = self.sort();
1857        if sort.is_unit() {
1858            Ty::indexed(self.clone(), Expr::unit())
1859        } else {
1860            Ty::exists(Binder::bind_with_sort(Ty::indexed(self.clone(), Expr::nu()), sort))
1861        }
1862    }
1863
1864    pub fn to_subset_ty_ctor(&self) -> SubsetTyCtor {
1865        let sort = self.sort();
1866        Binder::bind_with_sort(SubsetTy::trivial(self.clone(), Expr::nu()), sort)
1867    }
1868
1869    #[track_caller]
1870    pub fn expect_adt(&self) -> (&AdtDef, &[GenericArg]) {
1871        if let BaseTy::Adt(adt_def, args) = self {
1872            (adt_def, args)
1873        } else {
1874            tracked_span_bug!("expected adt `{self:?}`")
1875        }
1876    }
1877
1878    /// A type is an *atom* if it is "self-delimiting", i.e., it has a clear boundary
1879    /// when printed. This is used to avoid unnecessary parenthesis when pretty printing.
1880    pub fn is_atom(&self) -> bool {
1881        // (nilehmann) I'm not sure about this list, please adjust if you get any odd behavior
1882        matches!(
1883            self,
1884            BaseTy::Int(_)
1885                | BaseTy::Uint(_)
1886                | BaseTy::Slice(_)
1887                | BaseTy::Bool
1888                | BaseTy::Char
1889                | BaseTy::Str
1890                | BaseTy::Adt(..)
1891                | BaseTy::Tuple(..)
1892                | BaseTy::Param(_)
1893                | BaseTy::Array(..)
1894                | BaseTy::Never
1895                | BaseTy::Closure(..)
1896                | BaseTy::Coroutine(..)
1897                // opaque alias are atoms the way we print them now, but they won't
1898                // be if we print them as `impl Trait`
1899                | BaseTy::Alias(..)
1900        )
1901    }
1902
1903    /// Similar to [`rustc_infer::infer::canonical::ir::fast_reject::simplify_type`].
1904    ///
1905    /// This implementation is currently incomplete, so it should only be used in contexts
1906    /// where completeness is not required. Currently, it's used to find incoherent
1907    /// implementations when resolving associated constants. In this context, incompleteness
1908    /// is acceptable since the worst case outcome is simply failing to resolve a type-relative
1909    /// constant.
1910    fn simplify_type(&self) -> Option<SimplifiedType> {
1911        match self {
1912            BaseTy::Bool => Some(SimplifiedType::Bool),
1913            BaseTy::Char => Some(SimplifiedType::Char),
1914            BaseTy::Int(int_type) => Some(SimplifiedType::Int(*int_type)),
1915            BaseTy::Uint(uint_type) => Some(SimplifiedType::Uint(*uint_type)),
1916            BaseTy::Float(float_type) => Some(SimplifiedType::Float(*float_type)),
1917            BaseTy::Adt(def, _) => Some(SimplifiedType::Adt(def.did())),
1918            BaseTy::Str => Some(SimplifiedType::Str),
1919            BaseTy::Array(..) => Some(SimplifiedType::Array),
1920            BaseTy::Slice(..) => Some(SimplifiedType::Slice),
1921            BaseTy::RawPtr(_, mutbl) => Some(SimplifiedType::Ptr(*mutbl)),
1922            BaseTy::Ref(_, _, mutbl) => Some(SimplifiedType::Ref(*mutbl)),
1923            BaseTy::FnDef(def_id, _) | BaseTy::Closure(def_id, ..) => {
1924                Some(SimplifiedType::Closure(*def_id))
1925            }
1926            BaseTy::Coroutine(def_id, ..) => Some(SimplifiedType::Coroutine(*def_id)),
1927            BaseTy::Never => Some(SimplifiedType::Never),
1928            BaseTy::Tuple(tys) => Some(SimplifiedType::Tuple(tys.len())),
1929            BaseTy::FnPtr(poly_fn_sig) => {
1930                Some(SimplifiedType::Function(poly_fn_sig.skip_binder_ref().inputs().len()))
1931            }
1932            BaseTy::Foreign(def_id) => Some(SimplifiedType::Foreign(*def_id)),
1933            BaseTy::RawPtrMetadata(_)
1934            | BaseTy::Alias(..)
1935            | BaseTy::Param(_)
1936            | BaseTy::Dynamic(..)
1937            | BaseTy::Infer(_) => None,
1938        }
1939    }
1940}
1941
1942impl<'tcx> ToRustc<'tcx> for BaseTy {
1943    type T = rustc_middle::ty::Ty<'tcx>;
1944
1945    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
1946        use rustc_middle::ty;
1947        match self {
1948            BaseTy::Int(i) => ty::Ty::new_int(tcx, *i),
1949            BaseTy::Uint(i) => ty::Ty::new_uint(tcx, *i),
1950            BaseTy::Param(pty) => pty.to_ty(tcx),
1951            BaseTy::Slice(ty) => ty::Ty::new_slice(tcx, ty.to_rustc(tcx)),
1952            BaseTy::Bool => tcx.types.bool,
1953            BaseTy::Char => tcx.types.char,
1954            BaseTy::Str => tcx.types.str_,
1955            BaseTy::Adt(adt_def, args) => {
1956                let did = adt_def.did();
1957                let adt_def = tcx.adt_def(did);
1958                let args = args.to_rustc(tcx);
1959                ty::Ty::new_adt(tcx, adt_def, args)
1960            }
1961            BaseTy::FnDef(def_id, args) => {
1962                let args = args.to_rustc(tcx);
1963                ty::Ty::new_fn_def(tcx, *def_id, args)
1964            }
1965            BaseTy::Float(f) => ty::Ty::new_float(tcx, *f),
1966            BaseTy::RawPtr(ty, mutbl) => ty::Ty::new_ptr(tcx, ty.to_rustc(tcx), *mutbl),
1967            BaseTy::Ref(re, ty, mutbl) => {
1968                ty::Ty::new_ref(tcx, re.to_rustc(tcx), ty.to_rustc(tcx), *mutbl)
1969            }
1970            BaseTy::FnPtr(poly_sig) => ty::Ty::new_fn_ptr(tcx, poly_sig.to_rustc(tcx)),
1971            BaseTy::Tuple(tys) => {
1972                let ts = tys.iter().map(|ty| ty.to_rustc(tcx)).collect_vec();
1973                ty::Ty::new_tup(tcx, &ts)
1974            }
1975            BaseTy::Alias(kind, alias_ty) => {
1976                ty::Ty::new_alias(tcx, kind.to_rustc(tcx), alias_ty.to_rustc(tcx))
1977            }
1978            BaseTy::Array(ty, n) => {
1979                let ty = ty.to_rustc(tcx);
1980                let n = n.to_rustc(tcx);
1981                ty::Ty::new_array_with_const_len(tcx, ty, n)
1982            }
1983            BaseTy::Never => tcx.types.never,
1984            BaseTy::Closure(did, _, args) => ty::Ty::new_closure(tcx, *did, args.to_rustc(tcx)),
1985            BaseTy::Dynamic(exi_preds, re) => {
1986                let preds: Vec<_> = exi_preds
1987                    .iter()
1988                    .map(|pred| pred.to_rustc(tcx))
1989                    .collect_vec();
1990                let preds = tcx.mk_poly_existential_predicates(&preds);
1991                ty::Ty::new_dynamic(tcx, preds, re.to_rustc(tcx))
1992            }
1993            BaseTy::Coroutine(def_id, resume_ty, upvars) => {
1994                bug!("TODO: Generator {def_id:?} {resume_ty:?} {upvars:?}")
1995                // let args = args.iter().map(|arg| into_rustc_generic_arg(tcx, arg));
1996                // let args = tcx.mk_args_from_iter(args);
1997                // ty::Ty::new_generator(*tcx, *def_id, args, mov)
1998            }
1999            BaseTy::Infer(ty_vid) => ty::Ty::new_var(tcx, *ty_vid),
2000            BaseTy::Foreign(def_id) => ty::Ty::new_foreign(tcx, *def_id),
2001            BaseTy::RawPtrMetadata(ty) => {
2002                ty::Ty::new_ptr(
2003                    tcx,
2004                    ty.to_rustc(tcx),
2005                    RawPtrKind::FakeForPtrMetadata.to_mutbl_lossy(),
2006                )
2007            }
2008        }
2009    }
2010}
2011
2012#[derive(
2013    Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
2014)]
2015pub struct AliasTy {
2016    pub def_id: DefId,
2017    pub args: GenericArgs,
2018    /// Holds the refinement-arguments for opaque-types; empty for projections
2019    pub refine_args: RefineArgs,
2020}
2021
2022impl AliasTy {
2023    pub fn new(def_id: DefId, args: GenericArgs, refine_args: RefineArgs) -> Self {
2024        AliasTy { args, refine_args, def_id }
2025    }
2026}
2027
2028/// This methods work only with associated type projections (i.e., no opaque types)
2029impl AliasTy {
2030    pub fn self_ty(&self) -> SubsetTyCtor {
2031        self.args[0].expect_base().clone()
2032    }
2033
2034    pub fn with_self_ty(&self, self_ty: SubsetTyCtor) -> Self {
2035        Self {
2036            def_id: self.def_id,
2037            args: [GenericArg::Base(self_ty)]
2038                .into_iter()
2039                .chain(self.args.iter().skip(1).cloned())
2040                .collect(),
2041            refine_args: self.refine_args.clone(),
2042        }
2043    }
2044}
2045
2046impl<'tcx> ToRustc<'tcx> for AliasTy {
2047    type T = rustc_middle::ty::AliasTy<'tcx>;
2048
2049    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2050        rustc_middle::ty::AliasTy::new(tcx, self.def_id, self.args.to_rustc(tcx))
2051    }
2052}
2053
2054pub type RefineArgs = List<Expr>;
2055
2056#[extension(pub trait RefineArgsExt)]
2057impl RefineArgs {
2058    fn identity_for_item(genv: GlobalEnv, def_id: DefId) -> QueryResult<RefineArgs> {
2059        Self::for_item(genv, def_id, |param, index| {
2060            Ok(Expr::var(Var::EarlyParam(EarlyReftParam {
2061                index: index as u32,
2062                name: param.name(),
2063            })))
2064        })
2065    }
2066
2067    fn for_item<F>(genv: GlobalEnv, def_id: DefId, mut mk: F) -> QueryResult<RefineArgs>
2068    where
2069        F: FnMut(EarlyBinder<RefineParam>, usize) -> QueryResult<Expr>,
2070    {
2071        let reft_generics = genv.refinement_generics_of(def_id)?;
2072        let count = reft_generics.count();
2073        let mut args = Vec::with_capacity(count);
2074        reft_generics.fill_item(genv, &mut args, &mut mk)?;
2075        Ok(List::from_vec(args))
2076    }
2077}
2078
2079/// A type constructor meant to be used as generic a argument of [kind base]. This is just an alias
2080/// to [`Binder<SubsetTy>`], but we expect the binder to have a single bound variable of the sort of
2081/// the underlying [base type].
2082///
2083/// [kind base]: GenericParamDefKind::Base
2084/// [base type]: SubsetTy::bty
2085pub type SubsetTyCtor = Binder<SubsetTy>;
2086
2087impl SubsetTyCtor {
2088    pub fn as_bty_skipping_binder(&self) -> &BaseTy {
2089        &self.as_ref().skip_binder().bty
2090    }
2091
2092    pub fn to_ty(&self) -> Ty {
2093        let sort = self.sort();
2094        if sort.is_unit() {
2095            self.replace_bound_reft(&Expr::unit()).to_ty()
2096        } else if let Some(def_id) = sort.is_unit_adt() {
2097            self.replace_bound_reft(&Expr::unit_struct(def_id)).to_ty()
2098        } else {
2099            Ty::exists(self.as_ref().map(SubsetTy::to_ty))
2100        }
2101    }
2102
2103    pub fn to_ty_ctor(&self) -> TyCtor {
2104        self.as_ref().map(SubsetTy::to_ty)
2105    }
2106}
2107
2108/// A subset type is a simplified version of a type that has the form `{b[e] | p}` where `b` is a
2109/// [`BaseTy`], `e` a refinement index, and `p` a predicate.
2110///
2111/// These are mainly found under a [`Binder`] with a single variable of the base type's sort. This
2112/// can be interpreted as a type constructor or an existential type. For example, under a binder with a
2113/// variable `v` of sort `int`, we can interpret `{i32[v] | v > 0}` as:
2114/// - A lambda `λv:int. {i32[v] | v > 0}` that "constructs" types when applied to ints, or
2115/// - An existential type `∃v:int. {i32[v] | v > 0}`.
2116///
2117/// This second interpretation is the reason we call this a subset type, i.e., the type `∃v. {b[v] | p}`
2118/// corresponds to the subset of values of  type `b` whose index satisfies `p`. These are the types
2119/// written as `B{v: p}` in the surface syntax and correspond to the types supported in other
2120/// refinement type systems like Liquid Haskell (with the difference that we are explicit
2121/// about separating refinements from program values via an index).
2122///
2123/// The main purpose for subset types is to be used as generic arguments of [kind base] when
2124/// interpreted as type constructors. They have two key properties that makes them suitable
2125/// for this:
2126///
2127/// 1. **Syntactic Restriction**: Subset types are syntactically restricted, making it easier to
2128///    relate them structurally (e.g., for subtyping). For instance, given two types `S<λv. T1>` and
2129///    `S<λ. T2>`, if `T1` and `T2` are subset types, we know they match structurally (at least
2130///    shallowly). In particularly, the syntactic restriction rules out complex types like
2131///    `S<λv. (i32[v], i32[v])>` simplifying some operations.
2132///
2133/// 2. **Eager Canonicalization**: Subset types can be eagerly canonicalized via [*strengthening*]
2134///    during substitution. For example, suppose we have a function:
2135///    ```text
2136///    fn foo<T>(x: T[@a], y: { T[@b] | b == a }) { }
2137///    ```
2138///    If we instantiate `T` with `λv. { i32[v] | v > 0}`, after substitution and applying the
2139///    lambda (the indexing syntax `T[a]` corresponds to an application of the lambda), we get:
2140///    ```text
2141///    fn foo(x: {i32[@a] | a > 0}, y: { { i32[@b] | b > 0 } | b == a }) { }
2142///    ```
2143///    Via *strengthening* we can canonicalize this to
2144///    ```text
2145///    fn foo(x: {i32[@a] | a > 0}, y: { i32[@b] | b == a && b > 0 }) { }
2146///    ```
2147///    As a result, we can guarantee the syntactic restriction through substitution.
2148///
2149/// [kind base]: GenericParamDefKind::Base
2150/// [*strengthening*]: https://arxiv.org/pdf/2010.07763.pdf
2151#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)]
2152pub struct SubsetTy {
2153    /// The base type `b` in the subset type `{b[e] | p}`.
2154    ///
2155    /// **NOTE:** This is mostly going to be under a [`Binder`]. It is not yet clear to me whether
2156    /// this [`BaseTy`] should be able to mention variables in the binder. In general, in a type
2157    /// `∃v. {b[e] | p}`, it's fine to mention `v` inside `b`, but since [`SubsetTy`] is meant to
2158    /// facilitate syntactic manipulation we may want to restrict this.
2159    pub bty: BaseTy,
2160    /// The refinement index `e` in the subset type `{b[e] | p}`. This can be an arbitrary expression,
2161    /// which makes manipulation easier. However, since this is mostly found under a binder, we expect
2162    /// it to be [`Expr::nu()`].
2163    pub idx: Expr,
2164    /// The predicate `p` in the subset type `{b[e] | p}`.
2165    pub pred: Expr,
2166}
2167
2168impl SubsetTy {
2169    pub fn new(bty: BaseTy, idx: impl Into<Expr>, pred: impl Into<Expr>) -> Self {
2170        Self { bty, idx: idx.into(), pred: pred.into() }
2171    }
2172
2173    pub fn trivial(bty: BaseTy, idx: impl Into<Expr>) -> Self {
2174        Self::new(bty, idx, Expr::tt())
2175    }
2176
2177    pub fn strengthen(&self, pred: impl Into<Expr>) -> Self {
2178        let this = self.clone();
2179        let pred = Expr::and(this.pred, pred).simplify(&SnapshotMap::default());
2180        Self { bty: this.bty, idx: this.idx, pred }
2181    }
2182
2183    pub fn to_ty(&self) -> Ty {
2184        let bty = self.bty.clone();
2185        if self.pred.is_trivially_true() {
2186            Ty::indexed(bty, &self.idx)
2187        } else {
2188            Ty::constr(&self.pred, Ty::indexed(bty, &self.idx))
2189        }
2190    }
2191}
2192
2193impl<'tcx> ToRustc<'tcx> for SubsetTy {
2194    type T = rustc_middle::ty::Ty<'tcx>;
2195
2196    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::Ty<'tcx> {
2197        self.bty.to_rustc(tcx)
2198    }
2199}
2200
2201#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)]
2202pub enum GenericArg {
2203    Ty(Ty),
2204    Base(SubsetTyCtor),
2205    Lifetime(Region),
2206    Const(Const),
2207}
2208
2209impl GenericArg {
2210    #[track_caller]
2211    pub fn expect_type(&self) -> &Ty {
2212        if let GenericArg::Ty(ty) = self {
2213            ty
2214        } else {
2215            bug!("expected `rty::GenericArg::Ty`, found `{self:?}`")
2216        }
2217    }
2218
2219    #[track_caller]
2220    pub fn expect_base(&self) -> &SubsetTyCtor {
2221        if let GenericArg::Base(ctor) = self {
2222            ctor
2223        } else {
2224            bug!("expected `rty::GenericArg::Base`, found `{self:?}`")
2225        }
2226    }
2227
2228    pub fn from_param_def(param: &GenericParamDef) -> Self {
2229        match param.kind {
2230            GenericParamDefKind::Type { .. } => {
2231                let param_ty = ParamTy { index: param.index, name: param.name };
2232                GenericArg::Ty(Ty::param(param_ty))
2233            }
2234            GenericParamDefKind::Base { .. } => {
2235                // λv. T[v]
2236                let param_ty = ParamTy { index: param.index, name: param.name };
2237                GenericArg::Base(Binder::bind_with_sort(
2238                    SubsetTy::trivial(BaseTy::Param(param_ty), Expr::nu()),
2239                    Sort::Param(param_ty),
2240                ))
2241            }
2242            GenericParamDefKind::Lifetime => {
2243                let region = EarlyParamRegion { index: param.index, name: param.name };
2244                GenericArg::Lifetime(Region::ReEarlyParam(region))
2245            }
2246            GenericParamDefKind::Const { .. } => {
2247                let param_const = ParamConst { index: param.index, name: param.name };
2248                let kind = ConstKind::Param(param_const);
2249                GenericArg::Const(Const { kind })
2250            }
2251        }
2252    }
2253
2254    /// Creates a `GenericArgs` from the definition of generic parameters, by calling a closure to
2255    /// obtain arg. The closures get to observe the `GenericArgs` as they're being built, which can
2256    /// be used to correctly replace defaults of generic parameters.
2257    pub fn for_item<F>(genv: GlobalEnv, def_id: DefId, mut mk_kind: F) -> QueryResult<GenericArgs>
2258    where
2259        F: FnMut(&GenericParamDef, &[GenericArg]) -> GenericArg,
2260    {
2261        let defs = genv.generics_of(def_id)?;
2262        let count = defs.count();
2263        let mut args = Vec::with_capacity(count);
2264        Self::fill_item(genv, &mut args, &defs, &mut mk_kind)?;
2265        Ok(List::from_vec(args))
2266    }
2267
2268    pub fn identity_for_item(genv: GlobalEnv, def_id: DefId) -> QueryResult<GenericArgs> {
2269        Self::for_item(genv, def_id, |param, _| GenericArg::from_param_def(param))
2270    }
2271
2272    fn fill_item<F>(
2273        genv: GlobalEnv,
2274        args: &mut Vec<GenericArg>,
2275        generics: &Generics,
2276        mk_kind: &mut F,
2277    ) -> QueryResult<()>
2278    where
2279        F: FnMut(&GenericParamDef, &[GenericArg]) -> GenericArg,
2280    {
2281        if let Some(def_id) = generics.parent {
2282            let parent_generics = genv.generics_of(def_id)?;
2283            Self::fill_item(genv, args, &parent_generics, mk_kind)?;
2284        }
2285        for param in &generics.own_params {
2286            let kind = mk_kind(param, args);
2287            tracked_span_assert_eq!(param.index as usize, args.len());
2288            args.push(kind);
2289        }
2290        Ok(())
2291    }
2292}
2293
2294impl From<TyOrBase> for GenericArg {
2295    fn from(v: TyOrBase) -> Self {
2296        match v {
2297            TyOrBase::Ty(ty) => GenericArg::Ty(ty),
2298            TyOrBase::Base(ctor) => GenericArg::Base(ctor),
2299        }
2300    }
2301}
2302
2303impl<'tcx> ToRustc<'tcx> for GenericArg {
2304    type T = rustc_middle::ty::GenericArg<'tcx>;
2305
2306    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2307        use rustc_middle::ty;
2308        match self {
2309            GenericArg::Ty(ty) => ty::GenericArg::from(ty.to_rustc(tcx)),
2310            GenericArg::Base(ctor) => ty::GenericArg::from(ctor.skip_binder_ref().to_rustc(tcx)),
2311            GenericArg::Lifetime(re) => ty::GenericArg::from(re.to_rustc(tcx)),
2312            GenericArg::Const(c) => ty::GenericArg::from(c.to_rustc(tcx)),
2313        }
2314    }
2315}
2316
2317pub type GenericArgs = List<GenericArg>;
2318
2319#[extension(pub trait GenericArgsExt)]
2320impl GenericArgs {
2321    #[track_caller]
2322    fn box_args(&self) -> (&Ty, &Ty) {
2323        if let [GenericArg::Ty(deref), GenericArg::Ty(alloc)] = &self[..] {
2324            (deref, alloc)
2325        } else {
2326            bug!("invalid generic arguments for box");
2327        }
2328    }
2329
2330    // We can't implement [`ToRustc`] because of coherence so we add it here
2331    fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::GenericArgsRef<'tcx> {
2332        tcx.mk_args_from_iter(self.iter().map(|arg| arg.to_rustc(tcx)))
2333    }
2334
2335    fn rebase_onto(
2336        &self,
2337        tcx: &TyCtxt,
2338        source_ancestor: DefId,
2339        target_args: &GenericArgs,
2340    ) -> List<GenericArg> {
2341        let defs = tcx.generics_of(source_ancestor);
2342        target_args
2343            .iter()
2344            .chain(self.iter().skip(defs.count()))
2345            .cloned()
2346            .collect()
2347    }
2348}
2349
2350#[derive(Debug)]
2351pub enum TyOrBase {
2352    Ty(Ty),
2353    Base(SubsetTyCtor),
2354}
2355
2356impl TyOrBase {
2357    pub fn into_ty(self) -> Ty {
2358        match self {
2359            TyOrBase::Ty(ty) => ty,
2360            TyOrBase::Base(ctor) => ctor.to_ty(),
2361        }
2362    }
2363
2364    #[track_caller]
2365    pub fn expect_base(self) -> SubsetTyCtor {
2366        match self {
2367            TyOrBase::Base(ctor) => ctor,
2368            TyOrBase::Ty(_) => tracked_span_bug!("expected `TyOrBase::Base`"),
2369        }
2370    }
2371
2372    pub fn as_base(self) -> Option<SubsetTyCtor> {
2373        match self {
2374            TyOrBase::Base(ctor) => Some(ctor),
2375            TyOrBase::Ty(_) => None,
2376        }
2377    }
2378}
2379
2380#[derive(Debug, Clone, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
2381pub enum TyOrCtor {
2382    Ty(Ty),
2383    Ctor(TyCtor),
2384}
2385
2386impl TyOrCtor {
2387    #[track_caller]
2388    pub fn expect_ctor(self) -> TyCtor {
2389        match self {
2390            TyOrCtor::Ctor(ctor) => ctor,
2391            TyOrCtor::Ty(_) => tracked_span_bug!("expected `TyOrCtor::Ctor`"),
2392        }
2393    }
2394
2395    pub fn expect_subset_ty_ctor(self) -> SubsetTyCtor {
2396        self.expect_ctor().map(|ty| {
2397            if let canonicalize::CanonicalTy::Constr(constr_ty) = ty.shallow_canonicalize()
2398                && let TyKind::Indexed(bty, idx) = constr_ty.ty().kind()
2399                && idx.is_nu()
2400            {
2401                SubsetTy::new(bty.clone(), Expr::nu(), constr_ty.pred())
2402            } else {
2403                tracked_span_bug!()
2404            }
2405        })
2406    }
2407
2408    pub fn to_ty(&self) -> Ty {
2409        match self {
2410            TyOrCtor::Ctor(ctor) => ctor.to_ty(),
2411            TyOrCtor::Ty(ty) => ty.clone(),
2412        }
2413    }
2414}
2415
2416impl From<TyOrBase> for TyOrCtor {
2417    fn from(v: TyOrBase) -> Self {
2418        match v {
2419            TyOrBase::Ty(ty) => TyOrCtor::Ty(ty),
2420            TyOrBase::Base(ctor) => TyOrCtor::Ctor(ctor.to_ty_ctor()),
2421        }
2422    }
2423}
2424
2425impl CoroutineObligPredicate {
2426    pub fn to_poly_fn_sig(&self) -> PolyFnSig {
2427        let vars = vec![];
2428
2429        let resume_ty = &self.resume_ty;
2430        let env_ty = Ty::coroutine(self.def_id, resume_ty.clone(), self.upvar_tys.clone());
2431
2432        let inputs = List::from_arr([env_ty, resume_ty.clone()]);
2433        let output =
2434            Binder::bind_with_vars(FnOutput::new(self.output.clone(), vec![]), List::empty());
2435
2436        PolyFnSig::bind_with_vars(
2437            FnSig::new(Safety::Safe, rustc_abi::ExternAbi::RustCall, List::empty(), inputs, output),
2438            List::from(vars),
2439        )
2440    }
2441}
2442
2443impl RefinementGenerics {
2444    pub fn count(&self) -> usize {
2445        self.parent_count + self.own_params.len()
2446    }
2447
2448    pub fn own_count(&self) -> usize {
2449        self.own_params.len()
2450    }
2451}
2452
2453impl EarlyBinder<RefinementGenerics> {
2454    pub fn parent(&self) -> Option<DefId> {
2455        self.skip_binder_ref().parent
2456    }
2457
2458    pub fn parent_count(&self) -> usize {
2459        self.skip_binder_ref().parent_count
2460    }
2461
2462    pub fn count(&self) -> usize {
2463        self.skip_binder_ref().count()
2464    }
2465
2466    pub fn own_count(&self) -> usize {
2467        self.skip_binder_ref().own_count()
2468    }
2469
2470    pub fn own_param_at(&self, index: usize) -> EarlyBinder<RefineParam> {
2471        self.as_ref().map(|this| this.own_params[index].clone())
2472    }
2473
2474    pub fn param_at(
2475        &self,
2476        param_index: usize,
2477        genv: GlobalEnv,
2478    ) -> QueryResult<EarlyBinder<RefineParam>> {
2479        if let Some(index) = param_index.checked_sub(self.parent_count()) {
2480            Ok(self.own_param_at(index))
2481        } else {
2482            let parent = self.parent().expect("parent_count > 0 but no parent?");
2483            genv.refinement_generics_of(parent)?
2484                .param_at(param_index, genv)
2485        }
2486    }
2487
2488    pub fn iter_own_params(&self) -> impl Iterator<Item = EarlyBinder<RefineParam>> + use<'_> {
2489        self.skip_binder_ref()
2490            .own_params
2491            .iter()
2492            .cloned()
2493            .map(EarlyBinder)
2494    }
2495
2496    pub fn fill_item<F, R>(&self, genv: GlobalEnv, vec: &mut Vec<R>, mk: &mut F) -> QueryResult
2497    where
2498        F: FnMut(EarlyBinder<RefineParam>, usize) -> QueryResult<R>,
2499    {
2500        if let Some(def_id) = self.parent() {
2501            genv.refinement_generics_of(def_id)?
2502                .fill_item(genv, vec, mk)?;
2503        }
2504        for param in self.iter_own_params() {
2505            vec.push(mk(param, vec.len())?);
2506        }
2507        Ok(())
2508    }
2509}
2510
2511impl EarlyBinder<GenericPredicates> {
2512    pub fn predicates(&self) -> EarlyBinder<List<Clause>> {
2513        EarlyBinder(self.0.predicates.clone())
2514    }
2515}
2516
2517impl EarlyBinder<FuncSort> {
2518    /// See [`subst::GenericsSubstForSort`]
2519    pub fn instantiate_func_sort<E>(
2520        self,
2521        sort_for_param: impl FnMut(ParamTy) -> Result<Sort, E>,
2522    ) -> Result<FuncSort, E> {
2523        self.0.try_fold_with(&mut subst::GenericsSubstFolder::new(
2524            subst::GenericsSubstForSort { sort_for_param },
2525            &[],
2526        ))
2527    }
2528}
2529
2530impl VariantSig {
2531    pub fn new(
2532        adt_def: AdtDef,
2533        args: GenericArgs,
2534        fields: List<Ty>,
2535        idx: Expr,
2536        requires: List<Expr>,
2537    ) -> Self {
2538        VariantSig { adt_def, args, fields, idx, requires }
2539    }
2540
2541    pub fn fields(&self) -> &[Ty] {
2542        &self.fields
2543    }
2544
2545    pub fn ret(&self) -> Ty {
2546        let bty = BaseTy::Adt(self.adt_def.clone(), self.args.clone());
2547        let idx = self.idx.clone();
2548        Ty::indexed(bty, idx)
2549    }
2550}
2551
2552impl FnSig {
2553    pub fn new(
2554        safety: Safety,
2555        abi: rustc_abi::ExternAbi,
2556        requires: List<Expr>,
2557        inputs: List<Ty>,
2558        output: Binder<FnOutput>,
2559    ) -> Self {
2560        FnSig { safety, abi, requires, inputs, output }
2561    }
2562
2563    pub fn requires(&self) -> &[Expr] {
2564        &self.requires
2565    }
2566
2567    pub fn inputs(&self) -> &[Ty] {
2568        &self.inputs
2569    }
2570
2571    pub fn output(&self) -> Binder<FnOutput> {
2572        self.output.clone()
2573    }
2574}
2575
2576impl<'tcx> ToRustc<'tcx> for FnSig {
2577    type T = rustc_middle::ty::FnSig<'tcx>;
2578
2579    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2580        tcx.mk_fn_sig(
2581            self.inputs().iter().map(|ty| ty.to_rustc(tcx)),
2582            self.output().as_ref().skip_binder().to_rustc(tcx),
2583            false,
2584            self.safety,
2585            self.abi,
2586        )
2587    }
2588}
2589
2590impl FnOutput {
2591    pub fn new(ret: Ty, ensures: impl Into<List<Ensures>>) -> Self {
2592        Self { ret, ensures: ensures.into() }
2593    }
2594}
2595
2596impl<'tcx> ToRustc<'tcx> for FnOutput {
2597    type T = rustc_middle::ty::Ty<'tcx>;
2598
2599    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2600        self.ret.to_rustc(tcx)
2601    }
2602}
2603
2604impl AdtDef {
2605    pub fn new(
2606        rustc: ty::AdtDef,
2607        sort_def: AdtSortDef,
2608        invariants: Vec<Invariant>,
2609        opaque: bool,
2610    ) -> Self {
2611        AdtDef(Interned::new(AdtDefData { invariants, sort_def, opaque, rustc }))
2612    }
2613
2614    pub fn did(&self) -> DefId {
2615        self.0.rustc.did()
2616    }
2617
2618    pub fn sort_def(&self) -> &AdtSortDef {
2619        &self.0.sort_def
2620    }
2621
2622    pub fn sort(&self, args: &[GenericArg]) -> Sort {
2623        self.sort_def().to_sort(args)
2624    }
2625
2626    pub fn is_box(&self) -> bool {
2627        self.0.rustc.is_box()
2628    }
2629
2630    pub fn is_enum(&self) -> bool {
2631        self.0.rustc.is_enum()
2632    }
2633
2634    pub fn is_struct(&self) -> bool {
2635        self.0.rustc.is_struct()
2636    }
2637
2638    pub fn is_union(&self) -> bool {
2639        self.0.rustc.is_union()
2640    }
2641
2642    pub fn variants(&self) -> &IndexSlice<VariantIdx, VariantDef> {
2643        self.0.rustc.variants()
2644    }
2645
2646    pub fn variant(&self, idx: VariantIdx) -> &VariantDef {
2647        self.0.rustc.variant(idx)
2648    }
2649
2650    pub fn invariants(&self) -> EarlyBinder<&[Invariant]> {
2651        EarlyBinder(&self.0.invariants)
2652    }
2653
2654    pub fn discriminants(&self) -> impl Iterator<Item = (VariantIdx, u128)> + '_ {
2655        self.0.rustc.discriminants()
2656    }
2657
2658    pub fn is_opaque(&self) -> bool {
2659        self.0.opaque
2660    }
2661}
2662
2663impl EarlyBinder<PolyVariant> {
2664    // The field_idx is `Some(i)` when we have the `i`-th field of a `union`, in which case,
2665    // the `inputs` are _just_ the `i`-th type (and not all the types...)
2666    pub fn to_poly_fn_sig(&self, field_idx: Option<crate::FieldIdx>) -> EarlyBinder<PolyFnSig> {
2667        self.as_ref().map(|poly_variant| {
2668            poly_variant.as_ref().map(|variant| {
2669                let ret = variant.ret().shift_in_escaping(1);
2670                let output = Binder::bind_with_vars(FnOutput::new(ret, vec![]), List::empty());
2671                let inputs = match field_idx {
2672                    None => variant.fields.clone(),
2673                    Some(i) => List::singleton(variant.fields[i.index()].clone()),
2674                };
2675                FnSig::new(
2676                    Safety::Safe,
2677                    rustc_abi::ExternAbi::Rust,
2678                    variant.requires.clone(),
2679                    inputs,
2680                    output,
2681                )
2682            })
2683        })
2684    }
2685}
2686
2687impl TyKind {
2688    fn intern(self) -> Ty {
2689        Ty(Interned::new(self))
2690    }
2691}
2692
2693/// returns the same invariants as for `usize` which is the length of a slice
2694fn slice_invariants(overflow_mode: OverflowMode) -> &'static [Invariant] {
2695    static DEFAULT: LazyLock<[Invariant; 1]> = LazyLock::new(|| {
2696        [Invariant { pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int) }]
2697    });
2698    static OVERFLOW: LazyLock<[Invariant; 2]> = LazyLock::new(|| {
2699        [
2700            Invariant {
2701                pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int),
2702            },
2703            Invariant {
2704                pred: Binder::bind_with_sort(
2705                    Expr::le(Expr::nu(), Expr::uint_max(UintTy::Usize)),
2706                    Sort::Int,
2707                ),
2708            },
2709        ]
2710    });
2711    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2712        &*OVERFLOW
2713    } else {
2714        &*DEFAULT
2715    }
2716}
2717
2718fn uint_invariants(uint_ty: UintTy, overflow_mode: OverflowMode) -> &'static [Invariant] {
2719    static DEFAULT: LazyLock<[Invariant; 1]> = LazyLock::new(|| {
2720        [Invariant { pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int) }]
2721    });
2722
2723    static OVERFLOW: LazyLock<UnordMap<UintTy, [Invariant; 2]>> = LazyLock::new(|| {
2724        UINT_TYS
2725            .into_iter()
2726            .map(|uint_ty| {
2727                let invariants = [
2728                    Invariant {
2729                        pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int),
2730                    },
2731                    Invariant {
2732                        pred: Binder::bind_with_sort(
2733                            Expr::le(Expr::nu(), Expr::uint_max(uint_ty)),
2734                            Sort::Int,
2735                        ),
2736                    },
2737                ];
2738                (uint_ty, invariants)
2739            })
2740            .collect()
2741    });
2742    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2743        &OVERFLOW[&uint_ty]
2744    } else {
2745        &*DEFAULT
2746    }
2747}
2748
2749fn int_invariants(int_ty: IntTy, overflow_mode: OverflowMode) -> &'static [Invariant] {
2750    static DEFAULT: [Invariant; 0] = [];
2751
2752    static OVERFLOW: LazyLock<UnordMap<IntTy, [Invariant; 2]>> = LazyLock::new(|| {
2753        INT_TYS
2754            .into_iter()
2755            .map(|int_ty| {
2756                let invariants = [
2757                    Invariant {
2758                        pred: Binder::bind_with_sort(
2759                            Expr::ge(Expr::nu(), Expr::int_min(int_ty)),
2760                            Sort::Int,
2761                        ),
2762                    },
2763                    Invariant {
2764                        pred: Binder::bind_with_sort(
2765                            Expr::le(Expr::nu(), Expr::int_max(int_ty)),
2766                            Sort::Int,
2767                        ),
2768                    },
2769                ];
2770                (int_ty, invariants)
2771            })
2772            .collect()
2773    });
2774    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2775        &OVERFLOW[&int_ty]
2776    } else {
2777        &DEFAULT
2778    }
2779}
2780
2781impl_internable!(AdtDefData, AdtSortDefData, TyKind);
2782impl_slice_internable!(
2783    Ty,
2784    GenericArg,
2785    Ensures,
2786    InferMode,
2787    Sort,
2788    SortArg,
2789    GenericParamDef,
2790    TraitRef,
2791    Binder<ExistentialPredicate>,
2792    Clause,
2793    PolyVariant,
2794    Invariant,
2795    RefineParam,
2796    FluxDefId,
2797    SortParamKind,
2798    AssocReft
2799);
2800
2801#[macro_export]
2802macro_rules! _Int {
2803    ($int_ty:pat, $idxs:pat) => {
2804        TyKind::Indexed(BaseTy::Int($int_ty), $idxs)
2805    };
2806}
2807pub use crate::_Int as Int;
2808
2809#[macro_export]
2810macro_rules! _Uint {
2811    ($uint_ty:pat, $idxs:pat) => {
2812        TyKind::Indexed(BaseTy::Uint($uint_ty), $idxs)
2813    };
2814}
2815pub use crate::_Uint as Uint;
2816
2817#[macro_export]
2818macro_rules! _Bool {
2819    ($idxs:pat) => {
2820        TyKind::Indexed(BaseTy::Bool, $idxs)
2821    };
2822}
2823pub use crate::_Bool as Bool;
2824
2825#[macro_export]
2826macro_rules! _Char {
2827    ($idxs:pat) => {
2828        TyKind::Indexed(BaseTy::Char, $idxs)
2829    };
2830}
2831pub use crate::_Char as Char;
2832
2833#[macro_export]
2834macro_rules! _Ref {
2835    ($($pats:pat),+ $(,)?) => {
2836        $crate::rty::TyKind::Indexed($crate::rty::BaseTy::Ref($($pats),+), _)
2837    };
2838}
2839pub use crate::_Ref as Ref;
2840
2841pub struct WfckResults {
2842    pub owner: FluxOwnerId,
2843    param_sorts: UnordMap<fhir::ParamId, Sort>,
2844    bin_op_sorts: ItemLocalMap<Sort>,
2845    fn_app_sorts: ItemLocalMap<List<SortArg>>,
2846    coercions: ItemLocalMap<Vec<Coercion>>,
2847    field_projs: ItemLocalMap<FieldProj>,
2848    node_sorts: ItemLocalMap<Sort>,
2849    record_ctors: ItemLocalMap<DefId>,
2850}
2851
2852#[derive(Clone, Copy, Debug)]
2853pub enum Coercion {
2854    Inject(DefId),
2855    Project(DefId),
2856}
2857
2858pub type ItemLocalMap<T> = UnordMap<fhir::ItemLocalId, T>;
2859
2860#[derive(Debug)]
2861pub struct LocalTableInContext<'a, T> {
2862    owner: FluxOwnerId,
2863    data: &'a ItemLocalMap<T>,
2864}
2865
2866pub struct LocalTableInContextMut<'a, T> {
2867    owner: FluxOwnerId,
2868    data: &'a mut ItemLocalMap<T>,
2869}
2870
2871impl WfckResults {
2872    pub fn new(owner: impl Into<FluxOwnerId>) -> Self {
2873        Self {
2874            owner: owner.into(),
2875            param_sorts: UnordMap::default(),
2876            bin_op_sorts: ItemLocalMap::default(),
2877            coercions: ItemLocalMap::default(),
2878            field_projs: ItemLocalMap::default(),
2879            node_sorts: ItemLocalMap::default(),
2880            record_ctors: ItemLocalMap::default(),
2881            fn_app_sorts: ItemLocalMap::default(),
2882        }
2883    }
2884
2885    pub fn param_sorts_mut(&mut self) -> &mut UnordMap<fhir::ParamId, Sort> {
2886        &mut self.param_sorts
2887    }
2888
2889    pub fn param_sorts(&self) -> &UnordMap<fhir::ParamId, Sort> {
2890        &self.param_sorts
2891    }
2892
2893    pub fn bin_op_sorts_mut(&mut self) -> LocalTableInContextMut<'_, Sort> {
2894        LocalTableInContextMut { owner: self.owner, data: &mut self.bin_op_sorts }
2895    }
2896
2897    pub fn fn_app_sorts_mut(&mut self) -> LocalTableInContextMut<'_, List<SortArg>> {
2898        LocalTableInContextMut { owner: self.owner, data: &mut self.fn_app_sorts }
2899    }
2900
2901    pub fn fn_app_sorts(&self) -> LocalTableInContext<'_, List<SortArg>> {
2902        LocalTableInContext { owner: self.owner, data: &self.fn_app_sorts }
2903    }
2904
2905    pub fn bin_op_sorts(&self) -> LocalTableInContext<'_, Sort> {
2906        LocalTableInContext { owner: self.owner, data: &self.bin_op_sorts }
2907    }
2908
2909    pub fn coercions_mut(&mut self) -> LocalTableInContextMut<'_, Vec<Coercion>> {
2910        LocalTableInContextMut { owner: self.owner, data: &mut self.coercions }
2911    }
2912
2913    pub fn coercions(&self) -> LocalTableInContext<'_, Vec<Coercion>> {
2914        LocalTableInContext { owner: self.owner, data: &self.coercions }
2915    }
2916
2917    pub fn field_projs_mut(&mut self) -> LocalTableInContextMut<'_, FieldProj> {
2918        LocalTableInContextMut { owner: self.owner, data: &mut self.field_projs }
2919    }
2920
2921    pub fn field_projs(&self) -> LocalTableInContext<'_, FieldProj> {
2922        LocalTableInContext { owner: self.owner, data: &self.field_projs }
2923    }
2924
2925    pub fn node_sorts_mut(&mut self) -> LocalTableInContextMut<'_, Sort> {
2926        LocalTableInContextMut { owner: self.owner, data: &mut self.node_sorts }
2927    }
2928
2929    pub fn node_sorts(&self) -> LocalTableInContext<'_, Sort> {
2930        LocalTableInContext { owner: self.owner, data: &self.node_sorts }
2931    }
2932
2933    pub fn record_ctors_mut(&mut self) -> LocalTableInContextMut<'_, DefId> {
2934        LocalTableInContextMut { owner: self.owner, data: &mut self.record_ctors }
2935    }
2936
2937    pub fn record_ctors(&self) -> LocalTableInContext<'_, DefId> {
2938        LocalTableInContext { owner: self.owner, data: &self.record_ctors }
2939    }
2940}
2941
2942impl<T> LocalTableInContextMut<'_, T> {
2943    pub fn insert(&mut self, fhir_id: FhirId, value: T) {
2944        tracked_span_assert_eq!(self.owner, fhir_id.owner);
2945        self.data.insert(fhir_id.local_id, value);
2946    }
2947}
2948
2949impl<'a, T> LocalTableInContext<'a, T> {
2950    pub fn get(&self, fhir_id: FhirId) -> Option<&'a T> {
2951        tracked_span_assert_eq!(self.owner, fhir_id.owner);
2952        self.data.get(&fhir_id.local_id)
2953    }
2954}