floats iter 4.5: codegen Float constants nan/inf/neg_inf as hex-double SSA values

crates/ailang-codegen/src/lib.rs

@@ -1248,6 +1248,19 @@ impl<'a> Emitter<'a> {
                 Literal::Float { bits } => (format!("0x{:016X}", bits), "double".into()),
             }),
             Term::Var { name } => {
+                // Floats iter 4.5: bare-value Float constants resolve
+                // directly to LLVM hex-float `double` SSA values at
+                // the use site — no global declaration, no
+                // intern-global path. Parallel to how `__unreachable__`
+                // is intercepted, but as a value rather than a
+                // terminator (constants are SSA values; the
+                // unreachable-instruction path doesn't apply).
+                match name.as_str() {
+                    "nan" => return Ok(("0x7FF8000000000000".into(), "double".into())),
+                    "inf" => return Ok(("0x7FF0000000000000".into(), "double".into())),
+                    "neg_inf" => return Ok(("0xFFF0000000000000".into(), "double".into())),
+                    _ => {}
+                }
                 // Iter 16d: `__unreachable__` is a polymorphic bottom
                 // value (`forall a. a`). At codegen we emit LLVM
                 // `unreachable` as the block terminator and return a
@@ -3213,4 +3226,47 @@ mod tests {
         assert!(ir.contains("@llvm.fptosi.sat.i64.f64"), "float_to_int_truncate intrinsic missing: {ir}");
         assert!(ir.contains("fcmp uno double"), "is_nan missing (must be fcmp uno x, x): {ir}");
     }
+
+    /// Floats iter 4.5 RED: `nan`/`inf`/`neg_inf` resolve as bare
+    /// `Term::Var` references and lower to direct hex-float `double`
+    /// SSA values at the use site (no global definition emitted —
+    /// they are values, not unreachable-style terminators).
+    #[test]
+    fn lowers_float_constants() {
+        use ailang_core::ast::*;
+        fn fn_def(name: &str, body: Term) -> Def {
+            Def::Fn(FnDef {
+                name: name.into(),
+                ty: Type::Fn {
+                    params: vec![], ret: Box::new(Type::float()), effects: vec![],
+                    param_modes: vec![], ret_mode: ParamMode::Implicit,
+                },
+                params: vec![], body, suppress: vec![], doc: None,
+            })
+        }
+        let main_def = Def::Fn(FnDef {
+            name: "main".into(),
+            ty: Type::Fn {
+                params: vec![], ret: Box::new(Type::unit()), effects: vec![],
+                param_modes: vec![], ret_mode: ParamMode::Implicit,
+            },
+            params: vec![], body: Term::Lit { lit: Literal::Unit },
+            suppress: vec![], doc: None,
+        });
+        let m = Module {
+            schema: ailang_core::SCHEMA.to_string(),
+            name: "t".into(),
+            imports: vec![],
+            defs: vec![
+                fn_def("k_nan", Term::Var { name: "nan".into() }),
+                fn_def("k_inf", Term::Var { name: "inf".into() }),
+                fn_def("k_neg_inf", Term::Var { name: "neg_inf".into() }),
+                main_def,
+            ],
+        };
+        let ir = emit_ir(&m).unwrap();
+        assert!(ir.contains("0x7FF8000000000000"), "nan bit pattern missing: {ir}");
+        assert!(ir.contains("0x7FF0000000000000"), "+inf bit pattern missing: {ir}");
+        assert!(ir.contains("0xFFF0000000000000"), "-inf bit pattern missing: {ir}");
+    }
 }