aver/ast/mod.rs
1pub mod types;
2pub use types::Type;
3
4/// Source line number (1-based). 0 = synthetic/unknown.
5pub type SourceLine = usize;
6
7/// A `bool` that compares as always-equal. Used for `last_use` annotations
8/// on `Expr::Resolved` — metadata that should not affect AST equality
9/// (same pattern as `Spanned` ignoring `line` in its `PartialEq`).
10#[derive(Debug, Clone, Copy, Default)]
11pub struct AnnotBool(pub bool);
12
13impl PartialEq for AnnotBool {
14 fn eq(&self, _: &Self) -> bool {
15 true
16 }
17}
18
19impl From<bool> for AnnotBool {
20 fn from(b: bool) -> Self {
21 Self(b)
22 }
23}
24
25/// AST node with source location plus an optional inferred type.
26///
27/// Line-agnostic equality: two `Spanned` values are equal iff their inner
28/// nodes are equal, regardless of line or attached type. The type slot is a
29/// `OnceLock<Type>` populated by the type checker; backends that have not
30/// been migrated to consume it stay agnostic and continue inferring locally.
31/// `OnceLock` (rather than `OnceCell`) keeps `Spanned` `Sync`, which matters
32/// because parts of the AST live behind `Arc` and cross thread boundaries
33/// (e.g. parallel verify execution, REPL background tasks).
34#[derive(Debug)]
35pub struct Spanned<T> {
36 pub node: T,
37 pub line: SourceLine,
38 pub ty: std::sync::OnceLock<Type>,
39}
40
41// `OnceLock` does not derive `Clone` (the cell is invariant over `T`), so the
42// inner type is cloned manually.
43impl<T: Clone> Clone for Spanned<T> {
44 fn clone(&self) -> Self {
45 let ty = std::sync::OnceLock::new();
46 if let Some(t) = self.ty.get() {
47 let _ = ty.set(t.clone());
48 }
49 Self {
50 node: self.node.clone(),
51 line: self.line,
52 ty,
53 }
54 }
55}
56
57impl<T: PartialEq> PartialEq for Spanned<T> {
58 fn eq(&self, other: &Self) -> bool {
59 self.node == other.node
60 }
61}
62
63impl<T> Spanned<T> {
64 pub fn new(node: T, line: SourceLine) -> Self {
65 Self {
66 node,
67 line,
68 ty: std::sync::OnceLock::new(),
69 }
70 }
71
72 /// Create a Spanned with line=0 (synthetic/generated AST, no source location).
73 pub fn bare(node: T) -> Self {
74 Self::new(node, 0)
75 }
76
77 /// Record the inferred type for this node. No-op if a type is already set
78 /// (later inference passes must not contradict the first one).
79 pub fn set_ty(&self, ty: Type) {
80 let _ = self.ty.set(ty);
81 }
82
83 /// Inferred type for this node, if the type checker has visited it.
84 pub fn ty(&self) -> Option<&Type> {
85 self.ty.get()
86 }
87}
88
89#[derive(Debug, Clone, PartialEq)]
90pub enum Literal {
91 Int(i64),
92 /// An integer literal whose magnitude does not fit `i64`. Aver's `Int` is
93 /// arbitrary-precision (ℤ) at runtime, so such a literal is kept as its
94 /// decimal digit string (unsigned magnitude — any sign is the surrounding
95 /// negation/subtraction, exactly as for `Int`) and lowered to the same
96 /// arbitrary-precision construction `Int.n("…")` uses on every backend.
97 /// Small literals stay `Int(i64)` so the common path is byte-identical.
98 BigInt(String),
99 Float(f64),
100 Str(String),
101 Bool(bool),
102 Unit,
103}
104
105#[derive(Debug, Clone, Copy, PartialEq)]
106pub enum BinOp {
107 Add,
108 Sub,
109 Mul,
110 Div,
111 Eq,
112 Neq,
113 Lt,
114 Gt,
115 Lte,
116 Gte,
117}
118
119#[derive(Debug)]
120pub struct MatchArm {
121 pub pattern: Pattern,
122 pub body: Box<Spanned<Expr>>,
123 /// Per-arm slot table for the pattern's bindings, in pattern order.
124 /// Filled by the resolver pass; backend code reads from here
125 /// instead of doing a name lookup, so two arms with the same
126 /// binding name (e.g. `deadline` showing up in both `TaskCreated`
127 /// and `DeadlineSet` with different field types) get separate
128 /// slots without colliding in the function-level slot table.
129 /// Wildcard-position bindings (`_`) are stored as `u16::MAX` and
130 /// must never be read.
131 pub binding_slots: std::sync::OnceLock<Vec<u16>>,
132}
133
134// `OnceLock` doesn't derive Clone (cell is invariant over T); copy
135// the inner manually so the resolver's allocations survive the
136// `Arc::make_mut` clones that happen during multimodule flatten.
137impl Clone for MatchArm {
138 fn clone(&self) -> Self {
139 let binding_slots = std::sync::OnceLock::new();
140 if let Some(v) = self.binding_slots.get() {
141 let _ = binding_slots.set(v.clone());
142 }
143 Self {
144 pattern: self.pattern.clone(),
145 body: self.body.clone(),
146 binding_slots,
147 }
148 }
149}
150
151impl PartialEq for MatchArm {
152 fn eq(&self, other: &Self) -> bool {
153 self.pattern == other.pattern && self.body == other.body
154 }
155}
156
157impl MatchArm {
158 /// Build a fresh arm with no binding-slot stamp yet — resolver
159 /// fills `binding_slots` after slot allocation. Use this from any
160 /// site that synthesises an arm (parser, AST rewrites, effect
161 /// lifting, tests).
162 pub fn new(pattern: Pattern, body: Spanned<Expr>) -> Self {
163 Self {
164 pattern,
165 body: Box::new(body),
166 binding_slots: std::sync::OnceLock::new(),
167 }
168 }
169
170 pub fn new_boxed(pattern: Pattern, body: Box<Spanned<Expr>>) -> Self {
171 Self {
172 pattern,
173 body,
174 binding_slots: std::sync::OnceLock::new(),
175 }
176 }
177}
178
179#[derive(Debug, Clone, PartialEq)]
180pub enum Pattern {
181 Wildcard,
182 Literal(Literal),
183 Ident(String),
184 /// Empty list pattern: `[]`
185 EmptyList,
186 /// Cons-like list pattern: `[head, ..tail]`
187 Cons(String, String),
188 /// Tuple pattern: `(a, b)` / `(_, x)` / nested tuples.
189 Tuple(Vec<Pattern>),
190 /// Constructor pattern: fully-qualified name + list of binding names.
191 /// Built-ins: Result.Ok(x), Result.Err(x), Option.Some(x), Option.None.
192 /// User-defined: Shape.Circle(r), Shape.Rect(w, h), Shape.Point.
193 Constructor(String, Vec<String>),
194}
195
196#[derive(Debug, Clone, PartialEq)]
197pub enum StrPart {
198 Literal(String),
199 Parsed(Box<Spanned<Expr>>),
200}
201
202/// Data for a tail-call expression.
203#[derive(Debug, Clone, PartialEq)]
204pub struct TailCallData {
205 /// Target function name (self or mutual-recursive peer).
206 pub target: String,
207 /// Arguments to pass.
208 pub args: Vec<Spanned<Expr>>,
209}
210
211impl TailCallData {
212 pub fn new(target: String, args: Vec<Spanned<Expr>>) -> Self {
213 Self { target, args }
214 }
215}
216
217#[derive(Debug, Clone, PartialEq)]
218pub enum Expr {
219 Literal(Literal),
220 Ident(String),
221 Attr(Box<Spanned<Expr>>, String),
222 FnCall(Box<Spanned<Expr>>, Vec<Spanned<Expr>>),
223 BinOp(BinOp, Box<Spanned<Expr>>, Box<Spanned<Expr>>),
224 /// Unary numeric negation: `-x`. Operand must be numeric (`Int` or
225 /// `Float`); result is the same type. Used to be desugared in the
226 /// parser to `BinOp(Sub, Literal(Int(0)), x)`, which loses the IEEE
227 /// `-0.0` sign bit on `Float` operands and produces an `Int`/`Float`
228 /// mixed `BinOp` that backends had to recognise with pattern hacks.
229 Neg(Box<Spanned<Expr>>),
230 Match {
231 subject: Box<Spanned<Expr>>,
232 arms: Vec<MatchArm>,
233 },
234 Constructor(String, Option<Box<Spanned<Expr>>>),
235 ErrorProp(Box<Spanned<Expr>>),
236 InterpolatedStr(Vec<StrPart>),
237 List(Vec<Spanned<Expr>>),
238 Tuple(Vec<Spanned<Expr>>),
239 /// Map literal: `{"a" => 1, "b" => 2}`
240 MapLiteral(Vec<(Spanned<Expr>, Spanned<Expr>)>),
241 /// Record creation: `User(name = "Alice", age = 30)`
242 RecordCreate {
243 type_name: String,
244 fields: Vec<(String, Spanned<Expr>)>,
245 },
246 /// Record update: `User.update(base, field = newVal, ...)`
247 RecordUpdate {
248 type_name: String,
249 base: Box<Spanned<Expr>>,
250 updates: Vec<(String, Spanned<Expr>)>,
251 },
252 /// Tail-position call to a function in the same SCC (self or mutual recursion).
253 /// Produced by the TCO transform pass before type-checking.
254 /// Reuse info is populated by `ir::reuse::annotate_program_reuse`.
255 TailCall(Box<TailCallData>),
256 /// Independent product: `(a, b, c)!` or `(a, b, c)?!`.
257 /// Elements are independent effectful expressions evaluated with no guaranteed order.
258 /// `unwrap=true` (`?!`): all elements must be Result; unwraps Ok values, propagates first Err.
259 /// `unwrap=false` (`!`): returns raw tuple of results.
260 /// Produces a replay group (effects matched by branch_path + effect_occurrence + type + args).
261 IndependentProduct(Vec<Spanned<Expr>>, bool),
262 /// Compiled variable lookup: `env[last][slot]` — O(1) instead of HashMap scan.
263 /// Produced by the resolver pass for locals inside function bodies.
264 /// `last_use` is set by `ir::last_use` — when true, this is the final
265 /// reference to this slot and backends can move instead of copy.
266 Resolved {
267 slot: u16,
268 name: String,
269 last_use: AnnotBool,
270 },
271}
272
273#[derive(Debug, Clone, PartialEq)]
274pub enum Stmt {
275 Binding(String, Option<String>, Spanned<Expr>),
276 Expr(Spanned<Expr>),
277}
278
279#[derive(Debug, Clone, PartialEq)]
280pub enum FnBody {
281 Block(Vec<Stmt>),
282}
283
284impl FnBody {
285 pub fn from_expr(expr: Spanned<Expr>) -> Self {
286 Self::Block(vec![Stmt::Expr(expr)])
287 }
288
289 pub fn stmts(&self) -> &[Stmt] {
290 match self {
291 Self::Block(stmts) => stmts,
292 }
293 }
294
295 pub fn stmts_mut(&mut self) -> &mut Vec<Stmt> {
296 match self {
297 Self::Block(stmts) => stmts,
298 }
299 }
300
301 pub fn tail_expr(&self) -> Option<&Spanned<Expr>> {
302 match self.stmts().last() {
303 Some(Stmt::Expr(expr)) => Some(expr),
304 _ => None,
305 }
306 }
307
308 pub fn tail_expr_mut(&mut self) -> Option<&mut Spanned<Expr>> {
309 match self.stmts_mut().last_mut() {
310 Some(Stmt::Expr(expr)) => Some(expr),
311 _ => None,
312 }
313 }
314}
315
316/// Compile-time resolution metadata for a function body.
317/// Produced by `resolver::resolve_fn` — maps local variable names to slot indices
318/// so the VM can use `Vec<Value>` instead of `HashMap` lookups.
319#[derive(Debug, Clone, PartialEq)]
320pub struct FnResolution {
321 /// Total number of local slots needed (params + bindings in body).
322 pub local_count: u16,
323 /// Map from local variable name → slot index in the local `Slots` frame.
324 pub local_slots: std::sync::Arc<std::collections::HashMap<String, u16>>,
325 /// Aver type per slot index. Length == `local_count`. Built post-
326 /// typecheck so each entry pulls from the matching `Spanned::ty()`
327 /// stamp on the producer expression, plus pattern-binding shape
328 /// rules (`Result.Ok` → T, `Cons head` → list element, tuple item
329 /// → tuple element, …). Backends that need a typed local table
330 /// (the wasm-gc lowering uses one to declare each `local` with a
331 /// concrete `ValType`) consume this directly instead of re-deriving
332 /// the same information from patterns.
333 ///
334 /// Default `Type::Invalid` for unreachable / unstamped slots — every
335 /// real binding gets overwritten during the slot-types pass, so an
336 /// `Invalid` reaching the backend means the slot was never the
337 /// target of a binding (resolver counted but no expression
338 /// produced into it; usually a wildcard slot the backend skips).
339 pub local_slot_types: std::sync::Arc<Vec<Type>>,
340 /// Whether each slot may share an arena entry with another slot.
341 /// Length == `local_count`. Set by `ir::alias::annotate_program_alias_slots`
342 /// post-`last_use`. Backends that have a `mem::take`-style fast path
343 /// for `Vector.set` / `Map.set` (the VM's `CALL_BUILTIN_OWNED` mask
344 /// plus the fused `VECTOR_SET_OR_KEEP`) must NOT take the fast path
345 /// on a flagged slot — rewriting the shared arena entry would
346 /// mutate the other binding too. Wasm-gc may use it to skip
347 /// clone-on-write when the slot is provably non-aliased; otherwise
348 /// it falls back to `array.copy` + `array.set` on the copy.
349 ///
350 /// Default `false` for slots the analysis hasn't reached (anything
351 /// pre-`last_use`, REPL, partial pipelines), which is the safe-but-
352 /// slow choice everywhere except the VM fast path.
353 pub aliased_slots: std::sync::Arc<Vec<bool>>,
354}
355
356#[derive(Debug, Clone, PartialEq)]
357pub struct FnDef {
358 pub name: String,
359 pub line: usize,
360 pub params: Vec<(String, String)>,
361 pub return_type: String,
362 pub effects: Vec<Spanned<String>>,
363 pub desc: Option<String>,
364 pub body: std::sync::Arc<FnBody>,
365 /// `None` for unresolved (REPL, module loading).
366 pub resolution: Option<FnResolution>,
367}
368
369#[derive(Debug, Clone, PartialEq)]
370pub struct Module {
371 pub name: String,
372 pub line: usize,
373 pub depends: Vec<String>,
374 pub exposes: Vec<String>,
375 pub exposes_opaque: Vec<String>,
376 pub exposes_line: Option<usize>,
377 pub intent: String,
378 /// Module-level effect surface declaration. `None` is legacy/mixed
379 /// (no enforcement, soft warning emitted by `aver check`); `Some([])`
380 /// is explicit pure; `Some([...])` is a declared boundary — every
381 /// function's `! [...]` must be a subset (namespace-level entry like
382 /// `Disk` admits any `Disk.*` method).
383 pub effects: Option<Vec<String>>,
384 pub effects_line: Option<usize>,
385}
386
387#[derive(Debug, Clone, PartialEq)]
388pub enum VerifyGivenDomain {
389 /// Integer range domain in verify law: `1..50` (inclusive).
390 IntRange { start: i64, end: i64 },
391 /// Explicit domain values in verify law: `[v1, v2, ...]`.
392 Explicit(Vec<Spanned<Expr>>),
393}
394
395#[derive(Debug, Clone, PartialEq)]
396pub struct VerifyGiven {
397 pub name: String,
398 pub type_name: String,
399 pub domain: VerifyGivenDomain,
400}
401
402#[derive(Debug, Clone, PartialEq)]
403pub struct VerifyLaw {
404 pub name: String,
405 pub givens: Vec<VerifyGiven>,
406 /// Optional precondition for the law template, written as `when <bool-expr>`.
407 pub when: Option<Spanned<Expr>>,
408 /// Template assertion from source before given-domain expansion.
409 pub lhs: Spanned<Expr>,
410 pub rhs: Spanned<Expr>,
411 /// Per-sample substituted guards for `when`, aligned with `VerifyBlock.cases`.
412 pub sample_guards: Vec<Spanned<Expr>>,
413}
414
415/// Source range for AST nodes that need location tracking.
416/// Used by verify case spans: `cases[i] <-> case_spans[i]`.
417#[derive(Debug, Clone, PartialEq, Default)]
418pub struct SourceSpan {
419 pub line: usize,
420 pub col: usize,
421 pub end_line: usize,
422 pub end_col: usize,
423}
424
425#[derive(Debug, Clone, PartialEq)]
426pub enum VerifyKind {
427 Cases,
428 Law(Box<VerifyLaw>),
429}
430
431#[derive(Debug, Clone, PartialEq)]
432pub struct VerifyBlock {
433 pub fn_name: String,
434 pub line: usize,
435 pub cases: Vec<(Spanned<Expr>, Spanned<Expr>)>,
436 pub case_spans: Vec<SourceSpan>,
437 /// Per-case given bindings for law verify (empty for Cases kind).
438 pub case_givens: Vec<Vec<(String, Spanned<Expr>)>>,
439 /// Parallel to `cases`: `true` when the case was injected by
440 /// `aver verify --hostile` (boundary-value expansion of a law's
441 /// `given` clause), `false` for cases the user wrote directly.
442 /// Empty under non-hostile runs; the renderer uses this to label
443 /// failures as "outside declared given — encode as `when` if
444 /// precondition" when they only fail under the hostile expansion.
445 pub case_hostile_origins: Vec<bool>,
446 /// Parallel to `cases`: per-case hostile effect-profile assignment
447 /// for `--hostile` mode. Each inner Vec lists `(method, profile)`
448 /// pairs (e.g. `("Time.now", "frozen")`) that the runner installs
449 /// as oracle stubs before running the case, alongside any user-given
450 /// stubs. Empty inner Vec for cases that aren't effect-hostile-
451 /// expanded (declared, value-hostile-only, or fns without applicable
452 /// classified effects). All entries empty under non-hostile runs.
453 pub case_hostile_profiles: Vec<Vec<(String, String)>>,
454 /// Parallel to `cases`: `true` when `aver verify --hostile` has
455 /// injected a reverse-order twin of an earlier case. The twin
456 /// shares LHS/RHS/given/profile with its forward sibling — only
457 /// the execution order of independent-product branches
458 /// (`(a, b)!` lowers to `CALL_PAR`) is flipped. A pure law claims
459 /// its branches are independent, so the twin must produce the
460 /// same result; divergence proves the claim doesn't hold under
461 /// the stub map and surfaces as `verify-hostile-order-mismatch`.
462 /// All entries `false` under non-hostile runs.
463 pub case_reverse_order: Vec<bool>,
464 pub kind: VerifyKind,
465 /// Oracle v1: `trace` keyword enables trace-aware assertions
466 /// (`.trace.*`, `.result`, event literals in `.contains` / match
467 /// patterns). Without it, a law checks only the return value, so
468 /// adding a debug print does not break proofs that do not care
469 /// about traces.
470 pub trace: bool,
471 /// Oracle v1: `given` clauses declared at the top of a cases-form
472 /// trace block. Law-form stores its givens inside `VerifyKind::Law`;
473 /// cases-form doesn't have that wrapper, so this field carries them
474 /// so the verify runner can build oracle-stub mappings from the
475 /// same data. Empty for non-trace or law-form blocks.
476 pub cases_givens: Vec<VerifyGiven>,
477}
478
479impl VerifyBlock {
480 /// Construct a VerifyBlock with default (zero) spans for each case.
481 /// Use when source location tracking is not needed (codegen, tests).
482 pub fn new_unspanned(
483 fn_name: String,
484 line: usize,
485 cases: Vec<(Spanned<Expr>, Spanned<Expr>)>,
486 kind: VerifyKind,
487 ) -> Self {
488 let case_spans = vec![SourceSpan::default(); cases.len()];
489 let case_hostile_origins = vec![false; cases.len()];
490 let case_hostile_profiles = vec![Vec::new(); cases.len()];
491 let case_reverse_order = vec![false; cases.len()];
492 Self {
493 fn_name,
494 line,
495 cases,
496 case_spans,
497 case_givens: vec![],
498 case_hostile_origins,
499 case_hostile_profiles,
500 case_reverse_order,
501 kind,
502 trace: false,
503 cases_givens: vec![],
504 }
505 }
506
507 pub fn iter_cases_with_spans(
508 &self,
509 ) -> impl Iterator<Item = (&(Spanned<Expr>, Spanned<Expr>), &SourceSpan)> {
510 debug_assert_eq!(self.cases.len(), self.case_spans.len());
511 self.cases.iter().zip(&self.case_spans)
512 }
513}
514
515#[derive(Debug, Clone, PartialEq)]
516pub struct DecisionBlock {
517 pub name: String,
518 pub line: usize,
519 pub date: String,
520 pub reason: String,
521 pub chosen: Spanned<DecisionImpact>,
522 pub rejected: Vec<Spanned<DecisionImpact>>,
523 pub impacts: Vec<Spanned<DecisionImpact>>,
524 pub author: Option<String>,
525}
526
527#[derive(Debug, Clone, PartialEq, Eq, Hash)]
528pub enum DecisionImpact {
529 Symbol(String),
530 Semantic(String),
531}
532
533impl DecisionImpact {
534 pub fn text(&self) -> &str {
535 match self {
536 DecisionImpact::Symbol(s) | DecisionImpact::Semantic(s) => s,
537 }
538 }
539
540 pub fn as_context_string(&self) -> String {
541 match self {
542 DecisionImpact::Symbol(s) => s.clone(),
543 DecisionImpact::Semantic(s) => format!("\"{}\"", s),
544 }
545 }
546}
547
548/// A variant in a sum type definition.
549/// e.g. `Circle(Float)` → `TypeVariant { name: "Circle", fields: ["Float"] }`
550#[derive(Debug, Clone, PartialEq)]
551pub struct TypeVariant {
552 pub name: String,
553 pub fields: Vec<String>, // type annotations (e.g. "Float", "String")
554}
555
556/// A user-defined type definition.
557#[derive(Debug, Clone, PartialEq)]
558pub enum TypeDef {
559 /// `type Shape` with variants Circle(Float), Rect(Float, Float), Point
560 Sum {
561 name: String,
562 variants: Vec<TypeVariant>,
563 line: usize,
564 },
565 /// `record User` with fields name: String, age: Int
566 Product {
567 name: String,
568 fields: Vec<(String, String)>,
569 line: usize,
570 },
571}
572
573#[derive(Debug, Clone, PartialEq)]
574pub enum TopLevel {
575 Module(Module),
576 FnDef(FnDef),
577 Verify(VerifyBlock),
578 Decision(DecisionBlock),
579 Stmt(Stmt),
580 TypeDef(TypeDef),
581}