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 PrimOpProp(&'fhir PrimOpProp<'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::PrimOpProp(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 NumLitKind {
1020 Int,
1021 Real,
1022}
1023
1024#[derive(Clone, Copy)]
1025pub enum Lit {
1026 Int(u128, Option<NumLitKind>),
1027 Bool(bool),
1028 Str(Symbol),
1029 Char(char),
1030}
1031
1032#[derive(Clone, Copy, Debug)]
1033pub enum ExprRes<Id = ParamId> {
1034 Param(ParamKind, Id),
1035 Const(DefId),
1036 Ctor(DefId),
1040 Variant(DefId),
1041 ConstGeneric(DefId),
1042 NumConst(i128),
1043 GlobalFunc(SpecFuncKind),
1044}
1045
1046impl<Id> ExprRes<Id> {
1047 pub fn map_param_id<R>(self, f: impl FnOnce(Id) -> R) -> ExprRes<R> {
1048 match self {
1049 ExprRes::Param(kind, param_id) => ExprRes::Param(kind, f(param_id)),
1050 ExprRes::Const(def_id) => ExprRes::Const(def_id),
1051 ExprRes::NumConst(val) => ExprRes::NumConst(val),
1052 ExprRes::GlobalFunc(kind) => ExprRes::GlobalFunc(kind),
1053 ExprRes::ConstGeneric(def_id) => ExprRes::ConstGeneric(def_id),
1054 ExprRes::Ctor(def_id) => ExprRes::Ctor(def_id),
1055 ExprRes::Variant(def_id) => ExprRes::Variant(def_id),
1056 }
1057 }
1058
1059 pub fn expect_param(self) -> (ParamKind, Id) {
1060 if let ExprRes::Param(kind, id) = self { (kind, id) } else { bug!("expected param") }
1061 }
1062}
1063
1064#[derive(Clone, Copy)]
1065pub struct PathExpr<'fhir> {
1066 pub segments: &'fhir [Ident],
1067 pub res: ExprRes,
1068 pub fhir_id: FhirId,
1069 pub span: Span,
1070}
1071
1072newtype_index! {
1073 #[debug_format = "a{}"]
1074 pub struct ParamId {}
1075}
1076
1077impl PolyTraitRef<'_> {
1078 pub fn trait_def_id(&self) -> DefId {
1079 let path = &self.trait_ref;
1080 if let Res::Def(DefKind::Trait, did) = path.res {
1081 did
1082 } else {
1083 span_bug!(path.span, "unexpected resolution {:?}", path.res);
1084 }
1085 }
1086}
1087
1088impl From<OwnerId> for FluxOwnerId {
1089 fn from(owner_id: OwnerId) -> Self {
1090 FluxOwnerId::Rust(owner_id)
1091 }
1092}
1093
1094impl<'fhir> Ty<'fhir> {
1095 pub fn as_path(&self) -> Option<Path<'fhir>> {
1096 match &self.kind {
1097 TyKind::BaseTy(bty) => bty.as_path(),
1098 _ => None,
1099 }
1100 }
1101}
1102
1103impl Res {
1104 pub fn descr(&self) -> &'static str {
1105 match self {
1106 Res::PrimTy(_) => "builtin type",
1107 Res::Def(kind, def_id) => kind.descr(*def_id),
1108 Res::SelfTyAlias { .. } | Res::SelfTyParam { .. } => "self type",
1109 Res::Err => "unresolved item",
1110 }
1111 }
1112
1113 pub fn is_box(&self, tcx: TyCtxt) -> bool {
1114 if let Res::Def(DefKind::Struct, def_id) = self {
1115 tcx.adt_def(def_id).is_box()
1116 } else {
1117 false
1118 }
1119 }
1120}
1121
1122impl<Id> TryFrom<rustc_hir::def::Res<Id>> for Res {
1123 type Error = ();
1124
1125 fn try_from(res: rustc_hir::def::Res<Id>) -> Result<Self, Self::Error> {
1126 match res {
1127 rustc_hir::def::Res::Def(kind, did) => Ok(Res::Def(kind, did)),
1128 rustc_hir::def::Res::PrimTy(prim_ty) => Ok(Res::PrimTy(prim_ty)),
1129 rustc_hir::def::Res::SelfTyAlias { alias_to, forbid_generic: false, is_trait_impl } => {
1130 Ok(Res::SelfTyAlias { alias_to, is_trait_impl })
1131 }
1132 rustc_hir::def::Res::SelfTyParam { trait_ } => Ok(Res::SelfTyParam { trait_ }),
1133 rustc_hir::def::Res::Err => Ok(Res::Err),
1134 _ => Err(()),
1135 }
1136 }
1137}
1138
1139impl QPath<'_> {
1140 pub fn span(&self) -> Span {
1141 match self {
1142 QPath::Resolved(_, path) => path.span,
1143 QPath::TypeRelative(qself, assoc) => qself.span.to(assoc.ident.span),
1144 }
1145 }
1146}
1147
1148impl Lit {
1149 pub const TRUE: Lit = Lit::Bool(true);
1150}
1151
1152#[derive(Clone, Debug)]
1154pub struct RefinedBy<'fhir> {
1155 pub sort_params: FxIndexSet<DefId>,
1170 pub fields: FxIndexMap<Symbol, Sort<'fhir>>,
1172}
1173
1174#[derive(Debug)]
1175pub struct SpecFunc<'fhir> {
1176 pub def_id: FluxLocalDefId,
1177 pub params: usize,
1178 pub args: &'fhir [RefineParam<'fhir>],
1179 pub sort: Sort<'fhir>,
1180 pub body: Option<Expr<'fhir>>,
1181 pub hide: bool,
1182}
1183#[derive(Debug)]
1184pub struct PrimOpProp<'fhir> {
1185 pub def_id: FluxLocalDefId,
1186 pub op: BinOp,
1187 pub args: &'fhir [RefineParam<'fhir>],
1188 pub body: Expr<'fhir>,
1189 pub span: Span,
1190}
1191
1192#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1193pub enum SpecFuncKind {
1194 Thy(liquid_fixpoint::ThyFunc),
1196 Uif(FluxDefId),
1198 Def(FluxDefId),
1200 Cast,
1202}
1203
1204impl SpecFuncKind {
1205 pub fn def_id(&self) -> Option<FluxDefId> {
1206 match self {
1207 SpecFuncKind::Uif(flux_id) | SpecFuncKind::Def(flux_id) => Some(*flux_id),
1208 _ => None,
1209 }
1210 }
1211}
1212
1213impl<'fhir> Generics<'fhir> {
1214 pub fn get_param(&self, def_id: LocalDefId) -> &'fhir GenericParam<'fhir> {
1215 self.params
1216 .iter()
1217 .find(|p| p.def_id.local_id() == def_id)
1218 .unwrap()
1219 }
1220}
1221
1222impl<'fhir> RefinedBy<'fhir> {
1223 pub fn new(fields: FxIndexMap<Symbol, Sort<'fhir>>, sort_params: FxIndexSet<DefId>) -> Self {
1224 RefinedBy { sort_params, fields }
1225 }
1226
1227 pub fn trivial() -> Self {
1228 RefinedBy { sort_params: Default::default(), fields: Default::default() }
1229 }
1230}
1231
1232impl<'fhir> From<PolyFuncSort<'fhir>> for Sort<'fhir> {
1233 fn from(fsort: PolyFuncSort<'fhir>) -> Self {
1234 Self::Func(fsort)
1235 }
1236}
1237
1238impl FuncSort<'_> {
1239 pub fn inputs(&self) -> &[Sort<'_>] {
1240 &self.inputs_and_output[..self.inputs_and_output.len() - 1]
1241 }
1242
1243 pub fn output(&self) -> &Sort<'_> {
1244 &self.inputs_and_output[self.inputs_and_output.len() - 1]
1245 }
1246}
1247
1248impl rustc_errors::IntoDiagArg for Ty<'_> {
1249 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1250 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1251 }
1252}
1253
1254impl rustc_errors::IntoDiagArg for Path<'_> {
1255 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1256 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1257 }
1258}
1259
1260impl StructDef<'_> {
1261 pub fn is_opaque(&self) -> bool {
1262 matches!(self.kind, StructKind::Opaque)
1263 }
1264}
1265
1266impl fmt::Debug for FnSig<'_> {
1267 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1268 write!(f, "{:?}", self.decl)
1269 }
1270}
1271
1272impl fmt::Debug for FnDecl<'_> {
1273 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1274 if !self.requires.is_empty() {
1275 write!(f, "[{:?}] ", self.requires.iter().format(", "))?;
1276 }
1277 write!(f, "fn({:?}) -> {:?}", self.inputs.iter().format(", "), self.output)
1278 }
1279}
1280
1281impl fmt::Debug for FnOutput<'_> {
1282 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1283 if !self.params.is_empty() {
1284 write!(
1285 f,
1286 "exists<{}> ",
1287 self.params.iter().format_with(", ", |param, f| {
1288 f(&format_args!("{}: {:?}", param.name, param.sort))
1289 })
1290 )?;
1291 }
1292 write!(f, "{:?}", self.ret)?;
1293 if !self.ensures.is_empty() {
1294 write!(f, "; [{:?}]", self.ensures.iter().format(", "))?;
1295 }
1296
1297 Ok(())
1298 }
1299}
1300
1301impl fmt::Debug for Requires<'_> {
1302 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1303 if !self.params.is_empty() {
1304 write!(
1305 f,
1306 "forall {}.",
1307 self.params.iter().format_with(",", |param, f| {
1308 f(&format_args!("{}:{:?}", param.name, param.sort))
1309 })
1310 )?;
1311 }
1312 write!(f, "{:?}", self.pred)
1313 }
1314}
1315
1316impl fmt::Debug for Ensures<'_> {
1317 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1318 match self {
1319 Ensures::Type(loc, ty) => write!(f, "{loc:?}: {ty:?}"),
1320 Ensures::Pred(e) => write!(f, "{e:?}"),
1321 }
1322 }
1323}
1324
1325impl fmt::Debug for Ty<'_> {
1326 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1327 match &self.kind {
1328 TyKind::BaseTy(bty) => write!(f, "{bty:?}"),
1329 TyKind::Indexed(bty, idx) => write!(f, "{bty:?}[{idx:?}]"),
1330 TyKind::Exists(params, ty) => {
1331 write!(f, "{{")?;
1332 write!(
1333 f,
1334 "{}",
1335 params.iter().format_with(",", |param, f| {
1336 f(&format_args!("{}:{:?}", param.name, param.sort))
1337 })
1338 )?;
1339 if let TyKind::Constr(pred, ty) = &ty.kind {
1340 write!(f, ". {ty:?} | {pred:?}}}")
1341 } else {
1342 write!(f, ". {ty:?}}}")
1343 }
1344 }
1345 TyKind::StrgRef(_lft, loc, ty) => write!(f, "&strg <{loc:?}: {ty:?}>"),
1346 TyKind::Ref(_lft, mut_ty) => {
1347 write!(f, "&{}{:?}", mut_ty.mutbl.prefix_str(), mut_ty.ty)
1348 }
1349 TyKind::BareFn(bare_fn_ty) => {
1350 write!(f, "{bare_fn_ty:?}")
1351 }
1352 TyKind::Tuple(tys) => write!(f, "({:?})", tys.iter().format(", ")),
1353 TyKind::Array(ty, len) => write!(f, "[{ty:?}; {len:?}]"),
1354 TyKind::Never => write!(f, "!"),
1355 TyKind::Constr(pred, ty) => write!(f, "{{{ty:?} | {pred:?}}}"),
1356 TyKind::RawPtr(ty, Mutability::Not) => write!(f, "*const {ty:?}"),
1357 TyKind::RawPtr(ty, Mutability::Mut) => write!(f, "*mut {ty:?}"),
1358 TyKind::Infer => write!(f, "_"),
1359 TyKind::OpaqueDef(opaque_ty) => {
1360 write!(f, "impl trait <def_id = {:?}>", opaque_ty.def_id.resolved_id(),)
1361 }
1362 TyKind::TraitObject(poly_traits, _lft, _syntax) => {
1363 write!(f, "dyn {poly_traits:?}")
1364 }
1365 TyKind::Err(_) => write!(f, "err"),
1366 }
1367 }
1368}
1369
1370impl fmt::Debug for BareFnTy<'_> {
1371 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1372 if !self.generic_params.is_empty() {
1373 write!(
1374 f,
1375 "for<{}>",
1376 self.generic_params
1377 .iter()
1378 .map(|param| param.name.ident())
1379 .format(",")
1380 )?;
1381 }
1382 write!(f, "{:?}", self.decl)
1383 }
1384}
1385
1386impl fmt::Debug for Lifetime {
1387 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1388 match self {
1389 Lifetime::Hole(_) => write!(f, "'_"),
1390 Lifetime::Resolved(lft) => write!(f, "{lft:?}"),
1391 }
1392 }
1393}
1394
1395impl fmt::Debug for ConstArg {
1396 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1397 write!(f, "{:?}", self.kind)
1398 }
1399}
1400
1401impl fmt::Debug for ConstArgKind {
1402 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1403 match self {
1404 ConstArgKind::Lit(n) => write!(f, "{n}"),
1405 ConstArgKind::Param(p) => write!(f, "{p:?}"),
1406 ConstArgKind::Infer => write!(f, "_"),
1407 }
1408 }
1409}
1410
1411impl fmt::Debug for BaseTy<'_> {
1412 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1413 match &self.kind {
1414 BaseTyKind::Path(qpath) => write!(f, "{qpath:?}"),
1415 BaseTyKind::Slice(ty) => write!(f, "[{ty:?}]"),
1416 BaseTyKind::Err(_) => write!(f, "err"),
1417 }
1418 }
1419}
1420
1421impl fmt::Debug for QPath<'_> {
1422 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1423 match self {
1424 QPath::Resolved(_, path) => write!(f, "{path:?}"),
1425 QPath::TypeRelative(qself, assoc) => write!(f, "<{qself:?}>::{assoc:?}"),
1426 }
1427 }
1428}
1429
1430impl fmt::Debug for Path<'_> {
1431 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1432 write!(f, "{:?}", self.segments.iter().format("::"))?;
1433 if !self.refine.is_empty() {
1434 write!(f, "({:?})", self.refine.iter().format(", "))?;
1435 }
1436 Ok(())
1437 }
1438}
1439
1440impl fmt::Debug for PathSegment<'_> {
1441 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1442 write!(f, "{}", self.ident)?;
1443 let args: Vec<_> = self
1444 .args
1445 .iter()
1446 .map(|a| a as &dyn std::fmt::Debug)
1447 .chain(self.constraints.iter().map(|b| b as &dyn std::fmt::Debug))
1448 .collect();
1449 if !args.is_empty() {
1450 write!(f, "<{:?}>", args.iter().format(", "))?;
1451 }
1452 Ok(())
1453 }
1454}
1455
1456impl fmt::Debug for GenericArg<'_> {
1457 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1458 match self {
1459 GenericArg::Type(ty) => write!(f, "{ty:?}"),
1460 GenericArg::Lifetime(lft) => write!(f, "{lft:?}"),
1461 GenericArg::Const(cst) => write!(f, "{cst:?}"),
1462 GenericArg::Infer => write!(f, "_"),
1463 }
1464 }
1465}
1466
1467impl fmt::Debug for AssocItemConstraint<'_> {
1468 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1469 match &self.kind {
1470 AssocItemConstraintKind::Equality { term } => {
1471 write!(f, "{:?} = {:?}", self.ident, term)
1472 }
1473 }
1474 }
1475}
1476
1477impl fmt::Debug for AliasReft<'_> {
1478 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1479 write!(f, "<{:?} as {:?}>::{}", self.qself, self.path, self.name)
1480 }
1481}
1482
1483impl fmt::Debug for QuantKind {
1484 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1485 match self {
1486 QuantKind::Forall => write!(f, "∀"),
1487 QuantKind::Exists => write!(f, "∃"),
1488 }
1489 }
1490}
1491
1492impl fmt::Debug for Expr<'_> {
1493 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1494 match self.kind {
1495 ExprKind::Var(x, ..) => write!(f, "{x:?}"),
1496 ExprKind::BinaryOp(op, e1, e2) => write!(f, "({e1:?} {op:?} {e2:?})"),
1497 ExprKind::PrimApp(op, e1, e2) => write!(f, "[{op:?}]({e1:?}, {e2:?})"),
1498 ExprKind::UnaryOp(op, e) => write!(f, "{op:?}{e:?}"),
1499 ExprKind::Literal(lit) => write!(f, "{lit:?}"),
1500 ExprKind::App(uf, es) => write!(f, "{uf:?}({:?})", es.iter().format(", ")),
1501 ExprKind::Alias(alias, refine_args) => {
1502 write!(f, "{alias:?}({:?})", refine_args.iter().format(", "))
1503 }
1504 ExprKind::IfThenElse(p, e1, e2) => {
1505 write!(f, "(if {p:?} {{ {e1:?} }} else {{ {e2:?} }})")
1506 }
1507 ExprKind::Dot(var, fld) => write!(f, "{var:?}.{fld}"),
1508 ExprKind::Abs(params, body) => {
1509 write!(
1510 f,
1511 "|{}| {body:?}",
1512 params.iter().format_with(", ", |param, f| {
1513 f(&format_args!("{}: {:?}", param.name, param.sort))
1514 })
1515 )
1516 }
1517 ExprKind::Record(flds) => {
1518 write!(f, "{{ {:?} }}", flds.iter().format(", "))
1519 }
1520 ExprKind::Constructor(path, exprs, spread) => {
1521 if let Some(path) = path
1522 && let Some(s) = spread
1523 {
1524 write!(f, "{:?} {{ {:?}, ..{:?} }}", path, exprs.iter().format(", "), s)
1525 } else if let Some(path) = path {
1526 write!(f, "{:?} {{ {:?} }}", path, exprs.iter().format(", "))
1527 } else if let Some(s) = spread {
1528 write!(f, "{{ {:?} ..{:?} }}", exprs.iter().format(", "), s)
1529 } else {
1530 write!(f, "{{ {:?} }}", exprs.iter().format(", "))
1531 }
1532 }
1533 ExprKind::BoundedQuant(kind, refine_param, rng, expr) => {
1534 write!(f, "{kind:?} {refine_param:?} in {}.. {} {{ {expr:?} }}", rng.start, rng.end)
1535 }
1536 ExprKind::Err(_) => write!(f, "err"),
1537 ExprKind::Block(decls, body) => {
1538 for decl in decls {
1539 write!(f, "let {:?} = {:?};", decl.param, decl.init)?;
1540 }
1541 write!(f, "{body:?}")
1542 }
1543 }
1544 }
1545}
1546
1547impl fmt::Debug for PathExpr<'_> {
1548 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1549 write!(f, "{}", self.segments.iter().format("::"))
1550 }
1551}
1552
1553impl fmt::Debug for Lit {
1554 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1555 match self {
1556 Lit::Int(i, Some(NumLitKind::Real)) => write!(f, "{i}real"),
1557 Lit::Int(i, _) => write!(f, "{i}"),
1558 Lit::Bool(b) => write!(f, "{b}"),
1559 Lit::Str(s) => write!(f, "\"{s:?}\""),
1560 Lit::Char(c) => write!(f, "\'{c}\'"),
1561 }
1562 }
1563}
1564
1565impl fmt::Debug for Sort<'_> {
1566 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1567 match self {
1568 Sort::Path(path) => write!(f, "{path:?}"),
1569 Sort::BitVec(w) => write!(f, "bitvec({w})"),
1570 Sort::Loc => write!(f, "loc"),
1571 Sort::Func(fsort) => write!(f, "{fsort:?}"),
1572 Sort::SortOf(bty) => write!(f, "<{bty:?}>::sort"),
1573 Sort::Infer => write!(f, "_"),
1574 Sort::Err(_) => write!(f, "err"),
1575 }
1576 }
1577}
1578
1579impl fmt::Debug for SortPath<'_> {
1580 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1581 write!(f, "{:?}", self.res)?;
1582 if !self.args.is_empty() {
1583 write!(f, "<{:?}>", self.args.iter().format(", "))?;
1584 }
1585 Ok(())
1586 }
1587}
1588
1589impl fmt::Debug for SortRes {
1590 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1591 match self {
1592 SortRes::PrimSort(PrimSort::Bool) => write!(f, "bool"),
1593 SortRes::PrimSort(PrimSort::Int) => write!(f, "int"),
1594 SortRes::PrimSort(PrimSort::Real) => write!(f, "real"),
1595 SortRes::PrimSort(PrimSort::Char) => write!(f, "char"),
1596 SortRes::PrimSort(PrimSort::Set) => write!(f, "Set"),
1597 SortRes::PrimSort(PrimSort::Map) => write!(f, "Map"),
1598 SortRes::SortParam(n) => write!(f, "@{n}"),
1599 SortRes::TyParam(def_id) => write!(f, "{}::sort", def_id_to_string(*def_id)),
1600 SortRes::SelfParam { trait_id } => {
1601 write!(f, "{}::Self::sort", def_id_to_string(*trait_id))
1602 }
1603 SortRes::SelfAlias { alias_to } => {
1604 write!(f, "{}::Self::sort", def_id_to_string(*alias_to))
1605 }
1606 SortRes::SelfParamAssoc { ident: assoc, .. } => {
1607 write!(f, "Self::{assoc}")
1608 }
1609 SortRes::User { name } => write!(f, "{name}"),
1610 SortRes::Adt(def_id) => write!(f, "{}::sort", def_id_to_string(*def_id)),
1611 }
1612 }
1613}
1614
1615impl fmt::Debug for PolyFuncSort<'_> {
1616 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1617 if self.params > 0 {
1618 write!(f, "for<{}>{:?}", self.params, self.fsort)
1619 } else {
1620 write!(f, "{:?}", self.fsort)
1621 }
1622 }
1623}
1624
1625impl fmt::Debug for FuncSort<'_> {
1626 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1627 match self.inputs() {
1628 [input] => {
1629 write!(f, "{:?} -> {:?}", input, self.output())
1630 }
1631 inputs => {
1632 write!(f, "({:?}) -> {:?}", inputs.iter().format(", "), self.output())
1633 }
1634 }
1635 }
1636}