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}
285
286impl FluxItem<'_> {
287 pub fn def_id(self) -> FluxLocalDefId {
288 match self {
289 FluxItem::Qualifier(qualifier) => qualifier.def_id,
290 FluxItem::Func(func) => func.def_id,
291 FluxItem::PrimOpProp(prop) => prop.def_id,
292 }
293 }
294}
295
296#[derive(Debug)]
297pub struct ForeignItem<'fhir> {
298 pub ident: Ident,
299 pub kind: ForeignItemKind<'fhir>,
300 pub owner_id: MaybeExternId<OwnerId>,
301 pub span: Span,
302}
303
304#[derive(Debug)]
305pub enum ForeignItemKind<'fhir> {
306 Fn(FnSig<'fhir>, &'fhir Generics<'fhir>),
307}
308
309#[derive(Debug, Clone, Copy)]
310pub struct SortDecl {
311 pub name: Symbol,
312 pub span: Span,
313}
314
315pub type SortDecls = FxHashMap<Symbol, SortDecl>;
316
317#[derive(Debug, Clone, Copy)]
318pub struct WhereBoundPredicate<'fhir> {
319 pub span: Span,
320 pub bounded_ty: Ty<'fhir>,
321 pub bounds: GenericBounds<'fhir>,
322}
323
324pub type GenericBounds<'fhir> = &'fhir [GenericBound<'fhir>];
325
326#[derive(Debug, Clone, Copy)]
327pub enum GenericBound<'fhir> {
328 Trait(PolyTraitRef<'fhir>),
329 Outlives(Lifetime),
330}
331
332#[derive(Debug, Clone, Copy)]
333pub struct PolyTraitRef<'fhir> {
334 pub bound_generic_params: &'fhir [GenericParam<'fhir>],
335 pub refine_params: &'fhir [RefineParam<'fhir>],
337 pub modifiers: TraitBoundModifier,
338 pub trait_ref: Path<'fhir>,
339 pub span: Span,
340}
341
342#[derive(Debug, Copy, Clone)]
343pub enum TraitBoundModifier {
344 None,
345 Maybe,
346}
347
348#[derive(Debug)]
349pub struct Trait<'fhir> {
350 pub assoc_refinements: &'fhir [TraitAssocReft<'fhir>],
351}
352
353impl<'fhir> Trait<'fhir> {
354 pub fn find_assoc_reft(&self, name: Symbol) -> Option<&'fhir TraitAssocReft<'fhir>> {
355 self.assoc_refinements
356 .iter()
357 .find(|assoc_reft| assoc_reft.name == name)
358 }
359}
360
361#[derive(Debug, Clone, Copy)]
362pub struct TraitAssocReft<'fhir> {
363 pub name: Symbol,
364 pub params: &'fhir [RefineParam<'fhir>],
365 pub output: Sort<'fhir>,
366 pub body: Option<Expr<'fhir>>,
367 pub span: Span,
368 pub final_: bool,
369}
370
371#[derive(Debug)]
372pub struct Impl<'fhir> {
373 pub assoc_refinements: &'fhir [ImplAssocReft<'fhir>],
374}
375
376impl<'fhir> Impl<'fhir> {
377 pub fn find_assoc_reft(&self, name: Symbol) -> Option<&'fhir ImplAssocReft<'fhir>> {
378 self.assoc_refinements
379 .iter()
380 .find(|assoc_reft| assoc_reft.name == name)
381 }
382}
383
384#[derive(Clone, Copy, Debug)]
385pub struct ImplAssocReft<'fhir> {
386 pub name: Symbol,
387 pub params: &'fhir [RefineParam<'fhir>],
388 pub output: Sort<'fhir>,
389 pub body: Expr<'fhir>,
390 pub span: Span,
391}
392
393#[derive(Debug)]
394pub struct OpaqueTy<'fhir> {
395 pub def_id: MaybeExternId,
396 pub bounds: GenericBounds<'fhir>,
397}
398
399pub type Arena = bumpalo::Bump;
400
401#[derive(Default)]
406pub struct FluxItems<'fhir> {
407 pub items: FxIndexMap<FluxLocalDefId, FluxItem<'fhir>>,
408}
409
410impl FluxItems<'_> {
411 pub fn new() -> Self {
412 Self { items: Default::default() }
413 }
414}
415
416#[derive(Debug)]
417pub struct TyAlias<'fhir> {
418 pub index: Option<RefineParam<'fhir>>,
419 pub ty: Ty<'fhir>,
420 pub span: Span,
421 pub lifted: bool,
423}
424
425#[derive(Debug, Clone, Copy)]
426pub struct StructDef<'fhir> {
427 pub refinement: &'fhir RefinementKind<'fhir>,
428 pub params: &'fhir [RefineParam<'fhir>],
429 pub kind: StructKind<'fhir>,
430 pub invariants: &'fhir [Expr<'fhir>],
431}
432
433#[derive(Debug, Clone, Copy)]
434pub enum StructKind<'fhir> {
435 Transparent { fields: &'fhir [FieldDef<'fhir>] },
436 Opaque,
437}
438
439#[derive(Debug, Clone, Copy)]
440pub struct FieldDef<'fhir> {
441 pub ty: Ty<'fhir>,
442 pub lifted: bool,
444}
445
446#[derive(Debug)]
447pub enum RefinementKind<'fhir> {
448 Refined(RefinedBy<'fhir>),
450 Reflected,
452}
453
454impl RefinementKind<'_> {
455 pub fn is_reflected(&self) -> bool {
456 matches!(self, RefinementKind::Reflected)
457 }
458}
459
460#[derive(Debug)]
461pub struct EnumDef<'fhir> {
462 pub refinement: &'fhir RefinementKind<'fhir>,
463 pub params: &'fhir [RefineParam<'fhir>],
464 pub variants: &'fhir [VariantDef<'fhir>],
465 pub invariants: &'fhir [Expr<'fhir>],
466}
467
468#[derive(Debug, Clone, Copy)]
469pub struct VariantDef<'fhir> {
470 pub def_id: LocalDefId,
471 pub params: &'fhir [RefineParam<'fhir>],
472 pub fields: &'fhir [FieldDef<'fhir>],
473 pub ret: VariantRet<'fhir>,
474 pub span: Span,
475 pub lifted: bool,
477}
478
479#[derive(Debug, Clone, Copy)]
480pub struct VariantRet<'fhir> {
481 pub enum_id: DefId,
482 pub idx: Expr<'fhir>,
483}
484
485#[derive(Clone, Copy)]
486pub struct FnDecl<'fhir> {
487 pub requires: &'fhir [Requires<'fhir>],
488 pub inputs: &'fhir [Ty<'fhir>],
489 pub output: FnOutput<'fhir>,
490 pub span: Span,
491 pub lifted: bool,
493}
494
495#[derive(Clone, Copy)]
497pub struct Requires<'fhir> {
498 pub params: &'fhir [RefineParam<'fhir>],
500 pub pred: Expr<'fhir>,
501}
502
503#[derive(Clone, Copy)]
504pub struct FnSig<'fhir> {
505 pub header: FnHeader,
506 pub decl: &'fhir FnDecl<'fhir>,
507}
508
509#[derive(Clone, Copy)]
510pub struct FnOutput<'fhir> {
511 pub params: &'fhir [RefineParam<'fhir>],
512 pub ret: Ty<'fhir>,
513 pub ensures: &'fhir [Ensures<'fhir>],
514}
515
516#[derive(Clone, Copy)]
517pub enum Ensures<'fhir> {
518 Type(PathExpr<'fhir>, &'fhir Ty<'fhir>),
520 Pred(Expr<'fhir>),
522}
523
524#[derive(Clone, Copy)]
525pub struct Ty<'fhir> {
526 pub kind: TyKind<'fhir>,
527 pub span: Span,
528}
529
530#[derive(Clone, Copy)]
531pub enum TyKind<'fhir> {
532 BaseTy(BaseTy<'fhir>),
541 Indexed(BaseTy<'fhir>, Expr<'fhir>),
542 Exists(&'fhir [RefineParam<'fhir>], &'fhir Ty<'fhir>),
543 Constr(Expr<'fhir>, &'fhir Ty<'fhir>),
546 StrgRef(Lifetime, &'fhir PathExpr<'fhir>, &'fhir Ty<'fhir>),
547 Ref(Lifetime, MutTy<'fhir>),
548 BareFn(&'fhir BareFnTy<'fhir>),
549 Tuple(&'fhir [Ty<'fhir>]),
550 Array(&'fhir Ty<'fhir>, ConstArg),
551 RawPtr(&'fhir Ty<'fhir>, Mutability),
552 OpaqueDef(&'fhir OpaqueTy<'fhir>),
553 TraitObject(&'fhir [PolyTraitRef<'fhir>], Lifetime, TraitObjectSyntax),
554 Never,
555 Infer,
556 Err(ErrorGuaranteed),
557}
558
559pub struct BareFnTy<'fhir> {
560 pub safety: Safety,
561 pub abi: rustc_abi::ExternAbi,
562 pub generic_params: &'fhir [GenericParam<'fhir>],
563 pub decl: &'fhir FnDecl<'fhir>,
564 pub param_idents: &'fhir [Option<Ident>],
565}
566
567#[derive(Clone, Copy)]
568pub struct MutTy<'fhir> {
569 pub ty: &'fhir Ty<'fhir>,
570 pub mutbl: Mutability,
571}
572
573#[derive(Copy, Clone, PartialEq, Eq)]
576pub enum Lifetime {
577 Hole(FhirId),
579 Resolved(ResolvedArg),
581}
582
583#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq, Encodable, Decodable)]
585pub enum FluxOwnerId {
586 Flux(FluxLocalDefId),
587 Rust(OwnerId),
588}
589
590impl FluxOwnerId {
591 pub fn def_id(self) -> Option<LocalDefId> {
592 match self {
593 FluxOwnerId::Flux(_) => None,
594 FluxOwnerId::Rust(owner_id) => Some(owner_id.def_id),
595 }
596 }
597}
598
599#[derive(Debug, Hash, PartialEq, Eq, Copy, Clone, Encodable, Decodable)]
607pub struct FhirId {
608 pub owner: FluxOwnerId,
609 pub local_id: ItemLocalId,
610}
611
612newtype_index! {
613 #[encodable]
615 pub struct ItemLocalId {}
616}
617
618#[derive(Clone, Copy)]
620pub struct BaseTy<'fhir> {
621 pub kind: BaseTyKind<'fhir>,
622 pub fhir_id: FhirId,
623 pub span: Span,
624}
625
626impl<'fhir> BaseTy<'fhir> {
627 pub fn from_qpath(qpath: QPath<'fhir>, fhir_id: FhirId) -> Self {
628 let span = qpath.span();
629 Self { kind: BaseTyKind::Path(qpath), fhir_id, span }
630 }
631
632 fn as_path(&self) -> Option<Path<'fhir>> {
633 match self.kind {
634 BaseTyKind::Path(QPath::Resolved(None, path)) => Some(path),
635 _ => None,
636 }
637 }
638}
639
640#[derive(Clone, Copy)]
641pub enum BaseTyKind<'fhir> {
642 Path(QPath<'fhir>),
643 Slice(&'fhir Ty<'fhir>),
644 Err(ErrorGuaranteed),
645}
646
647#[derive(Clone, Copy)]
648pub enum QPath<'fhir> {
649 Resolved(Option<&'fhir Ty<'fhir>>, Path<'fhir>),
650 TypeRelative(&'fhir Ty<'fhir>, &'fhir PathSegment<'fhir>),
651}
652
653#[derive(Clone, Copy)]
654pub struct Path<'fhir> {
655 pub res: Res,
656 pub fhir_id: FhirId,
657 pub segments: &'fhir [PathSegment<'fhir>],
658 pub refine: &'fhir [Expr<'fhir>],
659 pub span: Span,
660}
661
662impl<'fhir> Path<'fhir> {
663 pub fn last_segment(&self) -> &'fhir PathSegment<'fhir> {
664 self.segments.last().unwrap()
665 }
666}
667
668#[derive(Clone, Copy)]
669pub struct PathSegment<'fhir> {
670 pub ident: Ident,
671 pub res: Res,
672 pub args: &'fhir [GenericArg<'fhir>],
673 pub constraints: &'fhir [AssocItemConstraint<'fhir>],
674}
675
676#[derive(Clone, Copy)]
677pub struct AssocItemConstraint<'fhir> {
678 pub ident: Ident,
679 pub kind: AssocItemConstraintKind<'fhir>,
680}
681
682#[derive(Clone, Copy)]
683pub enum AssocItemConstraintKind<'fhir> {
684 Equality { term: Ty<'fhir> },
685}
686
687#[derive(Clone, Copy)]
688pub enum GenericArg<'fhir> {
689 Lifetime(Lifetime),
690 Type(&'fhir Ty<'fhir>),
691 Const(ConstArg),
692 Infer,
693}
694
695impl<'fhir> GenericArg<'fhir> {
696 pub fn expect_type(&self) -> &'fhir Ty<'fhir> {
697 if let GenericArg::Type(ty) = self { ty } else { bug!("expected `GenericArg::Type`") }
698 }
699}
700
701#[derive(PartialEq, Eq, Clone, Copy)]
702pub struct ConstArg {
703 pub kind: ConstArgKind,
704 pub span: Span,
705}
706
707#[derive(PartialEq, Eq, Clone, Copy)]
708pub enum ConstArgKind {
709 Lit(usize),
710 Param(DefId),
711 Infer,
712}
713
714#[derive(Eq, PartialEq, Debug, Copy, Clone)]
719pub enum Res<Id = !> {
720 Def(DefKind, DefId),
722 PrimTy(PrimTy),
724 SelfTyAlias {
726 alias_to: DefId,
727 is_trait_impl: bool,
728 },
729 SelfTyParam {
731 trait_: DefId,
732 },
733 Param(ParamKind, Id),
735 GlobalFunc(SpecFuncKind),
737 Err,
738}
739
740#[derive(Copy, Clone, Debug)]
742pub struct PartialRes<Id = !> {
743 base_res: Res<Id>,
744 unresolved_segments: usize,
745}
746
747impl<Id: Copy> PartialRes<Id> {
748 pub fn new(base_res: Res<Id>) -> Self {
749 Self { base_res, unresolved_segments: 0 }
750 }
751
752 pub fn with_unresolved_segments(base_res: Res<Id>, unresolved_segments: usize) -> Self {
753 Self { base_res, unresolved_segments }
754 }
755
756 #[inline]
757 pub fn base_res(&self) -> Res<Id> {
758 self.base_res
759 }
760
761 pub fn unresolved_segments(&self) -> usize {
762 self.unresolved_segments
763 }
764
765 #[inline]
766 pub fn full_res(&self) -> Option<Res<Id>> {
767 (self.unresolved_segments == 0).then_some(self.base_res)
768 }
769
770 #[inline]
771 pub fn expect_full_res(&self) -> Res<Id> {
772 self.full_res().unwrap_or_else(|| bug!("expected full res"))
773 }
774
775 pub fn is_box(&self, tcx: TyCtxt) -> bool {
776 self.full_res().is_some_and(|res| res.is_box(tcx))
777 }
778
779 pub fn map_param_id<R>(&self, f: impl FnOnce(Id) -> R) -> PartialRes<R> {
780 PartialRes {
781 base_res: self.base_res.map_param_id(f),
782 unresolved_segments: self.unresolved_segments,
783 }
784 }
785}
786
787#[derive(Debug, Clone, Copy)]
788pub struct RefineParam<'fhir> {
789 pub id: ParamId,
790 pub name: Symbol,
791 pub span: Span,
792 pub sort: Sort<'fhir>,
793 pub kind: ParamKind,
794 pub fhir_id: FhirId,
795}
796
797#[derive(PartialEq, Eq, Debug, Clone, Copy)]
799pub enum ParamKind {
800 Explicit(Option<ParamMode>),
802 At,
804 Pound,
806 Colon,
808 Loc,
810 Error,
821}
822
823impl ParamKind {
824 pub fn is_loc(&self) -> bool {
825 matches!(self, ParamKind::Loc)
826 }
827}
828
829#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
831pub enum InferMode {
832 EVar,
836 KVar,
840}
841
842impl InferMode {
843 pub fn from_param_kind(kind: ParamKind) -> InferMode {
844 if let ParamKind::Explicit(Some(ParamMode::Horn)) = kind {
845 InferMode::KVar
846 } else {
847 InferMode::EVar
848 }
849 }
850
851 pub fn prefix_str(self) -> &'static str {
852 match self {
853 InferMode::EVar => "?",
854 InferMode::KVar => "$",
855 }
856 }
857}
858
859#[derive(Clone, Copy)]
860pub enum PrimSort {
861 Int,
862 Bool,
863 Char,
864 Real,
865 Set,
866 Map,
867 Str,
868}
869
870impl PrimSort {
871 pub fn name_str(self) -> &'static str {
872 match self {
873 PrimSort::Int => "int",
874 PrimSort::Str => "str",
875 PrimSort::Bool => "bool",
876 PrimSort::Char => "char",
877 PrimSort::Real => "real",
878 PrimSort::Set => "Set",
879 PrimSort::Map => "Map",
880 }
881 }
882
883 pub fn generics(self) -> usize {
885 match self {
886 PrimSort::Int | PrimSort::Bool | PrimSort::Real | PrimSort::Char | PrimSort::Str => 0,
887 PrimSort::Set => 1,
888 PrimSort::Map => 2,
889 }
890 }
891}
892
893#[derive(Clone, Copy)]
894pub enum SortRes {
895 PrimSort(PrimSort),
897 User { name: Symbol },
899 SortParam(usize),
901 TyParam(DefId),
903 SelfParam {
905 trait_id: DefId,
907 },
908 SelfAlias {
910 alias_to: DefId,
912 },
913 SelfParamAssoc { trait_id: DefId, ident: Ident },
922 Adt(DefId),
924}
925
926#[derive(Clone, Copy)]
927pub enum Sort<'fhir> {
928 Path(SortPath<'fhir>),
929 Loc,
931 BitVec(u32),
933 Func(PolyFuncSort<'fhir>),
935 SortOf(BaseTy<'fhir>),
938 Infer,
940 Err(ErrorGuaranteed),
941}
942
943#[derive(Clone, Copy)]
945pub struct SortPath<'fhir> {
946 pub res: SortRes,
947 pub segments: &'fhir [Ident],
948 pub args: &'fhir [Sort<'fhir>],
949}
950
951#[derive(Clone, Copy)]
952pub struct FuncSort<'fhir> {
953 pub inputs_and_output: &'fhir [Sort<'fhir>],
955}
956
957#[derive(Clone, Copy)]
958pub struct PolyFuncSort<'fhir> {
959 pub params: usize,
960 pub fsort: FuncSort<'fhir>,
961}
962
963impl<'fhir> PolyFuncSort<'fhir> {
964 pub fn new(params: usize, inputs_and_output: &'fhir [Sort]) -> Self {
965 let fsort = FuncSort { inputs_and_output };
966 Self { params, fsort }
967 }
968}
969
970#[derive(Clone, Copy)]
972pub enum AliasReft<'fhir> {
973 Qualified { qself: &'fhir Ty<'fhir>, trait_: Path<'fhir>, name: Ident },
975 TypeRelative { qself: &'fhir Ty<'fhir>, name: Ident },
979}
980
981#[derive(Debug, Clone, Copy)]
982pub struct FieldExpr<'fhir> {
983 pub ident: Ident,
984 pub expr: Expr<'fhir>,
985 pub fhir_id: FhirId,
986 pub span: Span,
987}
988
989#[derive(Debug, Clone, Copy)]
990pub struct Spread<'fhir> {
991 pub expr: Expr<'fhir>,
992 pub span: Span,
993 pub fhir_id: FhirId,
994}
995
996#[derive(Clone, Copy)]
997pub struct Expr<'fhir> {
998 pub kind: ExprKind<'fhir>,
999 pub fhir_id: FhirId,
1000 pub span: Span,
1001}
1002
1003#[derive(Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
1004pub enum QuantKind {
1005 Forall,
1006 Exists,
1007}
1008
1009#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, Encodable, Decodable)]
1010pub struct Range {
1011 pub start: usize,
1012 pub end: usize,
1013}
1014
1015#[derive(Clone, Copy)]
1016pub enum ExprKind<'fhir> {
1017 Var(QPathExpr<'fhir>),
1018 Dot(&'fhir Expr<'fhir>, Ident),
1019 Literal(Lit),
1020 BinaryOp(BinOp, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1021 UnaryOp(UnOp, &'fhir Expr<'fhir>),
1022 App(PathExpr<'fhir>, &'fhir [Expr<'fhir>]),
1023 PrimApp(BinOp, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1025 Alias(AliasReft<'fhir>, &'fhir [Expr<'fhir>]),
1026 IfThenElse(&'fhir Expr<'fhir>, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1027 Abs(&'fhir [RefineParam<'fhir>], &'fhir Expr<'fhir>),
1028 BoundedQuant(QuantKind, RefineParam<'fhir>, Range, &'fhir Expr<'fhir>),
1029 Record(&'fhir [Expr<'fhir>]),
1030 Constructor(Option<PathExpr<'fhir>>, &'fhir [FieldExpr<'fhir>], Option<&'fhir Spread<'fhir>>),
1031 Block(&'fhir [LetDecl<'fhir>], &'fhir Expr<'fhir>),
1032 Err(ErrorGuaranteed),
1033}
1034
1035#[derive(Clone, Copy)]
1036pub enum QPathExpr<'fhir> {
1037 Resolved(PathExpr<'fhir>, Option<ParamKind>),
1038 TypeRelative(&'fhir Ty<'fhir>, Ident),
1039}
1040
1041#[derive(Clone, Copy)]
1042pub struct LetDecl<'fhir> {
1043 pub param: RefineParam<'fhir>,
1044 pub init: Expr<'fhir>,
1045}
1046
1047impl Expr<'_> {
1048 pub fn is_colon_param(&self) -> Option<ParamId> {
1049 if let ExprKind::Var(QPathExpr::Resolved(path, Some(ParamKind::Colon))) = &self.kind
1050 && let Res::Param(kind, id) = path.res
1051 {
1052 debug_assert_eq!(kind, ParamKind::Colon);
1053 Some(id)
1054 } else {
1055 None
1056 }
1057 }
1058}
1059
1060#[derive(Clone, Copy)]
1061pub enum NumLitKind {
1062 Int,
1063 Real,
1064}
1065
1066#[derive(Clone, Copy)]
1067pub enum Lit {
1068 Int(u128, Option<NumLitKind>),
1069 Bool(bool),
1070 Str(Symbol),
1071 Char(char),
1072}
1073
1074#[derive(Clone, Copy)]
1075pub struct PathExpr<'fhir> {
1076 pub segments: &'fhir [Ident],
1077 pub res: Res<ParamId>,
1078 pub fhir_id: FhirId,
1079 pub span: Span,
1080}
1081
1082newtype_index! {
1083 #[debug_format = "a{}"]
1084 pub struct ParamId {}
1085}
1086
1087impl PolyTraitRef<'_> {
1088 pub fn trait_def_id(&self) -> DefId {
1089 let path = &self.trait_ref;
1090 if let Res::Def(DefKind::Trait, did) = path.res {
1091 did
1092 } else {
1093 span_bug!(path.span, "unexpected resolution {:?}", path.res);
1094 }
1095 }
1096}
1097
1098impl From<OwnerId> for FluxOwnerId {
1099 fn from(owner_id: OwnerId) -> Self {
1100 FluxOwnerId::Rust(owner_id)
1101 }
1102}
1103
1104impl<'fhir> Ty<'fhir> {
1105 pub fn as_path(&self) -> Option<Path<'fhir>> {
1106 match &self.kind {
1107 TyKind::BaseTy(bty) => bty.as_path(),
1108 _ => None,
1109 }
1110 }
1111}
1112
1113impl<Id> Res<Id> {
1114 pub fn descr(&self) -> &'static str {
1115 match self {
1116 Res::PrimTy(_) => "builtin type",
1117 Res::Def(kind, def_id) => kind.descr(*def_id),
1118 Res::SelfTyAlias { .. } | Res::SelfTyParam { .. } => "self type",
1119 Res::Param(..) => "refinement parameter",
1120 Res::GlobalFunc(..) => "refinement function",
1121 Res::Err => "unresolved item",
1122 }
1123 }
1124
1125 pub fn is_box(&self, tcx: TyCtxt) -> bool {
1126 if let Res::Def(DefKind::Struct, def_id) = self {
1127 tcx.adt_def(def_id).is_box()
1128 } else {
1129 false
1130 }
1131 }
1132
1133 pub fn ns(&self) -> Option<Namespace> {
1135 match self {
1136 Res::Def(kind, ..) => kind.ns(),
1137 Res::PrimTy(..) | Res::SelfTyAlias { .. } | Res::SelfTyParam { .. } => {
1138 Some(Namespace::TypeNS)
1139 }
1140 Res::Param(..) | Res::GlobalFunc(..) => Some(Namespace::ValueNS),
1141 Res::Err => None,
1142 }
1143 }
1144
1145 pub fn matches_ns(&self, ns: Namespace) -> bool {
1147 self.ns().is_none_or(|actual_ns| actual_ns == ns)
1148 }
1149
1150 pub fn map_param_id<R>(self, f: impl FnOnce(Id) -> R) -> Res<R> {
1151 match self {
1152 Res::Param(kind, param_id) => Res::Param(kind, f(param_id)),
1153 Res::Def(def_kind, def_id) => Res::Def(def_kind, def_id),
1154 Res::PrimTy(prim_ty) => Res::PrimTy(prim_ty),
1155 Res::SelfTyAlias { alias_to, is_trait_impl } => {
1156 Res::SelfTyAlias { alias_to, is_trait_impl }
1157 }
1158 Res::SelfTyParam { trait_ } => Res::SelfTyParam { trait_ },
1159 Res::GlobalFunc(spec_func_kind) => Res::GlobalFunc(spec_func_kind),
1160 Res::Err => Res::Err,
1161 }
1162 }
1163
1164 pub fn expect_param(self) -> (ParamKind, Id) {
1165 if let Res::Param(kind, id) = self { (kind, id) } else { bug!("expected param") }
1166 }
1167}
1168
1169impl<Id1, Id2> TryFrom<rustc_hir::def::Res<Id1>> for Res<Id2> {
1170 type Error = ();
1171
1172 fn try_from(res: rustc_hir::def::Res<Id1>) -> Result<Self, Self::Error> {
1173 match res {
1174 rustc_hir::def::Res::Def(kind, did) => Ok(Res::Def(kind, did)),
1175 rustc_hir::def::Res::PrimTy(prim_ty) => Ok(Res::PrimTy(prim_ty)),
1176 rustc_hir::def::Res::SelfTyAlias { alias_to, forbid_generic: false, is_trait_impl } => {
1177 Ok(Res::SelfTyAlias { alias_to, is_trait_impl })
1178 }
1179 rustc_hir::def::Res::SelfTyParam { trait_ } => Ok(Res::SelfTyParam { trait_ }),
1180 rustc_hir::def::Res::Err => Ok(Res::Err),
1181 _ => Err(()),
1182 }
1183 }
1184}
1185
1186impl QPath<'_> {
1187 pub fn span(&self) -> Span {
1188 match self {
1189 QPath::Resolved(_, path) => path.span,
1190 QPath::TypeRelative(qself, assoc) => qself.span.to(assoc.ident.span),
1191 }
1192 }
1193}
1194
1195impl Lit {
1196 pub const TRUE: Lit = Lit::Bool(true);
1197}
1198
1199#[derive(Clone, Debug)]
1201pub struct RefinedBy<'fhir> {
1202 pub sort_params: FxIndexSet<DefId>,
1217 pub fields: FxIndexMap<Symbol, Sort<'fhir>>,
1219}
1220
1221#[derive(Debug)]
1222pub struct SpecFunc<'fhir> {
1223 pub def_id: FluxLocalDefId,
1224 pub params: usize,
1225 pub args: &'fhir [RefineParam<'fhir>],
1226 pub sort: Sort<'fhir>,
1227 pub body: Option<Expr<'fhir>>,
1228 pub hide: bool,
1229 pub ident_span: Span,
1230}
1231#[derive(Debug)]
1232pub struct PrimOpProp<'fhir> {
1233 pub def_id: FluxLocalDefId,
1234 pub op: BinOp,
1235 pub args: &'fhir [RefineParam<'fhir>],
1236 pub body: Expr<'fhir>,
1237 pub span: Span,
1238}
1239
1240#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1241pub enum SpecFuncKind {
1242 Thy(liquid_fixpoint::ThyFunc),
1244 Uif(FluxDefId),
1246 Def(FluxDefId),
1248 Cast,
1250}
1251
1252impl SpecFuncKind {
1253 pub fn def_id(&self) -> Option<FluxDefId> {
1254 match self {
1255 SpecFuncKind::Uif(flux_id) | SpecFuncKind::Def(flux_id) => Some(*flux_id),
1256 _ => None,
1257 }
1258 }
1259}
1260
1261impl<'fhir> Generics<'fhir> {
1262 pub fn get_param(&self, def_id: LocalDefId) -> &'fhir GenericParam<'fhir> {
1263 self.params
1264 .iter()
1265 .find(|p| p.def_id.local_id() == def_id)
1266 .unwrap()
1267 }
1268}
1269
1270impl<'fhir> RefinedBy<'fhir> {
1271 pub fn new(fields: FxIndexMap<Symbol, Sort<'fhir>>, sort_params: FxIndexSet<DefId>) -> Self {
1272 RefinedBy { sort_params, fields }
1273 }
1274
1275 pub fn trivial() -> Self {
1276 RefinedBy { sort_params: Default::default(), fields: Default::default() }
1277 }
1278}
1279
1280impl<'fhir> From<PolyFuncSort<'fhir>> for Sort<'fhir> {
1281 fn from(fsort: PolyFuncSort<'fhir>) -> Self {
1282 Self::Func(fsort)
1283 }
1284}
1285
1286impl FuncSort<'_> {
1287 pub fn inputs(&self) -> &[Sort<'_>] {
1288 &self.inputs_and_output[..self.inputs_and_output.len() - 1]
1289 }
1290
1291 pub fn output(&self) -> &Sort<'_> {
1292 &self.inputs_and_output[self.inputs_and_output.len() - 1]
1293 }
1294}
1295
1296impl rustc_errors::IntoDiagArg for Ty<'_> {
1297 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1298 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1299 }
1300}
1301
1302impl rustc_errors::IntoDiagArg for Path<'_> {
1303 fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1304 rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1305 }
1306}
1307
1308impl StructDef<'_> {
1309 pub fn is_opaque(&self) -> bool {
1310 matches!(self.kind, StructKind::Opaque)
1311 }
1312}
1313
1314impl fmt::Debug for FnSig<'_> {
1315 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1316 write!(f, "{:?}", self.decl)
1317 }
1318}
1319
1320impl fmt::Debug for FnDecl<'_> {
1321 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1322 if !self.requires.is_empty() {
1323 write!(f, "[{:?}] ", self.requires.iter().format(", "))?;
1324 }
1325 write!(f, "fn({:?}) -> {:?}", self.inputs.iter().format(", "), self.output)
1326 }
1327}
1328
1329impl fmt::Debug for FnOutput<'_> {
1330 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1331 if !self.params.is_empty() {
1332 write!(
1333 f,
1334 "exists<{}> ",
1335 self.params.iter().format_with(", ", |param, f| {
1336 f(&format_args!("{}: {:?}", param.name, param.sort))
1337 })
1338 )?;
1339 }
1340 write!(f, "{:?}", self.ret)?;
1341 if !self.ensures.is_empty() {
1342 write!(f, "; [{:?}]", self.ensures.iter().format(", "))?;
1343 }
1344
1345 Ok(())
1346 }
1347}
1348
1349impl fmt::Debug for Requires<'_> {
1350 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1351 if !self.params.is_empty() {
1352 write!(
1353 f,
1354 "forall {}.",
1355 self.params.iter().format_with(",", |param, f| {
1356 f(&format_args!("{}:{:?}", param.name, param.sort))
1357 })
1358 )?;
1359 }
1360 write!(f, "{:?}", self.pred)
1361 }
1362}
1363
1364impl fmt::Debug for Ensures<'_> {
1365 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1366 match self {
1367 Ensures::Type(loc, ty) => write!(f, "{loc:?}: {ty:?}"),
1368 Ensures::Pred(e) => write!(f, "{e:?}"),
1369 }
1370 }
1371}
1372
1373impl fmt::Debug for Ty<'_> {
1374 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1375 match &self.kind {
1376 TyKind::BaseTy(bty) => write!(f, "{bty:?}"),
1377 TyKind::Indexed(bty, idx) => write!(f, "{bty:?}[{idx:?}]"),
1378 TyKind::Exists(params, ty) => {
1379 write!(f, "{{")?;
1380 write!(
1381 f,
1382 "{}",
1383 params.iter().format_with(",", |param, f| {
1384 f(&format_args!("{}:{:?}", param.name, param.sort))
1385 })
1386 )?;
1387 if let TyKind::Constr(pred, ty) = &ty.kind {
1388 write!(f, ". {ty:?} | {pred:?}}}")
1389 } else {
1390 write!(f, ". {ty:?}}}")
1391 }
1392 }
1393 TyKind::StrgRef(_lft, loc, ty) => write!(f, "&strg <{loc:?}: {ty:?}>"),
1394 TyKind::Ref(_lft, mut_ty) => {
1395 write!(f, "&{}{:?}", mut_ty.mutbl.prefix_str(), mut_ty.ty)
1396 }
1397 TyKind::BareFn(bare_fn_ty) => {
1398 write!(f, "{bare_fn_ty:?}")
1399 }
1400 TyKind::Tuple(tys) => write!(f, "({:?})", tys.iter().format(", ")),
1401 TyKind::Array(ty, len) => write!(f, "[{ty:?}; {len:?}]"),
1402 TyKind::Never => write!(f, "!"),
1403 TyKind::Constr(pred, ty) => write!(f, "{{{ty:?} | {pred:?}}}"),
1404 TyKind::RawPtr(ty, Mutability::Not) => write!(f, "*const {ty:?}"),
1405 TyKind::RawPtr(ty, Mutability::Mut) => write!(f, "*mut {ty:?}"),
1406 TyKind::Infer => write!(f, "_"),
1407 TyKind::OpaqueDef(opaque_ty) => {
1408 write!(f, "impl trait <def_id = {:?}>", opaque_ty.def_id.resolved_id(),)
1409 }
1410 TyKind::TraitObject(poly_traits, _lft, _syntax) => {
1411 write!(f, "dyn {poly_traits:?}")
1412 }
1413 TyKind::Err(_) => write!(f, "err"),
1414 }
1415 }
1416}
1417
1418impl fmt::Debug for BareFnTy<'_> {
1419 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1420 if !self.generic_params.is_empty() {
1421 write!(
1422 f,
1423 "for<{}>",
1424 self.generic_params
1425 .iter()
1426 .map(|param| param.name.ident())
1427 .format(",")
1428 )?;
1429 }
1430 write!(f, "{:?}", self.decl)
1431 }
1432}
1433
1434impl fmt::Debug for Lifetime {
1435 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1436 match self {
1437 Lifetime::Hole(_) => write!(f, "'_"),
1438 Lifetime::Resolved(lft) => write!(f, "{lft:?}"),
1439 }
1440 }
1441}
1442
1443impl fmt::Debug for ConstArg {
1444 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1445 write!(f, "{:?}", self.kind)
1446 }
1447}
1448
1449impl fmt::Debug for ConstArgKind {
1450 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1451 match self {
1452 ConstArgKind::Lit(n) => write!(f, "{n}"),
1453 ConstArgKind::Param(p) => write!(f, "{p:?}"),
1454 ConstArgKind::Infer => write!(f, "_"),
1455 }
1456 }
1457}
1458
1459impl fmt::Debug for BaseTy<'_> {
1460 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1461 match &self.kind {
1462 BaseTyKind::Path(qpath) => write!(f, "{qpath:?}"),
1463 BaseTyKind::Slice(ty) => write!(f, "[{ty:?}]"),
1464 BaseTyKind::Err(_) => write!(f, "err"),
1465 }
1466 }
1467}
1468
1469impl fmt::Debug for QPath<'_> {
1470 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1471 match self {
1472 QPath::Resolved(_, path) => write!(f, "{path:?}"),
1473 QPath::TypeRelative(qself, assoc) => write!(f, "<{qself:?}>::{assoc:?}"),
1474 }
1475 }
1476}
1477
1478impl fmt::Debug for Path<'_> {
1479 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1480 write!(f, "{:?}", self.segments.iter().format("::"))?;
1481 if !self.refine.is_empty() {
1482 write!(f, "({:?})", self.refine.iter().format(", "))?;
1483 }
1484 Ok(())
1485 }
1486}
1487
1488impl fmt::Debug for PathSegment<'_> {
1489 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1490 write!(f, "{}", self.ident)?;
1491 let args: Vec<_> = self
1492 .args
1493 .iter()
1494 .map(|a| a as &dyn std::fmt::Debug)
1495 .chain(self.constraints.iter().map(|b| b as &dyn std::fmt::Debug))
1496 .collect();
1497 if !args.is_empty() {
1498 write!(f, "<{:?}>", args.iter().format(", "))?;
1499 }
1500 Ok(())
1501 }
1502}
1503
1504impl fmt::Debug for GenericArg<'_> {
1505 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1506 match self {
1507 GenericArg::Type(ty) => write!(f, "{ty:?}"),
1508 GenericArg::Lifetime(lft) => write!(f, "{lft:?}"),
1509 GenericArg::Const(cst) => write!(f, "{cst:?}"),
1510 GenericArg::Infer => write!(f, "_"),
1511 }
1512 }
1513}
1514
1515impl fmt::Debug for AssocItemConstraint<'_> {
1516 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1517 match &self.kind {
1518 AssocItemConstraintKind::Equality { term } => {
1519 write!(f, "{:?} = {:?}", self.ident, term)
1520 }
1521 }
1522 }
1523}
1524
1525impl fmt::Debug for AliasReft<'_> {
1526 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1527 match self {
1528 AliasReft::Qualified { qself, trait_, name } => {
1529 write!(f, "<{qself:?} as {trait_:?}>::{name}")
1530 }
1531 AliasReft::TypeRelative { qself, name } => {
1532 write!(f, "{qself:?}::{name}")
1533 }
1534 }
1535 }
1536}
1537
1538impl fmt::Debug for QuantKind {
1539 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1540 match self {
1541 QuantKind::Forall => write!(f, "∀"),
1542 QuantKind::Exists => write!(f, "∃"),
1543 }
1544 }
1545}
1546
1547impl fmt::Debug for Expr<'_> {
1548 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1549 match self.kind {
1550 ExprKind::Var(QPathExpr::Resolved(path, ..)) => write!(f, "{path:?}"),
1551 ExprKind::Var(QPathExpr::TypeRelative(qself, assoc)) => {
1552 write!(f, "<{qself:?}>::{assoc}")
1553 }
1554 ExprKind::BinaryOp(op, e1, e2) => write!(f, "({e1:?} {op:?} {e2:?})"),
1555 ExprKind::PrimApp(op, e1, e2) => write!(f, "[{op:?}]({e1:?}, {e2:?})"),
1556 ExprKind::UnaryOp(op, e) => write!(f, "{op:?}{e:?}"),
1557 ExprKind::Literal(lit) => write!(f, "{lit:?}"),
1558 ExprKind::App(uf, es) => write!(f, "{uf:?}({:?})", es.iter().format(", ")),
1559 ExprKind::Alias(alias, refine_args) => {
1560 write!(f, "{alias:?}({:?})", refine_args.iter().format(", "))
1561 }
1562 ExprKind::IfThenElse(p, e1, e2) => {
1563 write!(f, "(if {p:?} {{ {e1:?} }} else {{ {e2:?} }})")
1564 }
1565 ExprKind::Dot(var, fld) => write!(f, "{var:?}.{fld}"),
1566 ExprKind::Abs(params, body) => {
1567 write!(
1568 f,
1569 "|{}| {body:?}",
1570 params.iter().format_with(", ", |param, f| {
1571 f(&format_args!("{}: {:?}", param.name, param.sort))
1572 })
1573 )
1574 }
1575 ExprKind::Record(flds) => {
1576 write!(f, "{{ {:?} }}", flds.iter().format(", "))
1577 }
1578 ExprKind::Constructor(path, exprs, spread) => {
1579 if let Some(path) = path
1580 && let Some(s) = spread
1581 {
1582 write!(f, "{:?} {{ {:?}, ..{:?} }}", path, exprs.iter().format(", "), s)
1583 } else if let Some(path) = path {
1584 write!(f, "{:?} {{ {:?} }}", path, exprs.iter().format(", "))
1585 } else if let Some(s) = spread {
1586 write!(f, "{{ {:?} ..{:?} }}", exprs.iter().format(", "), s)
1587 } else {
1588 write!(f, "{{ {:?} }}", exprs.iter().format(", "))
1589 }
1590 }
1591 ExprKind::BoundedQuant(kind, refine_param, rng, expr) => {
1592 write!(f, "{kind:?} {refine_param:?} in {}.. {} {{ {expr:?} }}", rng.start, rng.end)
1593 }
1594 ExprKind::Err(_) => write!(f, "err"),
1595 ExprKind::Block(decls, body) => {
1596 for decl in decls {
1597 write!(f, "let {:?} = {:?};", decl.param, decl.init)?;
1598 }
1599 write!(f, "{body:?}")
1600 }
1601 }
1602 }
1603}
1604
1605impl fmt::Debug for PathExpr<'_> {
1606 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1607 write!(f, "{}", self.segments.iter().format("::"))
1608 }
1609}
1610
1611impl fmt::Debug for Lit {
1612 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1613 match self {
1614 Lit::Int(i, Some(NumLitKind::Real)) => write!(f, "{i}real"),
1615 Lit::Int(i, _) => write!(f, "{i}"),
1616 Lit::Bool(b) => write!(f, "{b}"),
1617 Lit::Str(s) => write!(f, "\"{s:?}\""),
1618 Lit::Char(c) => write!(f, "\'{c}\'"),
1619 }
1620 }
1621}
1622
1623impl fmt::Debug for Sort<'_> {
1624 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1625 match self {
1626 Sort::Path(path) => write!(f, "{path:?}"),
1627 Sort::BitVec(w) => write!(f, "bitvec({w})"),
1628 Sort::Loc => write!(f, "loc"),
1629 Sort::Func(fsort) => write!(f, "{fsort:?}"),
1630 Sort::SortOf(bty) => write!(f, "<{bty:?}>::sort"),
1631 Sort::Infer => write!(f, "_"),
1632 Sort::Err(_) => write!(f, "err"),
1633 }
1634 }
1635}
1636
1637impl fmt::Debug for SortPath<'_> {
1638 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1639 write!(f, "{:?}", self.res)?;
1640 if !self.args.is_empty() {
1641 write!(f, "<{:?}>", self.args.iter().format(", "))?;
1642 }
1643 Ok(())
1644 }
1645}
1646
1647impl fmt::Debug for SortRes {
1648 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1649 match self {
1650 SortRes::PrimSort(PrimSort::Bool) => write!(f, "bool"),
1651 SortRes::PrimSort(PrimSort::Int) => write!(f, "int"),
1652 SortRes::PrimSort(PrimSort::Real) => write!(f, "real"),
1653 SortRes::PrimSort(PrimSort::Char) => write!(f, "char"),
1654 SortRes::PrimSort(PrimSort::Str) => write!(f, "str"),
1655 SortRes::PrimSort(PrimSort::Set) => write!(f, "Set"),
1656 SortRes::PrimSort(PrimSort::Map) => write!(f, "Map"),
1657 SortRes::SortParam(n) => write!(f, "@{n}"),
1658 SortRes::TyParam(def_id) => write!(f, "{}::sort", def_id_to_string(*def_id)),
1659 SortRes::SelfParam { trait_id } => {
1660 write!(f, "{}::Self::sort", def_id_to_string(*trait_id))
1661 }
1662 SortRes::SelfAlias { alias_to } => {
1663 write!(f, "{}::Self::sort", def_id_to_string(*alias_to))
1664 }
1665 SortRes::SelfParamAssoc { ident: assoc, .. } => {
1666 write!(f, "Self::{assoc}")
1667 }
1668 SortRes::User { name } => write!(f, "{name}"),
1669 SortRes::Adt(def_id) => write!(f, "{}::sort", def_id_to_string(*def_id)),
1670 }
1671 }
1672}
1673
1674impl fmt::Debug for PolyFuncSort<'_> {
1675 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1676 if self.params > 0 {
1677 write!(f, "for<{}>{:?}", self.params, self.fsort)
1678 } else {
1679 write!(f, "{:?}", self.fsort)
1680 }
1681 }
1682}
1683
1684impl fmt::Debug for FuncSort<'_> {
1685 fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1686 match self.inputs() {
1687 [input] => {
1688 write!(f, "{:?} -> {:?}", input, self.output())
1689 }
1690 inputs => {
1691 write!(f, "({:?}) -> {:?}", inputs.iter().format(", "), self.output())
1692 }
1693 }
1694 }
1695}