f64-inf, f64-nan, f32-inf and f32-nan are constants the compiler supplies

TODO.org

@@ -138,12 +138,19 @@ big-endian bytes, which is how the hex literal reads. Two and not one with a
 wider operand because the intrinsic takes a single repeated byte: the byte fill
 is one instruction and the four-byte pattern is a loop on both backends.
 
-** NEXT There is no literal for an infinity or a NaN
-Decided 2026-09-25: four constants the compiler supplies, =f64-inf=, =f64-nan=, =f32-inf=, =f32-nan=, beside =f64-max= and the rest. Negative infinity is =(- f64-inf)=. Rules out Clojure's =##Inf= reader literal.
-=lib/reader.ml= has no literal for either, and =float_repr= prints =inf= and =nan=
-as words the reader will not read back. =(/ 1.0 0.0)= is the only route to an
-infinity, and the constant folder is integers only, so it cannot be a =defconst=.
-Closing it needs a reader literal or a float-capable folding pass.
+** DONE There is no literal for an infinity or a NaN
+CLOSED: [2026-09-25]
+=f64-inf=, =f64-nan=, =f32-inf= and =f32-nan= are names the checker supplies
+(=Check.special_float=), reached only after every local, global and function has
+missed, so a program's own binding of one wins. Negative infinity is
+=(- 0.0 f64-inf)=: the decision wrote =(- f64-inf)=, and there is no unary minus.
+Rules out Clojure's =##Inf= reader literal.
+
+** TODO (!= x x) is false for a NaN
+=!== on floats is LLVM's ordered =one= on both backends (=lib/emit.ml= =fcmp_op=,
+=lib/x86.ml= =float_cc=), so =(!= f64-nan f64-nan)= is =false= where C, Odin and
+IEEE 754 say =true=; =(not (= x x))= is the only NaN test that works. Changing it
+to =une= is a decision about what =!== means.
 
 ** DONE A u64 constant above 2^63 cannot be written in decimal
 CLOSED: [2026-09-25]

lib/check.ml

@@ -1598,6 +1598,17 @@ let defvar_neither env loc ~form gname n ~values ~cases =
    asked "is this name declared at all", so a global that is itself a defonce
    still undecided belongs on it: what it resolves to is the next pass's
    question, not this one's. *)
+(* The infinities and NaNs, which the reader has no literal for and the
+   integer-only constant folder cannot compute, so the compiler supplies them
+   beside the prelude's f64-max and the rest. Negative infinity is
+   [(- f64-inf)]. *)
+let special_float = function
+  | "f64-inf" -> Some (Float.infinity, Types.F64)
+  | "f64-nan" -> Some (Float.nan, Types.F64)
+  | "f32-inf" -> Some (Float.infinity, Types.F32)
+  | "f32-nan" -> Some (Float.nan, Types.F32)
+  | _ -> None
+
 (* Case name -> the data type it belongs to, read off the declarations rather
    than out of [env.cases]: this runs inside [collect], which has registered
    the data type *names* by here but not resolved their cases, so the table
@@ -1689,7 +1700,9 @@ let settle_defvars env (decls : Ast.decl list) : Ast.decl list =
          end
          else begin
            (match t.Ast.t with
-            | Ast.Tname s when not (List.mem s (Lazy.force values)) ->
+            | Ast.Tname s
+              when not (List.mem s (Lazy.force values))
+                   && special_float s = None ->
               defvar_neither env t.Ast.tloc ~form n s
                 ~values:(Lazy.force values) ~cases:(Lazy.force cases)
             | _ -> ());
@@ -1982,6 +1995,7 @@ let mk loc ty e : Tast.expr = { Tast.e; ty; loc }
 
 let unit_at loc = mk loc Types.Unit Tast.Unit
 
+
 (* The environment for a lifted body, built once its own body has been checked
    and [caught] is therefore final. spec-memory.md's case 2, and the whole of
    its machinery.
@@ -3928,7 +3942,14 @@ and var ctx ?(qualified = false) loc ~want name =
              expect ctx loc ~want
                (mk loc (Types.CFn (params, ret))
                   (Tast.FnAddr (Tast.Fnval name)))
-           | None -> unknown_name ctx loc name)
+           | None ->
+             (* The float constants no literal can write, reached only once
+                every table above has missed, so a program's own binding of
+                one of these names is the one it gets. *)
+             match special_float name with
+             | Some (x, k) ->
+               expect ctx loc ~want (mk loc (Types.Float k) (Tast.Float (x, k)))
+             | None -> unknown_name ctx loc name)
 
 (* What remains of spec-memory.md's ownership section after the repeals of
    2026-09-18 is the allocator's side alone: the region rule decides where a

lib/prelude.ml

@@ -713,9 +713,9 @@ let source = {flan|
 ;;
 ;; Every decimal below is the shortest one that round-trips to the exact value
 ;; intended, and each is pinned against an independent derivation in
-;; test/programs/limits.flan rather than trusted. There is no infinity or NaN
-;; constant, and there cannot be one written down: the reader has no literal
-;; for either. (/ 1.0 0.0) is the only way to reach an infinity today.
+;; test/programs/limits.flan rather than trusted. The infinities and NaNs,
+;; f64-inf, f64-nan, f32-inf and f32-nan, are not here: no literal writes one,
+;; so the checker supplies them (Check.special_float).
 (defconst f32-max f32 3.4028234663852886e38)
 (defconst f64-max f64 1.7976931348623157e308)
 (defconst f32-min-positive f32 1.1754943508222875e-38)

test/programs/limits.flan

@@ -118,4 +118,14 @@
        (< (- (f32 0.0) f32-max) (- (f32 0.0) f32-min-positive)))
   (say "f64's least value negates its greatest"
        (< (- 0.0 f64-max) (- 0.0 f64-min-positive)))
+
+  ;; The infinities and NaNs, which no literal writes. Each infinity is the
+  ;; overflow of its type's greatest value, negated it is below the least
+  ;; finite one, and a NaN is the one value not equal to itself.
+  (say "f64-inf" (= f64-inf (* f64-max 2.0)))
+  (say "f32-inf" (= f32-inf (* f32-max (f32 2.0))))
+  (say "f64-inf negated" (< (- 0.0 f64-inf) (- 0.0 f64-max)))
+  (say "f32-inf negated" (< (- (f32 0.0) f32-inf) (- (f32 0.0) f32-max)))
+  (say "f64-nan" (not (= f64-nan f64-nan)))
+  (say "f32-nan" (not (= f32-nan f32-nan)))
   0)

test/test_acceptance.ml

@@ -5283,7 +5283,9 @@ level "1"
        f32-max is the last finite f32 ok\n\
        f64-max is the last finite f64 ok\n\
        f32's least value negates its greatest ok\n\
-       f64's least value negates its greatest ok\n"
+       f64's least value negates its greatest ok\n\
+       f64-inf ok\nf32-inf ok\nf64-inf negated ok\nf32-inf negated ok\n\
+       f64-nan ok\nf32-nan ok\n"
     in
     outputs "type limits" "programs/limits.flan" limits_out;
     outputs ~opt:"-O0" "type limits, -O0" "programs/limits.flan" limits_out;