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