Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion .claude/commands/aver.md
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,8 @@ Rules:
- **arm bodies must start on the same line as `->`.** A multi-line body is a parse error; extract a helper function instead
- no colon after the subject
- no guards
- list patterns: `[]` and `[head, ..tail]` (the `..` rest must be named)
- list patterns: `[]`, `[head, ..tail]`, `[a, b]` (exactly two), `[a, b, ..rest]` (at least two), `[..all]`; the `..` rest comes last and must be named (or `_`)
- patterns nest: constructor fields and list or tuple elements are patterns, so `Option.Some(0)`, `Result.Ok("x")`, `Shape.Rect(0, h)`, `Option.Some(Option.None)` and `[Option.Some(x), ..rest]` all work. A literal never covers its constructor: after `Option.Some(0)` you still need `Option.Some(n)` or `Option.Some(_)`
- tuple patterns: `(a, b)`
- constructor patterns are always qualified: `Result.Ok`, `Option.None`, `Shape.Circle`
- literal patterns: `253 -> …` (`Int`), `"verack" -> …` (`String`), `1.5 -> …` (`Float`), `true` / `false` (`Bool`). An `Int` / `String` / `Float` match still needs a trailing `_ ->` or identifier arm. `-1 ->` is a parse error (there are no negative literal patterns), and so is an integer beyond 64 bits
Expand Down
2 changes: 1 addition & 1 deletion AGENTS.md
Original file line number Diff line number Diff line change
Expand Up @@ -230,7 +230,7 @@ The `src/lib.rs` exports all modules as `pub mod` so integration tests can acces
| `LexerError` | lexer.rs | Carry `msg`, `line`, `col`; formatted as `"Lexer error [L:C]: msg"` |
| `Literal` | ast.rs | `Int(i64)`, `Float(f64)`, `Str(String)`, `Bool(bool)` |
| `BinOp` | ast.rs | Arithmetic and comparison operators as enum variants |
| `Pattern` | ast.rs | Match arm pattern: `Wildcard`, `Literal`, `Ident`, `EmptyList`, `Cons`, `Constructor` |
| `Pattern` | ast.rs | Match arm pattern: `Wildcard`, `Literal`, `Ident`, `EmptyList`, `Cons`, `Tuple`, `Constructor`, plus the source-only `ConstructorNested` and `List` that `src/ir/nested_patterns.rs` compiles into nested flat matches inside the front door (after the program is checked as written), so no backend or proof exporter sees them |
| `StrPart` | ast.rs | Piece of an interpolated string: `Literal(String)` or `Parsed(Box<Expr>)` |
| `Expr` | ast.rs | Every expression form: `Literal`, `Ident`, `Resolved(u16)`, `Attr`, `FnCall`, `BinOp`, `Match`, `Constructor`, `ErrorProp`, `InterpolatedStr`, `List(Vec<Expr>)`, `Tuple(Vec<Expr>)`, `MapLiteral(Vec<(Expr, Expr)>)`, `RecordCreate { type_name, fields }`, `RecordUpdate { type_name, base, updates }`, `TailCall(Box<(String, Vec<Expr>)>)` |
| `Stmt` | ast.rs | `Binding(name, Option<type_ann>, expr)`, `Expr(expr)` |
Expand Down
12 changes: 12 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,18 @@ All notable changes to Aver are documented here. Starting with 0.10.0, minor rel

## Unreleased

### Added — literal, constructor and list patterns at any depth

