Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity
Files
f7f4c3b2377a701e86fab373237b53c39b968cb7
AILang/examples/prelude.ail
T
Brummel 6ccc756c0f audit + close: intrinsic-bodies — honest prelude docs + lockstep table + stale-model fix (refs #9) 
Milestone close for intrinsic-bodies (.1 mechanism 52ff873 + .2
migration/lock caa3618). Architect drift review over c42034b^..caa3618
plus the regression scripts. Both gates assessed; four drift items
resolved (3 fixed inline here, 1 filed to backlog).

Regression: both scripts exit 0.
  bench/check.py        → 34 metrics, 0 regressed, 2 improved beyond
                          tolerance (bench_hof_pipeline.bump_s -10.76%,
                          bench_list_sum_explicit.bump_s -12.27%), 32 stable.
  bench/compile_check.py → 24 metrics, 0 regressed, 24 stable.
  The milestone is behaviour-preserving; the two throughput improvements
  are noise within the bench's run-to-run band, not a milestone effect.

Drift items (architect):

1. [FIXED] examples/prelude.ail — the 13 migrated defs' doc strings
   still said "Body is placeholder for round-trip stability" and named
   `try_emit_primitive_instance_body` (the pre-raw-buf.1 dispatch fn).
   Post-migration the body IS an honest (intrinsic) marker, not a
   placeholder, and dispatch is `intercepts::lookup`. The docs lied
   about the very artefact the milestone exists to de-lie — an active
   honesty-rule infraction on main. Rewritten to present-tense
   "compiler-supplied (intrinsic) body; codegen emits <IR> via the
   intercept registry" across all 13 (7 Eq/Ord instance methods +
   6 float_* fns).

2. [FIXED] design/models/0007-kernel-extensions.md — claimed the
   `try_emit_primitive_instance_body` hardcoded list is "not yet
   migrated into a plugin registry ... deferred to the Series
   milestone". Stale since raw-buf.1 (the registry shipped) and
   intrinsic-bodies (the (intrinsic) marker + bijection pin). Rewritten
   to the present state: the registry exists, (intrinsic) declares
   membership, the bijection pin locks marker<->entry, and the
   optimisation-only class is named.

3. [FIXED] CLAUDE.md "Lockstep-invariant pairs" — added the third pair:
   INTERCEPTS entries <-> (intrinsic) markers, guarded by
   intercepts_bijection_with_intrinsic_markers, with the
   optimisation-only allowlist carve-out. Same class as the two existing
   tabled pairs; ships silently broken if one side moves without the
   other.

