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

flux_middle/
fhir.rs
