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    /// A `#[no_panic]` attribute
622    NoPanic,
623}
624
625#[derive(Debug)]
626pub struct Path {
627    pub segments: Vec<PathSegment>,
628    pub refine: Vec<RefineArg>,
629    pub node_id: NodeId,
630    pub span: Span,
631}
632
633impl Path {
634    pub fn last(&self) -> &PathSegment {
635        self.segments
636            .last()
637            .expect("path must have at least one segment")
638    }
639}
640
641#[derive(Debug)]
642pub struct PathSegment {
643    pub ident: Ident,
644    pub args: Vec<GenericArg>,
645    pub node_id: NodeId,
646}
647
648#[derive(Debug)]
649pub struct GenericArg {
650    pub kind: GenericArgKind,
651    pub node_id: NodeId,
652}
653
654#[derive(Debug)]
655pub enum GenericArgKind {
656    Type(Ty),
657    Constraint(Ident, Ty),
658}
659
660#[derive(Debug)]
661pub struct FieldExpr {
662    pub ident: Ident,
663    pub expr: Expr,
664    pub span: Span,
665    pub node_id: NodeId,
666}
667
668#[derive(Debug)]
669pub struct Spread {
670    pub expr: Expr,
671    pub span: Span,
672    pub node_id: NodeId,
673}
674
675#[derive(Debug)]
676pub enum ConstructorArg {
677    FieldExpr(FieldExpr),
678    Spread(Spread),
679}
680
681#[derive(Debug)]
682pub struct Expr {
683    pub kind: ExprKind,
684    pub node_id: NodeId,
685    pub span: Span,
686}
687
688#[derive(Debug)]
689pub enum QuantKind {
690    Forall,
691    Exists,
692}
693
694#[derive(Debug)]
695pub enum ExprKind {
696    Path(ExprPath),
697    Dot(Box<Expr>, Ident),
698    Literal(Lit),
699    BinaryOp(BinOp, Box<[Expr; 2]>),
700    UnaryOp(UnOp, Box<Expr>),
701    Call(Box<Expr>, Vec<Expr>),
702    /// A UIF representing a PrimOp expression, e.g. `[<<](x, y)`
703    PrimUIF(BinOp),
704    /// `<qself as path>::name`
705    AssocReft(Box<Ty>, Path, Ident),
706    IfThenElse(Box<[Expr; 3]>),
707    Constructor(Option<ExprPath>, Vec<ConstructorArg>),
708    BoundedQuant(QuantKind, RefineParam, Range<usize>, Box<Expr>),
709    Block(Vec<LetDecl>, Box<Expr>),
710    /// Set expression `#{ e1, e2, ..., en }`
711    SetLiteral(Vec<Expr>),
712}
713
714#[derive(Debug)]
715pub struct LetDecl {
716    pub param: RefineParam,
717    pub init: Expr,
718}
719
720/// A [`Path`] but for refinement expressions
721#[derive(Debug, Clone)]
722pub struct ExprPath {
723    pub segments: Vec<ExprPathSegment>,
724    pub node_id: NodeId,
725    pub span: Span,
726}
727
728#[derive(Debug, Clone)]
729pub struct ExprPathSegment {
730    pub ident: Ident,
731    pub node_id: NodeId,
732}
733#[derive(Copy, Clone, Hash, Eq, PartialEq)]
734pub enum BinOp {
735    Iff,
736    Imp,
737    Or,
738    And,
739    Eq,
740    Ne,
741    Gt,
742    Ge,
743    Lt,
744    Le,
745    Add,
746    Sub,
747    Mul,
748    Div,
749    Mod,
750    BitOr,
751    BitXor,
752    BitAnd,
753    BitShl,
754    BitShr,
755}
756
757impl fmt::Debug for BinOp {
758    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
759        match self {
760            BinOp::Iff => write!(f, "<=>"),
761            BinOp::Imp => write!(f, "=>"),
762            BinOp::Or => write!(f, "||"),
763            BinOp::And => write!(f, "&&"),
764            BinOp::Eq => write!(f, "=="),
765            BinOp::Ne => write!(f, "!="),
766            BinOp::Lt => write!(f, "<"),
767            BinOp::Le => write!(f, "<="),
768            BinOp::Gt => write!(f, ">"),
769            BinOp::Ge => write!(f, ">="),
770            BinOp::Add => write!(f, "+"),
771            BinOp::Sub => write!(f, "-"),
772            BinOp::Mod => write!(f, "mod"),
773            BinOp::Mul => write!(f, "*"),
774            BinOp::Div => write!(f, "/"),
775            BinOp::BitOr => write!(f, "|"),
776            BinOp::BitXor => write!(f, "^"),
777            BinOp::BitAnd => write!(f, "&"),
778            BinOp::BitShl => write!(f, "<<"),
779            BinOp::BitShr => write!(f, ">>"),
780        }
781    }
782}
783
784impl rustc_errors::IntoDiagArg for BinOp {
785    fn into_diag_arg(self, _path: &mut Option<std::path::PathBuf>) -> rustc_errors::DiagArgValue {
786        rustc_errors::DiagArgValue::Str(Cow::Owned(format!("{self:?}")))
787    }
788}
789
790#[derive(Copy, Clone)]
791pub enum UnOp {
792    Not,
793    Neg,
794}
795
796impl fmt::Debug for UnOp {
797    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
798        match self {
799            Self::Not => write!(f, "!"),
800            Self::Neg => write!(f, "-"),
801        }
802    }
803}
804
805impl BindKind {
806    pub fn token_str(&self) -> &'static str {
807        match self {
808            BindKind::At => "@",
809            BindKind::Pound => "#",
810        }
811    }
812}
813
814/// A punctuated sequence of values of type `T` separated by punctuation of type `P`
815pub struct Punctuated<T, P> {
816    inner: Vec<(T, P)>,
817    last: Option<Box<T>>,
818}
819
820impl<T, P> From<Vec<(T, P)>> for Punctuated<T, P> {
821    fn from(inner: Vec<(T, P)>) -> Self {
822        Self { inner, last: None }
823    }
824}
825
826impl<T, P> Punctuated<T, P> {
827    pub fn len(&self) -> usize {
828        self.inner.len() + self.last.is_some() as usize
829    }
830
831    /// Determines whether this punctuated sequence is empty, meaning it
832    /// contains no syntax tree nodes or punctuation.
833    pub fn is_empty(&self) -> bool {
834        self.inner.len() == 0 && self.last.is_none()
835    }
836
837    /// Appends a syntax tree node onto the end of this punctuated sequence. The
838    /// sequence must already have a trailing punctuation, or be empty.
839    ///
840    /// # Panics
841    ///
842    /// Panics if the sequence is nonempty and does not already have a trailing
843    /// punctuation.
844    pub fn push_value(&mut self, value: T) {
845        assert!(
846            self.empty_or_trailing(),
847            "Punctuated::push_value: cannot push value if Punctuated is missing trailing punctuation",
848        );
849
850        self.last = Some(Box::new(value));
851    }
852
853    /// Returns true if either this `Punctuated` is empty, or it has a trailing
854    /// punctuation.
855    ///
856    /// Equivalent to `punctuated.is_empty() || punctuated.trailing_punct()`.
857    pub fn empty_or_trailing(&self) -> bool {
858        self.last.is_none()
859    }
860
861    /// Determines whether this punctuated sequence ends with a trailing
862    /// punctuation.
863    pub fn trailing_punct(&self) -> bool {
864        self.last.is_none() && !self.is_empty()
865    }
866
867    pub fn into_values(self) -> Vec<T> {
868        let mut v: Vec<T> = self.inner.into_iter().map(|(v, _)| v).collect();
869        if let Some(last) = self.last {
870            v.push(*last);
871        }
872        v
873    }
874}
flux_syntax/surface.rs

flux_syntax/
surface.rs
