specl_syntax/
ast.rs

1//! Abstract Syntax Tree for the Specl specification language.
2
3use crate::token::Span;
4
5/// A Specl module (top-level compilation unit).
6#[derive(Debug, Clone)]
7pub struct Module {
8    /// Module name.
9    pub name: Ident,
10    /// Module declarations.
11    pub decls: Vec<Decl>,
12    /// Span covering the entire module.
13    pub span: Span,
14}
15
16/// An identifier with its source span.
17#[derive(Debug, Clone)]
18pub struct Ident {
19    /// The identifier name.
20    pub name: String,
21    /// Source span.
22    pub span: Span,
23}
24
25impl Ident {
26    pub fn new(name: impl Into<String>, span: Span) -> Self {
27        Self {
28            name: name.into(),
29            span,
30        }
31    }
32}
33
34/// A top-level declaration.
35#[derive(Debug, Clone)]
36pub enum Decl {
37    /// `use ModuleName`
38    Use(UseDecl),
39    /// `const NAME: Type`
40    Const(ConstDecl),
41    /// `var NAME: Type`
42    Var(VarDecl),
43    /// `type NAME = Type`
44    Type(TypeDecl),
45    /// `func NAME(params) { expr }`
46    Func(FuncDecl),
47    /// `init { ... }`
48    Init(InitDecl),
49    /// `action NAME(...) { ... }`
50    Action(ActionDecl),
51    /// `invariant NAME { ... }`
52    Invariant(InvariantDecl),
53    /// `property NAME { ... }`
54    Property(PropertyDecl),
55    /// `fairness { ... }`
56    Fairness(FairnessDecl),
57}
58
59impl Decl {
60    pub fn span(&self) -> Span {
61        match self {
62            Decl::Use(d) => d.span,
63            Decl::Const(d) => d.span,
64            Decl::Var(d) => d.span,
65            Decl::Type(d) => d.span,
66            Decl::Func(d) => d.span,
67            Decl::Init(d) => d.span,
68            Decl::Action(d) => d.span,
69            Decl::Invariant(d) => d.span,
70            Decl::Property(d) => d.span,
71            Decl::Fairness(d) => d.span,
72        }
73    }
74}
75
76/// `use ModuleName`
77#[derive(Debug, Clone)]
78pub struct UseDecl {
79    pub module: Ident,
80    pub span: Span,
81}
82
83/// The value of a constant declaration.
84#[derive(Debug, Clone)]
85pub enum ConstValue {
86    /// Type constraint: `const X: 0..10` - value provided at runtime via --constant
87    Type(TypeExpr),
88    /// Scalar value: `const X: 3` - fixed value
89    Scalar(i64),
90}
91
92/// `const NAME: Type` or `const NAME: value`
93#[derive(Debug, Clone)]
94pub struct ConstDecl {
95    pub name: Ident,
96    pub value: ConstValue,
97    pub span: Span,
98}
99
100/// `var NAME: Type`
101#[derive(Debug, Clone)]
102pub struct VarDecl {
103    pub name: Ident,
104    pub ty: TypeExpr,
105    pub span: Span,
106}
107
108/// `type NAME = Type`
109#[derive(Debug, Clone)]
110pub struct TypeDecl {
111    pub name: Ident,
112    pub ty: TypeExpr,
113    pub span: Span,
114}
115
116/// `func NAME(params) { body }`
117/// User-defined helper function for reuse (like TLA+ operator definitions).
118/// Functions are pure and are inlined at call sites during compilation.
119#[derive(Debug, Clone)]
120pub struct FuncDecl {
121    pub name: Ident,
122    pub params: Vec<FuncParam>,
123    pub body: Expr,
124    pub span: Span,
125}
126
127/// A function parameter (untyped - types are inferred).
128#[derive(Debug, Clone)]
129pub struct FuncParam {
130    pub name: Ident,
131    pub span: Span,
132}
133
134/// `init { expr }`
135#[derive(Debug, Clone)]
136pub struct InitDecl {
137    pub body: Expr,
138    pub span: Span,
139}
140
141/// `action NAME(params) { body }`
142#[derive(Debug, Clone)]
143pub struct ActionDecl {
144    pub name: Ident,
145    pub params: Vec<Param>,
146    pub body: ActionBody,
147    pub span: Span,
148}
149
150/// Action body with requires and effects.
151#[derive(Debug, Clone)]
152pub struct ActionBody {
153    /// Guard conditions (`require expr`).
154    pub requires: Vec<Expr>,
155    /// Effect expression (state transition relation).
156    pub effect: Option<Expr>,
157    pub span: Span,
158}
159
160/// A parameter declaration.
161#[derive(Debug, Clone)]
162pub struct Param {
163    pub name: Ident,
164    pub ty: TypeExpr,
165    pub span: Span,
166}
167
168/// `invariant NAME { expr }`
169#[derive(Debug, Clone)]
170pub struct InvariantDecl {
171    pub name: Ident,
172    pub body: Expr,
173    pub span: Span,
174}
175
176/// `property NAME { expr }`
177#[derive(Debug, Clone)]
178pub struct PropertyDecl {
179    pub name: Ident,
180    pub body: Expr,
181    pub span: Span,
182}
183
184/// `fairness { constraints }`
185#[derive(Debug, Clone)]
186pub struct FairnessDecl {
187    pub constraints: Vec<FairnessConstraint>,
188    pub span: Span,
189}
190
191/// A fairness constraint.
192#[derive(Debug, Clone)]
193pub struct FairnessConstraint {
194    pub kind: FairnessKind,
195    pub action: Ident,
196    pub span: Span,
197}
198
199/// Kind of fairness constraint.
200#[derive(Debug, Clone, Copy, PartialEq, Eq)]
201pub enum FairnessKind {
202    Weak,
203    Strong,
204}
205
206/// A type expression.
207#[derive(Debug, Clone)]
208pub enum TypeExpr {
209    /// Named type (e.g., `Nat`, `AccountId`).
210    Named(Ident),
211    /// Set type `Set[T]`.
212    Set(Box<TypeExpr>, Span),
213    /// Sequence type `Seq[T]`.
214    Seq(Box<TypeExpr>, Span),
215    /// Dict type `dict[K, V]`.
216    Dict(Box<TypeExpr>, Box<TypeExpr>, Span),
217    /// Option type `Option[T]`.
218    Option(Box<TypeExpr>, Span),
219    /// Range type `lo..hi`.
220    Range(Box<Expr>, Box<Expr>, Span),
221    /// Tuple type `(T1, T2, ...)`.
222    Tuple(Vec<TypeExpr>, Span),
223}
224
225impl TypeExpr {
226    pub fn span(&self) -> Span {
227        match self {
228            TypeExpr::Named(id) => id.span,
229            TypeExpr::Set(_, span) => *span,
230            TypeExpr::Seq(_, span) => *span,
231            TypeExpr::Dict(_, _, span) => *span,
232            TypeExpr::Option(_, span) => *span,
233            TypeExpr::Range(_, _, span) => *span,
234            TypeExpr::Tuple(_, span) => *span,
235        }
236    }
237}
238
239/// An expression.
240#[derive(Debug, Clone)]
241pub struct Expr {
242    pub kind: ExprKind,
243    pub span: Span,
244}
245
246impl Expr {
247    pub fn new(kind: ExprKind, span: Span) -> Self {
248        Self { kind, span }
249    }
250}
251
252/// The kind of expression.
253#[derive(Debug, Clone)]
254pub enum ExprKind {
255    /// Boolean literal.
256    Bool(bool),
257    /// Integer literal.
258    Int(i64),
259    /// String literal.
260    String(String),
261    /// Identifier.
262    Ident(String),
263    /// Primed identifier (next-state variable).
264    Primed(String),
265
266    /// Binary operation.
267    Binary {
268        op: BinOp,
269        left: Box<Expr>,
270        right: Box<Expr>,
271    },
272    /// Unary operation.
273    Unary { op: UnaryOp, operand: Box<Expr> },
274
275    /// Function/set/sequence indexing `e[i]`.
276    Index { base: Box<Expr>, index: Box<Expr> },
277    /// Sequence slicing `e[lo..hi]`.
278    Slice {
279        base: Box<Expr>,
280        lo: Box<Expr>,
281        hi: Box<Expr>,
282    },
283    /// Field access `e.field`.
284    Field { base: Box<Expr>, field: Ident },
285    /// Function call `f(args)`.
286    Call { func: Box<Expr>, args: Vec<Expr> },
287
288    /// Set literal `{ a, b, c }` or empty `{}`.
289    SetLit(Vec<Expr>),
290    /// Sequence literal `[a, b, c]` or empty `[]`.
291    SeqLit(Vec<Expr>),
292    /// Tuple literal `(a, b, c)`.
293    TupleLit(Vec<Expr>),
294    /// Dict literal `{ key: value, ... }` where keys are expressions.
295    DictLit(Vec<(Expr, Expr)>),
296    /// Function literal `fn(x in S) => e`.
297    FnLit {
298        var: Ident,
299        domain: Box<Expr>,
300        body: Box<Expr>,
301    },
302
303    /// Set comprehension `{ e for x in S }` or `{ x in S if P }` or `{ e for x in S if P }`.
304    SetComprehension {
305        element: Box<Expr>,
306        var: Ident,
307        domain: Box<Expr>,
308        filter: Option<Box<Expr>>,
309    },
310
311    /// Record update `e with { field: value, ... }`.
312    RecordUpdate {
313        base: Box<Expr>,
314        updates: Vec<RecordFieldUpdate>,
315    },
316
317    /// Quantifier `forall x in S: P` or `exists x in S: P`.
318    Quantifier {
319        kind: QuantifierKind,
320        bindings: Vec<Binding>,
321        body: Box<Expr>,
322    },
323    /// Choose `choose x in S: P`.
324    Choose {
325        var: Ident,
326        domain: Box<Expr>,
327        predicate: Box<Expr>,
328    },
329    /// Fix `fix x: P` - picks an arbitrary value satisfying P (used for CHOOSE without domain).
330    Fix { var: Ident, predicate: Box<Expr> },
331
332    /// Let binding `let x = e1 in e2`.
333    Let {
334        var: Ident,
335        value: Box<Expr>,
336        body: Box<Expr>,
337    },
338    /// Conditional `if c then t else f`.
339    If {
340        cond: Box<Expr>,
341        then_branch: Box<Expr>,
342        else_branch: Box<Expr>,
343    },
344
345    /// Require statement (in action body).
346    Require(Box<Expr>),
347    /// Changes operator (explicit nondeterminism).
348    Changes(Ident),
349    /// Enabled predicate `enabled(Action)`.
350    Enabled(Ident),
351
352    /// Sequence head `head(seq)` - get first element.
353    SeqHead(Box<Expr>),
354    /// Sequence tail `tail(seq)` - get all but first element.
355    SeqTail(Box<Expr>),
356    /// Length `len(x)` - get length of sequence, set, or function.
357    Len(Box<Expr>),
358    /// Function keys `keys(f)` - get domain of function as set.
359    Keys(Box<Expr>),
360    /// Function values `values(f)` - get range of function as set.
361    Values(Box<Expr>),
362    /// Distributed union `union_all(S)` - union of all sets in S.
363    BigUnion(Box<Expr>),
364    /// Powerset `powerset(S)` - set of all subsets of S.
365    Powerset(Box<Expr>),
366
367    /// Temporal: `always P`.
368    Always(Box<Expr>),
369    /// Temporal: `eventually P`.
370    Eventually(Box<Expr>),
371    /// Temporal: `P leads_to Q`.
372    LeadsTo { left: Box<Expr>, right: Box<Expr> },
373
374    /// Range expression `lo..hi` (as value, not type).
375    Range { lo: Box<Expr>, hi: Box<Expr> },
376
377    /// Parenthesized expression (for preserving source).
378    Paren(Box<Expr>),
379}
380
381/// A record field update.
382#[derive(Debug, Clone)]
383pub enum RecordFieldUpdate {
384    /// Simple field update `field: value`.
385    Field { name: Ident, value: Expr },
386    /// Dynamic key update `[key]: value`.
387    Dynamic { key: Expr, value: Expr },
388}
389
390/// Binary operator.
391#[derive(Debug, Clone, Copy, PartialEq, Eq)]
392pub enum BinOp {
393    // Logical
394    And,
395    Or,
396    Implies,
397    Iff,
398
399    // Comparison
400    Eq,
401    Ne,
402    Lt,
403    Le,
404    Gt,
405    Ge,
406
407    // Arithmetic
408    Add,
409    Sub,
410    Mul,
411    Div,
412    Mod,
413
414    // Set
415    In,
416    NotIn,
417    Union,
418    Intersect,
419    Diff,
420    SubsetOf,
421
422    // Sequence
423    Concat,
424}
425
426impl BinOp {
427    /// Get the precedence of this operator (higher = binds tighter).
428    pub fn precedence(self) -> u8 {
429        match self {
430            BinOp::Iff => 1,
431            BinOp::Implies => 2,
432            BinOp::Or => 3,
433            BinOp::And => 4,
434            BinOp::Eq | BinOp::Ne | BinOp::Lt | BinOp::Le | BinOp::Gt | BinOp::Ge => 5,
435            BinOp::In | BinOp::NotIn | BinOp::SubsetOf => 5,
436            BinOp::Union | BinOp::Diff | BinOp::Concat => 6,
437            BinOp::Add | BinOp::Sub => 6,
438            BinOp::Intersect => 7,
439            BinOp::Mul | BinOp::Div | BinOp::Mod => 7,
440        }
441    }
442
443    /// Check if this operator is right-associative.
444    pub fn is_right_assoc(self) -> bool {
445        matches!(self, BinOp::Implies | BinOp::Iff)
446    }
447}
448
449/// Unary operator.
450#[derive(Debug, Clone, Copy, PartialEq, Eq)]
451pub enum UnaryOp {
452    Not,
453    Neg,
454}
455
456/// Quantifier kind.
457#[derive(Debug, Clone, Copy, PartialEq, Eq)]
458pub enum QuantifierKind {
459    Forall,
460    Exists,
461}
462
463/// A variable binding `x in S`.
464#[derive(Debug, Clone)]
465pub struct Binding {
466    pub var: Ident,
467    pub domain: Expr,
468    pub span: Span,
469}
470
471#[cfg(test)]
472mod tests {
473    use super::*;
474
475    #[test]
476    fn test_binop_precedence() {
477        // Multiplication binds tighter than addition
478        assert!(BinOp::Mul.precedence() > BinOp::Add.precedence());
479        // Addition binds tighter than comparison
480        assert!(BinOp::Add.precedence() > BinOp::Eq.precedence());
481        // Comparison binds tighter than and
482        assert!(BinOp::Eq.precedence() > BinOp::And.precedence());
483        // And binds tighter than or
484        assert!(BinOp::And.precedence() > BinOp::Or.precedence());
485        // Or binds tighter than implies
486        assert!(BinOp::Or.precedence() > BinOp::Implies.precedence());
487    }
488}
specl_syntax/ast.rs

specl_syntax/
ast.rs
