Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

iter form-a-scalar-param-mode-carveout: scalar-param mode carve-out (docs-honesty tidy)

Browse Source 
Resolves the M1-fieldtest [friction] + [spec_gap]#1 shared root:
form_a.md stated an unconditional 'every (fn ...) param needs an
(own/borrow) mode' rule in 4 places, contradicting shipped checker
behaviour (scalars take and require bare (con Int); a mode on a
scalar trips body-pointing use-after-consume/consume-while-borrowed).
All 4 sites rewritten symmetric to the existing return-type carve-out;
DESIGN.md gains the bare-scalar export-param rule + a corpus-grounded
Form-A snippet; RED-first anti-regrowth pin via FORM_A_SPEC + norm().
Zero language/checker/codegen change. Plan 4c266a6.
This commit is contained in:
Brummel
2026-05-18 15:51:34 +02:00
parent 4c266a64b4
commit 7d7f04e1a4
6 changed files with 169 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-core/specs/form_a.md
+29 -11
View File
@@ -94,8 +94,10 @@ The `because` MUST be a non-empty justification — empty / whitespace-
only `because` is itself an error (`empty-suppress-reason`).
`type` is a `(fn-type ...)` (possibly wrapped in `(forall ...)` for
polymorphic defs). All parameters of a `(fn ...)` MUST carry a mode
annotation — see *Modes* below.
polymorphic defs). A *heap-shaped* parameter or return of a
`(fn ...)` MUST carry a mode annotation; a scalar (non-heap-shaped:
`(con Int)`, `(con Bool)`, `(con Unit)`, `(con Str)`) takes **no**
mode and is written bare — see *Modes* below.
`params` is a list of bare names that bind the parameters in `body`.
The list length must match the number of params in `type`.
@@ -227,7 +229,7 @@ TYVAR-NAME ; type variable (e.g. `a`, `T`)
annotation:
```
TYPE ; implicit mode (DO NOT USE in new (fn ...) defs)
TYPE ; no mode — REQUIRED for scalars (Int/Bool/Unit/Str), rejected for heap-shaped
(own TYPE) ; caller transfers ownership; callee consumes
(borrow TYPE) ; caller retains ownership; callee must not consume
```
@@ -344,12 +346,20 @@ The parser will accept syntactically valid Form-A that violates these;
the typechecker will not. Producing Form-A that obeys them yields
checked code on the first try.
1. **Mode annotations on every `(fn ...)` parameter.** Every type in
the `(params ...)` clause of a `(fn ...)` definition's
`(fn-type ...)` MUST be wrapped in `(own T)` or `(borrow T)`. The
return type MUST also carry a mode whenever the type is heap-shaped
1. **Mode annotations on every heap-shaped `(fn ...)` parameter.** A
parameter type in the `(params ...)` clause of a `(fn ...)`
definition's `(fn-type ...)`, and the return type, MUST be wrapped
in `(own T)` or `(borrow T)` whenever the type is heap-shaped
(i.e. anything other than `(con Int)`, `(con Bool)`, `(con Unit)`,
`(con Str)`). Implicit mode on a `(fn ...)` def is rejected.
`(con Str)`). A scalar (non-heap-shaped) parameter or return takes
**no** mode: write it bare, e.g. `(con Int)`. Scalars are
primitive value types, not linear resources; putting a mode on a
scalar makes the checker hold the primitive to linear discipline
(single use under `own`, no use while a `borrow` is live), so an
ordinary scalar reused in the body (`sample * sample`) trips a
body-pointing `use-after-consume` / `consume-while-borrowed`
rather than a mode error. Implicit (omitted) mode on a
*heap-shaped* `(fn ...)` parameter or return is rejected.
2. **Constructors via `term-ctor`.** `Cons(1, Nil)` becomes
`(term-ctor List Cons 1 (term-ctor List Nil))`, never
`(app Cons 1 (app Nil))`.
@@ -378,9 +388,17 @@ significantly.
it is interpreted as a type variable. So `(fn-type (params Int) ...)`
parses as "function with one type-variable parameter named Int",
which is almost certainly not what was meant.
- **Forgetting mode annotations.** `(fn-type (params (con List)) ...)`
is accepted by the parser but rejected by the checker. Wrap every
`(fn ...)` parameter in `(own ...)` or `(borrow ...)`.
- **Forgetting mode annotations on a heap-shaped parameter.**
`(fn-type (params (con List)) ...)` is accepted by the parser but
rejected by the checker. Wrap every *heap-shaped* `(fn ...)`
parameter in `(own ...)` or `(borrow ...)`.
- **Putting a mode on a scalar parameter.** The inverse trap:
`(fn-type (params (own (con Int))) ...)` is wrong — scalars
(`Int`/`Bool`/`Unit`/`Str`) take no mode, write them bare
`(con Int)`. A mode on a scalar makes the checker treat the
primitive as a linear resource, so an ordinary reuse trips a
body-pointing `use-after-consume` / `consume-while-borrowed`
instead of pointing at the signature.
- **Using `app` for constructors.** Constructors are NOT first-class
functions. `(app Cons 1 Nil)` is interpreted as "apply variable
`Cons` to ...", which then fails because `Cons` is not a fn.
crates/ailang-core/tests/docs_honesty_pin.rs
+37
View File
@@ -9,6 +9,7 @@
//! docs' hard line-wrap. Companion to `effect_doc_honesty_pin.rs` and
//! to Sweep 5 of `bench/architect_sweeps.sh`.
use ailang_core::FORM_A_SPEC;
use std::fs;
fn read(rel: &str) -> String {
@@ -98,3 +99,39 @@ fn prose_roundtrip_md_has_no_wunschdenken() {
assert!(p.contains("the lowest-common-denominator cycle and always works with any client"),
"PROSE_ROUNDTRIP.md must close present-tense on the static-prompt path");
}
#[test]
fn form_a_scalar_param_carveout_present_and_old_rule_absent() {
// form_a.md is read via the canonical include_str! const, not a
// re-derived path: single source of truth, compile-checked, no
// stale-path bug. norm() collapses the docs' hard line-wrap so
// every asserted substring below is the single-spaced form
// (planner Step-5 item 6: line-wrap is structurally discharged,
// the substrings need not be contiguous in the .md source).
let f = norm(FORM_A_SPEC);
let d = norm(&read("docs/DESIGN.md"));
// --- ABSENT: the four old unconditional phrasings must be gone ---
assert!(!f.contains("Mode annotations on every `(fn ...)` parameter."),
"form_a.md item 1 must no longer head with the unconditional 'every (fn ...) parameter' rule (site 3)");
assert!(!f.contains("All parameters of a `(fn ...)` MUST carry a mode annotation"),
"form_a.md ### Function prose must no longer state the unconditional all-params rule (site 1)");
assert!(!f.contains("(DO NOT USE in new (fn ...) defs)"),
"form_a.md grammar block must no longer blanket-forbid the bare (implicit-mode) form (site 2)");
assert!(!f.contains("Wrap every `(fn ...)` parameter in `(own ...)` or `(borrow ...)`."),
"form_a.md Pitfalls bullet must no longer state the unconditional 'wrap every parameter' imperative (site 4)");
// --- PRESENT: the scalar-parameter carve-out, the four sites ---
assert!(f.contains("A scalar (non-heap-shaped) parameter or return takes **no** mode: write it bare, e.g. `(con Int)`."),
"form_a.md item 1 must state the scalar-parameter carve-out symmetrically with the return-type carve-out (site 3)");
assert!(f.contains("a scalar (non-heap-shaped: `(con Int)`, `(con Bool)`, `(con Unit)`, `(con Str)`) takes **no** mode and is written bare"),
"form_a.md ### Function prose must carry the scalar carve-out (site 1)");
assert!(f.contains("; no mode — REQUIRED for scalars (Int/Bool/Unit/Str), rejected for heap-shaped"),
"form_a.md grammar block comment must state the bare form is required for scalars (site 2)");
assert!(f.contains("Putting a mode on a scalar parameter."),
"form_a.md Pitfalls must carry the inverse pitfall — over-wrapping a scalar (site 4)");
// --- PRESENT: the DESIGN.md §\"Embedding ABI (M1)\" mirror ---
assert!(d.contains("Export parameters are written **bare**: a scalar type carries no `own`/`borrow` mode"),
"DESIGN.md §Embedding ABI (M1) must mirror the canonical bare-scalar export-param rule");
}