iter form-a.0: prelude pilot — examples/prelude.ail rendered

First iteration of the form-a-default-authoring milestone. Mechanical:
one `ail render examples/prelude.ail.json > examples/prelude.ail`
captures the canonical Form-A projection (116 lines / 6386 bytes).
No source-code edits, no test edits.

The two auto-discovering roundtrip tests in
crates/ailang-surface/tests/round_trip.rs pick up the new fixture
via read_dir without test changes and both pass:
- every_ail_fixture_matches_its_json_counterpart — the .ail parses
  to canonical bytes byte-equal to prelude.ail.json (gate test).
- parse_then_print_then_parse_is_idempotent_on_every_ail_fixture —
  the Form-A printer is idempotent over prelude.

cargo test --workspace green at 558 tests (identical to pre-iter
baseline; audit-24 / iter-24.tidy lineage).

prelude.ail.json retained per spec §A2 — this is the singular
dual-form iter; iter 1 deletes it alongside the bulk test-infra
refactor.

Zero re-loops, zero review-phase repairs. Recon predictions matched
reality exactly (116 lines, 6386 bytes, `(module prelude` header,
558-test baseline). Strong signal that the iter-1+ bulk migration
mechanism is sound.
This commit is contained in:
2026-05-13 09:59:30 +02:00
parent 4c2a3c5d08
commit aabcadca5f
4 changed files with 204 additions and 0 deletions
+116
View File
@@ -0,0 +1,116 @@
(module prelude
(data Ordering
(doc "Result of a three-way comparison: LT (less than), EQ (equal), GT (greater than). Ships in milestone 23 as the codomain of Ord.compare.")
(ctor LT)
(ctor EQ)
(ctor GT))
(class Eq
(param a)
(doc "Structural equality. Ships in milestone 23 alongside Ord. The primitive `==` operator stays as the surface-level comparator this iter; routing `==` through `Eq.eq` is the declared P2 follow-up (see docs/specs/2026-05-10-23-eq-ord-prelude.md, `Out of scope`).")
(method eq
(type (fn-type (params (borrow a) (borrow a)) (ret (con Bool))))))
(instance
(class Eq)
(type (con Int))
(doc "Eq Int. Body lowers to `icmp eq i64` via the existing primitive `==` dispatch in `lower_eq`.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
(instance
(class Eq)
(type (con Bool))
(doc "Eq Bool. Body lowers to `icmp eq i1` via the existing primitive `==` dispatch in `lower_eq`.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
(instance
(class Eq)
(type (con Str))
(doc "Eq Str. The lambda body shape mirrors Int/Bool for round-trip stability, but the codegen intercept in `emit_fn` overrides the body to call `@ail_str_eq` directly — see `try_emit_primitive_instance_body` in `crates/ailang-codegen/src/lib.rs`.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (body (app == x y))))))
(class Ord
(param a)
(superclass (class Eq) (type a))
(doc "Total ordering. Ships in milestone 23 alongside Eq. `compare x y` returns LT, EQ, or GT (the three-ctor Ordering ADT also in the prelude). Decision 11's single-superclass closure requires `instance Eq T` for every `instance Ord T` — the three Ord instances below pair with the three Eq instances shipped in iter 23.2.3.")
(method compare
(type (fn-type (params (borrow a) (borrow a)) (ret (con Ordering))))))
(instance
(class Ord)
(type (con Int))
(doc "Ord Int. The lambda body shape is a placeholder for round-trip stability; the codegen intercept `try_emit_primitive_instance_body::\"compare__Int\"` emits a three-way `icmp slt` / `icmp eq` branch ladder constructing LT / EQ / GT.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (body (term-ctor Ordering EQ))))))
(instance
(class Ord)
(type (con Bool))
(doc "Ord Bool. Body lowered via `try_emit_primitive_instance_body::\"compare__Bool\"` — `icmp ult i1` LT-test, `icmp eq i1` EQ-test, GT default.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (body (term-ctor Ordering EQ))))))
(instance
(class Ord)
(type (con Str))
(doc "Ord Str. Body lowered via `try_emit_primitive_instance_body::\"compare__Str\"` — `call i32 @ail_str_compare(ptr, ptr)` then branch on slt-0 / eq-0 against the normalised {-1, 0, +1} return.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (body (term-ctor Ordering EQ))))))
(class Show
(param a)
(doc "Producer of a human-readable Str representation. Ships in milestone 24 with primitive instances for Int/Bool/Str/Float; user types declare their own instance.")
(method show
(type (fn-type (params (borrow a)) (ret (con Str))))))
(instance
(class Show)
(type (con Int))
(method show
(body (lam (params (typed x (con Int))) (ret (con Str)) (body (app int_to_str x))))))
(instance
(class Show)
(type (con Bool))
(method show
(body (lam (params (typed x (con Bool))) (ret (con Str)) (body (app bool_to_str x))))))
(instance
(class Show)
(type (con Str))
(method show
(body (lam (params (typed x (con Str))) (ret (con Str)) (body (app str_clone x))))))
(instance
(class Show)
(type (con Float))
(method show
(body (lam (params (typed x (con Float))) (ret (con Str)) (body (app float_to_str x))))))
(fn ne
(doc "Polymorphic disequality. `ne x y` ≡ not (eq x y). Ships in milestone 23 as the Eq-class free helper.")
(type (forall (vars a) (constraints (constraint Eq a)) (fn-type (params (borrow a) (borrow a)) (ret (con Bool)))))
(params x y)
(body (app not (app eq x y))))
(fn lt
(doc "Polymorphic strict-less-than. `lt x y` ≡ case compare x y of LT -> True; _ -> False. Ships in milestone 23 as the Ord-class free helper.")
(type (forall (vars a) (constraints (constraint Ord a)) (fn-type (params (borrow a) (borrow a)) (ret (con Bool)))))
(params x y)
(body (match (app compare x y)
(case (pat-ctor LT) true)
(case _ false))))
(fn le
(doc "Polymorphic less-than-or-equal. `le x y` ≡ case compare x y of GT -> False; _ -> True. Ships in milestone 23 as the Ord-class free helper.")
(type (forall (vars a) (constraints (constraint Ord a)) (fn-type (params (borrow a) (borrow a)) (ret (con Bool)))))
(params x y)
(body (match (app compare x y)
(case (pat-ctor GT) false)
(case _ true))))
(fn gt
(doc "Polymorphic strict-greater-than. `gt x y` ≡ case compare x y of GT -> True; _ -> False. Ships in milestone 23 as the Ord-class free helper.")
(type (forall (vars a) (constraints (constraint Ord a)) (fn-type (params (borrow a) (borrow a)) (ret (con Bool)))))
(params x y)
(body (match (app compare x y)
(case (pat-ctor GT) true)
(case _ false))))
(fn ge
(doc "Polymorphic greater-than-or-equal. `ge x y` ≡ case compare x y of LT -> False; _ -> True. Ships in milestone 23 as the Ord-class free helper.")
(type (forall (vars a) (constraints (constraint Ord a)) (fn-type (params (borrow a) (borrow a)) (ret (con Bool)))))
(params x y)
(body (match (app compare x y)
(case (pat-ctor LT) false)
(case _ true))))
(fn print
(doc "Polymorphic console-print helper. `print x` ≡ `do io/print_str (show x)` with an explicit let-binder around `show x` for heap-Str RC discipline per eob.1 Str carve-out. Ships in milestone 24 as the second half of the Show prelude.")
(type (forall (vars a) (constraints (constraint Show a)) (fn-type (params (borrow a)) (ret (con Unit)) (effects IO))))
(params x)
(body (let s (app show x) (do io/print_str s)))))