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 { name: Symbol },
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 is_numeric(&self) -> bool {
1015        matches!(self, Self::Int | Self::Real)
1016    }
1017
1018    pub fn cast_kind(self: &Sort, to: &Sort) -> CastKind {
1019        if self == to
1020            || (matches!(self, Sort::Char | Sort::Int) && matches!(to, Sort::Char | Sort::Int))
1021        {
1022            CastKind::Identity
1023        } else if matches!(self, Sort::Bool) && matches!(to, Sort::Int) {
1024            CastKind::BoolToInt
1025        } else if to.is_unit() {
1026            CastKind::IntoUnit
1027        } else {
1028            CastKind::Uninterpreted
1029        }
1030    }
1031
1032    pub fn walk(&self, mut f: impl FnMut(&Sort, &[FieldProj])) {
1033        fn go(sort: &Sort, f: &mut impl FnMut(&Sort, &[FieldProj]), proj: &mut Vec<FieldProj>) {
1034            match sort {
1035                Sort::Tuple(flds) => {
1036                    for (i, sort) in flds.iter().enumerate() {
1037                        proj.push(FieldProj::Tuple { arity: flds.len(), field: i as u32 });
1038                        go(sort, f, proj);
1039                        proj.pop();
1040                    }
1041                }
1042                Sort::App(SortCtor::Adt(sort_def), args) if sort_def.is_struct() => {
1043                    let field_sorts = sort_def.struct_variant().field_sorts(args);
1044                    for (i, sort) in field_sorts.iter().enumerate() {
1045                        proj.push(FieldProj::Adt { def_id: sort_def.did(), field: i as u32 });
1046                        go(sort, f, proj);
1047                        proj.pop();
1048                    }
1049                }
1050                _ => {
1051                    f(sort, proj);
1052                }
1053            }
1054        }
1055        go(self, &mut f, &mut vec![]);
1056    }
1057}
1058
1059/// The size of a [bit-vector]
1060///
1061/// [bit-vector]: Sort::BitVec
1062#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1063pub enum BvSize {
1064    /// A fixed size
1065    Fixed(u32),
1066    /// A size that has been parameterized, e.g., bound under a [`PolyFuncSort`]
1067    Param(ParamSort),
1068    /// A size that needs to be inferred. Used during sort checking to instantiate bit-vector
1069    /// sizes at call-sites.
1070    Infer(BvSizeVid),
1071}
1072
1073impl rustc_errors::IntoDiagArg for Sort {
1074    fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1075        rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1076    }
1077}
1078
1079impl rustc_errors::IntoDiagArg for FuncSort {
1080    fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1081        rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1082    }
1083}
1084
1085#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
1086pub struct FuncSort {
1087    pub inputs_and_output: List<Sort>,
1088}
1089
1090impl FuncSort {
1091    pub fn new(mut inputs: Vec<Sort>, output: Sort) -> Self {
1092        inputs.push(output);
1093        FuncSort { inputs_and_output: List::from_vec(inputs) }
1094    }
1095
1096    pub fn inputs(&self) -> &[Sort] {
1097        &self.inputs_and_output[0..self.inputs_and_output.len() - 1]
1098    }
1099
1100    pub fn output(&self) -> &Sort {
1101        &self.inputs_and_output[self.inputs_and_output.len() - 1]
1102    }
1103
1104    pub fn to_poly(&self) -> PolyFuncSort {
1105        PolyFuncSort::new(List::empty(), self.clone())
1106    }
1107}
1108
1109/// See [`PolyFuncSort`]
1110#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)]
1111pub enum SortParamKind {
1112    Sort,
1113    BvSize,
1114}
1115
1116/// A polymorphic function sort parametric over [sorts] or [bit-vector sizes].
1117///
1118/// Parameterizing over bit-vector sizes is a bit of a stretch, because smtlib doesn't support full
1119/// parametric reasoning over them. As long as we used functions parameterized over a size monomorphically
1120/// we should be fine. Right now, we can guarantee this, because size parameters are not exposed in
1121/// the surface syntax and they are only used for predefined (interpreted) theory functions.
1122///
1123/// [sorts]: Sort
1124/// [bit-vector sizes]: BvSize::Param
1125#[derive(Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)]
1126pub struct PolyFuncSort {
1127    /// The list of parameters including sorts and bit vector sizes
1128    params: List<SortParamKind>,
1129    fsort: FuncSort,
1130}
1131
1132impl PolyFuncSort {
1133    pub fn new(params: List<SortParamKind>, fsort: FuncSort) -> Self {
1134        PolyFuncSort { params, fsort }
1135    }
1136
1137    pub fn skip_binders(&self) -> FuncSort {
1138        self.fsort.clone()
1139    }
1140
1141    pub fn instantiate_identity(&self) -> FuncSort {
1142        self.fsort.clone()
1143    }
1144
1145    pub fn expect_mono(&self) -> FuncSort {
1146        assert!(self.params.is_empty());
1147        self.fsort.clone()
1148    }
1149
1150    pub fn params(&self) -> impl ExactSizeIterator<Item = SortParamKind> + '_ {
1151        self.params.iter().copied()
1152    }
1153
1154    pub fn instantiate(&self, args: &[SortArg]) -> FuncSort {
1155        self.fsort.fold_with(&mut SortSubst::new(args))
1156    }
1157}
1158
1159/// An argument for a generic parameter in a [`Sort`] which can be either a generic sort or a
1160/// generic bit-vector size.
1161#[derive(
1162    Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
1163)]
1164pub enum SortArg {
1165    Sort(Sort),
1166    BvSize(BvSize),
1167}
1168
1169#[derive(Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1170pub enum ConstantInfo {
1171    /// An uninterpreted constant
1172    Uninterpreted,
1173    /// A non-integral constant whose value is specified by the user
1174    Interpreted(Expr, Sort),
1175}
1176
1177#[derive(Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1178pub struct AdtDef(Interned<AdtDefData>);
1179
1180#[derive(Debug, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1181pub struct AdtDefData {
1182    invariants: Vec<Invariant>,
1183    sort_def: AdtSortDef,
1184    opaque: bool,
1185    rustc: ty::AdtDef,
1186}
1187
1188/// Option-like enum to explicitly mark that we don't have information about an ADT because it was
1189/// annotated with `#[flux::opaque]`. Note that only structs can be marked as opaque.
1190#[derive(Clone, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
1191pub enum Opaqueness<T> {
1192    Opaque,
1193    Transparent(T),
1194}
1195
1196impl<T> Opaqueness<T> {
1197    pub fn map<S>(self, f: impl FnOnce(T) -> S) -> Opaqueness<S> {
1198        match self {
1199            Opaqueness::Opaque => Opaqueness::Opaque,
1200            Opaqueness::Transparent(value) => Opaqueness::Transparent(f(value)),
1201        }
1202    }
1203
1204    pub fn as_ref(&self) -> Opaqueness<&T> {
1205        match self {
1206            Opaqueness::Opaque => Opaqueness::Opaque,
1207            Opaqueness::Transparent(value) => Opaqueness::Transparent(value),
1208        }
1209    }
1210
1211    pub fn as_deref(&self) -> Opaqueness<&T::Target>
1212    where
1213        T: std::ops::Deref,
1214    {
1215        match self {
1216            Opaqueness::Opaque => Opaqueness::Opaque,
1217            Opaqueness::Transparent(value) => Opaqueness::Transparent(value.deref()),
1218        }
1219    }
1220
1221    pub fn ok_or_else<E>(self, err: impl FnOnce() -> E) -> Result<T, E> {
1222        match self {
1223            Opaqueness::Transparent(v) => Ok(v),
1224            Opaqueness::Opaque => Err(err()),
1225        }
1226    }
1227
1228    #[track_caller]
1229    pub fn expect(self, msg: &str) -> T {
1230        match self {
1231            Opaqueness::Transparent(val) => val,
1232            Opaqueness::Opaque => bug!("{}", msg),
1233        }
1234    }
1235
1236    pub fn ok_or_query_err(self, struct_id: DefId) -> Result<T, QueryErr> {
1237        self.ok_or_else(|| QueryErr::OpaqueStruct { struct_id })
1238    }
1239}
1240
1241impl<T, E> Opaqueness<Result<T, E>> {
1242    pub fn transpose(self) -> Result<Opaqueness<T>, E> {
1243        match self {
1244            Opaqueness::Transparent(Ok(x)) => Ok(Opaqueness::Transparent(x)),
1245            Opaqueness::Transparent(Err(e)) => Err(e),
1246            Opaqueness::Opaque => Ok(Opaqueness::Opaque),
1247        }
1248    }
1249}
1250
1251pub static INT_TYS: [IntTy; 6] =
1252    [IntTy::Isize, IntTy::I8, IntTy::I16, IntTy::I32, IntTy::I64, IntTy::I128];
1253pub static UINT_TYS: [UintTy; 6] =
1254    [UintTy::Usize, UintTy::U8, UintTy::U16, UintTy::U32, UintTy::U64, UintTy::U128];
1255
1256#[derive(
1257    Debug, Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable, TypeFoldable, TypeVisitable,
1258)]
1259pub struct Invariant {
1260    // This predicate may have sort variables, but we don't explicitly mark it like in `PolyFuncSort`.
1261    // See comment on `apply` for details.
1262    pred: Binder<Expr>,
1263}
1264
1265impl Invariant {
1266    pub fn new(pred: Binder<Expr>) -> Self {
1267        Self { pred }
1268    }
1269
1270    pub fn apply(&self, idx: &Expr) -> Expr {
1271        // The predicate may have sort variables but we don't explicitly instantiate them. This
1272        // works because within an expression, sort variables can only appear inside the sort
1273        // annotation for a lambda and invariants cannot have lambdas. It remains to instantiate
1274        // variables in the sort of the binder itself, but since we are removing it, we can avoid
1275        // the explicit instantiation. Ultimately, this works because the expression we generate in
1276        // fixpoint doesn't need sort annotations (sorts are re-inferred).
1277        self.pred.replace_bound_reft(idx)
1278    }
1279}
1280
1281pub type PolyVariants = List<Binder<VariantSig>>;
1282pub type PolyVariant = Binder<VariantSig>;
1283
1284#[derive(Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1285pub struct VariantSig {
1286    pub adt_def: AdtDef,
1287    pub args: GenericArgs,
1288    pub fields: List<Ty>,
1289    pub idx: Expr,
1290    pub requires: List<Expr>,
1291}
1292
1293pub type PolyFnSig = Binder<FnSig>;
1294
1295#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
1296pub struct FnSig {
1297    pub safety: Safety,
1298    pub abi: rustc_abi::ExternAbi,
1299    pub requires: List<Expr>,
1300    pub inputs: List<Ty>,
1301    pub output: Binder<FnOutput>,
1302}
1303
1304#[derive(
1305    Debug, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
1306)]
1307pub struct FnOutput {
1308    pub ret: Ty,
1309    pub ensures: List<Ensures>,
1310}
1311
1312#[derive(Clone, Eq, PartialEq, Hash, TyEncodable, TyDecodable)]
1313pub enum Ensures {
1314    Type(Path, Ty),
1315    Pred(Expr),
1316}
1317
1318#[derive(Debug, TypeVisitable, TypeFoldable)]
1319pub struct Qualifier {
1320    pub def_id: FluxLocalDefId,
1321    pub body: Binder<Expr>,
1322    pub global: bool,
1323}
1324
1325/// A `PrimOpProp` is a single property for a primitive operation which
1326/// can be conjoined to get the definition of the [`PrimRel`] for that
1327/// primitive operation.
1328#[derive(Debug, TypeVisitable, TypeFoldable)]
1329pub struct PrimOpProp {
1330    pub def_id: FluxLocalDefId,
1331    pub op: BinOp,
1332    pub body: Binder<Expr>,
1333}
1334
1335#[derive(Debug, TypeVisitable, TypeFoldable)]
1336pub struct PrimRel {
1337    pub body: Binder<Expr>,
1338}
1339
1340pub type TyCtor = Binder<Ty>;
1341
1342impl TyCtor {
1343    pub fn to_ty(&self) -> Ty {
1344        match &self.vars()[..] {
1345            [] => {
1346                return self.skip_binder_ref().shift_out_escaping(1);
1347            }
1348            [BoundVariableKind::Refine(sort, ..)] => {
1349                if sort.is_unit() {
1350                    return self.replace_bound_reft(&Expr::unit());
1351                }
1352                if let Some(def_id) = sort.is_unit_adt() {
1353                    return self.replace_bound_reft(&Expr::unit_struct(def_id));
1354                }
1355            }
1356            _ => {}
1357        }
1358        Ty::exists(self.clone())
1359    }
1360}
1361
1362#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1363pub struct Ty(Interned<TyKind>);
1364
1365impl Ty {
1366    pub fn kind(&self) -> &TyKind {
1367        &self.0
1368    }
1369
1370    /// Dummy type used for the `Self` of a `TraitRef` created when converting a trait object, and
1371    /// which gets removed in `ExistentialTraitRef`. This type must not appear anywhere in other
1372    /// converted types and must be a valid `rustc` type (i.e., we must be able to call `to_rustc`
1373    /// on it). `TyKind::Infer(TyVid(0))` does the job, with the caveat that we must skip 0 when
1374    /// generating `TyKind::Infer` for "type holes".
1375    pub fn trait_object_dummy_self() -> Ty {
1376        Ty::infer(TyVid::from_u32(0))
1377    }
1378
1379    pub fn dynamic(preds: impl Into<List<Binder<ExistentialPredicate>>>, region: Region) -> Ty {
1380        BaseTy::Dynamic(preds.into(), region).to_ty()
1381    }
1382
1383    pub fn strg_ref(re: Region, path: Path, ty: Ty) -> Ty {
1384        TyKind::StrgRef(re, path, ty).intern()
1385    }
1386
1387    pub fn ptr(pk: impl Into<PtrKind>, path: impl Into<Path>) -> Ty {
1388        TyKind::Ptr(pk.into(), path.into()).intern()
1389    }
1390
1391    pub fn constr(p: impl Into<Expr>, ty: Ty) -> Ty {
1392        TyKind::Constr(p.into(), ty).intern()
1393    }
1394
1395    pub fn uninit() -> Ty {
1396        TyKind::Uninit.intern()
1397    }
1398
1399    pub fn indexed(bty: BaseTy, idx: impl Into<Expr>) -> Ty {
1400        TyKind::Indexed(bty, idx.into()).intern()
1401    }
1402
1403    pub fn exists(ty: Binder<Ty>) -> Ty {
1404        TyKind::Exists(ty).intern()
1405    }
1406
1407    pub fn exists_with_constr(bty: BaseTy, pred: Expr) -> Ty {
1408        let sort = bty.sort();
1409        let ty = Ty::indexed(bty, Expr::nu());
1410        Ty::exists(Binder::bind_with_sort(Ty::constr(pred, ty), sort))
1411    }
1412
1413    pub fn discr(adt_def: AdtDef, place: Place) -> Ty {
1414        TyKind::Discr(adt_def, place).intern()
1415    }
1416
1417    pub fn unit() -> Ty {
1418        Ty::tuple(vec![])
1419    }
1420
1421    pub fn bool() -> Ty {
1422        BaseTy::Bool.to_ty()
1423    }
1424
1425    pub fn int(int_ty: IntTy) -> Ty {
1426        BaseTy::Int(int_ty).to_ty()
1427    }
1428
1429    pub fn uint(uint_ty: UintTy) -> Ty {
1430        BaseTy::Uint(uint_ty).to_ty()
1431    }
1432
1433    pub fn param(param_ty: ParamTy) -> Ty {
1434        TyKind::Param(param_ty).intern()
1435    }
1436
1437    pub fn downcast(
1438        adt: AdtDef,
1439        args: GenericArgs,
1440        ty: Ty,
1441        variant: VariantIdx,
1442        fields: List<Ty>,
1443    ) -> Ty {
1444        TyKind::Downcast(adt, args, ty, variant, fields).intern()
1445    }
1446
1447    pub fn blocked(ty: Ty) -> Ty {
1448        TyKind::Blocked(ty).intern()
1449    }
1450
1451    pub fn str() -> Ty {
1452        BaseTy::Str.to_ty()
1453    }
1454
1455    pub fn char() -> Ty {
1456        BaseTy::Char.to_ty()
1457    }
1458
1459    pub fn float(float_ty: FloatTy) -> Ty {
1460        BaseTy::Float(float_ty).to_ty()
1461    }
1462
1463    pub fn mk_ref(region: Region, ty: Ty, mutbl: Mutability) -> Ty {
1464        BaseTy::Ref(region, ty, mutbl).to_ty()
1465    }
1466
1467    pub fn mk_slice(ty: Ty) -> Ty {
1468        BaseTy::Slice(ty).to_ty()
1469    }
1470
1471    pub fn mk_box(genv: GlobalEnv, deref_ty: Ty, alloc_ty: Ty) -> QueryResult<Ty> {
1472        let def_id = genv.tcx().require_lang_item(LangItem::OwnedBox, DUMMY_SP);
1473        let adt_def = genv.adt_def(def_id)?;
1474
1475        let args = List::from_arr([GenericArg::Ty(deref_ty), GenericArg::Ty(alloc_ty)]);
1476
1477        let bty = BaseTy::adt(adt_def, args);
1478        Ok(Ty::indexed(bty, Expr::unit_struct(def_id)))
1479    }
1480
1481    pub fn mk_box_with_default_alloc(genv: GlobalEnv, deref_ty: Ty) -> QueryResult<Ty> {
1482        let def_id = genv.tcx().require_lang_item(LangItem::OwnedBox, DUMMY_SP);
1483
1484        let generics = genv.generics_of(def_id)?;
1485        let alloc_ty = genv
1486            .lower_type_of(generics.own_params[1].def_id)?
1487            .skip_binder()
1488            .refine(&Refiner::default_for_item(genv, def_id)?)?;
1489
1490        Ty::mk_box(genv, deref_ty, alloc_ty)
1491    }
1492
1493    pub fn tuple(tys: impl Into<List<Ty>>) -> Ty {
1494        BaseTy::Tuple(tys.into()).to_ty()
1495    }
1496
1497    pub fn array(ty: Ty, c: Const) -> Ty {
1498        BaseTy::Array(ty, c).to_ty()
1499    }
1500
1501    pub fn closure(
1502        did: DefId,
1503        tys: impl Into<List<Ty>>,
1504        args: &flux_rustc_bridge::ty::GenericArgs,
1505    ) -> Ty {
1506        BaseTy::Closure(did, tys.into(), args.clone()).to_ty()
1507    }
1508
1509    pub fn coroutine(did: DefId, resume_ty: Ty, upvar_tys: List<Ty>) -> Ty {
1510        BaseTy::Coroutine(did, resume_ty, upvar_tys).to_ty()
1511    }
1512
1513    pub fn never() -> Ty {
1514        BaseTy::Never.to_ty()
1515    }
1516
1517    pub fn infer(vid: TyVid) -> Ty {
1518        TyKind::Infer(vid).intern()
1519    }
1520
1521    pub fn unconstr(&self) -> (Ty, Expr) {
1522        fn go(this: &Ty, preds: &mut Vec<Expr>) -> Ty {
1523            if let TyKind::Constr(pred, ty) = this.kind() {
1524                preds.push(pred.clone());
1525                go(ty, preds)
1526            } else {
1527                this.clone()
1528            }
1529        }
1530        let mut preds = vec![];
1531        (go(self, &mut preds), Expr::and_from_iter(preds))
1532    }
1533
1534    pub fn unblocked(&self) -> Ty {
1535        match self.kind() {
1536            TyKind::Blocked(ty) => ty.clone(),
1537            _ => self.clone(),
1538        }
1539    }
1540
1541    /// Whether the type is an `int` or a `uint`
1542    pub fn is_integral(&self) -> bool {
1543        self.as_bty_skipping_existentials()
1544            .map(BaseTy::is_integral)
1545            .unwrap_or_default()
1546    }
1547
1548    /// Whether the type is a `bool`
1549    pub fn is_bool(&self) -> bool {
1550        self.as_bty_skipping_existentials()
1551            .map(BaseTy::is_bool)
1552            .unwrap_or_default()
1553    }
1554
1555    /// Whether the type is a `char`
1556    pub fn is_char(&self) -> bool {
1557        self.as_bty_skipping_existentials()
1558            .map(BaseTy::is_char)
1559            .unwrap_or_default()
1560    }
1561
1562    pub fn is_uninit(&self) -> bool {
1563        matches!(self.kind(), TyKind::Uninit)
1564    }
1565
1566    pub fn is_box(&self) -> bool {
1567        self.as_bty_skipping_existentials()
1568            .map(BaseTy::is_box)
1569            .unwrap_or_default()
1570    }
1571
1572    pub fn is_struct(&self) -> bool {
1573        self.as_bty_skipping_existentials()
1574            .map(BaseTy::is_struct)
1575            .unwrap_or_default()
1576    }
1577
1578    pub fn is_array(&self) -> bool {
1579        self.as_bty_skipping_existentials()
1580            .map(BaseTy::is_array)
1581            .unwrap_or_default()
1582    }
1583
1584    pub fn is_slice(&self) -> bool {
1585        self.as_bty_skipping_existentials()
1586            .map(BaseTy::is_slice)
1587            .unwrap_or_default()
1588    }
1589
1590    pub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy> {
1591        match self.kind() {
1592            TyKind::Indexed(bty, _) => Some(bty),
1593            TyKind::Exists(ty) => Some(ty.skip_binder_ref().as_bty_skipping_existentials()?),
1594            TyKind::Constr(_, ty) => ty.as_bty_skipping_existentials(),
1595            _ => None,
1596        }
1597    }
1598
1599    #[track_caller]
1600    pub fn expect_discr(&self) -> (&AdtDef, &Place) {
1601        if let TyKind::Discr(adt_def, place) = self.kind() {
1602            (adt_def, place)
1603        } else {
1604            tracked_span_bug!("expected discr")
1605        }
1606    }
1607
1608    #[track_caller]
1609    pub fn expect_adt(&self) -> (&AdtDef, &[GenericArg], &Expr) {
1610        if let TyKind::Indexed(BaseTy::Adt(adt_def, args), idx) = self.kind() {
1611            (adt_def, args, idx)
1612        } else {
1613            tracked_span_bug!("expected adt `{self:?}`")
1614        }
1615    }
1616
1617    #[track_caller]
1618    pub fn expect_tuple(&self) -> &[Ty] {
1619        if let TyKind::Indexed(BaseTy::Tuple(tys), _) = self.kind() {
1620            tys
1621        } else {
1622            tracked_span_bug!("expected tuple found `{self:?}` (kind: `{:?}`)", self.kind())
1623        }
1624    }
1625
1626    pub fn simplify_type(&self) -> Option<SimplifiedType> {
1627        self.as_bty_skipping_existentials()
1628            .and_then(BaseTy::simplify_type)
1629    }
1630}
1631
1632impl<'tcx> ToRustc<'tcx> for Ty {
1633    type T = rustc_middle::ty::Ty<'tcx>;
1634
1635    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
1636        match self.kind() {
1637            TyKind::Indexed(bty, _) => bty.to_rustc(tcx),
1638            TyKind::Exists(ty) => ty.skip_binder_ref().to_rustc(tcx),
1639            TyKind::Constr(_, ty) => ty.to_rustc(tcx),
1640            TyKind::Param(pty) => pty.to_ty(tcx),
1641            TyKind::StrgRef(re, _, ty) => {
1642                rustc_middle::ty::Ty::new_ref(
1643                    tcx,
1644                    re.to_rustc(tcx),
1645                    ty.to_rustc(tcx),
1646                    Mutability::Mut,
1647                )
1648            }
1649            TyKind::Infer(vid) => rustc_middle::ty::Ty::new_var(tcx, *vid),
1650            TyKind::Uninit
1651            | TyKind::Ptr(_, _)
1652            | TyKind::Discr(..)
1653            | TyKind::Downcast(..)
1654            | TyKind::Blocked(_) => bug!("TODO: to_rustc for `{self:?}`"),
1655        }
1656    }
1657}
1658
1659#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable, Debug)]
1660pub enum TyKind {
1661    Indexed(BaseTy, Expr),
1662    Exists(Binder<Ty>),
1663    Constr(Expr, Ty),
1664    Uninit,
1665    StrgRef(Region, Path, Ty),
1666    Ptr(PtrKind, Path),
1667    /// This is a bit of a hack. We use this type internally to represent the result of
1668    /// [`Rvalue::Discriminant`] in a way that we can recover the necessary control information
1669    /// when checking a [`match`]. The hack is that we assume the dicriminant remains the same from
1670    /// the creation of this type until we use it in a [`match`].
1671    ///
1672    ///
1673    /// [`Rvalue::Discriminant`]: flux_rustc_bridge::mir::Rvalue::Discriminant
1674    /// [`match`]: flux_rustc_bridge::mir::TerminatorKind::SwitchInt
1675    Discr(AdtDef, Place),
1676    Param(ParamTy),
1677    Downcast(AdtDef, GenericArgs, Ty, VariantIdx, List<Ty>),
1678    Blocked(Ty),
1679    /// A type that needs to be inferred by matching the signature against a rust signature.
1680    /// [`TyKind::Infer`] appear as an intermediate step during `conv` and should not be present in
1681    /// the final signature.
1682    Infer(TyVid),
1683}
1684
1685#[derive(Copy, Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1686pub enum PtrKind {
1687    Mut(Region),
1688    Box,
1689}
1690
1691#[derive(Clone, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1692pub enum BaseTy {
1693    Int(IntTy),
1694    Uint(UintTy),
1695    Bool,
1696    Str,
1697    Char,
1698    Slice(Ty),
1699    Adt(AdtDef, GenericArgs),
1700    Float(FloatTy),
1701    RawPtr(Ty, Mutability),
1702    RawPtrMetadata(Ty),
1703    Ref(Region, Ty, Mutability),
1704    FnPtr(PolyFnSig),
1705    FnDef(DefId, GenericArgs),
1706    Tuple(List<Ty>),
1707    Alias(AliasKind, AliasTy),
1708    Array(Ty, Const),
1709    Never,
1710    Closure(DefId, /* upvar_tys */ List<Ty>, flux_rustc_bridge::ty::GenericArgs),
1711    Coroutine(DefId, /*resume_ty: */ Ty, /* upvar_tys: */ List<Ty>),
1712    Dynamic(List<Binder<ExistentialPredicate>>, Region),
1713    Param(ParamTy),
1714    Infer(TyVid),
1715    Foreign(DefId),
1716}
1717
1718impl BaseTy {
1719    pub fn opaque(alias_ty: AliasTy) -> BaseTy {
1720        BaseTy::Alias(AliasKind::Opaque, alias_ty)
1721    }
1722
1723    pub fn projection(alias_ty: AliasTy) -> BaseTy {
1724        BaseTy::Alias(AliasKind::Projection, alias_ty)
1725    }
1726
1727    pub fn adt(adt_def: AdtDef, args: GenericArgs) -> BaseTy {
1728        BaseTy::Adt(adt_def, args)
1729    }
1730
1731    pub fn fn_def(def_id: DefId, args: impl Into<GenericArgs>) -> BaseTy {
1732        BaseTy::FnDef(def_id, args.into())
1733    }
1734
1735    pub fn from_primitive_str(s: &str) -> Option<BaseTy> {
1736        match s {
1737            "i8" => Some(BaseTy::Int(IntTy::I8)),
1738            "i16" => Some(BaseTy::Int(IntTy::I16)),
1739            "i32" => Some(BaseTy::Int(IntTy::I32)),
1740            "i64" => Some(BaseTy::Int(IntTy::I64)),
1741            "i128" => Some(BaseTy::Int(IntTy::I128)),
1742            "u8" => Some(BaseTy::Uint(UintTy::U8)),
1743            "u16" => Some(BaseTy::Uint(UintTy::U16)),
1744            "u32" => Some(BaseTy::Uint(UintTy::U32)),
1745            "u64" => Some(BaseTy::Uint(UintTy::U64)),
1746            "u128" => Some(BaseTy::Uint(UintTy::U128)),
1747            "f16" => Some(BaseTy::Float(FloatTy::F16)),
1748            "f32" => Some(BaseTy::Float(FloatTy::F32)),
1749            "f64" => Some(BaseTy::Float(FloatTy::F64)),
1750            "f128" => Some(BaseTy::Float(FloatTy::F128)),
1751            "isize" => Some(BaseTy::Int(IntTy::Isize)),
1752            "usize" => Some(BaseTy::Uint(UintTy::Usize)),
1753            "bool" => Some(BaseTy::Bool),
1754            "char" => Some(BaseTy::Char),
1755            "str" => Some(BaseTy::Str),
1756            _ => None,
1757        }
1758    }
1759
1760    /// If `self` is a primitive, return its [`Symbol`].
1761    pub fn primitive_symbol(&self) -> Option<Symbol> {
1762        match self {
1763            BaseTy::Bool => Some(sym::bool),
1764            BaseTy::Char => Some(sym::char),
1765            BaseTy::Float(f) => {
1766                match f {
1767                    FloatTy::F16 => Some(sym::f16),
1768                    FloatTy::F32 => Some(sym::f32),
1769                    FloatTy::F64 => Some(sym::f64),
1770                    FloatTy::F128 => Some(sym::f128),
1771                }
1772            }
1773            BaseTy::Int(f) => {
1774                match f {
1775                    IntTy::Isize => Some(sym::isize),
1776                    IntTy::I8 => Some(sym::i8),
1777                    IntTy::I16 => Some(sym::i16),
1778                    IntTy::I32 => Some(sym::i32),
1779                    IntTy::I64 => Some(sym::i64),
1780                    IntTy::I128 => Some(sym::i128),
1781                }
1782            }
1783            BaseTy::Uint(f) => {
1784                match f {
1785                    UintTy::Usize => Some(sym::usize),
1786                    UintTy::U8 => Some(sym::u8),
1787                    UintTy::U16 => Some(sym::u16),
1788                    UintTy::U32 => Some(sym::u32),
1789                    UintTy::U64 => Some(sym::u64),
1790                    UintTy::U128 => Some(sym::u128),
1791                }
1792            }
1793            BaseTy::Str => Some(sym::str),
1794            _ => None,
1795        }
1796    }
1797
1798    pub fn is_integral(&self) -> bool {
1799        matches!(self, BaseTy::Int(_) | BaseTy::Uint(_))
1800    }
1801
1802    pub fn is_numeric(&self) -> bool {
1803        matches!(self, BaseTy::Int(_) | BaseTy::Uint(_) | BaseTy::Float(_))
1804    }
1805
1806    pub fn is_signed(&self) -> bool {
1807        matches!(self, BaseTy::Int(_))
1808    }
1809
1810    pub fn is_unsigned(&self) -> bool {
1811        matches!(self, BaseTy::Uint(_))
1812    }
1813
1814    pub fn is_float(&self) -> bool {
1815        matches!(self, BaseTy::Float(_))
1816    }
1817
1818    pub fn is_bool(&self) -> bool {
1819        matches!(self, BaseTy::Bool)
1820    }
1821
1822    fn is_struct(&self) -> bool {
1823        matches!(self, BaseTy::Adt(adt_def, _) if adt_def.is_struct())
1824    }
1825
1826    fn is_array(&self) -> bool {
1827        matches!(self, BaseTy::Array(..))
1828    }
1829
1830    fn is_slice(&self) -> bool {
1831        matches!(self, BaseTy::Slice(..))
1832    }
1833
1834    pub fn is_box(&self) -> bool {
1835        matches!(self, BaseTy::Adt(adt_def, _) if adt_def.is_box())
1836    }
1837
1838    pub fn is_char(&self) -> bool {
1839        matches!(self, BaseTy::Char)
1840    }
1841
1842    pub fn is_str(&self) -> bool {
1843        matches!(self, BaseTy::Str)
1844    }
1845
1846    pub fn unpack_box(&self) -> Option<(&Ty, &Ty)> {
1847        if let BaseTy::Adt(adt_def, args) = self
1848            && adt_def.is_box()
1849        {
1850            Some(args.box_args())
1851        } else {
1852            None
1853        }
1854    }
1855
1856    pub fn invariants(
1857        &self,
1858        tcx: TyCtxt,
1859        overflow_mode: OverflowMode,
1860    ) -> impl Iterator<Item = Invariant> {
1861        let (invariants, args) = match self {
1862            BaseTy::Adt(adt_def, args) => (adt_def.invariants().skip_binder(), &args[..]),
1863            BaseTy::Uint(uint_ty) => (uint_invariants(*uint_ty, overflow_mode), &[][..]),
1864            BaseTy::Int(int_ty) => (int_invariants(*int_ty, overflow_mode), &[][..]),
1865            BaseTy::Slice(_) => (slice_invariants(overflow_mode), &[][..]),
1866            _ => (&[][..], &[][..]),
1867        };
1868        invariants
1869            .iter()
1870            .map(move |inv| EarlyBinder(inv).instantiate_ref(tcx, args, &[]))
1871    }
1872
1873    pub fn to_ty(&self) -> Ty {
1874        let sort = self.sort();
1875        if sort.is_unit() {
1876            Ty::indexed(self.clone(), Expr::unit())
1877        } else {
1878            Ty::exists(Binder::bind_with_sort(Ty::indexed(self.clone(), Expr::nu()), sort))
1879        }
1880    }
1881
1882    pub fn to_subset_ty_ctor(&self) -> SubsetTyCtor {
1883        let sort = self.sort();
1884        Binder::bind_with_sort(SubsetTy::trivial(self.clone(), Expr::nu()), sort)
1885    }
1886
1887    #[track_caller]
1888    pub fn expect_adt(&self) -> (&AdtDef, &[GenericArg]) {
1889        if let BaseTy::Adt(adt_def, args) = self {
1890            (adt_def, args)
1891        } else {
1892            tracked_span_bug!("expected adt `{self:?}`")
1893        }
1894    }
1895
1896    /// A type is an *atom* if it is "self-delimiting", i.e., it has a clear boundary
1897    /// when printed. This is used to avoid unnecessary parenthesis when pretty printing.
1898    pub fn is_atom(&self) -> bool {
1899        // (nilehmann) I'm not sure about this list, please adjust if you get any odd behavior
1900        matches!(
1901            self,
1902            BaseTy::Int(_)
1903                | BaseTy::Uint(_)
1904                | BaseTy::Slice(_)
1905                | BaseTy::Bool
1906                | BaseTy::Char
1907                | BaseTy::Str
1908                | BaseTy::Adt(..)
1909                | BaseTy::Tuple(..)
1910                | BaseTy::Param(_)
1911                | BaseTy::Array(..)
1912                | BaseTy::Never
1913                | BaseTy::Closure(..)
1914                | BaseTy::Coroutine(..)
1915                // opaque alias are atoms the way we print them now, but they won't
1916                // be if we print them as `impl Trait`
1917                | BaseTy::Alias(..)
1918        )
1919    }
1920
1921    /// Similar to [`rustc_infer::infer::canonical::ir::fast_reject::simplify_type`].
1922    ///
1923    /// This implementation is currently incomplete, so it should only be used in contexts
1924    /// where completeness is not required. Currently, it's used to find incoherent
1925    /// implementations when resolving associated constants. In this context, incompleteness
1926    /// is acceptable since the worst case outcome is simply failing to resolve a type-relative
1927    /// constant.
1928    fn simplify_type(&self) -> Option<SimplifiedType> {
1929        match self {
1930            BaseTy::Bool => Some(SimplifiedType::Bool),
1931            BaseTy::Char => Some(SimplifiedType::Char),
1932            BaseTy::Int(int_type) => Some(SimplifiedType::Int(*int_type)),
1933            BaseTy::Uint(uint_type) => Some(SimplifiedType::Uint(*uint_type)),
1934            BaseTy::Float(float_type) => Some(SimplifiedType::Float(*float_type)),
1935            BaseTy::Adt(def, _) => Some(SimplifiedType::Adt(def.did())),
1936            BaseTy::Str => Some(SimplifiedType::Str),
1937            BaseTy::Array(..) => Some(SimplifiedType::Array),
1938            BaseTy::Slice(..) => Some(SimplifiedType::Slice),
1939            BaseTy::RawPtr(_, mutbl) => Some(SimplifiedType::Ptr(*mutbl)),
1940            BaseTy::Ref(_, _, mutbl) => Some(SimplifiedType::Ref(*mutbl)),
1941            BaseTy::FnDef(def_id, _) | BaseTy::Closure(def_id, ..) => {
1942                Some(SimplifiedType::Closure(*def_id))
1943            }
1944            BaseTy::Coroutine(def_id, ..) => Some(SimplifiedType::Coroutine(*def_id)),
1945            BaseTy::Never => Some(SimplifiedType::Never),
1946            BaseTy::Tuple(tys) => Some(SimplifiedType::Tuple(tys.len())),
1947            BaseTy::FnPtr(poly_fn_sig) => {
1948                Some(SimplifiedType::Function(poly_fn_sig.skip_binder_ref().inputs().len()))
1949            }
1950            BaseTy::Foreign(def_id) => Some(SimplifiedType::Foreign(*def_id)),
1951            BaseTy::RawPtrMetadata(_)
1952            | BaseTy::Alias(..)
1953            | BaseTy::Param(_)
1954            | BaseTy::Dynamic(..)
1955            | BaseTy::Infer(_) => None,
1956        }
1957    }
1958}
1959
1960impl<'tcx> ToRustc<'tcx> for BaseTy {
1961    type T = rustc_middle::ty::Ty<'tcx>;
1962
1963    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
1964        use rustc_middle::ty;
1965        match self {
1966            BaseTy::Int(i) => ty::Ty::new_int(tcx, *i),
1967            BaseTy::Uint(i) => ty::Ty::new_uint(tcx, *i),
1968            BaseTy::Param(pty) => pty.to_ty(tcx),
1969            BaseTy::Slice(ty) => ty::Ty::new_slice(tcx, ty.to_rustc(tcx)),
1970            BaseTy::Bool => tcx.types.bool,
1971            BaseTy::Char => tcx.types.char,
1972            BaseTy::Str => tcx.types.str_,
1973            BaseTy::Adt(adt_def, args) => {
1974                let did = adt_def.did();
1975                let adt_def = tcx.adt_def(did);
1976                let args = args.to_rustc(tcx);
1977                ty::Ty::new_adt(tcx, adt_def, args)
1978            }
1979            BaseTy::FnDef(def_id, args) => {
1980                let args = args.to_rustc(tcx);
1981                ty::Ty::new_fn_def(tcx, *def_id, args)
1982            }
1983            BaseTy::Float(f) => ty::Ty::new_float(tcx, *f),
1984            BaseTy::RawPtr(ty, mutbl) => ty::Ty::new_ptr(tcx, ty.to_rustc(tcx), *mutbl),
1985            BaseTy::Ref(re, ty, mutbl) => {
1986                ty::Ty::new_ref(tcx, re.to_rustc(tcx), ty.to_rustc(tcx), *mutbl)
1987            }
1988            BaseTy::FnPtr(poly_sig) => ty::Ty::new_fn_ptr(tcx, poly_sig.to_rustc(tcx)),
1989            BaseTy::Tuple(tys) => {
1990                let ts = tys.iter().map(|ty| ty.to_rustc(tcx)).collect_vec();
1991                ty::Ty::new_tup(tcx, &ts)
1992            }
1993            BaseTy::Alias(kind, alias_ty) => {
1994                ty::Ty::new_alias(tcx, kind.to_rustc(tcx), alias_ty.to_rustc(tcx))
1995            }
1996            BaseTy::Array(ty, n) => {
1997                let ty = ty.to_rustc(tcx);
1998                let n = n.to_rustc(tcx);
1999                ty::Ty::new_array_with_const_len(tcx, ty, n)
2000            }
2001            BaseTy::Never => tcx.types.never,
2002            BaseTy::Closure(did, _, args) => ty::Ty::new_closure(tcx, *did, args.to_rustc(tcx)),
2003            BaseTy::Dynamic(exi_preds, re) => {
2004                let preds: Vec<_> = exi_preds
2005                    .iter()
2006                    .map(|pred| pred.to_rustc(tcx))
2007                    .collect_vec();
2008                let preds = tcx.mk_poly_existential_predicates(&preds);
2009                ty::Ty::new_dynamic(tcx, preds, re.to_rustc(tcx))
2010            }
2011            BaseTy::Coroutine(def_id, resume_ty, upvars) => {
2012                bug!("TODO: Generator {def_id:?} {resume_ty:?} {upvars:?}")
2013                // let args = args.iter().map(|arg| into_rustc_generic_arg(tcx, arg));
2014                // let args = tcx.mk_args_from_iter(args);
2015                // ty::Ty::new_generator(*tcx, *def_id, args, mov)
2016            }
2017            BaseTy::Infer(ty_vid) => ty::Ty::new_var(tcx, *ty_vid),
2018            BaseTy::Foreign(def_id) => ty::Ty::new_foreign(tcx, *def_id),
2019            BaseTy::RawPtrMetadata(ty) => {
2020                ty::Ty::new_ptr(
2021                    tcx,
2022                    ty.to_rustc(tcx),
2023                    RawPtrKind::FakeForPtrMetadata.to_mutbl_lossy(),
2024                )
2025            }
2026        }
2027    }
2028}
2029
2030#[derive(
2031    Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable,
2032)]
2033pub struct AliasTy {
2034    pub def_id: DefId,
2035    pub args: GenericArgs,
2036    /// Holds the refinement-arguments for opaque-types; empty for projections
2037    pub refine_args: RefineArgs,
2038}
2039
2040impl AliasTy {
2041    pub fn new(def_id: DefId, args: GenericArgs, refine_args: RefineArgs) -> Self {
2042        AliasTy { args, refine_args, def_id }
2043    }
2044}
2045
2046/// This methods work only with associated type projections (i.e., no opaque types)
2047impl AliasTy {
2048    pub fn self_ty(&self) -> SubsetTyCtor {
2049        self.args[0].expect_base().clone()
2050    }
2051
2052    pub fn with_self_ty(&self, self_ty: SubsetTyCtor) -> Self {
2053        Self {
2054            def_id: self.def_id,
2055            args: [GenericArg::Base(self_ty)]
2056                .into_iter()
2057                .chain(self.args.iter().skip(1).cloned())
2058                .collect(),
2059            refine_args: self.refine_args.clone(),
2060        }
2061    }
2062}
2063
2064impl<'tcx> ToRustc<'tcx> for AliasTy {
2065    type T = rustc_middle::ty::AliasTy<'tcx>;
2066
2067    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2068        rustc_middle::ty::AliasTy::new(tcx, self.def_id, self.args.to_rustc(tcx))
2069    }
2070}
2071
2072pub type RefineArgs = List<Expr>;
2073
2074#[extension(pub trait RefineArgsExt)]
2075impl RefineArgs {
2076    fn identity_for_item(genv: GlobalEnv, def_id: DefId) -> QueryResult<RefineArgs> {
2077        Self::for_item(genv, def_id, |param, index| {
2078            Ok(Expr::var(Var::EarlyParam(EarlyReftParam {
2079                index: index as u32,
2080                name: param.name(),
2081            })))
2082        })
2083    }
2084
2085    fn for_item<F>(genv: GlobalEnv, def_id: DefId, mut mk: F) -> QueryResult<RefineArgs>
2086    where
2087        F: FnMut(EarlyBinder<RefineParam>, usize) -> QueryResult<Expr>,
2088    {
2089        let reft_generics = genv.refinement_generics_of(def_id)?;
2090        let count = reft_generics.count();
2091        let mut args = Vec::with_capacity(count);
2092        reft_generics.fill_item(genv, &mut args, &mut mk)?;
2093        Ok(List::from_vec(args))
2094    }
2095}
2096
2097/// A type constructor meant to be used as generic a argument of [kind base]. This is just an alias
2098/// to [`Binder<SubsetTy>`], but we expect the binder to have a single bound variable of the sort of
2099/// the underlying [base type].
2100///
2101/// [kind base]: GenericParamDefKind::Base
2102/// [base type]: SubsetTy::bty
2103pub type SubsetTyCtor = Binder<SubsetTy>;
2104
2105impl SubsetTyCtor {
2106    pub fn as_bty_skipping_binder(&self) -> &BaseTy {
2107        &self.as_ref().skip_binder().bty
2108    }
2109
2110    pub fn to_ty(&self) -> Ty {
2111        let sort = self.sort();
2112        if sort.is_unit() {
2113            self.replace_bound_reft(&Expr::unit()).to_ty()
2114        } else if let Some(def_id) = sort.is_unit_adt() {
2115            self.replace_bound_reft(&Expr::unit_struct(def_id)).to_ty()
2116        } else {
2117            Ty::exists(self.as_ref().map(SubsetTy::to_ty))
2118        }
2119    }
2120
2121    pub fn to_ty_ctor(&self) -> TyCtor {
2122        self.as_ref().map(SubsetTy::to_ty)
2123    }
2124}
2125
2126/// A subset type is a simplified version of a type that has the form `{b[e] | p}` where `b` is a
2127/// [`BaseTy`], `e` a refinement index, and `p` a predicate.
2128///
2129/// These are mainly found under a [`Binder`] with a single variable of the base type's sort. This
2130/// can be interpreted as a type constructor or an existential type. For example, under a binder with a
2131/// variable `v` of sort `int`, we can interpret `{i32[v] | v > 0}` as:
2132/// - A lambda `λv:int. {i32[v] | v > 0}` that "constructs" types when applied to ints, or
2133/// - An existential type `∃v:int. {i32[v] | v > 0}`.
2134///
2135/// This second interpretation is the reason we call this a subset type, i.e., the type `∃v. {b[v] | p}`
2136/// corresponds to the subset of values of  type `b` whose index satisfies `p`. These are the types
2137/// written as `B{v: p}` in the surface syntax and correspond to the types supported in other
2138/// refinement type systems like Liquid Haskell (with the difference that we are explicit
2139/// about separating refinements from program values via an index).
2140///
2141/// The main purpose for subset types is to be used as generic arguments of [kind base] when
2142/// interpreted as type constructors. They have two key properties that makes them suitable
2143/// for this:
2144///
2145/// 1. **Syntactic Restriction**: Subset types are syntactically restricted, making it easier to
2146///    relate them structurally (e.g., for subtyping). For instance, given two types `S<λv. T1>` and
2147///    `S<λ. T2>`, if `T1` and `T2` are subset types, we know they match structurally (at least
2148///    shallowly). In particularly, the syntactic restriction rules out complex types like
2149///    `S<λv. (i32[v], i32[v])>` simplifying some operations.
2150///
2151/// 2. **Eager Canonicalization**: Subset types can be eagerly canonicalized via [*strengthening*]
2152///    during substitution. For example, suppose we have a function:
2153///    ```text
2154///    fn foo<T>(x: T[@a], y: { T[@b] | b == a }) { }
2155///    ```
2156///    If we instantiate `T` with `λv. { i32[v] | v > 0}`, after substitution and applying the
2157///    lambda (the indexing syntax `T[a]` corresponds to an application of the lambda), we get:
2158///    ```text
2159///    fn foo(x: {i32[@a] | a > 0}, y: { { i32[@b] | b > 0 } | b == a }) { }
2160///    ```
2161///    Via *strengthening* we can canonicalize this to
2162///    ```text
2163///    fn foo(x: {i32[@a] | a > 0}, y: { i32[@b] | b == a && b > 0 }) { }
2164///    ```
2165///    As a result, we can guarantee the syntactic restriction through substitution.
2166///
2167/// [kind base]: GenericParamDefKind::Base
2168/// [*strengthening*]: https://arxiv.org/pdf/2010.07763.pdf
2169#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)]
2170pub struct SubsetTy {
2171    /// The base type `b` in the subset type `{b[e] | p}`.
2172    ///
2173    /// **NOTE:** This is mostly going to be under a [`Binder`]. It is not yet clear to me whether
2174    /// this [`BaseTy`] should be able to mention variables in the binder. In general, in a type
2175    /// `∃v. {b[e] | p}`, it's fine to mention `v` inside `b`, but since [`SubsetTy`] is meant to
2176    /// facilitate syntactic manipulation we may want to restrict this.
2177    pub bty: BaseTy,
2178    /// The refinement index `e` in the subset type `{b[e] | p}`. This can be an arbitrary expression,
2179    /// which makes manipulation easier. However, since this is mostly found under a binder, we expect
2180    /// it to be [`Expr::nu()`].
2181    pub idx: Expr,
2182    /// The predicate `p` in the subset type `{b[e] | p}`.
2183    pub pred: Expr,
2184}
2185
2186impl SubsetTy {
2187    pub fn new(bty: BaseTy, idx: impl Into<Expr>, pred: impl Into<Expr>) -> Self {
2188        Self { bty, idx: idx.into(), pred: pred.into() }
2189    }
2190
2191    pub fn trivial(bty: BaseTy, idx: impl Into<Expr>) -> Self {
2192        Self::new(bty, idx, Expr::tt())
2193    }
2194
2195    pub fn strengthen(&self, pred: impl Into<Expr>) -> Self {
2196        let this = self.clone();
2197        let pred = Expr::and(this.pred, pred).simplify(&SnapshotMap::default());
2198        Self { bty: this.bty, idx: this.idx, pred }
2199    }
2200
2201    pub fn to_ty(&self) -> Ty {
2202        let bty = self.bty.clone();
2203        if self.pred.is_trivially_true() {
2204            Ty::indexed(bty, &self.idx)
2205        } else {
2206            Ty::constr(&self.pred, Ty::indexed(bty, &self.idx))
2207        }
2208    }
2209}
2210
2211impl<'tcx> ToRustc<'tcx> for SubsetTy {
2212    type T = rustc_middle::ty::Ty<'tcx>;
2213
2214    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::Ty<'tcx> {
2215        self.bty.to_rustc(tcx)
2216    }
2217}
2218
2219#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)]
2220pub enum GenericArg {
2221    Ty(Ty),
2222    Base(SubsetTyCtor),
2223    Lifetime(Region),
2224    Const(Const),
2225}
2226
2227impl GenericArg {
2228    #[track_caller]
2229    pub fn expect_type(&self) -> &Ty {
2230        if let GenericArg::Ty(ty) = self {
2231            ty
2232        } else {
2233            bug!("expected `rty::GenericArg::Ty`, found `{self:?}`")
2234        }
2235    }
2236
2237    #[track_caller]
2238    pub fn expect_base(&self) -> &SubsetTyCtor {
2239        if let GenericArg::Base(ctor) = self {
2240            ctor
2241        } else {
2242            bug!("expected `rty::GenericArg::Base`, found `{self:?}`")
2243        }
2244    }
2245
2246    pub fn from_param_def(param: &GenericParamDef) -> Self {
2247        match param.kind {
2248            GenericParamDefKind::Type { .. } => {
2249                let param_ty = ParamTy { index: param.index, name: param.name };
2250                GenericArg::Ty(Ty::param(param_ty))
2251            }
2252            GenericParamDefKind::Base { .. } => {
2253                // λv. T[v]
2254                let param_ty = ParamTy { index: param.index, name: param.name };
2255                GenericArg::Base(Binder::bind_with_sort(
2256                    SubsetTy::trivial(BaseTy::Param(param_ty), Expr::nu()),
2257                    Sort::Param(param_ty),
2258                ))
2259            }
2260            GenericParamDefKind::Lifetime => {
2261                let region = EarlyParamRegion { index: param.index, name: param.name };
2262                GenericArg::Lifetime(Region::ReEarlyParam(region))
2263            }
2264            GenericParamDefKind::Const { .. } => {
2265                let param_const = ParamConst { index: param.index, name: param.name };
2266                let kind = ConstKind::Param(param_const);
2267                GenericArg::Const(Const { kind })
2268            }
2269        }
2270    }
2271
2272    /// Creates a `GenericArgs` from the definition of generic parameters, by calling a closure to
2273    /// obtain arg. The closures get to observe the `GenericArgs` as they're being built, which can
2274    /// be used to correctly replace defaults of generic parameters.
2275    pub fn for_item<F>(genv: GlobalEnv, def_id: DefId, mut mk_kind: F) -> QueryResult<GenericArgs>
2276    where
2277        F: FnMut(&GenericParamDef, &[GenericArg]) -> GenericArg,
2278    {
2279        let defs = genv.generics_of(def_id)?;
2280        let count = defs.count();
2281        let mut args = Vec::with_capacity(count);
2282        Self::fill_item(genv, &mut args, &defs, &mut mk_kind)?;
2283        Ok(List::from_vec(args))
2284    }
2285
2286    pub fn identity_for_item(genv: GlobalEnv, def_id: DefId) -> QueryResult<GenericArgs> {
2287        Self::for_item(genv, def_id, |param, _| GenericArg::from_param_def(param))
2288    }
2289
2290    fn fill_item<F>(
2291        genv: GlobalEnv,
2292        args: &mut Vec<GenericArg>,
2293        generics: &Generics,
2294        mk_kind: &mut F,
2295    ) -> QueryResult<()>
2296    where
2297        F: FnMut(&GenericParamDef, &[GenericArg]) -> GenericArg,
2298    {
2299        if let Some(def_id) = generics.parent {
2300            let parent_generics = genv.generics_of(def_id)?;
2301            Self::fill_item(genv, args, &parent_generics, mk_kind)?;
2302        }
2303        for param in &generics.own_params {
2304            let kind = mk_kind(param, args);
2305            tracked_span_assert_eq!(param.index as usize, args.len());
2306            args.push(kind);
2307        }
2308        Ok(())
2309    }
2310}
2311
2312impl From<TyOrBase> for GenericArg {
2313    fn from(v: TyOrBase) -> Self {
2314        match v {
2315            TyOrBase::Ty(ty) => GenericArg::Ty(ty),
2316            TyOrBase::Base(ctor) => GenericArg::Base(ctor),
2317        }
2318    }
2319}
2320
2321impl<'tcx> ToRustc<'tcx> for GenericArg {
2322    type T = rustc_middle::ty::GenericArg<'tcx>;
2323
2324    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2325        use rustc_middle::ty;
2326        match self {
2327            GenericArg::Ty(ty) => ty::GenericArg::from(ty.to_rustc(tcx)),
2328            GenericArg::Base(ctor) => ty::GenericArg::from(ctor.skip_binder_ref().to_rustc(tcx)),
2329            GenericArg::Lifetime(re) => ty::GenericArg::from(re.to_rustc(tcx)),
2330            GenericArg::Const(c) => ty::GenericArg::from(c.to_rustc(tcx)),
2331        }
2332    }
2333}
2334
2335pub type GenericArgs = List<GenericArg>;
2336
2337#[extension(pub trait GenericArgsExt)]
2338impl GenericArgs {
2339    #[track_caller]
2340    fn box_args(&self) -> (&Ty, &Ty) {
2341        if let [GenericArg::Ty(deref), GenericArg::Ty(alloc)] = &self[..] {
2342            (deref, alloc)
2343        } else {
2344            bug!("invalid generic arguments for box");
2345        }
2346    }
2347
2348    // We can't implement [`ToRustc`] because of coherence so we add it here
2349    fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> rustc_middle::ty::GenericArgsRef<'tcx> {
2350        tcx.mk_args_from_iter(self.iter().map(|arg| arg.to_rustc(tcx)))
2351    }
2352
2353    fn rebase_onto(
2354        &self,
2355        tcx: &TyCtxt,
2356        source_ancestor: DefId,
2357        target_args: &GenericArgs,
2358    ) -> List<GenericArg> {
2359        let defs = tcx.generics_of(source_ancestor);
2360        target_args
2361            .iter()
2362            .chain(self.iter().skip(defs.count()))
2363            .cloned()
2364            .collect()
2365    }
2366}
2367
2368#[derive(Debug)]
2369pub enum TyOrBase {
2370    Ty(Ty),
2371    Base(SubsetTyCtor),
2372}
2373
2374impl TyOrBase {
2375    pub fn into_ty(self) -> Ty {
2376        match self {
2377            TyOrBase::Ty(ty) => ty,
2378            TyOrBase::Base(ctor) => ctor.to_ty(),
2379        }
2380    }
2381
2382    #[track_caller]
2383    pub fn expect_base(self) -> SubsetTyCtor {
2384        match self {
2385            TyOrBase::Base(ctor) => ctor,
2386            TyOrBase::Ty(_) => tracked_span_bug!("expected `TyOrBase::Base`"),
2387        }
2388    }
2389
2390    pub fn as_base(self) -> Option<SubsetTyCtor> {
2391        match self {
2392            TyOrBase::Base(ctor) => Some(ctor),
2393            TyOrBase::Ty(_) => None,
2394        }
2395    }
2396}
2397
2398#[derive(Debug, Clone, TyEncodable, TyDecodable, TypeVisitable, TypeFoldable)]
2399pub enum TyOrCtor {
2400    Ty(Ty),
2401    Ctor(TyCtor),
2402}
2403
2404impl TyOrCtor {
2405    #[track_caller]
2406    pub fn expect_ctor(self) -> TyCtor {
2407        match self {
2408            TyOrCtor::Ctor(ctor) => ctor,
2409            TyOrCtor::Ty(_) => tracked_span_bug!("expected `TyOrCtor::Ctor`"),
2410        }
2411    }
2412
2413    pub fn expect_subset_ty_ctor(self) -> SubsetTyCtor {
2414        self.expect_ctor().map(|ty| {
2415            if let canonicalize::CanonicalTy::Constr(constr_ty) = ty.shallow_canonicalize()
2416                && let TyKind::Indexed(bty, idx) = constr_ty.ty().kind()
2417                && idx.is_nu()
2418            {
2419                SubsetTy::new(bty.clone(), Expr::nu(), constr_ty.pred())
2420            } else {
2421                tracked_span_bug!()
2422            }
2423        })
2424    }
2425
2426    pub fn to_ty(&self) -> Ty {
2427        match self {
2428            TyOrCtor::Ctor(ctor) => ctor.to_ty(),
2429            TyOrCtor::Ty(ty) => ty.clone(),
2430        }
2431    }
2432}
2433
2434impl From<TyOrBase> for TyOrCtor {
2435    fn from(v: TyOrBase) -> Self {
2436        match v {
2437            TyOrBase::Ty(ty) => TyOrCtor::Ty(ty),
2438            TyOrBase::Base(ctor) => TyOrCtor::Ctor(ctor.to_ty_ctor()),
2439        }
2440    }
2441}
2442
2443impl CoroutineObligPredicate {
2444    pub fn to_poly_fn_sig(&self) -> PolyFnSig {
2445        let vars = vec![];
2446
2447        let resume_ty = &self.resume_ty;
2448        let env_ty = Ty::coroutine(self.def_id, resume_ty.clone(), self.upvar_tys.clone());
2449
2450        let inputs = List::from_arr([env_ty, resume_ty.clone()]);
2451        let output =
2452            Binder::bind_with_vars(FnOutput::new(self.output.clone(), vec![]), List::empty());
2453
2454        PolyFnSig::bind_with_vars(
2455            FnSig::new(Safety::Safe, rustc_abi::ExternAbi::RustCall, List::empty(), inputs, output),
2456            List::from(vars),
2457        )
2458    }
2459}
2460
2461impl RefinementGenerics {
2462    pub fn count(&self) -> usize {
2463        self.parent_count + self.own_params.len()
2464    }
2465
2466    pub fn own_count(&self) -> usize {
2467        self.own_params.len()
2468    }
2469
2470    // /// Iterate and collect all parameters in this item including parents
2471    // pub fn collect_all_params<T, S>(
2472    //     &self,
2473    //     genv: GlobalEnv,
2474    //     mut f: impl FnMut(RefineParam) -> T,
2475    // ) -> QueryResult<S>
2476    // where
2477    //     S: FromIterator<T>,
2478    // {
2479    //     (0..self.count())
2480    //         .map(|i| Ok(f(self.param_at(i, genv)?)))
2481    //         .try_collect()
2482    // }
2483}
2484
2485impl EarlyBinder<RefinementGenerics> {
2486    pub fn parent(&self) -> Option<DefId> {
2487        self.skip_binder_ref().parent
2488    }
2489
2490    pub fn parent_count(&self) -> usize {
2491        self.skip_binder_ref().parent_count
2492    }
2493
2494    pub fn count(&self) -> usize {
2495        self.skip_binder_ref().count()
2496    }
2497
2498    pub fn own_count(&self) -> usize {
2499        self.skip_binder_ref().own_count()
2500    }
2501
2502    pub fn own_param_at(&self, index: usize) -> EarlyBinder<RefineParam> {
2503        self.as_ref().map(|this| this.own_params[index].clone())
2504    }
2505
2506    pub fn param_at(
2507        &self,
2508        param_index: usize,
2509        genv: GlobalEnv,
2510    ) -> QueryResult<EarlyBinder<RefineParam>> {
2511        if let Some(index) = param_index.checked_sub(self.parent_count()) {
2512            Ok(self.own_param_at(index))
2513        } else {
2514            let parent = self.parent().expect("parent_count > 0 but no parent?");
2515            genv.refinement_generics_of(parent)?
2516                .param_at(param_index, genv)
2517        }
2518    }
2519
2520    pub fn iter_own_params(&self) -> impl Iterator<Item = EarlyBinder<RefineParam>> + use<'_> {
2521        self.skip_binder_ref()
2522            .own_params
2523            .iter()
2524            .cloned()
2525            .map(EarlyBinder)
2526    }
2527
2528    pub fn fill_item<F, R>(&self, genv: GlobalEnv, vec: &mut Vec<R>, mk: &mut F) -> QueryResult
2529    where
2530        F: FnMut(EarlyBinder<RefineParam>, usize) -> QueryResult<R>,
2531    {
2532        if let Some(def_id) = self.parent() {
2533            genv.refinement_generics_of(def_id)?
2534                .fill_item(genv, vec, mk)?;
2535        }
2536        for param in self.iter_own_params() {
2537            vec.push(mk(param, vec.len())?);
2538        }
2539        Ok(())
2540    }
2541}
2542
2543impl EarlyBinder<GenericPredicates> {
2544    pub fn predicates(&self) -> EarlyBinder<List<Clause>> {
2545        EarlyBinder(self.0.predicates.clone())
2546    }
2547}
2548
2549impl EarlyBinder<FuncSort> {
2550    /// See [`subst::GenericsSubstForSort`]
2551    pub fn instantiate_func_sort<E>(
2552        self,
2553        sort_for_param: impl FnMut(ParamTy) -> Result<Sort, E>,
2554    ) -> Result<FuncSort, E> {
2555        self.0.try_fold_with(&mut subst::GenericsSubstFolder::new(
2556            subst::GenericsSubstForSort { sort_for_param },
2557            &[],
2558        ))
2559    }
2560}
2561
2562impl VariantSig {
2563    pub fn new(
2564        adt_def: AdtDef,
2565        args: GenericArgs,
2566        fields: List<Ty>,
2567        idx: Expr,
2568        requires: List<Expr>,
2569    ) -> Self {
2570        VariantSig { adt_def, args, fields, idx, requires }
2571    }
2572
2573    pub fn fields(&self) -> &[Ty] {
2574        &self.fields
2575    }
2576
2577    pub fn ret(&self) -> Ty {
2578        let bty = BaseTy::Adt(self.adt_def.clone(), self.args.clone());
2579        let idx = self.idx.clone();
2580        Ty::indexed(bty, idx)
2581    }
2582}
2583
2584impl FnSig {
2585    pub fn new(
2586        safety: Safety,
2587        abi: rustc_abi::ExternAbi,
2588        requires: List<Expr>,
2589        inputs: List<Ty>,
2590        output: Binder<FnOutput>,
2591    ) -> Self {
2592        FnSig { safety, abi, requires, inputs, output }
2593    }
2594
2595    pub fn requires(&self) -> &[Expr] {
2596        &self.requires
2597    }
2598
2599    pub fn inputs(&self) -> &[Ty] {
2600        &self.inputs
2601    }
2602
2603    pub fn output(&self) -> Binder<FnOutput> {
2604        self.output.clone()
2605    }
2606}
2607
2608impl<'tcx> ToRustc<'tcx> for FnSig {
2609    type T = rustc_middle::ty::FnSig<'tcx>;
2610
2611    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2612        tcx.mk_fn_sig(
2613            self.inputs().iter().map(|ty| ty.to_rustc(tcx)),
2614            self.output().as_ref().skip_binder().to_rustc(tcx),
2615            false,
2616            self.safety,
2617            self.abi,
2618        )
2619    }
2620}
2621
2622impl FnOutput {
2623    pub fn new(ret: Ty, ensures: impl Into<List<Ensures>>) -> Self {
2624        Self { ret, ensures: ensures.into() }
2625    }
2626}
2627
2628impl<'tcx> ToRustc<'tcx> for FnOutput {
2629    type T = rustc_middle::ty::Ty<'tcx>;
2630
2631    fn to_rustc(&self, tcx: TyCtxt<'tcx>) -> Self::T {
2632        self.ret.to_rustc(tcx)
2633    }
2634}
2635
2636impl AdtDef {
2637    pub fn new(
2638        rustc: ty::AdtDef,
2639        sort_def: AdtSortDef,
2640        invariants: Vec<Invariant>,
2641        opaque: bool,
2642    ) -> Self {
2643        AdtDef(Interned::new(AdtDefData { invariants, sort_def, opaque, rustc }))
2644    }
2645
2646    pub fn did(&self) -> DefId {
2647        self.0.rustc.did()
2648    }
2649
2650    pub fn sort_def(&self) -> &AdtSortDef {
2651        &self.0.sort_def
2652    }
2653
2654    pub fn sort(&self, args: &[GenericArg]) -> Sort {
2655        self.sort_def().to_sort(args)
2656    }
2657
2658    pub fn is_box(&self) -> bool {
2659        self.0.rustc.is_box()
2660    }
2661
2662    pub fn is_enum(&self) -> bool {
2663        self.0.rustc.is_enum()
2664    }
2665
2666    pub fn is_struct(&self) -> bool {
2667        self.0.rustc.is_struct()
2668    }
2669
2670    pub fn is_union(&self) -> bool {
2671        self.0.rustc.is_union()
2672    }
2673
2674    pub fn variants(&self) -> &IndexSlice<VariantIdx, VariantDef> {
2675        self.0.rustc.variants()
2676    }
2677
2678    pub fn variant(&self, idx: VariantIdx) -> &VariantDef {
2679        self.0.rustc.variant(idx)
2680    }
2681
2682    pub fn invariants(&self) -> EarlyBinder<&[Invariant]> {
2683        EarlyBinder(&self.0.invariants)
2684    }
2685
2686    pub fn discriminants(&self) -> impl Iterator<Item = (VariantIdx, u128)> + '_ {
2687        self.0.rustc.discriminants()
2688    }
2689
2690    pub fn is_opaque(&self) -> bool {
2691        self.0.opaque
2692    }
2693}
2694
2695impl EarlyBinder<PolyVariant> {
2696    // The field_idx is `Some(i)` when we have the `i`-th field of a `union`, in which case,
2697    // the `inputs` are _just_ the `i`-th type (and not all the types...)
2698    pub fn to_poly_fn_sig(&self, field_idx: Option<crate::FieldIdx>) -> EarlyBinder<PolyFnSig> {
2699        self.as_ref().map(|poly_variant| {
2700            poly_variant.as_ref().map(|variant| {
2701                let ret = variant.ret().shift_in_escaping(1);
2702                let output = Binder::bind_with_vars(FnOutput::new(ret, vec![]), List::empty());
2703                let inputs = match field_idx {
2704                    None => variant.fields.clone(),
2705                    Some(i) => List::singleton(variant.fields[i.index()].clone()),
2706                };
2707                FnSig::new(
2708                    Safety::Safe,
2709                    rustc_abi::ExternAbi::Rust,
2710                    variant.requires.clone(),
2711                    inputs,
2712                    output,
2713                )
2714            })
2715        })
2716    }
2717}
2718
2719impl TyKind {
2720    fn intern(self) -> Ty {
2721        Ty(Interned::new(self))
2722    }
2723}
2724
2725/// returns the same invariants as for `usize` which is the length of a slice
2726fn slice_invariants(overflow_mode: OverflowMode) -> &'static [Invariant] {
2727    static DEFAULT: LazyLock<[Invariant; 1]> = LazyLock::new(|| {
2728        [Invariant { pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int) }]
2729    });
2730    static OVERFLOW: LazyLock<[Invariant; 2]> = LazyLock::new(|| {
2731        [
2732            Invariant {
2733                pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int),
2734            },
2735            Invariant {
2736                pred: Binder::bind_with_sort(
2737                    Expr::le(Expr::nu(), Expr::uint_max(UintTy::Usize)),
2738                    Sort::Int,
2739                ),
2740            },
2741        ]
2742    });
2743    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2744        &*OVERFLOW
2745    } else {
2746        &*DEFAULT
2747    }
2748}
2749
2750fn uint_invariants(uint_ty: UintTy, overflow_mode: OverflowMode) -> &'static [Invariant] {
2751    static DEFAULT: LazyLock<[Invariant; 1]> = LazyLock::new(|| {
2752        [Invariant { pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int) }]
2753    });
2754
2755    static OVERFLOW: LazyLock<UnordMap<UintTy, [Invariant; 2]>> = LazyLock::new(|| {
2756        UINT_TYS
2757            .into_iter()
2758            .map(|uint_ty| {
2759                let invariants = [
2760                    Invariant {
2761                        pred: Binder::bind_with_sort(Expr::ge(Expr::nu(), Expr::zero()), Sort::Int),
2762                    },
2763                    Invariant {
2764                        pred: Binder::bind_with_sort(
2765                            Expr::le(Expr::nu(), Expr::uint_max(uint_ty)),
2766                            Sort::Int,
2767                        ),
2768                    },
2769                ];
2770                (uint_ty, invariants)
2771            })
2772            .collect()
2773    });
2774    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2775        &OVERFLOW[&uint_ty]
2776    } else {
2777        &*DEFAULT
2778    }
2779}
2780
2781fn int_invariants(int_ty: IntTy, overflow_mode: OverflowMode) -> &'static [Invariant] {
2782    static DEFAULT: [Invariant; 0] = [];
2783
2784    static OVERFLOW: LazyLock<UnordMap<IntTy, [Invariant; 2]>> = LazyLock::new(|| {
2785        INT_TYS
2786            .into_iter()
2787            .map(|int_ty| {
2788                let invariants = [
2789                    Invariant {
2790                        pred: Binder::bind_with_sort(
2791                            Expr::ge(Expr::nu(), Expr::int_min(int_ty)),
2792                            Sort::Int,
2793                        ),
2794                    },
2795                    Invariant {
2796                        pred: Binder::bind_with_sort(
2797                            Expr::le(Expr::nu(), Expr::int_max(int_ty)),
2798                            Sort::Int,
2799                        ),
2800                    },
2801                ];
2802                (int_ty, invariants)
2803            })
2804            .collect()
2805    });
2806    if matches!(overflow_mode, OverflowMode::Strict | OverflowMode::Lazy) {
2807        &OVERFLOW[&int_ty]
2808    } else {
2809        &DEFAULT
2810    }
2811}
2812
2813impl_internable!(AdtDefData, AdtSortDefData, TyKind);
2814impl_slice_internable!(
2815    Ty,
2816    GenericArg,
2817    Ensures,
2818    InferMode,
2819    Sort,
2820    SortArg,
2821    GenericParamDef,
2822    TraitRef,
2823    Binder<ExistentialPredicate>,
2824    Clause,
2825    PolyVariant,
2826    Invariant,
2827    RefineParam,
2828    FluxDefId,
2829    SortParamKind,
2830    AssocReft
2831);
2832
2833#[macro_export]
2834macro_rules! _Int {
2835    ($int_ty:pat, $idxs:pat) => {
2836        TyKind::Indexed(BaseTy::Int($int_ty), $idxs)
2837    };
2838}
2839pub use crate::_Int as Int;
2840
2841#[macro_export]
2842macro_rules! _Uint {
2843    ($uint_ty:pat, $idxs:pat) => {
2844        TyKind::Indexed(BaseTy::Uint($uint_ty), $idxs)
2845    };
2846}
2847pub use crate::_Uint as Uint;
2848
2849#[macro_export]
2850macro_rules! _Bool {
2851    ($idxs:pat) => {
2852        TyKind::Indexed(BaseTy::Bool, $idxs)
2853    };
2854}
2855pub use crate::_Bool as Bool;
2856
2857#[macro_export]
2858macro_rules! _Char {
2859    ($idxs:pat) => {
2860        TyKind::Indexed(BaseTy::Char, $idxs)
2861    };
2862}
2863pub use crate::_Char as Char;
2864
2865#[macro_export]
2866macro_rules! _Ref {
2867    ($($pats:pat),+ $(,)?) => {
2868        $crate::rty::TyKind::Indexed($crate::rty::BaseTy::Ref($($pats),+), _)
2869    };
2870}
2871pub use crate::_Ref as Ref;
2872
2873pub struct WfckResults {
2874    pub owner: FluxOwnerId,
2875    param_sorts: UnordMap<fhir::ParamId, Sort>,
2876    bin_op_sorts: ItemLocalMap<Sort>,
2877    fn_app_sorts: ItemLocalMap<List<SortArg>>,
2878    coercions: ItemLocalMap<Vec<Coercion>>,
2879    field_projs: ItemLocalMap<FieldProj>,
2880    node_sorts: ItemLocalMap<Sort>,
2881    record_ctors: ItemLocalMap<DefId>,
2882}
2883
2884#[derive(Clone, Copy, Debug)]
2885pub enum Coercion {
2886    Inject(DefId),
2887    Project(DefId),
2888}
2889
2890pub type ItemLocalMap<T> = UnordMap<fhir::ItemLocalId, T>;
2891
2892#[derive(Debug)]
2893pub struct LocalTableInContext<'a, T> {
2894    owner: FluxOwnerId,
2895    data: &'a ItemLocalMap<T>,
2896}
2897
2898pub struct LocalTableInContextMut<'a, T> {
2899    owner: FluxOwnerId,
2900    data: &'a mut ItemLocalMap<T>,
2901}
2902
2903impl WfckResults {
2904    pub fn new(owner: impl Into<FluxOwnerId>) -> Self {
2905        Self {
2906            owner: owner.into(),
2907            param_sorts: UnordMap::default(),
2908            bin_op_sorts: ItemLocalMap::default(),
2909            coercions: ItemLocalMap::default(),
2910            field_projs: ItemLocalMap::default(),
2911            node_sorts: ItemLocalMap::default(),
2912            record_ctors: ItemLocalMap::default(),
2913            fn_app_sorts: ItemLocalMap::default(),
2914        }
2915    }
2916
2917    pub fn param_sorts_mut(&mut self) -> &mut UnordMap<fhir::ParamId, Sort> {
2918        &mut self.param_sorts
2919    }
2920
2921    pub fn param_sorts(&self) -> &UnordMap<fhir::ParamId, Sort> {
2922        &self.param_sorts
2923    }
2924
2925    pub fn bin_op_sorts_mut(&mut self) -> LocalTableInContextMut<'_, Sort> {
2926        LocalTableInContextMut { owner: self.owner, data: &mut self.bin_op_sorts }
2927    }
2928
2929    pub fn fn_app_sorts_mut(&mut self) -> LocalTableInContextMut<'_, List<SortArg>> {
2930        LocalTableInContextMut { owner: self.owner, data: &mut self.fn_app_sorts }
2931    }
2932
2933    pub fn fn_app_sorts(&self) -> LocalTableInContext<'_, List<SortArg>> {
2934        LocalTableInContext { owner: self.owner, data: &self.fn_app_sorts }
2935    }
2936
2937    pub fn bin_op_sorts(&self) -> LocalTableInContext<'_, Sort> {
2938        LocalTableInContext { owner: self.owner, data: &self.bin_op_sorts }
2939    }
2940
2941    pub fn coercions_mut(&mut self) -> LocalTableInContextMut<'_, Vec<Coercion>> {
2942        LocalTableInContextMut { owner: self.owner, data: &mut self.coercions }
2943    }
2944
2945    pub fn coercions(&self) -> LocalTableInContext<'_, Vec<Coercion>> {
2946        LocalTableInContext { owner: self.owner, data: &self.coercions }
2947    }
2948
2949    pub fn field_projs_mut(&mut self) -> LocalTableInContextMut<'_, FieldProj> {
2950        LocalTableInContextMut { owner: self.owner, data: &mut self.field_projs }
2951    }
2952
2953    pub fn field_projs(&self) -> LocalTableInContext<'_, FieldProj> {
2954        LocalTableInContext { owner: self.owner, data: &self.field_projs }
2955    }
2956
2957    pub fn node_sorts_mut(&mut self) -> LocalTableInContextMut<'_, Sort> {
2958        LocalTableInContextMut { owner: self.owner, data: &mut self.node_sorts }
2959    }
2960
2961    pub fn node_sorts(&self) -> LocalTableInContext<'_, Sort> {
2962        LocalTableInContext { owner: self.owner, data: &self.node_sorts }
2963    }
2964
2965    pub fn record_ctors_mut(&mut self) -> LocalTableInContextMut<'_, DefId> {
2966        LocalTableInContextMut { owner: self.owner, data: &mut self.record_ctors }
2967    }
2968
2969    pub fn record_ctors(&self) -> LocalTableInContext<'_, DefId> {
2970        LocalTableInContext { owner: self.owner, data: &self.record_ctors }
2971    }
2972}
2973
2974impl<T> LocalTableInContextMut<'_, T> {
2975    pub fn insert(&mut self, fhir_id: FhirId, value: T) {
2976        tracked_span_assert_eq!(self.owner, fhir_id.owner);
2977        self.data.insert(fhir_id.local_id, value);
2978    }
2979}
2980
2981impl<'a, T> LocalTableInContext<'a, T> {
2982    pub fn get(&self, fhir_id: FhirId) -> Option<&'a T> {
2983        tracked_span_assert_eq!(self.owner, fhir_id.owner);
2984        self.data.get(&fhir_id.local_id)
2985    }
2986}