spec: floats milestone — Float as IEEE-754 binary64 primitive
This commit is contained in:
+21
-12
@@ -33,23 +33,32 @@ work progresses.
|
||||
|
||||
## P0 — In flight
|
||||
|
||||
- [x] **\[milestone\]** design-md-consolidation — `docs/DESIGN.md`
|
||||
is now a state-only specification across four thematic sweeps
|
||||
(history anchors out, REVERTED + migration plans out,
|
||||
schema-SoT inversion + data-model hardening, workflow /
|
||||
cross-reference cleanup). Closed 2026-05-10.
|
||||
- context: `docs/specs/2026-05-10-design-md-consolidation.md`,
|
||||
JOURNAL milestone-close entry of same date.
|
||||
- [~] **\[milestone\]** Floats — introduce `Float` as IEEE-754
|
||||
binary64 primitive type. One float type only (no `f32`).
|
||||
IEEE-conformant equality: `eq : Float → Float → Bool` returns
|
||||
`false` for `NaN == NaN`; **no `Eq` instance** (the partiality
|
||||
is real and surfaces through `Maybe`-shaped comparators rather
|
||||
than through a lying total instance). `Ord` likewise partial:
|
||||
`compare : Float → Float → Maybe Ordering`. Includes literal
|
||||
syntax in Form-A + Surface, codegen for arithmetic ops,
|
||||
conversions Int↔Float, and `Show`-style printing without the
|
||||
typeclass machinery (the typeclass wiring lands in Post-22
|
||||
Prelude).
|
||||
- context: this conversation (2026-05-10) — Float status quo
|
||||
was "documented as a primitive but never implemented";
|
||||
`crates/ailang-core/src/canonical.rs:14` says "no floats".
|
||||
|
||||
## P1 — Next
|
||||
|
||||
- [ ] **\[milestone\]** Post-22 Prelude — ship `Show` / `Eq` / `Ord`
|
||||
with the four primitive instances (Int, Bool, Str, Float); rewire
|
||||
`print` through `Show.show`. Originally queued as 22b.4 in the
|
||||
typeclass milestone, kept on hold pending demand.
|
||||
with the three total-orderable primitive instances (Int, Bool, Str);
|
||||
rewire `print` through `Show.show`. Float gets `Show` but **not**
|
||||
`Eq` / `Ord` (partial — see Floats milestone). Originally queued
|
||||
as 22b.4 in the typeclass milestone, kept on hold pending demand.
|
||||
- context: JOURNAL 2026-05-09 ("JOURNAL queue")
|
||||
- depends on: design-md-consolidation (touches DESIGN.md schema
|
||||
sections that the consolidation will reshape)
|
||||
- depends on: Floats (the partial-Eq/Ord story for Float must be
|
||||
settled before the Prelude classes ship, so the Prelude can
|
||||
decide what's instanced and what isn't)
|
||||
|
||||
## P2 — Medium-term
|
||||
|
||||
|
||||
@@ -0,0 +1,564 @@
|
||||
# Floats — Design Spec
|
||||
|
||||
**Date:** 2026-05-10
|
||||
**Status:** Draft — awaiting user spec review
|
||||
**Authors:** Brummel (orchestrator) + Claude
|
||||
|
||||
## Goal
|
||||
|
||||
Introduce `Float` as a fourth zero-arity primitive type, alongside
|
||||
`Int`, `Bool`, `Str`, `Unit`. `Float` is **IEEE-754 binary64**
|
||||
(LLVM `double`). One float type ships, no `f32` variant.
|
||||
|
||||
Status quo (2026-05-10):
|
||||
|
||||
- `crates/ailang-core/src/primitives.rs:17` lists primitives as
|
||||
`Int | Bool | Str | Unit` — no Float.
|
||||
- `crates/ailang-core/src/canonical.rs:14` doc comment explicitly
|
||||
says "no floats" because `serde_json::Number::to_string` is not
|
||||
bit-stable across versions for floating-point values.
|
||||
- `docs/DESIGN.md:1625` mentions `Float` once in an annotation
|
||||
example — dead text with no implementation behind it.
|
||||
|
||||
After this milestone:
|
||||
|
||||
- An LLM-author can write `1.5`, `1.5e3`, `(fadd x y)`,
|
||||
`(int_to_float n)` in surface form (B); the canonical form (A)
|
||||
carries float literals as bit-pattern hex strings; codegen emits
|
||||
IEEE-754 binary64 ops via LLVM `double`.
|
||||
- The eventual Post-22 Prelude milestone can ship `Show Float`,
|
||||
but **not** `Eq Float` or `Ord Float` — Float's IEEE-conformant
|
||||
equality (NaN ≠ NaN) and partial ordering are real and surface
|
||||
through builtins, not through total typeclass instances.
|
||||
|
||||
This milestone is **scoped to the primitive itself** — literal
|
||||
shape, lexer/parser/printer, type, builtins, codegen, IO,
|
||||
documentation. Typeclass wiring (`Show` / `Eq` / `Ord` instances,
|
||||
`Num` polymorphism) is out of scope and lives in the next
|
||||
milestone(s).
|
||||
|
||||
## Architecture
|
||||
|
||||
Five load-bearing decisions shape every component below.
|
||||
|
||||
### A1 — Form-A literal shape: bit-pattern hex string
|
||||
|
||||
```json
|
||||
{ "kind": "float", "bits": "4014000000000000" }
|
||||
```
|
||||
|
||||
`bits` is the lowercase 16-character hex representation of the
|
||||
IEEE-754 binary64 bit pattern as a `u64` (big-endian byte
|
||||
ordering). This is the *only* permitted form; serialising `1.5`
|
||||
as a JSON number is forbidden.
|
||||
|
||||
Rationale:
|
||||
|
||||
- **Hash stability.** Form-A bytes feed `def_hash` /
|
||||
`module_hash` via `canonical::to_bytes`. Today's number path
|
||||
uses `serde_json::Number::to_string`, which is not bit-stable
|
||||
across `serde_json` versions for floats and which cannot
|
||||
represent NaN / ±Inf in JSON at all (they collapse to `null`).
|
||||
Routing floats through the *string* path preserves bit-exact
|
||||
determinism without changing `canonical.rs`'s number arm.
|
||||
- **NaN / -0 / Inf are explicit.** `+0.0` is `0000000000000000`,
|
||||
`-0.0` is `8000000000000000`, the two are distinct bit
|
||||
patterns and therefore distinct Form-A literals; quiet NaN is
|
||||
`7ff8000000000000`; ±Inf are `7ff0000000000000` /
|
||||
`fff0000000000000`. All preserved bit-for-bit by hash.
|
||||
- **No ambiguity.** `0.1` parsed in surface lex becomes
|
||||
`bits = "3fb999999999999a"` once; round-tripping back to
|
||||
surface `0.1` is the printer's job, but the canonical truth
|
||||
is always the bits.
|
||||
|
||||
The `canonical.rs:14` "no floats" comment will be updated to
|
||||
"floats only via the string path (bit-pattern hex)".
|
||||
|
||||
### A2 — Surface lexer: decimal-point or exponent required
|
||||
|
||||
A float literal in form (B) is one of:
|
||||
|
||||
- `<digits>.<digits>` — e.g. `1.5`, `0.0`, `100.0`
|
||||
- `<digits>.<digits>e[+-]?<digits>` — e.g. `1.5e3`, `2.0e-10`
|
||||
- `<digits>e[+-]?<digits>` — e.g. `1e10`, `3e-5`
|
||||
|
||||
Out of scope (rejected at lex time):
|
||||
|
||||
- Hex floats `0x1.8p4` — adds lexer complexity for no LLM-author
|
||||
benefit (GPT/Claude don't reach for hex float literals
|
||||
unprompted).
|
||||
- Bare leading/trailing dot: `.5`, `5.` — the unambiguous form
|
||||
(`0.5`, `5.0`) is one keystroke longer; rejecting the short
|
||||
forms removes a class of "is this a float or a member access?"
|
||||
ambiguity.
|
||||
- NaN / Inf literals — these are bit patterns, not surface
|
||||
syntax. A future Float stdlib can expose `Float.nan` /
|
||||
`Float.infinity` constants; for now an LLM that needs a NaN
|
||||
literal in form-A can write the hex bits directly.
|
||||
|
||||
Negative float literals follow today's negative-int rule
|
||||
(`crates/ailang-surface/src/lex.rs:175` accepts `-` followed by a
|
||||
digit as part of a numeric token), so `-1.5` lexes as a single
|
||||
`Tok::Float`.
|
||||
|
||||
### A3 — Builtin operators: no overloading, explicit f-prefix
|
||||
|
||||
| Domain | Int (existing) | Float (new) |
|
||||
|---|---|---|
|
||||
| Arithmetic | `+ - * / %` | `fadd fsub fmul fdiv fneg` |
|
||||
| Equality | `== !=` (polymorphic, codegen-dispatched) | (same — codegen arm extended) |
|
||||
| Ordering | `< <= > >=` (Int-only) | `flt fle fgt fge` |
|
||||
|
||||
Rationale:
|
||||
|
||||
- AILang already rejects operator overloading
|
||||
(`docs/DESIGN.md` "Feature-acceptance criterion"). A
|
||||
polymorphic `+ : forall a. (a, a) -> a` would either need
|
||||
ad-hoc constraints (the typeclass story, out of scope here) or
|
||||
a hard-coded Int|Float type spec-case in the typechecker. Both
|
||||
cost more than two-name disambiguation.
|
||||
- The `==`/`!=` codegen-dispatch path already exists
|
||||
(`crates/ailang-check/src/builtins.rs:78`,
|
||||
`crates/ailang-codegen/src/lib.rs:2244-2266`). Extending the
|
||||
arm is one branch addition; introducing `feq`/`fne` would be a
|
||||
duplication of an already-polymorphic site for no semantic
|
||||
gain. IEEE-conformant `==` (NaN == NaN ⇒ false) falls out of
|
||||
LLVM `fcmp oeq` directly.
|
||||
- `<`/`<=`/`>`/`>=` on Int are monomorphic today, so widening
|
||||
them to polymorphic-Int|Float would require a *new* dispatch
|
||||
path. Cheaper and more honest to add `flt`/`fle`/`fgt`/`fge`
|
||||
alongside.
|
||||
- `fmod` is **excluded** for this milestone. IEEE 754-2008
|
||||
remainder semantics (`fmod` vs `remainder`) are subtle enough
|
||||
to deserve their own decision; not blocking the milestone on
|
||||
it.
|
||||
|
||||
Builtin signatures (added to
|
||||
`crates/ailang-check/src/builtins.rs::install`):
|
||||
|
||||
```
|
||||
fadd : (Float, Float) -> Float
|
||||
fsub : (Float, Float) -> Float
|
||||
fmul : (Float, Float) -> Float
|
||||
fdiv : (Float, Float) -> Float
|
||||
fneg : (Float) -> Float
|
||||
flt : (Float, Float) -> Bool
|
||||
fle : (Float, Float) -> Bool
|
||||
fgt : (Float, Float) -> Bool
|
||||
fge : (Float, Float) -> Bool
|
||||
int_to_float : (Int) -> Float
|
||||
float_to_int_truncate : (Float) -> Int
|
||||
float_to_str : (Float) -> Str
|
||||
```
|
||||
|
||||
### A4 — Conversions: total, foot-gun-free
|
||||
|
||||
- `int_to_float : (Int) -> Float` — LLVM `sitofp double`. Exact
|
||||
for `|n| < 2^53`, round-to-nearest-even otherwise.
|
||||
- `float_to_int_truncate : (Float) -> Int` — saturating
|
||||
truncation toward zero; `NaN → 0`. Matches Rust `as i64`
|
||||
semantics (since 1.45). Total, no UB, no `Maybe Int` wrapper.
|
||||
Lowered as LLVM `fptosi.sat.i64`.
|
||||
- `float_to_str : (Float) -> Str` — shortest round-trippable
|
||||
decimal. The runtime C glue calls a `dtoa`-style routine (we
|
||||
link an existing `ryu`-equivalent implementation; vendoring vs
|
||||
upstream is a plan-time decision).
|
||||
|
||||
A hypothetical `float_to_int_checked : (Float) -> Maybe Int`
|
||||
variant would be safer than an unchecked `fptosi`, but the
|
||||
saturating truncate is *also* safe and is one less ADT
|
||||
construction at the call site. If a future use case needs the
|
||||
distinction (e.g. NaN-detection without a dedicated `is_nan`
|
||||
builtin), revisit then.
|
||||
|
||||
### A5 — Determinism contract
|
||||
|
||||
Spec language for `docs/DESIGN.md` "Float semantics" section
|
||||
(added by this milestone):
|
||||
|
||||
- **Guaranteed:** every individual builtin
|
||||
(`fadd`/`fsub`/`fmul`/`fdiv`/`fneg`/`flt`/...) lowers to a
|
||||
single LLVM IR instruction (`fadd double`, `fsub double`, ...).
|
||||
On a fixed `(target triple, LLVM version)` pair, the bit
|
||||
pattern of the result of any single op is reproducible.
|
||||
- **Guaranteed:** NaN and ±Inf propagate per IEEE 754 (no
|
||||
silent collapse to zero, no trap).
|
||||
- **Guaranteed:** -0 and +0 are distinct bit patterns at the
|
||||
literal / hash / equality-bit level (`==` returns `true`
|
||||
comparing `-0.0 == 0.0` per IEEE, but they hash distinctly in
|
||||
Form-A — this is the correct asymmetry).
|
||||
- **Unspecified:** FMA contraction (LLVM may fold `fadd (fmul a
|
||||
b) c` into `fma a b c`); reassociation; subnormal flushing
|
||||
modes if the target enables FTZ/DAZ; the exact NaN bit
|
||||
pattern produced by an op (any qNaN bit pattern is
|
||||
conformant).
|
||||
|
||||
These are the Rust / Swift / standard-LLVM defaults, not
|
||||
research-grade reproducibility guarantees. The stronger
|
||||
guarantee (e.g. Pythonic `float.fromhex`-level bit
|
||||
reproducibility across ops) would require LLVM
|
||||
`-ffp-contract=off` plus per-op intrinsic selection — out of
|
||||
scope; revisit only if a real use case appears.
|
||||
|
||||
## Components
|
||||
|
||||
Touched files, by crate. Sizes given for scope estimation; see
|
||||
the plan for iteration boundaries.
|
||||
|
||||
### `crates/ailang-core/`
|
||||
|
||||
- `ast.rs` (785 LoC) — add `Literal::Float { bits: u64 }`
|
||||
variant. Serde `rename_all = "lowercase"` already gives us the
|
||||
`"kind": "float"` discriminator. The `bits` field needs a
|
||||
custom `Serialize`/`Deserialize` to emit/parse the
|
||||
16-character lowercase hex string (Serde's default for `u64`
|
||||
is decimal). Add `Type::float()` convenience constructor
|
||||
alongside `Type::int()`/`Type::bool_()`/`Type::unit()`.
|
||||
- `primitives.rs` (52 LoC) — append `"Float"` to both
|
||||
`is_primitive_name` and `primitive_surface_name`. The
|
||||
lockstep test there enforces both are updated; extend the
|
||||
test sample to include `"Float"`.
|
||||
- `canonical.rs` (200+ LoC) — **no logic change**. The float
|
||||
literal goes through the `String` path because `bits` is
|
||||
serialised as a hex string, not a JSON number. Update the
|
||||
module-level "no floats" doc comment to reflect the new
|
||||
reality ("floats encoded as bit-pattern hex strings; the
|
||||
number path is still int-only").
|
||||
- `desugar.rs` (2889 LoC) — add `Literal::Float` branch to
|
||||
whatever match-arms handle `Literal::Int` for desugar
|
||||
passthrough (likely a small, mechanical change).
|
||||
- `pretty.rs` (204 LoC) — add `Literal::Float` arm; render as
|
||||
shortest round-trippable decimal (mirrors what
|
||||
`float_to_str` will do at runtime).
|
||||
|
||||
### `crates/ailang-surface/`
|
||||
|
||||
- `lex.rs` (264 LoC) — extend the digit-lead lexer arm. Today
|
||||
it parses `<digits>` as `Tok::Int(i64)`. New: peek for `.` or
|
||||
`e`/`E` after the integer part; if present, parse the full
|
||||
float form (per A2), `f64::from_str`, then `f64::to_bits()`
|
||||
to produce `Tok::Float(u64)`. New error variant
|
||||
`LexError::InvalidFloat { literal, start }` parallel to the
|
||||
existing `InvalidInteger`.
|
||||
- `parse.rs` (2406 LoC) — accept `Tok::Float(bits)` where a
|
||||
literal is allowed; wrap as `Term::Lit { lit:
|
||||
Literal::Float { bits } }`.
|
||||
- `print.rs` (734 LoC) — `write_lit` arm for `Literal::Float`:
|
||||
reconstruct `f64::from_bits(bits)`, then write shortest
|
||||
round-trippable decimal. **Output must be unambiguously a
|
||||
float in the surface lexer** — the printer always emits at
|
||||
least one of `.` or `e`/`E`, so `1.0` prints as `"1.0"` (or
|
||||
`"1e0"`), never as `"1"`. Otherwise `lex(print(1.0))` would
|
||||
re-parse as `Tok::Int(1)` and the round-trip property breaks.
|
||||
Round-trip property: `lex(print(L)) == L` for every Float
|
||||
literal — this becomes a regression test.
|
||||
|
||||
Special-case bit patterns:
|
||||
- `+inf`, `-inf`, NaN cannot be expressed in surface form (per
|
||||
A2 — no NaN/Inf surface literal). The printer for these
|
||||
cases emits a clear non-round-trippable token like
|
||||
`(float-bits "7ff0000000000000")` or panics; the milestone
|
||||
picks the panic path, since a Float literal that arrived in
|
||||
the AST as NaN/Inf must have come from Form-A directly
|
||||
(surface lex cannot produce it), and the printer's job is
|
||||
surface output, not a Form-A escape hatch. Plan-time
|
||||
refinement.
|
||||
|
||||
### `crates/ailang-check/`
|
||||
|
||||
- `lib.rs` (4457 LoC) — `Literal::Float` is well-typed at
|
||||
`Type::float()`. Add the one-arm extension to whatever
|
||||
`Term::Lit` typing helper exists.
|
||||
- `builtins.rs` (183 LoC) — install all twelve new entries (per
|
||||
A3). Extend `list()` accordingly so `ail builtins` reflects
|
||||
them. The `==` polymorphic entry needs no change here — the
|
||||
signature stays `forall a. (a, a) -> Bool`; the codegen
|
||||
side (below) handles the new Float arm.
|
||||
|
||||
### `crates/ailang-codegen/`
|
||||
|
||||
- `lib.rs` (2877 LoC) — six new lowering paths:
|
||||
1. **Float literal** (`Literal::Float { bits }`) → emit
|
||||
`double` constant via LLVM hex-float syntax
|
||||
`0x1p+0`-style or via `bitcast i64 0x... to double`.
|
||||
Sites: every place `Literal::Int { value }` is matched
|
||||
today (lines 918, 1215).
|
||||
2. **Arithmetic builtins** `fadd/fsub/fmul/fdiv/fneg` →
|
||||
LLVM `fadd double`, `fsub double`, `fmul double`,
|
||||
`fdiv double`, `fneg double`. Site: parallel to the
|
||||
`t_add` / `+` lowering (line 1745 region).
|
||||
3. **Comparison builtins** `flt/fle/fgt/fge` → LLVM
|
||||
`fcmp olt`, `fcmp ole`, `fcmp ogt`, `fcmp oge`
|
||||
(ordered, so NaN compares yield `false`).
|
||||
4. **`==` / `!=` Float arm** in the existing dispatch
|
||||
(line 2263 region) → `fcmp oeq` / `fcmp one` for the
|
||||
`Float` case. Add the case alongside the existing
|
||||
`"Int"` / `"Bool"` / `"Str"` / `"Unit"` arms.
|
||||
5. **Conversions** `int_to_float` → `sitofp i64 to double`;
|
||||
`float_to_int_truncate` → `call double @llvm.fptosi.sat.i64`
|
||||
(or the legalised equivalent).
|
||||
6. **`io/print_float`** effect-op lowering parallel to
|
||||
`io/print_int` (line 2150 region) → call into runtime C
|
||||
glue.
|
||||
- ADT / container layout — `double` is 8 bytes, fits the
|
||||
existing 8-byte slot used for `i64` and `ptr`. **No layout
|
||||
change.** Confirm this by inspecting how `List<Int>` lowers
|
||||
today and verifying the same layout works for `List<Float>`.
|
||||
|
||||
### `crates/ailang-prose/`
|
||||
|
||||
- `lib.rs` (2125 LoC) — Form-A ↔ Form-B prose mapping for
|
||||
`Literal::Float`. Form-B prose says e.g. "the number 1.5";
|
||||
Form-A round-trips through bits. Mirrors the existing
|
||||
`Literal::Int` prose treatment.
|
||||
|
||||
### `runtime/`
|
||||
|
||||
- New file `runtime/print_float.c` (or extend an existing C
|
||||
file) — `void ail_print_float(double v)` that writes the
|
||||
shortest round-trippable decimal followed by a newline. We
|
||||
vendor a small `ryu`-style implementation, or — if simpler —
|
||||
use `printf("%.17g\n", v)` for the milestone and revisit if
|
||||
the redundancy is a problem.
|
||||
- The RC runtime (`rc.c`, `bump.c`) is **not touched**. Float
|
||||
is a value type with no heap allocation per literal.
|
||||
|
||||
### `crates/ail/` (CLI)
|
||||
|
||||
- `ail builtins` automatically picks up the twelve new entries
|
||||
via `builtins::list()` — no CLI-level change needed.
|
||||
|
||||
### `docs/DESIGN.md`
|
||||
|
||||
- §"Data model" `Literal` enumeration: add the `float` kind
|
||||
with the `bits` hex-string field documented.
|
||||
- §"Data model" — extend the §"Type constructors" / primitives
|
||||
list to include `Float`.
|
||||
- §"Float semantics" — new top-level subsection (~50-80 lines)
|
||||
containing A5 (determinism contract) and pointers to the
|
||||
builtins for arithmetic / comparison / conversion / IO.
|
||||
- §"Form-B surface" — extend the literal grammar production to
|
||||
include the float forms from A2.
|
||||
- §"Built-in operations" — add the twelve new entries.
|
||||
|
||||
### `docs/JOURNAL.md`
|
||||
|
||||
- Per-iteration entries during implementation.
|
||||
- Milestone-close entry summarising what landed.
|
||||
|
||||
## Data flow
|
||||
|
||||
The path of a float literal through the pipeline, end-to-end:
|
||||
|
||||
```
|
||||
surface text: 1.5
|
||||
↓ ailang-surface/lex.rs
|
||||
Tok::Float(0x3ff8000000000000)
|
||||
↓ ailang-surface/parse.rs
|
||||
Term::Lit { lit: Literal::Float { bits: 0x3ff8000000000000 } }
|
||||
↓ ailang-surface/print.rs (round-trip)
|
||||
surface text: 1.5
|
||||
↓ ailang-core/canonical.rs
|
||||
Form-A bytes: {"lit":{"bits":"3ff8000000000000","kind":"float"},"t":"lit"}
|
||||
↓ ailang-core/hash.rs
|
||||
def_hash: <16-hex stable>
|
||||
↓ ailang-check/lib.rs
|
||||
Type::float()
|
||||
↓ ailang-codegen/lib.rs
|
||||
LLVM IR: store double 0x3FF8000000000000, ptr %slot
|
||||
↓ clang -O2
|
||||
machine code: movsd xmm0, qword ptr [rip + .LCPI...]
|
||||
```
|
||||
|
||||
Every stage observable; every stage round-trippable; every
|
||||
canonical-JSON byte stable across runs and `serde_json` versions.
|
||||
|
||||
For an arithmetic op `(fadd a b)`:
|
||||
|
||||
```
|
||||
surface text: (fadd a b)
|
||||
↓ Term::App { fn: Var "fadd", args: [a, b] }
|
||||
↓ ailang-check resolves "fadd" → builtin (Float, Float) -> Float
|
||||
↓ ailang-codegen sees builtin "fadd" → emit `%r = fadd double %a, %b`
|
||||
```
|
||||
|
||||
No magic dispatch — the builtin name is the dispatch key, like
|
||||
`int_add` aka `+` is today.
|
||||
|
||||
## Error handling
|
||||
|
||||
Lexer errors:
|
||||
|
||||
- `LexError::InvalidFloat { literal, start }` — raised when a
|
||||
digit-lead token contains `.` or `e/E` but `f64::from_str`
|
||||
rejects it (e.g. `1..5`, `1.5e`, `1.5e++3`). Message:
|
||||
`"invalid float literal `<literal>`"`.
|
||||
|
||||
Type errors:
|
||||
|
||||
- Float operators on non-Float arguments: standard "expected
|
||||
Float, got X" unification error from the existing typechecker
|
||||
— no new diagnostic needed.
|
||||
|
||||
Codegen errors:
|
||||
|
||||
- A Float literal whose `bits` cannot fit in 16 hex characters
|
||||
is impossible by construction (`u64` is exactly 16 hex
|
||||
characters), so no runtime check is added.
|
||||
- Form-A deserialisation rejects malformed hex (length ≠ 16,
|
||||
non-hex characters) at the serde layer; the resulting
|
||||
`serde_json::Error` propagates up the existing `ail check`
|
||||
error path.
|
||||
|
||||
Runtime errors:
|
||||
|
||||
- None per literal. Arithmetic operations follow IEEE: division
|
||||
by zero produces `±Inf` or `NaN`; overflow produces `±Inf`;
|
||||
invalid ops produce NaN. **No traps**, no Rust-style panics.
|
||||
This is the IEEE-conformant choice committed in user-fixed
|
||||
constraint #2.
|
||||
|
||||
## Testing strategy
|
||||
|
||||
Per-iteration RED-first tests in `tests/` (unit) and
|
||||
`bench/`-adjacent E2E. The plan will sequence these; the spec
|
||||
fixes the *property set* that must be covered.
|
||||
|
||||
### Round-trip properties (lex/parse/print/hash)
|
||||
|
||||
- `lex(print(L)) == L` for every Float literal — covers
|
||||
shortest-round-trippable decimal output.
|
||||
- Form-A bytes for `Literal::Float { bits }` are exactly
|
||||
`{"bits":"<16-hex>","kind":"float"}` — string-encoded, never
|
||||
JSON-number-encoded.
|
||||
- `def_hash` of a module containing a Float literal is stable
|
||||
across runs and across `serde_json` patch versions (mirrors
|
||||
the existing Int regression test).
|
||||
|
||||
### IEEE-conformance properties
|
||||
|
||||
- `(fadd 0.1 0.2)` produces the exact `bits` of
|
||||
`0.1_f64 + 0.2_f64` (i.e. `bits == 0x3fd3333333333334`, not
|
||||
`0x3fd3333333333333`). A single `fadd` cannot be FMA-contracted
|
||||
(no `c` operand to absorb), so the result is bit-stable per A5.
|
||||
- `==` on the same NaN bit pattern (passed in as a Float literal)
|
||||
returns `false`. `!=` on the same NaN literal returns `true`.
|
||||
- `flt`, `fle`, `fgt`, `fge` all return `false` when either
|
||||
argument is NaN (ordered comparisons).
|
||||
- `(fdiv 1.0 0.0)` produces `+inf` (bits `7ff0000000000000`);
|
||||
`(fdiv -1.0 0.0)` produces `-inf` (bits `fff0000000000000`);
|
||||
`(fdiv 0.0 0.0)` produces *some* NaN (test asserts
|
||||
`(fne result result) == true` per IEEE NaN-detection idiom,
|
||||
**not** specific NaN bits — A5 leaves the qNaN payload
|
||||
unspecified).
|
||||
- `+0.0` and `-0.0` hash distinctly in Form-A but compare equal
|
||||
via `==`.
|
||||
|
||||
### Conversion properties
|
||||
|
||||
- `int_to_float` exact for `|n| < 2^53`, rounds half-to-even
|
||||
beyond.
|
||||
- `float_to_int_truncate` total: `nan → 0`, `+inf → i64::MAX`,
|
||||
`-inf → i64::MIN`, finite values truncate toward zero.
|
||||
|
||||
### Codegen / runtime smoke
|
||||
|
||||
- An `examples/floats.ail.json` fixture that exercises
|
||||
literal, arithmetic, comparison, conversion, and
|
||||
`io/print_float`; runs through the full
|
||||
`ail build → executable → stdout-check` chain.
|
||||
|
||||
### Bench regression
|
||||
|
||||
- `bench/check.py`, `bench/compile_check.py`,
|
||||
`bench/cross_lang.py` must stay GREEN. Float doesn't touch
|
||||
the Int code paths, so regressions are not expected; running
|
||||
the harnesses is a sanity gate.
|
||||
|
||||
### Spec-drift test
|
||||
|
||||
- `crates/ailang-core/tests/design_schema_drift.rs` — extend
|
||||
the anchor list to include the new `"kind":"float"` and
|
||||
`"Float"` primitive name. The drift test guards against
|
||||
removing them silently from `DESIGN.md`.
|
||||
|
||||
## Acceptance criteria
|
||||
|
||||
The milestone is closeable when **all** of the following hold:
|
||||
|
||||
1. `crates/ailang-core/src/primitives.rs::is_primitive_name`
|
||||
returns `true` for `"Float"`. The lockstep test passes.
|
||||
2. `Literal::Float { bits: u64 }` is serialised as
|
||||
`{"bits":"<16-hex>","kind":"float"}` in canonical JSON. The
|
||||
round-trip test passes.
|
||||
3. The twelve new builtins (per A3) appear in
|
||||
`ail builtins` output.
|
||||
4. `examples/floats.ail.json` builds, runs, and produces the
|
||||
expected stdout (printed floats round-trip the literal
|
||||
forms).
|
||||
5. `cargo test --workspace` is GREEN.
|
||||
6. `bench/check.py`, `bench/compile_check.py`,
|
||||
`bench/cross_lang.py` exit 0.
|
||||
7. `docs/DESIGN.md` carries the new §"Float semantics"
|
||||
subsection, the extended `Literal` enumeration, the
|
||||
extended primitives list, and the twelve builtin signatures.
|
||||
The `design_schema_drift.rs` test extends to cover the new
|
||||
anchors.
|
||||
8. `cargo doc --no-deps` warning count does not increase from
|
||||
the milestone-open baseline (16 warnings; this is the
|
||||
queued rustdoc-sweep baseline).
|
||||
9. JOURNAL milestone-close entry written.
|
||||
10. `docs/roadmap.md` Floats entry flipped from `[~]` to `[x]`;
|
||||
Post-22 Prelude unblocked (its `depends on: Floats` line
|
||||
can be removed in the same commit or in the Prelude's
|
||||
brainstorm step — orchestrator call).
|
||||
|
||||
Out of scope, explicitly:
|
||||
|
||||
- `Show Float` / `Eq Float` / `Ord Float` instances. (Float
|
||||
gets `Show` in the next milestone; `Eq` and `Ord` will
|
||||
*intentionally* not exist for `Float` because of A5 +
|
||||
user-fixed constraint #2.)
|
||||
- Polymorphic numeric class (`Num`).
|
||||
- `f32`.
|
||||
- `fmod` / IEEE-`remainder`.
|
||||
- NaN-detection builtin (`is_nan`); NaN-construction builtin.
|
||||
Workaround in scope: `(fne x x)` is `true` iff `x` is NaN
|
||||
(the canonical IEEE NaN test). Documented in
|
||||
§"Float semantics".
|
||||
- `Float.nan` / `Float.infinity` named constants — these come
|
||||
with the eventual Float stdlib, not the primitive milestone.
|
||||
- `print` rewiring through `Show.show` — that is Post-22
|
||||
Prelude.
|
||||
- Pattern-matching on Float literals (`Pattern::Lit { lit:
|
||||
Literal::Float { ... } }`). Semantically dubious — IEEE `==`
|
||||
semantics mean `NaN` never matches any literal pattern, and
|
||||
`0.1` in a pattern matches *only* the parsed bit pattern
|
||||
`0x3fb999999999999a`, not "approximately 0.1". The plan
|
||||
decides between (a) hard-reject Float in `Pattern::Lit` at
|
||||
the typechecker (recommended), or (b) allow it with an
|
||||
IEEE-`==` semantics, which the LLM-author has to remember.
|
||||
Either way: this milestone explicitly does NOT introduce a
|
||||
Float-pattern *idiom* — the documented way to discriminate
|
||||
Floats is via the comparison builtins (`flt`/`fle`/...) and
|
||||
the NaN-detection idiom `(fne x x)`.
|
||||
|
||||
## Notes for the plan
|
||||
|
||||
The plan should sequence iterations roughly:
|
||||
|
||||
- **Iteration 1**: AST + canonical + primitives (the schema
|
||||
layer). Pure schema, RED-first by canonical-bytes test.
|
||||
- **Iteration 2**: Surface lex + parse + print round-trip.
|
||||
RED-first by `lex(print(L)) == L` property.
|
||||
- **Iteration 3**: Type + builtins install. RED-first by
|
||||
typecheck unit test on `(fadd 1.0 2.0) : Float`.
|
||||
- **Iteration 4**: Codegen (literal + arithmetic + comparison +
|
||||
conversion + IO). RED-first by E2E
|
||||
`examples/floats.ail.json`.
|
||||
- **Iteration 5**: Prose + DESIGN.md + drift-test extension +
|
||||
rustdoc.
|
||||
|
||||
Iteration boundaries are the plan's call. The five-cluster
|
||||
shape above is the spec's scope estimate, not a binding
|
||||
sequence.
|
||||
Reference in New Issue
Block a user