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

flux_syntax/
surface.rs
