flux_syntax/
surface.rs

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