doc: fix Form-A ctor drift in cross-model-authoring spec — closes #28
The master spec at experiments/2026-05-12-cross-model-authoring/ master/spec.md taught two wrong Form-A keywords: - Term position: `(ctor TYPE-NAME CTOR-NAME ARG*)` — parser rejects this; the canonical keyword is `term-ctor`. The bare `(ctor ...)` is reserved for the inside of `(data ...)` definitions only. - Pattern position: `(ctor CTOR-NAME SUBPAT*)` — the canonical pattern keyword is `pat-ctor`. The JSON section was already correct (canonical schema tag IS "t": "ctor", per ast.rs:471). Only the AIL section had drifted. Empirically caught by the Qwen3-Coder naming-A/B run on 2026-05-21 (experiments/2026-05-21-naming-ab/runs/r1/), where every t4_count_zeros output produced `(ctor List Nil)` in term position and failed `ail check` 100 % across all three cohorts — a constant tax independent of the naming variable under test. Re-rendered rendered/ail.md from the patched master via xmodel-render. rendered/json.md unaffected. closes #28
This commit is contained in:
@@ -303,11 +303,14 @@ constructors have an empty argument list.
|
|||||||
Example: `(data List (ctor Nil) (ctor Cons Int (con List)))` is a
|
Example: `(data List (ctor Nil) (ctor Cons Int (con List)))` is a
|
||||||
monomorphic Int list with a Nil and a Cons constructor.
|
monomorphic Int list with a Nil and a Cons constructor.
|
||||||
|
|
||||||
Constructor invocation: `(ctor TYPE-NAME CTOR-NAME ARG*)`. The
|
Constructor invocation: `(term-ctor TYPE-NAME CTOR-NAME ARG*)`.
|
||||||
`TYPE-NAME` precedes the constructor name so the parser does not
|
The Form-A keyword is `term-ctor`, not `ctor` — the bare `(ctor
|
||||||
need a separate registry to resolve overlapping constructor names
|
...)` is reserved for the inside of `(data ...)` definitions and
|
||||||
across ADTs. Example: `(ctor List Cons 1 (ctor List Nil))` builds a
|
the parser rejects it in term position. `TYPE-NAME` precedes the
|
||||||
single-element list.
|
constructor name so the parser does not need a separate registry
|
||||||
|
to resolve overlapping constructor names across ADTs. Example:
|
||||||
|
`(term-ctor List Cons 1 (term-ctor List Nil))` builds a single-
|
||||||
|
element list.
|
||||||
{/form-only}
|
{/form-only}
|
||||||
|
|
||||||
{example: data_simple}
|
{example: data_simple}
|
||||||
@@ -359,7 +362,8 @@ Pattern shapes:
|
|||||||
- Variable: a bare identifier alone, e.g. `h`, binds the scrutinee.
|
- Variable: a bare identifier alone, e.g. `h`, binds the scrutinee.
|
||||||
- Literal: a literal value alone, e.g. `0`, `true`, `"abc"`,
|
- Literal: a literal value alone, e.g. `0`, `true`, `"abc"`,
|
||||||
`(unit)`, matches bit-equal scrutinees.
|
`(unit)`, matches bit-equal scrutinees.
|
||||||
- Constructor: `(ctor CTOR-NAME SUBPAT*)` — note no `type` slot
|
- Constructor: `(pat-ctor CTOR-NAME SUBPAT*)` — the Form-A
|
||||||
|
pattern keyword is `pat-ctor` (not `ctor`). No `type` slot
|
||||||
here, because the constructor name is resolved against the
|
here, because the constructor name is resolved against the
|
||||||
scrutinee's type.
|
scrutinee's type.
|
||||||
|
|
||||||
|
|||||||
@@ -252,11 +252,14 @@ constructors have an empty argument list.
|
|||||||
Example: `(data List (ctor Nil) (ctor Cons Int (con List)))` is a
|
Example: `(data List (ctor Nil) (ctor Cons Int (con List)))` is a
|
||||||
monomorphic Int list with a Nil and a Cons constructor.
|
monomorphic Int list with a Nil and a Cons constructor.
|
||||||
|
|
||||||
Constructor invocation: `(ctor TYPE-NAME CTOR-NAME ARG*)`. The
|
Constructor invocation: `(term-ctor TYPE-NAME CTOR-NAME ARG*)`.
|
||||||
`TYPE-NAME` precedes the constructor name so the parser does not
|
The Form-A keyword is `term-ctor`, not `ctor` — the bare `(ctor
|
||||||
need a separate registry to resolve overlapping constructor names
|
...)` is reserved for the inside of `(data ...)` definitions and
|
||||||
across ADTs. Example: `(ctor List Cons 1 (ctor List Nil))` builds a
|
the parser rejects it in term position. `TYPE-NAME` precedes the
|
||||||
single-element list.
|
constructor name so the parser does not need a separate registry
|
||||||
|
to resolve overlapping constructor names across ADTs. Example:
|
||||||
|
`(term-ctor List Cons 1 (term-ctor List Nil))` builds a single-
|
||||||
|
element list.
|
||||||
|
|
||||||
```ail
|
```ail
|
||||||
(module data_simple
|
(module data_simple
|
||||||
@@ -299,7 +302,8 @@ Pattern shapes:
|
|||||||
- Variable: a bare identifier alone, e.g. `h`, binds the scrutinee.
|
- Variable: a bare identifier alone, e.g. `h`, binds the scrutinee.
|
||||||
- Literal: a literal value alone, e.g. `0`, `true`, `"abc"`,
|
- Literal: a literal value alone, e.g. `0`, `true`, `"abc"`,
|
||||||
`(unit)`, matches bit-equal scrutinees.
|
`(unit)`, matches bit-equal scrutinees.
|
||||||
- Constructor: `(ctor CTOR-NAME SUBPAT*)` — note no `type` slot
|
- Constructor: `(pat-ctor CTOR-NAME SUBPAT*)` — the Form-A
|
||||||
|
pattern keyword is `pat-ctor` (not `ctor`). No `type` slot
|
||||||
here, because the constructor name is resolved against the
|
here, because the constructor name is resolved against the
|
||||||
scrutinee's type.
|
scrutinee's type.
|
||||||
|
|
||||||
@@ -349,13 +353,13 @@ arms or into code outside the `match`.
|
|||||||
|
|
||||||
Every function type carries an effect row — a set of effect labels
|
Every function type carries an effect row — a set of effect labels
|
||||||
that the function may raise. The two currently wired effects are
|
that the function may raise. The two currently wired effects are
|
||||||
`IO` (required to call effect operations like `io/print_str`) and
|
`IO` (required to call effect operations like `io/print_int`) and
|
||||||
`Diverge` (used for functions that may not terminate). An empty
|
`Diverge` (used for functions that may not terminate). An empty
|
||||||
effect row marks the function as pure.
|
effect row marks the function as pure.
|
||||||
|
|
||||||
Effect operations are reached through the `do` term, not through a
|
Effect operations are reached through the `do` term, not through a
|
||||||
regular function application. The `do` form names the operation
|
regular function application. The `do` form names the operation
|
||||||
(e.g. `io/print_str`) and lists the operation's arguments; the
|
(e.g. `io/print_int`) and lists the operation's arguments; the
|
||||||
typechecker resolves the operation against the prelude's effect-op
|
typechecker resolves the operation against the prelude's effect-op
|
||||||
table, checks the arguments, and accumulates the operation's
|
table, checks the arguments, and accumulates the operation's
|
||||||
effect label into the enclosing function's effect row.
|
effect label into the enclosing function's effect row.
|
||||||
@@ -374,9 +378,8 @@ in canonical output.
|
|||||||
|
|
||||||
Effect operation: `(do OP-NAME ARG*)` — the leading `do` head is
|
Effect operation: `(do OP-NAME ARG*)` — the leading `do` head is
|
||||||
the parser's signal that the next identifier is an effect op, not a
|
the parser's signal that the next identifier is an effect op, not a
|
||||||
function. Example: `(do io/print_str "hi\n")` prints the string
|
function. Example: `(do io/print_int 42)` prints the integer 42
|
||||||
`hi` followed by a newline and raises the `IO` effect. To print a
|
and raises the `IO` effect.
|
||||||
non-string value, first convert it: `(do io/print_str (app int_to_str 42))`.
|
|
||||||
|
|
||||||
Sequencing: `(seq LHS RHS)`. The value of `(seq X Y)` is `Y`'s
|
Sequencing: `(seq LHS RHS)`. The value of `(seq X Y)` is `Y`'s
|
||||||
value; `X`'s value is discarded. Chains of sequencing are written
|
value; `X`'s value is discarded. Chains of sequencing are written
|
||||||
@@ -386,10 +389,10 @@ value.
|
|||||||
```ail
|
```ail
|
||||||
(module fn_with_do_seq
|
(module fn_with_do_seq
|
||||||
(fn main
|
(fn main
|
||||||
(doc "Print two Ints in sequence. Exercises TermDo, TermSeq, the IO effect on a fn type, and int-to-str conversion via the prelude `int_to_str`. The trailing unit return is implicit in the last Do (op returns Unit).")
|
(doc "Print two Ints in sequence. Exercises TermDo, TermSeq, and the IO effect on a fn type. The trailing unit return is implicit in the last Do (op returns Unit).")
|
||||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||||
(params)
|
(params)
|
||||||
(body (seq (do io/print_str (app int_to_str 1)) (do io/print_str (app int_to_str 2))))))
|
(body (seq (do io/print_int 1) (do io/print_int 2)))))
|
||||||
```
|
```
|
||||||
|
|
||||||
## 9. Literals
|
## 9. Literals
|
||||||
@@ -548,14 +551,14 @@ Effect operations (reached through `do`, not `app`):
|
|||||||
|
|
||||||
| Op | Signature | Effect |
|
| Op | Signature | Effect |
|
||||||
|----|----------|-------|
|
|----|----------|-------|
|
||||||
|
| `io/print_int` | `(Int) -> Unit` | `IO` |
|
||||||
|
| `io/print_bool` | `(Bool) -> Unit` | `IO` |
|
||||||
| `io/print_str` | `(Str) -> Unit` | `IO` |
|
| `io/print_str` | `(Str) -> Unit` | `IO` |
|
||||||
|
| `io/print_float` | `(Float) -> Unit` | `IO` |
|
||||||
|
|
||||||
`io/print_str` is the only print operation, and it appends a
|
`int_to_str` is intentionally NOT in the prelude — it is type-
|
||||||
trailing newline (the runtime calls C `puts`). To print a non-string
|
installed in a future milestone but codegen-deferred pending the
|
||||||
value, convert it first via `int_to_str`, `float_to_str`, or
|
heap-Str ABI work. Do not call it.
|
||||||
`bool_to_str` — all three are in the prelude (see the prelude
|
|
||||||
table above). To print two values on consecutive lines, sequence
|
|
||||||
two `(do io/print_str ...)` calls with `seq`.
|
|
||||||
|
|
||||||
## 12. Content addressing
|
## 12. Content addressing
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user