flux_syntax/
surface.rs

1pub mod visit;
2
3use std::{fmt, ops::Range};
4
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 Item {
32    Qualifier(Qualifier),
33    FuncDef(SpecFunc),
34    SortDecl(SortDecl),
35}
36
37impl Item {
38    pub fn name(&self) -> Ident {
39        match self {
40            Item::Qualifier(qualifier) => qualifier.name,
41            Item::FuncDef(spec_func) => spec_func.name,
42            Item::SortDecl(sort_decl) => sort_decl.name,
43        }
44    }
45}
46
47#[derive(Debug)]
48pub struct Qualifier {
49    pub name: Ident,
50    pub params: RefineParams,
51    pub expr: Expr,
52    pub span: Span,
53    pub global: bool,
54}
55
56/// A global function definition. It can be either an uninterpreted function or a *syntactic abstraction*,
57/// i.e., a function with a body.
58#[derive(Debug)]
59pub struct SpecFunc {
60    pub name: Ident,
61    pub sort_vars: Vec<Ident>,
62    pub params: RefineParams,
63    pub output: Sort,
64    /// Body of the function. If not present this definition corresponds to an uninterpreted function.
65    pub body: Option<Expr>,
66    /// Is this function "hidden" i.e. to be considered
67    /// as uninterpreted by default (only makes sense if `body` is_some ...)
68    /// as otherwise it is *always* uninterpreted.
69    pub hide: bool,
70}
71
72#[derive(Debug)]
73pub struct Generics {
74    pub params: Vec<GenericParam>,
75    pub predicates: Option<Vec<WhereBoundPredicate>>,
76    pub span: Span,
77}
78
79#[derive(Debug)]
80pub struct GenericParam {
81    pub name: Ident,
82    pub kind: GenericParamKind,
83    pub node_id: NodeId,
84}
85
86#[derive(Debug)]
87pub enum GenericParamKind {
88    Type,
89    Base,
90}
91
92#[derive(Debug)]
93pub struct TyAlias {
94    pub ident: Ident,
95    pub generics: Generics,
96    pub params: RefineParams,
97    pub index: Option<RefineParam>,
98    pub ty: Ty,
99    pub node_id: NodeId,
100    pub span: Span,
101}
102
103#[derive(Debug)]
104pub struct ConstantInfo {
105    pub expr: Option<Expr>,
106}
107
108#[derive(Debug)]
109pub struct StructDef {
110    pub generics: Option<Generics>,
111    pub refined_by: Option<RefineParams>,
112    pub fields: Vec<Option<Ty>>,
113    pub opaque: bool,
114    pub invariants: Vec<Expr>,
115    pub node_id: NodeId,
116}
117
118impl StructDef {
119    /// Whether the struct contains any path that needs to be resolved.
120    pub fn needs_resolving(&self) -> bool {
121        self.fields.iter().any(Option::is_some)
122    }
123}
124
125#[derive(Debug)]
126pub struct EnumDef {
127    pub generics: Option<Generics>,
128    pub refined_by: Option<RefineParams>,
129    pub variants: Vec<Option<VariantDef>>,
130    pub invariants: Vec<Expr>,
131    pub node_id: NodeId,
132    pub reflected: bool,
133}
134
135impl EnumDef {
136    /// Whether the enum contains any path that needs to be resolved.
137    pub fn needs_resolving(&self) -> bool {
138        self.variants.iter().any(Option::is_some)
139    }
140}
141
142#[derive(Debug)]
143pub struct VariantDef {
144    pub fields: Vec<Ty>,
145    pub ret: Option<VariantRet>,
146    pub node_id: NodeId,
147    pub span: Span,
148}
149
150#[derive(Debug)]
151pub struct VariantRet {
152    pub path: Path,
153    /// Binders are not allowed at this position, but we parse this as a list of indices
154    /// for better error reporting.
155    pub indices: Indices,
156}
157
158pub type RefineParams = Vec<RefineParam>;
159
160#[derive(Debug, Default)]
161pub struct QualNames {
162    pub names: Vec<Ident>,
163}
164
165#[derive(Debug, Default)]
166pub struct RevealNames {
167    pub names: Vec<Ident>,
168}
169
170#[derive(Debug)]
171pub struct RefineParam {
172    pub ident: Ident,
173    pub sort: Sort,
174    pub mode: Option<ParamMode>,
175    pub span: Span,
176    pub node_id: NodeId,
177}
178
179#[derive(Clone, Copy, Debug, PartialEq, Eq)]
180pub enum ParamMode {
181    Horn,
182    Hindley,
183}
184
185#[derive(Debug)]
186pub enum Sort {
187    /// A _base_ sort, e.g., `int` or `bool`.
188    Base(BaseSort),
189    /// A _function_ sort of the form `(bi,...) -> bo` where `bi..` and `bo`
190    /// are all base sorts.
191    Func { inputs: Vec<BaseSort>, output: BaseSort },
192    /// A sort that needs to be inferred.
193    Infer,
194}
195
196#[derive(Debug)]
197pub enum BaseSort {
198    /// a bitvector sort, e.g., bitvec<32>
199    BitVec(u32),
200    SortOf(Box<Ty>, Path),
201    Path(SortPath),
202}
203
204/// A [`Path`] but for sorts.
205#[derive(Debug)]
206pub struct SortPath {
207    /// The segments in the path
208    pub segments: Vec<Ident>,
209    /// The sort arguments, i.e., the list `[int, bool]` in `Map<int, bool>`.
210    pub args: Vec<BaseSort>,
211    pub node_id: NodeId,
212}
213
214#[derive(Debug)]
215pub struct Impl {
216    pub generics: Option<Generics>,
217    pub assoc_refinements: Vec<ImplAssocReft>,
218}
219
220#[derive(Debug)]
221pub struct ImplAssocReft {
222    pub name: Ident,
223    pub params: RefineParams,
224    pub output: BaseSort,
225    pub body: Expr,
226    pub span: Span,
227}
228
229pub struct Trait {
230    pub generics: Option<Generics>,
231    pub assoc_refinements: Vec<TraitAssocReft>,
232}
233
234#[derive(Debug)]
235pub struct TraitAssocReft {
236    pub name: Ident,
237    pub params: RefineParams,
238    pub output: BaseSort,
239    pub body: Option<Expr>,
240    pub span: Span,
241}
242
243#[derive(Debug)]
244pub struct FnSpec {
245    pub fn_sig: Option<FnSig>,
246    pub qual_names: Option<QualNames>,
247    pub reveal_names: Option<RevealNames>,
248}
249
250#[derive(Debug)]
251pub struct FnSig {
252    pub asyncness: Async,
253    pub ident: Option<Ident>,
254    pub generics: Generics,
255    pub params: RefineParams,
256    /// example: `requires n > 0`
257    pub requires: Vec<Requires>,
258    /// example: `i32<@n>`
259    pub inputs: Vec<FnInput>,
260    pub output: FnOutput,
261    /// source span
262    pub span: Span,
263    pub node_id: NodeId,
264}
265
266#[derive(Debug)]
267pub struct Requires {
268    /// Optional list of universally quantified parameters
269    pub params: RefineParams,
270    pub pred: Expr,
271}
272
273#[derive(Debug)]
274pub struct FnOutput {
275    /// example `i32{v:v >= 0}`
276    pub returns: FnRetTy,
277    /// example: `*x: i32{v. v = n+1}` or just `x > 10`
278    pub ensures: Vec<Ensures>,
279    pub node_id: NodeId,
280}
281
282#[derive(Debug)]
283pub enum Ensures {
284    /// A type constraint on a location
285    Type(Ident, Ty, NodeId),
286    /// A predicate that needs to hold
287    Pred(Expr),
288}
289
290#[derive(Debug)]
291pub enum FnRetTy {
292    Default(Span),
293    Ty(Ty),
294}
295
296#[derive(Debug, Copy, Clone)]
297pub enum Async {
298    Yes { node_id: NodeId, span: Span },
299    No,
300}
301
302#[derive(Debug)]
303pub struct WhereBoundPredicate {
304    pub span: Span,
305    pub bounded_ty: Ty,
306    pub bounds: GenericBounds,
307}
308
309pub type GenericBounds = Vec<TraitRef>;
310
311#[derive(Debug)]
312pub struct TraitRef {
313    pub path: Path,
314    pub node_id: NodeId,
315}
316
317impl TraitRef {
318    fn is_fn_trait_name(name: Symbol) -> bool {
319        name == sym::FnOnce || name == sym::FnMut || name == sym::Fn
320    }
321
322    pub fn as_fn_trait_ref(&self) -> Option<(&GenericArg, &GenericArg)> {
323        if let [segment] = self.path.segments.as_slice()
324            && Self::is_fn_trait_name(segment.ident.name)
325            && let [in_arg, out_arg] = segment.args.as_slice()
326        {
327            return Some((in_arg, out_arg));
328        }
329        None
330    }
331}
332
333#[derive(Debug)]
334pub enum FnInput {
335    /// example `a: i32{a > 0}`
336    Constr(Ident, Path, Expr, NodeId),
337    /// example `v: &strg i32`
338    StrgRef(Ident, Ty, NodeId),
339    /// A type with an optional binder, e.g, `i32`, `x: i32` or `x: i32{v: v > 0}`.
340    /// The binder has a different meaning depending on the type.
341    Ty(Option<Ident>, Ty, NodeId),
342}
343
344#[derive(Debug)]
345pub struct Ty {
346    pub kind: TyKind,
347    pub node_id: NodeId,
348    pub span: Span,
349}
350
351#[derive(Debug)]
352pub enum TyKind {
353    /// ty
354    Base(BaseTy),
355    /// `B[r]`
356    Indexed {
357        bty: BaseTy,
358        indices: Indices,
359    },
360    /// B{v: r}
361    Exists {
362        bind: Ident,
363        bty: BaseTy,
364        pred: Expr,
365    },
366    GeneralExists {
367        params: RefineParams,
368        ty: Box<Ty>,
369        pred: Option<Expr>,
370    },
371    /// Mutable or shared reference
372    Ref(Mutability, Box<Ty>),
373    /// Constrained type: an exists without binder
374    Constr(Expr, Box<Ty>),
375    Tuple(Vec<Ty>),
376    Array(Box<Ty>, ConstArg),
377    /// The `NodeId` is used to resolve the type to a corresponding `OpaqueTy`
378    ImplTrait(NodeId, GenericBounds),
379    Hole,
380}
381
382impl Ty {
383    pub fn is_refined(&self) -> bool {
384        struct IsRefinedVisitor {
385            is_refined: bool,
386        }
387        let mut vis = IsRefinedVisitor { is_refined: false };
388        impl visit::Visitor for IsRefinedVisitor {
389            fn visit_ty(&mut self, ty: &Ty) {
390                match &ty.kind {
391                    TyKind::Tuple(_)
392                    | TyKind::Ref(..)
393                    | TyKind::Array(..)
394                    | TyKind::ImplTrait(..)
395                    | TyKind::Hole
396                    | TyKind::Base(_) => {
397                        visit::walk_ty(self, ty);
398                    }
399                    TyKind::Indexed { .. }
400                    | TyKind::Exists { .. }
401                    | TyKind::GeneralExists { .. }
402                    | TyKind::Constr(..) => {
403                        self.is_refined = true;
404                    }
405                }
406            }
407        }
408        vis.visit_ty(self);
409        vis.is_refined
410    }
411}
412#[derive(Debug)]
413pub struct BaseTy {
414    pub kind: BaseTyKind,
415    pub span: Span,
416}
417
418#[derive(Debug)]
419pub enum BaseTyKind {
420    Path(Option<Box<Ty>>, Path),
421    Slice(Box<Ty>),
422}
423
424#[derive(PartialEq, Eq, Clone, Debug, Copy)]
425pub struct ConstArg {
426    pub kind: ConstArgKind,
427    pub span: Span,
428}
429
430#[derive(PartialEq, Eq, Clone, Debug, Copy)]
431pub enum ConstArgKind {
432    Lit(usize),
433    Infer,
434}
435
436#[derive(Debug)]
437pub struct Indices {
438    pub indices: Vec<RefineArg>,
439    pub span: Span,
440}
441
442#[derive(Debug)]
443pub enum RefineArg {
444    /// `@n` or `#n`, the span corresponds to the span of the identifier plus the binder token (`@` or `#`)
445    Bind(Ident, BindKind, Span, NodeId),
446    Expr(Expr),
447    Abs(RefineParams, Expr, Span, NodeId),
448}
449
450#[derive(Debug, Clone, Copy)]
451pub enum BindKind {
452    At,
453    Pound,
454}
455
456#[derive(Debug)]
457pub struct Path {
458    pub segments: Vec<PathSegment>,
459    pub refine: Vec<RefineArg>,
460    pub node_id: NodeId,
461    pub span: Span,
462}
463
464impl Path {
465    pub fn last(&self) -> &PathSegment {
466        self.segments
467            .last()
468            .expect("path must have at least one segment")
469    }
470}
471
472#[derive(Debug)]
473pub struct PathSegment {
474    pub ident: Ident,
475    pub args: Vec<GenericArg>,
476    pub node_id: NodeId,
477}
478
479#[derive(Debug)]
480pub struct GenericArg {
481    pub kind: GenericArgKind,
482    pub node_id: NodeId,
483}
484
485#[derive(Debug)]
486pub enum GenericArgKind {
487    Type(Ty),
488    Constraint(Ident, Ty),
489}
490
491#[derive(Debug)]
492pub struct FieldExpr {
493    pub ident: Ident,
494    pub expr: Expr,
495    pub span: Span,
496    pub node_id: NodeId,
497}
498
499#[derive(Debug)]
500pub struct Spread {
501    pub expr: Expr,
502    pub span: Span,
503    pub node_id: NodeId,
504}
505
506#[derive(Debug)]
507pub enum ConstructorArg {
508    FieldExpr(FieldExpr),
509    Spread(Spread),
510}
511
512#[derive(Debug)]
513pub struct Expr {
514    pub kind: ExprKind,
515    pub node_id: NodeId,
516    pub span: Span,
517}
518
519#[derive(Debug)]
520pub enum QuantKind {
521    Forall,
522    Exists,
523}
524
525#[derive(Debug)]
526pub enum ExprKind {
527    Path(ExprPath),
528    Dot(Box<Expr>, Ident),
529    Literal(Lit),
530    BinaryOp(BinOp, Box<[Expr; 2]>),
531    UnaryOp(UnOp, Box<Expr>),
532    Call(Box<Expr>, Vec<Expr>),
533    /// `<qself as path>::name`
534    AssocReft(Box<Ty>, Path, Ident),
535    IfThenElse(Box<[Expr; 3]>),
536    Constructor(Option<ExprPath>, Vec<ConstructorArg>),
537    BoundedQuant(QuantKind, RefineParam, Range<usize>, Box<Expr>),
538    Block(Vec<LetDecl>, Box<Expr>),
539}
540
541#[derive(Debug)]
542pub struct LetDecl {
543    pub param: RefineParam,
544    pub init: Expr,
545}
546
547/// A [`Path`] but for refinement expressions
548#[derive(Debug, Clone)]
549pub struct ExprPath {
550    pub segments: Vec<ExprPathSegment>,
551    pub node_id: NodeId,
552    pub span: Span,
553}
554
555#[derive(Debug, Clone)]
556pub struct ExprPathSegment {
557    pub ident: Ident,
558    pub node_id: NodeId,
559}
560
561#[derive(Copy, Clone, PartialEq)]
562pub enum BinOp {
563    Iff,
564    Imp,
565    Or,
566    And,
567    Eq,
568    Ne,
569    Gt,
570    Ge,
571    Lt,
572    Le,
573    Add,
574    Sub,
575    Mul,
576    Div,
577    Mod,
578    BitAnd,
579    BitOr,
580    BitShl,
581    BitShr,
582}
583
584impl fmt::Debug for BinOp {
585    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
586        match self {
587            BinOp::Iff => write!(f, "<=>"),
588            BinOp::Imp => write!(f, "=>"),
589            BinOp::Or => write!(f, "||"),
590            BinOp::And => write!(f, "&&"),
591            BinOp::Eq => write!(f, "=="),
592            BinOp::Ne => write!(f, "!="),
593            BinOp::Lt => write!(f, "<"),
594            BinOp::Le => write!(f, "<="),
595            BinOp::Gt => write!(f, ">"),
596            BinOp::Ge => write!(f, ">="),
597            BinOp::Add => write!(f, "+"),
598            BinOp::Sub => write!(f, "-"),
599            BinOp::Mod => write!(f, "mod"),
600            BinOp::Mul => write!(f, "*"),
601            BinOp::Div => write!(f, "/"),
602            BinOp::BitAnd => write!(f, "&"),
603            BinOp::BitOr => write!(f, "|"),
604            BinOp::BitShl => write!(f, "<<"),
605            BinOp::BitShr => write!(f, ">>"),
606        }
607    }
608}
609
610#[derive(Copy, Clone)]
611pub enum UnOp {
612    Not,
613    Neg,
614}
615
616impl fmt::Debug for UnOp {
617    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
618        match self {
619            Self::Not => write!(f, "!"),
620            Self::Neg => write!(f, "-"),
621        }
622    }
623}
624
625impl BindKind {
626    pub fn token_str(&self) -> &'static str {
627        match self {
628            BindKind::At => "@",
629            BindKind::Pound => "#",
630        }
631    }
632}
633
634/// A punctuated sequence of values of type `T` separated by punctuation of type `P`
635pub struct Punctuated<T, P> {
636    inner: Vec<(T, P)>,
637    last: Option<Box<T>>,
638}
639
640impl<T, P> From<Vec<(T, P)>> for Punctuated<T, P> {
641    fn from(inner: Vec<(T, P)>) -> Self {
642        Self { inner, last: None }
643    }
644}
645
646impl<T, P> Punctuated<T, P> {
647    pub fn len(&self) -> usize {
648        self.inner.len() + self.last.is_some() as usize
649    }
650
651    /// Determines whether this punctuated sequence is empty, meaning it
652    /// contains no syntax tree nodes or punctuation.
653    pub fn is_empty(&self) -> bool {
654        self.inner.len() == 0 && self.last.is_none()
655    }
656
657    /// Appends a syntax tree node onto the end of this punctuated sequence. The
658    /// sequence must already have a trailing punctuation, or be empty.
659    ///
660    /// # Panics
661    ///
662    /// Panics if the sequence is nonempty and does not already have a trailing
663    /// punctuation.
664    pub fn push_value(&mut self, value: T) {
665        assert!(
666            self.empty_or_trailing(),
667            "Punctuated::push_value: cannot push value if Punctuated is missing trailing punctuation",
668        );
669
670        self.last = Some(Box::new(value));
671    }
672
673    /// Returns true if either this `Punctuated` is empty, or it has a trailing
674    /// punctuation.
675    ///
676    /// Equivalent to `punctuated.is_empty() || punctuated.trailing_punct()`.
677    pub fn empty_or_trailing(&self) -> bool {
678        self.last.is_none()
679    }
680
681    /// Determines whether this punctuated sequence ends with a trailing
682    /// punctuation.
683    pub fn trailing_punct(&self) -> bool {
684        self.last.is_none() && !self.is_empty()
685    }
686
687    pub fn into_values(self) -> Vec<T> {
688        let mut v: Vec<T> = self.inner.into_iter().map(|(v, _)| v).collect();
689        if let Some(last) = self.last {
690            v.push(*last);
691        }
692        v
693    }
694}
flux_syntax/surface.rs

flux_syntax/
surface.rs
