176821c2e7
The 3020-line docs/DESIGN.md is replaced by the design/ ledger:
design/INDEX.md (sole addressable spine, typed Contracts+Models tables,
polymorphic links — prose file OR authoritative source //!), 14
design/contracts/*.md test-linked invariants + 3 source-link-only
contracts (mangling/env-construction/qualified-xref, no prose file —
code is SoT), 5 design/models/*.md whitepapers, and
docs/journals/2026-05-19-design-decision-records.md (the
relitigation-guard archive — every why/rejected/does-not-do/rollback/
empirical ### moved out at ###-granularity). Clean cut: git rm
docs/DESIGN.md, no stub.
RED-first crates/ailang-core/tests/design_index_pin.rs — the 4-clause
anti-regrowth spine (DESIGN.md-gone / every-INDEX-link-resolves /
every-contract-names-a-resolvable-ratifier /
contracts-carry-no-decision-record-prose) — demonstrably RED before,
GREEN after. Build-atomic by task ordering: design_schema_drift.rs's
include_str! (the only compile-time consumer) retargeted to
design/contracts/data-model.md BEFORE the deletion; its
## Data model/## Pipeline slicer dropped (a simplification the split
enables). 2 NoInstance diagnostics + 2 lockstep E2Es retargeted to
design/contracts/{float-semantics,typeclasses}.md. ~12 agent reading
lists + 5 SKILL bodies + CLAUDE.md + skills/README.md + ~25
code/C/.ail/spec comment xrefs retargeted; OQ7 dangling 'Iter 13b'
cite deleted (no forward target — a pointer would be fiction).
honesty-rule.md rewritten so the rule names the new home
(rationale->journals), resolving the recon-found internal
contradiction; the two docs_honesty_pin.rs:70,72 pinned phrases kept
verbatim+contiguous.
Boss-verified independently: cargo test --workspace 646 passed /
0 failed; design_index_pin 4/4; acceptance grep CLEAN of live
DESIGN.md refs (residuals = only the spec-mandated clause-4
deletion-enforcer). 2 DONE_WITH_CONCERNS routed to the mandatory
milestone-close audit: (a) str-abi.md:23 '(iter str-concat,
2026-05-13)' provenance stamp trips advisory architect_sweeps Sweep-1
— Boss-confirmed byte-identical to DESIGN.md@deeffb1:2062-2065, a
faithfully-migrated PRE-EXISTING anchor (regexes verbatim, only path
retargeted), NOT split-introduced — RATIFY-or-tidy at audit; (b) a
now stale-direction intra-prose 'see Str ABI below' cross-ref in
float-semantics.md — audit-adjudication candidate. Plan defect noted:
Task 9 Step 4's verbatim acceptance grep used a ^./ anchor not
matching the system's grep -rIn output; substance re-verified CLEAN.
Spec grounding-check PASS x2. Journals INDEX + decision-records
pointer appended (Boss-only).
187 lines
10 KiB
Markdown
187 lines
10 KiB
Markdown
# What is not (yet) supported
|
|
|
|
## What is not (yet) supported
|
|
|
|
Snapshot of the current boundary. Items move out of this list
|
|
as iterations land; the JOURNAL records when.
|
|
|
|
- No effect handlers — only the built-in `IO` op (`io/print_str`).
|
|
`Diverge` is a reserved effect name with no op and no codegen.
|
|
- No refinements / SMT escalation.
|
|
- No HM inference inside bodies. Top-level def types are explicit;
|
|
polymorphism is opt-in via `Type::Forall { vars, body }`. Inside
|
|
a body, lambdas check monomorphically against their declared type.
|
|
- Polymorphic fns must be **directly called** at the use site.
|
|
Passing a polymorphic fn as a value (`let f = id in f(42)`) is
|
|
not yet supported — it would need one closure-pair global per
|
|
instantiation, deferred.
|
|
- No higher-rank polymorphism. Passing a polymorphic fn to another
|
|
polymorphic fn (`apply(id, 42)`) is not supported.
|
|
- No recursive `let` for non-fn values. Plain `let x = … in …` only
|
|
sees `x` inside the body, not inside its own RHS — recursive value
|
|
bindings would break Decision 10's acyclicity invariant. Recursive
|
|
*fn* bindings are supported via `Term::LetRec` (`{ "t": "letrec",
|
|
... }`); the desugar pass lifts most occurrences to a synthetic
|
|
top-level fn, with `lift_letrecs` finishing the residue after
|
|
typecheck.
|
|
- No visibility rules in imports. Every top-level def of an imported module
|
|
is reachable; there is no `pub` / `priv`.
|
|
|
|
What **is** supported (and used as the smoke test for the pipeline):
|
|
|
|
- Int, Bool, Unit, **Str**, **Float** as primitive types.
|
|
- `if`, `let`, function calls, recursion.
|
|
- Effects on function signatures, with `do op(args)` for direct effect
|
|
ops (`io/print_str`). The per-type print ops
|
|
`io/print_int`, `io/print_bool`, `io/print_float` were retired in
|
|
iter rpe.1; the polymorphic `print` (§"Polymorphic print") is the
|
|
canonical output path for non-Str values.
|
|
- **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`) of type
|
|
`forall a. (a, a) -> a` (codegen-restricted to `{Int, Float}`);
|
|
`%` of type `(Int, Int) -> Int` (Int-only — `fmod` semantics for
|
|
Float deferred); ordering operators and `!=` (`!=`, `<`, `<=`,
|
|
`>`, `>=`) of type `forall a. (a, a) -> Bool` (codegen-restricted
|
|
to `{Int, Float}`); polymorphic `neg : forall a. (a) -> a`
|
|
(codegen-restricted to `{Int, Float}`; Float arm uses LLVM
|
|
`fneg double` for correct `-0.0` handling); logical
|
|
`not : (Bool) -> Bool`; conversions
|
|
`int_to_float : (Int) -> Float`,
|
|
`float_to_int_truncate : (Float) -> Int` (saturating, NaN → 0),
|
|
`float_to_str : (Float) -> Str`,
|
|
`int_to_str : (Int) -> Str` (both allocate a heap-Str slab at
|
|
call time and return it with `ret_mode: Own`; see "Str ABI" for
|
|
the dual heap-/static-Str realisation); inspection
|
|
`is_nan : (Float) -> Bool` (LLVM
|
|
`fcmp uno`); Float bit-pattern constants `nan : Float`,
|
|
`inf : Float`, `neg_inf : Float` (resolved as bare values, lower
|
|
to direct hex-float `double` SSA constants at use site); the IO
|
|
effect op `io/print_str`; **`==` : forall a.
|
|
(a, a) -> Bool**; and **`__unreachable__ : forall a. a`**.
|
|
- **`==` is polymorphic.** The typechecker accepts
|
|
`==` at any type whose two sides agree (the rigid `a` of the
|
|
`Forall` is unified by HM at the use site). Codegen
|
|
monomorphises and dispatches on the resolved AIL arg type:
|
|
`Int` → `icmp eq i64`; `Bool` → `icmp eq i1`;
|
|
`Str` → `call @strcmp(ptr, ptr)` then `icmp eq i32 0`
|
|
(`@strcmp` is declared in the LLVM IR header alongside
|
|
`@printf` / `@GC_malloc`); `Unit` → constant `i1 true`
|
|
(Unit has a single inhabitant; both sides are still
|
|
evaluated for any side effects); `Float` → `fcmp oeq double`.
|
|
ADT and `Fn` arg types are rejected at codegen with a
|
|
`CodegenError::Internal` mentioning `==` and the offending
|
|
type — neither has a canonical structural-equality scheme
|
|
yet, and the language deliberately does not silently elide
|
|
the check. **`!=` for Float uses `fcmp UNE double` (NOT
|
|
`one`)** — `one` is "ordered and not equal" and would return
|
|
false for `nan != nan`, violating IEEE-`!=`.
|
|
- **`__unreachable__`** is a polymorphic bottom value: a use of
|
|
`__unreachable__` typechecks against any expected type at
|
|
the use site and codegens to the LLVM `unreachable`
|
|
instruction (UB if ever executed). It is the chain
|
|
machinery's deepest fall-through for matches that the
|
|
typechecker proved exhaustive, and it is available to user
|
|
code as an explicit panic primitive
|
|
(`(if cond __unreachable__ ...)` for assertions or
|
|
impossible branches). Reference site is
|
|
`Term::Var { name = "__unreachable__" }` / form-A bare
|
|
`__unreachable__`.
|
|
- **ADTs + pattern matching.** Sub-patterns of a Ctor pattern may be `Var`, `Wild`,
|
|
another `Ctor`, or a literal. The desugar pass flattens
|
|
nested Ctor patterns into a chain of let + match and rewrites every
|
|
`Pattern::Lit` (top-level or sub-) to a `Term::If` on `==` before
|
|
typecheck/codegen — see `ailang-core::desugar` and Pipeline above.
|
|
- Literal patterns at top level and inside Ctor sub-patterns (via desugar).
|
|
`(pat-lit 0)` and `(pat-ctor Cons (pat-lit 0) _)` both
|
|
parse and lower; the rewrite is to `Term::If { cond = (== sv lit) }`,
|
|
so any literal kind whose `==` is supported is authorable. With `==`
|
|
polymorphic over `Int`/`Bool`/`Str`/`Unit`, that
|
|
covers every lit kind the AST ships — including `(pat-lit "hi")`
|
|
over a `Str` scrutinee, exercised by `examples/eq_demo.ail.json`.
|
|
- **Imports + qualified cross-module references** via dotted names.
|
|
Extends to **types and constructors**: a foreign
|
|
module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as
|
|
`(term-ctor std_pair.Pair MkPair x y)` and `(pat-ctor MkPair x y)`
|
|
inside that scrutinee. Std-library demos (`examples/std_*_demo.ail.json`)
|
|
exercise this end-to-end.
|
|
- **AI-authoring text surface, form (A)** (Decision 6). The `ailang-surface` crate parses `.ail` form-A
|
|
text into a canonical `ailang-core::ast::Module` and prints any module
|
|
back as form-A text. `ail render` and `ail describe` use it as the
|
|
sole text projection; `ail parse` is the inverse direction. Round-trip
|
|
identity (text → AST → JSON → AST → text) is gated by
|
|
`ailang-surface/tests/round_trip.rs` over every shipped fixture.
|
|
- **Memory management via Boehm conservative GC** (Decision 9),
|
|
with **per-fn arena via stack `alloca` for non-escaping allocations**
|
|
layered on top. Every ADT box, lambda env, and closure
|
|
pair allocates either via `@GC_malloc` (escaping; Boehm-managed) or
|
|
via LLVM `alloca` (non-escaping; freed at fn return). The decision
|
|
is made by an escape-analysis pre-pass over the fn body — see
|
|
Decision 9's "Per-fn arena via stack `alloca`" subsection.
|
|
Boehm-only soak tests are unchanged: `examples/gc_stress.ail.json`
|
|
and `examples/std_list_stress.ail.json` still allocate via
|
|
`@GC_malloc` because their boxes flow into other fns and escape.
|
|
The per-fn-arena path is exercised end-to-end by
|
|
`examples/escape_local_demo.ail.json`.
|
|
- **First-class function references.** A top-level fn name (or
|
|
qualified `prefix.def`) used as a `Term::Var` is a fn-value.
|
|
- **Anonymous lambdas with capture.** `Term::Lam` constructs a
|
|
closure that captures any free variables of its body from the
|
|
enclosing scope. All fn-values share a single ABI: a `ptr` to a
|
|
closure pair `{ thunk_ptr, env_ptr }`. Top-level fns get an auto-
|
|
generated adapter and a static closure pair (env = null) so they
|
|
remain passable as values without heap overhead.
|
|
- **Polymorphism via `Type::Forall`** at top-level def types.
|
|
Use sites instantiate fresh metavars; unification pins them against
|
|
the concrete types of the call args. Codegen monomorphises on
|
|
demand: each unique instantiation emits a specialised LLVM fn
|
|
mangled `@ail_<m>_<def>__<descriptor>` (e.g. `id__I` for `id` at
|
|
`Int`, `apply__I_I` for `apply` at `(Int, Int)`).
|
|
- **Parameterised ADTs.** `TypeDef.vars: Vec<String>`
|
|
declares type parameters; `Type::Con.args: Vec<Type>` carries the
|
|
type arguments at use sites. Both fields default to empty and are
|
|
skipped during serialization, so canonical-JSON hashes of every
|
|
existing definition stay bit-identical (regression test in
|
|
`crates/ailang-core/src/hash.rs`). Ctor and match codegen stay
|
|
inline at every use site — there is no specialised ADT symbol —
|
|
but LLVM field types are derived per use site by substituting
|
|
through `cdef.ail_fields`. The substitution is read off the call's
|
|
arg types (ctor) or the scrutinee's `Type::Con.args` (match). An
|
|
unresolved `Type::Var` reaching `llvm_type` is a hard error
|
|
rather than a silent fallback to `ptr`.
|
|
Pipeline regression smoke tests:
|
|
|
|
- `examples/sum.ail.json` → prints 55 (recursion, arithmetic).
|
|
- `examples/list.ail.json` → prints 42 (ADTs + match).
|
|
- `examples/hof.ail.json` → prints 42 (first-class fn-refs, indirect call).
|
|
- `examples/closure.ail.json` → prints 42 (lambda capturing a let-bound var).
|
|
- `examples/list_map.ail.json` → prints 2/4/6 (ADTs + closure + recursive
|
|
HOF + IO; the dogfood smoke test).
|
|
- `examples/sort.ail.json` → prints sorted [3,1,4,1,5,9,2,6,5,3,5]
|
|
one-per-line (insertion sort over an 11-element list).
|
|
- `examples/poly_id.ail.json` → prints 42 then "true" (polymorphic
|
|
identity at `Int` and `Bool`; two specialised fns emitted).
|
|
- `examples/poly_apply.ail.json` → prints 42 (polymorphic `apply`
|
|
with a fn-typed parameter; `apply(succ, 41)`).
|
|
- `examples/box.ail.json` → prints 42 (parameterised ADT round-
|
|
trip: `MkBox(42)` constructed, then projected by a polymorphic
|
|
`unbox : forall a. (Box<a>) -> a` and printed).
|
|
- `examples/maybe_int.ail.json` → prints 7 then 99 (pattern match
|
|
over `Maybe<Int>`: `or_else(Some(7), 99)` then
|
|
`or_else(None, 99)`).
|
|
- `examples/std_list_demo.ail.json` → exercises
|
|
`std_list`'s combinators (length, sum, reverse, take/drop-style
|
|
uses) end-to-end against `std_list`'s `List<a>`.
|
|
- `examples/std_maybe_demo.ail.json` → exercises `std_maybe`
|
|
combinators over `Maybe<Int>`, including `from_maybe` and `map`.
|
|
- `examples/std_either_demo.ail.json` → first program with
|
|
three distinct type variables in a single fn (the `either`
|
|
eliminator), monomorphised six different ways in the IR.
|
|
- `examples/std_pair_demo.ail.json` → drives every
|
|
`std_pair` combinator (fst, snd, swap, map_first, map_second);
|
|
expected output 7, 9, 9, 7, 8, 18.
|
|
- `examples/nested_pat.ail.json` → first program to use a
|
|
nested `(pat-ctor Cons a (pat-ctor Cons b _))`; the desugar pass
|
|
flattens it into a chain that the existing flat-match codegen
|
|
consumes. Prints 30 for a 3-element input list.
|
|
|
|
Ratified by: `crates/ailang-core/tests/effect_doc_honesty_pin.rs`.
|