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

flux_middle/
fhir.rs
