Brummel
af35612c1d
Eliminates the Unit-typed chain default that 16c left in place.
Adds __unreachable__ : forall a. a — codegen lowers to LLVM
unreachable. The 16a/16c chain machinery now uses it as the
deepest fall-through, so exhaustive matches with non-Unit arms
no longer need a (case _ ...) workaround.
- check/builtins.rs: register __unreachable__ as Forall(a, a).
- codegen: Term::Var "__unreachable__" emits LLVM unreachable
and sets block_terminated; If/Match/fn-body gate downstream
work on that flag.
- desugar: chain default switched from Lit{Unit} to Var.
- examples/lit_pat: categorize_first's trailing _ arm removed.
Hash changes from c4faec3abc2ed388 to 644de0c0ec15fc17.
- examples/unreachable_demo: positive fixture using safe_div
with __unreachable__ in the impossible branch.
- e2e + desugar tests: 122 → 124 (+2).
Path-a from 16b.2 planning: real primitive over a desugar-time
exhaustiveness pre-check (which would need cross-module type
registry access from desugar).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
36 lines
1.3 KiB
Plaintext
36 lines
1.3 KiB
Plaintext
; Iter 16d — `__unreachable__` as an explicit user-callable primitive.
|
|
; Type: forall a. a (lowered to LLVM `unreachable`).
|
|
;
|
|
; This fixture exercises `__unreachable__` in a value position that is
|
|
; statically unreachable but still type-checks: the impossible branch
|
|
; of an if. `safe_div(a, b)` returns `a / b` when `b != 0` and panics
|
|
; via `__unreachable__` otherwise. The driver only ever calls it with
|
|
; non-zero divisors, so the panic branch is never executed.
|
|
;
|
|
; The point of the fixture is the type-system + codegen surface:
|
|
; `__unreachable__` unifies against `Int` (the fn's return type) at
|
|
; the typechecker, and codegen lowers it to `unreachable` followed by
|
|
; the rest of the if's join machinery, which is sound because the
|
|
; surrounding if's `block_terminated` flag is honoured.
|
|
;
|
|
; Expected stdout (one per line): 4, 5.
|
|
|
|
(module unreachable_demo
|
|
|
|
(fn safe_div
|
|
(doc "a/b for b != 0; otherwise panic via __unreachable__.")
|
|
(type (fn-type (params (con Int) (con Int)) (ret (con Int))))
|
|
(params a b)
|
|
(body
|
|
(if (app == b 0)
|
|
__unreachable__
|
|
(app / a b))))
|
|
|
|
(fn main
|
|
(doc "Drive safe_div with non-zero divisors. Expected: 4, 5.")
|
|
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
|
(params)
|
|
(body
|
|
(seq (do io/print_int (app safe_div 8 2))
|
|
(do io/print_int (app safe_div 15 3))))))
|