Merge pull request #49 from aallan/c6j-effect-handler-compilation

C6j: Effect handler compilation — handle[State<T>] via host imports

Author: aallan

CHANGELOG.md

@@ -6,6 +6,17 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+## [0.0.19] - 2026-02-25
+
+### Added
+- **Effect handler compilation** (C6j — closes [#28](https://github.com/aallan/vera/issues/28)): compile `handle[State<T>]` expressions to WASM via host imports
+  - State handler translation: `handle[State<T>](@T = init) { get/put clauses } in { body }` compiles by initializing state via `state_put_T`, then compiling body with get/put mapped to host imports
+  - Handler clauses serve as specifications (not compiled) — `resume()` calls describe the default State semantics, validated by type checker
+  - Effect discharge: pure functions containing `handle[State<T>]` are compilable — state imports registered by scanning function body for handle expressions
+  - Unsupported handlers (`Exn<E>`, custom effects) cause function to be skipped with warning
+- **Reworked `examples/effect_handler.vera`**: removed `safe_parse` (uses String + undefined `parse_int`), added `test_state_init` and `test_put_get` (simple compilable tests)
+- **Codegen tests**: 14 new tests — state initialization, put/get, increment pattern, run_counter, let bindings, Bool state, WAT inspection, unsupported handler skip, example file round-trips (691 total, up from 677)
+
 ## [0.0.18] - 2026-02-25
 
 ### Added
@@ -314,7 +325,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 - Grammar: handler body simplified to avoid LALR reduce/reduce conflict
 - `pyproject.toml`: corrected build backend, package discovery, PEP 639 compliance
 
-[Unreleased]: https://github.com/aallan/vera/compare/v0.0.17...HEAD
+[Unreleased]: https://github.com/aallan/vera/compare/v0.0.19...HEAD
+[0.0.19]: https://github.com/aallan/vera/compare/v0.0.18...v0.0.19
+[0.0.18]: https://github.com/aallan/vera/compare/v0.0.17...v0.0.18
 [0.0.17]: https://github.com/aallan/vera/compare/v0.0.16...v0.0.17
 [0.0.16]: https://github.com/aallan/vera/compare/v0.0.15...v0.0.16
 [0.0.15]: https://github.com/aallan/vera/compare/v0.0.14...v0.0.15

README.md

@@ -159,7 +159,7 @@ Development follows an **interleaved spiral** — each phase adds a complete com
 | C3 | v0.0.5 | **Type checker** — decidable type checking, slot resolution, effect tracking | Done |
 | C4 | v0.0.8 | **Contract verifier** — Z3 integration, refinement types, counterexamples | Done |
 | C5 | v0.0.9 | **WASM codegen** — compile to WebAssembly, `vera compile` / `vera run` | Done |
-| C6 | v0.0.10–0.0.23 | **Codegen completeness** — ADTs, match, closures, effects, generics in WASM | **In progress** (C6a–C6i, C6h done) |
+| C6 | v0.0.10–0.0.23 | **Codegen completeness** — ADTs, match, closures, effects, generics in WASM | **In progress** (C6a–C6j done) |
 | C7 | — | **Module system** — cross-file imports, public/private visibility | Planned |
 | C8 | v0.1.0 | **End-to-end** — all examples compile and run, spec complete, polish | Planned |
 
@@ -190,7 +190,7 @@ C6 extends WASM compilation to all language constructs, working through the depe
 | Sub-phase | Scope | Closes | Unlocks |
 |-----------|-------|--------|---------|
 | ~~C6h~~ | ~~Closures — closure conversion, `call_indirect`~~ | ~~[#27](https://github.com/aallan/vera/issues/27)~~ | ~~Done (v0.0.18)~~ |
-| C6j | Effect handlers — handle/resume compilation | [#28](https://github.com/aallan/vera/issues/28) | effect_handler.vera |
+| ~~C6j~~ | ~~Effect handlers — handle/resume compilation~~ | ~~[#28](https://github.com/aallan/vera/issues/28)~~ | ~~Done (v0.0.19)~~ |
 
 **Collections, runtime, and documentation:**
 

examples/effect_handler.vera

@@ -1,12 +1,12 @@
--- Effect handlers — State and Exception patterns
+-- Effect handlers — State patterns
 
--- State effect: a counter
+-- A counter effect (user-defined effect)
 effect Counter {
   op get_count(Unit -> Int);
   op increment(Unit -> Unit);
 }
 
--- Use the counter effect
+-- Use the counter effect (not compilable — Counter is not a host effect)
 fn count_to_three(@Unit -> @Unit)
   requires(true)
   ensures(true)
@@ -17,7 +17,8 @@ fn count_to_three(@Unit -> @Unit)
   Counter.increment(())
 }
 
--- Handle the counter with a State handler
+-- Handle State<Int> to implement a counter
+-- The handle expression discharges the effect: run_counter is pure
 fn run_counter(@Unit -> @Int)
   requires(true)
   ensures(true)
@@ -35,23 +36,38 @@ fn run_counter(@Unit -> @Int)
   }
 }
 
--- Exception effect
-effect Exn<E> {
-  op throw(E -> Unit);
+-- Simpler test: read the initial state value
+fn test_state_init(@Unit -> @Int)
+  requires(true)
+  ensures(true)
+  effects(pure)
+{
+  handle[State<Int>](@Int = 42) {
+    get(@Unit) -> { resume(@Int.0) },
+    put(@Int) -> { resume(()) }
+  } in {
+    get(())
+  }
 }
 
-data Option<T> { None, Some(T) }
-
--- Handle exceptions by returning None on failure
-fn safe_parse(@String -> @Option<Int>)
+-- Test: put then get
+fn test_put_get(@Unit -> @Int)
   requires(true)
   ensures(true)
   effects(pure)
 {
-  handle[Exn<String>] {
-    throw(@String) -> { None }
+  handle[State<Int>](@Int = 0) {
+    get(@Unit) -> { resume(@Int.0) },
+    put(@Int) -> { resume(()) }
   } in {
-    let @Int = parse_int(@String.0);
-    Some(@Int.0)
+    put(99);
+    get(())
   }
 }
+
+-- Exception effect (demonstrates non-State handler, not compilable)
+effect Exn<E> {
+  op throw(E -> Unit);
+}
+
+data Option<T> { None, Some(T) }

pyproject.toml

@@ -1,6 +1,6 @@
 [project]
 name = "vera"
-version = "0.0.18"
+version = "0.0.19"
 description = "Vera: a programming language designed for LLMs, with full contracts, algebraic effects, and typed slot references"
 readme = "README.md"
 license = "MIT"

spec/11-compilation.md

@@ -390,14 +390,49 @@ call_indirect (type $closure_sig_N)    ;; indirect call
 
 `apply_fn` is a compiler built-in, not a user-defined function. The checker issues a warning about it being unresolved, but the code generator recognizes it and emits the appropriate `call_indirect` sequence.
 
-## 11.11 Limitations
+## 11.11 Effect Handler Compilation
+
+The `handle[Effect<T>]` expression compiles effect handlers to WASM. Currently, `State<T>` handlers are supported via the existing host import mechanism (Section 11.7.2).
+
+### 11.11.1 State Handler Compilation
+
+A `handle[State<T>](@T = init) { clauses } in { body }` expression compiles to:
+
+1. **Initialize state**: compile `init` expression, call `$vera.state_put_T`
+2. **Compile body**: with `get`/`put` mapped to `$vera.state_get_T`/`$vera.state_put_T` host imports
+3. **Return body result**: the handle expression evaluates to the body's final expression
+
+```wat
+;; handle[State<Int>](@Int = 42) { ... } in { put(get(()) + 1); get(()) }
+i64.const 42                ;; init expr
+call $vera.state_put_Int    ;; initialize state
+call $vera.state_get_Int    ;; get(())
+i64.const 1
+i64.add
+call $vera.state_put_Int    ;; put(get(()) + 1)
+call $vera.state_get_Int    ;; get(()) — body result
+```
+
+### 11.11.2 Handler Clauses as Specifications
+
+Handler clauses (e.g. `get(@Unit) -> { resume(@Int.0) }`) describe the handler's operational semantics but are not compiled to WASM. The host runtime already implements the correct `get`/`put` behavior. The `resume` calls in handler clauses serve as specifications validated by the type checker.
+
+### 11.11.3 Effect Discharge
+
+A `handle[State<T>]` expression discharges the `State<T>` effect. This means a function can be declared `effects(pure)` and still use `get`/`put` operations within a handler body. The compiler registers the State<T> host imports by scanning the function body for handle expressions, not just the function's declared effects.
+
+### 11.11.4 Unsupported Handlers
+
+Handler types other than `State<T>` (e.g. `Exn<E>`, custom effects) are not yet compilable. Functions containing unsupported handler types are skipped with a warning.
+
+## 11.12 Limitations
 
 The current compilation model has the following limitations, each tracked as a GitHub issue:
 
 | Limitation | Issue | Notes |
 |-----------|-------|-------|
-| No effect handler codegen | [#28](https://github.com/aallan/vera/issues/28) | Needs continuation-passing transform |
 | No Byte type codegen | [#30](https://github.com/aallan/vera/issues/30) | Needs linear memory byte operations |
 | No module-level code generation | — | Each file compiles independently |
 | No garbage collection | — | Bump allocator only; linear memory is not reclaimed |
 | String constants only | — | No dynamic string construction |
+| Only State\<T\> handlers | — | Exn\<E\> and custom effect handlers not yet compilable |