aver/
ast.rs

1/// Source line number (1-based). 0 = synthetic/unknown.
2pub type SourceLine = usize;
3
4/// A `bool` that compares as always-equal. Used for `last_use` annotations
5/// on `Expr::Resolved` — metadata that should not affect AST equality
6/// (same pattern as `Spanned` ignoring `line` in its `PartialEq`).
7#[derive(Debug, Clone, Copy, Default)]
8pub struct AnnotBool(pub bool);
9
10impl PartialEq for AnnotBool {
11    fn eq(&self, _: &Self) -> bool {
12        true
13    }
14}
15
16impl From<bool> for AnnotBool {
17    fn from(b: bool) -> Self {
18        Self(b)
19    }
20}
21
22/// AST node with source location. Line-agnostic equality: two `Spanned` values
23/// are equal iff their inner nodes are equal, regardless of line.
24#[derive(Debug, Clone)]
25pub struct Spanned<T> {
26    pub node: T,
27    pub line: SourceLine,
28}
29
30impl<T: PartialEq> PartialEq for Spanned<T> {
31    fn eq(&self, other: &Self) -> bool {
32        self.node == other.node
33    }
34}
35
36impl<T> Spanned<T> {
37    pub fn new(node: T, line: SourceLine) -> Self {
38        Self { node, line }
39    }
40
41    /// Create a Spanned with line=0 (synthetic/generated AST, no source location).
42    pub fn bare(node: T) -> Self {
43        Self { node, line: 0 }
44    }
45}
46
47#[derive(Debug, Clone, PartialEq)]
48pub enum Literal {
49    Int(i64),
50    Float(f64),
51    Str(String),
52    Bool(bool),
53    Unit,
54}
55
56#[derive(Debug, Clone, Copy, PartialEq)]
57pub enum BinOp {
58    Add,
59    Sub,
60    Mul,
61    Div,
62    Eq,
63    Neq,
64    Lt,
65    Gt,
66    Lte,
67    Gte,
68}
69
70#[derive(Debug, Clone, PartialEq)]
71pub struct MatchArm {
72    pub pattern: Pattern,
73    pub body: Box<Spanned<Expr>>,
74}
75
76#[derive(Debug, Clone, PartialEq)]
77pub enum Pattern {
78    Wildcard,
79    Literal(Literal),
80    Ident(String),
81    /// Empty list pattern: `[]`
82    EmptyList,
83    /// Cons-like list pattern: `[head, ..tail]`
84    Cons(String, String),
85    /// Tuple pattern: `(a, b)` / `(_, x)` / nested tuples.
86    Tuple(Vec<Pattern>),
87    /// Constructor pattern: fully-qualified name + list of binding names.
88    /// Built-ins: Result.Ok(x), Result.Err(x), Option.Some(x), Option.None.
89    /// User-defined: Shape.Circle(r), Shape.Rect(w, h), Shape.Point.
90    Constructor(String, Vec<String>),
91}
92
93#[derive(Debug, Clone, PartialEq)]
94pub enum StrPart {
95    Literal(String),
96    Parsed(Box<Spanned<Expr>>),
97}
98
99/// Data for a tail-call expression.
100#[derive(Debug, Clone, PartialEq)]
101pub struct TailCallData {
102    /// Target function name (self or mutual-recursive peer).
103    pub target: String,
104    /// Arguments to pass.
105    pub args: Vec<Spanned<Expr>>,
106}
107
108impl TailCallData {
109    pub fn new(target: String, args: Vec<Spanned<Expr>>) -> Self {
110        Self { target, args }
111    }
112}
113
114#[derive(Debug, Clone, PartialEq)]
115pub enum Expr {
116    Literal(Literal),
117    Ident(String),
118    Attr(Box<Spanned<Expr>>, String),
119    FnCall(Box<Spanned<Expr>>, Vec<Spanned<Expr>>),
120    BinOp(BinOp, Box<Spanned<Expr>>, Box<Spanned<Expr>>),
121    Match {
122        subject: Box<Spanned<Expr>>,
123        arms: Vec<MatchArm>,
124    },
125    Constructor(String, Option<Box<Spanned<Expr>>>),
126    ErrorProp(Box<Spanned<Expr>>),
127    InterpolatedStr(Vec<StrPart>),
128    List(Vec<Spanned<Expr>>),
129    Tuple(Vec<Spanned<Expr>>),
130    /// Map literal: `{"a" => 1, "b" => 2}`
131    MapLiteral(Vec<(Spanned<Expr>, Spanned<Expr>)>),
132    /// Record creation: `User(name = "Alice", age = 30)`
133    RecordCreate {
134        type_name: String,
135        fields: Vec<(String, Spanned<Expr>)>,
136    },
137    /// Record update: `User.update(base, field = newVal, ...)`
138    RecordUpdate {
139        type_name: String,
140        base: Box<Spanned<Expr>>,
141        updates: Vec<(String, Spanned<Expr>)>,
142    },
143    /// Tail-position call to a function in the same SCC (self or mutual recursion).
144    /// Produced by the TCO transform pass before type-checking.
145    /// Reuse info is populated by `ir::reuse::annotate_program_reuse`.
146    TailCall(Box<TailCallData>),
147    /// Independent product: `(a, b, c)!` or `(a, b, c)?!`.
148    /// Elements are independent effectful expressions evaluated with no guaranteed order.
149    /// `unwrap=true` (`?!`): all elements must be Result; unwraps Ok values, propagates first Err.
150    /// `unwrap=false` (`!`): returns raw tuple of results.
151    /// Produces a replay group (effects matched by branch_path + effect_occurrence + type + args).
152    IndependentProduct(Vec<Spanned<Expr>>, bool),
153    /// Compiled variable lookup: `env[last][slot]` — O(1) instead of HashMap scan.
154    /// Produced by the resolver pass for locals inside function bodies.
155    /// `last_use` is set by `ir::last_use` — when true, this is the final
156    /// reference to this slot and backends can move instead of copy.
157    Resolved {
158        slot: u16,
159        name: String,
160        last_use: AnnotBool,
161    },
162}
163
164#[derive(Debug, Clone, PartialEq)]
165pub enum Stmt {
166    Binding(String, Option<String>, Spanned<Expr>),
167    Expr(Spanned<Expr>),
168}
169
170#[derive(Debug, Clone, PartialEq)]
171pub enum FnBody {
172    Block(Vec<Stmt>),
173}
174
175impl FnBody {
176    pub fn from_expr(expr: Spanned<Expr>) -> Self {
177        Self::Block(vec![Stmt::Expr(expr)])
178    }
179
180    pub fn stmts(&self) -> &[Stmt] {
181        match self {
182            Self::Block(stmts) => stmts,
183        }
184    }
185
186    pub fn stmts_mut(&mut self) -> &mut Vec<Stmt> {
187        match self {
188            Self::Block(stmts) => stmts,
189        }
190    }
191
192    pub fn tail_expr(&self) -> Option<&Spanned<Expr>> {
193        match self.stmts().last() {
194            Some(Stmt::Expr(expr)) => Some(expr),
195            _ => None,
196        }
197    }
198
199    pub fn tail_expr_mut(&mut self) -> Option<&mut Spanned<Expr>> {
200        match self.stmts_mut().last_mut() {
201            Some(Stmt::Expr(expr)) => Some(expr),
202            _ => None,
203        }
204    }
205}
206
207/// Compile-time resolution metadata for a function body.
208/// Produced by `resolver::resolve_fn` — maps local variable names to slot indices
209/// so the VM can use `Vec<Value>` instead of `HashMap` lookups.
210#[derive(Debug, Clone, PartialEq)]
211pub struct FnResolution {
212    /// Total number of local slots needed (params + bindings in body).
213    pub local_count: u16,
214    /// Map from local variable name → slot index in the local `Slots` frame.
215    pub local_slots: std::sync::Arc<std::collections::HashMap<String, u16>>,
216}
217
218#[derive(Debug, Clone, PartialEq)]
219pub struct FnDef {
220    pub name: String,
221    pub line: usize,
222    pub params: Vec<(String, String)>,
223    pub return_type: String,
224    pub effects: Vec<Spanned<String>>,
225    pub desc: Option<String>,
226    pub body: std::sync::Arc<FnBody>,
227    /// `None` for unresolved (REPL, module loading).
228    pub resolution: Option<FnResolution>,
229}
230
231#[derive(Debug, Clone, PartialEq)]
232pub struct Module {
233    pub name: String,
234    pub line: usize,
235    pub depends: Vec<String>,
236    pub exposes: Vec<String>,
237    pub exposes_opaque: Vec<String>,
238    pub exposes_line: Option<usize>,
239    pub intent: String,
240}
241
242#[derive(Debug, Clone, PartialEq)]
243pub enum VerifyGivenDomain {
244    /// Integer range domain in verify law: `1..50` (inclusive).
245    IntRange { start: i64, end: i64 },
246    /// Explicit domain values in verify law: `[v1, v2, ...]`.
247    Explicit(Vec<Spanned<Expr>>),
248}
249
250#[derive(Debug, Clone, PartialEq)]
251pub struct VerifyGiven {
252    pub name: String,
253    pub type_name: String,
254    pub domain: VerifyGivenDomain,
255}
256
257#[derive(Debug, Clone, PartialEq)]
258pub struct VerifyLaw {
259    pub name: String,
260    pub givens: Vec<VerifyGiven>,
261    /// Optional precondition for the law template, written as `when <bool-expr>`.
262    pub when: Option<Spanned<Expr>>,
263    /// Template assertion from source before given-domain expansion.
264    pub lhs: Spanned<Expr>,
265    pub rhs: Spanned<Expr>,
266    /// Per-sample substituted guards for `when`, aligned with `VerifyBlock.cases`.
267    pub sample_guards: Vec<Spanned<Expr>>,
268}
269
270/// Source range for AST nodes that need location tracking.
271/// Used by verify case spans: `cases[i] <-> case_spans[i]`.
272#[derive(Debug, Clone, PartialEq, Default)]
273pub struct SourceSpan {
274    pub line: usize,
275    pub col: usize,
276    pub end_line: usize,
277    pub end_col: usize,
278}
279
280#[derive(Debug, Clone, PartialEq)]
281pub enum VerifyKind {
282    Cases,
283    Law(Box<VerifyLaw>),
284}
285
286#[derive(Debug, Clone, PartialEq)]
287pub struct VerifyBlock {
288    pub fn_name: String,
289    pub line: usize,
290    pub cases: Vec<(Spanned<Expr>, Spanned<Expr>)>,
291    pub case_spans: Vec<SourceSpan>,
292    /// Per-case given bindings for law verify (empty for Cases kind).
293    pub case_givens: Vec<Vec<(String, Spanned<Expr>)>>,
294    pub kind: VerifyKind,
295    /// Oracle v1: `trace` keyword enables trace-aware assertions
296    /// (`.trace.*`, `.result`, event literals in `.contains` / match
297    /// patterns). Without it, a law checks only the return value, so
298    /// adding a debug print does not break proofs that do not care
299    /// about traces.
300    pub trace: bool,
301    /// Oracle v1: `given` clauses declared at the top of a cases-form
302    /// trace block. Law-form stores its givens inside `VerifyKind::Law`;
303    /// cases-form doesn't have that wrapper, so this field carries them
304    /// so the verify runner can build oracle-stub mappings from the
305    /// same data. Empty for non-trace or law-form blocks.
306    pub cases_givens: Vec<VerifyGiven>,
307}
308
309impl VerifyBlock {
310    /// Construct a VerifyBlock with default (zero) spans for each case.
311    /// Use when source location tracking is not needed (codegen, tests).
312    pub fn new_unspanned(
313        fn_name: String,
314        line: usize,
315        cases: Vec<(Spanned<Expr>, Spanned<Expr>)>,
316        kind: VerifyKind,
317    ) -> Self {
318        let case_spans = vec![SourceSpan::default(); cases.len()];
319        Self {
320            fn_name,
321            line,
322            cases,
323            case_spans,
324            case_givens: vec![],
325            kind,
326            trace: false,
327            cases_givens: vec![],
328        }
329    }
330
331    pub fn iter_cases_with_spans(
332        &self,
333    ) -> impl Iterator<Item = (&(Spanned<Expr>, Spanned<Expr>), &SourceSpan)> {
334        debug_assert_eq!(self.cases.len(), self.case_spans.len());
335        self.cases.iter().zip(&self.case_spans)
336    }
337}
338
339#[derive(Debug, Clone, PartialEq)]
340pub struct DecisionBlock {
341    pub name: String,
342    pub line: usize,
343    pub date: String,
344    pub reason: String,
345    pub chosen: Spanned<DecisionImpact>,
346    pub rejected: Vec<Spanned<DecisionImpact>>,
347    pub impacts: Vec<Spanned<DecisionImpact>>,
348    pub author: Option<String>,
349}
350
351#[derive(Debug, Clone, PartialEq, Eq, Hash)]
352pub enum DecisionImpact {
353    Symbol(String),
354    Semantic(String),
355}
356
357impl DecisionImpact {
358    pub fn text(&self) -> &str {
359        match self {
360            DecisionImpact::Symbol(s) | DecisionImpact::Semantic(s) => s,
361        }
362    }
363
364    pub fn as_context_string(&self) -> String {
365        match self {
366            DecisionImpact::Symbol(s) => s.clone(),
367            DecisionImpact::Semantic(s) => format!("\"{}\"", s),
368        }
369    }
370}
371
372/// A variant in a sum type definition.
373/// e.g. `Circle(Float)` → `TypeVariant { name: "Circle", fields: ["Float"] }`
374#[derive(Debug, Clone, PartialEq)]
375pub struct TypeVariant {
376    pub name: String,
377    pub fields: Vec<String>, // type annotations (e.g. "Float", "String")
378}
379
380/// A user-defined type definition.
381#[derive(Debug, Clone, PartialEq)]
382pub enum TypeDef {
383    /// `type Shape` with variants Circle(Float), Rect(Float, Float), Point
384    Sum {
385        name: String,
386        variants: Vec<TypeVariant>,
387        line: usize,
388    },
389    /// `record User` with fields name: String, age: Int
390    Product {
391        name: String,
392        fields: Vec<(String, String)>,
393        line: usize,
394    },
395}
396
397#[derive(Debug, Clone, PartialEq)]
398pub enum TopLevel {
399    Module(Module),
400    FnDef(FnDef),
401    Verify(VerifyBlock),
402    Decision(DecisionBlock),
403    Stmt(Stmt),
404    TypeDef(TypeDef),
405}
aver/ast.rs

aver/
ast.rs
