From ad2c432f93617caf84372e790ef726fcda74dc55 Mon Sep 17 00:00:00 2001 From: jasisz Date: Fri, 25 Sep 2026 04:39:45 +0200 Subject: [PATCH] Add nested literal, constructor and list patterns Constructor fields and list or tuple elements are now patterns at any depth: Option.Some(0), Result.Ok("x"), Shape.Rect(0, h), Option.Some(Option.None), and list patterns [a], [a, b], [a, b, ..rest], [..all] with pattern elements such as [0, ..rest] or [Option.Some(x), ..rest]. The checker reads the patterns as written: exhaustiveness counts list patterns by length and never lets a literal cover its constructor, literal and list patterns are type-checked against their position, and pattern errors point at the arm. The front door then compiles each such match into nested flat matches (src/ir/nested_patterns.rs) and checks the lowered program again, so the VM, Rust, wasm-gc, wasip2, the Lean export and the certificate model all read ordinary matches. An arm the compiled tree never reaches is reported as unreachable. Nested patterns inside a yield function are refused for now. aver format prints match patterns in canonical spelling, changing only whitespace. Also fix the escape pass: a one-parameter body holding a match that binds a name is no longer spliced into its caller, where the binder's slot did not exist (VM index panic, wasm-gc validation failure, or a clobbered caller local). Co-Authored-By: Claude Opus 5.5 (1M context) --- .claude/commands/aver.md | 3 +- AGENTS.md | 2 +- CHANGELOG.md | 12 + docs/language.md | 42 ++ src/ast/mod.rs | 66 ++ src/ast/unparse.rs | 38 ++ src/ast_rewrite.rs | 3 + src/checker/coverage/shapes.rs | 5 + src/checker/serve_path.rs | 1 + src/codegen/recursion/cycle_measure.rs | 9 +- src/codegen/recursion/detect.rs | 1 + src/ir/buffer_build/driver_step.rs | 16 + src/ir/buffer_build/mod.rs | 3 + src/ir/chars_fusion.rs | 5 + src/ir/escape.rs | 43 +- src/ir/hir/resolve.rs | 6 + src/ir/mod.rs | 1 + src/ir/nested_patterns.rs | 772 ++++++++++++++++++++++ src/ir/nested_patterns/tests.rs | 128 ++++ src/ir/pipeline.rs | 72 +- src/ir/string_index.rs | 5 + src/ir/vars.rs | 7 + src/main/commands.rs | 13 +- src/main/format_cmd.rs | 85 +++ src/parser/mod.rs | 1 + src/parser/patterns.rs | 114 +++- src/resolver.rs | 10 + src/source.rs | 9 +- src/stdlib/profile_render.rs | 17 + src/types/checker/exhaustiveness.rs | 48 +- src/types/checker/infer/patterns.rs | 191 ++++-- src/types/checker/mod.rs | 10 + src/yield_lowering/build.rs | 7 + src/yield_lowering/trace/source/inline.rs | 14 +- tests/fixtures/nested_patterns.av | 122 ++++ tests/fixtures/nested_patterns.expected | 32 + tests/fixtures/nested_patterns_law.av | 33 + tests/nested_patterns_spec.rs | 112 ++++ tests/parser_spec.rs | 163 +++++ tests/proof_spec.rs | 13 + tests/rust_codegen_differential.rs | 12 + tests/typechecker_spec.rs | 145 ++++ tools/website/llms.txt | 3 +- 43 files changed, 2308 insertions(+), 86 deletions(-) create mode 100644 src/ir/nested_patterns.rs create mode 100644 src/ir/nested_patterns/tests.rs create mode 100644 tests/fixtures/nested_patterns.av create mode 100644 tests/fixtures/nested_patterns.expected create mode 100644 tests/fixtures/nested_patterns_law.av create mode 100644 tests/nested_patterns_spec.rs diff --git a/.claude/commands/aver.md b/.claude/commands/aver.md index ca45910d4..940990e2e 100644 --- a/.claude/commands/aver.md +++ b/.claude/commands/aver.md @@ -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 diff --git a/AGENTS.md b/AGENTS.md index 893184e84..673b3809b 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -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` | ast.rs | Every expression form: `Literal`, `Ident`, `Resolved(u16)`, `Attr`, `FnCall`, `BinOp`, `Match`, `Constructor`, `ErrorProp`, `InterpolatedStr`, `List(Vec)`, `Tuple(Vec)`, `MapLiteral(Vec<(Expr, Expr)>)`, `RecordCreate { type_name, fields }`, `RecordUpdate { type_name, base, updates }`, `TailCall(Box<(String, Vec)>)` | | `Stmt` | ast.rs | `Binding(name, Option, expr)`, `Expr(expr)` | diff --git a/CHANGELOG.md b/CHANGELOG.md index c97fda9e0..bd9adf4fe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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`) 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. diff --git a/docs/language.md b/docs/language.md index 5e210f834..47fc45c4d 100644 --- a/docs/language.md +++ b/docs/language.md @@ -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) -> 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>) -> 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: diff --git a/src/ast/mod.rs b/src/ast/mod.rs index 4cd0f11d7..142d06117 100644 --- a/src/ast/mod.rs +++ b/src/ast/mod.rs @@ -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), + /// 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), + /// 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, + rest: Option, + }, +} + +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)] diff --git a/src/ast/unparse.rs b/src/ast/unparse.rs index 7b09743ec..f21c7650a 100644 --- a/src/ast/unparse.rs +++ b/src/ast/unparse.rs @@ -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 => { @@ -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(()) + } } } diff --git a/src/ast_rewrite.rs b/src/ast_rewrite.rs index 570275eb5..e74d84c4d 100644 --- a/src/ast_rewrite.rs +++ b/src/ast_rewrite.rs @@ -46,6 +46,9 @@ fn collect_pattern_bindings(pattern: &Pattern, out: &mut Vec) { } } Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => {} + Pattern::ConstructorNested(..) | Pattern::List { .. } => { + out.extend(pattern.binder_names().into_iter().map(str::to_string)) + } } } diff --git a/src/checker/coverage/shapes.rs b/src/checker/coverage/shapes.rs index 56a9209c0..a169ab318 100644 --- a/src/checker/coverage/shapes.rs +++ b/src/checker/coverage/shapes.rs @@ -198,6 +198,11 @@ fn forget_pattern_bindings(pattern: &Pattern, bindings: &mut HashMap {} + Pattern::ConstructorNested(..) | Pattern::List { .. } => { + for name in pattern.binder_names() { + bindings.remove(name); + } + } } } diff --git a/src/checker/serve_path.rs b/src/checker/serve_path.rs index 5073c89d0..97fb61804 100644 --- a/src/checker/serve_path.rs +++ b/src/checker/serve_path.rs @@ -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()), } } diff --git a/src/codegen/recursion/cycle_measure.rs b/src/codegen/recursion/cycle_measure.rs index c9e1b8710..180017a2d 100644 --- a/src/codegen/recursion/cycle_measure.rs +++ b/src/codegen/recursion/cycle_measure.rs @@ -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 { diff --git a/src/codegen/recursion/detect.rs b/src/codegen/recursion/detect.rs index 05edff165..b13790e1b 100644 --- a/src/codegen/recursion/detect.rs +++ b/src/codegen/recursion/detect.rs @@ -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(), } } diff --git a/src/ir/buffer_build/driver_step.rs b/src/ir/buffer_build/driver_step.rs index 29bfa4b53..eadd3cdfe 100644 --- a/src/ir/buffer_build/driver_step.rs +++ b/src/ir/buffer_build/driver_step.rs @@ -595,6 +595,11 @@ fn collect_binders_of_pattern(pattern: &Pattern, out: &mut HashSet) { insert_binder(b, out); } } + Pattern::ConstructorNested(..) | Pattern::List { .. } => { + for b in pattern.binder_names() { + insert_binder(b, out); + } + } } } @@ -896,6 +901,17 @@ fn rename_pattern(pattern: &mut Pattern, rename: &HashMap) { } } } + 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(); + } + } } } diff --git a/src/ir/buffer_build/mod.rs b/src/ir/buffer_build/mod.rs index 6dc8eb940..77e7164a5 100644 --- a/src/ir/buffer_build/mod.rs +++ b/src/ir/buffer_build/mod.rs @@ -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) + } } } diff --git a/src/ir/chars_fusion.rs b/src/ir/chars_fusion.rs index 010df573d..1fff07d0a 100644 --- a/src/ir/chars_fusion.rs +++ b/src/ir/chars_fusion.rs @@ -1630,6 +1630,11 @@ fn pattern_bindings(pattern: &Pattern) -> Vec { 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(), } } diff --git a/src/ir/escape.rs b/src/ir/escape.rs index 26a08703b..3eb650c39 100644 --- a/src/ir/escape.rs +++ b/src/ir/escape.rs @@ -161,10 +161,21 @@ fn classify_fn(fd: &FnDef) -> Option { 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(), @@ -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, _| { diff --git a/src/ir/hir/resolve.rs b/src/ir/hir/resolve.rs index 1be40bb22..9740aa796 100644 --- a/src/ir/hir/resolve.rs +++ b/src/ir/hir/resolve.rs @@ -668,6 +668,12 @@ fn resolve_pattern(ctx: &ResolveCtx<'_>, pat: &Pattern) -> ResolvedPattern { Pattern::Constructor(name, bindings) => { ResolvedPattern::Ctor(classify_ctor(ctx, name), bindings.clone()) } + // The front door compiles every match holding one of these into + // nested flat matches (`crate::ir::nested_patterns`) before any + // door resolves the program, so the HIR has no form for them. + Pattern::ConstructorNested(..) | Pattern::List { .. } => panic!( + "nested pattern reached HIR resolve without the front door compiling it: {pat:?}" + ), } } diff --git a/src/ir/mod.rs b/src/ir/mod.rs index ff38ef4e0..956645580 100644 --- a/src/ir/mod.rs +++ b/src/ir/mod.rs @@ -17,6 +17,7 @@ mod matches; /// epic) is doc-only; see `src/ir/mir/mod.rs` for the overview and /// `src/ir/mir/RFC.md` for the full design. pub mod mir; +pub mod nested_patterns; mod pass_diag; pub mod pipeline; pub mod proof_ir; diff --git a/src/ir/nested_patterns.rs b/src/ir/nested_patterns.rs new file mode 100644 index 000000000..0b66a9dab --- /dev/null +++ b/src/ir/nested_patterns.rs @@ -0,0 +1,772 @@ +//! Nested-pattern compilation: the front-door pass that turns every +//! `match` holding a nested constructor pattern (`Option.Some(0)`, +//! `Pair.Of(1, x)`) or a general list pattern (`[a, b, ..rest]`, +//! `[a, b]`, `[0, ..rest]`) into a tree of flat matches that every +//! backend and proof exporter already reads. +//! +//! The pass runs in [`crate::ir::pipeline::front`] after the program was +//! type-checked AS WRITTEN (so exhaustiveness, redundancy and type +//! errors speak about the patterns the user wrote) and before the +//! lowered program is checked again. Nothing below the front door ever +//! sees [`Pattern::ConstructorNested`] or [`Pattern::List`]. +//! +//! The compilation is the classic clause-matrix one: pick the first +//! column the first row tests, switch on it with one flat match (one arm +//! per constructor or literal that appears, plus `_` when the arms do not +//! cover the type), specialise the rows for each arm and recurse. A row +//! whose remaining patterns are all binders is a leaf: its body, with the +//! row's binders renamed to the values they matched. First-match order is +//! kept because rows are never reordered, so the tree takes exactly the +//! arm the written match takes. Bodies are cloned into every leaf that +//! reaches them; a matched value is never computed twice (the subject is +//! evaluated once, sub-values are bound by the flat patterns). +//! +//! An arm that reaches no leaf can never be taken: it is reported as +//! unreachable, which covers the cases the pairwise check in +//! `types::checker::exhaustiveness` cannot see. + +use std::collections::{HashMap, HashSet}; + +use crate::ast::{Expr, FnBody, Literal, MatchArm, Pattern, Spanned, Stmt, TopLevel, VerifyKind}; +use crate::types::checker::TypeError; + +/// Leaves one match may expand to before the pass refuses it. The +/// clause-matrix expansion is exponential only on adversarial pattern +/// sets; a real program stays far below this. +const MAX_LEAVES: usize = 4096; + +/// True when some `match` in `items` uses a nested constructor pattern +/// or a general list pattern. +pub fn has_nested_patterns(items: &[TopLevel]) -> bool { + let mut found = false; + for_each_root_expr(items, &mut |expr| { + if !found { + found = expr_has_nested(expr); + } + }); + found +} + +/// The `yield` functions of `items` that use a nested pattern: the +/// `yield` lowering reads the program as written, so these are refused +/// until it learns the nested forms. +pub fn nested_patterns_in_yield_fns(items: &[TopLevel]) -> Vec { + items + .iter() + .filter_map(|item| match item { + TopLevel::FnDef(fd) if crate::yield_lowering::is_yield_fn(fd) => { + let has = fd.body.stmts().iter().any(|stmt| match stmt { + Stmt::Binding(_, _, expr) | Stmt::Expr(expr) => expr_has_nested(expr), + }); + has.then(|| TypeError { + message: format!( + "nested constructor and list patterns are not supported inside the \ + `yield` function '{}' yet; move the match into a helper function", + fd.name + ), + line: fd.line, + col: 0, + origin: None, + secondary: None, + }) + } + _ => None, + }) + .collect() +} + +/// Compile every match holding a nested pattern into flat matches. +/// `families` maps a constructor spelled in a pattern to the variant +/// names of its sum type (from the check of the written program). +/// Returns the arms that can never be taken. +pub fn lower_nested_patterns( + items: &mut [TopLevel], + families: &HashMap>, +) -> Vec { + let mut errors = Vec::new(); + for item in items.iter_mut() { + match item { + TopLevel::FnDef(fd) => { + let has = fd.body.stmts().iter().any(|stmt| match stmt { + Stmt::Binding(_, _, expr) | Stmt::Expr(expr) => expr_has_nested(expr), + }); + if !has { + continue; + } + let mut lowering = Lowering::new(families, &mut errors); + let FnBody::Block(stmts) = std::sync::Arc::make_mut(&mut fd.body); + for stmt in stmts { + match stmt { + Stmt::Binding(_, _, expr) | Stmt::Expr(expr) => lowering.rewrite(expr), + } + } + } + TopLevel::Stmt(Stmt::Binding(_, _, expr) | Stmt::Expr(expr)) => { + if expr_has_nested(expr) { + Lowering::new(families, &mut errors).rewrite(expr); + } + } + TopLevel::Verify(vb) => { + let mut lowering = Lowering::new(families, &mut errors); + for (lhs, rhs) in &mut vb.cases { + lowering.rewrite_if_nested(lhs); + lowering.rewrite_if_nested(rhs); + } + for givens in &mut vb.case_givens { + for (_, expr) in givens { + lowering.rewrite_if_nested(expr); + } + } + if let VerifyKind::Law(law) = &mut vb.kind { + lowering.rewrite_if_nested(&mut law.lhs); + lowering.rewrite_if_nested(&mut law.rhs); + if let Some(when) = &mut law.when { + lowering.rewrite_if_nested(when); + } + for expr in law.because.iter_mut().chain(law.sample_guards.iter_mut()) { + lowering.rewrite_if_nested(expr); + } + } + } + _ => {} + } + } + errors +} + +fn for_each_root_expr(items: &[TopLevel], f: &mut impl FnMut(&Spanned)) { + for item in items { + match item { + TopLevel::FnDef(fd) => { + for stmt in fd.body.stmts() { + match stmt { + Stmt::Binding(_, _, expr) | Stmt::Expr(expr) => f(expr), + } + } + } + TopLevel::Stmt(Stmt::Binding(_, _, expr) | Stmt::Expr(expr)) => f(expr), + TopLevel::Verify(vb) => { + for (lhs, rhs) in &vb.cases { + f(lhs); + f(rhs); + } + for givens in &vb.case_givens { + for (_, expr) in givens { + f(expr); + } + } + if let VerifyKind::Law(law) = &vb.kind { + f(&law.lhs); + f(&law.rhs); + if let Some(when) = &law.when { + f(when); + } + law.because + .iter() + .chain(law.sample_guards.iter()) + .for_each(&mut *f); + } + } + _ => {} + } + } +} + +fn expr_has_nested(expr: &Spanned) -> bool { + crate::codegen::expr_walk::any(expr, &mut |e| match &e.node { + Expr::Match { arms, .. } => arms.iter().any(|arm| arm.pattern.has_nested_form()), + _ => false, + }) +} + +/// A pattern of the clause matrix: the written pattern with binders +/// split from wildcards and list patterns spelled as cons chains. +#[derive(Debug, Clone)] +enum Pat { + Wild, + Bind(String), + Lit(Literal), + Tuple(Vec), + Ctor(String, Vec), + Nil, + Cons(Box, Box), +} + +impl Pat { + fn from_ast(pattern: &Pattern) -> Pat { + match pattern { + Pattern::Wildcard => Pat::Wild, + Pattern::Ident(name) => Pat::binder(name), + Pattern::Literal(lit) => Pat::Lit(lit.clone()), + Pattern::EmptyList => Pat::Nil, + Pattern::Cons(head, tail) => { + Pat::Cons(Box::new(Pat::binder(head)), Box::new(Pat::binder(tail))) + } + Pattern::Tuple(items) => Pat::Tuple(items.iter().map(Pat::from_ast).collect()), + Pattern::Constructor(name, binders) => Pat::Ctor( + name.clone(), + binders.iter().map(|b| Pat::binder(b)).collect(), + ), + Pattern::ConstructorNested(name, fields) => { + Pat::Ctor(name.clone(), fields.iter().map(Pat::from_ast).collect()) + } + Pattern::List { items, rest } => { + let tail = rest.as_deref().map(Pat::binder).unwrap_or(Pat::Nil); + items.iter().rev().fold(tail, |tail, item| { + Pat::Cons(Box::new(Pat::from_ast(item)), Box::new(tail)) + }) + } + } + } + + fn binder(name: &str) -> Pat { + if name == "_" { + Pat::Wild + } else { + Pat::Bind(name.to_string()) + } + } + + fn is_irrefutable(&self) -> bool { + matches!(self, Pat::Wild | Pat::Bind(_)) + } + + fn push_binders<'a>(&'a self, out: &mut Vec<&'a str>) { + match self { + Pat::Wild | Pat::Lit(_) | Pat::Nil => {} + Pat::Bind(name) => out.push(name), + Pat::Tuple(items) | Pat::Ctor(_, items) => { + items.iter().for_each(|item| item.push_binders(out)) + } + Pat::Cons(head, tail) => { + head.push_binders(out); + tail.push_binders(out); + } + } + } +} + +/// Where the value a column tests lives. +#[derive(Debug, Clone)] +enum Occ { + /// A variable in scope (a parameter, a local, or a binder a flat + /// pattern introduced). + Var(String), + /// The match subject itself, when it is not a variable and no row + /// binds it whole: it is evaluated exactly once, by the root switch. + Subject(Box>), + /// A field no row looks at. + Unused, +} + +#[derive(Debug, Clone)] +struct Row { + pats: Vec, + /// `(user binder, variable holding its value)` for binders already + /// consumed by a switch above. + renames: Vec<(String, String)>, + arm: usize, +} + +impl Row { + fn binders_outside(&self, column: usize) -> Vec<&str> { + let mut out = Vec::new(); + for (index, pat) in self.pats.iter().enumerate() { + if index != column { + pat.push_binders(&mut out); + } + } + out + } +} + +/// Constructor families of one switch. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +enum Kind { + Tuple, + Ctor, + List, + Bool, + Lit, +} + +fn kind_of(pat: &Pat) -> Kind { + match pat { + Pat::Tuple(_) => Kind::Tuple, + Pat::Ctor(_, _) => Kind::Ctor, + Pat::Nil | Pat::Cons(_, _) => Kind::List, + Pat::Lit(Literal::Bool(_)) => Kind::Bool, + Pat::Lit(_) => Kind::Lit, + Pat::Wild | Pat::Bind(_) => { + unreachable!("a switch column is chosen on a refutable pattern") + } + } +} + +/// `Module.Type.Variant` and `Type.Variant` name the same constructor: +/// compare the last two segments, as the exhaustiveness check does. +fn ctor_key(name: &str) -> (&str, &str) { + let mut parts = name.rsplit('.'); + let variant = parts.next().unwrap_or(name); + let owner = parts.next().unwrap_or(""); + (owner, variant) +} + +/// One case of a switch: what the flat arm tests, and how many +/// sub-values it binds. +#[derive(Debug, Clone)] +enum Case { + Tuple(usize), + Ctor(String, usize), + Nil, + Cons, + Lit(Literal), +} + +impl Case { + fn arity(&self) -> usize { + match self { + Case::Tuple(n) | Case::Ctor(_, n) => *n, + Case::Cons => 2, + Case::Nil | Case::Lit(_) => 0, + } + } + + /// The sub-patterns `pat` contributes under this case, or `None` + /// when `pat` is a different refutable case. + fn specialize(&self, pat: &Pat) -> Option> { + match (self, pat) { + (_, Pat::Wild | Pat::Bind(_)) => Some(vec![Pat::Wild; self.arity()]), + (Case::Tuple(n), Pat::Tuple(items)) if items.len() == *n => Some(items.clone()), + (Case::Ctor(name, n), Pat::Ctor(other, args)) + if ctor_key(name) == ctor_key(other) && args.len() == *n => + { + Some(args.clone()) + } + (Case::Nil, Pat::Nil) => Some(Vec::new()), + (Case::Cons, Pat::Cons(head, tail)) => Some(vec![(**head).clone(), (**tail).clone()]), + (Case::Lit(a), Pat::Lit(b)) if a == b => Some(Vec::new()), + _ => None, + } + } + + fn same_as(&self, pat: &Pat) -> bool { + !pat.is_irrefutable() && self.specialize(pat).is_some() + } + + fn of(pat: &Pat) -> Case { + match pat { + Pat::Tuple(items) => Case::Tuple(items.len()), + Pat::Ctor(name, args) => Case::Ctor(name.clone(), args.len()), + Pat::Nil => Case::Nil, + Pat::Cons(_, _) => Case::Cons, + Pat::Lit(lit) => Case::Lit(lit.clone()), + Pat::Wild | Pat::Bind(_) => unreachable!("cases are read off refutable patterns"), + } + } + + /// The flat pattern of this case's arm, binding `fields`. + fn flat_pattern(&self, fields: &[String]) -> Pattern { + match self { + Case::Tuple(_) => Pattern::Tuple( + fields + .iter() + .map(|name| { + if name == "_" { + Pattern::Wildcard + } else { + Pattern::Ident(name.clone()) + } + }) + .collect(), + ), + Case::Ctor(name, _) => Pattern::Constructor(name.clone(), fields.to_vec()), + Case::Nil => Pattern::EmptyList, + Case::Cons => Pattern::Cons(fields[0].clone(), fields[1].clone()), + Case::Lit(lit) => Pattern::Literal(lit.clone()), + } + } +} + +struct Lowering<'a> { + families: &'a HashMap>, + errors: &'a mut Vec, + fresh: usize, +} + +/// Per-match state: the written arm bodies, which arms some leaf +/// reached, and how many leaves were built. +struct MatchState<'b> { + bodies: &'b [Spanned], + reached: Vec, + leaves: usize, + line: usize, +} + +impl<'a> Lowering<'a> { + fn new(families: &'a HashMap>, errors: &'a mut Vec) -> Self { + Self { + families, + errors, + fresh: 0, + } + } + + fn rewrite_if_nested(&mut self, expr: &mut Spanned) { + if expr_has_nested(expr) { + self.rewrite(expr); + } + } + + /// Post-order: inner matches are compiled first, so the arm bodies a + /// match clones are already flat. + fn rewrite(&mut self, expr: &mut Spanned) { + crate::codegen::expr_walk::for_each_child_mut(expr, &mut |child| self.rewrite(child)); + let Expr::Match { subject, arms } = &expr.node else { + return; + }; + if !arms.iter().any(|arm| arm.pattern.has_nested_form()) { + return; + } + let line = expr.line; + if let Some(compiled) = self.compile_match(subject, arms, line) { + expr.node = compiled.node; + } + } + + fn fresh_name(&mut self) -> String { + let name = format!("__pat{}", self.fresh); + self.fresh += 1; + name + } + + fn compile_match( + &mut self, + subject: &Spanned, + arms: &[MatchArm], + line: usize, + ) -> Option> { + let bodies: Vec> = arms.iter().map(|arm| (*arm.body).clone()).collect(); + let rows: Vec = arms + .iter() + .enumerate() + .map(|(arm, a)| Row { + pats: vec![Pat::from_ast(&a.pattern)], + renames: Vec::new(), + arm, + }) + .collect(); + let mut state = MatchState { + bodies: &bodies, + reached: vec![false; arms.len()], + leaves: 0, + line, + }; + + // The root value: a variable is used as it is; any other subject + // is either tested once by the root switch, or — when some arm + // binds it whole — bound first by a one-arm match. + let root_binders: Vec<&str> = rows + .iter() + .filter_map(|row| match &row.pats[0] { + Pat::Bind(name) => Some(name.as_str()), + _ => None, + }) + .collect(); + let compiled = match &subject.node { + Expr::Ident(name) => self.compile(&[Occ::Var(name.clone())], rows, &mut state), + _ if root_binders.is_empty() => { + self.compile(&[Occ::Subject(Box::new(subject.clone()))], rows, &mut state) + } + _ => { + let name = self.fresh_name(); + let inner = self.compile(&[Occ::Var(name.clone())], rows, &mut state); + Spanned::new( + Expr::Match { + subject: Box::new(subject.clone()), + arms: vec![MatchArm::new(Pattern::Ident(name), inner)], + }, + line, + ) + } + }; + + if state.leaves > MAX_LEAVES { + self.errors.push(error_at( + line, + format!( + "this match expands to more than {MAX_LEAVES} cases once its nested patterns are compiled; split it into smaller matches" + ), + )); + return None; + } + for (index, reached) in state.reached.iter().enumerate() { + if !reached { + self.errors.push(error_at( + arms[index].body.line.max(line), + format!( + "Unreachable match arm: no value reaches pattern {} — the arms above it already match everything it matches", + crate::ast::unparse::pattern_to_source(&arms[index].pattern) + ), + )); + } + } + Some(compiled) + } + + fn compile( + &mut self, + occs: &[Occ], + rows: Vec, + state: &mut MatchState<'_>, + ) -> Spanned { + let line = state.line; + let first = &rows[0]; + let Some(column) = first.pats.iter().position(|pat| !pat.is_irrefutable()) else { + return self.leaf(occs, first, state); + }; + if state.leaves > MAX_LEAVES { + // Already refused; stop expanding. + return self.leaf(occs, first, state); + } + let occ = occs[column].clone(); + let kind = kind_of(&first.pats[column]); + + // The cases this column tests, in order of first appearance. + let mut cases: Vec = Vec::new(); + for row in &rows { + let pat = &row.pats[column]; + if pat.is_irrefutable() || cases.iter().any(|case| case.same_as(pat)) { + continue; + } + cases.push(Case::of(pat)); + } + let complete = match kind { + Kind::Tuple => true, + Kind::List => cases.len() == 2, + Kind::Bool => cases.len() == 2, + Kind::Lit => false, + Kind::Ctor => self.ctor_cases_complete(&cases), + }; + + let mut out_arms = Vec::new(); + for case in &cases { + let spec: Vec<(Row, Vec)> = rows + .iter() + .filter_map(|row| { + let fields = case.specialize(&row.pats[column])?; + Some((self.consume(row, column, &occ), fields)) + }) + .collect(); + let (names, field_occs) = self.name_fields(&spec, state); + let mut sub_occs: Vec = Vec::with_capacity(occs.len() - 1 + field_occs.len()); + sub_occs.extend(field_occs); + sub_occs.extend( + occs.iter() + .enumerate() + .filter(|(index, _)| *index != column) + .map(|(_, occ)| occ.clone()), + ); + let sub_rows: Vec = spec + .into_iter() + .map(|(mut row, fields)| { + let rest: Vec = row + .pats + .drain(..) + .enumerate() + .filter(|(index, _)| *index != column) + .map(|(_, pat)| pat) + .collect(); + row.pats = fields; + row.pats.extend(rest); + row + }) + .collect(); + let body = self.compile(&sub_occs, sub_rows, state); + out_arms.push(MatchArm::new(case.flat_pattern(&names), body)); + } + if !complete { + let default_rows: Vec = rows + .iter() + .filter(|row| row.pats[column].is_irrefutable()) + .map(|row| { + let mut row = self.consume(row, column, &occ); + row.pats.remove(column); + row + }) + .collect(); + // No row for the values no case names: the written match is + // not exhaustive there. The check of the written program has + // already refused that, except where it stops looking (deep + // recursive types); leaving the arm out makes the check of + // the lowered program report it instead of guessing. + if !default_rows.is_empty() { + let sub_occs: Vec = occs + .iter() + .enumerate() + .filter(|(index, _)| *index != column) + .map(|(_, occ)| occ.clone()) + .collect(); + let body = self.compile(&sub_occs, default_rows, state); + out_arms.push(MatchArm::new(Pattern::Wildcard, body)); + } + } + + let subject = match occ { + Occ::Var(name) => Spanned::new(Expr::Ident(name), line), + Occ::Subject(expr) => *expr, + Occ::Unused => unreachable!("an unused field is never tested"), + }; + Spanned::new( + Expr::Match { + subject: Box::new(subject), + arms: out_arms, + }, + line, + ) + } + + /// The row with the binder at `column` (if any) recorded as a rename + /// to the variable holding that column's value. + fn consume(&self, row: &Row, column: usize, occ: &Occ) -> Row { + let mut row = row.clone(); + if let Pat::Bind(name) = &row.pats[column] { + match occ { + Occ::Var(var) => { + if name != var { + row.renames.push((name.clone(), var.clone())); + } + } + // The root is bound first whenever an arm binds it whole, + // and a binder always makes a field a variable. + Occ::Subject(_) | Occ::Unused => { + unreachable!("a bound column always has a variable") + } + } + } + row.pats[column] = Pat::Wild; + row + } + + fn ctor_cases_complete(&self, cases: &[Case]) -> bool { + let Some(Case::Ctor(first, _)) = cases.first() else { + return false; + }; + let (owner, _) = ctor_key(first); + let variants: Vec = match owner { + "Option" => vec!["Some".to_string(), "None".to_string()], + "Result" => vec!["Ok".to_string(), "Err".to_string()], + _ => match self.families.get(first) { + Some(variants) => variants.clone(), + None => return false, + }, + }; + let present: HashSet<&str> = cases + .iter() + .filter_map(|case| match case { + Case::Ctor(name, _) => Some(ctor_key(name).1), + _ => None, + }) + .collect(); + variants + .iter() + .all(|variant| present.contains(variant.as_str())) + } + + /// Names for the sub-values a case binds. A field no row looks at is + /// `_`; a field every binding row binds under the same name `x` is + /// bound as `x` itself (when that cannot capture anything); any + /// other field gets a fresh `__patN`. + fn name_fields( + &mut self, + spec: &[(Row, Vec)], + state: &MatchState<'_>, + ) -> (Vec, Vec) { + let arity = spec.first().map(|(_, fields)| fields.len()).unwrap_or(0); + let mut names = Vec::with_capacity(arity); + let mut occs = Vec::with_capacity(arity); + for index in 0..arity { + let column: Vec<&Pat> = spec.iter().map(|(_, fields)| &fields[index]).collect(); + if column.iter().all(|pat| matches!(pat, Pat::Wild)) { + names.push("_".to_string()); + occs.push(Occ::Unused); + continue; + } + let binders: HashSet<&str> = column + .iter() + .filter_map(|pat| match pat { + Pat::Bind(name) => Some(name.as_str()), + _ => None, + }) + .collect(); + let reuse = match binders.iter().next() { + Some(name) if binders.len() == 1 => { + let name = *name; + let clash = spec.iter().any(|(row, fields)| { + let binds_here = matches!(&fields[index], Pat::Bind(n) if n == name); + let mut elsewhere = row.binders_outside(usize::MAX); + for (other, field) in fields.iter().enumerate() { + if other != index || !binds_here { + field.push_binders(&mut elsewhere); + } + } + elsewhere.contains(&name) + || row.renames.iter().any(|(user, _)| user == name) + || (!binds_here && mentions(&state.bodies[row.arm], name)) + }); + (!clash).then(|| name.to_string()) + } + _ => None, + }; + let name = reuse.unwrap_or_else(|| self.fresh_name()); + names.push(name.clone()); + occs.push(Occ::Var(name)); + } + (names, occs) + } + + fn leaf(&mut self, occs: &[Occ], row: &Row, state: &mut MatchState<'_>) -> Spanned { + state.leaves += 1; + state.reached[row.arm] = true; + let mut renames: HashMap = row.renames.iter().cloned().collect(); + for (pat, occ) in row.pats.iter().zip(occs) { + if let (Pat::Bind(name), Occ::Var(var)) = (pat, occ) + && name != var + { + renames.insert(name.clone(), var.clone()); + } + } + let body = &state.bodies[row.arm]; + if renames.is_empty() { + return body.clone(); + } + crate::ast_rewrite::rewrite_idents_scoped(body, |name| { + renames + .get(name) + .map(|var| Spanned::new(Expr::Ident(var.clone()), body.line)) + }) + } +} + +/// Whether `name` appears as an identifier anywhere in `expr` (binder +/// scoping ignored — the safe direction for the capture check). +fn mentions(expr: &Spanned, name: &str) -> bool { + crate::codegen::expr_walk::any(expr, &mut |e| match &e.node { + Expr::Ident(n) => n == name, + Expr::TailCall(call) => call.target == name, + _ => false, + }) +} + +fn error_at(line: usize, message: String) -> TypeError { + TypeError { + message, + line, + col: 0, + origin: None, + secondary: None, + } +} + +#[cfg(test)] +mod tests; diff --git a/src/ir/nested_patterns/tests.rs b/src/ir/nested_patterns/tests.rs new file mode 100644 index 000000000..c378e5204 --- /dev/null +++ b/src/ir/nested_patterns/tests.rs @@ -0,0 +1,128 @@ +use super::*; + +fn parse(source: &str) -> Vec { + let tokens = crate::lexer::Lexer::new(source) + .tokenize() + .expect("lex failed"); + crate::parser::Parser::new(tokens) + .parse() + .expect("parse failed") +} + +/// Check the program as written, compile its nested patterns, and +/// return the lowered program as source plus the lowering's errors. +fn lower(source: &str) -> (String, Vec) { + let mut items = parse(source); + let checked = crate::types::checker::run_type_check_full(&items, None); + assert!( + checked.errors.is_empty(), + "the written program must check: {:?}", + checked.errors + ); + let errors = lower_nested_patterns(&mut items, &checked.pattern_ctor_families); + assert!(!has_nested_patterns(&items), "every nested pattern is gone"); + let lowered = crate::types::checker::run_type_check_full(&items, None); + assert!( + lowered.errors.is_empty() || !errors.is_empty(), + "the lowered program must check too: {:?}", + lowered.errors + ); + ( + crate::ast::unparse::unparse(&items).expect("unparse"), + errors.into_iter().map(|e| e.message).collect(), + ) +} + +fn fn_source<'a>(program: &'a str, name: &str) -> &'a str { + let start = program + .find(&format!("fn {name}(")) + .unwrap_or_else(|| panic!("fn {name} in:\n{program}")); + let rest = &program[start..]; + let end = rest[1..].find("\nfn ").map(|i| i + 1).unwrap_or(rest.len()); + rest[..end].trim_end() +} + +#[test] +fn literal_inside_option_keeps_user_binder_names() { + let (program, errors) = lower( + "fn classify(o: Option) -> String\n match o\n Option.Some(0) -> \"zero\"\n Option.Some(n) -> \"many\"\n Option.None -> \"none\"\n", + ); + assert!(errors.is_empty(), "{errors:?}"); + let body = fn_source(&program, "classify"); + assert!( + body.contains("Option.Some(n) -> match n") && body.contains("0 -> \"zero\""), + "the field is bound under the user's own name and tested by a flat literal match:\n{body}" + ); + assert!(!body.contains("__pat"), "no fresh name is needed:\n{body}"); +} + +#[test] +fn complete_constructor_switch_gets_no_default_arm() { + // `Option.Some(true)`, `Option.Some(false)` and `Option.None` + // cover everything: no `_` arm a Lean `match` would call + // redundant. + let (program, errors) = lower( + "fn flags(p: Option) -> Int\n match p\n Option.Some(true) -> 1\n Option.Some(false) -> 2\n Option.None -> 3\n", + ); + assert!(errors.is_empty(), "{errors:?}"); + let body = fn_source(&program, "flags"); + assert!(!body.contains("_ ->"), "no default arm:\n{body}"); +} + +#[test] +fn user_sum_type_family_is_known_so_no_default_is_emitted() { + let (program, errors) = lower( + "type Shape\n Circle(Int)\n Dot\n\nfn area(s: Shape) -> Int\n match s\n Shape.Circle(0) -> 0\n Shape.Circle(r) -> r\n Shape.Dot -> 1\n", + ); + assert!(errors.is_empty(), "{errors:?}"); + let body = fn_source(&program, "area"); + assert_eq!( + body.matches("_ ->").count(), + 1, + "only the literal switch on the radius has a default:\n{body}" + ); +} + +#[test] +fn list_patterns_become_cons_chains() { + let (program, errors) = lower( + "fn size(xs: List) -> Int\n match xs\n [] -> 0\n [a] -> 1\n [a, b, ..rest] -> 2\n", + ); + assert!(errors.is_empty(), "{errors:?}"); + let body = fn_source(&program, "size"); + assert!(body.contains("[] -> 0"), "{body}"); + assert!(body.contains("[a, .."), "the head keeps its name:\n{body}"); +} + +#[test] +fn an_arm_no_value_reaches_is_reported() { + // The pairwise check cannot see this: neither `Option.Some(true)` + // nor `Option.Some(false)` alone covers `Option.Some(_)`. + let (_, errors) = lower( + "fn f(p: Option) -> Int\n match p\n Option.Some(true) -> 1\n Option.Some(false) -> 2\n Option.Some(_) -> 3\n Option.None -> 4\n", + ); + assert_eq!(errors.len(), 1, "{errors:?}"); + assert!( + errors[0].contains("Unreachable match arm") && errors[0].contains("Option.Some(_)"), + "{errors:?}" + ); +} + +#[test] +fn non_variable_subject_is_evaluated_once() { + // A computed subject that some arm binds whole is bound first, so + // it is not recomputed for the nested test. + let (program, errors) = lower( + "fn g(n: Int) -> Option\n Option.Some(n)\n\nfn f(n: Int) -> Int\n match g(n)\n Option.Some(0) -> 0\n other -> 1\n", + ); + assert!(errors.is_empty(), "{errors:?}"); + let body = fn_source(&program, "f"); + assert_eq!(body.matches("g(n)").count(), 1, "{body}"); +} + +#[test] +fn flat_matches_are_left_alone() { + let source = "fn f(o: Option) -> Int\n match o\n Option.Some(n) -> n\n Option.None -> 0\n"; + let items = parse(source); + assert!(!has_nested_patterns(&items)); +} diff --git a/src/ir/pipeline.rs b/src/ir/pipeline.rs index 883f7909b..1c04ddf30 100644 --- a/src/ir/pipeline.rs +++ b/src/ir/pipeline.rs @@ -58,6 +58,13 @@ pub enum PipelineStage { /// items of the program and both proof exporters see them. Fires /// only when a function was lowered. YieldLower, + /// Nested-pattern compilation: every `match` with a nested + /// constructor pattern or a general list pattern becomes nested flat + /// matches, after the program was checked as written. Runs inside + /// [`front`], ABOVE the proof line: it adds no entity the source + /// does not contain, only the case analysis the source spelled. + /// Fires only when a match was compiled. + PatternLower, Typecheck, InterpLower, BufferBuild, @@ -142,6 +149,7 @@ impl PipelineStage { match self { Self::Tco => "tco", Self::YieldLower => "yield_lower", + Self::PatternLower => "pattern_lower", Self::Typecheck => "typecheck", Self::InterpLower => "interp_lower", Self::BufferBuild => "buffer_build", @@ -878,7 +886,9 @@ pub fn lower_loaded_yield_modules( let marked = marked.with_run_entry(""); let mut errors = Vec::new(); for index in 0..loaded.len() { - if !crate::yield_lowering::has_yield_fns(&loaded[index].items) { + if !crate::yield_lowering::has_yield_fns(&loaded[index].items) + && !crate::ir::nested_patterns::has_nested_patterns(&loaded[index].items) + { continue; } let deps: Vec = loaded[..index].to_vec(); @@ -986,6 +996,23 @@ pub fn front(items: &mut Vec, cfg: FrontConfig<'_, '_>) -> FrontResult }) .collect(); let phase_one = typecheck(&written, mode); + let nested_in_yield = if phase_one.errors.is_empty() { + crate::ir::nested_patterns::nested_patterns_in_yield_fns(items) + } else { + Vec::new() + }; + if !nested_in_yield.is_empty() { + let tc = TypeCheckResult { + errors: nested_in_yield, + ..phase_one + }; + result + .pass_diagnostics + .push(diag_for_typecheck(&tc, items.len())); + fire(PipelineStage::Typecheck, items); + result.typecheck = Some(tc); + return result; + } // The answer modules say what they answer in their own headers, and // the check has just read every module this one can see. let marked = marked.with_answer_pairs(&phase_one.answers); @@ -1015,6 +1042,25 @@ pub fn front(items: &mut Vec, cfg: FrontConfig<'_, '_>) -> FrontResult } result.yield_lowering = Some(report); fire(PipelineStage::YieldLower, items); + if crate::ir::nested_patterns::has_nested_patterns(items) { + let errors = crate::ir::nested_patterns::lower_nested_patterns( + items, + &phase_one.pattern_ctor_families, + ); + fire(PipelineStage::PatternLower, items); + if !errors.is_empty() { + let tc = TypeCheckResult { + errors, + ..phase_one + }; + result + .pass_diagnostics + .push(diag_for_typecheck(&tc, items.len())); + fire(PipelineStage::Typecheck, items); + result.typecheck = Some(tc); + return result; + } + } let mut tc = typecheck(items, mode); if tc.errors.is_empty() { tc.errors.extend(crate::resolver::check_shadowing( @@ -1028,6 +1074,30 @@ pub fn front(items: &mut Vec, cfg: FrontConfig<'_, '_>) -> FrontResult ..phase_one }, } + } else if crate::ir::nested_patterns::has_nested_patterns(items) { + // Checked as written first, so exhaustiveness, redundancy, type + // and shadowing errors name the patterns the user wrote; then the + // nested patterns are compiled to flat matches and the lowered + // program is checked again, which stamps the nodes the + // compilation made. + let phase_one = typecheck_gate(items, mode, &items[..user_program_len]); + if !phase_one.errors.is_empty() { + phase_one + } else { + let errors = crate::ir::nested_patterns::lower_nested_patterns( + items, + &phase_one.pattern_ctor_families, + ); + fire(PipelineStage::PatternLower, items); + if errors.is_empty() { + typecheck(items, mode) + } else { + TypeCheckResult { + errors, + ..phase_one + } + } + } } else { typecheck_gate(items, mode, &items[..user_program_len]) }; diff --git a/src/ir/string_index.rs b/src/ir/string_index.rs index 65a7291d6..6aed6df90 100644 --- a/src/ir/string_index.rs +++ b/src/ir/string_index.rs @@ -1232,6 +1232,11 @@ fn pattern_bindings(pattern: &Pattern) -> Vec { 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(), } } diff --git a/src/ir/vars.rs b/src/ir/vars.rs index 0e89db083..088a22ccf 100644 --- a/src/ir/vars.rs +++ b/src/ir/vars.rs @@ -171,6 +171,13 @@ pub fn pattern_bindings(pat: &Pattern) -> HashSet { bindings.extend(pattern_bindings(p)); } } + Pattern::ConstructorNested(..) | Pattern::List { .. } => { + for name in pat.binder_names() { + if name != "_" { + bindings.insert(name.to_string()); + } + } + } Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => {} } bindings diff --git a/src/main/commands.rs b/src/main/commands.rs index e0c98f1a6..08057806f 100644 --- a/src/main/commands.rs +++ b/src/main/commands.rs @@ -622,7 +622,17 @@ fn walk_pattern_for_exposes( .collect::>(); mark_path_use(&parts, dep_targets, unique_type_owner, used_by_target); } - Pattern::Tuple(items) => { + Pattern::ConstructorNested(path, fields) => { + let parts = path + .split('.') + .map(|part| part.to_string()) + .collect::>(); + mark_path_use(&parts, dep_targets, unique_type_owner, used_by_target); + for field in fields { + walk_pattern_for_exposes(field, dep_targets, unique_type_owner, used_by_target); + } + } + Pattern::Tuple(items) | Pattern::List { items, .. } => { for item in items { walk_pattern_for_exposes(item, dep_targets, unique_type_owner, used_by_target); } @@ -4888,6 +4898,7 @@ pub(super) fn cmd_emit_ir_after(file: &str, module_root_override: Option<&str>, "mir" => Some(PipelineStage::NameResolve), "tco" => Some(PipelineStage::Tco), "yield_lower" => Some(PipelineStage::YieldLower), + "pattern_lower" => Some(PipelineStage::PatternLower), "typecheck" => Some(PipelineStage::Typecheck), "interp_lower" => Some(PipelineStage::InterpLower), "buffer_build" => Some(PipelineStage::BufferBuild), diff --git a/src/main/format_cmd.rs b/src/main/format_cmd.rs index 09f1124c6..e2b6b795d 100644 --- a/src/main/format_cmd.rs +++ b/src/main/format_cmd.rs @@ -477,6 +477,61 @@ fn normalize_function_header_effects_tracked( .collect() } +/// Per-line formatter for match-arm patterns: an arm line +/// ` -> ` gets its pattern in the canonical +/// spelling (`[a, b, ..rest]`, `Option.Some(0)`, `(x, _)`). Only +/// whitespace inside the pattern ever changes: a rewrite whose text +/// differs from the original in anything but whitespace is dropped. +fn normalize_match_arm_patterns_tracked( + lines: Vec, + violations: &mut Vec, + line_offset: Option<&[usize]>, +) -> Vec { + lines + .into_iter() + .enumerate() + .map(|(idx, line)| { + let rewritten = normalize_match_arm_pattern_line(&line); + if rewritten != line { + let source_line = line_offset + .and_then(|off| off.get(idx)) + .copied() + .unwrap_or(idx + 1); + violations.push(aver::diagnostics::model::FormatViolation { + line: source_line, + col: 1, + rule: "bad-match-pattern", + message: "match pattern spacing differs from canonical form".to_string(), + before: Some(line.clone()), + after: Some(rewritten.clone()), + }); + } + rewritten + }) + .collect() +} + +fn normalize_match_arm_pattern_line(line: &str) -> String { + let body = line.trim_start_matches(' '); + let indent = &line[..line.len() - body.len()]; + if indent.is_empty() { + return line.to_string(); + } + let Some((pattern, arrow_col)) = aver::parser::parse_match_arm_head(body) else { + return line.to_string(); + }; + let Some(arrow_byte) = body.char_indices().nth(arrow_col).map(|(byte, _)| byte) else { + return line.to_string(); + }; + let written = &body[..arrow_byte]; + let canonical = aver::ast::unparse::pattern_to_source(&pattern); + let squeeze = |s: &str| s.chars().filter(|c| !c.is_whitespace()).collect::(); + if squeeze(written) != squeeze(&canonical) || written.trim_end() == canonical { + return line.to_string(); + } + format!("{indent}{canonical} {}", &body[arrow_byte..]) +} + fn normalize_effect_declaration_blocks_tracked( lines: Vec, violations: &mut Vec, @@ -899,6 +954,7 @@ fn normalize_source_lines_tracked( let lines = normalize_effect_declaration_blocks_tracked(lines, violations, Some(&line_offset)); let lines = normalize_function_header_effects_tracked(lines, violations, Some(&line_offset)); + let lines = normalize_match_arm_patterns_tracked(lines, violations, Some(&line_offset)); let lines = normalize_module_intent_blocks_tracked(lines, violations, Some(&line_offset)); let lines = normalize_module_effects_blocks_tracked(lines, violations, Some(&line_offset)); normalize_inline_decision_fields_tracked(lines, violations, Some(&line_offset)) @@ -1385,6 +1441,35 @@ pub fn format_source(source: &str) -> String { mod tests { use super::{format_source, try_format_source}; + #[test] + fn prints_match_patterns_in_canonical_spelling() { + let src = "fn f(xs: List>) -> Int\n ? \"t\"\n match xs\n [ ] -> 0\n [Option.Some( 0 ),..rest] -> 1\n [a,b] -> 2\n [ .. all ] -> 3\n"; + let got = format_source(src); + assert_eq!( + got, + "fn f(xs: List>) -> Int\n ? \"t\"\n match xs\n [] -> 0\n [Option.Some(0), ..rest] -> 1\n [a, b] -> 2\n [..all] -> 3\n" + ); + assert_eq!( + format_source(&got), + got, + "canonical output is a fixed point" + ); + let (_, violations) = try_format_source(src).expect("format"); + assert_eq!( + violations + .iter() + .filter(|v| v.rule == "bad-match-pattern") + .count(), + 4 + ); + } + + #[test] + fn match_pattern_rule_leaves_string_literals_alone() { + let src = "fn f(s: String) -> Int\n ? \"t\"\n match s\n \"a b\" -> 0\n _ -> 1\n"; + assert_eq!(format_source(src), src); + } + #[test] fn normalizes_line_endings_and_trailing_ws() { let src = "module A\r\n fn x() -> Int \r\n 1\t \r\n"; diff --git a/src/parser/mod.rs b/src/parser/mod.rs index 9eb39a772..2512659bc 100644 --- a/src/parser/mod.rs +++ b/src/parser/mod.rs @@ -58,4 +58,5 @@ mod expr; mod functions; mod module; mod patterns; +pub use patterns::parse_match_arm_head; mod types; diff --git a/src/parser/patterns.rs b/src/parser/patterns.rs index 040321f68..b7e2c2e0b 100644 --- a/src/parser/patterns.rs +++ b/src/parser/patterns.rs @@ -1,5 +1,30 @@ use super::*; +/// Read the head of one match-arm line: `line` (indentation stripped) is +/// `pattern -> body`; the result is the arm's pattern and the char index +/// where `->` starts. `None` for anything else — a line with no `->`, or +/// whose text before `->` is not exactly one pattern. The formatter uses +/// it to print arm patterns in their canonical spelling. +pub fn parse_match_arm_head(line: &str) -> Option<(Pattern, usize)> { + let tokens = crate::lexer::Lexer::new(line).tokenize().ok()?; + let arrow = tokens + .iter() + .position(|token| token.kind == TokenKind::Arrow)?; + let arrow_col = tokens[arrow].col; + let mut head: Vec = tokens[..arrow].to_vec(); + head.push(Token { + kind: TokenKind::Eof, + line: tokens[arrow].line, + col: arrow_col, + }); + let mut parser = Parser::new(head); + let pattern = parser.parse_pattern().ok()?; + if !parser.is_eof() { + return None; + } + Some((pattern, arrow_col.checked_sub(1)?)) +} + impl Parser { pub(super) fn parse_match(&mut self) -> Result { self.expect_exact(&TokenKind::Match)?; @@ -70,22 +95,48 @@ impl Parser { return Ok(Pattern::EmptyList); } - let head = self.expect_user_identifier( - "Expected identifier for list head in [head, ..tail] pattern", - "pattern binders", - )?; - - self.expect_exact(&TokenKind::Comma)?; - self.expect_exact(&TokenKind::Dot)?; - self.expect_exact(&TokenKind::Dot)?; - - let tail = self.expect_user_identifier( - "Expected identifier for list tail in [head, ..tail] pattern", - "pattern binders", - )?; - + // `[p1, p2, ..rest]`, `[p1, p2]`, `[..rest]`: element + // patterns separated by commas, optionally closed by one + // `..binder` for the remaining list. + let mut items = Vec::new(); + let mut rest = None; + loop { + if self.check_exact(&TokenKind::Dot) { + self.advance(); + self.expect_exact(&TokenKind::Dot)?; + rest = Some(self.expect_user_identifier( + "Expected identifier after '..' in list pattern like [head, ..tail]", + "pattern binders", + )?); + if !self.check_exact(&TokenKind::RBracket) { + return Err(self.error( + "'..rest' must be the last part of a list pattern, like [a, b, ..rest]" + .to_string(), + )); + } + break; + } + items.push(self.parse_pattern()?); + if self.check_exact(&TokenKind::Comma) { + self.advance(); + continue; + } + break; + } self.expect_exact(&TokenKind::RBracket)?; - Ok(Pattern::Cons(head, tail)) + + // `[head, ..tail]` with two binders keeps its original flat + // form; every other shape is the general list pattern. + if let (Some(tail), [single]) = (&rest, items.as_slice()) { + match single { + Pattern::Ident(head) => return Ok(Pattern::Cons(head.clone(), tail.clone())), + Pattern::Wildcard => { + return Ok(Pattern::Cons("_".to_string(), tail.clone())); + } + _ => {} + } + } + Ok(Pattern::List { items, rest }) } TokenKind::LParen => { self.advance(); // '(' @@ -116,26 +167,33 @@ impl Parser { name ))); } - let mut bindings = vec![]; + let mut fields = vec![]; if self.check_exact(&TokenKind::LParen) { self.advance(); while !self.check_exact(&TokenKind::RParen) && !self.is_eof() { - if self.check_exact(&TokenKind::Comma) { - self.advance(); - continue; - } - if matches!(self.current().kind, TokenKind::Ident(_)) { - bindings.push(self.expect_user_identifier( - "Expected constructor pattern binding", - "pattern binders", - )?); - } else { + fields.push(self.parse_pattern()?); + if !self.check_exact(&TokenKind::Comma) { break; } + self.advance(); } self.expect_exact(&TokenKind::RParen)?; } - Ok(Pattern::Constructor(name, bindings)) + // Fields that are all binders (or `_`) keep the flat form + // every backend reads; any literal, constructor, tuple or + // list field makes it a nested constructor pattern. + let binders: Option> = fields + .iter() + .map(|field| match field { + Pattern::Ident(name) => Some(name.clone()), + Pattern::Wildcard => Some("_".to_string()), + _ => None, + }) + .collect(); + match binders { + Some(bindings) => Ok(Pattern::Constructor(name, bindings)), + None => Ok(Pattern::ConstructorNested(name, fields)), + } } TokenKind::Ident(_) => Ok(Pattern::Ident(self.expect_user_identifier( "Expected match pattern identifier", @@ -162,7 +220,7 @@ impl Parser { Ok(Pattern::Literal(Literal::Bool(b))) } _ => Err(self.error(format!( - "Expected match pattern (identifier, literal, '[]', tuple, or constructor), found {}", + "Expected match pattern (identifier, literal, list, tuple, or constructor), found {}", self.current().kind ))), } diff --git a/src/resolver.rs b/src/resolver.rs index 595ad92c6..13ebd0161 100644 --- a/src/resolver.rs +++ b/src/resolver.rs @@ -411,6 +411,13 @@ impl<'a> ResolverState<'a> { slots } Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => Vec::new(), + // Compiled away by the front door before a program is + // resolved; slots in binder order keep the walk total. + Pattern::ConstructorNested(..) | Pattern::List { .. } => pattern + .binder_names() + .into_iter() + .map(|name| self.declare(name, Type::Invalid)) + .collect(), } } } @@ -614,6 +621,9 @@ impl ShadowWalker<'_> { Self::pattern_binders(item, out); } } + Pattern::ConstructorNested(..) | Pattern::List { .. } => { + out.extend(pattern.binder_names().into_iter().map(str::to_string)) + } } } diff --git a/src/source.rs b/src/source.rs index 042fc4d62..767845bd2 100644 --- a/src/source.rs +++ b/src/source.rs @@ -587,7 +587,10 @@ fn compute_lowering_memo( let yielding: Vec = dependencies .iter() .enumerate() - .filter(|(_, module)| crate::yield_lowering::has_yield_fns(&module.items)) + .filter(|(_, module)| { + crate::yield_lowering::has_yield_fns(&module.items) + || crate::ir::nested_patterns::has_nested_patterns(&module.items) + }) .map(|(index, _)| index) .collect(); if yielding.is_empty() { @@ -601,7 +604,9 @@ fn compute_lowering_memo( // A module that still has `yield` functions failed to lower; // leave it out so the next caller retries it (and hits the same // errors) instead of memoizing a broken half-state. - if !crate::yield_lowering::has_yield_fns(&entry.items) { + if !crate::yield_lowering::has_yield_fns(&entry.items) + && !crate::ir::nested_patterns::has_nested_patterns(&entry.items) + { memo.insert(entry.path.clone(), entry.clone()); } } diff --git a/src/stdlib/profile_render.rs b/src/stdlib/profile_render.rs index 210b42cc9..b2a5c3783 100644 --- a/src/stdlib/profile_render.rs +++ b/src/stdlib/profile_render.rs @@ -134,6 +134,23 @@ fn pattern(pattern: &Pattern) -> Result { } Pattern::Constructor(name, bindings) if bindings.is_empty() => name.clone(), Pattern::Constructor(name, bindings) => format!("{name}({})", bindings.join(", ")), + Pattern::ConstructorNested(name, fields) => { + let rendered = fields + .iter() + .map(self::pattern) + .collect::, _>>()?; + format!("{name}({})", rendered.join(", ")) + } + Pattern::List { items, rest } => { + let mut rendered = items + .iter() + .map(self::pattern) + .collect::, _>>()?; + if let Some(rest) = rest { + rendered.push(format!("..{rest}")); + } + format!("[{}]", rendered.join(", ")) + } }) } diff --git a/src/types/checker/exhaustiveness.rs b/src/types/checker/exhaustiveness.rs index 17d8d3372..e68107cc2 100644 --- a/src/types/checker/exhaustiveness.rs +++ b/src/types/checker/exhaustiveness.rs @@ -98,7 +98,9 @@ impl TypeChecker { let witness_msg = if let Some(first) = witness_vec.first() { if is_catch_all_witness(first) { "missing catch-all (_) pattern".to_string() - } else if matches!(first, CoverPat::Cons(_, _)) { + } else if matches!(first, CoverPat::Cons(h, t) + if matches!((&**h, &**t), (CoverPat::Wild, CoverPat::Wild))) + { "missing pattern [h, ..t]".to_string() } else { format!("missing pattern {}", format_cover_pattern(first)) @@ -121,6 +123,12 @@ impl TypeChecker { if types.is_empty() { return if rows.is_empty() { Some(vec![]) } else { None }; } + // Nothing left to cover these columns: every value is missing, and + // `_` says so. Drilling into the first constructor would name one + // arbitrary shape (`[_]`) instead of the whole gap (`[_, .._]`). + if rows.is_empty() { + return Some(vec![CoverPat::Wild; types.len()]); + } if depth >= EXHAUSTIVENESS_MAX_DEPTH { return None; } @@ -314,6 +322,21 @@ fn normalize_pattern(pattern: &Pattern) -> CoverPat { Pattern::Constructor(name, bindings) => { CoverPat::Constructor(name.clone(), vec![CoverPat::Wild; bindings.len()]) } + Pattern::ConstructorNested(name, fields) => { + CoverPat::Constructor(name.clone(), fields.iter().map(normalize_pattern).collect()) + } + // `[a, b, ..rest]` is `a :: b :: rest`; without `..rest` the + // chain ends in `[]`, so list patterns cover by length. + Pattern::List { items, rest } => { + let tail = if rest.is_some() { + CoverPat::Wild + } else { + CoverPat::EmptyList + }; + items.iter().rev().fold(tail, |tail, item| { + CoverPat::Cons(Box::new(normalize_pattern(item)), Box::new(tail)) + }) + } } } @@ -437,11 +460,24 @@ fn format_cover_pattern(pat: &CoverPat) -> String { CoverPat::Lit(Literal::Unit) => "Unit".to_string(), CoverPat::EmptyList => "[]".to_string(), CoverPat::Cons(head, tail) => { - format!( - "[{}, ..{}]", - format_cover_pattern(head), - format_cover_pattern(tail) - ) + // Print a cons chain as the list pattern that spells it: + // `[_, _]`, `[0, .._]`. + let mut parts = vec![format_cover_pattern(head)]; + let mut cursor = &**tail; + loop { + match cursor { + CoverPat::Cons(h, t) => { + parts.push(format_cover_pattern(h)); + cursor = t; + } + CoverPat::EmptyList => break, + other => { + parts.push(format!("..{}", format_cover_pattern(other))); + break; + } + } + } + format!("[{}]", parts.join(", ")) } CoverPat::Tuple(items) => { let parts = items.iter().map(format_cover_pattern).collect::>(); diff --git a/src/types/checker/infer/patterns.rs b/src/types/checker/infer/patterns.rs index bfc55aee4..ee7ef0de7 100644 --- a/src/types/checker/infer/patterns.rs +++ b/src/types/checker/infer/patterns.rs @@ -13,7 +13,14 @@ impl TypeChecker { expected: Option<&Type>, ) -> Type { let mut bindings = Vec::new(); + let errors_before = self.errors.len(); self.collect_pattern_bindings(pattern, subject_ty, &mut bindings); + // A pattern error belongs to its arm, not to the enclosing fn. + if body.line > 0 { + for error in &mut self.errors[errors_before..] { + error.line = body.line; + } + } let mut prev = Vec::new(); for (bind_name, bind_ty) in bindings { @@ -87,6 +94,114 @@ impl TypeChecker { unknowns() } + /// The field types a constructor pattern binds, after the checks + /// every constructor pattern gets: no match on an opaque type or a + /// capability resource, and no `Result` / `Option` constructor + /// against a subject of another type. `None` when the pattern is + /// refused (its fields then bind `Invalid`). + fn constructor_pattern_field_types( + &mut self, + name: &str, + subject_ty: &Type, + arity: usize, + ) -> Option> { + // Check if this pattern matches on an opaque type's representation. + // Iron — A3: resolve the bare type prefix through + // `sig_aliases` because `opaque_types` is keyed by the + // canonical `Module.Type` form. + let type_prefix = name.split('.').next().unwrap_or(name); + let canon_prefix = self.canonical_type_name(type_prefix); + if !self.self_host_mode && self.opaque_types.contains(&canon_prefix) { + if self.is_capability_resource_type(type_prefix) { + self.error(format!( + "Cannot pattern match on capability resource '{}'", + type_prefix + )); + } else { + self.error(format!( + "Cannot pattern match on opaque type '{}'", + type_prefix + )); + } + return None; + } + // A `Result` / `Option` constructor pattern against a + // subject that is neither is always a bug: no value of the + // subject's type can ever take the arm, so the match walks + // off the end at runtime with no diagnostic. The literal + // smart-constructor discharge makes this reachable by + // ordinary edits — `match Bytes.fromList([1, 2])` used to + // scrutinise a `Result` and now scrutinises a `Bytes` — so + // the migration has to be loud instead of silent. + if matches!(type_prefix, "Result" | "Option") + && !matches!( + subject_ty, + Type::Result(_, _) | Type::Option(_) | Type::Invalid | Type::Var(_) + ) + { + self.error(format!( + "Pattern '{}' matches a {} value, but the match subject is {}", + name, + type_prefix, + subject_ty.display() + )); + } + self.record_pattern_constructor_family(name, subject_ty); + Some(self.pattern_constructor_binding_types(name, subject_ty, arity)) + } + + /// A literal pattern can only ever match a value of its own + /// primitive type; against any other concrete subject the arm is + /// dead, so say so. Named types (refinements, records) and + /// not-yet-known types are left alone. + fn check_literal_pattern(&mut self, literal: &Literal, subject_ty: &Type) { + let fits = match (literal, subject_ty) { + (_, Type::Invalid | Type::Var(_) | Type::Named { .. }) => return, + (Literal::Int(_) | Literal::BigInt(_), Type::Int) + | (Literal::Float(_), Type::Float) + | (Literal::Str(_), Type::Str) + | (Literal::Bool(_), Type::Bool) + | (Literal::Unit, Type::Unit) => true, + _ => false, + }; + if !fits { + let kind = match literal { + Literal::Int(_) | Literal::BigInt(_) => "Int", + Literal::Float(_) => "Float", + Literal::Str(_) => "String", + Literal::Bool(_) => "Bool", + Literal::Unit => "Unit", + }; + self.error(format!( + "Literal pattern of type {} cannot match a value of type {}", + kind, + subject_ty.display() + )); + } + } + + /// Remember, for the constructor spelled `name` in a pattern, the + /// variants of the sum type it belongs to. The nested-pattern + /// compiler reads it to know when the constructors of one switch + /// cover the whole type, so it never emits a default arm no value + /// can reach. + fn record_pattern_constructor_family(&mut self, name: &str, subject_ty: &Type) { + let Type::Named { + name: type_name, .. + } = subject_ty + else { + return; + }; + if self.pattern_ctor_families.contains_key(name) { + return; + } + if let Some(variants) = self.variants_for(type_name) { + let variants = variants.clone(); + self.pattern_ctor_families + .insert(name.to_string(), variants); + } + } + pub(in super::super) fn collect_pattern_bindings( &mut self, pattern: &Pattern, @@ -108,60 +223,52 @@ impl TypeChecker { } } Pattern::Constructor(name, bindings) => { - // Check if this pattern matches on an opaque type's representation. - // Iron — A3: resolve the bare type prefix through - // `sig_aliases` because `opaque_types` is keyed by the - // canonical `Module.Type` form. - let type_prefix = name.split('.').next().unwrap_or(name); - let canon_prefix = self.canonical_type_name(type_prefix); - if !self.self_host_mode && self.opaque_types.contains(&canon_prefix) { - if self.is_capability_resource_type(type_prefix) { - self.error(format!( - "Cannot pattern match on capability resource '{}'", - type_prefix - )); - } else { - self.error(format!( - "Cannot pattern match on opaque type '{}'", - type_prefix - )); - } + let Some(binding_tys) = + self.constructor_pattern_field_types(name, subject_ty, bindings.len()) + else { for bind_name in bindings { if bind_name != "_" { out.push((bind_name.clone(), Type::Invalid)); } } return; - } - // A `Result` / `Option` constructor pattern against a - // subject that is neither is always a bug: no value of the - // subject's type can ever take the arm, so the match walks - // off the end at runtime with no diagnostic. The literal - // smart-constructor discharge makes this reachable by - // ordinary edits — `match Bytes.fromList([1, 2])` used to - // scrutinise a `Result` and now scrutinises a `Bytes` — so - // the migration has to be loud instead of silent. - if matches!(type_prefix, "Result" | "Option") - && !matches!( - subject_ty, - Type::Result(_, _) | Type::Option(_) | Type::Invalid | Type::Var(_) - ) - { - self.error(format!( - "Pattern '{}' matches a {} value, but the match subject is {}", - name, - type_prefix, - subject_ty.display() - )); - } - let binding_tys = - self.pattern_constructor_binding_types(name, subject_ty, bindings.len()); + }; for (bind_name, bind_ty) in bindings.iter().zip(binding_tys) { if bind_name != "_" { out.push((bind_name.clone(), bind_ty)); } } } + Pattern::ConstructorNested(name, fields) => { + let field_tys = self + .constructor_pattern_field_types(name, subject_ty, fields.len()) + .unwrap_or_else(|| vec![Type::Invalid; fields.len()]); + for (field, field_ty) in fields.iter().zip(field_tys.iter()) { + self.collect_pattern_bindings(field, field_ty, out); + } + } + Pattern::List { items, rest } => { + let elem_ty = match subject_ty { + Type::List(inner) => *inner.clone(), + Type::Invalid | Type::Var(_) => Type::Invalid, + other => { + self.error(format!( + "List pattern matches a List value, but the match subject is {}", + other.display() + )); + Type::Invalid + } + }; + for item in items { + self.collect_pattern_bindings(item, &elem_ty, out); + } + if let Some(rest) = rest + && rest != "_" + { + out.push((rest.clone(), Type::List(Box::new(elem_ty)))); + } + } + Pattern::Literal(literal) => self.check_literal_pattern(literal, subject_ty), Pattern::Tuple(items) => { let elem_tys = match subject_ty { Type::Tuple(elems) if elems.len() == items.len() => elems.clone(), diff --git a/src/types/checker/mod.rs b/src/types/checker/mod.rs index 102ed27a4..5fc6772f2 100644 --- a/src/types/checker/mod.rs +++ b/src/types/checker/mod.rs @@ -91,6 +91,12 @@ pub struct TypeCheckResult { /// whose source spelling would not name them here; see /// [`SymbolTable::generated_type_spellings`]. pub type_spellings: HashMap, + /// For every constructor spelled in a pattern of a user sum type, + /// the variant names of that type (`"Shape.Circle"` → + /// `["Circle", "Rect"]`). The nested-pattern compiler + /// ([`crate::ir::nested_patterns`]) reads it to tell a switch that + /// covers the whole type from one that needs a default arm. + pub pattern_ctor_families: HashMap>, } pub fn run_type_check(items: &[TopLevel]) -> Vec { @@ -374,6 +380,7 @@ fn finalize_check_result(mut checker: TypeChecker, items: &[TopLevel]) -> TypeCh imported_processes: checker.imported_processes, answers, type_spellings, + pattern_ctor_families: checker.pattern_ctor_families, } } @@ -724,6 +731,8 @@ struct TypeChecker { /// Variant names for sum types: "Shape" → ["Circle", "Rect", "Point"]. /// Pre-populated for Result and Option; extended by user-defined sum types. type_variants: HashMap>, + /// See [`TypeCheckResult::pattern_ctor_families`]. + pattern_ctor_families: HashMap>, /// Module prefix of the items currently being checked. `None` /// while checking entry-scope items. Per-module sub-checkers /// (`check_loaded_module_bodies`) set this to the dep module's @@ -819,6 +828,7 @@ impl TypeChecker { value_members: HashMap::new(), record_field_types: HashMap::new(), type_variants, + pattern_ctor_families: HashMap::new(), current_module_prefix: None, available_laws: std::collections::BTreeSet::new(), imported_processes: HashMap::new(), diff --git a/src/yield_lowering/build.rs b/src/yield_lowering/build.rs index cb211de5b..c1e00e44f 100644 --- a/src/yield_lowering/build.rs +++ b/src/yield_lowering/build.rs @@ -143,6 +143,13 @@ pub(super) fn pattern_binders(pattern: &Pattern, out: &mut Vec) { Pattern::Constructor(_, names) => { out.extend(names.iter().filter(|n| *n != "_").cloned()); } + Pattern::ConstructorNested(..) | Pattern::List { .. } => out.extend( + pattern + .binder_names() + .into_iter() + .filter(|n| *n != "_") + .map(str::to_string), + ), } } diff --git a/src/yield_lowering/trace/source/inline.rs b/src/yield_lowering/trace/source/inline.rs index da83e660c..5fae9b136 100644 --- a/src/yield_lowering/trace/source/inline.rs +++ b/src/yield_lowering/trace/source/inline.rs @@ -106,11 +106,23 @@ impl<'a> Compiler<'a> { bind(field); } } - Pattern::Tuple(fields) => { + Pattern::Tuple(fields) | Pattern::ConstructorNested(_, fields) => { for field in fields { self.rename_pattern(field, names); } } + Pattern::List { items, rest } => { + for item in items { + self.rename_pattern(item, names); + } + if let Some(rest) = rest + && rest != "_" + { + let fresh = self.name(); + names.insert(rest.clone(), fresh.clone()); + *rest = fresh; + } + } Pattern::Wildcard | Pattern::Literal(_) | Pattern::EmptyList => {} } } diff --git a/tests/fixtures/nested_patterns.av b/tests/fixtures/nested_patterns.av new file mode 100644 index 000000000..0900e9e34 --- /dev/null +++ b/tests/fixtures/nested_patterns.av @@ -0,0 +1,122 @@ +module Nested + intent = "Nested literal, constructor and list patterns, run the same on every backend." + effects [Console.print] + +type Shape + Circle(Int) + Rect(Int, Int) + Dot + +fn classify(o: Option) -> String + ? "Literal inside a constructor." + match o + Option.Some(0) -> "zero" + Option.Some(1) -> "one" + Option.Some(n) -> "many {n}" + Option.None -> "none" + +verify classify + classify(Option.Some(0)) => "zero" + classify(Option.Some(7)) => "many 7" + classify(Option.None) => "none" + +fn okText(r: Result) -> Int + ? "String literal inside Result.Ok." + match r + Result.Ok("x") -> 1 + Result.Ok(s) -> String.len(s) + Result.Err(0) -> 0 - 1 + Result.Err(e) -> e + +fn flags(p: Option) -> Int + ? "Bool literals nested." + match p + Option.Some(true) -> 1 + Option.Some(false) -> 2 + Option.None -> 3 + +fn area(s: Shape) -> Int + ? "Literals in user constructor fields." + match s + Shape.Rect(0, _) -> 0 + Shape.Rect(_, 0) -> 0 + Shape.Rect(w, h) -> w * h + Shape.Circle(0) -> 0 + Shape.Circle(r) -> 3 * r * r + Shape.Dot -> 1 + +fn deep(o: Option>) -> Int + ? "Constructors inside constructors." + match o + Option.Some(Option.Some(7)) -> 70 + Option.Some(Option.Some(x)) -> x + Option.Some(Option.None) -> 0 - 1 + Option.None -> 0 - 2 + +fn pairs(t: Tuple>) -> Int + ? "Tuple with a nested constructor." + match t + (0, Option.Some(1)) -> 100 + (a, Option.Some(b)) -> a + b + (a, Option.None) -> a + +fn size(xs: List) -> String + ? "List patterns by length." + match xs + [] -> "empty" + [a] -> "one {a}" + [a, b] -> "two {a} {b}" + [0, ..rest] -> "zero then {List.len(rest)}" + [a, b, ..rest] -> "many {a} {b} +{List.len(rest)}" + +verify size + size([]) => "empty" + size([0, 1, 2]) => "zero then 2" + size([5, 6, 7, 8]) => "many 5 6 +2" + +fn firstSome(xs: List>) -> Int + ? "Constructor pattern as a list element." + match xs + [Option.Some(x), ..rest] -> x + [Option.None, ..rest] -> firstSome(rest) + [] -> 0 + +fn whole(xs: List) -> Int + ? "Rest binder alone." + match xs + [..all] -> List.len(all) + +fn main() -> Unit + ! [Console.print] + Console.print("{classify(Option.Some(0))}") + Console.print("{classify(Option.Some(1))}") + Console.print("{classify(Option.Some(5))}") + Console.print("{classify(Option.None)}") + Console.print("{okText(Result.Ok("x"))}") + Console.print("{okText(Result.Ok("hello"))}") + Console.print("{okText(Result.Err(0))}") + Console.print("{okText(Result.Err(9))}") + Console.print("{flags(Option.Some(true))}") + Console.print("{flags(Option.Some(false))}") + Console.print("{flags(Option.None)}") + Console.print("{area(Shape.Rect(0, 5))}") + Console.print("{area(Shape.Rect(4, 0))}") + Console.print("{area(Shape.Rect(4, 5))}") + Console.print("{area(Shape.Circle(0))}") + Console.print("{area(Shape.Circle(2))}") + Console.print("{area(Shape.Dot)}") + Console.print("{deep(Option.Some(Option.Some(7)))}") + Console.print("{deep(Option.Some(Option.Some(3)))}") + Console.print("{deep(Option.Some(Option.None))}") + Console.print("{deep(Option.None)}") + Console.print("{pairs((0, Option.Some(1)))}") + Console.print("{pairs((2, Option.Some(3)))}") + Console.print("{pairs((4, Option.None))}") + Console.print("{size([])}") + Console.print("{size([1])}") + Console.print("{size([1, 2])}") + Console.print("{size([0, 2, 3])}") + Console.print("{size([1, 2, 3, 4])}") + Console.print("{firstSome([Option.None, Option.None, Option.Some(4)])}") + Console.print("{firstSome([Option.None])}") + Console.print("{whole([1, 2, 3])}") diff --git a/tests/fixtures/nested_patterns.expected b/tests/fixtures/nested_patterns.expected new file mode 100644 index 000000000..b0f5fffdb --- /dev/null +++ b/tests/fixtures/nested_patterns.expected @@ -0,0 +1,32 @@ +zero +one +many 5 +none +1 +5 +-1 +9 +1 +2 +3 +0 +0 +20 +0 +12 +1 +70 +3 +-1 +-2 +100 +5 +4 +empty +one 1 +two 1 2 +zero then 2 +many 1 2 +2 +4 +0 +3 diff --git a/tests/fixtures/nested_patterns_law.av b/tests/fixtures/nested_patterns_law.av new file mode 100644 index 000000000..e957ec15e --- /dev/null +++ b/tests/fixtures/nested_patterns_law.av @@ -0,0 +1,33 @@ +module NestedLaw + intent = "A law over a function that matches a nested literal pattern." + +fn score(o: Option) -> Int + ? "Zero scores ten, any other present value scores itself, absence scores zero." + match o + Option.Some(0) -> 10 + Option.Some(n) -> n + Option.None -> 0 + +verify score + score(Option.Some(0)) => 10 + score(Option.Some(4)) => 4 + score(Option.None) => 0 + +verify score law presentZero + given n: Int = [0, 1, 5] + score(Option.Some(0)) => 10 + +verify score law absent + given n: Int = [0, 1] + score(Option.None) => 0 + +fn headOrZero(xs: List) -> Int + ? "First element when the list starts with a known shape." + match xs + [0, ..rest] -> 100 + [x, ..rest] -> x + [] -> 0 + +verify headOrZero law leadingZero + given k: Int = [1, 2, 3] + headOrZero([0, k]) => 100 diff --git a/tests/nested_patterns_spec.rs b/tests/nested_patterns_spec.rs new file mode 100644 index 000000000..e6e0cf884 --- /dev/null +++ b/tests/nested_patterns_spec.rs @@ -0,0 +1,112 @@ +//! Nested literal / constructor patterns and general list patterns end to +//! end: the front door compiles them into flat matches, so every backend +//! runs the same program. One fixture, one expected stdout, each backend +//! compared against it; plus the checker's diagnostics as the CLI prints +//! them. + +#[path = "support/aver_cmd.rs"] +mod aver_cmd; + +use aver_cmd::{aver_bin, cleanup, format_output, repo_root, temp_module}; +use std::process::Command; + +const FIXTURE: &str = "tests/fixtures/nested_patterns.av"; +const EXPECTED: &str = "tests/fixtures/nested_patterns.expected"; + +fn expected() -> String { + std::fs::read_to_string(repo_root().join(EXPECTED)).expect("read the expected output") +} + +fn run(extra: &[&str]) -> String { + let out = Command::new(aver_bin()) + .current_dir(repo_root()) + .arg("run") + .arg(FIXTURE) + .args(extra) + .output() + .expect("run aver"); + assert!(out.status.success(), "{}", format_output(&out)); + String::from_utf8_lossy(&out.stdout).into_owned() +} + +#[test] +fn vm_runs_nested_patterns() { + assert_eq!(run(&[]), expected()); +} + +#[cfg(feature = "wasm")] +#[test] +fn wasm_gc_runs_nested_patterns_like_the_vm() { + assert_eq!(run(&["--wasm-gc"]), expected()); +} + +#[cfg(feature = "wasip2")] +#[test] +fn wasip2_runs_nested_patterns_like_the_vm() { + assert_eq!(run(&["--wasip2"]), expected()); +} + +#[test] +fn verify_runs_cases_over_nested_patterns() { + let out = Command::new(aver_bin()) + .current_dir(repo_root()) + .arg("verify") + .arg(FIXTURE) + .output() + .expect("run aver verify"); + assert!(out.status.success(), "{}", format_output(&out)); +} + +fn check(prefix: &str, source: &str) -> String { + let path = temp_module(prefix, source); + let out = Command::new(aver_bin()) + .current_dir(repo_root()) + .arg("check") + .arg(&path) + .output() + .expect("run aver check"); + cleanup(&path); + format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ) +} + +#[test] +fn check_names_the_missing_nested_case() { + let report = check( + "nested-missing", + "module M\n intent = \"t\"\n\nfn f(o: Option) -> Int\n ? \"t\"\n match o\n Option.Some(0) -> 1\n Option.None -> 0\n", + ); + assert!( + report.contains("Non-exhaustive match: missing pattern Option.Some(_)"), + "{report}" + ); +} + +#[test] +fn check_reports_an_arm_only_the_compiled_match_can_see_is_dead() { + // No single earlier arm covers `Option.Some(_)`; `true` and `false` + // together do, which only the compiled decision tree sees. + let report = check( + "nested-dead", + "module M\n intent = \"t\"\n\nfn f(o: Option) -> Int\n ? \"t\"\n match o\n Option.Some(true) -> 1\n Option.Some(false) -> 2\n Option.Some(_) -> 3\n Option.None -> 0\n", + ); + assert!( + report.contains("Unreachable match arm: no value reaches pattern Option.Some(_)"), + "{report}" + ); +} + +#[test] +fn nested_patterns_inside_a_yield_function_are_refused() { + let report = check( + "nested-yield", + "module M\n intent = \"t\"\n\nfn f(o: Option) -> Int\n ? \"t\"\n ! [yield]\n match o\n Option.Some(0) -> 1\n _ -> 0\n", + ); + assert!( + report.contains("not supported inside the `yield` function 'f'"), + "{report}" + ); +} diff --git a/tests/parser_spec.rs b/tests/parser_spec.rs index d632d7e52..a67c23871 100644 --- a/tests/parser_spec.rs +++ b/tests/parser_spec.rs @@ -2006,3 +2006,166 @@ fn well_formed_effect_lists_still_parse() { assert_eq!(items.len(), 1, "expected one item from: {shape}"); } } + +// --------------------------------------------------------------------------- +// Nested literal / constructor patterns and general list patterns +// --------------------------------------------------------------------------- + +fn arm_patterns(src: &str) -> Vec { + let items = parse(src); + let TopLevel::FnDef(fd) = &items[0] else { + panic!("expected FnDef"); + }; + let Expr::Match { arms, .. } = single_expr_body(fd) else { + panic!("expected match"); + }; + arms.iter().map(|arm| arm.pattern.clone()).collect() +} + +#[test] +fn constructor_with_literal_field_is_a_nested_pattern() { + let pats = arm_patterns( + "fn f(o: Option) -> Int\n match o\n Option.Some(0) -> 1\n Option.Some(n) -> n\n Option.None -> 0\n", + ); + assert_eq!( + pats[0], + Pattern::ConstructorNested( + "Option.Some".to_string(), + vec![Pattern::Literal(Literal::Int(0))] + ) + ); + // All-binder fields keep the flat form every backend reads. + assert_eq!( + pats[1], + Pattern::Constructor("Option.Some".to_string(), vec!["n".to_string()]) + ); + assert_eq!( + pats[2], + Pattern::Constructor("Option.None".to_string(), vec![]) + ); +} + +#[test] +fn nested_constructor_string_bool_and_tuple_fields() { + let pats = arm_patterns( + "fn f(x: Int) -> Int\n match x\n Result.Ok(\"x\") -> 1\n Pair.Of(1, y) -> 2\n Option.Some(Option.Some(true)) -> 3\n Option.Some((0, _)) -> 4\n _ -> 5\n", + ); + assert_eq!( + pats[0], + Pattern::ConstructorNested( + "Result.Ok".to_string(), + vec![Pattern::Literal(Literal::Str("x".to_string()))] + ) + ); + assert_eq!( + pats[1], + Pattern::ConstructorNested( + "Pair.Of".to_string(), + vec![ + Pattern::Literal(Literal::Int(1)), + Pattern::Ident("y".to_string()) + ] + ) + ); + assert_eq!( + pats[2], + Pattern::ConstructorNested( + "Option.Some".to_string(), + vec![Pattern::ConstructorNested( + "Option.Some".to_string(), + vec![Pattern::Literal(Literal::Bool(true))] + )] + ) + ); + assert_eq!( + pats[3], + Pattern::ConstructorNested( + "Option.Some".to_string(), + vec![Pattern::Tuple(vec![ + Pattern::Literal(Literal::Int(0)), + Pattern::Wildcard + ])] + ) + ); +} + +#[test] +fn list_patterns_with_and_without_rest() { + let pats = arm_patterns( + "fn f(xs: List) -> Int\n match xs\n [] -> 0\n [a] -> 1\n [a, b] -> 2\n [0, ..rest] -> 3\n [a, b, ..rest] -> 4\n [Option.Some(x), ..rest] -> 5\n [h, ..t] -> 6\n [..all] -> 7\n", + ); + let ident = |name: &str| Pattern::Ident(name.to_string()); + assert_eq!(pats[0], Pattern::EmptyList); + assert_eq!( + pats[1], + Pattern::List { + items: vec![ident("a")], + rest: None + } + ); + assert_eq!( + pats[2], + Pattern::List { + items: vec![ident("a"), ident("b")], + rest: None + } + ); + assert_eq!( + pats[3], + Pattern::List { + items: vec![Pattern::Literal(Literal::Int(0))], + rest: Some("rest".to_string()) + } + ); + assert_eq!( + pats[4], + Pattern::List { + items: vec![ident("a"), ident("b")], + rest: Some("rest".to_string()) + } + ); + assert_eq!( + pats[5], + Pattern::List { + items: vec![Pattern::Constructor( + "Option.Some".to_string(), + vec!["x".to_string()] + )], + rest: Some("rest".to_string()) + } + ); + // `[head, ..tail]` with two binders keeps the flat cons form. + assert_eq!(pats[6], Pattern::Cons("h".to_string(), "t".to_string())); + assert_eq!( + pats[7], + Pattern::List { + items: vec![], + rest: Some("all".to_string()) + } + ); +} + +#[test] +fn list_rest_must_be_last_and_a_binder() { + assert!(parse_fails( + "fn f(xs: List) -> Int\n match xs\n [..rest, a] -> 0\n _ -> 1\n" + )); + assert!(parse_fails( + "fn f(xs: List) -> Int\n match xs\n [a, ..0] -> 0\n _ -> 1\n" + )); + assert!(parse_fails( + "fn f(xs: List) -> Int\n match xs\n [a, ..__rest] -> 0\n _ -> 1\n" + )); +} + +#[test] +fn nested_patterns_round_trip_through_unparse() { + let src = "fn f(xs: List>) -> Int\n match xs\n [Option.Some(0), ..rest] -> 0\n [a, b] -> 1\n _ -> 2\n"; + let items = parse(src); + let printed = aver::ast::unparse::unparse(&items).expect("unparse"); + assert!( + printed.contains("[Option.Some(0), ..rest] -> 0") && printed.contains("[a, b] -> 1"), + "{printed}" + ); + assert_eq!(parse(&printed), items); +} diff --git a/tests/proof_spec.rs b/tests/proof_spec.rs index 412fc3dc5..c9f0b4310 100644 --- a/tests/proof_spec.rs +++ b/tests/proof_spec.rs @@ -416,6 +416,19 @@ const FUEL_PROBE_AV: &str = "module FuelProbe\n\ /// /// The fixture puts five such builtins behind a compound receiver. With the /// old test in place it reports twelve build errors. +/// Laws over functions whose matches use nested literal and list patterns +/// (`Option.Some(0)`, `[0, ..rest]`). The front door compiles those matches +/// into nested ordinary matches before the exporter reads the program, so +/// the Lean definitions are ordinary nested `match`es and the laws close +/// with no `sorry`. +#[test] +fn laws_over_nested_literal_and_list_patterns_build() { + assert_proof_builds( + "tests/fixtures/nested_patterns_law.av", + "aver-proof-nested-patterns", + ); +} + #[test] fn a_method_application_in_argument_position_is_emitted_atomically() { assert_proof_builds( diff --git a/tests/rust_codegen_differential.rs b/tests/rust_codegen_differential.rs index ee7fa06b8..aa3734610 100644 --- a/tests/rust_codegen_differential.rs +++ b/tests/rust_codegen_differential.rs @@ -436,6 +436,18 @@ fn tuple_match_with_list_literal_and_option_elements_matches_between_rust_and_vm assert_plain_parity(FIXTURE, None).unwrap_or_else(|e| panic!("{e}")); } +/// Nested literal / constructor patterns and list patterns (`Option.Some(0)`, +/// `Shape.Rect(0, _)`, `[a, b, ..rest]`, `[Option.Some(x), ..rest]`). The +/// front door compiles them into nested flat matches over fresh binders +/// before any backend runs; only a build proves the Rust those matches +/// render borrows and moves the bound sub-values correctly, and only a run +/// proves the compiled decision tree takes the arm the VM takes. +#[test] +fn nested_literal_and_list_patterns_match_between_rust_and_vm() { + assert_plain_parity("tests/fixtures/nested_patterns.av", None) + .unwrap_or_else(|e| panic!("{e}")); +} + /// A one-arm wildcard match over an effectful call: `match say(x)` with a /// single `_ ->` arm is how a process performs something in place before it /// goes on, and the Rust backend used to render the arm's body alone, so the diff --git a/tests/typechecker_spec.rs b/tests/typechecker_spec.rs index aeda1e9f0..1d2c7eb21 100644 --- a/tests/typechecker_spec.rs +++ b/tests/typechecker_spec.rs @@ -5911,3 +5911,148 @@ fn a_shadowing_arm_does_not_type_a_live_variables_state_field() { errs.join("\n ") ); } + +// --------------------------------------------------------------------------- +// Nested literal / constructor patterns and list patterns +// --------------------------------------------------------------------------- + +#[test] +fn nested_literal_patterns_with_a_binder_fallback_are_exhaustive() { + let errs = errors( + "fn f(o: Option) -> Int\n match o\n Option.Some(0) -> 1\n Option.Some(n) -> n\n Option.None -> 0\n\nfn g(r: Result) -> Int\n match r\n Result.Ok(\"x\") -> 1\n Result.Ok(_) -> 2\n Result.Err(0) -> 3\n Result.Err(e) -> e\n", + ); + assert!(errs.is_empty(), "unexpected errors: {:?}", errs); +} + +#[test] +fn a_nested_literal_never_covers_its_constructor() { + let errs = errors( + "fn f(o: Option) -> Int\n match o\n Option.Some(0) -> 1\n Option.None -> 0\n", + ); + assert!( + errs.iter() + .any(|e| e == "Non-exhaustive match: missing pattern Option.Some(_)"), + "{:?}", + errs + ); +} + +#[test] +fn nested_bool_literals_cover_by_value() { + assert!( + errors( + "fn f(o: Option) -> Int\n match o\n Option.Some(true) -> 1\n Option.Some(false) -> 2\n Option.None -> 0\n", + ) + .is_empty() + ); + let errs = errors( + "fn f(o: Option) -> Int\n match o\n Option.Some(true) -> 1\n Option.None -> 0\n", + ); + assert!( + errs.iter() + .any(|e| e == "Non-exhaustive match: missing pattern Option.Some(false)"), + "{:?}", + errs + ); +} + +#[test] +fn nested_user_constructor_fields_are_checked() { + let errs = errors( + "type Shape\n Rect(Int, Int)\n Dot\n\nfn f(s: Shape) -> Int\n match s\n Shape.Rect(0, _) -> 0\n Shape.Dot -> 1\n", + ); + assert!( + errs.iter() + .any(|e| e.starts_with("Non-exhaustive match: missing pattern Shape.Rect(")), + "{:?}", + errs + ); +} + +#[test] +fn list_patterns_cover_by_length() { + assert!( + errors( + "fn f(xs: List) -> Int\n match xs\n [] -> 0\n [a] -> a\n [a, b, ..rest] -> a + b\n", + ) + .is_empty() + ); + let errs = errors( + "fn f(xs: List) -> Int\n match xs\n [] -> 0\n [a] -> a\n [a, b] -> a + b\n", + ); + assert!( + errs.iter() + .any(|e| e == "Non-exhaustive match: missing pattern [_, _, _, .._]"), + "{:?}", + errs + ); + let errs = errors( + "fn f(xs: List) -> Int\n match xs\n [0, ..rest] -> 0\n [] -> 1\n", + ); + assert!( + errs.iter() + .any(|e| e == "Non-exhaustive match: missing pattern [h, ..t]"), + "{:?}", + errs + ); +} + +#[test] +fn a_nested_arm_under_a_binder_arm_is_unreachable() { + let errs = errors( + "fn f(o: Option) -> Int\n match o\n Option.Some(n) -> n\n Option.Some(0) -> 1\n Option.None -> 0\n", + ); + assert!( + errs.iter() + .any(|e| e + .starts_with("Unreachable match arm: pattern Option.Some(0) is already covered")), + "{:?}", + errs + ); + let errs = errors( + "fn f(xs: List) -> Int\n match xs\n [] -> 0\n [_, ..rest] -> 1\n [a, b] -> 2\n", + ); + assert!( + errs.iter() + .any(|e| e.starts_with("Unreachable match arm: pattern [_, _]")), + "{:?}", + errs + ); +} + +#[test] +fn nested_pattern_binders_get_field_types() { + let errs = errors( + "fn f(xs: List>) -> String\n match xs\n [Option.Some(x), ..rest] -> x\n _ -> \"\"\n", + ); + assert!( + errs.iter() + .any(|e| e.contains("Int") && e.contains("String")), + "x is an Int, so returning it as a String must fail: {:?}", + errs + ); +} + +#[test] +fn nested_literal_of_the_wrong_type_is_rejected() { + let errs = errors( + "fn f(o: Option) -> Int\n match o\n Option.Some(\"x\") -> 1\n _ -> 0\n", + ); + assert!( + errs.iter() + .any(|e| e == "Literal pattern of type String cannot match a value of type Int"), + "{:?}", + errs + ); +} + +#[test] +fn list_pattern_against_a_non_list_is_rejected() { + let errs = errors("fn f(n: Int) -> Int\n match n\n [a, b] -> a\n _ -> 0\n"); + assert!( + errs.iter() + .any(|e| e == "List pattern matches a List value, but the match subject is Int"), + "{:?}", + errs + ); +} diff --git a/tools/website/llms.txt b/tools/website/llms.txt index 225aa181b..f434f7357 100644 --- a/tools/website/llms.txt +++ b/tools/website/llms.txt @@ -146,7 +146,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