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    /// Module-level effect surface declaration. `None` is legacy/mixed
241    /// (no enforcement, soft warning emitted by `aver check`); `Some([])`
242    /// is explicit pure; `Some([...])` is a declared boundary — every
243    /// function's `! [...]` must be a subset (namespace-level entry like
244    /// `Disk` admits any `Disk.*` method).
245    pub effects: Option<Vec<String>>,
246    pub effects_line: Option<usize>,
247}
248
249#[derive(Debug, Clone, PartialEq)]
250pub enum VerifyGivenDomain {
251    /// Integer range domain in verify law: `1..50` (inclusive).
252    IntRange { start: i64, end: i64 },
253    /// Explicit domain values in verify law: `[v1, v2, ...]`.
254    Explicit(Vec<Spanned<Expr>>),
255}
256
257#[derive(Debug, Clone, PartialEq)]
258pub struct VerifyGiven {
259    pub name: String,
260    pub type_name: String,
261    pub domain: VerifyGivenDomain,
262}
263
264#[derive(Debug, Clone, PartialEq)]
265pub struct VerifyLaw {
266    pub name: String,
267    pub givens: Vec<VerifyGiven>,
268    /// Optional precondition for the law template, written as `when <bool-expr>`.
269    pub when: Option<Spanned<Expr>>,
270    /// Template assertion from source before given-domain expansion.
271    pub lhs: Spanned<Expr>,
272    pub rhs: Spanned<Expr>,
273    /// Per-sample substituted guards for `when`, aligned with `VerifyBlock.cases`.
274    pub sample_guards: Vec<Spanned<Expr>>,
275}
276
277/// Source range for AST nodes that need location tracking.
278/// Used by verify case spans: `cases[i] <-> case_spans[i]`.
279#[derive(Debug, Clone, PartialEq, Default)]
280pub struct SourceSpan {
281    pub line: usize,
282    pub col: usize,
283    pub end_line: usize,
284    pub end_col: usize,
285}
286
287#[derive(Debug, Clone, PartialEq)]
288pub enum VerifyKind {
289    Cases,
290    Law(Box<VerifyLaw>),
291}
292
293#[derive(Debug, Clone, PartialEq)]
294pub struct VerifyBlock {
295    pub fn_name: String,
296    pub line: usize,
297    pub cases: Vec<(Spanned<Expr>, Spanned<Expr>)>,
298    pub case_spans: Vec<SourceSpan>,
299    /// Per-case given bindings for law verify (empty for Cases kind).
300    pub case_givens: Vec<Vec<(String, Spanned<Expr>)>>,
301    /// Parallel to `cases`: `true` when the case was injected by
302    /// `aver verify --hostile` (boundary-value expansion of a law's
303    /// `given` clause), `false` for cases the user wrote directly.
304    /// Empty under non-hostile runs; the renderer uses this to label
305    /// failures as "outside declared given — encode as `when` if
306    /// precondition" when they only fail under the hostile expansion.
307    pub case_hostile_origins: Vec<bool>,
308    /// Parallel to `cases`: per-case hostile effect-profile assignment
309    /// for `--hostile` mode. Each inner Vec lists `(method, profile)`
310    /// pairs (e.g. `("Time.now", "frozen")`) that the runner installs
311    /// as oracle stubs before running the case, alongside any user-given
312    /// stubs. Empty inner Vec for cases that aren't effect-hostile-
313    /// expanded (declared, value-hostile-only, or fns without applicable
314    /// classified effects). All entries empty under non-hostile runs.
315    pub case_hostile_profiles: Vec<Vec<(String, String)>>,
316    pub kind: VerifyKind,
317    /// Oracle v1: `trace` keyword enables trace-aware assertions
318    /// (`.trace.*`, `.result`, event literals in `.contains` / match
319    /// patterns). Without it, a law checks only the return value, so
320    /// adding a debug print does not break proofs that do not care
321    /// about traces.
322    pub trace: bool,
323    /// Oracle v1: `given` clauses declared at the top of a cases-form
324    /// trace block. Law-form stores its givens inside `VerifyKind::Law`;
325    /// cases-form doesn't have that wrapper, so this field carries them
326    /// so the verify runner can build oracle-stub mappings from the
327    /// same data. Empty for non-trace or law-form blocks.
328    pub cases_givens: Vec<VerifyGiven>,
329}
330
331impl VerifyBlock {
332    /// Construct a VerifyBlock with default (zero) spans for each case.
333    /// Use when source location tracking is not needed (codegen, tests).
334    pub fn new_unspanned(
335        fn_name: String,
336        line: usize,
337        cases: Vec<(Spanned<Expr>, Spanned<Expr>)>,
338        kind: VerifyKind,
339    ) -> Self {
340        let case_spans = vec![SourceSpan::default(); cases.len()];
341        let case_hostile_origins = vec![false; cases.len()];
342        let case_hostile_profiles = vec![Vec::new(); cases.len()];
343        Self {
344            fn_name,
345            line,
346            cases,
347            case_spans,
348            case_givens: vec![],
349            case_hostile_origins,
350            case_hostile_profiles,
351            kind,
352            trace: false,
353            cases_givens: vec![],
354        }
355    }
356
357    pub fn iter_cases_with_spans(
358        &self,
359    ) -> impl Iterator<Item = (&(Spanned<Expr>, Spanned<Expr>), &SourceSpan)> {
360        debug_assert_eq!(self.cases.len(), self.case_spans.len());
361        self.cases.iter().zip(&self.case_spans)
362    }
363}
364
365#[derive(Debug, Clone, PartialEq)]
366pub struct DecisionBlock {
367    pub name: String,
368    pub line: usize,
369    pub date: String,
370    pub reason: String,
371    pub chosen: Spanned<DecisionImpact>,
372    pub rejected: Vec<Spanned<DecisionImpact>>,
373    pub impacts: Vec<Spanned<DecisionImpact>>,
374    pub author: Option<String>,
375}
376
377#[derive(Debug, Clone, PartialEq, Eq, Hash)]
378pub enum DecisionImpact {
379    Symbol(String),
380    Semantic(String),
381}
382
383impl DecisionImpact {
384    pub fn text(&self) -> &str {
385        match self {
386            DecisionImpact::Symbol(s) | DecisionImpact::Semantic(s) => s,
387        }
388    }
389
390    pub fn as_context_string(&self) -> String {
391        match self {
392            DecisionImpact::Symbol(s) => s.clone(),
393            DecisionImpact::Semantic(s) => format!("\"{}\"", s),
394        }
395    }
396}
397
398/// A variant in a sum type definition.
399/// e.g. `Circle(Float)` → `TypeVariant { name: "Circle", fields: ["Float"] }`
400#[derive(Debug, Clone, PartialEq)]
401pub struct TypeVariant {
402    pub name: String,
403    pub fields: Vec<String>, // type annotations (e.g. "Float", "String")
404}
405
406/// A user-defined type definition.
407#[derive(Debug, Clone, PartialEq)]
408pub enum TypeDef {
409    /// `type Shape` with variants Circle(Float), Rect(Float, Float), Point
410    Sum {
411        name: String,
412        variants: Vec<TypeVariant>,
413        line: usize,
414    },
415    /// `record User` with fields name: String, age: Int
416    Product {
417        name: String,
418        fields: Vec<(String, String)>,
419        line: usize,
420    },
421}
422
423#[derive(Debug, Clone, PartialEq)]
424pub enum TopLevel {
425    Module(Module),
426    FnDef(FnDef),
427    Verify(VerifyBlock),
428    Decision(DecisionBlock),
429    Stmt(Stmt),
430    TypeDef(TypeDef),
431}
aver/ast.rs

aver/
ast.rs
