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