1mod 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#[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 field_names: Vec<Symbol>,
79 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 def_id: DefId,
135 params: Vec<ParamTy>,
142 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 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 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 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 pub fn kind_skipping_binder(&self) -> ClauseKind {
347 self.kind.clone().skip_binder()
348 }
349
350 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 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(), 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 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 #[debug_format = "?{}s"]
823 #[encodable]
824 pub struct ParamSort {}
825}
826
827newtype_index! {
828 #[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 #[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#[derive(PartialEq, Eq, Clone, Copy, Hash, Encodable, Decodable)]
900pub enum SortInfer {
901 SortVar(SortVid),
903 NumVar(NumVid),
905}
906
907newtype_index! {
908 #[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,
956 BoolToInt,
958 IntoUnit,
960 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 pub fn is_pred(&self) -> bool {
1003 matches!(self, Sort::Func(fsort) if fsort.skip_binders().output().is_bool())
1004 }
1005
1006 #[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#[derive(Clone, Copy, PartialEq, Eq, Hash, TyEncodable, TyDecodable)]
1063pub enum BvSize {
1064 Fixed(u32),
1066 Param(ParamSort),
1068 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#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)]
1111pub enum SortParamKind {
1112 Sort,
1113 BvSize,
1114}
1115
1116#[derive(Clone, PartialEq, Eq, Hash, Debug, TyEncodable, TyDecodable)]
1126pub struct PolyFuncSort {
1127 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#[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 Uninterpreted,
1173 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#[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 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 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#[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 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 pub fn is_integral(&self) -> bool {
1543 self.as_bty_skipping_existentials()
1544 .map(BaseTy::is_integral)
1545 .unwrap_or_default()
1546 }
1547
1548 pub fn is_bool(&self) -> bool {
1550 self.as_bty_skipping_existentials()
1551 .map(BaseTy::is_bool)
1552 .unwrap_or_default()
1553 }
1554
1555 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 Discr(AdtDef, Place),
1676 Param(ParamTy),
1677 Downcast(AdtDef, GenericArgs, Ty, VariantIdx, List<Ty>),
1678 Blocked(Ty),
1679 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, List<Ty>, flux_rustc_bridge::ty::GenericArgs),
1711 Coroutine(DefId, Ty, 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 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 pub fn is_atom(&self) -> bool {
1899 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 | BaseTy::Alias(..)
1918 )
1919 }
1920
1921 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 }
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 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
2046impl 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
2097pub 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#[derive(PartialEq, Clone, Eq, Hash, TyEncodable, TyDecodable)]
2170pub struct SubsetTy {
2171 pub bty: BaseTy,
2178 pub idx: Expr,
2182 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 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 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 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 }
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 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 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
2725fn 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}