flux_syntax/
surface.rs

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

flux_syntax/
surface.rs
