From 0981804dd32db5fbaf76f2611849a5f039f99eb4 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 10 May 2026 15:24:13 +0200 Subject: [PATCH] floats iter 3.1: widen +/-/*/// and !=//>= to polymorphic forall a --- crates/ailang-check/src/builtins.rs | 160 ++++++++++++++++++++++++---- crates/ailang-codegen/src/synth.rs | 45 ++++++-- 2 files changed, 177 insertions(+), 28 deletions(-) diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs index c1687ad..7997185 100644 --- a/crates/ailang-check/src/builtins.rs +++ b/crates/ailang-check/src/builtins.rs @@ -48,6 +48,38 @@ pub struct EffectOpSig { /// [`list()`] is resolvable in `env`. Idempotent for a fresh `Env`; calling /// it twice would shadow the same entries with identical types. pub fn install(env: &mut crate::Env) { + // Iter 22-floats.3: arithmetic and comparison ops are polymorphic. + // Same shape as `==` below — the {Int, Float}-restriction is + // enforced at codegen, not at typecheck. `%` stays Int-only + // (no fmod yet — see spec section A3). + let poly_a_a_to_a = || Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::Var { name: "a".into() }), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }), + }; + let poly_a_a_to_bool = || Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::bool_()), + effects: vec![], + param_modes: vec![], + ret_mode: ailang_core::ast::ParamMode::Implicit, + }), + }; let int_int_int = Type::Fn { params: vec![Type::int(), Type::int()], ret: Box::new(Type::int()), @@ -55,18 +87,12 @@ pub fn install(env: &mut crate::Env) { param_modes: vec![], ret_mode: ailang_core::ast::ParamMode::Implicit, }; - let int_int_bool = Type::Fn { - params: vec![Type::int(), Type::int()], - ret: Box::new(Type::bool_()), - effects: vec![], - param_modes: vec![], - ret_mode: ailang_core::ast::ParamMode::Implicit, - }; - for op in ["+", "-", "*", "/", "%"] { - env.globals.insert(op.into(), int_int_int.clone()); + for op in ["+", "-", "*", "/"] { + env.globals.insert(op.into(), poly_a_a_to_a()); } + env.globals.insert("%".into(), int_int_int); for op in ["!=", "<", "<=", ">", ">="] { - env.globals.insert(op.into(), int_int_bool.clone()); + env.globals.insert(op.into(), poly_a_a_to_bool()); } // Iter 16e: `==` is polymorphic — `forall a. (a, a) -> Bool`. @@ -163,17 +189,17 @@ pub fn value_names() -> Vec<&'static str> { /// `ail builtins`, when the LLM wants to check expected signatures. pub fn list() -> Vec<(&'static str, &'static str)> { vec![ - ("+", "(Int, Int) -> Int"), - ("-", "(Int, Int) -> Int"), - ("*", "(Int, Int) -> Int"), - ("/", "(Int, Int) -> Int"), + ("+", "forall a. (a, a) -> a"), + ("-", "forall a. (a, a) -> a"), + ("*", "forall a. (a, a) -> a"), + ("/", "forall a. (a, a) -> a"), ("%", "(Int, Int) -> Int"), ("==", "forall a. (a, a) -> Bool"), - ("!=", "(Int, Int) -> Bool"), - ("<", "(Int, Int) -> Bool"), - ("<=", "(Int, Int) -> Bool"), - (">", "(Int, Int) -> Bool"), - (">=", "(Int, Int) -> Bool"), + ("!=", "forall a. (a, a) -> Bool"), + ("<", "forall a. (a, a) -> Bool"), + ("<=", "forall a. (a, a) -> Bool"), + (">", "forall a. (a, a) -> Bool"), + (">=", "forall a. (a, a) -> Bool"), ("not", "(Bool) -> Bool"), ("__unreachable__", "forall a. a"), ("io/print_int", "(Int) -> Unit !IO [effect op]"), @@ -181,3 +207,99 @@ pub fn list() -> Vec<(&'static str, &'static str)> { ("io/print_str", "(Str) -> Unit !IO [effect op]"), ] } + +#[cfg(test)] +mod tests { + use super::*; + use crate::{Env, Subst}; + use ailang_core::ast::{Literal, Term}; + use indexmap::IndexMap; + use std::collections::BTreeSet; + + /// Synthesize the type of a small expression in a fresh Env that has + /// only the builtins installed (no user defs). Returns the fully- + /// applied (substitution-resolved) result type; effects ignored for + /// this helper. Wraps `crate::synth` with the boilerplate state + /// (locals, effects sink, subst, counter, residuals) the real + /// typechecker entry points (`check_module`) would otherwise own. + fn synth_in_builtins_env(t: &Term) -> Type { + let mut env = Env::default(); + install(&mut env); + let mut locals: IndexMap = IndexMap::new(); + let mut effects: BTreeSet = BTreeSet::new(); + let mut subst = Subst::default(); + let mut counter: u32 = 0; + let mut residuals = Vec::new(); + let ty = crate::synth( + t, + &env, + &mut locals, + &mut effects, + "", + &mut subst, + &mut counter, + &mut residuals, + ) + .expect("synth"); + subst.apply(&ty) + } + + fn lit_int(v: i64) -> Term { + Term::Lit { lit: Literal::Int { value: v } } + } + fn lit_float(bits: u64) -> Term { + Term::Lit { lit: Literal::Float { bits } } + } + fn app(callee: &str, args: Vec) -> Term { + Term::App { + callee: Box::new(Term::Var { name: callee.into() }), + args, + tail: false, + } + } + + /// Iter 22-floats.3: regression — `(+ 1 2)` still resolves to `Int` + /// after the widening from `(Int, Int) -> Int` to + /// `forall a. (a, a) -> a`. Protects the no-regression invariant + /// for every existing Int-using fixture: the polymorphic `+` + /// instantiated at `(Int, Int)` must still return `Int`, + /// bit-identical to the pre-widening monomorphic shape. + #[test] + fn widen_plus_keeps_int_int_int() { + let ty = synth_in_builtins_env(&app("+", vec![lit_int(1), lit_int(2)])); + assert_eq!(ty, Type::int(), "(+ 1 2) must still type as Int"); + } + + /// Iter 22-floats.3: new acceptance — `(+ 1.5 2.5)` types as `Float`. + /// Pre-widening this would have failed with `TypeMismatch` because + /// `+` was monomorphic `(Int, Int) -> Int`. The widening to + /// `forall a. (a, a) -> a` makes Float arithmetic a typecheck-clean + /// shape; codegen filtering of the {Int, Float} arg-type set + /// happens in iter 4. + #[test] + fn widen_plus_accepts_float_float_float() { + let bits = 1.5_f64.to_bits(); + let ty = synth_in_builtins_env(&app("+", vec![lit_float(bits), lit_float(bits)])); + assert_eq!(ty, Type::float(), "(+ 1.5 2.5) must type as Float"); + } + + /// Iter 22-floats.3: regression — `(< 1 2)` still resolves to `Bool` + /// after the widening to `forall a. (a, a) -> Bool`. Mirrors the + /// `+` regression check for the comparison-op path. + #[test] + fn widen_lt_keeps_int_int_bool() { + let ty = synth_in_builtins_env(&app("<", vec![lit_int(1), lit_int(2)])); + assert_eq!(ty, Type::bool_(), "(< 1 2) must still type as Bool"); + } + + /// Iter 22-floats.3: new acceptance — `(< 1.5 2.5)` types as `Bool`. + /// Pre-widening this would have failed with `TypeMismatch`. The + /// widening to `forall a. (a, a) -> Bool` lets Float ordering + /// typecheck cleanly; codegen lowers to `fcmp olt double` in iter 4. + #[test] + fn widen_lt_accepts_float_float_bool() { + let bits = 1.5_f64.to_bits(); + let ty = synth_in_builtins_env(&app("<", vec![lit_float(bits), lit_float(bits)])); + assert_eq!(ty, Type::bool_(), "(< 1.5 1.5) must type as Bool"); + } +} diff --git a/crates/ailang-codegen/src/synth.rs b/crates/ailang-codegen/src/synth.rs index c3b5485..ad0c092 100644 --- a/crates/ailang-codegen/src/synth.rs +++ b/crates/ailang-codegen/src/synth.rs @@ -59,6 +59,39 @@ pub(crate) fn fn_sig_from_type(t: &Type) -> Option { /// `synth_arg_type` for arg-type inference at polymorphic call sites. /// Mirrors what the typechecker installs in its env via `builtins`. pub(crate) fn builtin_ail_type(name: &str) -> Option { + // Iter 22-floats.3: same widening as `crates/ailang-check/src/ + // builtins.rs` — `+`/`-`/`*`/`/` and `!=`/`<`/`<=`/`>`/`>=` are + // polymorphic. `%` stays monomorphic-Int. Codegen lowering for + // these ops still goes through `builtin_binop` (Int-only) in + // iter 3; iter 4 converts that to type-dispatched. + let poly_a_a_to_a = || Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::Var { name: "a".into() }), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }), + }; + let poly_a_a_to_bool = || Type::Forall { + vars: vec!["a".into()], + constraints: vec![], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::bool_()), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }), + }; let int_int_int = || Type::Fn { params: vec![Type::int(), Type::int()], ret: Box::new(Type::int()), @@ -66,16 +99,10 @@ pub(crate) fn builtin_ail_type(name: &str) -> Option { param_modes: vec![], ret_mode: ParamMode::Implicit, }; - let int_int_bool = || Type::Fn { - params: vec![Type::int(), Type::int()], - ret: Box::new(Type::bool_()), - effects: vec![], - param_modes: vec![], - ret_mode: ParamMode::Implicit, - }; Some(match name { - "+" | "-" | "*" | "/" | "%" => int_int_int(), - "!=" | "<" | "<=" | ">" | ">=" => int_int_bool(), + "+" | "-" | "*" | "/" => poly_a_a_to_a(), + "%" => int_int_int(), + "!=" | "<" | "<=" | ">" | ">=" => poly_a_a_to_bool(), // Iter 16e: `==` is polymorphic — `forall a. (a, a) -> Bool`. // The mono pipeline asks `synth_arg_type` for the actual arg // types at the call site; `lower_app` then dispatches to the