From 00a1c5f0e73c64bfd1bbcbd1f2696788a3d399f4 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 10 May 2026 15:20:09 +0200 Subject: [PATCH] =?UTF-8?q?plan:=20floats=20iter=203=20=E2=80=94=20typeche?= =?UTF-8?q?ck=20+=20builtins=20(widen=20+=20install=20+=20Pattern::Lit::Fl?= =?UTF-8?q?oat=20reject)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- docs/plans/2026-05-10-floats-3-typecheck.md | 926 ++++++++++++++++++++ 1 file changed, 926 insertions(+) create mode 100644 docs/plans/2026-05-10-floats-3-typecheck.md diff --git a/docs/plans/2026-05-10-floats-3-typecheck.md b/docs/plans/2026-05-10-floats-3-typecheck.md new file mode 100644 index 0000000..bca172f --- /dev/null +++ b/docs/plans/2026-05-10-floats-3-typecheck.md @@ -0,0 +1,926 @@ +# Floats Iteration 3 — Typecheck + Builtins (Implementation Plan) + +> **Parent spec:** `docs/specs/2026-05-10-floats.md` (committed +> `e37366f`, approved 2026-05-10) — section A3 + the +> `crates/ailang-check/` Components subsection. +> +> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement` +> to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Widen the existing arithmetic / comparison builtins +(`+`, `-`, `*`, `/`, `!=`, `<`, `<=`, `>`, `>=`) from monomorphic +`(Int, Int) -> {Int,Bool}` to polymorphic `forall a. (a, a) -> a` +(resp. `forall a. (a, a) -> Bool`), install the new Float builtins +(`neg`, `int_to_float`, `float_to_int_truncate`, `float_to_str`, +`is_nan`), install the three Float constants (`nan`, `inf`, +`neg_inf`) and the `io/print_float` effect op, and hard-reject +`Pattern::Lit { lit: Literal::Float { .. } }` at the typechecker. + +**Architecture:** The widening uses the same +`Type::Forall { vars: ["a"], body: Type::Fn { params: [a, a], ret: +.. } }` shape `==` already has. The check-side install at +`crates/ailang-check/src/builtins.rs::install` and the codegen-side +parallel table at `crates/ailang-codegen/src/synth.rs::builtin_ail_type` +stay in lockstep. The actual {Int, Float} arg-type filtering happens +at codegen (iter 4) — typecheck accepts any matching pair (mirrors +how `==` works today). The `Pattern::Lit::Float` rejection adds a +new `CheckError::FloatPatternNotAllowed` variant; the iter-1 +compile-completeness arm (`Literal::Float { .. } => Type::float()`) +is replaced with an `Err` return. No codegen *lowering* changes — +iter 3 only updates the type metadata the codegen consults. + +**Tech Stack:** `crates/ailang-check/` (`builtins.rs`, `lib.rs`), +`crates/ailang-codegen/` (`synth.rs` — type metadata only). No +runtime, no LLVM IR emission. + +**No-regression invariant:** `cargo test --workspace` must stay +GREEN after EACH task. The widening must not change the resolved +type of any existing Int-only call site — a polymorphic `+` of +type `forall a. (a, a) -> a` instantiated at `(Int, Int)` returns +`Int`, identical to the pre-widening monomorphic shape. End-to-end +Int fixtures (`examples/*.ail.json`) and the codegen `builtin_binop` +Int table stay untouched. + +--- + +## Files this plan creates or modifies + +- Modify: `crates/ailang-check/src/builtins.rs` — widen `install` + arithmetic / comparison entries, add 5 new builtin-fn entries + (`neg`, `int_to_float`, `float_to_int_truncate`, `float_to_str`, + `is_nan`), add 3 new constant entries (`nan`, `inf`, `neg_inf`), + add 1 new effect-op entry (`io/print_float`); refresh `list()` + display strings to match. +- Modify: `crates/ailang-codegen/src/synth.rs` — widen + `builtin_ail_type` arithmetic / comparison entries (lockstep + mirror), add 5 new builtin-fn entries, add 3 new constant entries, + extend `builtin_effect_op_ret` to include `io/print_float`. +- Modify: `crates/ailang-check/src/lib.rs` — add + `CheckError::FloatPatternNotAllowed` variant; replace the + iter-1 `Literal::Float { .. } => Type::float()` arm at line 2312 + with an `Err(CheckError::FloatPatternNotAllowed)` return. +- Modify: `docs/JOURNAL.md` — append iteration-close entry. + +No file outside this list is touched. + +--- + +## Task 1: WIDEN existing arithmetic / comparison builtins to polymorphic + +**Files:** +- Modify: `crates/ailang-check/src/builtins.rs:50-70` (install of + `+`/`-`/`*`/`/`/`%`/`!=`/`<`/`<=`/`>`/`>=`), `:164-183` (list). +- Modify: `crates/ailang-codegen/src/synth.rs:61-114` + (builtin_ail_type, the `+ | - | * | / | %` and `!= | < | <= | > | >=` + arms at lines 77-78). + +- [ ] **Step 1: Write the RED widening test** + +In `crates/ailang-check/src/builtins.rs`, append a `#[cfg(test)] mod +tests` block at the file end (no test mod exists currently per +`grep "^#\[cfg(test)\]\|^mod tests" crates/ailang-check/src/builtins.rs`): + +```rust +#[cfg(test)] +mod tests { + use super::*; + use crate::Env; + use ailang_core::ast::{Literal, Term}; + + /// Synthesize the type of a small expression in a fresh Env that + /// has only the builtins installed (no user defs). Returns the + /// fully-applied result type; effects ignored for this helper. + fn synth_in_builtins_env(t: &Term) -> Type { + let mut env = Env::default(); + install(&mut env); + crate::synth_term(&env, t).expect("synth").0 + } + + fn lit_int(v: i64) -> Term { + Term::Lit { lit: Literal::Int { value: v } } + } + fn lit_float(bits: u64) -> Term { + Term::Lit { lit: Literal::Float { bits } } + } + fn app(callee: &str, args: Vec) -> Term { + Term::App { + callee: Box::new(Term::Var { name: callee.into() }), + args, + tail: false, + } + } + + /// Iter 22-floats.3: regression — `(+ 1 2)` still resolves to + /// `Int` after the widening from `(Int, Int) -> Int` to + /// `forall a. (a, a) -> a`. + #[test] + fn widen_plus_keeps_int_int_int() { + let ty = synth_in_builtins_env(&app("+", vec![lit_int(1), lit_int(2)])); + assert_eq!(ty, Type::int(), "(+ 1 2) must still type as Int"); + } + + /// Iter 22-floats.3: new acceptance — `(+ 1.5 2.5)` types as + /// `Float`. Pre-widening this would have failed with + /// `TypeMismatch`. + #[test] + fn widen_plus_accepts_float_float_float() { + let bits = 1.5_f64.to_bits(); + let ty = synth_in_builtins_env(&app("+", vec![lit_float(bits), lit_float(bits)])); + assert_eq!(ty, Type::float(), "(+ 1.5 2.5) must type as Float"); + } + + /// Iter 22-floats.3: regression — `(< 1 2)` still resolves to + /// `Bool` after the widening to `forall a. (a, a) -> Bool`. + #[test] + fn widen_lt_keeps_int_int_bool() { + let ty = synth_in_builtins_env(&app("<", vec![lit_int(1), lit_int(2)])); + assert_eq!(ty, Type::bool_(), "(< 1 2) must still type as Bool"); + } + + /// Iter 22-floats.3: new acceptance — `(< 1.5 2.5)` types as + /// `Bool`. + #[test] + fn widen_lt_accepts_float_float_bool() { + let bits = 1.5_f64.to_bits(); + let ty = synth_in_builtins_env(&app("<", vec![lit_float(bits), lit_float(bits)])); + assert_eq!(ty, Type::bool_(), "(< 1.5 1.5) must type as Bool"); + } +} +``` + +If `crate::synth_term` is private or has a different signature, use +the lowest-overhead public typecheck entry point — read the top of +`crates/ailang-check/src/lib.rs` to find the right helper. Most +likely `synth_term` is `pub(crate)` and visible to a same-crate +`mod tests`. If not, switch to `crate::check::synth_term` or +construct a minimal `Module` and call `crate::check_module`. + +- [ ] **Step 2: Run tests to verify RED** + +Run: `cargo test -p ailang-check --lib builtins::tests` +Expected: 2 of 4 tests FAIL — `widen_plus_accepts_float_float_float` +and `widen_lt_accepts_float_float_bool` fail with a +`TypeMismatch { expected: "Int", got: "Float" }` panic. The two +regression tests (`widen_plus_keeps_int_int_int`, +`widen_lt_keeps_int_int_bool`) pass. + +- [ ] **Step 3: Widen the check-side install** + +In `crates/ailang-check/src/builtins.rs`, replace the block at +lines 51-70 (the `int_int_int` / `int_int_bool` constructors and +the two `for` loops) with: + +```rust + // Iter 22-floats.3: arithmetic and comparison ops are polymorphic. + // Same shape as `==` below — the {Int, Float}-restriction is + // enforced at codegen, not at typecheck. `%` stays Int-only + // (no fmod yet — see spec section A3). + let poly_a_a_to_a = || Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::Var { name: "a".into() }), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }), + }; + let poly_a_a_to_bool = || Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::bool_()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }), + }; + let int_int_int = Type::Fn { + params: vec![Type::int(), Type::int()], + ret: Box::new(Type::int()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }; + for op in ["+", "-", "*", "/"] { + env.globals.insert(op.into(), poly_a_a_to_a()); + } + env.globals.insert("%".into(), int_int_int); + for op in ["!=", "<", "<=", ">", ">="] { + env.globals.insert(op.into(), poly_a_a_to_bool()); + } +``` + +The `int_int_bool` local is gone (its only consumer, the `!=` / +ordering loop, now uses `poly_a_a_to_bool`). + +- [ ] **Step 4: Widen the codegen-side type table** + +In `crates/ailang-codegen/src/synth.rs`, replace the +`int_int_int` / `int_int_bool` closures and the two arithmetic / +comparison match arms at lines 62-78: + +```rust + // Iter 22-floats.3: same widening as `crates/ailang-check/src/ + // builtins.rs` — `+`/`-`/`*`/`/` and `!=`/`<`/`<=`/`>`/`>=` are + // polymorphic. `%` stays monomorphic-Int. Codegen lowering for + // these ops still goes through `builtin_binop` (Int-only) in + // iter 3; iter 4 converts that to type-dispatched. + let poly_a_a_to_a = || Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::Var { name: "a".into() }), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }), + }; + let poly_a_a_to_bool = || Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::bool_()), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }), + }; + let int_int_int = || Type::Fn { + params: vec![Type::int(), Type::int()], + ret: Box::new(Type::int()), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }; + Some(match name { + "+" | "-" | "*" | "/" => poly_a_a_to_a(), + "%" => int_int_int(), + "!=" | "<" | "<=" | ">" | ">=" => poly_a_a_to_bool(), +``` + +The rest of the match (`==`, `not`, `__unreachable__`, fallback) +stays unchanged. + +- [ ] **Step 5: Refresh `list()` display strings** + +In `crates/ailang-check/src/builtins.rs`, replace lines 165-176 +(the arithmetic / comparison rows in `list()`): + +```rust + vec![ + ("+", "forall a. (a, a) -> a"), + ("-", "forall a. (a, a) -> a"), + ("*", "forall a. (a, a) -> a"), + ("/", "forall a. (a, a) -> a"), + ("%", "(Int, Int) -> Int"), + ("==", "forall a. (a, a) -> Bool"), + ("!=", "forall a. (a, a) -> Bool"), + ("<", "forall a. (a, a) -> Bool"), + ("<=", "forall a. (a, a) -> Bool"), + (">", "forall a. (a, a) -> Bool"), + (">=", "forall a. (a, a) -> Bool"), + ("not", "(Bool) -> Bool"), + ("__unreachable__", "forall a. a"), + ("io/print_int", "(Int) -> Unit !IO [effect op]"), + ("io/print_bool", "(Bool) -> Unit !IO [effect op]"), + ("io/print_str", "(Str) -> Unit !IO [effect op]"), + ] +``` + +- [ ] **Step 6: Verify all four widening tests now GREEN** + +Run: `cargo test -p ailang-check --lib builtins::tests` +Expected: all 4 tests PASS. + +- [ ] **Step 7: Verify no workspace regression** + +Run: `cargo test --workspace` +Expected: 383 passed, 0 failed (matches iter-2-close baseline). +Specifically: every existing `examples/*.ail.json` Int-using +fixture continues to pass — the polymorphic `+` instantiated at +`(Int, Int)` returns `Int`, bit-identical to the pre-widening +shape. Codegen lowering is unchanged (iter 4 widens the +`builtin_binop` table; iter 3 leaves it Int-only). + +- [ ] **Step 8: Commit** + +```bash +git add crates/ailang-check/src/builtins.rs \ + crates/ailang-codegen/src/synth.rs +git commit -m "floats iter 3.1: widen +/-/*/// and !=//>= to polymorphic forall a" +``` + +--- + +## Task 2: INSTALL new Float builtins (`neg`, `int_to_float`, `float_to_int_truncate`, `float_to_str`, `is_nan`) + +**Files:** +- Modify: `crates/ailang-check/src/builtins.rs` — `install` + function and `list` function. +- Modify: `crates/ailang-codegen/src/synth.rs` — + `builtin_ail_type`. + +- [ ] **Step 1: Write the RED test for the five new builtins** + +In `crates/ailang-check/src/builtins.rs::tests`, append: + +```rust +/// Iter 22-floats.3: `neg` is polymorphic — `forall a. (a) -> a`. +/// Both `(neg 5) : Int` and `(neg 1.5) : Float` typecheck. +#[test] +fn install_neg_is_polymorphic() { + let ty_int = synth_in_builtins_env(&app("neg", vec![lit_int(5)])); + assert_eq!(ty_int, Type::int(), "(neg 5) must type as Int"); + let bits = 1.5_f64.to_bits(); + let ty_float = synth_in_builtins_env(&app("neg", vec![lit_float(bits)])); + assert_eq!(ty_float, Type::float(), "(neg 1.5) must type as Float"); +} + +/// Iter 22-floats.3: `int_to_float : (Int) -> Float`. +#[test] +fn install_int_to_float_signature() { + let ty = synth_in_builtins_env(&app("int_to_float", vec![lit_int(5)])); + assert_eq!(ty, Type::float(), "(int_to_float 5) must type as Float"); +} + +/// Iter 22-floats.3: `float_to_int_truncate : (Float) -> Int`. +/// Saturating truncation toward zero per spec A4 — typecheck only +/// cares about the signature here; semantics is iter 4's +/// codegen lowering. +#[test] +fn install_float_to_int_truncate_signature() { + let bits = 1.5_f64.to_bits(); + let ty = synth_in_builtins_env(&app("float_to_int_truncate", vec![lit_float(bits)])); + assert_eq!(ty, Type::int(), "(float_to_int_truncate 1.5) must type as Int"); +} + +/// Iter 22-floats.3: `float_to_str : (Float) -> Str`. +#[test] +fn install_float_to_str_signature() { + let bits = 1.5_f64.to_bits(); + let ty = synth_in_builtins_env(&app("float_to_str", vec![lit_float(bits)])); + assert_eq!(ty, Type::str_(), "(float_to_str 1.5) must type as Str"); +} + +/// Iter 22-floats.3: `is_nan : (Float) -> Bool`. Codegen lowers to +/// `fcmp uno double %x, %x` in iter 4. +#[test] +fn install_is_nan_signature() { + let bits = 1.5_f64.to_bits(); + let ty = synth_in_builtins_env(&app("is_nan", vec![lit_float(bits)])); + assert_eq!(ty, Type::bool_(), "(is_nan 1.5) must type as Bool"); +} +``` + +- [ ] **Step 2: Run tests to verify RED** + +Run: `cargo test -p ailang-check --lib builtins::tests::install` +Expected: 5 tests FAIL with `UnknownIdent` panic (the names are not +yet in `env.globals`). + +- [ ] **Step 3: Add the five new builtins to `install`** + +In `crates/ailang-check/src/builtins.rs::install`, immediately +AFTER the `__unreachable__` insert (line 119) and BEFORE the +`env.effect_ops.insert("io/print_int", ...)` block, add: + +```rust + // Iter 22-floats.3: Float-conversion and inspection builtins. + // Codegen lowering lands in iter 4; iter 3 only registers types. + env.globals.insert("neg".into(), Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![Type::Var { name: "a".into() }], + ret: Box::new(Type::Var { name: "a".into() }), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }), + }); + env.globals.insert("int_to_float".into(), Type::Fn { + params: vec![Type::int()], + ret: Box::new(Type::float()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }); + env.globals.insert("float_to_int_truncate".into(), Type::Fn { + params: vec![Type::float()], + ret: Box::new(Type::int()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }); + env.globals.insert("float_to_str".into(), Type::Fn { + params: vec![Type::float()], + ret: Box::new(Type::str_()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }); + env.globals.insert("is_nan".into(), Type::Fn { + params: vec![Type::float()], + ret: Box::new(Type::bool_()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }); +``` + +- [ ] **Step 4: Add the same five entries to `synth.rs::builtin_ail_type`** + +In `crates/ailang-codegen/src/synth.rs::builtin_ail_type`, immediately +AFTER the `__unreachable__` arm (line 107-111) and BEFORE the +`_ => return None,` fallback, add: + +```rust + // Iter 22-floats.3: Float-conversion and inspection builtins. + // Same lockstep with `crates/ailang-check/src/builtins.rs`. + "neg" => Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![Type::Var { name: "a".into() }], + ret: Box::new(Type::Var { name: "a".into() }), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }), + }, + "int_to_float" => Type::Fn { + params: vec![Type::int()], + ret: Box::new(Type::float()), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }, + "float_to_int_truncate" => Type::Fn { + params: vec![Type::float()], + ret: Box::new(Type::int()), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }, + "float_to_str" => Type::Fn { + params: vec![Type::float()], + ret: Box::new(Type::str_()), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }, + "is_nan" => Type::Fn { + params: vec![Type::float()], + ret: Box::new(Type::bool_()), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }, +``` + +- [ ] **Step 5: Add the five entries to `list()`** + +In `crates/ailang-check/src/builtins.rs::list()`, append the five +new rows immediately after the `__unreachable__` row and before +the effect-op rows (around line 178): + +```rust + ("__unreachable__", "forall a. a"), + ("neg", "forall a. (a) -> a"), + ("int_to_float", "(Int) -> Float"), + ("float_to_int_truncate", "(Float) -> Int"), + ("float_to_str", "(Float) -> Str"), + ("is_nan", "(Float) -> Bool"), + ("io/print_int", "(Int) -> Unit !IO [effect op]"), +``` + +- [ ] **Step 6: Verify the RED tests now GREEN** + +Run: `cargo test -p ailang-check --lib builtins::tests::install` +Expected: all 5 PASS. + +- [ ] **Step 7: Verify no workspace regression** + +Run: `cargo test --workspace` +Expected: 383+ tests passed, 0 failed. + +- [ ] **Step 8: Commit** + +```bash +git add crates/ailang-check/src/builtins.rs \ + crates/ailang-codegen/src/synth.rs +git commit -m "floats iter 3.2: install neg/int_to_float/float_to_int_truncate/float_to_str/is_nan" +``` + +--- + +## Task 3: INSTALL new constants (`nan`, `inf`, `neg_inf`) + new effect op (`io/print_float`) + +**Files:** +- Modify: `crates/ailang-check/src/builtins.rs` — `install` + function (constants + effect op) and `list` function. +- Modify: `crates/ailang-codegen/src/synth.rs` — + `builtin_ail_type` (constants), `builtin_effect_op_ret` + (effect op). + +- [ ] **Step 1: Write the RED test for constants and effect op** + +In `crates/ailang-check/src/builtins.rs::tests`, append: + +```rust +/// Iter 22-floats.3: `nan`, `inf`, `neg_inf` are bare-value +/// constants of type `Float`. They are NOT functions — reference +/// site is `(var nan)`, not `(app nan)`. Parallel to +/// `__unreachable__` which is `forall a. a`. +#[test] +fn install_float_constants() { + let ty_nan = synth_in_builtins_env(&Term::Var { name: "nan".into() }); + assert_eq!(ty_nan, Type::float(), "nan must type as Float"); + let ty_inf = synth_in_builtins_env(&Term::Var { name: "inf".into() }); + assert_eq!(ty_inf, Type::float(), "inf must type as Float"); + let ty_neg_inf = synth_in_builtins_env(&Term::Var { name: "neg_inf".into() }); + assert_eq!(ty_neg_inf, Type::float(), "neg_inf must type as Float"); +} + +/// Iter 22-floats.3: `io/print_float : (Float) -> Unit !IO`. +/// Codegen lowering parallels `io/print_int` in iter 4. +#[test] +fn install_io_print_float_signature() { + let bits = 1.5_f64.to_bits(); + let mut env = Env::default(); + install(&mut env); + let do_term = Term::Do { + op: "io/print_float".into(), + args: vec![lit_float(bits)], + tail: false, + }; + let (ret, effects) = crate::synth_term(&env, &do_term).expect("synth"); + assert_eq!(ret, Type::unit(), "io/print_float returns Unit"); + assert!( + effects.iter().any(|e| e == "IO"), + "io/print_float must accumulate IO effect, got {effects:?}" + ); +} +``` + +If `crate::synth_term`'s second return value (effect set) has a +different type than `Vec`, adjust the assertion accordingly +— read the function's signature at the top of `lib.rs`. + +- [ ] **Step 2: Run tests to verify RED** + +Run: `cargo test -p ailang-check --lib builtins::tests::install_float_constants builtins::tests::install_io_print_float_signature` +Expected: both FAIL — `install_float_constants` with +`UnknownIdent("nan")`; `install_io_print_float_signature` with +`UnknownEffectOp("io/print_float")`. + +- [ ] **Step 3: Install the three constants** + +In `crates/ailang-check/src/builtins.rs::install`, immediately +AFTER the five new builtin inserts from Task 2 and BEFORE the +`env.effect_ops.insert("io/print_int", ...)` block, add: + +```rust + // Iter 22-floats.3: Float bit-pattern constants. Bare values, + // not fns — reference site is `(var nan)`. Codegen emits + // `double 0x7FF8000000000000` etc. at the use site in iter 4. + // Parallel to `__unreachable__` but typed as concrete `Float` + // rather than the polymorphic bottom. + env.globals.insert("nan".into(), Type::float()); + env.globals.insert("inf".into(), Type::float()); + env.globals.insert("neg_inf".into(), Type::float()); +``` + +- [ ] **Step 4: Install the effect op** + +In `crates/ailang-check/src/builtins.rs::install`, after the existing +`env.effect_ops.insert("io/print_str", …)` block (line 137-144) and +before the closing `}` of `install`, add: + +```rust + // Iter 22-floats.3: parallel to io/print_int|bool|str. Codegen + // lowers via runtime C glue `@ail_print_float` in iter 4. + env.effect_ops.insert( + "io/print_float".into(), + EffectOpSig { + effect: "IO".into(), + params: vec![Type::float()], + ret: Type::unit(), + }, + ); +``` + +- [ ] **Step 5: Add the constants to `synth.rs::builtin_ail_type`** + +In `crates/ailang-codegen/src/synth.rs::builtin_ail_type`, +immediately after the five Task-2 entries (`is_nan` arm) and +BEFORE the `_ => return None,` fallback, add: + +```rust + "nan" | "inf" | "neg_inf" => Type::float(), +``` + +- [ ] **Step 6: Add `io/print_float` to `builtin_effect_op_ret`** + +In `crates/ailang-codegen/src/synth.rs::builtin_effect_op_ret` at +line 118-122, replace the match body: + +```rust +pub(crate) fn builtin_effect_op_ret(op: &str) -> Option { + Some(match op { + "io/print_int" | "io/print_bool" | "io/print_str" | "io/print_float" => Type::unit(), + _ => return None, + }) +} +``` + +- [ ] **Step 7: Add the four entries to `list()`** + +In `crates/ailang-check/src/builtins.rs::list()`, immediately after +the five Task-2 rows and before the existing effect-op rows, add: + +```rust + ("is_nan", "(Float) -> Bool"), + ("nan", "Float"), + ("inf", "Float"), + ("neg_inf", "Float"), + ("io/print_int", "(Int) -> Unit !IO [effect op]"), + ("io/print_bool", "(Bool) -> Unit !IO [effect op]"), + ("io/print_str", "(Str) -> Unit !IO [effect op]"), + ("io/print_float", "(Float) -> Unit !IO [effect op]"), +``` + +(The `is_nan` row is kept unchanged from Task 2; the four new rows +are `nan`, `inf`, `neg_inf`, `io/print_float`.) + +- [ ] **Step 8: Verify the RED tests now GREEN** + +Run: `cargo test -p ailang-check --lib builtins::tests` +Expected: all builtins-tests PASS (4 widen + 5 install + 2 +constants/effect-op = 11 tests). + +- [ ] **Step 9: Verify no workspace regression** + +Run: `cargo test --workspace` +Expected: 383+ tests passed, 0 failed. + +- [ ] **Step 10: Commit** + +```bash +git add crates/ailang-check/src/builtins.rs \ + crates/ailang-codegen/src/synth.rs +git commit -m "floats iter 3.3: install Float constants nan/inf/neg_inf + io/print_float effect op" +``` + +--- + +## Task 4: REJECT `Pattern::Lit { lit: Literal::Float { .. } }` at typecheck + +**Files:** +- Modify: `crates/ailang-check/src/lib.rs` — + `CheckError` enum (add new variant), Pattern::Lit typecheck arm + at line 2306-2316. + +- [ ] **Step 1: Write the RED test for Float-pattern rejection** + +In `crates/ailang-check/src/builtins.rs::tests`, append a NEW test +(uses the same `synth_in_builtins_env` helper): + +```rust +/// Iter 22-floats.3: pattern-matching on Float literals is hard- +/// rejected at typecheck per spec line 723-735 recommendation (a). +/// IEEE-`==` semantics make Float patterns semantically dubious +/// (NaN never matches; equality is bit-exact not approximate). +/// Surface lex / parser accept the syntax (iter 2); typecheck +/// surfaces the error here. +#[test] +fn reject_float_pattern_in_match() { + use ailang_core::ast::{Arm, Pattern}; + let bits = 1.5_f64.to_bits(); + let scrut = lit_float(bits); + let arm = Arm { + pat: Pattern::Lit { lit: Literal::Float { bits } }, + body: lit_int(0), + }; + let term = Term::Match { + scrutinee: Box::new(scrut), + arms: vec![arm], + }; + let mut env = Env::default(); + install(&mut env); + let err = crate::synth_term(&env, &term).expect_err("must reject"); + assert!( + matches!(err, crate::CheckError::FloatPatternNotAllowed), + "expected FloatPatternNotAllowed, got {err:?}" + ); +} +``` + +If `Arm` has different fields (e.g. additional `guard`, `binding`), +read the AST `Arm` struct in `crates/ailang-core/src/ast.rs` and +adjust accordingly. + +- [ ] **Step 2: Run test to verify RED** + +Run: `cargo test -p ailang-check --lib builtins::tests::reject_float_pattern_in_match` +Expected: FAIL — currently the iter-1 arm `Literal::Float { .. } +=> Type::float()` makes the typecheck succeed, so `synth_term` +returns `Ok(...)`, the `expect_err` panics with "must reject". + +- [ ] **Step 3: Add `CheckError::FloatPatternNotAllowed` variant** + +In `crates/ailang-check/src/lib.rs`, in the `pub enum CheckError` +block (around lines 273-420), add a new variant immediately AFTER +`PrimitiveNeedsWildcard` (line 371): + +```rust + /// A `Pattern::Lit` matched against a `Literal::Float`. Float + /// patterns are semantically dubious (NaN never matches via + /// IEEE-`==`; equality is bit-exact not approximate), so the + /// typechecker hard-rejects them. The surface lex / parser + /// accept the syntax (iter 2); this diagnostic surfaces at + /// typecheck time. Code: `float-pattern-not-allowed`. + #[error("float-literal patterns are not allowed: use ordering operators (`<`, `>`, ...) and `is_nan` to discriminate floats")] + FloatPatternNotAllowed, +``` + +- [ ] **Step 4: Replace the iter-1 arm in `Pattern::Lit` typecheck** + +In `crates/ailang-check/src/lib.rs`, at lines 2306-2316, replace the +`Pattern::Lit { lit }` block: + +```rust + Pattern::Lit { lit } => { + let lt = match lit { + Literal::Int { .. } => Type::int(), + Literal::Bool { .. } => Type::bool_(), + Literal::Str { .. } => Type::str_(), + Literal::Unit => Type::unit(), + Literal::Float { .. } => { + return Err(CheckError::FloatPatternNotAllowed); + } + }; + expect_eq(expected, <)?; + Ok(vec![]) + } +``` + +The `match` no longer needs the Float arm to compute `lt` because +the `Float` case takes the early-return path before `lt` is used. + +- [ ] **Step 5: Verify RED test now GREEN** + +Run: `cargo test -p ailang-check --lib builtins::tests::reject_float_pattern_in_match` +Expected: PASS. + +- [ ] **Step 6: Verify no workspace regression** + +Run: `cargo test --workspace` +Expected: 383+ tests passed, 0 failed. The new `CheckError` +variant is purely additive — no diagnostic-code uniqueness check +or test enumerates the variants exhaustively beyond the +`#[derive(thiserror::Error)]` machinery. + +- [ ] **Step 7: Commit** + +```bash +git add crates/ailang-check/src/lib.rs +git commit -m "floats iter 3.4: typecheck rejects Pattern::Lit Float with FloatPatternNotAllowed" +``` + +--- + +## Task 5: Iteration close — JOURNAL entry + +**Files:** +- Modify: `docs/JOURNAL.md` — append entry at file end. + +- [ ] **Step 1: Append the iteration-close entry** + +In `docs/JOURNAL.md`, append a new section at the end of the file +(use the orchestrator-authored template; substitute the actual +per-task commit SHAs): + +```markdown +## 2026-05-10 — Iteration Floats.3: typecheck + builtins + +Widened the existing arithmetic and comparison builtins (`+`, `-`, +`*`, `/`, `!=`, `<`, `<=`, `>`, `>=`) from monomorphic +`(Int, Int) -> {Int,Bool}` to polymorphic `forall a. (a, a) -> a` +(resp. `... -> Bool`). Same shape `==` already had since iter 16e. +The `{Int, Float}` filter is enforced at codegen (iter 4); typecheck +accepts any matching pair, mirroring how `==` works today. `%` stays +monomorphic-Int (no fmod yet — spec section A3). The widening is +type-side only; codegen lowering for `+` etc. continues to use the +monomorphic-Int `synth::builtin_binop` table (iter 4 converts that to +type-dispatched). The lockstep partner table at +`crates/ailang-codegen/src/synth.rs::builtin_ail_type` was widened in +the same commit so no codegen call site sees an out-of-date polymorphic +shape. + +Five new Float builtins installed: `neg : forall a. (a) -> a` +(polymorphic; parallel to widened `+`), `int_to_float : (Int) -> +Float`, `float_to_int_truncate : (Float) -> Int`, `float_to_str : +(Float) -> Str`, `is_nan : (Float) -> Bool`. The polymorphic `neg` +rationale: spec section A3 calls out that the `(- 0.0 x)` desugar is +wrong for `-0.0` (returns `+0.0` per IEEE rounding), so Float +negation needs its own builtin name. Reusing the `forall a. (a) -> a` +shape lets Int negation share the symbol. + +Three Float bit-pattern constants installed as bare values (parallel +to `__unreachable__` but with concrete `Type::float()` rather than +`forall a. a`): `nan`, `inf`, `neg_inf`. Reference site is `(var +nan)`, not `(app nan)`. Codegen emits `double 0x7FF8000000000000` / +`double 0x7FF0000000000000` / `double 0xFFF0000000000000` at the use +site in iter 4. + +One new effect op installed: `io/print_float : (Float) -> Unit !IO`. +Mirrors `io/print_int|bool|str`. Codegen lowering through runtime C +glue `@ail_print_float` lands in iter 4. + +Pattern-matching on Float literals is now typecheck-rejected via the +new `CheckError::FloatPatternNotAllowed` variant per spec line +723-735 recommendation (a). The surface lex / parser still ACCEPT +Float patterns (iter 2 left this open); the typecheck diagnostic +fires at the `Pattern::Lit { lit }` arm in +`crates/ailang-check/src/lib.rs`. The error message points the +LLM-author to the documented alternative — ordering operators and +`is_nan` for Float discrimination. + +`ail builtins` reflects all twelve new entries (4 widened arithmetic +display strings + 5 Float fn builtins + 3 Float constants + 1 +io/print_float effect op) via the refreshed `list()` table. + +Per-task commits: + +- `` floats iter 3.1: widen +/-/*/// and !=//>= to polymorphic forall a +- `` floats iter 3.2: install neg/int_to_float/float_to_int_truncate/float_to_str/is_nan +- `` floats iter 3.3: install Float constants nan/inf/neg_inf + io/print_float effect op +- `` floats iter 3.4: typecheck rejects Pattern::Lit Float with FloatPatternNotAllowed + +Known debt deliberately deferred to later iterations of this milestone: + +- Codegen LOWERING for the widened `+`/`-`/`*`/`/` etc. — iter 4 + converts the monomorphic-Int `synth::builtin_binop` table to + type-dispatched; emits `fadd double` / `fcmp olt double` / etc. + for the Float arm. +- Codegen LOWERING for `neg` (Int → `sub i64 0, %x`, Float → + `fneg double %x`) — iter 4. +- Codegen LOWERING for `int_to_float` (`sitofp`), + `float_to_int_truncate` (`@llvm.fptosi.sat.i64.f64`), + `float_to_str` (runtime C glue), `is_nan` (`fcmp uno`) — iter 4. +- Codegen LOWERING for `nan`/`inf`/`neg_inf` constants (LLVM hex- + float literals at the use site) — iter 4. +- Codegen LOWERING for `io/print_float` (parallel to `io/print_int`, + runtime glue `@ail_print_float`) — iter 4. +- Prose round-trip for Float literals — iter 5. +- DESIGN.md §"Float semantics" subsection (A5 determinism contract) + and the line-2033 "supported primitive types" list update — iter 5. +``` + +Replace each `` placeholder with the actual commit SHA at +write time. + +- [ ] **Step 2: Commit** + +```bash +git add docs/JOURNAL.md +git commit -m "floats iter 3: JOURNAL — iteration close (typecheck + builtins)" +``` + +--- + +## Iteration acceptance + +- [ ] `cargo build --workspace` is clean. +- [ ] `cargo test --workspace` is GREEN — pre-existing tests all + stay GREEN; the 11 new builtins-tests + 1 new typecheck-rejection + test all PASS. +- [ ] `ail builtins` reflects the widened signatures and the twelve + new entries. +- [ ] `crates/ailang-check/src/builtins.rs::install` and + `crates/ailang-codegen/src/synth.rs::builtin_ail_type` are in + lockstep (same set of names with matching types). +- [ ] No file touched outside the four listed in the file map. +- [ ] JOURNAL entry committed with the actual per-task commit SHAs. + +When all five tasks are committed and the acceptance checklist is +green, hand back to the orchestrator. Iteration 4 (Codegen WIDEN + +Float lowering paths) is the next dispatch.