- **A constructor pattern takes patterns in its fields.** `Option.Some(0)`, `Result.Ok("x")`, `Result.Err(404)`, `Shape.Rect(0, h)`, `Option.Some(true)`, `Option.Some(Option.None)` and `Option.Some((0, _))` are patterns now; before, each field had to be a name or `_`. The literals are the ones a top-level arm accepts: `Int`, `String`, `Float` and `Bool`.
- **List patterns name any number of leading elements.** `[a]` and `[a, b]` match lists of exactly that length, `[a, b, ..rest]` a list of at least two, `[..all]` any list. Elements are patterns: `[0, ..rest]`, `[Option.Some(x), ..rest]`. `[]` and `[h, ..t]` are unchanged.
- **The checker reads them.** A literal field never covers its constructor, so `Option.Some(0)` and `Option.None` alone are reported as `Non-exhaustive match: missing pattern Option.Some(_)`. List patterns cover by length (`missing pattern [_, _, _, .._]`). An arm no value can reach is an error, including one that several earlier arms cover only together, such as `Option.Some(_)` after `Option.Some(true)` and `Option.Some(false)`. A literal of the wrong type (`Option.Some("x")` on an `Option<Int>`) and a list pattern on a value that is not a list are errors.
- **Every backend runs the same match.** The compiler turns such a match into nested ordinary matches right after checking it, so the VM, generated Rust, wasm-gc, `wasip2` and the Lean export all read the same program. A `match` that uses these patterns inside a `yield` function is refused for now; move it into a helper function.
- **`aver format` prints match patterns in one spelling:** `[a, b, ..rest]`, `Option.Some(0)`, `(x, _)`.

### Fixed — a spliced call no longer reads a slot of the function it came from

- **A one-parameter function whose body matches, called with a literal record or constructor, runs right on every backend.** The compiler copies such a body into the caller; when the body held another `match` that binds a name, the copy used a local slot of the original function, which crashed the VM (`index out of bounds`), failed wasm-gc validation, or overwrote an unrelated local of the caller. Such a body is now called instead of copied.

### Migration — the process layer, version 2

The generated loop is now written from the program's source alone, and the manifest keeps only deployment. Every program that used `answer =`, the job seam or `[run]` has to be migrated; a manifest that still has any of them is refused with the repair. A program that writes its own loop over `Work` and `Wait.poll` is unaffected.
Expand Down
42 changes: 42 additions & 0 deletions docs/language.md
Original file line number Diff line number Diff line change
Expand Up @@ -100,18 +100,60 @@ match value
x -> "bound to {x}" // identifier binding
[] -> "empty list" // empty list
[h, ..t] -> "head {h}, {List.len(t)} more" // list cons
[a, b] -> "exactly two" // fixed-length list
[a, b, ..rest] -> "at least two" // leading elements + rest
Result.Ok(v) -> "success: {v}" // constructor
Result.Err(e) -> "error: {e}"
Shape.Circle(r) -> "circle r={r}"
Shape.Point -> "point"
(a, b) -> "pair: {a}, {b}" // tuple destructuring
((x, y), z) -> "nested: {x}" // nested tuple
Option.Some(0) -> "zero" // literal inside a constructor
Result.Ok(Option.Some(v)) -> "{v}" // constructor inside a constructor
```

Constructor patterns are always qualified (`Result.Ok`, `Option.None`, `Shape.Circle`). Records cannot be destructured positionally in a pattern. Bind the whole record and use field access (`user.name`, `user.age`).

A match may nest inside a match arm. The arm body must follow `->` on the same line, so move a complex expression into a named function.

### Nested patterns

Every field of a constructor pattern and every element of a list or tuple pattern is itself a pattern, at any depth. A literal, a constructor, a tuple or a list pattern may stand where a name may:

```aver
fn describe(o: Option<Int>) -> String
? "Zero and one get words; other values are printed."
match o
Option.Some(0) -> "zero"
Option.Some(1) -> "one"
Option.Some(n) -> "{n}"
Option.None -> "nothing"

