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

flux_middle/
fhir.rs
