flux_middle/
fhir.rs

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

flux_middle/
fhir.rs