4. [BACKLOG #41, label idea] INTERCEPTS conflates two concepts —
   intrinsic-backed (compiler-supplied body) vs optimisation-of-a-
   real-body (the 5 *__Int icmp family). The .2 bijection pin contains
   it with a hardcoded OPTIMISATION_ONLY allowlist + a stale-allowlist
   guard; a structural split (an Intercept kind field) is the
   forward direction but is its own focused change, out of scope here.

What holds (architect confirmed): data-model contract matches the
shipped Term::Intrinsic (design_schema_drift gates it); no INDEX row
needed (data-model addition, not a new contract); both existing
lockstep pairs untouched (answer lowers via the ordinary qualified-fn
path, no new lower_app arm; no Pattern::Lit reject); 0007-honesty-rule
correctly needed no edit (general rule, never named the dummies).

RATIFY — baseline move: the prelude module hash pin
(crates/ailang-surface/tests/prelude_module_hash_pin.rs) moves
2ea61ef21ebc1913 -> b1373a2c69e70a3f. Cause: this tidy's 13 doc-string
rewrites (item 1). doc is part of the canonical JSON, so the module
hash shifts; behaviour is unchanged. The 6 mono eq/compare def-hashes
do NOT move (synthesise_mono_fn sets doc: None, so instance-method docs
never reach the synthesised symbol). Full workspace test green
post-rebaseline.

Milestone intrinsic-bodies is closed. It unblocks the raw-buf.2 redo
(the polymorphic kernel-tier fns RawBuf needs now have an honest body
form). raw-buf (#7) remains parked; resuming it is a fresh decision.
2026-05-29 17:56:10 +02:00

154 lines
8.0 KiB
Plaintext
Raw Blame History

(module prelude
(kernel)
(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. The class-method `eq` is the surface-level comparator; `==` as a surface name is not part of the language. Primitive instances Eq Int / Bool / Str / Unit are lowered via try_emit_primitive_instance_body in the codegen.")
(method eq
(type (fn-type (params (borrow a) (borrow a)) (ret (con Bool))))))
(instance
(class Eq)
(type (con Int))
(doc "Eq Int. Compiler-supplied (intrinsic) body; codegen emits `icmp eq i64` with the alwaysinline attribute via the intercept registry.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
(instance
(class Eq)
(type (con Bool))
(doc "Eq Bool. Compiler-supplied (intrinsic) body; codegen emits `icmp eq i1` with the alwaysinline attribute via the intercept registry.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
(instance
(class Eq)
(type (con Str))
(doc "Eq Str. Compiler-supplied (intrinsic) body; codegen emits a call to `@ail_str_eq` with the alwaysinline attribute via the intercept registry.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
(instance
(class Eq)
(type (con Unit))
(doc "Eq Unit. Unit is single-inhabitant so all values compare equal. Compiler-supplied (intrinsic) body; codegen emits `ret i1 1` via the intercept registry.")
(method eq
(body (lam (params (typed x a) (typed y a)) (ret (con Bool)) (intrinsic)))))
(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. Compiler-supplied (intrinsic) body; codegen emits a three-way `icmp slt` / `icmp eq` branch ladder constructing LT / EQ / GT via the intercept registry.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (intrinsic)))))
(instance
(class Ord)
(type (con Bool))
(doc "Ord Bool. Compiler-supplied (intrinsic) body; codegen emits `icmp ult i1` LT-test, `icmp eq i1` EQ-test, GT default, via the intercept registry.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (intrinsic)))))
(instance
(class Ord)
(type (con Str))
(doc "Ord Str. Compiler-supplied (intrinsic) body; codegen emits `call i32 @ail_str_compare(ptr, ptr)` then branches on slt-0 / eq-0 against the normalised {-1, 0, +1} return, via the intercept registry.")
(method compare
(body (lam (params (typed x a) (typed y a)) (ret (con Ordering)) (intrinsic)))))
(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 (own (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))))
(fn float_eq
(doc "IEEE Float equality. `float_eq x y` returns true iff both operands are non-NaN and bit-equal. Compiler-supplied (intrinsic) body; codegen emits `fcmp oeq double` with alwaysinline via the intercept registry. Replaces the milestone-deleted polymorphic `==` on Float.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_ne
(doc "IEEE Float disequality. `float_ne nan nan` returns true (unordered-or-not-equal per IEEE-754). Compiler-supplied (intrinsic) body; codegen emits `fcmp une double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_lt
(doc "IEEE Float strict less-than. `float_lt nan x` returns false for any x (unordered). Compiler-supplied (intrinsic) body; codegen emits `fcmp olt double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_le
(doc "IEEE Float less-than-or-equal. Compiler-supplied (intrinsic) body; codegen emits `fcmp ole double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_gt
(doc "IEEE Float strict greater-than. Compiler-supplied (intrinsic) body; codegen emits `fcmp ogt double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic))
(fn float_ge
(doc "IEEE Float greater-than-or-equal. Compiler-supplied (intrinsic) body; codegen emits `fcmp oge double`.")
(type (fn-type (params (con Float) (con Float)) (ret (con Bool))))
(params x y)
(intrinsic)))
Reference in New Issue View Git Blame Copy Permalink