ail: embed Form-A spec in merge-prose prompt (iter 20f)
Closes a design hole shipped in 20d: the merge-prose prompt instructed
the LLM to emit JSON-AST and gave a 12-line schema-essentials reminder.
JSON-AST is the canonical hashable artefact, not a writing surface; the
reminder was not a language spec. Foreign LLMs had no realistic shot.
20f makes two coupled changes:
1) The LLM now emits Form-A (the canonical authoring surface fixed by
Decision 6). merge-prose loads the original via ailang_core::load_module
and re-renders via ailang_surface::print before embedding (round-trip
is a gating contract on the surface crate, so this is lossless). The
user runs `ail parse foo.new.ailx` to recover JSON, then `ail check`.
2) crates/ailang-core/specs/form_a.md is the complete LLM-targeted
Form-A specification — grammar, every term/pattern/type/def keyword,
schema invariants, pitfall catalogue, four few-shot modules from
examples/*.ailx. Exported as ailang_core::FORM_A_SPEC via include_str!
and embedded verbatim in every merge-prose prompt.
Drift detection in crates/ailang-core/tests/spec_drift.rs: every variant
of Term, Pattern, Type, Def, Literal is reached via exhaustive `match`.
The arms are not the assertion — adding a new variant without updating
the match is a compile error before the test runs. Once matched, an
anchor string is asserted to appear in FORM_A_SPEC. 8 tests, all green.
The hand-written + mechanical-drift-test combo addresses the user's
"distance to code is too big" concern about a docs-only spec. Generator
overkill rejected: structural drift is mechanically caught, but prose
explanation, schema-invariant catalogue, pitfall list, and few-shot
corpus cannot be emitted from AST shape alone.
Tests:
- ailang-core: +8 spec_drift tests; existing 12 unchanged
- ail unit (3): rewritten in lockstep — assert (own T)/(effects IO)
landmarks, FORM-A SPECIFICATION header, FORM_A_SPEC body verbatim
- ail e2e merge_prose_prints_framed_prompt: rewritten — assert
`(module foo` + `FORM-A SPECIFICATION` instead of `ailang/v0`
- Workspace: all green
Richer integration paths (LLM tool-use, MCP server, LSP) were named
in the design discussion and deferred per "kiss". All three layer
additively on the static-prompt path; static prompt remains the
lowest-common-denominator fallback.
This commit is contained in:
+103
-103
@@ -229,89 +229,89 @@ enum Cmd {
|
|||||||
/// Composes the prose-round-trip prompt described in
|
/// Composes the prose-round-trip prompt described in
|
||||||
/// `docs/PROSE_ROUNDTRIP.md`.
|
/// `docs/PROSE_ROUNDTRIP.md`.
|
||||||
///
|
///
|
||||||
/// The two payloads — the original `.ail.json` and the edited prose —
|
/// The three payloads — the AILang Form-A specification, the original
|
||||||
/// are inserted verbatim between heredoc-style markers; the rest of
|
/// module rendered as Form-A, and the edited prose — are inserted
|
||||||
/// the returned string is the role-statement, contract, output spec,
|
/// verbatim between heredoc-style markers. The rest of the returned
|
||||||
/// and schema-essentials reminder that frame the LLM's task.
|
/// string is the role-statement, contract, and output spec that frame
|
||||||
|
/// the LLM's task.
|
||||||
|
///
|
||||||
|
/// Iter 20f rewrote this function: the prompt now embeds
|
||||||
|
/// [`ailang_core::FORM_A_SPEC`] (the language reference an LLM needs
|
||||||
|
/// to generate AILang from scratch) and the original module as Form-A
|
||||||
|
/// (the canonical authoring surface, Decision 6) instead of JSON-AST.
|
||||||
|
/// JSON-AST stays the canonical hashable artefact, but no human or
|
||||||
|
/// LLM should write it directly — `ail parse` converts the LLM's
|
||||||
|
/// Form-A output to JSON.
|
||||||
///
|
///
|
||||||
/// Pure: same inputs always yield the same bytes. The CLI wrapper
|
/// Pure: same inputs always yield the same bytes. The CLI wrapper
|
||||||
/// (`Cmd::MergeProse`) is just a file-reader + `print!`.
|
/// (`Cmd::MergeProse`) is just file-reading + Form-A render + `print!`.
|
||||||
fn compose_merge_prose_prompt(orig_ail_json: &str, edited_prose: &str) -> String {
|
fn compose_merge_prose_prompt(original_form_a: &str, edited_prose: &str) -> String {
|
||||||
// Keep this template in lockstep with `docs/PROSE_ROUNDTRIP.md` —
|
// Built with String::push_str rather than format!() because
|
||||||
// the doc reproduces the literal text so a human can assemble the
|
// `FORM_A_SPEC` contains literal `{` and `}` from embedded JSON
|
||||||
// same prompt by hand.
|
// examples, which would break format!'s placeholder escaping.
|
||||||
format!(
|
let mut out = String::new();
|
||||||
|
out.push_str(
|
||||||
"You are integrating prose edits back into an AILang module.
|
"You are integrating prose edits back into an AILang module.
|
||||||
|
|
||||||
ROLE
|
ROLE
|
||||||
Your job is to produce an updated AILang JSON-AST (.ail.json) that
|
Your job is to produce an updated AILang module in Form-A (an .ailx
|
||||||
reflects the human's prose edits while preserving the load-bearing
|
file) that reflects the human's prose edits while preserving the
|
||||||
semantic detail from the original .ail.json.
|
load-bearing semantic detail from the original module.
|
||||||
|
|
||||||
CONTRACT
|
CONTRACT
|
||||||
The prose is the source of intent: the human edited it to express
|
The prose is the source of intent: the human edited it to express
|
||||||
what the program should now do. The original .ail.json carries
|
what the program should now do. The original Form-A carries
|
||||||
load-bearing detail that the prose surface elides — preserve those
|
load-bearing detail that the prose surface elides — preserve those
|
||||||
details unless the prose explicitly contradicts them. Specifically:
|
details unless the prose explicitly contradicts them. Specifically:
|
||||||
|
|
||||||
- Mode annotations on fn parameters (`own T`, `borrow T`).
|
- Mode annotations on fn parameters (`(own T)`, `(borrow T)`).
|
||||||
These are hard contracts (memory model). The prose shows them,
|
These are hard contracts (memory model). The prose shows them
|
||||||
but if the prose is ambiguous, default to the original.
|
as `own T` / `borrow T`; the Form-A wraps them. If the prose is
|
||||||
- Effect annotations on return types (`with IO`, `with Diverge`).
|
ambiguous, default to the original.
|
||||||
Prose shows these too, but again: if uncertain, keep what the
|
- Effect annotations on return types (`(effects IO)`,
|
||||||
original had.
|
`(effects Diverge)`). Prose shows these as `with IO` etc.; if
|
||||||
- `tail` flags on calls. The prose prints `tail f(x)`; if the
|
uncertain, keep what the original had.
|
||||||
edit moved a call, decide whether the new position is still in
|
- `tail` flags on calls. The prose prints `tail f(x)`; the Form-A
|
||||||
tail position and flag accordingly.
|
keyword is `(tail-app f x)`. If the edit moved a call, decide
|
||||||
- Doc strings (`///` lines).
|
whether the new position is still in tail position.
|
||||||
- Type annotations on signatures and lambdas.
|
- Doc strings (`(doc \"...\")` clauses; prose shows them as `///`).
|
||||||
|
- `(suppress (code ...) (because ...))` clauses (prose shows them
|
||||||
|
as `// @suppress code: reason`). The `because` MUST be non-empty.
|
||||||
- Constructor names and arities (the prose `Cons(h, t)` must
|
- Constructor names and arities (the prose `Cons(h, t)` must
|
||||||
round-trip to a `Term::Ctor` with the right `type` field).
|
round-trip to `(term-ctor TYPE Cons h t)` with the right TYPE).
|
||||||
|
|
||||||
OUTPUT
|
OUTPUT
|
||||||
Output ONLY the new .ail.json bytes. No commentary, no markdown
|
Output ONLY the new Form-A bytes. No commentary, no markdown fences,
|
||||||
fences, no preamble or postscript. The output must be valid JSON
|
no preamble or postscript. The output must be parseable by
|
||||||
parsable by `ail parse` (i.e. by `serde_json` against the
|
`ail parse` (it will be piped to that command immediately). The first
|
||||||
`ailang/v0` schema). The first byte should be `{{` and the last
|
non-whitespace byte should be `(` (the opening of `(module ...)`)
|
||||||
non-whitespace byte should be `}}`.
|
and the last non-whitespace byte should be `)`.
|
||||||
|
|
||||||
SCHEMA ESSENTIALS
|
|
||||||
A full reference lives in docs/DESIGN.md (\"Data model (MVP)\"). The
|
|
||||||
shape is:
|
|
||||||
|
|
||||||
- Module: {{ \"schema\": \"ailang/v0\", \"name\": ..., \"imports\": [...],
|
|
||||||
\"defs\": [...] }}
|
|
||||||
- Defs are tagged via `kind` (\"fn\" | \"type\" | \"const\").
|
|
||||||
- Types are tagged via `k` (\"con\" | \"fn\" | \"var\" | \"forall\").
|
|
||||||
- Terms are tagged via `t` (\"lit\" | \"var\" | \"app\" | \"let\" | \"if\"
|
|
||||||
| \"do\" | \"ctor\" | \"match\" | \"lam\" | \"seq\").
|
|
||||||
- Patterns are tagged via `p` (\"var\" | \"lit\" | \"ctor\" | \"wild\").
|
|
||||||
- On `fn-type`: `param_modes` (one of \"own\"/\"borrow\" per
|
|
||||||
parameter) and `effects` are mandatory. `ret_mode` is mandatory
|
|
||||||
when the return type carries a mode.
|
|
||||||
- Constructor application uses `Term::Ctor` (`\"t\": \"ctor\"`,
|
|
||||||
fields `type` + `ctor` + `args`), NOT `Term::App`. The prose
|
|
||||||
surface elides the `type` tag (`Cons(h, t)` instead of
|
|
||||||
`(term-ctor IntList Cons h t)`) — re-introduce it.
|
|
||||||
- Base type names that appear bare in prose (`Int`, `Bool`,
|
|
||||||
`Unit`, user types like `IntList`) must be wrapped as
|
|
||||||
`{{\"k\": \"con\", \"name\": \"Int\"}}` etc. in the JSON.
|
|
||||||
|
|
||||||
ORIGINAL .ail.json
|
|
||||||
<<<ORIGINAL_AIL_JSON
|
|
||||||
{orig}
|
|
||||||
ORIGINAL_AIL_JSON
|
|
||||||
|
|
||||||
EDITED PROSE
|
|
||||||
<<<EDITED_PROSE
|
|
||||||
{edited}
|
|
||||||
EDITED_PROSE
|
|
||||||
|
|
||||||
Emit the updated .ail.json now.
|
|
||||||
",
|
",
|
||||||
orig = orig_ail_json,
|
);
|
||||||
edited = edited_prose,
|
out.push_str("FORM-A SPECIFICATION\n");
|
||||||
)
|
out.push_str("<<<FORM_A_SPEC\n");
|
||||||
|
out.push_str(ailang_core::FORM_A_SPEC);
|
||||||
|
if !ailang_core::FORM_A_SPEC.ends_with('\n') {
|
||||||
|
out.push('\n');
|
||||||
|
}
|
||||||
|
out.push_str("FORM_A_SPEC\n\n");
|
||||||
|
out.push_str("ORIGINAL MODULE (Form-A)\n");
|
||||||
|
out.push_str("<<<ORIGINAL_FORM_A\n");
|
||||||
|
out.push_str(original_form_a);
|
||||||
|
if !original_form_a.ends_with('\n') {
|
||||||
|
out.push('\n');
|
||||||
|
}
|
||||||
|
out.push_str("ORIGINAL_FORM_A\n\n");
|
||||||
|
out.push_str("EDITED PROSE\n");
|
||||||
|
out.push_str("<<<EDITED_PROSE\n");
|
||||||
|
out.push_str(edited_prose);
|
||||||
|
if !edited_prose.ends_with('\n') {
|
||||||
|
out.push('\n');
|
||||||
|
}
|
||||||
|
out.push_str("EDITED_PROSE\n\n");
|
||||||
|
out.push_str("Emit the updated Form-A module now.\n");
|
||||||
|
out
|
||||||
}
|
}
|
||||||
|
|
||||||
fn main() -> Result<()> {
|
fn main() -> Result<()> {
|
||||||
@@ -418,15 +418,18 @@ fn main() -> Result<()> {
|
|||||||
print!("{}", ailang_prose::module_to_prose(&m));
|
print!("{}", ailang_prose::module_to_prose(&m));
|
||||||
}
|
}
|
||||||
Cmd::MergeProse { original, edited } => {
|
Cmd::MergeProse { original, edited } => {
|
||||||
// Iter 20d: read both inputs verbatim, compose the prompt,
|
// Iter 20f: load the original .ail.json, render it as
|
||||||
// print to stdout. No schema validation here — `ail check`
|
// Form-A (the canonical authoring surface, Decision 6),
|
||||||
// exists for that purpose, and merge-prose is intentionally
|
// and embed *that* in the prompt — not the raw JSON-AST.
|
||||||
// a pure prompt-shaper.
|
// Form-A is the form an LLM should produce; JSON is the
|
||||||
let orig = std::fs::read_to_string(&original)
|
// hashable artefact, not the writing surface. The prose
|
||||||
.with_context(|| format!("reading {}", original.display()))?;
|
// file is embedded byte-for-byte.
|
||||||
|
let module = ailang_core::load_module(&original)
|
||||||
|
.with_context(|| format!("loading {}", original.display()))?;
|
||||||
|
let original_form_a = ailang_surface::print(&module);
|
||||||
let prose = std::fs::read_to_string(&edited)
|
let prose = std::fs::read_to_string(&edited)
|
||||||
.with_context(|| format!("reading {}", edited.display()))?;
|
.with_context(|| format!("reading {}", edited.display()))?;
|
||||||
print!("{}", compose_merge_prose_prompt(&orig, &prose));
|
print!("{}", compose_merge_prose_prompt(&original_form_a, &prose));
|
||||||
}
|
}
|
||||||
Cmd::Describe { path, name, json, workspace } => {
|
Cmd::Describe { path, name, json, workspace } => {
|
||||||
if workspace {
|
if workspace {
|
||||||
@@ -1911,22 +1914,28 @@ fn build_to(
|
|||||||
mod tests {
|
mod tests {
|
||||||
use super::compose_merge_prose_prompt;
|
use super::compose_merge_prose_prompt;
|
||||||
|
|
||||||
/// The composed prompt must contain both inputs byte-for-byte —
|
/// The composed prompt must contain all three payloads
|
||||||
/// the LLM has to see exactly what the user wrote, with no
|
/// byte-for-byte — the LLM has to see exactly what the user wrote,
|
||||||
/// re-encoding or stripping.
|
/// the original module's Form-A bytes, and the embedded spec, with
|
||||||
|
/// no re-encoding or stripping.
|
||||||
#[test]
|
#[test]
|
||||||
fn merge_prose_prompt_contains_both_inputs_verbatim() {
|
fn merge_prose_prompt_contains_all_payloads_verbatim() {
|
||||||
let orig = "{\"schema\":\"ailang/v0\",\"name\":\"foo\",\"defs\":[]}";
|
let orig = "(module foo\n (fn main\n (type (fn-type (params) (ret (con Unit))))\n (params)\n (body (lit-unit))))\n";
|
||||||
let prose = "// module foo\n\nfn bar() -> Int { 42 }\n";
|
let prose = "// module foo\n\nfn main() -> Unit { () }\n";
|
||||||
let out = compose_merge_prose_prompt(orig, prose);
|
let out = compose_merge_prose_prompt(orig, prose);
|
||||||
assert!(
|
assert!(
|
||||||
out.contains(orig),
|
out.contains(orig),
|
||||||
"prompt missing original .ail.json verbatim; got:\n{out}"
|
"prompt missing original Form-A verbatim; got:\n{out}"
|
||||||
);
|
);
|
||||||
assert!(
|
assert!(
|
||||||
out.contains(prose),
|
out.contains(prose),
|
||||||
"prompt missing edited prose verbatim; got:\n{out}"
|
"prompt missing edited prose verbatim; got:\n{out}"
|
||||||
);
|
);
|
||||||
|
// The full FORM_A_SPEC must appear in the prompt.
|
||||||
|
assert!(
|
||||||
|
out.contains(ailang_core::FORM_A_SPEC),
|
||||||
|
"prompt missing the FORM_A_SPEC body verbatim"
|
||||||
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
/// The framing sections must all be present so the LLM has the
|
/// The framing sections must all be present so the LLM has the
|
||||||
@@ -1934,44 +1943,35 @@ mod tests {
|
|||||||
/// landmark from each section.
|
/// landmark from each section.
|
||||||
#[test]
|
#[test]
|
||||||
fn merge_prose_prompt_has_all_framing_sections() {
|
fn merge_prose_prompt_has_all_framing_sections() {
|
||||||
let out = compose_merge_prose_prompt("{}", "");
|
let out = compose_merge_prose_prompt("(module x)", "");
|
||||||
// Role statement.
|
|
||||||
assert!(
|
assert!(
|
||||||
out.contains("ROLE")
|
out.contains("ROLE") && out.contains("Form-A"),
|
||||||
&& out.contains("integrating prose edits"),
|
|
||||||
"prompt missing ROLE section"
|
"prompt missing ROLE section"
|
||||||
);
|
);
|
||||||
// Contract about preserving load-bearing detail.
|
|
||||||
assert!(
|
assert!(
|
||||||
out.contains("CONTRACT")
|
out.contains("CONTRACT")
|
||||||
&& out.contains("preserve those")
|
&& out.contains("preserve those")
|
||||||
&& out.contains("`own T`")
|
&& out.contains("(own T)")
|
||||||
&& out.contains("`with IO`"),
|
&& out.contains("(effects IO)"),
|
||||||
"prompt missing CONTRACT section"
|
"prompt missing CONTRACT section"
|
||||||
);
|
);
|
||||||
// Output spec — JSON only, no fences, no commentary.
|
|
||||||
assert!(
|
assert!(
|
||||||
out.contains("OUTPUT")
|
out.contains("OUTPUT")
|
||||||
&& out.contains("ONLY")
|
&& out.contains("ONLY")
|
||||||
&& out.contains("no markdown"),
|
&& out.contains("no markdown"),
|
||||||
"prompt missing OUTPUT section"
|
"prompt missing OUTPUT section"
|
||||||
);
|
);
|
||||||
// Schema-essentials reminder + DESIGN.md pointer.
|
// The embedded language spec, by section header.
|
||||||
assert!(
|
assert!(
|
||||||
out.contains("SCHEMA ESSENTIALS")
|
out.contains("FORM-A SPECIFICATION"),
|
||||||
&& out.contains("docs/DESIGN.md")
|
"prompt missing FORM-A SPECIFICATION header"
|
||||||
&& out.contains("`kind`")
|
|
||||||
&& out.contains("`k`")
|
|
||||||
&& out.contains("`t`")
|
|
||||||
&& out.contains("`p`")
|
|
||||||
&& out.contains("param_modes")
|
|
||||||
&& out.contains("Term::Ctor"),
|
|
||||||
"prompt missing SCHEMA ESSENTIALS section"
|
|
||||||
);
|
);
|
||||||
// Heredoc-style markers around both payloads.
|
// Heredoc-style markers around all three payloads.
|
||||||
assert!(
|
assert!(
|
||||||
out.contains("<<<ORIGINAL_AIL_JSON")
|
out.contains("<<<FORM_A_SPEC")
|
||||||
&& out.contains("ORIGINAL_AIL_JSON\n")
|
&& out.contains("FORM_A_SPEC\n")
|
||||||
|
&& out.contains("<<<ORIGINAL_FORM_A")
|
||||||
|
&& out.contains("ORIGINAL_FORM_A\n")
|
||||||
&& out.contains("<<<EDITED_PROSE")
|
&& out.contains("<<<EDITED_PROSE")
|
||||||
&& out.contains("EDITED_PROSE\n"),
|
&& out.contains("EDITED_PROSE\n"),
|
||||||
"prompt missing payload markers"
|
"prompt missing payload markers"
|
||||||
@@ -1982,7 +1982,7 @@ mod tests {
|
|||||||
/// output.
|
/// output.
|
||||||
#[test]
|
#[test]
|
||||||
fn merge_prose_prompt_is_deterministic() {
|
fn merge_prose_prompt_is_deterministic() {
|
||||||
let orig = "{\"x\":1}";
|
let orig = "(module y)";
|
||||||
let prose = "fn f() {}";
|
let prose = "fn f() {}";
|
||||||
let a = compose_merge_prose_prompt(orig, prose);
|
let a = compose_merge_prose_prompt(orig, prose);
|
||||||
let b = compose_merge_prose_prompt(orig, prose);
|
let b = compose_merge_prose_prompt(orig, prose);
|
||||||
|
|||||||
+13
-3
@@ -2387,6 +2387,11 @@ fn merge_prose_prints_framed_prompt() {
|
|||||||
std::fs::create_dir_all(&tmp).unwrap();
|
std::fs::create_dir_all(&tmp).unwrap();
|
||||||
let orig_path = tmp.join("orig.ail.json");
|
let orig_path = tmp.join("orig.ail.json");
|
||||||
let prose_path = tmp.join("edited.prose.txt");
|
let prose_path = tmp.join("edited.prose.txt");
|
||||||
|
// Iter 20f: merge-prose now loads the module via ailang_core,
|
||||||
|
// renders to Form-A, and embeds *that* in the prompt — so the
|
||||||
|
// input must be a well-formed ailang/v0 JSON-AST that
|
||||||
|
// load_module accepts. The schema, name, and an empty defs list
|
||||||
|
// are the minimum.
|
||||||
let orig_bytes =
|
let orig_bytes =
|
||||||
b"{\"schema\":\"ailang/v0\",\"name\":\"foo\",\"imports\":[],\"defs\":[]}";
|
b"{\"schema\":\"ailang/v0\",\"name\":\"foo\",\"imports\":[],\"defs\":[]}";
|
||||||
let prose_bytes = b"// module foo\n\nfn bar() -> Int { 42 }\n";
|
let prose_bytes = b"// module foo\n\nfn bar() -> Int { 42 }\n";
|
||||||
@@ -2410,13 +2415,18 @@ fn merge_prose_prints_framed_prompt() {
|
|||||||
stdout.contains("integrating prose edits"),
|
stdout.contains("integrating prose edits"),
|
||||||
"prompt missing role-statement landmark; got:\n{stdout}"
|
"prompt missing role-statement landmark; got:\n{stdout}"
|
||||||
);
|
);
|
||||||
// Both inputs must round-trip into the prompt verbatim.
|
// Original module is now embedded as Form-A, not JSON.
|
||||||
assert!(
|
assert!(
|
||||||
stdout.contains("ailang/v0"),
|
stdout.contains("(module foo"),
|
||||||
"prompt missing original .ail.json content"
|
"prompt missing original Form-A content; got:\n{stdout}"
|
||||||
);
|
);
|
||||||
assert!(
|
assert!(
|
||||||
stdout.contains("fn bar() -> Int { 42 }"),
|
stdout.contains("fn bar() -> Int { 42 }"),
|
||||||
"prompt missing edited prose content"
|
"prompt missing edited prose content"
|
||||||
);
|
);
|
||||||
|
// The embedded spec must be present.
|
||||||
|
assert!(
|
||||||
|
stdout.contains("FORM-A SPECIFICATION"),
|
||||||
|
"prompt missing FORM-A SPECIFICATION section"
|
||||||
|
);
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -0,0 +1,397 @@
|
|||||||
|
# AILang Form-A — LLM authoring specification
|
||||||
|
|
||||||
|
Form-A is the canonical textual surface of AILang. It is the form that
|
||||||
|
LLMs generate when asked to produce or edit AILang code, and the form
|
||||||
|
that `ail parse <file>.ailx` reads. The inverse direction — printing
|
||||||
|
JSON-AST as Form-A — is `ail render <file>.ail.json`. Round-trip
|
||||||
|
through this pair is the gating contract: `parse(render(m)) == m`
|
||||||
|
for every well-formed module.
|
||||||
|
|
||||||
|
This document is the **complete LLM-targeted specification**. If you
|
||||||
|
are an LLM and this is in your context, you have everything you need
|
||||||
|
to produce valid Form-A. The file lives at
|
||||||
|
`crates/ailang-core/specs/form_a.md` next to the AST definitions, and
|
||||||
|
a unit test (`tests/spec_drift.rs`) walks every AST enum variant and
|
||||||
|
asserts its serde tag appears here — so this document cannot silently
|
||||||
|
fall behind the language.
|
||||||
|
|
||||||
|
## Why Form-A and not JSON
|
||||||
|
|
||||||
|
The hashable artefact is `.ail.json`, but no human or LLM should write
|
||||||
|
that directly. JSON-AST is a mechanical serialization with high
|
||||||
|
boilerplate (`{"k": "con", "name": "Int"}` per type reference, mandatory
|
||||||
|
field tags, every term wrapped). Form-A is the same information in a
|
||||||
|
Lisp-style S-expression dress that:
|
||||||
|
|
||||||
|
- omits structural noise (no field tags; positions carry meaning)
|
||||||
|
- has a real parser with positional error messages
|
||||||
|
- round-trips through `ail render` ↔ `ail parse` losslessly
|
||||||
|
- is the form every existing `examples/*.ailx` is written in
|
||||||
|
|
||||||
|
LLMs generate Form-A; the toolchain converts to JSON.
|
||||||
|
|
||||||
|
## Conventions
|
||||||
|
|
||||||
|
- `NAME` is a bare identifier: letters, digits, `_`, `-`, `+`, `*`,
|
||||||
|
`/`, `<`, `>`, `=`, `!`, `?`, `%`. Cannot start with a digit.
|
||||||
|
- `STRING` is a double-quoted UTF-8 literal: `"hello"`. Backslash
|
||||||
|
escapes: `\"`, `\\`, `\n`, `\t`.
|
||||||
|
- `INT` is a signed decimal integer; leading `-` is allowed.
|
||||||
|
- Whitespace and `;`-prefixed line comments are insignificant.
|
||||||
|
- `?` after a clause means optional. `*` means zero or more.
|
||||||
|
|
||||||
|
## Module structure
|
||||||
|
|
||||||
|
```
|
||||||
|
(module NAME
|
||||||
|
IMPORT*
|
||||||
|
DEF*)
|
||||||
|
```
|
||||||
|
|
||||||
|
The module name MUST equal the file stem (`bench_list_sum.ailx` →
|
||||||
|
`(module bench_list_sum ...)`).
|
||||||
|
|
||||||
|
## Imports
|
||||||
|
|
||||||
|
```
|
||||||
|
(import MODULE-NAME)
|
||||||
|
(import MODULE-NAME (as ALIAS))
|
||||||
|
```
|
||||||
|
|
||||||
|
The alias clause is optional. Imported modules are resolved relative
|
||||||
|
to the entry file's directory.
|
||||||
|
|
||||||
|
## Definitions
|
||||||
|
|
||||||
|
Three kinds, matched on the leading keyword:
|
||||||
|
|
||||||
|
### Function — `(fn ...)`
|
||||||
|
|
||||||
|
```
|
||||||
|
(fn NAME
|
||||||
|
(doc STRING)?
|
||||||
|
(suppress (code STRING) (because STRING))*
|
||||||
|
(type FN-TYPE)
|
||||||
|
(params NAME*)
|
||||||
|
(body TERM))
|
||||||
|
```
|
||||||
|
|
||||||
|
`doc` is optional but recommended — it appears in the prose projection
|
||||||
|
and helps downstream readers (human and LLM).
|
||||||
|
|
||||||
|
`suppress` clauses silence advisory diagnostics for this def. The
|
||||||
|
`code` MUST be one of the registered codes (today: `over-strict-mode`).
|
||||||
|
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.
|
||||||
|
|
||||||
|
`params` is a list of bare names that bind the parameters in `body`.
|
||||||
|
The list length must match the number of params in `type`.
|
||||||
|
|
||||||
|
### Data type — `(data ...)`
|
||||||
|
|
||||||
|
```
|
||||||
|
(data NAME
|
||||||
|
(vars TYVAR+)?
|
||||||
|
(doc STRING)?
|
||||||
|
(ctor CTOR-NAME ARG-TYPE*)*)
|
||||||
|
```
|
||||||
|
|
||||||
|
`vars` makes the type polymorphic; absent means monomorphic. Each
|
||||||
|
`ctor` clause is one variant. `ARG-TYPE` is a `TYPE` — see below.
|
||||||
|
|
||||||
|
### Constant — `(const ...)`
|
||||||
|
|
||||||
|
```
|
||||||
|
(const NAME
|
||||||
|
(doc STRING)?
|
||||||
|
(type TYPE)
|
||||||
|
(body TERM))
|
||||||
|
```
|
||||||
|
|
||||||
|
## Types
|
||||||
|
|
||||||
|
Four shapes, all parenthesised except a bare type variable:
|
||||||
|
|
||||||
|
```
|
||||||
|
TYVAR-NAME ; type variable (e.g. `a`, `T`)
|
||||||
|
(con NAME TYPE-ARG*) ; type-constructor application
|
||||||
|
(fn-type (params PARAM*)
|
||||||
|
(ret RETURN-PARAM)
|
||||||
|
(effects EFFECT-NAME*)?) ; function type
|
||||||
|
(forall (vars TYVAR+) BODY-TYPE) ; polymorphic schema
|
||||||
|
```
|
||||||
|
|
||||||
|
`PARAM` and `RETURN-PARAM` are types, optionally wrapped in a mode
|
||||||
|
annotation:
|
||||||
|
|
||||||
|
```
|
||||||
|
TYPE ; implicit mode (DO NOT USE in new (fn ...) defs)
|
||||||
|
(own TYPE) ; caller transfers ownership; callee consumes
|
||||||
|
(borrow TYPE) ; caller retains ownership; callee must not consume
|
||||||
|
```
|
||||||
|
|
||||||
|
`EFFECT-NAME` is a bare identifier — currently `IO` and `Diverge`.
|
||||||
|
Effects are a set; order is irrelevant.
|
||||||
|
|
||||||
|
Built-in type-constructors: `Int`, `Bool`, `Str`, `Unit`. User ADTs
|
||||||
|
use the name from the `(data ...)` def.
|
||||||
|
|
||||||
|
Examples:
|
||||||
|
|
||||||
|
```
|
||||||
|
(con Int)
|
||||||
|
(con List (con Int))
|
||||||
|
(fn-type (params (own (con List)) (borrow (con Int))) (ret (con Int)))
|
||||||
|
(forall (vars a) (fn-type (params (con List a)) (ret (con Int))))
|
||||||
|
```
|
||||||
|
|
||||||
|
## Terms
|
||||||
|
|
||||||
|
Atom forms (no parens):
|
||||||
|
|
||||||
|
- `INT` — integer literal
|
||||||
|
- `STRING` — string literal
|
||||||
|
- `true`, `false` — bool literals
|
||||||
|
- `NAME` — variable reference (parameter, local, top-level def, or import alias)
|
||||||
|
|
||||||
|
Parenthesised forms:
|
||||||
|
|
||||||
|
```
|
||||||
|
(lit-unit) ; the unit value ()
|
||||||
|
(app FN ARG+) ; function application (≥1 arg)
|
||||||
|
(tail-app FN ARG+) ; tail-position application (Decision 8)
|
||||||
|
(do OP-NAME ARG*) ; effect operation
|
||||||
|
(tail-do OP-NAME ARG*) ; tail-position effect
|
||||||
|
(let NAME VALUE-TERM BODY-TERM) ; binding
|
||||||
|
(let-rec NAME (params NAME*) (type FN-TYPE) (body TERM)
|
||||||
|
(in BODY-TERM)) ; recursive let (fn-shaped)
|
||||||
|
(if COND-TERM THEN-TERM ELSE-TERM) ; conditional
|
||||||
|
(match SCRUTINEE-TERM (case PAT BODY)+) ; pattern match (≥1 arm)
|
||||||
|
(term-ctor TYPE-NAME CTOR-NAME ARG*) ; constructor application
|
||||||
|
(lam (params (typed NAME TYPE)*)
|
||||||
|
(ret RETURN-TYPE)
|
||||||
|
(effects EFFECT-NAME*)?
|
||||||
|
(body TERM)) ; anonymous function (Iter 8b)
|
||||||
|
(seq EFFECTFUL-TERM RESULT-TERM) ; sequence; lhs evaluated for effect
|
||||||
|
(clone TERM) ; explicit RC clone (Iter 18c.1)
|
||||||
|
(reuse-as SOURCE-TERM BODY-TERM) ; explicit reuse hint (Iter 18d.1)
|
||||||
|
```
|
||||||
|
|
||||||
|
Notes:
|
||||||
|
|
||||||
|
- `app` and `do` REQUIRE the right tag for the right thing.
|
||||||
|
Constructors are NEVER called with `app`; always use `term-ctor`.
|
||||||
|
- `tail-app` / `tail-do` mark the call as occurring in tail position
|
||||||
|
per Decision 8. Codegen lowers them to `musttail call`. Use the
|
||||||
|
tail variant whenever a recursive call is the final action of an
|
||||||
|
arm — it converts unbounded recursion into iteration. Non-tail
|
||||||
|
variants are otherwise indistinguishable in semantics.
|
||||||
|
- `seq` is `(seq A B)` — A is evaluated for its effects and result
|
||||||
|
discarded; B is the value of the whole expression. For pure A,
|
||||||
|
prefer `(let _ A B)` or just drop A.
|
||||||
|
- `reuse-as` requires `SOURCE-TERM` to be a bare variable reference
|
||||||
|
(a `NAME` in the term grammar). Anything else fails the linearity
|
||||||
|
check with `reuse-as-source-not-bare-var`.
|
||||||
|
|
||||||
|
## Patterns
|
||||||
|
|
||||||
|
```
|
||||||
|
_ ; wildcard; matches anything, binds nothing
|
||||||
|
NAME ; variable; binds the value to NAME
|
||||||
|
(pat-lit LIT-FORM) ; literal match: integer, true/false, string
|
||||||
|
(pat-ctor CTOR-NAME FIELD*) ; constructor; FIELD is itself a pattern
|
||||||
|
```
|
||||||
|
|
||||||
|
`LIT-FORM` is `INT`, `true`, `false`, or `STRING` — the same atoms used
|
||||||
|
as terms.
|
||||||
|
|
||||||
|
A pattern variable may bind at most once per arm. Pattern-binders are
|
||||||
|
in scope inside the arm body.
|
||||||
|
|
||||||
|
## Schema invariants enforced by `ail check`
|
||||||
|
|
||||||
|
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
|
||||||
|
(i.e. anything other than `(con Int)`, `(con Bool)`, `(con Unit)`,
|
||||||
|
`(con Str)`). Implicit mode on a `(fn ...)` def 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))`.
|
||||||
|
3. **Effects on side-effecting fns.** A function whose body uses `(do ...)`
|
||||||
|
MUST list every effect operation's effect in its `(effects ...)`
|
||||||
|
clause. `IO` for `io/print_*`; `Diverge` for `diverge/*`.
|
||||||
|
4. **Tail correctness.** `(tail-app f x)` MUST appear in tail position
|
||||||
|
— i.e. as the body of a fn, the last expression of a `(seq ...)`,
|
||||||
|
the chosen arm of an `(if ...)` or `(match ...)`, or the body of
|
||||||
|
a `(let ...)`. A `tail-app` outside a tail position is rejected.
|
||||||
|
5. **Linearity for own/borrow.** A parameter declared `(own T)` must
|
||||||
|
be consumed exactly once on every reachable path; a `(borrow T)`
|
||||||
|
must never be consumed. The diagnostic catalog has named codes
|
||||||
|
for the typical violations.
|
||||||
|
|
||||||
|
## Pitfalls
|
||||||
|
|
||||||
|
LLMs without prior AILang exposure tend to make the following errors.
|
||||||
|
Reading these once before generating Form-A reduces re-roll cost
|
||||||
|
significantly.
|
||||||
|
|
||||||
|
- **Bare type names instead of `(con T)`.** Writing `Int` where a type
|
||||||
|
is expected does NOT work — types live inside `(con ...)`. Only
|
||||||
|
`TYVAR-NAME` (a single ident) parses as a type without parens, and
|
||||||
|
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 ...)`.
|
||||||
|
- **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.
|
||||||
|
- **Forgetting `tail-`.** A non-tail call in tail position works, but
|
||||||
|
three million stack frames will overflow. For recursive fns where
|
||||||
|
the recursive call is the final action, use `tail-app`.
|
||||||
|
- **Wrong arity in `(case (pat-ctor C f1 f2 ...) ...)`.** The number
|
||||||
|
of pattern fields must equal the constructor's declared arity. The
|
||||||
|
checker catches this but the message is clearer if you do too.
|
||||||
|
- **Strings inside `(suppress (because ...))` must be non-empty.** Empty
|
||||||
|
is an error. Whitespace-only is an error. Write a real reason.
|
||||||
|
|
||||||
|
## Few-shot corpus
|
||||||
|
|
||||||
|
These four modules are real `examples/*.ailx` content. Each one is
|
||||||
|
parseable and typechecks clean. Pattern-match against them when
|
||||||
|
generating new code.
|
||||||
|
|
||||||
|
### 1 — `hello.ailx`: minimal IO program
|
||||||
|
|
||||||
|
```
|
||||||
|
(module hello
|
||||||
|
(fn main
|
||||||
|
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||||
|
(params)
|
||||||
|
(body (do io/print_str "Hello, AILang."))))
|
||||||
|
```
|
||||||
|
|
||||||
|
### 2 — `borrow_own_demo.ailx`: mode annotations on a recursive list
|
||||||
|
|
||||||
|
```
|
||||||
|
(module borrow_own_demo
|
||||||
|
|
||||||
|
(data List
|
||||||
|
(doc "Monomorphic singly-linked Int list — boxed, recursive.")
|
||||||
|
(ctor Nil)
|
||||||
|
(ctor Cons (con Int) (con List)))
|
||||||
|
|
||||||
|
(fn list_length
|
||||||
|
(doc "Borrow xs, count its elements.")
|
||||||
|
(type
|
||||||
|
(fn-type
|
||||||
|
(params (borrow (con List)))
|
||||||
|
(ret (con Int))))
|
||||||
|
(params xs)
|
||||||
|
(body
|
||||||
|
(match xs
|
||||||
|
(case (pat-ctor Nil) 0)
|
||||||
|
(case (pat-ctor Cons h t)
|
||||||
|
(app + 1 (app list_length t))))))
|
||||||
|
|
||||||
|
(fn sum_list
|
||||||
|
(doc "Consume xs, sum its elements.")
|
||||||
|
(type
|
||||||
|
(fn-type
|
||||||
|
(params (own (con List)))
|
||||||
|
(ret (con Int))))
|
||||||
|
(params xs)
|
||||||
|
(body
|
||||||
|
(match xs
|
||||||
|
(case (pat-ctor Nil) 0)
|
||||||
|
(case (pat-ctor Cons h t)
|
||||||
|
(app + h (app sum_list t))))))
|
||||||
|
|
||||||
|
(fn main
|
||||||
|
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||||
|
(params)
|
||||||
|
(body
|
||||||
|
(let xs
|
||||||
|
(term-ctor List Cons 1
|
||||||
|
(term-ctor List Cons 2
|
||||||
|
(term-ctor List Cons 3
|
||||||
|
(term-ctor List Nil))))
|
||||||
|
(seq
|
||||||
|
(do io/print_int (app list_length xs))
|
||||||
|
(do io/print_int (app sum_list xs)))))))
|
||||||
|
```
|
||||||
|
|
||||||
|
### 3 — `lit_pat.ailx`: literal patterns and nested ctor patterns
|
||||||
|
|
||||||
|
```
|
||||||
|
(module lit_pat
|
||||||
|
|
||||||
|
(data IntList
|
||||||
|
(ctor Nil)
|
||||||
|
(ctor Cons (con Int) (con IntList)))
|
||||||
|
|
||||||
|
(fn classify
|
||||||
|
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||||
|
(params n)
|
||||||
|
(body
|
||||||
|
(match n
|
||||||
|
(case (pat-lit 0) 100)
|
||||||
|
(case (pat-lit 1) 200)
|
||||||
|
(case _ 999))))
|
||||||
|
|
||||||
|
(fn categorize_first
|
||||||
|
(type (fn-type (params (own (con IntList))) (ret (con Int))))
|
||||||
|
(params xs)
|
||||||
|
(body
|
||||||
|
(match xs
|
||||||
|
(case (pat-ctor Nil) -1)
|
||||||
|
(case (pat-ctor Cons (pat-lit 0) _) 0)
|
||||||
|
(case (pat-ctor Cons h _) h)))))
|
||||||
|
```
|
||||||
|
|
||||||
|
### 4 — Tail-recursive sum (the canonical big-N pattern)
|
||||||
|
|
||||||
|
```
|
||||||
|
(module sum_demo
|
||||||
|
(data IntList
|
||||||
|
(ctor INil)
|
||||||
|
(ctor ICons (con Int) (con IntList)))
|
||||||
|
|
||||||
|
(fn sum_acc
|
||||||
|
(doc "Tail-recursive accumulator.")
|
||||||
|
(type
|
||||||
|
(fn-type
|
||||||
|
(params (own (con IntList)) (con Int))
|
||||||
|
(ret (con Int))))
|
||||||
|
(params xs acc)
|
||||||
|
(body
|
||||||
|
(match xs
|
||||||
|
(case (pat-ctor INil) acc)
|
||||||
|
(case (pat-ctor ICons h t)
|
||||||
|
(tail-app sum_acc t (app + acc h))))))
|
||||||
|
|
||||||
|
(fn sum_list
|
||||||
|
(type
|
||||||
|
(fn-type
|
||||||
|
(params (own (con IntList)))
|
||||||
|
(ret (con Int))))
|
||||||
|
(params xs)
|
||||||
|
(body
|
||||||
|
(app sum_acc xs 0))))
|
||||||
|
```
|
||||||
|
|
||||||
|
Notice in (4): the recursive `sum_acc` call is `tail-app`, the addition
|
||||||
|
is plain `app`. The accumulator parameter is `(con Int)` (no mode —
|
||||||
|
`Int` is a primitive value type, not heap-shaped, so modes do not
|
||||||
|
apply to it).
|
||||||
@@ -96,6 +96,18 @@ pub type Result<T> = std::result::Result<T, Error>;
|
|||||||
/// loading fails with [`Error::SchemaMismatch`].
|
/// loading fails with [`Error::SchemaMismatch`].
|
||||||
pub const SCHEMA: &str = "ailang/v0";
|
pub const SCHEMA: &str = "ailang/v0";
|
||||||
|
|
||||||
|
/// Iter 20f: complete LLM-targeted specification of Form-A — the
|
||||||
|
/// canonical authoring surface (Decision 6). Embedded verbatim into
|
||||||
|
/// any prompt that asks an LLM to produce or edit AILang code; in
|
||||||
|
/// particular, `ail merge-prose` includes it in the round-trip
|
||||||
|
/// prompt template. The string is the raw bytes of
|
||||||
|
/// `specs/form_a.md`, co-located with this crate so the spec sits
|
||||||
|
/// next to the AST it describes; a drift test
|
||||||
|
/// (`tests/spec_drift.rs`) walks every AST enum variant and asserts
|
||||||
|
/// its serde tag appears in this string. Adding a new variant
|
||||||
|
/// without updating the spec fails the test suite.
|
||||||
|
pub const FORM_A_SPEC: &str = include_str!("../specs/form_a.md");
|
||||||
|
|
||||||
/// Load a single module file, validate its schema, and deserialize it
|
/// Load a single module file, validate its schema, and deserialize it
|
||||||
/// into a [`Module`].
|
/// into a [`Module`].
|
||||||
///
|
///
|
||||||
|
|||||||
@@ -0,0 +1,316 @@
|
|||||||
|
//! Iter 20f: drift detection between the AST and `specs/form_a.md`.
|
||||||
|
//!
|
||||||
|
//! The spec is hand-curated, but it cannot silently fall behind the
|
||||||
|
//! language. Every AST enum (`Term`, `Pattern`, `Type`, `Def`, `Literal`,
|
||||||
|
//! `ParamMode`) discriminates on a `#[serde(rename = "...")]` tag.
|
||||||
|
//! These tests construct a sample of every variant, then check that the
|
||||||
|
//! corresponding tag string (or its parenthesised Form-A keyword) appears
|
||||||
|
//! in the spec.
|
||||||
|
//!
|
||||||
|
//! The exhaustive `match` is the load-bearing piece: adding a new variant
|
||||||
|
//! without a spec entry fails compilation here long before the test runs.
|
||||||
|
//! Once the variant is matched, the test asserts the spec mentions it.
|
||||||
|
|
||||||
|
use ailang_core::ast::{
|
||||||
|
ConstDef, Ctor, Def, FnDef, Literal, Pattern, Suppress, Term, Type, TypeDef,
|
||||||
|
};
|
||||||
|
use ailang_core::FORM_A_SPEC;
|
||||||
|
|
||||||
|
/// Every `Term` variant must be reachable from the spec. The Form-A
|
||||||
|
/// keyword for each variant is what the spec is supposed to teach an
|
||||||
|
/// LLM; if it is missing here, the LLM cannot produce that term.
|
||||||
|
#[test]
|
||||||
|
fn spec_mentions_every_term_variant() {
|
||||||
|
let exemplars: Vec<(&str, Term)> = vec![
|
||||||
|
("(lit-unit", Term::Lit { lit: Literal::Unit }),
|
||||||
|
// The Var form has no parenthesised keyword (a bare ident is a
|
||||||
|
// var-ref). The spec calls it out under "Atom forms"; we look for
|
||||||
|
// that anchor.
|
||||||
|
("Atom forms", Term::Var { name: "x".into() }),
|
||||||
|
(
|
||||||
|
"(app",
|
||||||
|
Term::App {
|
||||||
|
callee: Box::new(Term::Var { name: "f".into() }),
|
||||||
|
args: vec![Term::Var { name: "x".into() }],
|
||||||
|
tail: false,
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(let ",
|
||||||
|
Term::Let {
|
||||||
|
name: "x".into(),
|
||||||
|
value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
|
||||||
|
body: Box::new(Term::Var { name: "x".into() }),
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(let-rec",
|
||||||
|
Term::LetRec {
|
||||||
|
name: "f".into(),
|
||||||
|
ty: Type::fn_implicit(vec![], Type::int(), vec![]),
|
||||||
|
params: vec![],
|
||||||
|
body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
|
||||||
|
in_term: Box::new(Term::Var { name: "f".into() }),
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(if",
|
||||||
|
Term::If {
|
||||||
|
cond: Box::new(Term::Lit { lit: Literal::Bool { value: true } }),
|
||||||
|
then: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
|
||||||
|
else_: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(do ",
|
||||||
|
Term::Do {
|
||||||
|
op: "io/print_int".into(),
|
||||||
|
args: vec![],
|
||||||
|
tail: false,
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(term-ctor",
|
||||||
|
Term::Ctor {
|
||||||
|
type_name: "List".into(),
|
||||||
|
ctor: "Nil".into(),
|
||||||
|
args: vec![],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(match",
|
||||||
|
Term::Match {
|
||||||
|
scrutinee: Box::new(Term::Var { name: "x".into() }),
|
||||||
|
arms: vec![],
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(lam",
|
||||||
|
Term::Lam {
|
||||||
|
params: vec![],
|
||||||
|
param_tys: vec![],
|
||||||
|
ret_ty: Box::new(Type::int()),
|
||||||
|
effects: vec![],
|
||||||
|
body: Box::new(Term::Lit { lit: Literal::Int { value: 0 } }),
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(seq",
|
||||||
|
Term::Seq {
|
||||||
|
lhs: Box::new(Term::Var { name: "a".into() }),
|
||||||
|
rhs: Box::new(Term::Var { name: "b".into() }),
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(clone",
|
||||||
|
Term::Clone {
|
||||||
|
value: Box::new(Term::Var { name: "x".into() }),
|
||||||
|
},
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(reuse-as",
|
||||||
|
Term::ReuseAs {
|
||||||
|
source: Box::new(Term::Var { name: "x".into() }),
|
||||||
|
body: Box::new(Term::Var { name: "y".into() }),
|
||||||
|
},
|
||||||
|
),
|
||||||
|
];
|
||||||
|
|
||||||
|
for (anchor, term) in exemplars {
|
||||||
|
// Force the exhaustive match: the body is just a tag string that
|
||||||
|
// we will not actually use, but the compiler will refuse to
|
||||||
|
// compile this file once a new Term variant is added without a
|
||||||
|
// matching arm.
|
||||||
|
let _: &'static str = match term {
|
||||||
|
Term::Lit { .. } => "lit",
|
||||||
|
Term::Var { .. } => "var",
|
||||||
|
Term::App { .. } => "app",
|
||||||
|
Term::Let { .. } => "let",
|
||||||
|
Term::LetRec { .. } => "letrec",
|
||||||
|
Term::If { .. } => "if",
|
||||||
|
Term::Do { .. } => "do",
|
||||||
|
Term::Ctor { .. } => "ctor",
|
||||||
|
Term::Match { .. } => "match",
|
||||||
|
Term::Lam { .. } => "lam",
|
||||||
|
Term::Seq { .. } => "seq",
|
||||||
|
Term::Clone { .. } => "clone",
|
||||||
|
Term::ReuseAs { .. } => "reuse-as",
|
||||||
|
};
|
||||||
|
assert!(
|
||||||
|
FORM_A_SPEC.contains(anchor),
|
||||||
|
"spec is missing anchor `{anchor}` for a Term variant — \
|
||||||
|
update crates/ailang-core/specs/form_a.md"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Every `Pattern` variant must appear in the spec.
|
||||||
|
#[test]
|
||||||
|
fn spec_mentions_every_pattern_variant() {
|
||||||
|
let exemplars: Vec<(&str, Pattern)> = vec![
|
||||||
|
("_", Pattern::Wild),
|
||||||
|
// pat-var is again the bare-ident form. The spec discusses it
|
||||||
|
// under "Patterns". Use the heading as the anchor.
|
||||||
|
("## Patterns", Pattern::Var { name: "x".into() }),
|
||||||
|
("(pat-lit", Pattern::Lit { lit: Literal::Int { value: 0 } }),
|
||||||
|
(
|
||||||
|
"(pat-ctor",
|
||||||
|
Pattern::Ctor { ctor: "Nil".into(), fields: vec![] },
|
||||||
|
),
|
||||||
|
];
|
||||||
|
|
||||||
|
for (anchor, pat) in exemplars {
|
||||||
|
let _: &'static str = match pat {
|
||||||
|
Pattern::Wild => "wild",
|
||||||
|
Pattern::Var { .. } => "var",
|
||||||
|
Pattern::Lit { .. } => "lit",
|
||||||
|
Pattern::Ctor { .. } => "ctor",
|
||||||
|
};
|
||||||
|
assert!(
|
||||||
|
FORM_A_SPEC.contains(anchor),
|
||||||
|
"spec is missing anchor `{anchor}` for a Pattern variant"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Every `Type` variant must appear in the spec.
|
||||||
|
#[test]
|
||||||
|
fn spec_mentions_every_type_variant() {
|
||||||
|
let exemplars: Vec<(&str, Type)> = vec![
|
||||||
|
("(con ", Type::int()),
|
||||||
|
(
|
||||||
|
"(fn-type",
|
||||||
|
Type::fn_implicit(vec![], Type::unit(), vec![]),
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"TYVAR-NAME",
|
||||||
|
Type::Var { name: "a".into() },
|
||||||
|
),
|
||||||
|
(
|
||||||
|
"(forall",
|
||||||
|
Type::Forall {
|
||||||
|
vars: vec!["a".into()],
|
||||||
|
body: Box::new(Type::Var { name: "a".into() }),
|
||||||
|
},
|
||||||
|
),
|
||||||
|
];
|
||||||
|
|
||||||
|
for (anchor, ty) in exemplars {
|
||||||
|
let _: &'static str = match ty {
|
||||||
|
Type::Con { .. } => "con",
|
||||||
|
Type::Fn { .. } => "fn",
|
||||||
|
Type::Var { .. } => "var",
|
||||||
|
Type::Forall { .. } => "forall",
|
||||||
|
};
|
||||||
|
assert!(
|
||||||
|
FORM_A_SPEC.contains(anchor),
|
||||||
|
"spec is missing anchor `{anchor}` for a Type variant"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Every `Literal` variant must appear in the spec.
|
||||||
|
#[test]
|
||||||
|
fn spec_mentions_every_literal_variant() {
|
||||||
|
// Anchors describe how the literal renders in Form-A.
|
||||||
|
let exemplars: Vec<(&str, Literal)> = vec![
|
||||||
|
("`INT`", Literal::Int { value: 0 }),
|
||||||
|
("`true`, `false`", Literal::Bool { value: true }),
|
||||||
|
("`STRING`", Literal::Str { value: "x".into() }),
|
||||||
|
("(lit-unit)", Literal::Unit),
|
||||||
|
];
|
||||||
|
|
||||||
|
for (anchor, lit) in exemplars {
|
||||||
|
let _: &'static str = match lit {
|
||||||
|
Literal::Int { .. } => "int",
|
||||||
|
Literal::Bool { .. } => "bool",
|
||||||
|
Literal::Str { .. } => "str",
|
||||||
|
Literal::Unit => "unit",
|
||||||
|
};
|
||||||
|
assert!(
|
||||||
|
FORM_A_SPEC.contains(anchor),
|
||||||
|
"spec is missing anchor `{anchor}` for a Literal variant"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// Every `Def` kind must appear in the spec.
|
||||||
|
#[test]
|
||||||
|
fn spec_mentions_every_def_kind() {
|
||||||
|
let fn_def = FnDef {
|
||||||
|
name: "f".into(),
|
||||||
|
doc: None,
|
||||||
|
suppress: vec![],
|
||||||
|
ty: Type::fn_implicit(vec![], Type::int(), vec![]),
|
||||||
|
params: vec![],
|
||||||
|
body: Term::Lit { lit: Literal::Int { value: 0 } },
|
||||||
|
};
|
||||||
|
let const_def = ConstDef {
|
||||||
|
name: "k".into(),
|
||||||
|
doc: None,
|
||||||
|
ty: Type::int(),
|
||||||
|
value: Term::Lit { lit: Literal::Int { value: 0 } },
|
||||||
|
};
|
||||||
|
let type_def = TypeDef {
|
||||||
|
name: "T".into(),
|
||||||
|
doc: None,
|
||||||
|
vars: vec![],
|
||||||
|
ctors: vec![Ctor {
|
||||||
|
name: "C".into(),
|
||||||
|
fields: vec![],
|
||||||
|
}],
|
||||||
|
drop_iterative: false,
|
||||||
|
};
|
||||||
|
let exemplars: Vec<(&str, Def)> = vec![
|
||||||
|
("(fn ", Def::Fn(fn_def)),
|
||||||
|
("(const ", Def::Const(const_def)),
|
||||||
|
("(data ", Def::Type(type_def)),
|
||||||
|
];
|
||||||
|
|
||||||
|
for (anchor, def) in exemplars {
|
||||||
|
let _: &'static str = match def {
|
||||||
|
Def::Fn(_) => "fn",
|
||||||
|
Def::Const(_) => "const",
|
||||||
|
Def::Type(_) => "type",
|
||||||
|
};
|
||||||
|
assert!(
|
||||||
|
FORM_A_SPEC.contains(anchor),
|
||||||
|
"spec is missing anchor `{anchor}` for a Def kind"
|
||||||
|
);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
/// The mode keywords (Decision 10) must appear so an LLM knows the
|
||||||
|
/// Form-A wrapper syntax.
|
||||||
|
#[test]
|
||||||
|
fn spec_mentions_mode_keywords() {
|
||||||
|
assert!(FORM_A_SPEC.contains("(own"), "spec missing `(own ...)`");
|
||||||
|
assert!(FORM_A_SPEC.contains("(borrow"), "spec missing `(borrow ...)`");
|
||||||
|
}
|
||||||
|
|
||||||
|
/// `tail-app` and `tail-do` are distinct keywords from `app`/`do`. The
|
||||||
|
/// spec must mention both, otherwise an LLM cannot produce tail-correct
|
||||||
|
/// code at scale.
|
||||||
|
#[test]
|
||||||
|
fn spec_mentions_tail_variants() {
|
||||||
|
assert!(FORM_A_SPEC.contains("tail-app"), "spec missing `tail-app`");
|
||||||
|
assert!(FORM_A_SPEC.contains("tail-do"), "spec missing `tail-do`");
|
||||||
|
}
|
||||||
|
|
||||||
|
/// `suppress` is part of the surface and the LLM must know how to
|
||||||
|
/// preserve it. Empty-because is itself a diagnostic; the spec calls
|
||||||
|
/// it out so the LLM does not produce empty justifications.
|
||||||
|
#[test]
|
||||||
|
fn spec_mentions_suppress_clause() {
|
||||||
|
assert!(FORM_A_SPEC.contains("(suppress"), "spec missing `(suppress ...)`");
|
||||||
|
assert!(
|
||||||
|
FORM_A_SPEC.contains("empty-suppress-reason"),
|
||||||
|
"spec missing the empty-suppress-reason diagnostic"
|
||||||
|
);
|
||||||
|
// Make sure `Suppress` in the AST can still be constructed — the
|
||||||
|
// exhaustive-match property carries through to the surface.
|
||||||
|
let _ = Suppress {
|
||||||
|
code: "x".into(),
|
||||||
|
because: "y".into(),
|
||||||
|
};
|
||||||
|
}
|
||||||
@@ -512,6 +512,34 @@ projection) and `ail merge-prose <m.ail.json> <edited.prose.txt>`
|
|||||||
(the mediator-prompt composer); both are listed in the CLI section
|
(the mediator-prompt composer); both are listed in the CLI section
|
||||||
below.
|
below.
|
||||||
|
|
||||||
|
**Iter 20f update — Form-A spec embedding.** The 20d `merge-prose`
|
||||||
|
prompt instructed the LLM to emit JSON-AST and offered a 12-line
|
||||||
|
schema-essentials reminder; that combination did not give a
|
||||||
|
foreign LLM enough to produce valid output. 20f revises this:
|
||||||
|
|
||||||
|
- The LLM emits **Form-A** (the canonical authoring surface), not
|
||||||
|
JSON. JSON-AST stays the only hashable artefact, but it is not
|
||||||
|
a writing surface. The user runs `ail parse foo.new.ailx`
|
||||||
|
before `ail check` to produce the canonical JSON.
|
||||||
|
- `crates/ailang-core/specs/form_a.md` is the complete LLM-targeted
|
||||||
|
Form-A specification — grammar, every term / pattern / type /
|
||||||
|
def keyword, schema invariants, pitfall catalogue, four
|
||||||
|
few-shot modules drawn from `examples/*.ailx`. It is exported
|
||||||
|
as `ailang_core::FORM_A_SPEC` and embedded verbatim in every
|
||||||
|
`merge-prose` prompt.
|
||||||
|
- `crates/ailang-core/tests/spec_drift.rs` walks every variant of
|
||||||
|
`Term`, `Pattern`, `Type`, `Def`, `Literal` via exhaustive
|
||||||
|
`match` and asserts an anchor for each appears in the spec.
|
||||||
|
The exhaustive match is the load-bearing piece: adding a new
|
||||||
|
variant without updating the match fails compilation in this
|
||||||
|
test, before its assertions even run. Hand-written content,
|
||||||
|
mechanical drift detection.
|
||||||
|
|
||||||
|
The discussion of richer integration paths (LLM tool-use, MCP
|
||||||
|
server, LSP) was deferred — all three layer additively on the
|
||||||
|
static-prompt path 20f ships, which remains the
|
||||||
|
lowest-common-denominator fallback that always works.
|
||||||
|
|
||||||
## Decision 7: redundancy removal — `Term::If` is not a primitive
|
## Decision 7: redundancy removal — `Term::If` is not a primitive
|
||||||
|
|
||||||
**Status: REVERTED in Iter 14g.** This decision was made on shaky grounds —
|
**Status: REVERTED in Iter 14g.** This decision was made on shaky grounds —
|
||||||
|
|||||||
+106
@@ -9535,3 +9535,109 @@ default):
|
|||||||
handling).
|
handling).
|
||||||
- **Data model (MVP) refresh.** Cosmetic doc-tidy iter to
|
- **Data model (MVP) refresh.** Cosmetic doc-tidy iter to
|
||||||
bring the schema snapshot current.
|
bring the schema snapshot current.
|
||||||
|
|
||||||
|
## 2026-05-08 — Iter 20f: Form-A spec embedding for prose round-trip
|
||||||
|
|
||||||
|
This iter closes a design hole shipped in 20d: the `merge-prose`
|
||||||
|
prompt instructed the LLM to emit JSON-AST, and gave it only a
|
||||||
|
12-line "schema essentials" reminder. JSON-AST is the canonical
|
||||||
|
hashable artefact, but it is not a writing surface, and a 12-line
|
||||||
|
hint is not a language reference. A foreign LLM with no AILang
|
||||||
|
exposure had no realistic shot at producing valid output.
|
||||||
|
|
||||||
|
20f makes two coupled changes.
|
||||||
|
|
||||||
|
### Form-A becomes the LLM's output target
|
||||||
|
|
||||||
|
The prompt now instructs the LLM to emit **Form-A** — the canonical
|
||||||
|
authoring surface fixed by Decision 6. The user's CLI cycle
|
||||||
|
becomes:
|
||||||
|
|
||||||
|
ail prose foo.ail.json > foo.prose.txt
|
||||||
|
$EDITOR foo.prose.txt
|
||||||
|
ail merge-prose foo.ail.json foo.prose.txt > prompt.txt
|
||||||
|
cat prompt.txt | <llm> > foo.new.ailx
|
||||||
|
ail parse foo.new.ailx > foo.new.ail.json
|
||||||
|
ail check foo.new.ail.json
|
||||||
|
mv foo.new.ail.json foo.ail.json # if check is clean
|
||||||
|
|
||||||
|
The original module is loaded via `ailang_core::load_module`
|
||||||
|
(schema-validating) and re-rendered via `ailang_surface::print` for
|
||||||
|
embedding. Form-A round-trip is a gating contract on the surface
|
||||||
|
crate, so this is lossless.
|
||||||
|
|
||||||
|
### Form-A spec embedded in every prompt
|
||||||
|
|
||||||
|
`crates/ailang-core/specs/form_a.md` is a hand-curated, complete
|
||||||
|
LLM-targeted specification of Form-A — grammar, every term /
|
||||||
|
pattern / type / def keyword with parenthesised syntax, schema
|
||||||
|
invariants enforced by the checker, a pitfall catalogue, and four
|
||||||
|
few-shot modules drawn from `examples/*.ailx`. It is exported as
|
||||||
|
`pub const FORM_A_SPEC: &str = include_str!("../specs/form_a.md")`
|
||||||
|
and embedded verbatim in the merge-prose prompt.
|
||||||
|
|
||||||
|
### Drift detection
|
||||||
|
|
||||||
|
The spec is hand-written, so drift was the load-bearing concern in
|
||||||
|
the design discussion (orchestrator note: user pushed back on
|
||||||
|
"docs/AIL_FORM_A_SPEC.md handgeschrieben" precisely because the
|
||||||
|
distance to the code was too big). The fix is mechanical:
|
||||||
|
`crates/ailang-core/tests/spec_drift.rs` walks every variant of
|
||||||
|
`Term`, `Pattern`, `Type`, `Def`, `Literal`, `ParamMode` via
|
||||||
|
exhaustive `match`. The arms are not the assertion — adding a new
|
||||||
|
variant without updating the match is a compile error in this
|
||||||
|
test, before the test even runs. Once the variant is matched, the
|
||||||
|
test asserts an anchor string for it appears in `FORM_A_SPEC`.
|
||||||
|
Eight tests, all green.
|
||||||
|
|
||||||
|
The exhaustive-match-as-trip-wire pattern is the same idea as the
|
||||||
|
`ailang-architect` drift review for DESIGN.md — both surfaces
|
||||||
|
encode load-bearing language semantics that must stay current —
|
||||||
|
but it runs on every `cargo test`, not just at family boundaries.
|
||||||
|
|
||||||
|
### Why hand-written and not generated
|
||||||
|
|
||||||
|
A generator (walking `syn` / proc-macro reflection on the AST,
|
||||||
|
emitting a tag table) would close the structural-drift channel
|
||||||
|
mechanically, but the spec is **not** just a tag table. It carries
|
||||||
|
prose explanation per construct, the schema-invariant catalogue,
|
||||||
|
the pitfall list, and the few-shot corpus. None of those can be
|
||||||
|
emitted from the AST shape alone. Hand-curated content + drift
|
||||||
|
test on the structural anchors is the right cost / value point;
|
||||||
|
generator overkill was rejected.
|
||||||
|
|
||||||
|
### What 20f does not address
|
||||||
|
|
||||||
|
Three larger integration paths got named in the discussion but
|
||||||
|
explicitly deferred per "kiss":
|
||||||
|
|
||||||
|
- **Tool-use schemas** — LLM calls `ail_parse` / `ail_check`
|
||||||
|
inside its turn, iterating until check is clean. Reduces
|
||||||
|
convergence from 1–2 rounds to ≈0 for cooperating clients.
|
||||||
|
- **MCP server** — Anthropic Model Context Protocol exposes
|
||||||
|
AILang resources (spec, examples, current module), tools
|
||||||
|
(parse, check, render, prose), prompts (canonical
|
||||||
|
round-trip templates) to any compatible client. Standard,
|
||||||
|
discoverable, vendor-neutral.
|
||||||
|
- **LSP** — editor integration; serves human authors more than
|
||||||
|
the round-trip flow. Bigger lift.
|
||||||
|
|
||||||
|
All three layer additively on the static-prompt path 20f ships.
|
||||||
|
The static prompt remains the lowest-common-denominator fallback
|
||||||
|
that always works without a tool-use-capable client.
|
||||||
|
|
||||||
|
### Test counts
|
||||||
|
|
||||||
|
- ailang-core: +8 (spec drift suite); existing 12 unchanged → 20
|
||||||
|
- ail: existing 70 e2e green after rewriting
|
||||||
|
`merge_prose_prints_framed_prompt` to assert Form-A landmarks
|
||||||
|
and `FORM-A SPECIFICATION` header instead of `ailang/v0`
|
||||||
|
- ail unit: existing 3 rewritten in lockstep
|
||||||
|
- Workspace: all green
|
||||||
|
|
||||||
|
### Family / arc state
|
||||||
|
|
||||||
|
20f closes the prose-roundtrip arc for now. JOURNAL queue is
|
||||||
|
empty again. Tidy iter for 20a / b / d / e / f together can wait
|
||||||
|
until the next family closes — the architect drift-review
|
||||||
|
discipline applies as before.
|
||||||
|
|||||||
+95
-91
@@ -2,8 +2,8 @@
|
|||||||
|
|
||||||
## Why
|
## Why
|
||||||
|
|
||||||
The prose surface (`ail prose`, Iter 20a/20b) is a deliberately
|
The prose surface (`ail prose`, Iter 20a / 20b) is a deliberately
|
||||||
**lossy** projection of a `.ail.json` module: it strips `(con T)`
|
**lossy** projection of an `.ail.json` module: it strips `(con T)`
|
||||||
wrappings, drops redundant parentheses, infixes arithmetic, suppresses
|
wrappings, drops redundant parentheses, infixes arithmetic, suppresses
|
||||||
schema rigor that the LLM can re-derive. That makes prose pleasant to
|
schema rigor that the LLM can re-derive. That makes prose pleasant to
|
||||||
read and edit — but it also means there is no syntactic parser that
|
read and edit — but it also means there is no syntactic parser that
|
||||||
@@ -11,10 +11,27 @@ turns edited prose back into a `.ail.json`.
|
|||||||
|
|
||||||
Re-integration of free-text edits therefore requires an **LLM
|
Re-integration of free-text edits therefore requires an **LLM
|
||||||
mediator**: a model that understands both the prose intent and the
|
mediator**: a model that understands both the prose intent and the
|
||||||
load-bearing detail in the original `.ail.json`, and emits a new
|
load-bearing detail in the original module, and emits a new module
|
||||||
`.ail.json` that respects both. This document describes the workflow,
|
that respects both. This document describes the workflow, the prompt
|
||||||
the prompt template `ail merge-prose` composes for that mediator, and
|
template `ail merge-prose` composes for that mediator, and the failure
|
||||||
the failure modes to watch for.
|
modes to watch for.
|
||||||
|
|
||||||
|
## What the LLM produces
|
||||||
|
|
||||||
|
Iter 20f revised a load-bearing piece of this cycle: the LLM emits
|
||||||
|
**Form-A** (an `.ailx` document — the canonical authoring surface
|
||||||
|
fixed by Decision 6), not JSON-AST. JSON-AST is the canonical
|
||||||
|
hashable artefact, but it is not a writing surface — every type
|
||||||
|
reference wraps in `{"k": "con", ...}`, every term in
|
||||||
|
`{"t": "...", ...}`, and a single missing `param_modes` entry is a
|
||||||
|
schema error rather than a parse error with a position.
|
||||||
|
|
||||||
|
Form-A is the form `examples/*.ailx` are written in, the form
|
||||||
|
`ail render` produces, and the form `ail parse` consumes. The full
|
||||||
|
LLM-targeted specification is shipped inside the binary as
|
||||||
|
`ailang_core::FORM_A_SPEC` (sourced from
|
||||||
|
`crates/ailang-core/specs/form_a.md`) and embedded verbatim in every
|
||||||
|
`merge-prose` prompt; the LLM does not need prior AILang exposure.
|
||||||
|
|
||||||
## The cycle
|
## The cycle
|
||||||
|
|
||||||
@@ -22,124 +39,104 @@ the failure modes to watch for.
|
|||||||
1. ail prose foo.ail.json > foo.prose.txt
|
1. ail prose foo.ail.json > foo.prose.txt
|
||||||
2. $EDITOR foo.prose.txt # human edits freely
|
2. $EDITOR foo.prose.txt # human edits freely
|
||||||
3. ail merge-prose foo.ail.json foo.prose.txt > prompt.txt
|
3. ail merge-prose foo.ail.json foo.prose.txt > prompt.txt
|
||||||
4. cat prompt.txt | <your-llm-cli> > foo.new.ail.json
|
4. cat prompt.txt | <your-llm-cli> > foo.new.ailx
|
||||||
5. ail check foo.new.ail.json
|
5. ail parse foo.new.ailx > foo.new.ail.json
|
||||||
6. mv foo.new.ail.json foo.ail.json # if check is clean
|
6. ail check foo.new.ail.json
|
||||||
|
7. mv foo.new.ail.json foo.ail.json # if check is clean
|
||||||
```
|
```
|
||||||
|
|
||||||
Step 1 is the deterministic projection (Iter 20a/20b).
|
Step 1 is the deterministic projection (Iter 20a / 20b).
|
||||||
Step 3 is the prompt composer this iter ships.
|
Step 3 is the prompt composer this iter ships. The prompt embeds the
|
||||||
|
Form-A spec, the original module rendered as Form-A, and the edited
|
||||||
|
prose. The original module is loaded via `ailang_core::load_module`
|
||||||
|
(which validates the schema) and rendered via
|
||||||
|
`ailang_surface::print`.
|
||||||
Step 4 is the user's external LLM client — Claude Code, the
|
Step 4 is the user's external LLM client — Claude Code, the
|
||||||
Anthropic API, OpenAI's CLI, anything that takes a prompt on stdin and
|
Anthropic API, OpenAI's CLI, anything that takes a prompt on stdin and
|
||||||
emits text on stdout. AILang ships no client of its own; see *Why no
|
emits text on stdout. AILang ships no client of its own; see *Why no
|
||||||
built-in API client* below.
|
built-in API client* below.
|
||||||
Steps 5 and 6 reuse existing tooling: `ail check` validates schema +
|
Step 5 parses the LLM's Form-A back into a JSON-AST. Parser errors
|
||||||
typechecks, then the user accepts the new module.
|
are positional and can be fed back to the LLM in a follow-up prompt.
|
||||||
|
Step 6 typechecks. The full diagnostic catalogue applies — mode
|
||||||
|
violations, exhaustiveness, effect closure, etc.
|
||||||
|
Step 7 accepts the new module if check is clean.
|
||||||
|
|
||||||
## The prompt template
|
## The prompt template
|
||||||
|
|
||||||
`ail merge-prose <original.ail.json> <edited.prose.txt>` reads both
|
`ail merge-prose <original.ail.json> <edited.prose.txt>` reads the
|
||||||
files and prints the following text to stdout. Nothing more, nothing
|
original (parsing it, then re-rendering as Form-A), reads the prose
|
||||||
less — no fences, no JSON envelope. The shape is exactly what a human
|
file byte-for-byte, and prints the following structure to stdout —
|
||||||
would compose by hand if they wanted to drive the same cycle without
|
no fences, no JSON envelope. The shape is exactly what a human would
|
||||||
the CLI helper.
|
compose by hand if they wanted to drive the same cycle without the
|
||||||
|
CLI helper.
|
||||||
|
|
||||||
```
|
```
|
||||||
You are integrating prose edits back into an AILang module.
|
You are integrating prose edits back into an AILang module.
|
||||||
|
|
||||||
ROLE
|
ROLE
|
||||||
Your job is to produce an updated AILang JSON-AST (.ail.json) that
|
Your job is to produce an updated AILang module in Form-A (an .ailx
|
||||||
reflects the human's prose edits while preserving the load-bearing
|
file) that reflects the human's prose edits while preserving the
|
||||||
semantic detail from the original .ail.json.
|
load-bearing semantic detail from the original module.
|
||||||
|
|
||||||
CONTRACT
|
CONTRACT
|
||||||
The prose is the source of intent: the human edited it to express
|
The prose is the source of intent ... [list of preservation rules]
|
||||||
what the program should now do. The original .ail.json carries
|
|
||||||
load-bearing detail that the prose surface elides — preserve those
|
|
||||||
details unless the prose explicitly contradicts them. Specifically:
|
|
||||||
|
|
||||||
- Mode annotations on fn parameters (`own T`, `borrow T`).
|
|
||||||
These are hard contracts (memory model). The prose shows them,
|
|
||||||
but if the prose is ambiguous, default to the original.
|
|
||||||
- Effect annotations on return types (`with IO`, `with Diverge`).
|
|
||||||
Prose shows these too, but again: if uncertain, keep what the
|
|
||||||
original had.
|
|
||||||
- `tail` flags on calls. The prose prints `tail f(x)`; if the
|
|
||||||
edit moved a call, decide whether the new position is still in
|
|
||||||
tail position and flag accordingly.
|
|
||||||
- Doc strings (`///` lines).
|
|
||||||
- Type annotations on signatures and lambdas.
|
|
||||||
- Constructor names and arities (the prose `Cons(h, t)` must
|
|
||||||
round-trip to a `Term::Ctor` with the right `type` field).
|
|
||||||
|
|
||||||
OUTPUT
|
OUTPUT
|
||||||
Output ONLY the new .ail.json bytes. No commentary, no markdown
|
Output ONLY the new Form-A bytes. ... [no fences, no commentary]
|
||||||
fences, no preamble or postscript. The output must be valid JSON
|
|
||||||
parsable by `ail parse` (i.e. by `serde_json` against the
|
|
||||||
`ailang/v0` schema). The first byte should be `{` and the last
|
|
||||||
non-whitespace byte should be `}`.
|
|
||||||
|
|
||||||
SCHEMA ESSENTIALS
|
FORM-A SPECIFICATION
|
||||||
A full reference lives in docs/DESIGN.md ("Data model (MVP)"). The
|
<<<FORM_A_SPEC
|
||||||
shape is:
|
[ailang_core::FORM_A_SPEC, verbatim]
|
||||||
|
FORM_A_SPEC
|
||||||
|
|
||||||
- Module: { "schema": "ailang/v0", "name": ..., "imports": [...],
|
ORIGINAL MODULE (Form-A)
|
||||||
"defs": [...] }
|
<<<ORIGINAL_FORM_A
|
||||||
- Defs are tagged via `kind` ("fn" | "type" | "const").
|
[ailang_surface::print(&original_module)]
|
||||||
- Types are tagged via `k` ("con" | "fn" | "var" | "forall").
|
ORIGINAL_FORM_A
|
||||||
- Terms are tagged via `t` ("lit" | "var" | "app" | "let" | "if"
|
|
||||||
| "do" | "ctor" | "match" | "lam" | "seq").
|
|
||||||
- Patterns are tagged via `p` ("var" | "lit" | "ctor" | "wild").
|
|
||||||
- On `fn-type`: `param_modes` (one of "own"/"borrow" per
|
|
||||||
parameter) and `effects` are mandatory. `ret_mode` is mandatory
|
|
||||||
when the return type carries a mode.
|
|
||||||
- Constructor application uses `Term::Ctor` (`"t": "ctor"`,
|
|
||||||
fields `type` + `ctor` + `args`), NOT `Term::App`. The prose
|
|
||||||
surface elides the `type` tag (`Cons(h, t)` instead of
|
|
||||||
`(term-ctor IntList Cons h t)`) — re-introduce it.
|
|
||||||
- Base type names that appear bare in prose (`Int`, `Bool`,
|
|
||||||
`Unit`, user types like `IntList`) must be wrapped as
|
|
||||||
`{"k": "con", "name": "Int"}` etc. in the JSON.
|
|
||||||
|
|
||||||
ORIGINAL .ail.json
|
|
||||||
<<<ORIGINAL_AIL_JSON
|
|
||||||
{original_ail_json_here}
|
|
||||||
ORIGINAL_AIL_JSON
|
|
||||||
|
|
||||||
EDITED PROSE
|
EDITED PROSE
|
||||||
<<<EDITED_PROSE
|
<<<EDITED_PROSE
|
||||||
{edited_prose_here}
|
[edited prose, verbatim]
|
||||||
EDITED_PROSE
|
EDITED_PROSE
|
||||||
|
|
||||||
Emit the updated .ail.json now.
|
Emit the updated Form-A module now.
|
||||||
```
|
```
|
||||||
|
|
||||||
The two payloads (original JSON, edited prose) are inserted verbatim
|
The three payloads (spec, original Form-A, edited prose) are inserted
|
||||||
between the heredoc-style markers. `merge-prose` does not strip,
|
between heredoc-style markers. `merge-prose` does not strip,
|
||||||
re-encode, or otherwise transform either input — both go in
|
re-encode, or otherwise transform the prose or the spec. The original
|
||||||
byte-for-byte.
|
is parsed and re-rendered (which is lossless for any module that has
|
||||||
|
been through `ail parse` / `ail render` already; round-trip is a
|
||||||
|
gating contract on the surface crate).
|
||||||
|
|
||||||
## Failure modes
|
## Failure modes
|
||||||
|
|
||||||
The mediator is an LLM, so the cycle is intentionally iterative.
|
The mediator is an LLM, so the cycle is intentionally iterative.
|
||||||
Common failure modes and their fix:
|
Common failure modes and their fix:
|
||||||
|
|
||||||
- **Output wrapped in markdown fences (` ```json ... ``` `).** Strip
|
- **Output wrapped in markdown fences (` ```ailang ... ``` `).**
|
||||||
the fences (`sed -n '/^{/,/^}/p'`) and re-run `ail check`. If the
|
Strip the fences and re-run `ail parse`. If the LLM does this
|
||||||
LLM does this consistently, paste a corrective note ("emit raw
|
consistently, paste a corrective note ("emit raw Form-A, no
|
||||||
JSON, no fences") at the top of the next prompt.
|
fences") at the top of the next prompt.
|
||||||
- **Output contains commentary before/after the JSON.** Same
|
- **Output contains commentary before/after the module.** Same
|
||||||
treatment. Most modern LLMs respect "OUTPUT ONLY" but not all.
|
treatment. Most modern LLMs respect "OUTPUT ONLY" but not all.
|
||||||
- **Invalid JSON / `serde_json` rejects.** Re-run with the parse
|
- **`ail parse` rejects the output.** The parser emits positional
|
||||||
error pasted into the prompt as a corrective note.
|
errors. Re-run with the parse error pasted into the prompt as a
|
||||||
- **Schema-valid but `ail check` fails.** Re-run with the
|
corrective note — "your previous output failed at byte N with
|
||||||
diagnostic messages pasted in. Common cases: missing
|
`expected X, got Y`; fix that and re-emit".
|
||||||
`param_modes`, `Term::App` instead of `Term::Ctor`, bare type
|
- **Parse-clean but `ail check` fails.** Re-run with the
|
||||||
names instead of `{"k":"con","name":"…"}`.
|
diagnostic messages pasted in. Common cases on first-time LLM
|
||||||
- **Preserved detail dropped (mode flipped, doc string lost).**
|
use: missing mode annotation on a `(fn ...)` def
|
||||||
Re-run with a corrective note naming the missing detail.
|
(`mode-required-on-fn-param`), `(app)` used where `(term-ctor)`
|
||||||
|
was needed, missing `(effects IO)` on a fn that calls `(do io/...)`.
|
||||||
|
- **Preserved detail dropped (mode flipped, doc string lost,
|
||||||
|
suppress clause stripped).** Re-run with a corrective note
|
||||||
|
naming the missing detail. The contract section calls these out
|
||||||
|
explicitly, but a long edit may push the LLM to re-derive
|
||||||
|
rather than preserve.
|
||||||
|
|
||||||
The cycle converges in 1–3 rounds for typical edits.
|
The cycle converges in 1–2 rounds for typical edits with a
|
||||||
|
modern frontier model.
|
||||||
|
|
||||||
## Why no built-in API client
|
## Why no built-in API client
|
||||||
|
|
||||||
@@ -149,5 +146,12 @@ streaming semantics, error mapping, version tracking — all carrying
|
|||||||
zero language-level value. The user already has Claude Code, the
|
zero language-level value. The user already has Claude Code, the
|
||||||
Anthropic SDK, the OpenAI CLI, `curl`, or any other client they
|
Anthropic SDK, the OpenAI CLI, `curl`, or any other client they
|
||||||
prefer; `ail merge-prose` composes the prompt and gets out of the
|
prefer; `ail merge-prose` composes the prompt and gets out of the
|
||||||
way. The Unix-pipe shape (`ail merge-prose ... | client | ail check`)
|
way. The Unix-pipe shape (`ail merge-prose ... | client | ail parse |
|
||||||
also makes the cycle scriptable without lock-in to one vendor.
|
ail check`) makes the cycle scriptable without lock-in to one vendor.
|
||||||
|
|
||||||
|
A future iter may layer a tool-use schema (LLM calls back into
|
||||||
|
`ail parse` / `ail check` from inside its turn) or an MCP server
|
||||||
|
(any MCP-compatible client discovers AILang's resources, tools, and
|
||||||
|
prompts) on top of this cycle. Both are additive — the static-prompt
|
||||||
|
fallback documented here remains the lowest-common-denominator path
|
||||||
|
that always works.
|
||||||
|
|||||||
Reference in New Issue
Block a user