floats iter 3.3: install Float constants nan/inf/neg_inf + io/print_float effect op

crates/ailang-check/src/builtins.rs

@@ -211,6 +211,18 @@ pub fn install(env: &mut crate::Env) {
         },
     );
 
+    // Iter 22-floats.3: Float bit-pattern constants. Bare values, not
+    // fns — reference site is `(var nan)`. Codegen emits
+    // `double 0x7FF8000000000000` (NaN), `double 0x7FF0000000000000`
+    // (+Inf), `double 0xFFF0000000000000` (-Inf) at the use site in
+    // iter 4. Parallel to `__unreachable__` but typed as concrete
+    // `Float` rather than the polymorphic bottom — these constants
+    // always denote a specific `f64` bit pattern, never a generic
+    // missing value.
+    env.globals.insert("nan".into(), Type::float());
+    env.globals.insert("inf".into(), Type::float());
+    env.globals.insert("neg_inf".into(), Type::float());
+
     env.effect_ops.insert(
         "io/print_int".into(),
         EffectOpSig {
@@ -235,6 +247,16 @@ pub fn install(env: &mut crate::Env) {
             ret: Type::unit(),
         },
     );
+    // 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(),
+        },
+    );
 }
 
 /// Names of value-level built-ins (operators, `not`) — the ones that
@@ -274,9 +296,13 @@ pub fn list() -> Vec<(&'static str, &'static str)> {
         ("float_to_int_truncate", "(Float) -> Int"),
         ("float_to_str", "(Float) -> Str"),
         ("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]"),
     ]
 }
 
@@ -429,4 +455,60 @@ mod tests {
         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");
     }
+
+    /// 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`, but here the type is the concrete `Float`
+    /// instead of the polymorphic bottom — these constants always denote
+    /// a specific `f64` bit pattern.
+    #[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`.
+    /// Mirrors `io/print_int|bool|str`. Codegen lowering through runtime
+    /// C glue `@ail_print_float` lands in iter 4. Effects are collected
+    /// in the mutable `effects` sink (mirrors the real typechecker
+    /// pipeline); we assert both the return type and that `IO` was
+    /// accumulated.
+    #[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 mut locals: IndexMap<String, Type> = IndexMap::new();
+        let mut effects: BTreeSet<String> = BTreeSet::new();
+        let mut subst = Subst::default();
+        let mut counter: u32 = 0;
+        let mut residuals = Vec::new();
+        let ret = crate::synth(
+            &do_term,
+            &env,
+            &mut locals,
+            &mut effects,
+            "<test>",
+            &mut subst,
+            &mut counter,
+            &mut residuals,
+        )
+        .expect("synth");
+        let ret = subst.apply(&ret);
+        assert_eq!(ret, Type::unit(), "io/print_float returns Unit");
+        assert!(
+            effects.contains("IO"),
+            "io/print_float must accumulate IO effect, got {effects:?}"
+        );
+    }
 }

crates/ailang-codegen/src/synth.rs

@@ -177,6 +177,11 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
             param_modes: vec![],
             ret_mode: ParamMode::Implicit,
         },
+        // Iter 22-floats.3: Float bit-pattern constants. Bare values,
+        // not fns — referenced via `Term::Var`. Mirrors the
+        // typechecker's `builtins::install`. Codegen emits LLVM hex-
+        // float literals at the use site in iter 4.
+        "nan" | "inf" | "neg_inf" => Type::float(),
         _ => return None,
     })
 }
@@ -185,7 +190,7 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option<Type> {
 /// param signature is irrelevant here since we only consume the ret.
 pub(crate) fn builtin_effect_op_ret(op: &str) -> Option<Type> {
     Some(match op {
-        "io/print_int" | "io/print_bool" | "io/print_str" => Type::unit(),
+        "io/print_int" | "io/print_bool" | "io/print_str" | "io/print_float" => Type::unit(),
         _ => return None,
     })
 }