Skip to main content

flux_syntax/
surface.rs

1pub mod visit;
2
3use std::{borrow::Cow, fmt, ops::Range};
4
5use flux_config::PartialInferOpts;
6pub use rustc_ast::{
7    Mutability,
8    token::{Lit, LitKind},
9};
10use rustc_hash::FxHashSet;
11pub use rustc_span::{Span, symbol::Ident};
12use rustc_span::{Symbol, symbol::sym};
13
14use crate::surface::visit::Visitor;
15
16/// A [`NodeId`] is a unique identifier we assign to some AST nodes to be able to attach information
17/// to them. For example, to assign a resolution to a [`Path`]. The [`NodeId`] is unique within a crate.
18#[derive(Copy, Clone, Debug, Hash, PartialEq, Eq)]
19pub struct NodeId(pub(super) usize);
20
21impl NodeId {
22    pub fn as_usize(&self) -> usize {
23        self.0
24    }
25}
26
27#[derive(Debug)]
28pub struct SortDecl {
29    pub name: Ident,
30    pub sort_vars: Vec<Ident>,
31}
32
33#[derive(Debug)]
34pub enum FluxItem {
35    Qualifier(Qualifier),
36    FuncDef(SpecFunc),
37    SortDecl(SortDecl),
38    PrimOpProp(PrimOpProp),
39    Use(UseTree),
40}
41
42impl FluxItem {
43    pub fn name(&self) -> Option<Ident> {
44        match self {
45            FluxItem::Qualifier(qualifier) => Some(qualifier.name),
46            FluxItem::FuncDef(spec_func) => Some(spec_func.name),
47            FluxItem::SortDecl(sort_decl) => Some(sort_decl.name),
48            FluxItem::PrimOpProp(primop_prop) => Some(primop_prop.name),
49            FluxItem::Use(_) => None,
50        }
51    }
52}
53
54#[derive(Debug)]
55pub struct UseTree {
56    pub prefix: ExprPath,
57    pub kind: UseTreeKind,
58}
59
60#[derive(Debug)]
61pub enum UseTreeKind {
62    /// `use a::b::c`
63    Simple,
64    /// `use a::b::{...}`
65    Nested(Vec<UseTree>),
66}
67
68#[derive(Debug)]
69pub struct Qualifier {
70    pub name: Ident,
71    pub params: RefineParams,
72    pub wildcards: Vec<bool>,
73    pub expr: Expr,
74    pub span: Span,
75    pub kind: QualifierKind,
76}
77
78#[derive(Debug)]
79pub enum QualifierKind {
80    Global,
81    Local,
82    Hint,
83}
84
85/// A global function definition. It can be either an uninterpreted function or a *syntactic abstraction*,
86/// i.e., a function with a body.
87#[derive(Debug)]
88pub struct SpecFunc {
89    pub name: Ident,
90    pub sort_vars: Vec<Ident>,
91    pub params: RefineParams,
92    pub output: Sort,
93    /// Body of the function. If not present this definition corresponds to an uninterpreted function.
94    pub body: Option<Expr>,
95    /// Is this function "hidden" i.e. to be considered
96    /// as uninterpreted by default (only makes sense if `body` is_some ...)
97    /// as otherwise it is *always* uninterpreted.
98    pub hide: bool,
99}
100
101/// A (currently global) *primop property*; see tests/tests/pos/surface/
102#[derive(Debug)]
103pub struct PrimOpProp {
104    /// The name of the property
105    pub name: Ident,
106    /// The binop it is attached to
107    pub op: BinOp,
108    /// The sort _at_ which the primop is defined,
109    /// The binders for the inputs of the primop; the output sort is always `Bool`
110    pub params: RefineParams,
111    /// The actual definition of the property
112    pub body: Expr,
113    pub span: Span,
114}
115
116#[derive(Debug)]
117pub struct Generics {
118    pub params: Vec<GenericParam>,
119    pub predicates: Option<Vec<WhereBoundPredicate>>,
120    pub span: Span,
121}
122
123#[derive(Debug)]
124pub struct GenericParam {
125    pub name: Ident,
126    pub node_id: NodeId,
127}
128
129#[derive(Debug)]
130pub struct TyAlias {
131    pub ident: Ident,
132    pub generics: Generics,
133    pub params: RefineParams,
134    pub index: Option<RefineParam>,
135    pub ty: Ty,
136    pub node_id: NodeId,
137    pub span: Span,
138}
139
140pub struct Item {
141    pub attrs: Vec<Attr>,
142    pub kind: ItemKind,
143    pub node_id: NodeId,
144}
145
146pub enum ItemKind {
147    Fn(Option<FnSig>),
148    Struct(StructDef),
149    Enum(EnumDef),
150    Trait(Trait),
151    Impl(Impl),
152    Const(ConstantInfo),
153    TyAlias(Box<TyAlias>),
154    Static(StaticInfo),
155    /// Modules can't be refined but we collect attributes for them, e.g., `#[trusted]`
156    /// This kind is also used for the crate root, for which we also collect attributes.
157    Mod,
158}
159
160pub struct TraitItemFn {
161    pub attrs: Vec<Attr>,
162    pub sig: Option<FnSig>,
163    pub node_id: NodeId,
164}
165
166pub struct ImplItemFn {
167    pub attrs: Vec<Attr>,
168    pub sig: Option<FnSig>,
169    pub node_id: NodeId,
170}
171
172#[derive(Debug)]
173pub struct DetachedSpecs {
174    pub items: Vec<DetachedItem>,
175}
176
177#[derive(Debug)]
178pub struct DetachedTraitImpl {
179    pub trait_: ExprPath,
180    pub items: Vec<DetachedItem<FnSig>>,
181    pub refts: Vec<ImplAssocReft>,
182    pub span: Span,
183}
184
185#[derive(Debug, Default)]
186pub struct DetachedTrait {
187    pub items: Vec<DetachedItem<FnSig>>,
188    pub refts: Vec<TraitAssocReft>,
189}
190
191#[derive(Debug)]
192pub struct DetachedInherentImpl {
193    pub items: Vec<DetachedItem<FnSig>>,
194    pub span: Span,
195}
196
197impl DetachedInherentImpl {
198    pub fn extend(&mut self, other: DetachedInherentImpl) {
199        self.items.extend(other.items);
200    }
201}
202
203#[derive(Debug)]
204pub struct DetachedItem<K = DetachedItemKind> {
205    pub attrs: Vec<Attr>,
206    pub path: ExprPath,
207    pub kind: K,
208    pub node_id: NodeId,
209}
210
211impl<K> DetachedItem<K> {
212    pub fn map_kind<R>(self, f: impl FnOnce(K) -> R) -> DetachedItem<R> {
213        DetachedItem {
214            attrs: self.attrs,
215            path: self.path,
216            kind: f(self.kind),
217            node_id: self.node_id,
218        }
219    }
220}
221
222impl DetachedItem<DetachedItemKind> {
223    pub fn span(&self) -> Span {
224        match &self.kind {
225            DetachedItemKind::InherentImpl(impl_) => impl_.span,
226            DetachedItemKind::TraitImpl(trait_impl) => trait_impl.span,
227            _ => self.path.span,
228        }
229    }
230}
231
232#[derive(Debug)]
233pub enum DetachedItemKind {
234    FnSig(FnSig),
235    Mod(DetachedSpecs),
236    Struct(StructDef),
237    Enum(EnumDef),
238    InherentImpl(DetachedInherentImpl),
239    TraitImpl(DetachedTraitImpl),
240    Trait(DetachedTrait),
241    Static(StaticInfo),
242}
243
244#[derive(Debug)]
245pub struct ConstantInfo {
246    pub expr: Option<Expr>,
247}
248
249#[derive(Debug)]
250pub struct StaticInfo {
251    pub ty: Ty,
252}
253
254#[derive(Debug)]
255pub struct StructDef {
256    pub generics: Option<Generics>,
257    pub refined_by: Option<RefineParams>,
258    pub fields: Vec<Option<Ty>>,
259    pub opaque: bool,
260    pub invariants: Vec<Expr>,
261}
262
263#[derive(Debug)]
264pub struct EnumDef {
265    pub generics: Option<Generics>,
266    pub refined_by: Option<RefineParams>,
267    pub variants: Vec<Option<VariantDef>>,
268    pub invariants: Vec<Expr>,
269    pub reflected: bool,
270}
271
272#[derive(Debug)]
273pub struct VariantDef {
274    pub ident: Option<Ident>,
275    pub fields: Vec<Ty>,
276    pub ret: Option<VariantRet>,
277    pub node_id: NodeId,
278    pub span: Span,
279}
280
281#[derive(Debug)]
282pub struct VariantRet {
283    pub path: Path,
284    /// Binders are not allowed at this position, but we parse this as a list of indices
285    /// for better error reporting.
286    pub indices: Indices,
287}
288
289pub type RefineParams = Vec<RefineParam>;
290
291#[derive(Debug)]
292pub struct RefineParam {
293    pub ident: Ident,
294    pub sort: Sort,
295    pub mode: Option<ParamMode>,
296    pub span: Span,
297    pub node_id: NodeId,
298}
299
300#[derive(Clone, Copy, Debug, PartialEq, Eq)]
301pub enum ParamMode {
302    Horn,
303    Hindley,
304}
305
306#[derive(Debug)]
307pub enum Sort {
308    /// A _base_ sort, e.g., `int` or `bool`.
309    Base(BaseSort),
310    /// A _function_ sort of the form `(bi,...) -> bo` where `bi..` and `bo`
311    /// are all base sorts.
312    Func { inputs: Vec<BaseSort>, output: BaseSort },
313    /// A sort that needs to be inferred.
314    Infer,
315}
316
317#[derive(Debug)]
318pub enum BaseSort {
319    /// a bitvector sort, e.g., bitvec<32>
320    BitVec(u32),
321    SortOf(Box<Ty>, Path),
322    Path(SortPath),
323    /// a tuple sort, e.g., (int, bool)
324    Tuple(Vec<BaseSort>),
325}
326
327/// A [`Path`] but for sorts.
328#[derive(Debug)]
329pub struct SortPath {
330    /// The segments in the path
331    pub segments: Vec<Ident>,
332    /// The sort arguments, i.e., the list `[int, bool]` in `Map<int, bool>`.
333    pub args: Vec<BaseSort>,
334    pub node_id: NodeId,
335}
336
337#[derive(Debug)]
338pub struct Impl {
339    pub generics: Option<Generics>,
340    pub assoc_refinements: Vec<ImplAssocReft>,
341}
342
343#[derive(Debug)]
344pub struct ImplAssocReft {
345    pub name: Ident,
346    pub params: RefineParams,
347    pub output: BaseSort,
348    pub body: Expr,
349    pub span: Span,
350}
351
352#[derive(Debug)]
353pub struct Trait {
354    pub generics: Option<Generics>,
355    pub assoc_refinements: Vec<TraitAssocReft>,
356}
357
358#[derive(Debug)]
359pub struct TraitAssocReft {
360    pub name: Ident,
361    pub params: RefineParams,
362    pub output: BaseSort,
363    pub body: Option<Expr>,
364    pub span: Span,
365    pub final_: bool,
366}
367
368#[derive(Debug)]
369pub struct FnSig {
370    pub asyncness: Async,
371    pub ident: Option<Ident>,
372    pub generics: Generics,
373    pub params: RefineParams,
374    /// example: `requires n > 0`
375    pub requires: Vec<Requires>,
376    /// example: `i32<@n>`
377    pub inputs: Vec<FnInput>,
378    pub output: FnOutput,
379    /// source span
380    pub span: Span,
381    pub node_id: NodeId,
382    pub no_panic: Option<Expr>,
383}
384
385#[derive(Debug)]
386pub struct Requires {
387    /// Optional list of universally quantified parameters
388    pub params: RefineParams,
389    pub pred: Expr,
390}
391
392#[derive(Debug)]
393pub struct FnOutput {
394    /// example `i32{v:v >= 0}`
395    pub returns: FnRetTy,
396    /// example: `*x: i32{v. v = n+1}` or just `x > 10`
397    pub ensures: Vec<Ensures>,
398    pub node_id: NodeId,
399}
400
401#[derive(Debug)]
402pub enum Ensures {
403    /// A type constraint on a location
404    Type(Ident, Ty, NodeId),
405    /// A predicate that needs to hold
406    Pred(Expr),
407}
408
409#[derive(Debug)]
410pub enum FnRetTy {
411    Default(Span),
412    Ty(Box<Ty>),
413}
414
415#[derive(Debug, Copy, Clone)]
416pub enum Async {
417    Yes { node_id: NodeId, span: Span },
418    No,
419}
420
421#[derive(Debug)]
422pub struct WhereBoundPredicate {
423    pub span: Span,
424    pub bounded_ty: Ty,
425    pub bounds: GenericBounds,
426}
427
428pub type GenericBounds = Vec<TraitRef>;
429
430#[derive(Debug)]
431pub struct TraitRef {
432    pub path: Path,
433    pub node_id: NodeId,
434}
435
436impl TraitRef {
437    fn is_fn_trait_name(name: Symbol) -> bool {
438        name == sym::FnOnce || name == sym::FnMut || name == sym::Fn
439    }
440
441    pub fn as_fn_trait_ref(&self) -> Option<(&GenericArg, &GenericArg)> {
442        if let [segment] = self.path.segments.as_slice()
443            && Self::is_fn_trait_name(segment.ident.name)
444            && let [in_arg, out_arg] = segment.args.as_slice()
445        {
446            return Some((in_arg, out_arg));
447        }
448        None
449    }
450}
451
452#[derive(Debug)]
453pub enum FnInput {
454    /// example `a: i32{a > 0}`
455    Constr(Ident, Path, Expr, NodeId),
456    /// example `v: &strg i32`
457    StrgRef(Ident, Ty, NodeId),
458    /// A type with an optional binder, e.g, `i32`, `x: i32` or `x: i32{v: v > 0}`.
459    /// The binder has a different meaning depending on the type.
460    Ty(Option<Ident>, Ty, NodeId),
461}
462
463#[derive(Debug)]
464pub struct Ty {
465    pub kind: TyKind,
466    pub node_id: NodeId,
467    pub span: Span,
468}
469
470#[derive(Debug)]
471pub enum TyKind {
472    /// ty
473    Base(BaseTy),
474    /// `B[r]`
475    Indexed {
476        bty: BaseTy,
477        indices: Indices,
478    },
479    /// B{v: r}
480    Exists {
481        bind: Ident,
482        bty: BaseTy,
483        pred: Expr,
484    },
485    GeneralExists {
486        params: RefineParams,
487        ty: Box<Ty>,
488        pred: Option<Expr>,
489    },
490    /// Mutable or shared reference
491    Ref(Mutability, Box<Ty>),
492    /// Constrained type: an exists without binder
493    Constr(Expr, Box<Ty>),
494    Tuple(Vec<Ty>),
495    Array(Box<Ty>, ConstArg),
496    /// The `NodeId` is used to resolve the type to a corresponding `OpaqueTy`
497    ImplTrait(NodeId, GenericBounds),
498    Hole,
499}
500
501impl Ty {
502    pub fn is_refined(&self) -> bool {
503        struct IsRefinedVisitor {
504            is_refined: bool,
505        }
506        let mut vis = IsRefinedVisitor { is_refined: false };
507        impl visit::Visitor for IsRefinedVisitor {
508            fn visit_ty(&mut self, ty: &Ty) {
509                match &ty.kind {
510                    TyKind::Tuple(_)
511                    | TyKind::Ref(..)
512                    | TyKind::Array(..)
513                    | TyKind::ImplTrait(..)
514                    | TyKind::Hole
515                    | TyKind::Base(_) => {
516                        visit::walk_ty(self, ty);
517                    }
518                    TyKind::Indexed { .. }
519                    | TyKind::Exists { .. }
520                    | TyKind::GeneralExists { .. }
521                    | TyKind::Constr(..) => {
522                        self.is_refined = true;
523                    }
524                }
525            }
526        }
527        vis.visit_ty(self);
528        vis.is_refined
529    }
530
531    pub fn is_potential_const_arg(&self) -> Option<&Path> {
532        if let TyKind::Base(bty) = &self.kind
533            && let BaseTyKind::Path(None, path) = &bty.kind
534            && let [segment] = &path.segments[..]
535            && segment.args.is_empty()
536        {
537            Some(path)
538        } else {
539            None
540        }
541    }
542}
543#[derive(Debug)]
544pub struct BaseTy {
545    pub kind: BaseTyKind,
546    pub span: Span,
547}
548
549#[derive(Debug)]
550pub enum BaseTyKind {
551    Path(Option<Box<Ty>>, Path),
552    Slice(Box<Ty>),
553    /// Raw pointer (*const T or *mut T), optionally with refinement on pointer value
554    Ptr(Mutability, Box<Ty>),
555}
556
557#[derive(Debug)]
558pub struct ConstArg {
559    pub kind: ConstArgKind,
560    pub span: Span,
561}
562
563#[derive(Debug)]
564pub enum ConstArgKind {
565    Lit(usize),
566    Path(Path),
567    Infer,
568}
569
570#[derive(Debug)]
571pub struct Indices {
572    pub indices: Vec<RefineArg>,
573    pub span: Span,
574}
575
576#[derive(Debug)]
577pub enum RefineArg {
578    /// `@n` or `#n`, the span corresponds to the span of the identifier plus the binder token (`@` or `#`)
579    Bind(Ident, BindKind, Span, NodeId),
580    Expr(Expr),
581    Abs(RefineParams, Expr, Span, NodeId),
582}
583
584#[derive(Debug, Clone, Copy)]
585pub enum BindKind {
586    At,
587    Pound,
588}
589
590/// A boolean-like enum used to mark whether some code should be trusted.
591#[derive(Debug, Eq, PartialEq, Copy, Clone)]
592pub enum Trusted {
593    Yes,
594    No,
595}
596
597impl Trusted {
598    pub fn to_bool(self) -> bool {
599        match self {
600            Trusted::Yes => true,
601            Trusted::No => false,
602        }
603    }
604}
605
606impl From<bool> for Trusted {
607    fn from(value: bool) -> Self {
608        if value { Trusted::Yes } else { Trusted::No }
609    }
610}
611
612/// A boolean-like enum used to mark whether a piece of code is ignored.
613#[derive(Debug, Eq, PartialEq, Copy, Clone)]
614pub enum Ignored {
615    Yes,
616    No,
617}
618
619impl Ignored {
620    pub fn to_bool(self) -> bool {
621        match self {
622            Ignored::Yes => true,
623            Ignored::No => false,
624        }
625    }
626}
627
628impl From<bool> for Ignored {
629    fn from(value: bool) -> Self {
630        if value { Ignored::Yes } else { Ignored::No }
631    }
632}
633
634/// An attribute attaches metadata to an item.
635///
636/// Note that some of these attributes correspond to a Rust attribute, but some don't. For example,
637/// when annotating a function, a `#[flux::trusted]` is mapped to [`Attr::Trusted`] because it
638/// corresponds to metadata associated to the function, however, a `#[flux::spec(...)]` doesn't
639/// map to any [`Attr`] because that's considered to be part of the *refined syntax* of the item.
640///
641/// Note that these attributes can also originate from detached specs.
642#[derive(Debug)]
643pub enum Attr {
644    /// A `#[trusted(...)]` attribute
645    Trusted(Trusted),
646    /// A `#[trusted_impl(...)]` attribute
647    TrustedImpl(Trusted),
648    /// A `#[trusted_derive(...)]` attribute
649    TrustedDerive(Trusted),
650    /// A `#[ignore(...)]` attribute
651    Ignore(Ignored),
652    /// A `#[proven_externally]` attribute
653    ProvenExternally(Span),
654    /// A `#[should_fail]` attribute
655    ShouldFail,
656    /// A `#[qualifiers(...)]` attribute
657    Qualifiers(Vec<Ident>),
658    /// A `#[reveal(...)]` attribute
659    Reveal(Vec<Ident>),
660    /// A `#[opts(...)]` attribute
661    InferOpts(PartialInferOpts),
662    /// A `#[no_panic]` attribute
663    NoPanic,
664    /// A `#[assume_parametric(...)]` attribute
665    AssumeParametric(Vec<Ident>),
666    /// A `#[no_suggestions]` attribute
667    NoSuggestions,
668}
669
670#[derive(Debug)]
671pub struct Path {
672    pub segments: Vec<PathSegment>,
673    pub refine: Vec<RefineArg>,
674    pub node_id: NodeId,
675    pub span: Span,
676}
677
678impl Path {
679    pub fn last(&self) -> &PathSegment {
680        self.segments
681            .last()
682            .expect("path must have at least one segment")
683    }
684}
685
686#[derive(Debug)]
687pub struct PathSegment {
688    pub ident: Ident,
689    pub args: Vec<GenericArg>,
690    pub node_id: NodeId,
691}
692
693#[derive(Debug)]
694pub struct GenericArg {
695    pub kind: GenericArgKind,
696    pub node_id: NodeId,
697}
698
699#[derive(Debug)]
700pub enum GenericArgKind {
701    Type(Ty),
702    Constraint(Ident, Ty),
703}
704
705#[derive(Debug)]
706pub struct FieldExpr {
707    pub ident: Ident,
708    pub expr: RefineArg,
709    pub span: Span,
710    pub node_id: NodeId,
711}
712
713#[derive(Debug)]
714pub struct Spread {
715    pub expr: Expr,
716    pub span: Span,
717    pub node_id: NodeId,
718}
719
720#[derive(Debug)]
721pub enum ConstructorArg {
722    FieldExpr(FieldExpr),
723    Spread(Spread),
724}
725
726#[derive(Debug)]
727pub struct Expr {
728    pub kind: ExprKind,
729    pub node_id: NodeId,
730    pub span: Span,
731}
732
733#[derive(Debug)]
734pub enum QuantKind {
735    Forall,
736    Exists,
737}
738
739#[derive(Debug)]
740pub enum ExprKind {
741    Path(ExprPath),
742    Dot(Box<Expr>, Ident),
743    Literal(Lit),
744    BinaryOp(BinOp, Box<[Expr; 2]>),
745    UnaryOp(UnOp, Box<Expr>),
746    Call(Box<Expr>, Vec<Expr>),
747    /// A UIF representing a PrimOp expression, e.g. `[<<](x, y)`
748    PrimUIF(BinOp),
749    /// `<qself as path>::name`
750    AssocReft(Box<Ty>, Path, Ident),
751    IfThenElse(Box<[Expr; 3]>),
752    Constructor(Option<ExprPath>, Vec<ConstructorArg>),
753    Quant(QuantKind, RefineParam, Option<Range<usize>>, Box<Expr>),
754    Block(Vec<LetDecl>, Box<Expr>),
755    /// Set expression `#{ e1, e2, ..., en }`
756    SetLiteral(Vec<Expr>),
757    /// Tuple expression `(e1, e2, ..., en)`
758    Tuple(Vec<Expr>),
759}
760
761#[derive(Debug)]
762pub struct LetDecl {
763    pub param: RefineParam,
764    pub init: Expr,
765}
766
767/// A [`Path`] but for refinement expressions
768#[derive(Debug, Clone)]
769pub struct ExprPath {
770    pub segments: Vec<ExprPathSegment>,
771    pub node_id: NodeId,
772    pub span: Span,
773}
774
775#[derive(Debug, Clone)]
776pub struct ExprPathSegment {
777    pub ident: Ident,
778    pub node_id: NodeId,
779}
780#[derive(Copy, Clone, Hash, Eq, PartialEq)]
781pub enum BinOp {
782    Iff,
783    Imp,
784    Or,
785    And,
786    Eq,
787    Ne,
788    Gt,
789    Ge,
790    Lt,
791    Le,
792    Add,
793    Sub,
794    Mul,
795    Div,
796    Mod,
797    BitOr,
798    BitXor,
799    BitAnd,
800    BitShl,
801    BitShr,
802}
803
804impl fmt::Debug for BinOp {
805    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
806        match self {
807            BinOp::Iff => write!(f, "<=>"),
808            BinOp::Imp => write!(f, "=>"),
809            BinOp::Or => write!(f, "||"),
810            BinOp::And => write!(f, "&&"),
811            BinOp::Eq => write!(f, "=="),
812            BinOp::Ne => write!(f, "!="),
813            BinOp::Lt => write!(f, "<"),
814            BinOp::Le => write!(f, "<="),
815            BinOp::Gt => write!(f, ">"),
816            BinOp::Ge => write!(f, ">="),
817            BinOp::Add => write!(f, "+"),
818            BinOp::Sub => write!(f, "-"),
819            BinOp::Mod => write!(f, "mod"),
820            BinOp::Mul => write!(f, "*"),
821            BinOp::Div => write!(f, "/"),
822            BinOp::BitOr => write!(f, "|"),
823            BinOp::BitXor => write!(f, "^"),
824            BinOp::BitAnd => write!(f, "&"),
825            BinOp::BitShl => write!(f, "<<"),
826            BinOp::BitShr => write!(f, ">>"),
827        }
828    }
829}
830
831impl rustc_errors::IntoDiagArg for BinOp {
832    fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
833        rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
834    }
835}
836
837#[derive(Copy, Clone)]
838pub enum UnOp {
839    Not,
840    Neg,
841}
842
843impl fmt::Debug for UnOp {
844    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
845        match self {
846            Self::Not => write!(f, "!"),
847            Self::Neg => write!(f, "-"),
848        }
849    }
850}
851
852impl BindKind {
853    pub fn token_str(&self) -> &'static str {
854        match self {
855            BindKind::At => "@",
856            BindKind::Pound => "#",
857        }
858    }
859}
860
861/// A punctuated sequence of values of type `T` separated by punctuation of type `P`
862pub struct Punctuated<T, P> {
863    inner: Vec<(T, P)>,
864    last: Option<Box<T>>,
865}
866
867impl<T, P> From<Vec<(T, P)>> for Punctuated<T, P> {
868    fn from(inner: Vec<(T, P)>) -> Self {
869        Self { inner, last: None }
870    }
871}
872
873impl<T, P> Punctuated<T, P> {
874    pub fn len(&self) -> usize {
875        self.inner.len() + self.last.is_some() as usize
876    }
877
878    /// Determines whether this punctuated sequence is empty, meaning it
879    /// contains no syntax tree nodes or punctuation.
880    pub fn is_empty(&self) -> bool {
881        self.inner.len() == 0 && self.last.is_none()
882    }
883
884    /// Appends a syntax tree node onto the end of this punctuated sequence. The
885    /// sequence must already have a trailing punctuation, or be empty.
886    ///
887    /// # Panics
888    ///
889    /// Panics if the sequence is nonempty and does not already have a trailing
890    /// punctuation.
891    pub fn push_value(&mut self, value: T) {
892        assert!(
893            self.empty_or_trailing(),
894            "Punctuated::push_value: cannot push value if Punctuated is missing trailing punctuation",
895        );
896
897        self.last = Some(Box::new(value));
898    }
899
900    /// Returns true if either this `Punctuated` is empty, or it has a trailing
901    /// punctuation.
902    ///
903    /// Equivalent to `punctuated.is_empty() || punctuated.trailing_punct()`.
904    pub fn empty_or_trailing(&self) -> bool {
905        self.last.is_none()
906    }
907
908    /// Determines whether this punctuated sequence ends with a trailing
909    /// punctuation.
910    pub fn trailing_punct(&self) -> bool {
911        self.last.is_none() && !self.is_empty()
912    }
913
914    pub fn into_values(self) -> Vec<T> {
915        let mut v: Vec<T> = self.inner.into_iter().map(|(v, _)| v).collect();
916        if let Some(last) = self.last {
917            v.push(*last);
918        }
919        v
920    }
921}
922
923impl Expr {
924    /// Collects all free variables in an expression.
925    /// A free variable is an `ExprKind::Path` with a single identifier segment.
926    pub fn free_vars(&self) -> FxHashSet<Ident> {
927        struct FreeVarsVisitor {
928            vars: FxHashSet<Ident>,
929        }
930
931        impl visit::Visitor for FreeVarsVisitor {
932            fn visit_expr(&mut self, expr: &Expr) {
933                match &expr.kind {
934                    ExprKind::Path(path) => {
935                        // Only collect paths with a single segment
936                        if let [segment] = path.segments.as_slice() {
937                            self.vars.insert(segment.ident);
938                        }
939                    }
940                    ExprKind::Call(callee, args) => {
941                        // The callee of a call is a refinement function, not a variable, so
942                        // don't collect it. Anything that's not a path may contain free
943                        // variables, so visit it normally.
944                        if !matches!(&callee.kind, ExprKind::Path(_)) {
945                            self.visit_expr(callee);
946                        }
947                        for arg in args {
948                            self.visit_expr(arg);
949                        }
950                    }
951                    // Continue visiting child expressions
952                    _ => visit::walk_expr(self, expr),
953                }
954            }
955        }
956
957        let mut visitor = FreeVarsVisitor { vars: FxHashSet::default() };
958        visitor.visit_expr(self);
959        visitor.vars
960    }
961}