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

flux_syntax/
surface.rs