fn area(s: Shape) -> Int
? "A rectangle with a zero side is empty."
match s
Shape.Rect(0, _) -> 0
Shape.Rect(_, 0) -> 0
Shape.Rect(w, h) -> w * h
Shape.Circle(r) -> 3 * r * r
Shape.Point -> 0
```

List patterns match by length. `[]` is the empty list, `[a]` and `[a, b]` are lists of exactly one and two elements, and `[a, b, ..rest]` is a list of at least two, binding the remaining list to `rest` (`..rest` comes last; `.._` ignores it). `[..all]` matches any list. The elements are patterns too:

```aver
fn firstPresent(xs: List<Option<Int>>) -> Int
? "The first present value, or zero."
match xs
[Option.Some(x), ..rest] -> x
[Option.None, ..rest] -> firstPresent(rest)
[] -> 0
```

Arms are still tried top to bottom. Exhaustiveness counts every case: a literal never covers its constructor, so `Option.Some(0)` needs an `Option.Some(n)` or `Option.Some(_)` arm after it, and the checker names the missing case (`Non-exhaustive match: missing pattern Option.Some(_)`, `missing pattern [_, _, _, .._]` when a list of three or more has no arm). An arm that no value can reach is an error, also when it is covered only by several earlier arms together, as `Option.Some(_)` is after `Option.Some(true)` and `Option.Some(false)`.

The compiler turns a match with nested patterns into nested ordinary matches right after checking it, so every backend and the Lean export read the same program. Such a match inside a `yield` function is not supported yet; move it into a helper function.

### Literal patterns

An arm may be a literal instead of a binding. It fires when the subject equals the literal. This is how you dispatch on a command name or a tag byte. There is no `else if`, and there is no need to spread the decision over a chain of single-purpose helper functions:
Expand Down
66 changes: 66 additions & 0 deletions src/ast/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -457,6 +457,72 @@ pub enum Pattern {
/// Built-ins: Result.Ok(x), Result.Err(x), Option.Some(x), Option.None.
/// User-defined: Shape.Circle(r), Shape.Rect(w, h), Shape.Point.
Constructor(String, Vec<String>),
/// Constructor pattern with at least one field that is not a plain
/// binder: `Option.Some(0)`, `Result.Ok("x")`, `Pair.Of(1, x)`,
/// `Option.Some(Option.Some(y))`. A constructor whose fields are all
/// binders or `_` stays [`Pattern::Constructor`].
///
/// Source-level only: the front door checks the match as written
/// and then compiles it into nested flat matches
/// (`crate::ir::nested_patterns`), so no backend, proof exporter or
/// later pass ever sees this form.
ConstructorNested(String, Vec<Pattern>),
/// General list pattern: `[a, b]`, `[a, b, ..rest]`, `[0, ..rest]`,
/// `[Option.Some(x), ..rest]`, `[..rest]`. `rest` is the binder after
/// `..` (`_` allowed); `None` means the list has exactly
/// `items.len()` elements. `[]` stays [`Pattern::EmptyList`] and
/// `[head, ..tail]` with two binders stays [`Pattern::Cons`].
///
/// Source-level only, like [`Pattern::ConstructorNested`].
List {
items: Vec<Pattern>,
rest: Option<String>,
},
}

impl Pattern {
/// Every name this pattern spells in a binder position, in source
/// order and at any depth — `_` included wherever the flat forms
/// store it as a name, exactly as the per-form walks always did.
pub fn binder_names(&self) -> Vec<&str> {
let mut out = Vec::new();
self.push_binder_names(&mut out);
out
}

fn push_binder_names<'a>(&'a self, out: &mut Vec<&'a str>) {
match self {
Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => {}
Pattern::Ident(name) => out.push(name),
Pattern::Cons(head, tail) => out.extend([head.as_str(), tail.as_str()]),
Pattern::Constructor(_, names) => out.extend(names.iter().map(String::as_str)),
Pattern::Tuple(items) | Pattern::ConstructorNested(_, items) => {
items.iter().for_each(|item| item.push_binder_names(out))
}
Pattern::List { items, rest } => {
items.iter().for_each(|item| item.push_binder_names(out));
if let Some(rest) = rest {
out.push(rest);
}
}
}
}

/// True for the source-level forms the front door compiles away
/// ([`Pattern::ConstructorNested`], [`Pattern::List`]), anywhere
/// inside this pattern.
pub fn has_nested_form(&self) -> bool {
match self {
Pattern::ConstructorNested(_, _) | Pattern::List { .. } => true,
Pattern::Tuple(items) => items.iter().any(Pattern::has_nested_form),
Pattern::Wildcard
| Pattern::Literal(_)
| Pattern::Ident(_)
| Pattern::EmptyList
| Pattern::Cons(_, _)
| Pattern::Constructor(_, _) => false,
}
}
}

#[derive(Debug, Clone, PartialEq)]
Expand Down
38 changes: 38 additions & 0 deletions src/ast/unparse.rs
Original file line number Diff line number Diff line change
Expand Up @@ -611,6 +611,15 @@ fn write_literal(out: &mut String, lit: &Literal) -> Result<()> {
Ok(())
}

/// A match pattern spelled as source, for diagnostics.
pub fn pattern_to_source(pattern: &Pattern) -> String {
let mut out = String::new();
match write_pattern(&mut out, pattern) {
Ok(()) => out,
Err(_) => format!("{pattern:?}"),
}
}

fn write_pattern(out: &mut String, pattern: &Pattern) -> Result<()> {
match pattern {
Pattern::Wildcard => {
Expand Down Expand Up @@ -650,6 +659,35 @@ fn write_pattern(out: &mut String, pattern: &Pattern) -> Result<()> {
}
Ok(())
}
Pattern::ConstructorNested(name, fields) => {
out.push_str(name);
out.push('(');
for (i, field) in fields.iter().enumerate() {
if i > 0 {
out.push_str(", ");
}
write_pattern(out, field)?;
}
out.push(')');
Ok(())
}
Pattern::List { items, rest } => {
out.push('[');
for (i, item) in items.iter().enumerate() {
if i > 0 {
out.push_str(", ");
}
write_pattern(out, item)?;
}
if let Some(rest) = rest {
if !items.is_empty() {
out.push_str(", ");
}
write!(out, "..{rest}")?;
}
out.push(']');
Ok(())
}
}
}

Expand Down
3 changes: 3 additions & 0 deletions src/ast_rewrite.rs
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,9 @@ fn collect_pattern_bindings(pattern: &Pattern, out: &mut Vec<String>) {
}
}
Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => {}
Pattern::ConstructorNested(..) | Pattern::List { .. } => {
out.extend(pattern.binder_names().into_iter().map(str::to_string))
}
}
}

Expand Down
5 changes: 5 additions & 0 deletions src/checker/coverage/shapes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -198,6 +198,11 @@ fn forget_pattern_bindings(pattern: &Pattern, bindings: &mut HashMap<String, Sha
}
}
Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => {}
Pattern::ConstructorNested(..) | Pattern::List { .. } => {
for name in pattern.binder_names() {
bindings.remove(name);
}
}
}
}

Expand Down
1 change: 1 addition & 0 deletions src/checker/serve_path.rs
Original file line number Diff line number Diff line change
Expand Up @@ -392,6 +392,7 @@ fn pattern_bindings<'a>(pattern: &'a Pattern, out: &mut Vec<&'a str>) {
Pattern::Tuple(items) => items.iter().for_each(|item| pattern_bindings(item, out)),
Pattern::Constructor(_, names) => out.extend(names.iter().map(String::as_str)),
Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => {}
Pattern::ConstructorNested(..) | Pattern::List { .. } => out.extend(pattern.binder_names()),
}
}

Expand Down
9 changes: 8 additions & 1 deletion src/codegen/recursion/cycle_measure.rs
Original file line number Diff line number Diff line change
Expand Up @@ -374,7 +374,14 @@ fn arm_scope(
);
}
}
Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => {}
// Compiled into flat matches before any proof pass reads
// the program; binding nothing as a strict part here is the
// conservative reading if one ever arrives.
Pattern::Wildcard
| Pattern::Literal(_)
| Pattern::EmptyList
| Pattern::ConstructorNested(..)
| Pattern::List { .. } => {}
}
}
match pattern {
Expand Down
1 change: 1 addition & 0 deletions src/codegen/recursion/detect.rs
Original file line number Diff line number Diff line change
Expand Up @@ -192,6 +192,7 @@ pub(crate) fn pattern_bound_names(pattern: &Pattern) -> Vec<&str> {
Pattern::Cons(head, tail) => vec![head.as_str(), tail.as_str()],
Pattern::Constructor(_, binders) => binders.iter().map(String::as_str).collect(),
Pattern::Tuple(items) => items.iter().flat_map(pattern_bound_names).collect(),
Pattern::ConstructorNested(..) | Pattern::List { .. } => pattern.binder_names(),
}
}

Expand Down
16 changes: 16 additions & 0 deletions src/ir/buffer_build/driver_step.rs
Original file line number Diff line number Diff line change
Expand Up @@ -595,6 +595,11 @@ fn collect_binders_of_pattern(pattern: &Pattern, out: &mut HashSet<String>) {
insert_binder(b, out);
}
}
Pattern::ConstructorNested(..) | Pattern::List { .. } => {
for b in pattern.binder_names() {
insert_binder(b, out);
}
}
}
}

Expand Down Expand Up @@ -896,6 +901,17 @@ fn rename_pattern(pattern: &mut Pattern, rename: &HashMap<String, String>) {
}
}
}
Pattern::ConstructorNested(_, fields) => {
fields.iter_mut().for_each(|p| rename_pattern(p, rename))
}
Pattern::List { items, rest } => {
items.iter_mut().for_each(|p| rename_pattern(p, rename));
if let Some(rest) = rest
&& let Some(fresh) = rename.get(rest)
{
*rest = fresh.clone();
}
}
}
}

Expand Down
3 changes: 3 additions & 0 deletions src/ir/buffer_build/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -644,6 +644,9 @@ fn pattern_binds_name(pattern: &Pattern, name: &str) -> bool {
Pattern::Cons(head, tail) => head == name || tail == name,
Pattern::Tuple(items) => items.iter().any(|p| pattern_binds_name(p, name)),
Pattern::Constructor(_, bindings) => bindings.iter().any(|b| b == name),
Pattern::ConstructorNested(..) | Pattern::List { .. } => {
pattern.binder_names().contains(&name)
}
}
}

Expand Down
5 changes: 5 additions & 0 deletions src/ir/chars_fusion.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1630,6 +1630,11 @@ fn pattern_bindings(pattern: &Pattern) -> Vec<String> {
Pattern::Cons(head, tail) => vec![head.clone(), tail.clone()],
Pattern::Tuple(items) => items.iter().flat_map(pattern_bindings).collect(),
Pattern::Constructor(_, bindings) => bindings.clone(),
Pattern::ConstructorNested(..) | Pattern::List { .. } => pattern
.binder_names()
.into_iter()
.map(str::to_string)
.collect(),
}
}

Expand Down
43 changes: 42 additions & 1 deletion src/ir/escape.rs
Original file line number Diff line number Diff line change
Expand Up @@ -161,10 +161,21 @@ fn classify_fn(fd: &FnDef) -> Option<InlineCandidate> {
if contains_tail_call(&body.node) {
return None;
}
// The splice copies the body into the CALLER's frame, where only the
// substituted parameter (and, for shape B, the top-level arm
// binders) are accounted for. A `match` whose pattern binds a name
// owns a slot of the callee's frame that the caller never allocated:
// the spliced body would read and write a slot index the caller does
// not have, or one the caller uses for something else (VM slot-index
// panic, wasm-gc validation error, a clobbered caller local). Such a
// body stays a call.
if binds_below_top(&body.node) {
return None;
}

// Shape A: body uses param only via Attr(p, field). Inline at
// call sites where arg is RecordCreate.
if body_uses_param_only_via_attr(&body.node, param_slot) {
if body_uses_param_only_via_attr(&body.node, param_slot) && !binds_at_top(&body.node) {
return Some(InlineCandidate::RecordAccess {
param_slot,
body: body.clone(),
Expand Down Expand Up @@ -317,6 +328,36 @@ fn walk_expr_with_context(expr: &Expr, in_attr_obj: bool, visit: &mut dyn FnMut(
}
}

/// True when `expr` is a `match` whose own arms bind a name.
fn binds_at_top(expr: &Expr) -> bool {
matches!(expr, Expr::Match { arms, .. }
if arms.iter().any(|arm| arm.pattern.binder_names().iter().any(|name| *name != "_")))
}

/// True when a `match` anywhere below the top-level expression — or in
/// the arm bodies of a top-level `match` — binds a name.
fn binds_below_top(expr: &Expr) -> bool {
let binds = |pattern: &Pattern| pattern.binder_names().iter().any(|name| *name != "_");
let mut found = false;
let mut visit = |e: &Expr, _| {
if let Expr::Match { arms, .. } = e
&& arms.iter().any(|arm| binds(&arm.pattern))
{
found = true;
}
};
match expr {
Expr::Match { subject, arms } => {
walk_expr_with_context(&subject.node, false, &mut visit);
for arm in arms {
walk_expr_with_context(&arm.body.node, false, &mut visit);
}
}
other => walk_expr_with_context(other, false, &mut visit),
}
found
}

fn contains_tail_call(expr: &Expr) -> bool {
let mut found = false;
walk_expr_with_context(expr, false, &mut |e, _| {
Expand Down
Loading
Loading