flux_syntax/
surface.rs

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

flux_syntax/
surface.rs
