flux_middle/
fhir.rs

1//! Flux High-Level Intermediate Representation
2//!
3//! The fhir corresponds to the desugared version of source level flux annotations. The main
4//! difference with the surface syntax is that the list of refinement parameters is explicit
5//! in fhir. For example, the following signature
6//!
7//! `fn(x: &strg i32[@n]) ensures x: i32[n + 1]`
8//!
9//! desugars to
10//!
11//! `for<n: int, l: loc> fn(&strg<l: i32[n]>) ensures l: i32[n + 1]`.
12//!
13//! The name fhir is borrowed (pun intended) from rustc's hir to refer to something a bit lower
14//! than the surface syntax.
15
16pub 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    NoPanic,
53}
54
55#[derive(Clone, Copy, Default)]
56pub struct AttrMap<'fhir> {
57    pub attrs: &'fhir [Attr],
58    pub qualifiers: &'fhir [FluxLocalDefId],
59    pub reveals: &'fhir [FluxDefId],
60}
61
62impl AttrMap<'_> {
63    pub(crate) fn proven_externally(&self) -> bool {
64        self.attrs
65            .iter()
66            .any(|attr| matches!(attr, Attr::ProvenExternally))
67    }
68
69    pub(crate) fn ignored(&self) -> Option<Ignored> {
70        self.attrs
71            .iter()
72            .find_map(|attr| if let Attr::Ignore(ignored) = *attr { Some(ignored) } else { None })
73    }
74
75    pub(crate) fn trusted(&self) -> Option<Trusted> {
76        self.attrs
77            .iter()
78            .find_map(|attr| if let Attr::Trusted(trusted) = *attr { Some(trusted) } else { None })
79    }
80
81    pub(crate) fn trusted_impl(&self) -> Option<Trusted> {
82        self.attrs.iter().find_map(|attr| {
83            if let Attr::TrustedImpl(trusted) = *attr { Some(trusted) } else { None }
84        })
85    }
86
87    pub(crate) fn should_fail(&self) -> bool {
88        self.attrs
89            .iter()
90            .any(|attr| matches!(attr, Attr::ShouldFail))
91    }
92
93    pub(crate) fn infer_opts(&self) -> Option<PartialInferOpts> {
94        self.attrs
95            .iter()
96            .find_map(|attr| if let Attr::InferOpts(opts) = *attr { Some(opts) } else { None })
97    }
98
99    pub(crate) fn no_panic(&self) -> bool {
100        self.attrs.iter().any(|attr| matches!(attr, Attr::NoPanic))
101    }
102}
103
104#[derive(Debug, Clone, Copy)]
105pub struct Generics<'fhir> {
106    pub params: &'fhir [GenericParam<'fhir>],
107    pub refinement_params: &'fhir [RefineParam<'fhir>],
108    pub predicates: Option<&'fhir [WhereBoundPredicate<'fhir>]>,
109}
110
111#[derive(Debug, Clone, Copy)]
112pub struct GenericParam<'fhir> {
113    pub def_id: MaybeExternId,
114    pub name: ParamName,
115    pub kind: GenericParamKind<'fhir>,
116}
117
118#[derive(Debug, Clone, Copy)]
119pub enum GenericParamKind<'fhir> {
120    Type { default: Option<Ty<'fhir>> },
121    Lifetime,
122    Const { ty: Ty<'fhir> },
123}
124
125#[derive(Debug)]
126pub struct Qualifier<'fhir> {
127    pub def_id: FluxLocalDefId,
128    pub args: &'fhir [RefineParam<'fhir>],
129    pub expr: Expr<'fhir>,
130    pub global: bool,
131}
132
133#[derive(Clone, Copy, Debug)]
134pub enum Node<'fhir> {
135    Item(&'fhir Item<'fhir>),
136    TraitItem(&'fhir TraitItem<'fhir>),
137    ImplItem(&'fhir ImplItem<'fhir>),
138    OpaqueTy(&'fhir OpaqueTy<'fhir>),
139    ForeignItem(&'fhir ForeignItem<'fhir>),
140    Ctor,
141    AnonConst,
142    Expr,
143}
144
145impl<'fhir> Node<'fhir> {
146    pub fn as_owner(self) -> Option<OwnerNode<'fhir>> {
147        match self {
148            Node::Item(item) => Some(OwnerNode::Item(item)),
149            Node::TraitItem(trait_item) => Some(OwnerNode::TraitItem(trait_item)),
150            Node::ImplItem(impl_item) => Some(OwnerNode::ImplItem(impl_item)),
151            Node::ForeignItem(foreign_item) => Some(OwnerNode::ForeignItem(foreign_item)),
152            Node::OpaqueTy(_) | Node::AnonConst | Node::Expr | Node::Ctor => None,
153        }
154    }
155
156    pub fn expect_opaque_ty(&self) -> &'fhir OpaqueTy<'fhir> {
157        if let Node::OpaqueTy(opaque_ty) = &self { opaque_ty } else { bug!("expected opaque type") }
158    }
159}
160
161#[derive(Clone, Copy, Debug)]
162pub enum OwnerNode<'fhir> {
163    Item(&'fhir Item<'fhir>),
164    TraitItem(&'fhir TraitItem<'fhir>),
165    ImplItem(&'fhir ImplItem<'fhir>),
166    ForeignItem(&'fhir ForeignItem<'fhir>),
167}
168
169impl<'fhir> OwnerNode<'fhir> {
170    pub fn fn_sig(&self) -> Option<&'fhir FnSig<'fhir>> {
171        match self {
172            OwnerNode::Item(Item { kind: ItemKind::Fn(fn_sig, ..), .. })
173            | OwnerNode::TraitItem(TraitItem { kind: TraitItemKind::Fn(fn_sig), .. })
174            | OwnerNode::ImplItem(ImplItem { kind: ImplItemKind::Fn(fn_sig), .. })
175            | OwnerNode::ForeignItem(ForeignItem {
176                kind: ForeignItemKind::Fn(fn_sig, ..), ..
177            }) => Some(fn_sig),
178            _ => None,
179        }
180    }
181
182    pub fn generics(self) -> &'fhir Generics<'fhir> {
183        match self {
184            OwnerNode::Item(item) => &item.generics,
185            OwnerNode::TraitItem(trait_item) => &trait_item.generics,
186            OwnerNode::ImplItem(impl_item) => &impl_item.generics,
187            OwnerNode::ForeignItem(foreign_item) => {
188                match foreign_item.kind {
189                    ForeignItemKind::Fn(_, generics) => generics,
190                }
191            }
192        }
193    }
194
195    pub fn owner_id(&self) -> MaybeExternId<OwnerId> {
196        match self {
197            OwnerNode::Item(item) => item.owner_id,
198            OwnerNode::TraitItem(trait_item) => trait_item.owner_id,
199            OwnerNode::ImplItem(impl_item) => impl_item.owner_id,
200            OwnerNode::ForeignItem(foreign_item) => foreign_item.owner_id,
201        }
202    }
203}
204
205#[derive(Debug)]
206pub struct Item<'fhir> {
207    pub owner_id: MaybeExternId<OwnerId>,
208    pub generics: Generics<'fhir>,
209    pub kind: ItemKind<'fhir>,
210}
211
212impl<'fhir> Item<'fhir> {
213    pub fn expect_enum(&self) -> &EnumDef<'fhir> {
214        if let ItemKind::Enum(enum_def) = &self.kind { enum_def } else { bug!("expected enum") }
215    }
216
217    pub fn expect_struct(&self) -> &StructDef<'fhir> {
218        if let ItemKind::Struct(struct_def) = &self.kind {
219            struct_def
220        } else {
221            bug!("expected struct")
222        }
223    }
224
225    pub fn expect_type_alias(&self) -> &TyAlias<'fhir> {
226        if let ItemKind::TyAlias(ty_alias) = &self.kind {
227            ty_alias
228        } else {
229            bug!("expected type alias")
230        }
231    }
232
233    pub fn expect_impl(&self) -> &Impl<'fhir> {
234        if let ItemKind::Impl(impl_) = &self.kind { impl_ } else { bug!("expected impl") }
235    }
236
237    pub fn expect_trait(&self) -> &Trait<'fhir> {
238        if let ItemKind::Trait(trait_) = &self.kind { trait_ } else { bug!("expected trait") }
239    }
240}
241
242#[derive(Debug)]
243pub enum ItemKind<'fhir> {
244    Enum(EnumDef<'fhir>),
245    Struct(StructDef<'fhir>),
246    TyAlias(&'fhir TyAlias<'fhir>),
247    Trait(Trait<'fhir>),
248    Impl(Impl<'fhir>),
249    Fn(FnSig<'fhir>),
250    Const(Option<Expr<'fhir>>),
251}
252
253#[derive(Debug)]
254pub struct TraitItem<'fhir> {
255    pub owner_id: MaybeExternId<OwnerId>,
256    pub generics: Generics<'fhir>,
257    pub kind: TraitItemKind<'fhir>,
258}
259
260#[derive(Debug)]
261pub enum TraitItemKind<'fhir> {
262    Fn(FnSig<'fhir>),
263    Const,
264    Type,
265}
266
267#[derive(Debug)]
268pub struct ImplItem<'fhir> {
269    pub owner_id: MaybeExternId<OwnerId>,
270    pub kind: ImplItemKind<'fhir>,
271    pub generics: Generics<'fhir>,
272}
273
274#[derive(Debug)]
275pub enum ImplItemKind<'fhir> {
276    Fn(FnSig<'fhir>),
277    Const,
278    Type,
279}
280
281#[derive(Copy, Clone, Debug)]
282pub enum FluxItem<'fhir> {
283    Qualifier(&'fhir Qualifier<'fhir>),
284    Func(&'fhir SpecFunc<'fhir>),
285    PrimOpProp(&'fhir PrimOpProp<'fhir>),
286    SortDecl(&'fhir SortDecl),
287}
288
289impl FluxItem<'_> {
290    pub fn def_id(self) -> FluxLocalDefId {
291        match self {
292            FluxItem::Qualifier(qualifier) => qualifier.def_id,
293            FluxItem::Func(func) => func.def_id,
294            FluxItem::PrimOpProp(prop) => prop.def_id,
295            FluxItem::SortDecl(sort_decl) => sort_decl.def_id,
296        }
297    }
298}
299
300#[derive(Debug)]
301pub struct ForeignItem<'fhir> {
302    pub ident: Ident,
303    pub kind: ForeignItemKind<'fhir>,
304    pub owner_id: MaybeExternId<OwnerId>,
305    pub span: Span,
306}
307
308#[derive(Debug)]
309pub enum ForeignItemKind<'fhir> {
310    Fn(FnSig<'fhir>, &'fhir Generics<'fhir>),
311}
312
313#[derive(Debug, Clone, Copy)]
314pub struct SortDecl {
315    pub def_id: FluxLocalDefId,
316    pub params: usize,
317    pub span: Span,
318}
319
320pub type SortDecls = FxHashMap<Symbol, SortDecl>;
321
322#[derive(Debug, Clone, Copy)]
323pub struct WhereBoundPredicate<'fhir> {
324    pub span: Span,
325    pub bounded_ty: Ty<'fhir>,
326    pub bounds: GenericBounds<'fhir>,
327}
328
329pub type GenericBounds<'fhir> = &'fhir [GenericBound<'fhir>];
330
331#[derive(Debug, Clone, Copy)]
332pub enum GenericBound<'fhir> {
333    Trait(PolyTraitRef<'fhir>),
334    Outlives(Lifetime),
335}
336
337#[derive(Debug, Clone, Copy)]
338pub struct PolyTraitRef<'fhir> {
339    pub bound_generic_params: &'fhir [GenericParam<'fhir>],
340    /// To represent binders for closures i.e. in Fn* traits; see tests/pos/surface/closure{07,08,09,10}.rs
341    pub refine_params: &'fhir [RefineParam<'fhir>],
342    pub modifiers: TraitBoundModifier,
343    pub trait_ref: Path<'fhir>,
344    pub span: Span,
345}
346
347#[derive(Debug, Copy, Clone)]
348pub enum TraitBoundModifier {
349    None,
350    Maybe,
351}
352
353#[derive(Debug)]
354pub struct Trait<'fhir> {
355    pub assoc_refinements: &'fhir [TraitAssocReft<'fhir>],
356}
357
358impl<'fhir> Trait<'fhir> {
359    pub fn find_assoc_reft(&self, name: Symbol) -> Option<&'fhir TraitAssocReft<'fhir>> {
360        self.assoc_refinements
361            .iter()
362            .find(|assoc_reft| assoc_reft.name == name)
363    }
364}
365
366#[derive(Debug, Clone, Copy)]
367pub struct TraitAssocReft<'fhir> {
368    pub name: Symbol,
369    pub params: &'fhir [RefineParam<'fhir>],
370    pub output: Sort<'fhir>,
371    pub body: Option<Expr<'fhir>>,
372    pub span: Span,
373    pub final_: bool,
374}
375
376#[derive(Debug)]
377pub struct Impl<'fhir> {
378    pub assoc_refinements: &'fhir [ImplAssocReft<'fhir>],
379}
380
381impl<'fhir> Impl<'fhir> {
382    pub fn find_assoc_reft(&self, name: Symbol) -> Option<&'fhir ImplAssocReft<'fhir>> {
383        self.assoc_refinements
384            .iter()
385            .find(|assoc_reft| assoc_reft.name == name)
386    }
387}
388
389#[derive(Clone, Copy, Debug)]
390pub struct ImplAssocReft<'fhir> {
391    pub name: Symbol,
392    pub params: &'fhir [RefineParam<'fhir>],
393    pub output: Sort<'fhir>,
394    pub body: Expr<'fhir>,
395    pub span: Span,
396}
397
398#[derive(Debug)]
399pub struct OpaqueTy<'fhir> {
400    pub def_id: MaybeExternId,
401    pub bounds: GenericBounds<'fhir>,
402}
403
404pub type Arena = bumpalo::Bump;
405
406/// A map between rust definitions and flux annotations in their desugared `fhir` form.
407///
408/// note: most items in this struct have been moved out into their own query or method in genv.
409/// We should eventually get rid of this or change its name.
410#[derive(Default)]
411pub struct FluxItems<'fhir> {
412    pub items: FxIndexMap<FluxLocalDefId, FluxItem<'fhir>>,
413}
414
415impl FluxItems<'_> {
416    pub fn new() -> Self {
417        Self { items: Default::default() }
418    }
419}
420
421#[derive(Debug)]
422pub struct TyAlias<'fhir> {
423    pub index: Option<RefineParam<'fhir>>,
424    pub ty: Ty<'fhir>,
425    pub span: Span,
426    /// Whether this alias was lifted from a `hir` alias
427    pub lifted: bool,
428}
429
430#[derive(Debug, Clone, Copy)]
431pub struct StructDef<'fhir> {
432    pub refinement: &'fhir RefinementKind<'fhir>,
433    pub params: &'fhir [RefineParam<'fhir>],
434    pub kind: StructKind<'fhir>,
435    pub invariants: &'fhir [Expr<'fhir>],
436}
437
438#[derive(Debug, Clone, Copy)]
439pub enum StructKind<'fhir> {
440    Transparent { fields: &'fhir [FieldDef<'fhir>] },
441    Opaque,
442}
443
444#[derive(Debug, Clone, Copy)]
445pub struct FieldDef<'fhir> {
446    pub ty: Ty<'fhir>,
447    /// Whether this field was lifted from a `hir` field
448    pub lifted: bool,
449}
450
451#[derive(Debug)]
452pub enum RefinementKind<'fhir> {
453    /// User specified indices (e.g. length, elems, etc.)
454    Refined(RefinedBy<'fhir>),
455    /// Singleton refinements e.g. `State[On]`, `State[Off]`
456    Reflected,
457}
458
459impl RefinementKind<'_> {
460    pub fn is_reflected(&self) -> bool {
461        matches!(self, RefinementKind::Reflected)
462    }
463}
464
465#[derive(Debug)]
466pub struct EnumDef<'fhir> {
467    pub refinement: &'fhir RefinementKind<'fhir>,
468    pub params: &'fhir [RefineParam<'fhir>],
469    pub variants: &'fhir [VariantDef<'fhir>],
470    pub invariants: &'fhir [Expr<'fhir>],
471}
472
473#[derive(Debug, Clone, Copy)]
474pub struct VariantDef<'fhir> {
475    pub def_id: LocalDefId,
476    pub params: &'fhir [RefineParam<'fhir>],
477    pub fields: &'fhir [FieldDef<'fhir>],
478    pub ret: VariantRet<'fhir>,
479    pub span: Span,
480    /// Whether this variant was lifted from a hir variant
481    pub lifted: bool,
482}
483
484#[derive(Debug, Clone, Copy)]
485pub struct VariantRet<'fhir> {
486    pub enum_id: DefId,
487    pub idx: Expr<'fhir>,
488}
489
490#[derive(Clone, Copy)]
491pub struct FnDecl<'fhir> {
492    pub requires: &'fhir [Requires<'fhir>],
493    pub inputs: &'fhir [Ty<'fhir>],
494    pub output: FnOutput<'fhir>,
495    pub span: Span,
496    /// Whether the sig was lifted from a hir signature
497    pub lifted: bool,
498}
499
500/// A predicate required to hold before calling a function.
501#[derive(Clone, Copy)]
502pub struct Requires<'fhir> {
503    /// An (optional) list of universally quantified parameters
504    pub params: &'fhir [RefineParam<'fhir>],
505    pub pred: Expr<'fhir>,
506}
507
508#[derive(Clone, Copy)]
509pub struct FnSig<'fhir> {
510    pub header: FnHeader,
511    pub decl: &'fhir FnDecl<'fhir>,
512}
513
514#[derive(Clone, Copy)]
515pub struct FnOutput<'fhir> {
516    pub params: &'fhir [RefineParam<'fhir>],
517    pub ret: Ty<'fhir>,
518    pub ensures: &'fhir [Ensures<'fhir>],
519}
520
521#[derive(Clone, Copy)]
522pub enum Ensures<'fhir> {
523    /// A type constraint on a location
524    Type(PathExpr<'fhir>, &'fhir Ty<'fhir>),
525    /// A predicate that needs to hold on function exit
526    Pred(Expr<'fhir>),
527}
528
529#[derive(Clone, Copy)]
530pub struct Ty<'fhir> {
531    pub kind: TyKind<'fhir>,
532    pub span: Span,
533}
534
535#[derive(Clone, Copy)]
536pub enum TyKind<'fhir> {
537    /// A type that parses as a [`BaseTy`] but was written without refinements. Most types in
538    /// this category are base types and will be converted into an [existential], e.g., `i32` is
539    /// converted into `∃v:int. i32[v]`. However, this category also contains generic variables
540    /// of kind [type]. We cannot distinguish these syntactially so we resolve them later in the
541    /// analysis.
542    ///
543    /// [existential]: crate::rty::TyKind::Exists
544    /// [type]: GenericParamKind::Type
545    BaseTy(BaseTy<'fhir>),
546    Indexed(BaseTy<'fhir>, Expr<'fhir>),
547    Exists(&'fhir [RefineParam<'fhir>], &'fhir Ty<'fhir>),
548    /// Constrained types `{T | p}` are like existentials but without binders, and are useful
549    /// for specifying constraints on indexed values e.g. `{i32[@a] | 0 <= a}`
550    Constr(Expr<'fhir>, &'fhir Ty<'fhir>),
551    StrgRef(Lifetime, &'fhir PathExpr<'fhir>, &'fhir Ty<'fhir>),
552    Ref(Lifetime, MutTy<'fhir>),
553    BareFn(&'fhir BareFnTy<'fhir>),
554    Tuple(&'fhir [Ty<'fhir>]),
555    Array(&'fhir Ty<'fhir>, ConstArg),
556    RawPtr(&'fhir Ty<'fhir>, Mutability),
557    OpaqueDef(&'fhir OpaqueTy<'fhir>),
558    TraitObject(&'fhir [PolyTraitRef<'fhir>], Lifetime, TraitObjectSyntax),
559    Never,
560    Infer,
561    Err(ErrorGuaranteed),
562}
563
564pub struct BareFnTy<'fhir> {
565    pub safety: Safety,
566    pub abi: rustc_abi::ExternAbi,
567    pub generic_params: &'fhir [GenericParam<'fhir>],
568    pub decl: &'fhir FnDecl<'fhir>,
569    pub param_idents: &'fhir [Option<Ident>],
570}
571
572#[derive(Clone, Copy)]
573pub struct MutTy<'fhir> {
574    pub ty: &'fhir Ty<'fhir>,
575    pub mutbl: Mutability,
576}
577
578/// Our surface syntax doesn't have lifetimes. To deal with them we create a *hole* for every lifetime
579/// which we then resolve when we check for structural compatibility against the rust type.
580#[derive(Copy, Clone, PartialEq, Eq)]
581pub enum Lifetime {
582    /// A lifetime hole created during desugaring.
583    Hole(FhirId),
584    /// A resolved lifetime created during lifting.
585    Resolved(ResolvedArg),
586}
587
588/// Owner version of [`FluxLocalDefId`]
589#[derive(Debug, Copy, Clone, Hash, PartialEq, Eq, Encodable, Decodable)]
590pub enum FluxOwnerId {
591    Flux(FluxLocalDefId),
592    Rust(OwnerId),
593}
594
595impl FluxOwnerId {
596    pub fn def_id(self) -> Option<LocalDefId> {
597        match self {
598            FluxOwnerId::Flux(_) => None,
599            FluxOwnerId::Rust(owner_id) => Some(owner_id.def_id),
600        }
601    }
602}
603
604/// A unique identifier for a node in the AST. Like [`HirId`] it is composed of an `owner` and a
605/// `local_id`. We don't generate ids for all nodes, but only for those we need to remember
606/// information elaborated during well-formedness checking to later be used during conversion into
607/// [`rty`].
608///
609/// [`rty`]: crate::rty
610/// [`HirId`]: rustc_hir::HirId
611#[derive(Debug, Hash, PartialEq, Eq, Copy, Clone, Encodable, Decodable)]
612pub struct FhirId {
613    pub owner: FluxOwnerId,
614    pub local_id: ItemLocalId,
615}
616
617newtype_index! {
618    /// An `ItemLocalId` uniquely identifies something within a given "item-like".
619    #[encodable]
620    pub struct ItemLocalId {}
621}
622
623/// These are types of things that may be refined with indices or existentials
624#[derive(Clone, Copy)]
625pub struct BaseTy<'fhir> {
626    pub kind: BaseTyKind<'fhir>,
627    pub fhir_id: FhirId,
628    pub span: Span,
629}
630
631impl<'fhir> BaseTy<'fhir> {
632    pub fn from_qpath(qpath: QPath<'fhir>, fhir_id: FhirId) -> Self {
633        let span = qpath.span();
634        Self { kind: BaseTyKind::Path(qpath), fhir_id, span }
635    }
636
637    fn as_path(&self) -> Option<Path<'fhir>> {
638        match self.kind {
639            BaseTyKind::Path(QPath::Resolved(None, path)) => Some(path),
640            _ => None,
641        }
642    }
643}
644
645#[derive(Clone, Copy)]
646pub enum BaseTyKind<'fhir> {
647    Path(QPath<'fhir>),
648    Slice(&'fhir Ty<'fhir>),
649    Err(ErrorGuaranteed),
650}
651
652#[derive(Clone, Copy)]
653pub enum QPath<'fhir> {
654    Resolved(Option<&'fhir Ty<'fhir>>, Path<'fhir>),
655    TypeRelative(&'fhir Ty<'fhir>, &'fhir PathSegment<'fhir>),
656}
657
658#[derive(Clone, Copy)]
659pub struct Path<'fhir> {
660    pub res: Res,
661    pub fhir_id: FhirId,
662    pub segments: &'fhir [PathSegment<'fhir>],
663    pub refine: &'fhir [Expr<'fhir>],
664    pub span: Span,
665}
666
667impl<'fhir> Path<'fhir> {
668    pub fn last_segment(&self) -> &'fhir PathSegment<'fhir> {
669        self.segments.last().unwrap()
670    }
671}
672
673#[derive(Clone, Copy)]
674pub struct PathSegment<'fhir> {
675    pub ident: Ident,
676    pub res: Res,
677    pub args: &'fhir [GenericArg<'fhir>],
678    pub constraints: &'fhir [AssocItemConstraint<'fhir>],
679}
680
681#[derive(Clone, Copy)]
682pub struct AssocItemConstraint<'fhir> {
683    pub ident: Ident,
684    pub kind: AssocItemConstraintKind<'fhir>,
685}
686
687#[derive(Clone, Copy)]
688pub enum AssocItemConstraintKind<'fhir> {
689    Equality { term: Ty<'fhir> },
690}
691
692#[derive(Clone, Copy)]
693pub enum GenericArg<'fhir> {
694    Lifetime(Lifetime),
695    Type(&'fhir Ty<'fhir>),
696    Const(ConstArg),
697    Infer,
698}
699
700impl<'fhir> GenericArg<'fhir> {
701    pub fn expect_type(&self) -> &'fhir Ty<'fhir> {
702        if let GenericArg::Type(ty) = self { ty } else { bug!("expected `GenericArg::Type`") }
703    }
704}
705
706#[derive(PartialEq, Eq, Clone, Copy)]
707pub struct ConstArg {
708    pub kind: ConstArgKind,
709    pub span: Span,
710}
711
712#[derive(PartialEq, Eq, Clone, Copy)]
713pub enum ConstArgKind {
714    Lit(usize),
715    Param(DefId),
716    Infer,
717}
718
719/// The resolution of a path
720///
721/// The enum contains a subset of the variants in [`rustc_hir::def::Res`] plus some extra variants
722/// for stuff refinements resolve to.
723#[derive(Eq, PartialEq, Debug, Copy, Clone)]
724pub enum Res<Id = !> {
725    /// See [`rustc_hir::def::Res::Def`]
726    Def(DefKind, DefId),
727    /// See [`rustc_hir::def::Res::PrimTy`]
728    PrimTy(PrimTy),
729    /// See [`rustc_hir::def::Res::SelfTyAlias`]
730    SelfTyAlias {
731        alias_to: DefId,
732        is_trait_impl: bool,
733    },
734    /// See [`rustc_hir::def::Res::SelfTyParam`]
735    SelfTyParam {
736        trait_: DefId,
737    },
738    /// A refinement parameter, e.g., declared with `@n` syntax
739    Param(ParamKind, Id),
740    /// A refinement function defined with `flux::defs! { ... }`
741    GlobalFunc(SpecFuncKind),
742    Err,
743}
744
745/// See [`rustc_hir::def::PartialRes`]
746#[derive(Copy, Clone, Debug)]
747pub struct PartialRes<Id = !> {
748    base_res: Res<Id>,
749    unresolved_segments: usize,
750}
751
752impl<Id: Copy> PartialRes<Id> {
753    pub fn new(base_res: Res<Id>) -> Self {
754        Self { base_res, unresolved_segments: 0 }
755    }
756
757    pub fn with_unresolved_segments(base_res: Res<Id>, unresolved_segments: usize) -> Self {
758        Self { base_res, unresolved_segments }
759    }
760
761    #[inline]
762    pub fn base_res(&self) -> Res<Id> {
763        self.base_res
764    }
765
766    pub fn unresolved_segments(&self) -> usize {
767        self.unresolved_segments
768    }
769
770    #[inline]
771    pub fn full_res(&self) -> Option<Res<Id>> {
772        (self.unresolved_segments == 0).then_some(self.base_res)
773    }
774
775    #[inline]
776    pub fn expect_full_res(&self) -> Res<Id> {
777        self.full_res().unwrap_or_else(|| bug!("expected full res"))
778    }
779
780    pub fn is_box(&self, tcx: TyCtxt) -> bool {
781        self.full_res().is_some_and(|res| res.is_box(tcx))
782    }
783
784    pub fn map_param_id<R>(&self, f: impl FnOnce(Id) -> R) -> PartialRes<R> {
785        PartialRes {
786            base_res: self.base_res.map_param_id(f),
787            unresolved_segments: self.unresolved_segments,
788        }
789    }
790}
791
792#[derive(Debug, Clone, Copy)]
793pub struct RefineParam<'fhir> {
794    pub id: ParamId,
795    pub name: Symbol,
796    pub span: Span,
797    pub sort: Sort<'fhir>,
798    pub kind: ParamKind,
799    pub fhir_id: FhirId,
800}
801
802/// How a parameter was declared in the surface syntax.
803#[derive(PartialEq, Eq, Debug, Clone, Copy)]
804pub enum ParamKind {
805    /// A parameter declared in an explicit scope, e.g., `fn foo[hdl n: int](x: i32[n])`
806    Explicit(Option<ParamMode>),
807    /// An implicitly scoped parameter declared with `@a` syntax
808    At,
809    /// An implicitly scoped parameter declared with `#a` syntax
810    Pound,
811    /// An implicitly scoped parameter declared with `x: T` syntax.
812    Colon,
813    /// A location declared with `x: &strg T` syntax.
814    Loc,
815    /// A parameter introduced with `x: T` syntax that we know *syntactically* is always and error
816    /// to use inside a refinement. For example, consider the following:
817    /// ```ignore
818    /// fn(x: {v. i32[v] | v > 0}) -> i32[x]
819    /// ```
820    /// In this definition, we know syntactically that `x` binds to a non-base type so it's an error
821    /// to use `x` as an index in the return type.
822    ///
823    /// These parameters should not appear in a desugared item and we only track them during name
824    /// resolution to report errors at the use site.
825    Error,
826}
827
828impl ParamKind {
829    pub fn is_loc(&self) -> bool {
830        matches!(self, ParamKind::Loc)
831    }
832}
833
834/// *Infer*ence *mode* for a parameter.
835#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
836pub enum InferMode {
837    /// Generate a fresh evar for the parameter and solve it via syntactic unification. The parameter
838    /// must appear at least once as an index for unification to succeed, but otherwise it can appear
839    /// (mostly) freely.
840    EVar,
841    /// Generate a fresh kvar and let fixpoint infer it. This mode can only be used with abstract
842    /// refinement predicates. If the parameter is marked as kvar then it can only appear in
843    /// positions that will result in a _horn_ constraint as required by fixpoint.
844    KVar,
845}
846
847impl InferMode {
848    pub fn from_param_kind(kind: ParamKind) -> InferMode {
849        if let ParamKind::Explicit(Some(ParamMode::Horn)) = kind {
850            InferMode::KVar
851        } else {
852            InferMode::EVar
853        }
854    }
855
856    pub fn prefix_str(self) -> &'static str {
857        match self {
858            InferMode::EVar => "?",
859            InferMode::KVar => "$",
860        }
861    }
862}
863
864#[derive(Clone, Copy)]
865pub enum PrimSort {
866    Int,
867    Bool,
868    Char,
869    Real,
870    Set,
871    Map,
872    Str,
873}
874
875impl PrimSort {
876    pub fn name_str(self) -> &'static str {
877        match self {
878            PrimSort::Int => "int",
879            PrimSort::Str => "str",
880            PrimSort::Bool => "bool",
881            PrimSort::Char => "char",
882            PrimSort::Real => "real",
883            PrimSort::Set => "Set",
884            PrimSort::Map => "Map",
885        }
886    }
887
888    /// Number of generics expected by this primitive sort
889    pub fn generics(self) -> usize {
890        match self {
891            PrimSort::Int | PrimSort::Bool | PrimSort::Real | PrimSort::Char | PrimSort::Str => 0,
892            PrimSort::Set => 1,
893            PrimSort::Map => 2,
894        }
895    }
896}
897
898#[derive(Clone, Copy)]
899pub enum SortRes {
900    /// A primitive sort.
901    PrimSort(PrimSort),
902    /// A user declared sort.
903    User(FluxDefId),
904    /// A sort parameter inside a polymorphic function or data sort.
905    SortParam(usize),
906    /// The sort associated to a (generic) type parameter
907    TyParam(DefId),
908    /// The sort of the `Self` type, as used within a trait.
909    SelfParam {
910        /// The trait this `Self` is a generic parameter for.
911        trait_id: DefId,
912    },
913    /// The sort of a `Self` type, as used somewhere other than within a trait.
914    SelfAlias {
915        /// The item introducing the `Self` type alias, e.g., an impl block.
916        alias_to: DefId,
917    },
918    /// The sort of an associated type in a trait declaration, e.g:
919    ///
920    /// ```ignore
921    /// #[assoc(fn assoc_reft(x: Self::Assoc) -> bool)]
922    /// trait MyTrait {
923    ///     type Assoc;
924    /// }
925    /// ```
926    SelfParamAssoc { trait_id: DefId, ident: Ident },
927    /// The sort automatically generated for an adt (enum/struct) with a `flux::refined_by` annotation
928    Adt(DefId),
929}
930
931#[derive(Clone, Copy)]
932pub enum Sort<'fhir> {
933    Path(SortPath<'fhir>),
934    /// The sort of a location parameter introduced with the `x: &strg T` syntax.
935    Loc,
936    /// A bit vector with the given width.
937    BitVec(u32),
938    /// A polymorphic sort function.
939    Func(PolyFuncSort<'fhir>),
940    /// The sort associated with a base type. This is normalized into a concrete sort during
941    /// conversion
942    SortOf(BaseTy<'fhir>),
943    /// A sort that needs to be inferred.
944    Infer,
945    Err(ErrorGuaranteed),
946}
947
948/// See [`flux_syntax::surface::SortPath`]
949#[derive(Clone, Copy)]
950pub struct SortPath<'fhir> {
951    pub res: SortRes,
952    pub segments: &'fhir [Ident],
953    pub args: &'fhir [Sort<'fhir>],
954}
955
956#[derive(Clone, Copy)]
957pub struct FuncSort<'fhir> {
958    /// inputs and output in order
959    pub inputs_and_output: &'fhir [Sort<'fhir>],
960}
961
962#[derive(Clone, Copy)]
963pub struct PolyFuncSort<'fhir> {
964    pub params: usize,
965    pub fsort: FuncSort<'fhir>,
966}
967
968impl<'fhir> PolyFuncSort<'fhir> {
969    pub fn new(params: usize, inputs_and_output: &'fhir [Sort]) -> Self {
970        let fsort = FuncSort { inputs_and_output };
971        Self { params, fsort }
972    }
973}
974
975/// `<qself as path>::name`
976#[derive(Clone, Copy)]
977pub enum AliasReft<'fhir> {
978    /// A fully qualified associated refinement `<qself as trait_>::name`
979    Qualified { qself: &'fhir Ty<'fhir>, trait_: Path<'fhir>, name: Ident },
980    /// A type-relative associated refinement, e.g., `Self::name`. Note that
981    /// we can only resolve this when `ty` is a parameter, similar to how
982    /// type-relative associated types are resolved.
983    TypeRelative { qself: &'fhir Ty<'fhir>, name: Ident },
984}
985
986#[derive(Debug, Clone, Copy)]
987pub struct FieldExpr<'fhir> {
988    pub ident: Ident,
989    pub expr: Expr<'fhir>,
990    pub fhir_id: FhirId,
991    pub span: Span,
992}
993
994#[derive(Debug, Clone, Copy)]
995pub struct Spread<'fhir> {
996    pub expr: Expr<'fhir>,
997    pub span: Span,
998    pub fhir_id: FhirId,
999}
1000
1001#[derive(Clone, Copy)]
1002pub struct Expr<'fhir> {
1003    pub kind: ExprKind<'fhir>,
1004    pub fhir_id: FhirId,
1005    pub span: Span,
1006}
1007
1008#[derive(Clone, Copy, PartialEq, Eq, Hash, Encodable, Decodable)]
1009pub enum QuantKind {
1010    Forall,
1011    Exists,
1012}
1013
1014#[derive(Clone, Copy, PartialEq, Eq, Hash, Debug, Encodable, Decodable)]
1015pub struct Range {
1016    pub start: usize,
1017    pub end: usize,
1018}
1019
1020#[derive(Clone, Copy)]
1021pub enum ExprKind<'fhir> {
1022    Var(QPathExpr<'fhir>),
1023    Dot(&'fhir Expr<'fhir>, Ident),
1024    Literal(Lit),
1025    BinaryOp(BinOp, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1026    UnaryOp(UnOp, &'fhir Expr<'fhir>),
1027    App(PathExpr<'fhir>, &'fhir [Expr<'fhir>]),
1028    /// UIF application representing a primitive operation, e.g. `[<<](x, y)`
1029    PrimApp(BinOp, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1030    Alias(AliasReft<'fhir>, &'fhir [Expr<'fhir>]),
1031    IfThenElse(&'fhir Expr<'fhir>, &'fhir Expr<'fhir>, &'fhir Expr<'fhir>),
1032    Abs(&'fhir [RefineParam<'fhir>], &'fhir Expr<'fhir>),
1033    BoundedQuant(QuantKind, RefineParam<'fhir>, Range, &'fhir Expr<'fhir>),
1034    Record(&'fhir [Expr<'fhir>]),
1035    SetLiteral(&'fhir [Expr<'fhir>]),
1036    Constructor(Option<PathExpr<'fhir>>, &'fhir [FieldExpr<'fhir>], Option<&'fhir Spread<'fhir>>),
1037    Block(&'fhir [LetDecl<'fhir>], &'fhir Expr<'fhir>),
1038    Err(ErrorGuaranteed),
1039}
1040
1041#[derive(Clone, Copy)]
1042pub enum QPathExpr<'fhir> {
1043    Resolved(PathExpr<'fhir>, Option<ParamKind>),
1044    TypeRelative(&'fhir Ty<'fhir>, Ident),
1045}
1046
1047#[derive(Clone, Copy)]
1048pub struct LetDecl<'fhir> {
1049    pub param: RefineParam<'fhir>,
1050    pub init: Expr<'fhir>,
1051}
1052
1053#[derive(Clone, Copy)]
1054pub enum NumLitKind {
1055    Int,
1056    Real,
1057}
1058
1059#[derive(Clone, Copy)]
1060pub enum Lit {
1061    Int(u128, Option<NumLitKind>),
1062    Bool(bool),
1063    Str(Symbol),
1064    Char(char),
1065}
1066
1067#[derive(Clone, Copy)]
1068pub struct PathExpr<'fhir> {
1069    pub segments: &'fhir [Ident],
1070    pub res: Res<ParamId>,
1071    pub fhir_id: FhirId,
1072    pub span: Span,
1073}
1074
1075newtype_index! {
1076    #[debug_format = "a{}"]
1077    pub struct ParamId {}
1078}
1079
1080impl PolyTraitRef<'_> {
1081    pub fn trait_def_id(&self) -> DefId {
1082        let path = &self.trait_ref;
1083        if let Res::Def(DefKind::Trait, did) = path.res {
1084            did
1085        } else {
1086            span_bug!(path.span, "unexpected resolution {:?}", path.res);
1087        }
1088    }
1089}
1090
1091impl From<OwnerId> for FluxOwnerId {
1092    fn from(owner_id: OwnerId) -> Self {
1093        FluxOwnerId::Rust(owner_id)
1094    }
1095}
1096
1097impl<'fhir> Ty<'fhir> {
1098    pub fn as_path(&self) -> Option<Path<'fhir>> {
1099        match &self.kind {
1100            TyKind::BaseTy(bty) => bty.as_path(),
1101            _ => None,
1102        }
1103    }
1104}
1105
1106impl<Id> Res<Id> {
1107    pub fn descr(&self) -> &'static str {
1108        match self {
1109            Res::PrimTy(_) => "builtin type",
1110            Res::Def(kind, def_id) => kind.descr(*def_id),
1111            Res::SelfTyAlias { .. } | Res::SelfTyParam { .. } => "self type",
1112            Res::Param(..) => "refinement parameter",
1113            Res::GlobalFunc(..) => "refinement function",
1114            Res::Err => "unresolved item",
1115        }
1116    }
1117
1118    pub fn is_box(&self, tcx: TyCtxt) -> bool {
1119        if let Res::Def(DefKind::Struct, def_id) = self {
1120            tcx.adt_def(def_id).is_box()
1121        } else {
1122            false
1123        }
1124    }
1125
1126    /// Returns `None` if this is `Res::Err`
1127    pub fn ns(&self) -> Option<Namespace> {
1128        match self {
1129            Res::Def(kind, ..) => kind.ns(),
1130            Res::PrimTy(..) | Res::SelfTyAlias { .. } | Res::SelfTyParam { .. } => {
1131                Some(Namespace::TypeNS)
1132            }
1133            Res::Param(..) | Res::GlobalFunc(..) => Some(Namespace::ValueNS),
1134            Res::Err => None,
1135        }
1136    }
1137
1138    /// Always returns `true` if `self` is `Res::Err`
1139    pub fn matches_ns(&self, ns: Namespace) -> bool {
1140        self.ns().is_none_or(|actual_ns| actual_ns == ns)
1141    }
1142
1143    pub fn map_param_id<R>(self, f: impl FnOnce(Id) -> R) -> Res<R> {
1144        match self {
1145            Res::Param(kind, param_id) => Res::Param(kind, f(param_id)),
1146            Res::Def(def_kind, def_id) => Res::Def(def_kind, def_id),
1147            Res::PrimTy(prim_ty) => Res::PrimTy(prim_ty),
1148            Res::SelfTyAlias { alias_to, is_trait_impl } => {
1149                Res::SelfTyAlias { alias_to, is_trait_impl }
1150            }
1151            Res::SelfTyParam { trait_ } => Res::SelfTyParam { trait_ },
1152            Res::GlobalFunc(spec_func_kind) => Res::GlobalFunc(spec_func_kind),
1153            Res::Err => Res::Err,
1154        }
1155    }
1156
1157    pub fn expect_param(self) -> (ParamKind, Id) {
1158        if let Res::Param(kind, id) = self { (kind, id) } else { bug!("expected param") }
1159    }
1160}
1161
1162impl<Id1, Id2> TryFrom<rustc_hir::def::Res<Id1>> for Res<Id2> {
1163    type Error = ();
1164
1165    fn try_from(res: rustc_hir::def::Res<Id1>) -> Result<Self, Self::Error> {
1166        match res {
1167            rustc_hir::def::Res::Def(kind, did) => Ok(Res::Def(kind, did)),
1168            rustc_hir::def::Res::PrimTy(prim_ty) => Ok(Res::PrimTy(prim_ty)),
1169            rustc_hir::def::Res::SelfTyAlias { alias_to, forbid_generic: false, is_trait_impl } => {
1170                Ok(Res::SelfTyAlias { alias_to, is_trait_impl })
1171            }
1172            rustc_hir::def::Res::SelfTyParam { trait_ } => Ok(Res::SelfTyParam { trait_ }),
1173            rustc_hir::def::Res::Err => Ok(Res::Err),
1174            _ => Err(()),
1175        }
1176    }
1177}
1178
1179impl QPath<'_> {
1180    pub fn span(&self) -> Span {
1181        match self {
1182            QPath::Resolved(_, path) => path.span,
1183            QPath::TypeRelative(qself, assoc) => qself.span.to(assoc.ident.span),
1184        }
1185    }
1186}
1187
1188impl Lit {
1189    pub const TRUE: Lit = Lit::Bool(true);
1190}
1191
1192/// Information about the refinement parameters associated with an adt (struct/enum).
1193#[derive(Clone, Debug)]
1194pub struct RefinedBy<'fhir> {
1195    /// When a `#[flux::refined_by(..)]` annotation mentions generic type parameters we implicitly
1196    /// generate a *polymorphic* data sort.
1197    ///
1198    /// For example, if we have:
1199    /// ```ignore
1200    /// #[refined_by(keys: Set<K>)]
1201    /// RMap<K, V> { ... }
1202    /// ```
1203    /// we implicitly create a data sort of the form `forall #0. { keys: Set<#0> }`, where `#0` is a
1204    /// *sort variable*.
1205    ///
1206    /// This [`FxIndexSet`] is used to track a mapping between sort variables and their corresponding
1207    /// type parameter. The [`DefId`] is the id of the type parameter and its index in the set is the
1208    /// position of the sort variable.
1209    pub sort_params: FxIndexSet<DefId>,
1210    /// Fields indexed by their name in the same order they appear in the `#[refined_by(..)]` annotation.
1211    pub fields: FxIndexMap<Symbol, Sort<'fhir>>,
1212}
1213
1214#[derive(Debug)]
1215pub struct SpecFunc<'fhir> {
1216    pub def_id: FluxLocalDefId,
1217    pub params: usize,
1218    pub args: &'fhir [RefineParam<'fhir>],
1219    pub sort: Sort<'fhir>,
1220    pub body: Option<Expr<'fhir>>,
1221    pub hide: bool,
1222    pub ident_span: Span,
1223}
1224#[derive(Debug)]
1225pub struct PrimOpProp<'fhir> {
1226    pub def_id: FluxLocalDefId,
1227    pub op: BinOp,
1228    pub args: &'fhir [RefineParam<'fhir>],
1229    pub body: Expr<'fhir>,
1230    pub span: Span,
1231}
1232
1233#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
1234pub enum SpecFuncKind {
1235    /// Theory symbols *interpreted* by the SMT solver
1236    Thy(liquid_fixpoint::ThyFunc),
1237    /// User-defined uninterpreted functions with no definition
1238    Uif(FluxDefId),
1239    /// User-defined functions with a body definition
1240    Def(FluxDefId),
1241    /// Casts between sorts: id for char, int; if-then-else for bool-int; uninterpreted otherwise.
1242    Cast,
1243}
1244
1245impl SpecFuncKind {
1246    pub fn def_id(&self) -> Option<FluxDefId> {
1247        match self {
1248            SpecFuncKind::Uif(flux_id) | SpecFuncKind::Def(flux_id) => Some(*flux_id),
1249            _ => None,
1250        }
1251    }
1252}
1253
1254impl<'fhir> Generics<'fhir> {
1255    pub fn get_param(&self, def_id: LocalDefId) -> &'fhir GenericParam<'fhir> {
1256        self.params
1257            .iter()
1258            .find(|p| p.def_id.local_id() == def_id)
1259            .unwrap()
1260    }
1261}
1262
1263impl<'fhir> RefinedBy<'fhir> {
1264    pub fn new(fields: FxIndexMap<Symbol, Sort<'fhir>>, sort_params: FxIndexSet<DefId>) -> Self {
1265        RefinedBy { sort_params, fields }
1266    }
1267
1268    pub fn trivial() -> Self {
1269        RefinedBy { sort_params: Default::default(), fields: Default::default() }
1270    }
1271}
1272
1273impl<'fhir> From<PolyFuncSort<'fhir>> for Sort<'fhir> {
1274    fn from(fsort: PolyFuncSort<'fhir>) -> Self {
1275        Self::Func(fsort)
1276    }
1277}
1278
1279impl FuncSort<'_> {
1280    pub fn inputs(&self) -> &[Sort<'_>] {
1281        &self.inputs_and_output[..self.inputs_and_output.len() - 1]
1282    }
1283
1284    pub fn output(&self) -> &Sort<'_> {
1285        &self.inputs_and_output[self.inputs_and_output.len() - 1]
1286    }
1287}
1288
1289impl rustc_errors::IntoDiagArg for Ty<'_> {
1290    fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1291        rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1292    }
1293}
1294
1295impl rustc_errors::IntoDiagArg for Path<'_> {
1296    fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
1297        rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
1298    }
1299}
1300
1301impl StructDef<'_> {
1302    pub fn is_opaque(&self) -> bool {
1303        matches!(self.kind, StructKind::Opaque)
1304    }
1305}
1306
1307impl fmt::Debug for FnSig<'_> {
1308    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1309        write!(f, "{:?}", self.decl)
1310    }
1311}
1312
1313impl fmt::Debug for FnDecl<'_> {
1314    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1315        if !self.requires.is_empty() {
1316            write!(f, "[{:?}] ", self.requires.iter().format(", "))?;
1317        }
1318        write!(f, "fn({:?}) -> {:?}", self.inputs.iter().format(", "), self.output)
1319    }
1320}
1321
1322impl fmt::Debug for FnOutput<'_> {
1323    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1324        if !self.params.is_empty() {
1325            write!(
1326                f,
1327                "exists<{}> ",
1328                self.params.iter().format_with(", ", |param, f| {
1329                    f(&format_args!("{}: {:?}", param.name, param.sort))
1330                })
1331            )?;
1332        }
1333        write!(f, "{:?}", self.ret)?;
1334        if !self.ensures.is_empty() {
1335            write!(f, "; [{:?}]", self.ensures.iter().format(", "))?;
1336        }
1337
1338        Ok(())
1339    }
1340}
1341
1342impl fmt::Debug for Requires<'_> {
1343    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1344        if !self.params.is_empty() {
1345            write!(
1346                f,
1347                "forall {}.",
1348                self.params.iter().format_with(",", |param, f| {
1349                    f(&format_args!("{}:{:?}", param.name, param.sort))
1350                })
1351            )?;
1352        }
1353        write!(f, "{:?}", self.pred)
1354    }
1355}
1356
1357impl fmt::Debug for Ensures<'_> {
1358    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1359        match self {
1360            Ensures::Type(loc, ty) => write!(f, "{loc:?}: {ty:?}"),
1361            Ensures::Pred(e) => write!(f, "{e:?}"),
1362        }
1363    }
1364}
1365
1366impl fmt::Debug for Ty<'_> {
1367    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1368        match &self.kind {
1369            TyKind::BaseTy(bty) => write!(f, "{bty:?}"),
1370            TyKind::Indexed(bty, idx) => write!(f, "{bty:?}[{idx:?}]"),
1371            TyKind::Exists(params, ty) => {
1372                write!(f, "{{")?;
1373                write!(
1374                    f,
1375                    "{}",
1376                    params.iter().format_with(",", |param, f| {
1377                        f(&format_args!("{}:{:?}", param.name, param.sort))
1378                    })
1379                )?;
1380                if let TyKind::Constr(pred, ty) = &ty.kind {
1381                    write!(f, ". {ty:?} | {pred:?}}}")
1382                } else {
1383                    write!(f, ". {ty:?}}}")
1384                }
1385            }
1386            TyKind::StrgRef(_lft, loc, ty) => write!(f, "&strg <{loc:?}: {ty:?}>"),
1387            TyKind::Ref(_lft, mut_ty) => {
1388                write!(f, "&{}{:?}", mut_ty.mutbl.prefix_str(), mut_ty.ty)
1389            }
1390            TyKind::BareFn(bare_fn_ty) => {
1391                write!(f, "{bare_fn_ty:?}")
1392            }
1393            TyKind::Tuple(tys) => write!(f, "({:?})", tys.iter().format(", ")),
1394            TyKind::Array(ty, len) => write!(f, "[{ty:?}; {len:?}]"),
1395            TyKind::Never => write!(f, "!"),
1396            TyKind::Constr(pred, ty) => write!(f, "{{{ty:?} | {pred:?}}}"),
1397            TyKind::RawPtr(ty, Mutability::Not) => write!(f, "*const {ty:?}"),
1398            TyKind::RawPtr(ty, Mutability::Mut) => write!(f, "*mut {ty:?}"),
1399            TyKind::Infer => write!(f, "_"),
1400            TyKind::OpaqueDef(opaque_ty) => {
1401                write!(f, "impl trait <def_id = {:?}>", opaque_ty.def_id.resolved_id(),)
1402            }
1403            TyKind::TraitObject(poly_traits, _lft, _syntax) => {
1404                write!(f, "dyn {poly_traits:?}")
1405            }
1406            TyKind::Err(_) => write!(f, "err"),
1407        }
1408    }
1409}
1410
1411impl fmt::Debug for BareFnTy<'_> {
1412    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1413        if !self.generic_params.is_empty() {
1414            write!(
1415                f,
1416                "for<{}>",
1417                self.generic_params
1418                    .iter()
1419                    .map(|param| param.name.ident())
1420                    .format(",")
1421            )?;
1422        }
1423        write!(f, "{:?}", self.decl)
1424    }
1425}
1426
1427impl fmt::Debug for Lifetime {
1428    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1429        match self {
1430            Lifetime::Hole(_) => write!(f, "'_"),
1431            Lifetime::Resolved(lft) => write!(f, "{lft:?}"),
1432        }
1433    }
1434}
1435
1436impl fmt::Debug for ConstArg {
1437    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1438        write!(f, "{:?}", self.kind)
1439    }
1440}
1441
1442impl fmt::Debug for ConstArgKind {
1443    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1444        match self {
1445            ConstArgKind::Lit(n) => write!(f, "{n}"),
1446            ConstArgKind::Param(p) => write!(f, "{p:?}"),
1447            ConstArgKind::Infer => write!(f, "_"),
1448        }
1449    }
1450}
1451
1452impl fmt::Debug for BaseTy<'_> {
1453    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1454        match &self.kind {
1455            BaseTyKind::Path(qpath) => write!(f, "{qpath:?}"),
1456            BaseTyKind::Slice(ty) => write!(f, "[{ty:?}]"),
1457            BaseTyKind::Err(_) => write!(f, "err"),
1458        }
1459    }
1460}
1461
1462impl fmt::Debug for QPath<'_> {
1463    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1464        match self {
1465            QPath::Resolved(_, path) => write!(f, "{path:?}"),
1466            QPath::TypeRelative(qself, assoc) => write!(f, "<{qself:?}>::{assoc:?}"),
1467        }
1468    }
1469}
1470
1471impl fmt::Debug for Path<'_> {
1472    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1473        write!(f, "{:?}", self.segments.iter().format("::"))?;
1474        if !self.refine.is_empty() {
1475            write!(f, "({:?})", self.refine.iter().format(", "))?;
1476        }
1477        Ok(())
1478    }
1479}
1480
1481impl fmt::Debug for PathSegment<'_> {
1482    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1483        write!(f, "{}", self.ident)?;
1484        let args: Vec<_> = self
1485            .args
1486            .iter()
1487            .map(|a| a as &dyn std::fmt::Debug)
1488            .chain(self.constraints.iter().map(|b| b as &dyn std::fmt::Debug))
1489            .collect();
1490        if !args.is_empty() {
1491            write!(f, "<{:?}>", args.iter().format(", "))?;
1492        }
1493        Ok(())
1494    }
1495}
1496
1497impl fmt::Debug for GenericArg<'_> {
1498    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1499        match self {
1500            GenericArg::Type(ty) => write!(f, "{ty:?}"),
1501            GenericArg::Lifetime(lft) => write!(f, "{lft:?}"),
1502            GenericArg::Const(cst) => write!(f, "{cst:?}"),
1503            GenericArg::Infer => write!(f, "_"),
1504        }
1505    }
1506}
1507
1508impl fmt::Debug for AssocItemConstraint<'_> {
1509    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1510        match &self.kind {
1511            AssocItemConstraintKind::Equality { term } => {
1512                write!(f, "{:?} = {:?}", self.ident, term)
1513            }
1514        }
1515    }
1516}
1517
1518impl fmt::Debug for AliasReft<'_> {
1519    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1520        match self {
1521            AliasReft::Qualified { qself, trait_, name } => {
1522                write!(f, "<{qself:?} as {trait_:?}>::{name}")
1523            }
1524            AliasReft::TypeRelative { qself, name } => {
1525                write!(f, "{qself:?}::{name}")
1526            }
1527        }
1528    }
1529}
1530
1531impl fmt::Debug for QuantKind {
1532    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1533        match self {
1534            QuantKind::Forall => write!(f, "∀"),
1535            QuantKind::Exists => write!(f, "∃"),
1536        }
1537    }
1538}
1539
1540impl fmt::Debug for Expr<'_> {
1541    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1542        match self.kind {
1543            ExprKind::Var(QPathExpr::Resolved(path, ..)) => write!(f, "{path:?}"),
1544            ExprKind::Var(QPathExpr::TypeRelative(qself, assoc)) => {
1545                write!(f, "<{qself:?}>::{assoc}")
1546            }
1547            ExprKind::BinaryOp(op, e1, e2) => write!(f, "({e1:?} {op:?} {e2:?})"),
1548            ExprKind::PrimApp(op, e1, e2) => write!(f, "[{op:?}]({e1:?}, {e2:?})"),
1549            ExprKind::UnaryOp(op, e) => write!(f, "{op:?}{e:?}"),
1550            ExprKind::Literal(lit) => write!(f, "{lit:?}"),
1551            ExprKind::App(uf, es) => write!(f, "{uf:?}({:?})", es.iter().format(", ")),
1552            ExprKind::Alias(alias, refine_args) => {
1553                write!(f, "{alias:?}({:?})", refine_args.iter().format(", "))
1554            }
1555            ExprKind::IfThenElse(p, e1, e2) => {
1556                write!(f, "(if {p:?} {{ {e1:?} }} else {{ {e2:?} }})")
1557            }
1558            ExprKind::Dot(var, fld) => write!(f, "{var:?}.{fld}"),
1559            ExprKind::Abs(params, body) => {
1560                write!(
1561                    f,
1562                    "|{}| {body:?}",
1563                    params.iter().format_with(", ", |param, f| {
1564                        f(&format_args!("{}: {:?}", param.name, param.sort))
1565                    })
1566                )
1567            }
1568            ExprKind::Record(flds) => {
1569                write!(f, "{{ {:?} }}", flds.iter().format(", "))
1570            }
1571            ExprKind::SetLiteral(elems) => {
1572                write!(f, "#{{ {:?} }}", elems.iter().format(", "))
1573            }
1574            ExprKind::Constructor(path, exprs, spread) => {
1575                if let Some(path) = path
1576                    && let Some(s) = spread
1577                {
1578                    write!(f, "{:?} {{ {:?}, ..{:?} }}", path, exprs.iter().format(", "), s)
1579                } else if let Some(path) = path {
1580                    write!(f, "{:?} {{ {:?} }}", path, exprs.iter().format(", "))
1581                } else if let Some(s) = spread {
1582                    write!(f, "{{ {:?} ..{:?} }}", exprs.iter().format(", "), s)
1583                } else {
1584                    write!(f, "{{ {:?} }}", exprs.iter().format(", "))
1585                }
1586            }
1587            ExprKind::BoundedQuant(kind, refine_param, rng, expr) => {
1588                write!(f, "{kind:?} {refine_param:?} in {}.. {} {{ {expr:?} }}", rng.start, rng.end)
1589            }
1590            ExprKind::Err(_) => write!(f, "err"),
1591            ExprKind::Block(decls, body) => {
1592                for decl in decls {
1593                    write!(f, "let {:?} = {:?};", decl.param, decl.init)?;
1594                }
1595                write!(f, "{body:?}")
1596            }
1597        }
1598    }
1599}
1600
1601impl fmt::Debug for PathExpr<'_> {
1602    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1603        write!(f, "{}", self.segments.iter().format("::"))
1604    }
1605}
1606
1607impl fmt::Debug for Lit {
1608    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1609        match self {
1610            Lit::Int(i, Some(NumLitKind::Real)) => write!(f, "{i}real"),
1611            Lit::Int(i, _) => write!(f, "{i}"),
1612            Lit::Bool(b) => write!(f, "{b}"),
1613            Lit::Str(s) => write!(f, "\"{s:?}\""),
1614            Lit::Char(c) => write!(f, "\'{c}\'"),
1615        }
1616    }
1617}
1618
1619impl fmt::Debug for Sort<'_> {
1620    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1621        match self {
1622            Sort::Path(path) => write!(f, "{path:?}"),
1623            Sort::BitVec(w) => write!(f, "bitvec({w})"),
1624            Sort::Loc => write!(f, "loc"),
1625            Sort::Func(fsort) => write!(f, "{fsort:?}"),
1626            Sort::SortOf(bty) => write!(f, "<{bty:?}>::sort"),
1627            Sort::Infer => write!(f, "_"),
1628            Sort::Err(_) => write!(f, "err"),
1629        }
1630    }
1631}
1632
1633impl fmt::Debug for SortPath<'_> {
1634    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1635        write!(f, "{:?}", self.res)?;
1636        if !self.args.is_empty() {
1637            write!(f, "<{:?}>", self.args.iter().format(", "))?;
1638        }
1639        Ok(())
1640    }
1641}
1642
1643impl fmt::Debug for SortRes {
1644    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1645        match self {
1646            SortRes::PrimSort(PrimSort::Bool) => write!(f, "bool"),
1647            SortRes::PrimSort(PrimSort::Int) => write!(f, "int"),
1648            SortRes::PrimSort(PrimSort::Real) => write!(f, "real"),
1649            SortRes::PrimSort(PrimSort::Char) => write!(f, "char"),
1650            SortRes::PrimSort(PrimSort::Str) => write!(f, "str"),
1651            SortRes::PrimSort(PrimSort::Set) => write!(f, "Set"),
1652            SortRes::PrimSort(PrimSort::Map) => write!(f, "Map"),
1653            SortRes::SortParam(n) => write!(f, "@{n}"),
1654            SortRes::TyParam(def_id) => write!(f, "{}::sort", def_id_to_string(*def_id)),
1655            SortRes::SelfParam { trait_id } => {
1656                write!(f, "{}::Self::sort", def_id_to_string(*trait_id))
1657            }
1658            SortRes::SelfAlias { alias_to } => {
1659                write!(f, "{}::Self::sort", def_id_to_string(*alias_to))
1660            }
1661            SortRes::SelfParamAssoc { ident: assoc, .. } => {
1662                write!(f, "Self::{assoc}")
1663            }
1664            SortRes::User(def_id) => write!(f, "{:?}", def_id.name()),
1665            SortRes::Adt(def_id) => write!(f, "{}::sort", def_id_to_string(*def_id)),
1666        }
1667    }
1668}
1669
1670impl fmt::Debug for PolyFuncSort<'_> {
1671    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1672        if self.params > 0 {
1673            write!(f, "for<{}>{:?}", self.params, self.fsort)
1674        } else {
1675            write!(f, "{:?}", self.fsort)
1676        }
1677    }
1678}
1679
1680impl fmt::Debug for FuncSort<'_> {
1681    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
1682        match self.inputs() {
1683            [input] => {
1684                write!(f, "{:?} -> {:?}", input, self.output())
1685            }
1686            inputs => {
1687                write!(f, "({:?}) -> {:?}", inputs.iter().format(", "), self.output())
1688            }
1689        }
1690    }
1691}
flux_middle/fhir.rs

flux_middle/
fhir.rs
