spec: floats LLVM-IR fixes — fcmp une for !=, synth.rs sites, container-slot precision

Three classes of fix from the LLVM-IR audit:

1. != on Float: fcmp une, NOT fcmp one. one is 'ordered and not
   equal' (false for nan!=nan, breaks IEEE / user-fixed constraint).
   une is 'unordered or not equal' (true for nan!=nan, matches IEEE
   and Rust f64::ne).

2. crates/ailang-codegen/src/synth.rs touches the Float primitive at
   five sites the original spec missed: llvm_type, builtin_ail_type,
   builtin_effect_op_ret, type_descriptor (descriptor 'Fl' to avoid
   collision with ADT-name F-prefix), builtin_binop (becomes a
   transitional artefact, replaced by type-dispatched helper).

3. Float literals lower as LLVM hex-float syntax (double 0x4014...);
   nan/inf/neg_inf as direct SSA double constants at use site (NOT
   via the __unreachable__ analogue, which is a terminator
   instruction not a value); container slot layout precision
   (monomorphisation vs bitcast).
This commit is contained in:
2026-05-10 14:14:54 +02:00
parent f7e2c3ee7a
commit e37366f8dd
+115 -31
View File
@@ -133,12 +133,23 @@ lib.rs:2244-2266`):
| `*` | `mul i64` | `fmul double` |
| `/` | `sdiv i64` | `fdiv double` |
| `==` | existing `icmp eq i64` / `i1` / `@strcmp` / `i1 1` | `fcmp oeq double` |
| `!=` | derived from `==` | `fcmp one double` |
| `!=` | existing `icmp ne i64` etc. | `fcmp une double` |
| `<` | `icmp slt i64` | `fcmp olt double` |
| `<=` | `icmp sle i64` | `fcmp ole double` |
| `>` | `icmp sgt i64` | `fcmp ogt double` |
| `>=` | `icmp sge i64` | `fcmp oge double` |
**Note on `!=`:** the LLVM `fcmp` predicate for IEEE-`!=` is
`une` ("unordered or not equal"), **not** `one` ("ordered and
not equal"). `one` would return `false` for `nan != nan`, which
contradicts user-fixed constraint #2 (NaN ≠ NaN per IEEE).
`une` matches Rust's `f64::ne` and IEEE 754 `!=` exactly.
**Note on `==`:** `fcmp oeq` returns `false` whenever either
operand is NaN, which is the IEEE-`==` semantics we want.
Bit-level NaN-detection is separate and uses `is_nan` (below)
or `fcmp uno`.
Non-{Int,Float} resolutions for `+`/`-`/`*`/`/`/`<`/`<=`/`>`/`>=`
get rejected at codegen with the same diagnostic shape the `==`
path uses today (`"+ not supported for type X"`). The reject
@@ -356,50 +367,123 @@ the plan for iteration boundaries.
### `crates/ailang-codegen/`
- `lib.rs` (2877 LoC) — six lowering changes:
- `synth.rs` (218 LoC) — five sites mirroring the Float
primitive into the codegen-side type/op tables:
1. `llvm_type` (line 14): add `"Float" => Ok("double".into())`
arm parallel to the existing Int/Bool/Str/Unit arms.
2. `builtin_ail_type` (line 61): widen the `+`/`-`/`*`/`/`,
`<`/`<=`/`>`/`>=`, `!=` entries from `int_int_int` /
`int_int_bool` to the polymorphic `forall a. (a, a) -> a`
/ `forall a. (a, a) -> Bool` shape (mirrors what
`check/builtins.rs` installs). Add new entries for `neg`
(polymorphic), `int_to_float`, `float_to_int_truncate`,
`float_to_str`, `is_nan`, `nan`/`inf`/`neg_inf` (the
constants resolve as zero-arg "values", not fns — the
branch returns the bare `Type::float()` like
`__unreachable__` returns `forall a. a`).
3. `builtin_effect_op_ret` (line 118): add
`"io/print_float" => Type::unit()`.
4. `type_descriptor` (line 129): add `"Float" => "Fl"` arm.
Two letters because the single letter `F` is taken as
the ADT-name prefix (`FList`, `FFoo`); `Fl` is unambiguous
and short.
5. `builtin_binop` (line 167): this monomorphic-Int table
becomes a transitional artefact. Either convert it into a
type-dispatched helper that takes the operand `Type` and
returns the matching `(instr, llvm_ty)` pair, or remove
the table entirely and let the new dispatch helper in
`lib.rs` handle every site. Plan-time call.
- `lib.rs` (2877 LoC) — seven lowering changes:
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).
a `double` constant. The idiomatic LLVM form for a
bit-exact float constant is the hex-float literal
`double 0x4014000000000000` (LangRef: "the only time
hexadecimal floating point constants are required ...
is when a floating point constant must be emitted but
it cannot be represented as a decimal floating point
number in a reasonable number of digits", which covers
NaN, ±Inf, and any non-trivial decimal). Use this form
uniformly so every Float literal in the IR has the same
shape. Sites: every place `Literal::Int { value }` is
matched today (lines 918, 1215).
2. **Widen arithmetic dispatch.** `+`/`-`/`*`/`/` are
today lowered as monomorphic Int instructions
(line 1745 region). Convert the lowering site into a
type-dispatched helper analogous to the existing `==`
dispatch (`lib.rs:2244-2266`): Int arm emits
`add/sub/mul/sdiv i64`, Float arm emits
`fadd/fsub/fmul/fdiv double`, anything else fails with
`"<op> not supported for type X"`.
3. **Widen comparison dispatch.** `<`/`<=`/`>`/`>=` get the
same treatment: Int arm `icmp s{lt,le,gt,ge} i64`, Float
arm `fcmp o{lt,le,gt,ge} double`, reject otherwise.
4. **`==` / `!=` Float arm** in the existing dispatch
(line 2263 region) → `fcmp oeq` / `fcmp one` for the
`Float` case, alongside the existing arms.
(line 1745 region) using the `synth::builtin_binop`
table. Convert the lowering site into a type-dispatched
helper analogous to the existing `==` dispatch
(`lib.rs:2244-2266`): Int arm emits `add/sub/mul/sdiv
i64`, Float arm emits `fadd/fsub/fmul/fdiv double`,
anything else fails with `"<op> not supported for type
X"`. The existing test at `lib.rs:2627-2630` (which
pins `define i64 @ail_t_add(i64 %arg_a, i64 %arg_b)` and
`add i64 %arg_a, %arg_b`) must stay GREEN.
3. **Widen comparison dispatch.** `<`/`<=`/`>`/`>=`/`!=`
get the same treatment: Int arm `icmp s{lt,le,gt,ge} i64`
/ `icmp ne i64`, Float arm `fcmp o{lt,le,gt,ge} double`
/ **`fcmp une double` for `!=`** (NOT `fcmp one` —
`one` is "ordered and not equal" and returns `false`
for `nan != nan`, which violates IEEE; `une` is
"unordered or not equal" and matches IEEE / Rust).
4. **`==` Float arm** in the existing dispatch
(line 2263 region) → `fcmp oeq double` for the `Float`
case, alongside the existing arms. (`!=` is handled
under #3 above.)
5. **`neg` polymorphic** — Int arm `sub i64 0, %x`, Float
arm `fneg double %x` (correct for `-0.0`, unlike a
hypothetical `(- 0.0 x)` desugar). Reject other types.
arm `fneg double %x`. The `fneg` instruction (LLVM 8+)
correctly handles `-0.0` — `0.0 - 0.0` is `+0.0` per
IEEE rounding, so a `fsub double 0.0, %x` desugar would
wrongly produce `+0.0` for `neg(+0.0)` instead of
`-0.0`. Reject other types with the dispatch's standard
diagnostic.
6. **Conversions and IO**:
- `int_to_float` → `sitofp i64 ... to double`.
- `float_to_int_truncate` → `@llvm.fptosi.sat.i64.f64`
intrinsic (or the legalised cast sequence if the
target backend doesn't expose it directly).
intrinsic (LLVM 12+; AILang targets clang 22, so
always available). Spec semantics — NaN → 0,
+∞ → i64::MAX, -∞ → i64::MIN, finite-out-of-range
saturates, finite-in-range truncates toward zero —
are exactly the intrinsic's documented semantics, no
wrapping needed.
- `is_nan` → `fcmp uno double %x, %x` (returns `i1`,
which already coerces to AILang `Bool`).
which is AILang `Bool` directly per `synth.rs:18`).
- `float_to_str` → call into runtime C glue
`@ail_float_to_str`.
- `io/print_float` → parallel to `io/print_int`
(line 2150 region) → call into runtime C glue
`@ail_print_float`.
7. **Float constants** `nan`/`inf`/`neg_inf` lower as
`Term::Var` references resolving to compile-time `double`
constants (the codegen path that resolves `Var "x"` to
the SSA value of a global gets a builtin-constant arm,
same way `__unreachable__` resolves to `unreachable`).
- 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>`.
`Term::Var` references resolving directly to a `double`
SSA constant at the use site (LLVM hex-float literal):
- `nan` → `double 0x7FF8000000000000` (canonical qNaN)
- `inf` → `double 0x7FF0000000000000`
- `neg_inf` → `double 0xFFF0000000000000`
This is **unlike** the `__unreachable__` lowering, which
emits the `unreachable` *terminator instruction*.
Constants are SSA *values*, so the dispatch arm in
`lower_var` (or wherever `Var` resolution lives) returns
`(value-string, "double")` directly without going through
a global declaration.
- **ADT / container slot layout** — both `i64` and `double`
occupy 8 bytes, but they are distinct LLVM types. Two cases:
- **Monomorphisation produces concrete slot types.** If the
mono pass (`crates/ailang-check/src/mono.rs`) lowers
`List<Float>` to a concrete `List_Fl` whose field type is
`double`, no bitcast is needed. The `type_descriptor`
extension above (`Fl`) ensures the mangled name is
distinct from `List<Int>` (`List_I`).
- **Polymorphic / type-erased slots, if any.** If any
container path uses `i64` or `ptr` as a generic 8-byte
slot (e.g. an erased `Box<a>` that doesn't get
monomorphised), Float values traversing it need
`bitcast double to i64` going in and `bitcast i64 to
double` coming out. The plan verifies which case applies
by reading `mono.rs` and `lib.rs::lower_ctor` /
`lower_field_access`. The expected outcome is "fully
monomorphised, no bitcasts needed", but this is a
*check*, not an assumption.
### `crates/ailang-prose/`