1pub mod visit;
17
18use std::{borrow::Cow, fmt};
19
20use flux_common::{bug, span_bug};
21use flux_config::PartialInferOpts;
22use flux_rustc_bridge::def_id_to_string;
23pub use flux_syntax::surface::{BinOp, UnOp};
24use flux_syntax::surface::{Ignored, ParamMode, Trusted};
25use itertools::Itertools;
26use rustc_abi;
27pub use rustc_abi::VariantIdx;
28use rustc_ast::TraitObjectSyntax;
29use rustc_data_structures::fx::{FxIndexMap, FxIndexSet};
30use rustc_hash::FxHashMap;
31pub use rustc_hir::PrimTy;
32use rustc_hir::{
33 FnHeader, OwnerId, ParamName, Safety,
34 def::{DefKind, Namespace},
35 def_id::{DefId, LocalDefId},
36};
37use rustc_index::newtype_index;
38use rustc_macros::{Decodable, Encodable};
39pub use rustc_middle::mir::Mutability;
40use rustc_middle::{middle::resolve_bound_vars::ResolvedArg, ty::TyCtxt};
41use rustc_span::{ErrorGuaranteed, Span, Symbol, symbol::Ident};
42
43use crate::def_id::{FluxDefId, FluxLocalDefId, MaybeExternId};
44
45pub enum Attr {
46 Trusted(Trusted),
47 TrustedImpl(Trusted),
48 Ignore(Ignored),
49 ProvenExternally,
50 ShouldFail,
51 InferOpts(PartialInferOpts),
52}
53
54#[derive(Clone, Copy, Default)]
55pub struct AttrMap<'fhir> {
56 pub attrs: &'fhir [Attr],
57 pub qualifiers: &'fhir [FluxLocalDefId],
58 pub reveals: &'fhir [FluxDefId],
59}
60
61impl AttrMap<'_> {
62 pub(crate) fn proven_externally(&self) -> bool {
63 self.attrs
64 .iter()
65 .any(|attr| matches!(attr, Attr::ProvenExternally))
66 }
67
68 pub(crate) fn ignored(&self) -> Option<Ignored> {
69 self.attrs
70 .iter()
71 .find_map(|attr| if let Attr::Ignore(ignored) = *attr { Some(ignored) } else { None })
72 }
73
74 pub(crate) fn trusted(&self) -> Option<Trusted> {
75 self.attrs
76 .iter()
77 .find_map(|attr| if let Attr::Trusted(trusted) = *attr { Some(trusted) } else { None })
78 }
79
80 pub(crate) fn trusted_impl(&self) -> Option<Trusted> {
81 self.attrs.iter().find_map(|attr| {
82 if let Attr::TrustedImpl(trusted) = *attr { Some(trusted) } else { None }
83 })
84 }
85
86 pub(crate) fn should_fail(&self) -> bool {
87 self.attrs
88 .iter()
89 .any(|attr| matches!(attr, Attr::ShouldFail))
90 }
91
92 pub(crate) fn infer_opts(&self) -> Option<PartialInferOpts> {
93 self.attrs
94 .iter()
95 .find_map(|attr| if let Attr::InferOpts(opts) = *attr { Some(opts) } else { None })
96 }
97}
98
99#[derive(Debug, Clone, Copy)]
100pub struct Generics<'fhir> {
101 pub params: &'fhir [GenericParam<'fhir>],
102 pub refinement_params: &'fhir [RefineParam<'fhir>],
103 pub predicates: Option<&'fhir [WhereBoundPredicate<'fhir>]>,
104}
105
106#[derive(Debug, Clone, Copy)]
107pub struct GenericParam<'fhir> {
108 pub def_id: MaybeExternId,
109 pub name: ParamName,
110 pub kind: GenericParamKind<'fhir>,
111}
112
113#[derive(Debug, Clone, Copy)]
114pub enum GenericParamKind<'fhir> {
115 Type { default: Option<Ty<'fhir>> },
116 Lifetime,
117 Const { ty: Ty<'fhir> },
118}
119
120#[derive(Debug)]
121pub struct Qualifier<'fhir> {
122 pub def_id: FluxLocalDefId,
123 pub args: &'fhir [RefineParam<'fhir>],
124 pub expr: Expr<'fhir>,
125 pub global: bool,
126}
127
128#[derive(Clone, Copy, Debug)]
129pub enum Node<'fhir> {
130 Item(&'fhir Item<'fhir>),
131 TraitItem(&'fhir TraitItem<'fhir>),
132 ImplItem(&'fhir ImplItem<'fhir>),
133 OpaqueTy(&'fhir OpaqueTy<'fhir>),
134 ForeignItem(&'fhir ForeignItem<'fhir>),
135 Ctor,
136 AnonConst,
137 Expr,
138}
139
140impl<'fhir> Node<'fhir> {
141 pub fn as_owner(self) -> Option<OwnerNode<'fhir>> {
142 match self {
143 Node::Item(item) => Some(OwnerNode::Item(item)),
144 Node::TraitItem(trait_item) => Some(OwnerNode::TraitItem(trait_item)),
145 Node::ImplItem(impl_item) => Some(OwnerNode::ImplItem(impl_item)),
146 Node::ForeignItem(foreign_item) => Some(OwnerNode::ForeignItem(foreign_item)),
147 Node::OpaqueTy(_) => None,
148 Node::AnonConst => None,
149 Node::Expr => None,
150 Node::Ctor => None,
151 }
152 }
153
154 pub fn expect_opaque_ty(&self) -> &'fhir OpaqueTy<'fhir> {
155 if let Node::OpaqueTy(opaque_ty) = &self { opaque_ty } else { bug!("expected opaque type") }
156 }
157}
158
159#[derive(Clone, Copy, Debug)]
160pub enum OwnerNode<'fhir> {
161 Item(&'fhir Item<'fhir>),
162 TraitItem(&'fhir TraitItem<'fhir>),
163 ImplItem(&'fhir ImplItem<'fhir>),
164 ForeignItem(&'fhir ForeignItem<'fhir>),
165}
166
167impl<'fhir> OwnerNode<'fhir> {
168 pub fn fn_sig(&self) -> Option<&'fhir FnSig<'fhir>> {
169 match self {
170 OwnerNode::Item(Item { kind: ItemKind::Fn(fn_sig, ..), .. })
171 | OwnerNode::TraitItem(TraitItem { kind: TraitItemKind::Fn(fn_sig), .. })
172 | OwnerNode::ImplItem(ImplItem { kind: ImplItemKind::Fn(fn_sig), .. })
173 | OwnerNode::ForeignItem(ForeignItem {
174 kind: ForeignItemKind::Fn(fn_sig, ..), ..
175 }) => Some(fn_sig),
176 _ => None,
177 }
178 }
179
180 pub fn generics(self) -> &'fhir Generics<'fhir> {
181 match self {
182 OwnerNode::Item(item) => &item.generics,
183 OwnerNode::TraitItem(trait_item) => &trait_item.generics,
184 OwnerNode::ImplItem(impl_item) => &impl_item.generics,
185 OwnerNode::ForeignItem(foreign_item) => {
186 match foreign_item.kind {
187 ForeignItemKind::Fn(_, generics) => generics,
188 }
189 }
190 }
191 }
192
193 pub fn owner_id(&self) -> MaybeExternId<OwnerId> {
194 match self {
195 OwnerNode::Item(item) => item.owner_id,
196 OwnerNode::TraitItem(trait_item) => trait_item.owner_id,
197 OwnerNode::ImplItem(impl_item) => impl_item.owner_id,
198 OwnerNode::ForeignItem(foreign_item) => foreign_item.owner_id,
199 }
200 }
201}
202
203#[derive(Debug)]
204pub struct Item<'fhir> {
205 pub owner_id: MaybeExternId<OwnerId>,
206 pub generics: Generics<'fhir>,
207 pub kind: ItemKind<'fhir>,
208}
209
210impl<'fhir> Item<'fhir> {
211 pub fn expect_enum(&self) -> &EnumDef<'fhir> {
212 if let ItemKind::Enum(enum_def) = &self.kind { enum_def } else { bug!("expected enum") }
213 }
214
215 pub fn expect_struct(&self) -> &StructDef<'fhir> {
216 if let ItemKind::Struct(struct_def) = &self.kind {
217 struct_def
218 } else {
219 bug!("expected struct")
220 }
221 }
222
223 pub fn expect_type_alias(&self) -> &TyAlias<'fhir> {
224 if let ItemKind::TyAlias(ty_alias) = &self.kind {
225 ty_alias
226 } else {
227 bug!("expected type alias")
228 }
229 }
230
231 pub fn expect_impl(&self) -> &Impl<'fhir> {
232 if let ItemKind::Impl(impl_) = &self.kind { impl_ } else { bug!("expected impl") }
233 }
234
235 pub fn expect_trait(&self) -> &Trait<'fhir> {
236 if let ItemKind::Trait(trait_) = &self.kind { trait_ } else { bug!("expected trait") }
237 }
238}
239
240#[derive(Debug)]
241pub enum ItemKind<'fhir> {
242 Enum(EnumDef<'fhir>),
243 Struct(StructDef<'fhir>),
244 TyAlias(&'fhir TyAlias<'fhir>),
245 Trait(Trait<'fhir>),
246 Impl(Impl<'fhir>),
247 Fn(FnSig<'fhir>),
248 Const(Option<Expr<'fhir>>),
249}
250
251#[derive(Debug)]
252pub struct TraitItem<'fhir> {
253 pub owner_id: MaybeExternId<OwnerId>,
254 pub generics: Generics<'fhir>,
255 pub kind: TraitItemKind<'fhir>,
256}
257
258#[derive(Debug)]
259pub enum TraitItemKind<'fhir> {
260 Fn(FnSig<'fhir>),
261 Const,
262 Type,
263}
264
265#[derive(Debug)]
266pub struct ImplItem<'fhir> {
267 pub owner_id: MaybeExternId<OwnerId>,
268 pub kind: ImplItemKind<'fhir>,
269 pub generics: Generics<'fhir>,
270}
271
272#[derive(Debug)]
273pub enum ImplItemKind<'fhir> {
274 Fn(FnSig<'fhir>),
275 Const,
276 Type,
277}
278
279#[derive(Copy, Clone, Debug)]
280pub enum FluxItem<'fhir> {
281 Qualifier(&'fhir Qualifier<'fhir>),
282 Func(&'fhir SpecFunc<'fhir>),
283 PrimOpProp(&'fhir PrimOpProp<'fhir>),
284 SortDecl(&'fhir SortDecl),
285}
286
287impl FluxItem<'_> {
288 pub fn def_id(self) -> FluxLocalDefId {
289 match self {
290 FluxItem::Qualifier(qualifier) => qualifier.def_id,
291 FluxItem::Func(func) => func.def_id,
292 FluxItem::PrimOpProp(prop) => prop.def_id,
293 FluxItem::SortDecl(sort_decl) => sort_decl.def_id,
294 }
295 }
296}
297
298#[derive(Debug)]
299pub struct ForeignItem<'fhir> {
300 pub ident: Ident,
301 pub kind: ForeignItemKind<'fhir>,
302 pub owner_id: MaybeExternId<OwnerId>,
303 pub span: Span,
304}
305
306#[derive(Debug)]
307pub enum ForeignItemKind<'fhir> {
308 Fn(FnSig<'fhir>, &'fhir Generics<'fhir>),
309}
310
311#[derive(Debug, Clone, Copy)]
312pub struct SortDecl {
313 pub def_id: FluxLocalDefId,
314 pub params: usize,
315 pub span: Span,
316}
317
318pub type SortDecls = FxHashMap<Symbol, SortDecl>;
319
320#[derive(Debug, Clone, Copy)]
321pub struct WhereBoundPredicate<'fhir> {
322 pub span: Span,
323 pub bounded_ty: Ty<'fhir>,
324 pub bounds: GenericBounds<'fhir>,
325}
326
327pub type GenericBounds<'fhir> = &'fhir [GenericBound<'fhir>];
328
329#[derive(Debug, Clone, Copy)]
330pub enum GenericBound<'fhir> {
331 Trait(PolyTraitRef<'fhir>),
332 Outlives(Lifetime),
333}
334
335#[derive(Debug, Clone, Copy)]
336pub struct PolyTraitRef<'fhir> {
337 pub bound_generic_params: &'fhir [GenericParam<'fhir>],
338 pub refine_params: &'fhir [RefineParam<'fhir>],
340 pub modifiers: TraitBoundModifier,
341 pub trait_ref: Path<'fhir>,
342 pub span: Span,
343}
344
345#[derive(Debug, Copy, Clone)]
346pub enum TraitBoundModifier {
347 None,
348 Maybe,
349}
350
351#[derive(Debug)]
352pub struct Trait<'fhir> {
353 pub assoc_refinements: &'fhir [TraitAssocReft<'fhir>],
354}
355
356impl<'fhir> Trait<'fhir> {
357 pub fn find_assoc_reft(&self, name: Symbol) -> Option<&'fhir TraitAssocReft<'fhir>> {
358 self.assoc_refinements
359 .iter()
360 .find(|assoc_reft| assoc_reft.name == name)
361 }
362}
363
364#[derive(Debug, Clone, Copy)]
365pub struct TraitAssocReft<'fhir> {
366 pub name: Symbol,
367 pub params: &'fhir [RefineParam<'fhir>],
368 pub output: Sort<'fhir>,
369 pub body: Option<Expr<'fhir>>,
370 pub span: Span,
371 pub final_: bool,
372}
373
374#[derive(Debug)]
375pub struct Impl<'fhir> {
376 pub assoc_refinements: &'fhir [ImplAssocReft<'fhir>],
377}
378
379impl<'fhir> Impl<'fhir> {
380 pub fn find_assoc_reft(&self, name: Symbol) -> Option<&'fhir ImplAssocReft<'fhir>> {
381 self.assoc_refinements
382 .iter()
383 .find(|assoc_reft| assoc_reft.name == name)
384 }
385}
386
387#[derive(Clone, Copy, Debug)]
388pub struct ImplAssocReft<'fhir> {
389 pub name: Symbol,
390 pub params: &'fhir [RefineParam<'fhir>],
391 pub output: Sort<'fhir>,
392 pub body: Expr<'fhir>,
393 pub span: Span,
394}
395
396#[derive(Debug)]
397pub struct OpaqueTy<'fhir> {
398 pub def_id: MaybeExternId,
399 pub bounds: GenericBounds<'fhir>,
400}
401
402pub type Arena = bumpalo::Bump;
403
404#[derive(Default)]
409pub struct FluxItems<'fhir> {
410 pub items: FxIndexMap<FluxLocalDefId, FluxItem<'fhir>>,
411}
412
413impl FluxItems<'_> {
414 pub fn new() -> Self {
415 Self { items: Default::default() }
416 }
417}
418
419#[derive(Debug)]
420pub struct TyAlias<'fhir> {
421 pub index: Option<RefineParam<'fhir>>,
422 pub ty: Ty<'fhir>,
423 pub span: Span,
424 pub lifted: bool,
426}
427
428#[derive(Debug, Clone, Copy)]
429pub struct StructDef<'fhir> {
430 pub refinement: &'fhir RefinementKind<'fhir>,
431 pub params: &'fhir [RefineParam<'fhir>],
432 pub kind: StructKind<'fhir>,
433 pub invariants: &'fhir [Expr<'fhir>],
434}
435
436#[derive(Debug, Clone, Copy)]
437pub enum StructKind<'fhir> {
438 Transparent { fields: &'fhir [FieldDef<'fhir>] },
439 Opaque,
440}
441
442#[derive(Debug, Clone, Copy)]
443pub struct FieldDef<'fhir> {
444 pub ty: Ty<'fhir>,
445 pub lifted: bool,
447}
448
449#[derive(Debug)]
450pub enum RefinementKind<'fhir> {
451 Refined(RefinedBy<'fhir>),
453 Reflected,
455}
456
457impl RefinementKind<'_> {
458 pub fn is_reflected(&self) -> bool {
459 matches!(self, RefinementKind::Reflected)
460 }
461}
462
463#[derive(Debug)]
464pub struct EnumDef<'fhir> {
465 pub refinement: &'fhir RefinementKind<'fhir>,
466 pub params: &'fhir [RefineParam<'fhir>],
467 pub variants: &'fhir [VariantDef<'fhir>],
468 pub invariants: &'fhir [Expr<'fhir>],
469}
470
471#[derive(Debug, Clone, Copy)]
472pub struct VariantDef<'fhir> {
473 pub def_id: LocalDefId,
474 pub params: &'fhir [RefineParam<'fhir>],
475 pub fields: &'fhir [FieldDef<'fhir>],
476 pub ret: VariantRet<'fhir>,
477 pub span: Span,
478 pub lifted: bool,
480}
481
482#[derive(Debug, Clone, Copy)]
483pub struct VariantRet<'fhir> {
484 pub enum_id: DefId,
485 pub idx: Expr<'fhir>,
486}
487
488#[derive(Clone, Copy)]
489pub struct FnDecl<'fhir> {
490 pub requires: &'fhir [Requires<'fhir>],
491 pub inputs: &'fhir [Ty<'fhir>],
492 pub output: FnOutput<'fhir>,
493 pub span: Span,
494 pub lifted: bool,
496}
497
498#[derive(Clone, Copy)]
500pub struct Requires<'fhir> {
501 pub params: &'fhir [RefineParam<'fhir>],
503 pub pred: Expr<'fhir>,
504}
505
506#[derive(Clone, Copy)]
507pub struct FnSig<'fhir> {
508 pub header: FnHeader,
509 pub decl: &'fhir FnDecl<'fhir>,
510}
511
512#[derive(Clone, Copy)]
513pub struct FnOutput<'fhir> {
514 pub params: &'fhir [RefineParam<'fhir>],
515 pub ret: Ty<'fhir>,
516 pub ensures: &'fhir [Ensures<'fhir>],
517}
518
519#[derive(Clone, Copy)]
520pub enum Ensures<'fhir> {
521 Type(PathExpr<'fhir>, &'fhir Ty<'fhir>),
523 Pred(Expr<'fhir>),
525}
526
527#[derive(Clone, Copy)]
528pub struct Ty<'fhir> {
529 pub kind: TyKind<'fhir>,
530 pub span: Span,
531}
532
533#[derive(Clone, Copy)]
534pub enum TyKind<'fhir> {
535 BaseTy(BaseTy<'fhir>),
544 Indexed(BaseTy<'fhir>, Expr<'fhir>),
545 Exists(&'fhir [RefineParam<'fhir>], &'fhir Ty<'fhir>),
546 Constr(Expr<'fhir>, &'fhir Ty<'fhir>),
549 StrgRef(Lifetime, &'fhir PathExpr<'fhir>, &'fhir Ty<'fhir>),
550 Ref(Lifetime, MutTy<'fhir>),
551 BareFn(&'fhir BareFnTy<'fhir>),
552 Tuple(&'fhir [Ty<'fhir>]),
553 Array(&'fhir Ty<'fhir>, ConstArg),
554 RawPtr(&'fhir Ty<'fhir>, Mutability),
555 OpaqueDef(&'fhir OpaqueTy<'fhir>),
556 TraitObject(&'fhir [PolyTraitRef<'fhir>], Lifetime, TraitObjectSyntax),
557 Never,
558 Infer,
559 Err(ErrorGuaranteed),
560}
561
562pub struct BareFnTy<'fhir> {
563 pub safety: Safety,
564 pub abi: rustc_abi::ExternAbi,
565 pub generic_params: &'fhir [GenericParam<'fhir>],
566 pub decl: &'fhir FnDecl<'fhir>,
567 pub param_idents: &'fhir [Option<Ident>],
568}
569
570#[derive(Clone, Copy)]
571pub struct MutTy<'fhir> {
572 pub ty: &'fhir Ty<'fhir>,
573 pub mutbl: Mutability,
574}
575
576#[derive(Copy, Clone, PartialEq, Eq)]
579pub enum Lifetime {
580 Hole(FhirId),
582 Resolved(ResolvedArg),
584}
585
586#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq, Encodable, Decodable)]
588pub enum FluxOwnerId {
589 Flux(FluxLocalDefId),
590 Rust(OwnerId),
591}
592
593impl FluxOwnerId {
594 pub fn def_id(self) -> Option<LocalDefId> {
595 match self {
596 FluxOwnerId::Flux(_) => None,
597 FluxOwnerId::Rust(owner_id) => Some(owner_id.def_id),
598 }
599 }
600}
601
602#[derive(Debug, Hash, PartialEq, Eq, Copy, Clone, Encodable, Decodable)]
610pub struct FhirId {
611 pub owner: FluxOwnerId,
612 pub local_id: ItemLocalId,
613}
614
615newtype_index! {
616 #[encodable]
618 pub struct ItemLocalId {}
619}
620
621#[derive(Clone, Copy)]
623pub struct BaseTy<'fhir> {
624 pub kind: BaseTyKind<'fhir>,
625 pub fhir_id: FhirId,
626 pub span: Span,
627}
628
629impl<'fhir> BaseTy<'fhir> {
630 pub fn from_qpath(qpath: QPath<'fhir>, fhir_id: FhirId) -> Self {
631 let span = qpath.span();
632 Self { kind: BaseTyKind::Path(qpath), fhir_id, span }
633 }
634
635 fn as_path(&self) -> Option<Path<'fhir>> {
636 match self.kind {
637 BaseTyKind::Path(QPath::Resolved(None, path)) => Some(path),
638 _ => None,
639 }
640 }
641}
642
643#[derive(Clone, Copy)]
644pub enum BaseTyKind<'fhir> {
645 Path(QPath<'fhir>),
646 Slice(&'fhir Ty<'fhir>),
647 Err(ErrorGuaranteed),
648}
649
650#[derive(Clone, Copy)]
651pub enum QPath<'fhir> {
652 Resolved(Option<&'fhir Ty<'fhir>>, Path<'fhir>),
653 TypeRelative(&'fhir Ty<'fhir>, &'fhir PathSegment<'fhir>),
654}
655
656#[derive(Clone, Copy)]
657pub struct Path<'fhir> {
658 pub res: Res,
659 pub fhir_id: FhirId,
660 pub segments: &'fhir [PathSegment<'fhir>],
661 pub refine: &'fhir [Expr<'fhir>],
662 pub span: Span,
663}
664
665impl<'fhir> Path<'fhir> {
666 pub fn last_segment(&self) -> &'fhir PathSegment<'fhir> {
667 self.segments.last().unwrap()
668 }
669}
670
671#[derive(Clone, Copy)]
672pub struct PathSegment<'fhir> {
673 pub ident: Ident,
674 pub res: Res,
675 pub args: &'fhir [GenericArg<'fhir>],
676 pub constraints: &'fhir [AssocItemConstraint<'fhir>],
677}
678
679#[derive(Clone, Copy)]
680pub struct AssocItemConstraint<'fhir> {
681 pub ident: Ident,
682 pub kind: AssocItemConstraintKind<'fhir>,
683}
684
685#[derive(Clone, Copy)]
686pub enum AssocItemConstraintKind<'fhir> {
687 Equality { term: Ty<'fhir> },
688}
689
690#[derive(Clone, Copy)]
691pub enum GenericArg<'fhir> {
692 Lifetime(Lifetime),
693 Type(&'fhir Ty<'fhir>),
694 Const(ConstArg),
695 Infer,
696}
697
698impl<'fhir> GenericArg<'fhir> {
699 pub fn expect_type(&self) -> &'fhir Ty<'fhir> {
700 if let GenericArg::Type(ty) = self { ty } else { bug!("expected `GenericArg::Type`") }
701 }
702}
703
704#[derive(PartialEq, Eq, Clone, Copy)]
705pub struct ConstArg {
706 pub kind: ConstArgKind,
707 pub span: Span,
708}
709
710#[derive(PartialEq, Eq, Clone, Copy)]
711pub enum ConstArgKind {
712 Lit(usize),
713 Param(DefId),
714 Infer,
715}
716
717#[derive(Eq, PartialEq, Debug, Copy, Clone)]
722pub enum Res<Id = !> {
723 Def(DefKind, DefId),
725 PrimTy(PrimTy),
727 SelfTyAlias {
729 alias_to: DefId,
730 is_trait_impl: bool,
731 },
732 SelfTyParam {
734 trait_: DefId,
735 },
736 Param(ParamKind, Id),
738 GlobalFunc(SpecFuncKind),
740 Err,
741}
742
743#[derive(Copy, Clone, Debug)]
745pub struct PartialRes<Id = !> {
746 base_res: Res<Id>,
747 unresolved_segments: usize,
748}
749
750impl<Id: Copy> PartialRes<Id> {
751 pub fn new(base_res: Res<Id>) -> Self {
752 Self { base_res, unresolved_segments: 0 }
753 }
754
755 pub fn with_unresolved_segments(base_res: Res<Id>, unresolved_segments: usize) -> Self {
756 Self { base_res, unresolved_segments }
757 }
758
759 #[inline]
760 pub fn base_res(&self) -> Res<Id> {
761 self.base_res
762 }
763
764 pub fn unresolved_segments(&self) -> usize {
765 self.unresolved_segments
766 }
767
768 #[inline]
769 pub fn full_res(&self) -> Option<Res<Id>> {
770 (self.unresolved_segments == 0).then_some(self.base_res)
771 }
772
773 #[inline]
774 pub fn expect_full_res(&self) -> Res<Id> {
775 self.full_res().unwrap_or_else(|| bug!("expected full res"))
776 }
777
778 pub fn is_box(&self, tcx: TyCtxt) -> bool {
779 self.full_res().is_some_and(|res| res.is_box(tcx))
780 }
781
782 pub fn map_param_id<R>(&self, f: impl FnOnce(Id) -> R) -> PartialRes<R> {
783 PartialRes {
784 base_res: self.base_res.map_param_id(f),
785 unresolved_segments: self.unresolved_segments,
786 }
787 }
788}
789
790#[derive(Debug, Clone, Copy)]
791pub struct RefineParam<'fhir> {
792 pub id: ParamId,
793 pub name: Symbol,
794 pub span: Span,
795 pub sort: Sort<'fhir>,
796 pub kind: ParamKind,
797 pub fhir_id: FhirId,
798}
799
800#[derive(PartialEq, Eq, Debug, Clone, Copy)]
802pub enum ParamKind {
803 Explicit(Option<ParamMode>),
805 At,
807 Pound,
809 Colon,
811 Loc,
813 Error,
824}
825
826impl ParamKind {
827 pub fn is_loc(&self) -> bool {
828 matches!(self, ParamKind::Loc)
829 }
830}
831
832#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
834pub enum InferMode {
835 EVar,
839 KVar,
843}
844
845impl InferMode {
846 pub fn from_param_kind(kind: ParamKind) -> InferMode {
847 if let ParamKind::Explicit(Some(ParamMode::Horn)) = kind {
848 InferMode::KVar
849 } else {
850 InferMode::EVar
851 }
852 }
853
854 pub fn prefix_str(self) -> &'static str {
855 match self {
856 InferMode::EVar => "?",
857 InferMode::KVar => "$",
858 }
859 }
860}
861
862#[derive(Clone, Copy)]
863pub enum PrimSort {
864 Int,
865 Bool,
866 Char,
867 Real,
868 Set,
869 Map,
870 Str,
871}
872
873impl PrimSort {
874 pub fn name_str(self) -> &'static str {
875 match self {
876 PrimSort::Int => "int",
877 PrimSort::Str => "str",
878 PrimSort::Bool => "bool",
879 PrimSort::Char => "char",
880 PrimSort::Real => "real",
881 PrimSort::Set => "Set",
882 PrimSort::Map => "Map",
883 }
884 }
885
886 pub fn generics(self) -> usize {
888 match self {
889 PrimSort::Int | PrimSort::Bool | PrimSort::Real | PrimSort::Char | PrimSort::Str => 0,
890 PrimSort::Set => 1,
891 PrimSort::Map => 2,
892 }
893 }
894}
895
896#[derive(Clone, Copy)]
897pub enum SortRes {
898 PrimSort(PrimSort),
900 User(FluxDefId),
902 SortParam(usize),
904 TyParam(DefId),
906 SelfParam {
908 trait_id: DefId,
910 },
911 SelfAlias {
913 alias_to: DefId,
915 },
916 SelfParamAssoc { trait_id: DefId, ident: Ident },
925 Adt(DefId),
927}
928
929#[derive(Clone, Copy)]
930pub enum Sort<'fhir> {
931 Path(SortPath<'fhir>),
932 Loc,
934 BitVec(u32),
936 Func(PolyFuncSort<'fhir>),
938 SortOf(BaseTy<'fhir>),
941 Infer,
943 Err(ErrorGuaranteed),
944}
945
946#[derive(Clone, Copy)]
948pub struct SortPath<'fhir> {
949 pub res: SortRes,
950 pub segments: &'fhir [Ident],
951 pub args: &'fhir [Sort<'fhir>],
952}
953
954#[derive(Clone, Copy)]
955pub struct FuncSort<'fhir> {
956 pub inputs_and_output: &'fhir [Sort<'fhir>],
958}
959
960#[derive(Clone, Copy)]
961pub struct PolyFuncSort<'fhir> {
962 pub params: usize,
963 pub fsort: FuncSort<'fhir>,
964}
965
966impl<'fhir> PolyFuncSort<'fhir> {
967 pub fn new(params: usize, inputs_and_output: &'fhir [Sort]) -> Self {
968 let fsort = FuncSort { inputs_and_output };
969 Self { params, fsort }
970 }
971}
972
973#[derive(Clone, Copy)]
975pub enum AliasReft<'fhir> {
976 Qualified { qself: &'fhir Ty<'fhir>, trait_: Path<'fhir>, name: Ident },
978 TypeRelative { qself: &'fhir Ty<'fhir>, name: Ident },
982}
983
984#[derive(Debug, Clone, Copy)]
985pub struct FieldExpr<'fhir> {
986 pub ident: Ident,
987 pub expr: Expr<'fhir>,
988 pub fhir_id: FhirId,
989 pub span: Span,
990}
991
992#[derive(Debug, Clone, Copy)]
993pub struct Spread<'fhir> {
994 pub expr: Expr<'fhir>,
995 pub span: Span,
996 pub fhir_id: FhirId,
997}
998
999#[derive(Clone, Copy)]
1000pub struct Expr<'fhir> {
1001 pub kind: ExprKind<'fhir>,
1002 pub fhir_id: FhirId,
1003 pub span: Span,
1004}
1005
1006#[derive(Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
1007pub enum QuantKind {
1008 Forall,
1009 Exists,
1010}
1011
1012#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, Encodable, Decodable)]
1013pub struct Range {
1014 pub start: usize,
1015 pub end: usize,
1016}
1017
1018#[derive(Clone, Copy)]
1019pub enum ExprKind<'fhir> {
1020 Var(QPathExpr<'fhir>),
1021 Dot(&'fhir Expr<'fhir>, Ident),
1022 Literal(Lit),
1023 BinaryOp(BinOp, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1024 UnaryOp(UnOp, &'fhir Expr<'fhir>),
1025 App(PathExpr<'fhir>, &'fhir [Expr<'fhir>]),
1026 PrimApp(BinOp, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1028 Alias(AliasReft<'fhir>, &'fhir [Expr<'fhir>]),
1029 IfThenElse(&'fhir Expr<'fhir>, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1030 Abs(&'fhir [RefineParam<'fhir>], &'fhir Expr<'fhir>),
1031 BoundedQuant(QuantKind, RefineParam<'fhir>, Range, &'fhir Expr<'fhir>),
1032 Record(&'fhir [Expr<'fhir>]),
1033 Constructor(Option<PathExpr<'fhir>>, &'fhir [FieldExpr<'fhir>], Option<&'fhir Spread<'fhir>>),
1034 Block(&'fhir [LetDecl<'fhir>], &'fhir Expr<'fhir>),
1035 Err(ErrorGuaranteed),
1036}
1037
1038#[derive(Clone, Copy)]
1039pub enum QPathExpr<'fhir> {
1040 Resolved(PathExpr<'fhir>, Option<ParamKind>),
1041 TypeRelative(&'fhir Ty<'fhir>, Ident),
1042}
1043
1044#[derive(Clone, Copy)]
1045pub struct LetDecl<'fhir> {
1046 pub param: RefineParam<'fhir>,
1047 pub init: Expr<'fhir>,
1048}
1049
1050impl Expr<'_> {
1051 pub fn is_colon_param(&self) -> Option<ParamId> {
1052 if let ExprKind::Var(QPathExpr::Resolved(path, Some(ParamKind::Colon))) = &self.kind
1053 && let Res::Param(kind, id) = path.res
1054 {
1055 debug_assert_eq!(kind, ParamKind::Colon);
1056 Some(id)
1057 } else {
1058 None
1059 }
1060 }
1061}
1062
1063#[derive(Clone, Copy)]
1064pub enum NumLitKind {
1065 Int,
1066 Real,
1067}
1068
1069#[derive(Clone, Copy)]
1070pub enum Lit {
1071 Int(u128, Option<NumLitKind>),
1072 Bool(bool),
1073 Str(Symbol),
1074 Char(char),
1075}
1076
1077#[derive(Clone, Copy)]
1078pub struct PathExpr<'fhir> {
1079 pub segments: &'fhir [Ident],
1080 pub res: Res<ParamId>,
1081 pub fhir_id: FhirId,
1082 pub span: Span,
1083}
1084
1085newtype_index! {
1086 #[debug_format = "a{}"]
1087 pub struct ParamId {}
1088}
1089
1090impl PolyTraitRef<'_> {
1091 pub fn trait_def_id(&self) -> DefId {
1092 let path = &self.trait_ref;
1093 if let Res::Def(DefKind::Trait, did) = path.res {
1094 did
1095 } else {
1096 span_bug!(path.span, "unexpected resolution {:?}", path.res);
1097 }
1098 }
1099}
1100
1101impl From<OwnerId> for FluxOwnerId {
1102 fn from(owner_id: OwnerId) -> Self {
1103 FluxOwnerId::Rust(owner_id)
1104 }
1105}
1106
1107impl<'fhir> Ty<'fhir> {
1108 pub fn as_path(&self) -> Option<Path<'fhir>> {
1109 match &self.kind {
1110 TyKind::BaseTy(bty) => bty.as_path(),
1111 _ => None,
1112 }
1113 }
1114}
1115
1116impl<Id> Res<Id> {
1117 pub fn descr(&self) -> &'static str {
1118 match self {
1119 Res::PrimTy(_) => "builtin type",
1120 Res::Def(kind, def_id) => kind.descr(*def_id),
1121 Res::SelfTyAlias { .. } | Res::SelfTyParam { .. } => "self type",
1122 Res::Param(..) => "refinement parameter",
1123 Res::GlobalFunc(..) => "refinement function",
1124 Res::Err => "unresolved item",
1125 }
1126 }
1127
1128 pub fn is_box(&self, tcx: TyCtxt) -> bool {
1129 if let Res::Def(DefKind::Struct, def_id) = self {
1130 tcx.adt_def(def_id).is_box()
1131 } else {
1132 false
1133 }
1134 }
1135
1136 pub fn ns(&self) -> Option<Namespace> {
1138 match self {
1139 Res::Def(kind, ..) => kind.ns(),
1140 Res::PrimTy(..) | Res::SelfTyAlias { .. } | Res::SelfTyParam { .. } => {
1141 Some(Namespace::TypeNS)
1142 }
1143 Res::Param(..) | Res::GlobalFunc(..) => Some(Namespace::ValueNS),
1144 Res::Err => None,
1145 }
1146 }
1147
1148 pub fn matches_ns(&self, ns: Namespace) -> bool {
1150 self.ns().is_none_or(|actual_ns| actual_ns == ns)
1151 }
1152
1153 pub fn map_param_id<R>(self, f: impl FnOnce(Id) -> R) -> Res<R> {
1154 match self {
1155 Res::Param(kind, param_id) => Res::Param(kind, f(param_id)),
1156 Res::Def(def_kind, def_id) => Res::Def(def_kind, def_id),
1157 Res::PrimTy(prim_ty) => Res::PrimTy(prim_ty),
1158 Res::SelfTyAlias { alias_to, is_trait_impl } => {
1159 Res::SelfTyAlias { alias_to, is_trait_impl }
1160 }
1161 Res::SelfTyParam { trait_ } => Res::SelfTyParam { trait_ },
1162 Res::GlobalFunc(spec_func_kind) => Res::GlobalFunc(spec_func_kind),
1163 Res::Err => Res::Err,
1164 }
1165 }
1166
1167 pub fn expect_param(self) -> (ParamKind, Id) {
1168 if let Res::Param(kind, id) = self { (kind, id) } else { bug!("expected param") }
1169 }
1170}
1171
1172impl<Id1, Id2> TryFrom<rustc_hir::def::Res<Id1>> for Res<Id2> {
1173 type Error = ();
1174
1175 fn try_from(res: rustc_hir::def::Res<Id1>) -> Result<Self, Self::Error> {
1176 match res {
1177 rustc_hir::def::Res::Def(kind, did) => Ok(Res::Def(kind, did)),
1178 rustc_hir::def::Res::PrimTy(prim_ty) => Ok(Res::PrimTy(prim_ty)),
1179 rustc_hir::def::Res::SelfTyAlias { alias_to, forbid_generic: false, is_trait_impl } => {
1180 Ok(Res::SelfTyAlias { alias_to, is_trait_impl })
1181 }
1182 rustc_hir::def::Res::SelfTyParam { trait_ } => Ok(Res::SelfTyParam { trait_ }),
1183 rustc_hir::def::Res::Err => Ok(Res::Err),
1184 _ => Err(()),
1185 }
1186 }
1187}
1188
1189impl QPath<'_> {
1190 pub fn span(&self) -> Span {
1191 match self {
1192 QPath::Resolved(_, path) => path.span,
1193 QPath::TypeRelative(qself, assoc) => qself.span.to(assoc.ident.span),
1194 }
1195 }
1196}
1197
1198impl Lit {
1199 pub const TRUE: Lit = Lit::Bool(true);
1200}
1201
1202#[derive(Clone, Debug)]
1204pub struct RefinedBy<'fhir> {
1205 pub sort_params: FxIndexSet<DefId>,
1220 pub fields: FxIndexMap<Symbol, Sort<'fhir>>,
1222}
1223
1224#[derive(Debug)]
1225pub struct SpecFunc<'fhir> {
1226 pub def_id: FluxLocalDefId,
1227 pub params: usize,
1228 pub args: &'fhir [RefineParam<'fhir>],
1229 pub sort: Sort<'fhir>,
1230 pub body: Option<Expr<'fhir>>,
1231 pub hide: bool,
1232 pub ident_span: Span,
1233}
1234#[derive(Debug)]
1235pub struct PrimOpProp<'fhir> {
1236 pub def_id: FluxLocalDefId,
1237 pub op: BinOp,
1238 pub args: &'fhir [RefineParam<'fhir>],
1239 pub body: Expr<'fhir>,
1240 pub span: Span,
1241}
1242
1243#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1244pub enum SpecFuncKind {
1245 Thy(liquid_fixpoint::ThyFunc),
1247 Uif(FluxDefId),
1249 Def(FluxDefId),
1251 Cast,
1253}
1254
1255impl SpecFuncKind {
1256 pub fn def_id(&self) -> Option<FluxDefId> {
1257 match self {
1258 SpecFuncKind::Uif(flux_id) | SpecFuncKind::Def(flux_id) => Some(*flux_id),
1259 _ => None,
1260 }
1261 }
1262}
1263
1264impl<'fhir> Generics<'fhir> {
1265 pub fn get_param(&self, def_id: LocalDefId) -> &'fhir GenericParam<'fhir> {
1266 self.params
1267 .iter()
1268 .find(|p| p.def_id.local_id() == def_id)
1269 .unwrap()
1270 }
1271}
1272
1273impl<'fhir> RefinedBy<'fhir> {
1274 pub fn new(fields: FxIndexMap<Symbol, Sort<'fhir>>, sort_params: FxIndexSet<DefId>) -> Self {
1275 RefinedBy { sort_params, fields }
1276 }
1277
1278 pub fn trivial() -> Self {
1279 RefinedBy { sort_params: Default::default(), fields: Default::default() }
1280 }
1281}
1282
1283impl<'fhir> From<PolyFuncSort<'fhir>> for Sort<'fhir> {
1284 fn from(fsort: PolyFuncSort<'fhir>) -> Self {
1285 Self::Func(fsort)
1286 }
1287}
1288
1289impl FuncSort<'_> {
1290 pub fn inputs(&self) -> &[Sort<'_>] {
1291 &self.inputs_and_output[..self.inputs_and_output.len() - 1]
1292 }
1293
1294 pub fn output(&self) -> &Sort<'_> {
1295 &self.inputs_and_output[self.inputs_and_output.len() - 1]
1296 }
1297}
1298
1299impl rustc_errors::IntoDiagArg for Ty<'_> {
1300 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1301 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1302 }
1303}
1304
1305impl rustc_errors::IntoDiagArg for Path<'_> {
1306 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1307 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1308 }
1309}
1310
1311impl StructDef<'_> {
1312 pub fn is_opaque(&self) -> bool {
1313 matches!(self.kind, StructKind::Opaque)
1314 }
1315}
1316
1317impl fmt::Debug for FnSig<'_> {
1318 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1319 write!(f, "{:?}", self.decl)
1320 }
1321}
1322
1323impl fmt::Debug for FnDecl<'_> {
1324 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1325 if !self.requires.is_empty() {
1326 write!(f, "[{:?}] ", self.requires.iter().format(", "))?;
1327 }
1328 write!(f, "fn({:?}) -> {:?}", self.inputs.iter().format(", "), self.output)
1329 }
1330}
1331
1332impl fmt::Debug for FnOutput<'_> {
1333 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1334 if !self.params.is_empty() {
1335 write!(
1336 f,
1337 "exists<{}> ",
1338 self.params.iter().format_with(", ", |param, f| {
1339 f(&format_args!("{}: {:?}", param.name, param.sort))
1340 })
1341 )?;
1342 }
1343 write!(f, "{:?}", self.ret)?;
1344 if !self.ensures.is_empty() {
1345 write!(f, "; [{:?}]", self.ensures.iter().format(", "))?;
1346 }
1347
1348 Ok(())
1349 }
1350}
1351
1352impl fmt::Debug for Requires<'_> {
1353 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1354 if !self.params.is_empty() {
1355 write!(
1356 f,
1357 "forall {}.",
1358 self.params.iter().format_with(",", |param, f| {
1359 f(&format_args!("{}:{:?}", param.name, param.sort))
1360 })
1361 )?;
1362 }
1363 write!(f, "{:?}", self.pred)
1364 }
1365}
1366
1367impl fmt::Debug for Ensures<'_> {
1368 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1369 match self {
1370 Ensures::Type(loc, ty) => write!(f, "{loc:?}: {ty:?}"),
1371 Ensures::Pred(e) => write!(f, "{e:?}"),
1372 }
1373 }
1374}
1375
1376impl fmt::Debug for Ty<'_> {
1377 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1378 match &self.kind {
1379 TyKind::BaseTy(bty) => write!(f, "{bty:?}"),
1380 TyKind::Indexed(bty, idx) => write!(f, "{bty:?}[{idx:?}]"),
1381 TyKind::Exists(params, ty) => {
1382 write!(f, "{{")?;
1383 write!(
1384 f,
1385 "{}",
1386 params.iter().format_with(",", |param, f| {
1387 f(&format_args!("{}:{:?}", param.name, param.sort))
1388 })
1389 )?;
1390 if let TyKind::Constr(pred, ty) = &ty.kind {
1391 write!(f, ". {ty:?} | {pred:?}}}")
1392 } else {
1393 write!(f, ". {ty:?}}}")
1394 }
1395 }
1396 TyKind::StrgRef(_lft, loc, ty) => write!(f, "&strg <{loc:?}: {ty:?}>"),
1397 TyKind::Ref(_lft, mut_ty) => {
1398 write!(f, "&{}{:?}", mut_ty.mutbl.prefix_str(), mut_ty.ty)
1399 }
1400 TyKind::BareFn(bare_fn_ty) => {
1401 write!(f, "{bare_fn_ty:?}")
1402 }
1403 TyKind::Tuple(tys) => write!(f, "({:?})", tys.iter().format(", ")),
1404 TyKind::Array(ty, len) => write!(f, "[{ty:?}; {len:?}]"),
1405 TyKind::Never => write!(f, "!"),
1406 TyKind::Constr(pred, ty) => write!(f, "{{{ty:?} | {pred:?}}}"),
1407 TyKind::RawPtr(ty, Mutability::Not) => write!(f, "*const {ty:?}"),
1408 TyKind::RawPtr(ty, Mutability::Mut) => write!(f, "*mut {ty:?}"),
1409 TyKind::Infer => write!(f, "_"),
1410 TyKind::OpaqueDef(opaque_ty) => {
1411 write!(f, "impl trait <def_id = {:?}>", opaque_ty.def_id.resolved_id(),)
1412 }
1413 TyKind::TraitObject(poly_traits, _lft, _syntax) => {
1414 write!(f, "dyn {poly_traits:?}")
1415 }
1416 TyKind::Err(_) => write!(f, "err"),
1417 }
1418 }
1419}
1420
1421impl fmt::Debug for BareFnTy<'_> {
1422 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1423 if !self.generic_params.is_empty() {
1424 write!(
1425 f,
1426 "for<{}>",
1427 self.generic_params
1428 .iter()
1429 .map(|param| param.name.ident())
1430 .format(",")
1431 )?;
1432 }
1433 write!(f, "{:?}", self.decl)
1434 }
1435}
1436
1437impl fmt::Debug for Lifetime {
1438 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1439 match self {
1440 Lifetime::Hole(_) => write!(f, "'_"),
1441 Lifetime::Resolved(lft) => write!(f, "{lft:?}"),
1442 }
1443 }
1444}
1445
1446impl fmt::Debug for ConstArg {
1447 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1448 write!(f, "{:?}", self.kind)
1449 }
1450}
1451
1452impl fmt::Debug for ConstArgKind {
1453 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1454 match self {
1455 ConstArgKind::Lit(n) => write!(f, "{n}"),
1456 ConstArgKind::Param(p) => write!(f, "{p:?}"),
1457 ConstArgKind::Infer => write!(f, "_"),
1458 }
1459 }
1460}
1461
1462impl fmt::Debug for BaseTy<'_> {
1463 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1464 match &self.kind {
1465 BaseTyKind::Path(qpath) => write!(f, "{qpath:?}"),
1466 BaseTyKind::Slice(ty) => write!(f, "[{ty:?}]"),
1467 BaseTyKind::Err(_) => write!(f, "err"),
1468 }
1469 }
1470}
1471
1472impl fmt::Debug for QPath<'_> {
1473 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1474 match self {
1475 QPath::Resolved(_, path) => write!(f, "{path:?}"),
1476 QPath::TypeRelative(qself, assoc) => write!(f, "<{qself:?}>::{assoc:?}"),
1477 }
1478 }
1479}
1480
1481impl fmt::Debug for Path<'_> {
1482 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1483 write!(f, "{:?}", self.segments.iter().format("::"))?;
1484 if !self.refine.is_empty() {
1485 write!(f, "({:?})", self.refine.iter().format(", "))?;
1486 }
1487 Ok(())
1488 }
1489}
1490
1491impl fmt::Debug for PathSegment<'_> {
1492 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1493 write!(f, "{}", self.ident)?;
1494 let args: Vec<_> = self
1495 .args
1496 .iter()
1497 .map(|a| a as &dyn std::fmt::Debug)
1498 .chain(self.constraints.iter().map(|b| b as &dyn std::fmt::Debug))
1499 .collect();
1500 if !args.is_empty() {
1501 write!(f, "<{:?}>", args.iter().format(", "))?;
1502 }
1503 Ok(())
1504 }
1505}
1506
1507impl fmt::Debug for GenericArg<'_> {
1508 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1509 match self {
1510 GenericArg::Type(ty) => write!(f, "{ty:?}"),
1511 GenericArg::Lifetime(lft) => write!(f, "{lft:?}"),
1512 GenericArg::Const(cst) => write!(f, "{cst:?}"),
1513 GenericArg::Infer => write!(f, "_"),
1514 }
1515 }
1516}
1517
1518impl fmt::Debug for AssocItemConstraint<'_> {
1519 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1520 match &self.kind {
1521 AssocItemConstraintKind::Equality { term } => {
1522 write!(f, "{:?} = {:?}", self.ident, term)
1523 }
1524 }
1525 }
1526}
1527
1528impl fmt::Debug for AliasReft<'_> {
1529 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1530 match self {
1531 AliasReft::Qualified { qself, trait_, name } => {
1532 write!(f, "<{qself:?} as {trait_:?}>::{name}")
1533 }
1534 AliasReft::TypeRelative { qself, name } => {
1535 write!(f, "{qself:?}::{name}")
1536 }
1537 }
1538 }
1539}
1540
1541impl fmt::Debug for QuantKind {
1542 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1543 match self {
1544 QuantKind::Forall => write!(f, "∀"),
1545 QuantKind::Exists => write!(f, "∃"),
1546 }
1547 }
1548}
1549
1550impl fmt::Debug for Expr<'_> {
1551 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1552 match self.kind {
1553 ExprKind::Var(QPathExpr::Resolved(path, ..)) => write!(f, "{path:?}"),
1554 ExprKind::Var(QPathExpr::TypeRelative(qself, assoc)) => {
1555 write!(f, "<{qself:?}>::{assoc}")
1556 }
1557 ExprKind::BinaryOp(op, e1, e2) => write!(f, "({e1:?} {op:?} {e2:?})"),
1558 ExprKind::PrimApp(op, e1, e2) => write!(f, "[{op:?}]({e1:?}, {e2:?})"),
1559 ExprKind::UnaryOp(op, e) => write!(f, "{op:?}{e:?}"),
1560 ExprKind::Literal(lit) => write!(f, "{lit:?}"),
1561 ExprKind::App(uf, es) => write!(f, "{uf:?}({:?})", es.iter().format(", ")),
1562 ExprKind::Alias(alias, refine_args) => {
1563 write!(f, "{alias:?}({:?})", refine_args.iter().format(", "))
1564 }
1565 ExprKind::IfThenElse(p, e1, e2) => {
1566 write!(f, "(if {p:?} {{ {e1:?} }} else {{ {e2:?} }})")
1567 }
1568 ExprKind::Dot(var, fld) => write!(f, "{var:?}.{fld}"),
1569 ExprKind::Abs(params, body) => {
1570 write!(
1571 f,
1572 "|{}| {body:?}",
1573 params.iter().format_with(", ", |param, f| {
1574 f(&format_args!("{}: {:?}", param.name, param.sort))
1575 })
1576 )
1577 }
1578 ExprKind::Record(flds) => {
1579 write!(f, "{{ {:?} }}", flds.iter().format(", "))
1580 }
1581 ExprKind::Constructor(path, exprs, spread) => {
1582 if let Some(path) = path
1583 && let Some(s) = spread
1584 {
1585 write!(f, "{:?} {{ {:?}, ..{:?} }}", path, exprs.iter().format(", "), s)
1586 } else if let Some(path) = path {
1587 write!(f, "{:?} {{ {:?} }}", path, exprs.iter().format(", "))
1588 } else if let Some(s) = spread {
1589 write!(f, "{{ {:?} ..{:?} }}", exprs.iter().format(", "), s)
1590 } else {
1591 write!(f, "{{ {:?} }}", exprs.iter().format(", "))
1592 }
1593 }
1594 ExprKind::BoundedQuant(kind, refine_param, rng, expr) => {
1595 write!(f, "{kind:?} {refine_param:?} in {}.. {} {{ {expr:?} }}", rng.start, rng.end)
1596 }
1597 ExprKind::Err(_) => write!(f, "err"),
1598 ExprKind::Block(decls, body) => {
1599 for decl in decls {
1600 write!(f, "let {:?} = {:?};", decl.param, decl.init)?;
1601 }
1602 write!(f, "{body:?}")
1603 }
1604 }
1605 }
1606}
1607
1608impl fmt::Debug for PathExpr<'_> {
1609 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1610 write!(f, "{}", self.segments.iter().format("::"))
1611 }
1612}
1613
1614impl fmt::Debug for Lit {
1615 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1616 match self {
1617 Lit::Int(i, Some(NumLitKind::Real)) => write!(f, "{i}real"),
1618 Lit::Int(i, _) => write!(f, "{i}"),
1619 Lit::Bool(b) => write!(f, "{b}"),
1620 Lit::Str(s) => write!(f, "\"{s:?}\""),
1621 Lit::Char(c) => write!(f, "\'{c}\'"),
1622 }
1623 }
1624}
1625
1626impl fmt::Debug for Sort<'_> {
1627 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1628 match self {
1629 Sort::Path(path) => write!(f, "{path:?}"),
1630 Sort::BitVec(w) => write!(f, "bitvec({w})"),
1631 Sort::Loc => write!(f, "loc"),
1632 Sort::Func(fsort) => write!(f, "{fsort:?}"),
1633 Sort::SortOf(bty) => write!(f, "<{bty:?}>::sort"),
1634 Sort::Infer => write!(f, "_"),
1635 Sort::Err(_) => write!(f, "err"),
1636 }
1637 }
1638}
1639
1640impl fmt::Debug for SortPath<'_> {
1641 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1642 write!(f, "{:?}", self.res)?;
1643 if !self.args.is_empty() {
1644 write!(f, "<{:?}>", self.args.iter().format(", "))?;
1645 }
1646 Ok(())
1647 }
1648}
1649
1650impl fmt::Debug for SortRes {
1651 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1652 match self {
1653 SortRes::PrimSort(PrimSort::Bool) => write!(f, "bool"),
1654 SortRes::PrimSort(PrimSort::Int) => write!(f, "int"),
1655 SortRes::PrimSort(PrimSort::Real) => write!(f, "real"),
1656 SortRes::PrimSort(PrimSort::Char) => write!(f, "char"),
1657 SortRes::PrimSort(PrimSort::Str) => write!(f, "str"),
1658 SortRes::PrimSort(PrimSort::Set) => write!(f, "Set"),
1659 SortRes::PrimSort(PrimSort::Map) => write!(f, "Map"),
1660 SortRes::SortParam(n) => write!(f, "@{n}"),
1661 SortRes::TyParam(def_id) => write!(f, "{}::sort", def_id_to_string(*def_id)),
1662 SortRes::SelfParam { trait_id } => {
1663 write!(f, "{}::Self::sort", def_id_to_string(*trait_id))
1664 }
1665 SortRes::SelfAlias { alias_to } => {
1666 write!(f, "{}::Self::sort", def_id_to_string(*alias_to))
1667 }
1668 SortRes::SelfParamAssoc { ident: assoc, .. } => {
1669 write!(f, "Self::{assoc}")
1670 }
1671 SortRes::User(def_id) => write!(f, "{:?}", def_id.name()),
1672 SortRes::Adt(def_id) => write!(f, "{}::sort", def_id_to_string(*def_id)),
1673 }
1674 }
1675}
1676
1677impl fmt::Debug for PolyFuncSort<'_> {
1678 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1679 if self.params > 0 {
1680 write!(f, "for<{}>{:?}", self.params, self.fsort)
1681 } else {
1682 write!(f, "{:?}", self.fsort)
1683 }
1684 }
1685}
1686
1687impl fmt::Debug for FuncSort<'_> {
1688 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1689 match self.inputs() {
1690 [input] => {
1691 write!(f, "{:?} -> {:?}", input, self.output())
1692 }
1693 inputs => {
1694 write!(f, "({:?}) -> {:?}", inputs.iter().format(", "), self.output())
1695 }
1696 }
1697 }
1698}