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