AILang/crates/ailang-check/src/builtins.rs

//! Built-in operations known to the typechecker (and codegen).
//!
//! This module owns the **fixed** symbol set the language ships with — the
//! arithmetic / comparison / logical operators (`+`, `==`, `not`, ...) and
//! the IO effect ops (`io/print_int`, ...). User code cannot define
//! anything in here; conversely the typechecker treats every entry as
//! always-in-scope without an explicit import.
//!
//! Builtins are kept in a **separate table** from user globals (see
//! [`crate::Env::globals`] vs [`crate::Env::effect_ops`]) only because the
//! two channels surface differently in the AST: value-level builtins are
//! reached through `Term::Var { name }` (they live alongside user defs in
//! `Env.globals`), while effect ops are reached through `Term::Do { op }`
//! and need to carry an extra effect label, hence the dedicated
//! [`struct@EffectOpSig`] payload in `Env.effect_ops`.
//!
//! The typechecker calls [`install()`] once per module-check, before any
//! user-supplied globals are added. The CLI's `ail builtins` subcommand
//! reflects the same data via [`list()`] / [`value_names()`].

use ailang_core::ast::Type;

/// Signature of a builtin effect operation: the effect label it raises,
/// its parameter types, and its return type.
///
/// The typechecker consults this when synthesising the type of a
/// `Term::Do { op, args }` — it unifies `args` against `params`, returns
/// `ret`, and inserts `effect` into the body's accumulated effect set so
/// the surrounding fn's declared effect row is checked against actual
/// usage.
#[derive(Debug, Clone)]
pub struct EffectOpSig {
    /// Effect label this op raises (e.g. `"IO"`). Compared against the
    /// declared effect row on the enclosing fn type.
    pub effect: String,
    /// Positional parameter types. Length and order are the contract for
    /// `Term::Do { args }`.
    pub params: Vec<Type>,
    /// Return type of the op. Often [`Type::unit`] for sinks like
    /// `io/print_int`.
    pub ret: Type,
}

/// Populates `env` with every built-in operator and effect op.
///
/// Called once at the start of `check_in_workspace`, before user
/// type defs and globals are folded in. After this returns, every name in
/// [`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 — `%` semantics for Float require an explicit
    // decision on sign-of-result and ±0/±Inf edge cases that has
    // not been made).
    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()),
        effects: vec![],
        param_modes: vec![],
        ret_mode: ailang_core::ast::ParamMode::Implicit,
    };
    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(), poly_a_a_to_bool());
    }

    // `==` is polymorphic — `forall a. (a, a) -> Bool`. Codegen
    // dispatches on the resolved arg type at the call site:
    // `Int` → `icmp eq i64`, `Bool` → `icmp eq i1`, `Str` → `@strcmp`,
    // `Unit` → constant `i1 1`, `Float` → `fcmp oeq double`. ADT/Fn
    // equality is rejected at codegen with a clear "== not supported
    // for type X" error. The ordering ops (`<`, `<=`, `>`, `>=`, `!=`)
    // share the same polymorphic shape but with `Bool` return; `==`
    // stays in its own arm only because the codegen-side dispatch
    // table has historically been per-op.
    env.globals.insert(
        "==".into(),
        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,
            }),
        },
    );
    env.globals.insert(
        "not".into(),
        Type::Fn {
            params: vec![Type::bool_()],
            ret: Box::new(Type::bool_()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ailang_core::ast::ParamMode::Implicit,
        },
    );

    // Iter 16d: `__unreachable__` is the polymorphic bottom value.
    // Type: `forall a. a`. Used by the desugar pass as the chain
    // terminator of an exhaustive match, and available to user code as
    // a primitive panic point. Codegen lowers it to LLVM `unreachable`.
    // It is a value, not a fn — reference site is `(var __unreachable__)`,
    // not `(app __unreachable__)`.
    env.globals.insert(
        "__unreachable__".into(),
        Type::Forall {
            vars: vec!["a".into()],
            constraints: vec![],
            body: Box::new(Type::Var { name: "a".into() }),
        },
    );

    // Iter 22-floats.3: Float-conversion and inspection builtins.
    // Codegen lowering lands in iter 4; iter 3 only registers types.
    // `neg` is polymorphic (`forall a. (a) -> a`) for the same reason
    // the widened `+` is — Int and Float negation share one symbol;
    // the spec section A3 also notes that `(- 0.0 x)` desugar is
    // wrong for `-0.0` (returns `+0.0` per IEEE rounding), so Float
    // negation needs its own builtin name.
    env.globals.insert(
        "neg".into(),
        Type::Forall {
            vars: vec!["a".into()],
            constraints: vec![],
            body: Box::new(Type::Fn {
                params: vec![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,
            }),
        },
    );
    env.globals.insert(
        "int_to_float".into(),
        Type::Fn {
            params: vec![Type::int()],
            ret: Box::new(Type::float()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ailang_core::ast::ParamMode::Implicit,
        },
    );
    env.globals.insert(
        "float_to_int_truncate".into(),
        Type::Fn {
            params: vec![Type::float()],
            ret: Box::new(Type::int()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ailang_core::ast::ParamMode::Implicit,
        },
    );
    env.globals.insert(
        "float_to_str".into(),
        Type::Fn {
            params: vec![Type::float()],
            ret: Box::new(Type::str_()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ailang_core::ast::ParamMode::Implicit,
        },
    );
    env.globals.insert(
        "int_to_str".into(),
        Type::Fn {
            params: vec![Type::int()],
            ret: Box::new(Type::str_()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ailang_core::ast::ParamMode::Implicit,
        },
    );
    env.globals.insert(
        "is_nan".into(),
        Type::Fn {
            params: vec![Type::float()],
            ret: Box::new(Type::bool_()),
            effects: vec![],
            param_modes: vec![],
            ret_mode: ailang_core::ast::ParamMode::Implicit,
        },
    );

    // 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 {
            effect: "IO".into(),
            params: vec![Type::int()],
            ret: Type::unit(),
        },
    );
    env.effect_ops.insert(
        "io/print_bool".into(),
        EffectOpSig {
            effect: "IO".into(),
            params: vec![Type::bool_()],
            ret: Type::unit(),
        },
    );
    env.effect_ops.insert(
        "io/print_str".into(),
        EffectOpSig {
            effect: "IO".into(),
            params: vec![Type::str_()],
            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
/// show up as `Term::Var { name }` references in user code. Effect ops
/// are excluded because they reach codegen via `Term::Do`, not `Var`.
///
/// Single source of truth: derived from `list()` by filtering out the
/// effect-op rows. Kept as a function (not a `const`) because `list()`
/// already allocates; this is only consulted by tooling (`ail deps`).
pub fn value_names() -> Vec<&'static str> {
    list()
        .into_iter()
        .filter(|(_, sig)| !sig.contains("[effect op]"))
        .map(|(n, _)| n)
        .collect()
}

/// Returns the list of all registered built-ins. Useful for the CLI subcommand
/// `ail builtins`, when the LLM wants to check expected signatures.
pub fn list() -> Vec<(&'static str, &'static str)> {
    vec![
        ("+", "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"),
        ("!=", "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"),
        ("neg", "forall a. (a) -> a"),
        ("int_to_float", "(Int) -> Float"),
        ("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]"),
    ]
}

#[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<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 mut free_fn_calls = Vec::new();
        let ty = crate::synth(
            t,
            &env,
            &mut locals,
            &mut effects,
            "<test>",
            &mut subst,
            &mut counter,
            &mut residuals,
            &mut free_fn_calls,
        )
        .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 {
        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_a = 1.5_f64.to_bits();
        let bits_b = 2.5_f64.to_bits();
        let ty = synth_in_builtins_env(&app("+", vec![lit_float(bits_a), lit_float(bits_b)]));
        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_a = 1.5_f64.to_bits();
        let bits_b = 2.5_f64.to_bits();
        let ty = synth_in_builtins_env(&app("<", vec![lit_float(bits_a), lit_float(bits_b)]));
        assert_eq!(ty, Type::bool_(), "(< 1.5 2.5) must type as Bool");
    }

    /// Iter 22-floats.3: `neg` is polymorphic — `forall a. (a) -> a`.
    /// Both `(neg 5) : Int` and `(neg 1.5) : Float` typecheck. The
    /// polymorphic shape is the same as the widened arithmetic ops, so
    /// Int and Float negation share one symbol; codegen dispatches on
    /// the resolved arg type at the call site (iter 4).
    #[test]
    fn install_neg_is_polymorphic() {
        let ty_int = synth_in_builtins_env(&app("neg", vec![lit_int(5)]));
        assert_eq!(ty_int, Type::int(), "(neg 5) must type as Int");
        let bits = 1.5_f64.to_bits();
        let ty_float = synth_in_builtins_env(&app("neg", vec![lit_float(bits)]));
        assert_eq!(ty_float, Type::float(), "(neg 1.5) must type as Float");
    }

    /// Iter 22-floats.3: `int_to_float : (Int) -> Float`. The
    /// monomorphic conversion builtin — codegen lowers via `sitofp` in
    /// iter 4. Typecheck only validates the signature here.
    #[test]
    fn install_int_to_float_signature() {
        let ty = synth_in_builtins_env(&app("int_to_float", vec![lit_int(5)]));
        assert_eq!(ty, Type::float(), "(int_to_float 5) must type as Float");
    }

    /// Iter 22-floats.3: `float_to_int_truncate : (Float) -> Int`.
    /// Saturating truncation toward zero per spec A4 — typecheck only
    /// validates the signature; semantics is iter 4's codegen lowering
    /// via `@llvm.fptosi.sat.i64.f64`.
    #[test]
    fn install_float_to_int_truncate_signature() {
        let bits = 1.5_f64.to_bits();
        let ty = synth_in_builtins_env(&app("float_to_int_truncate", vec![lit_float(bits)]));
        assert_eq!(ty, Type::int(), "(float_to_int_truncate 1.5) must type as Int");
    }

    /// Iter 22-floats.3: `float_to_str : (Float) -> Str`. Codegen lowers
    /// via runtime C glue in iter 4; typecheck only validates the signature.
    #[test]
    fn install_float_to_str_signature() {
        let bits = 1.5_f64.to_bits();
        let ty = synth_in_builtins_env(&app("float_to_str", vec![lit_float(bits)]));
        assert_eq!(ty, Type::str_(), "(float_to_str 1.5) must type as Str");
    }

    /// Iter hs.4: `int_to_str : (Int) -> Str`. Codegen lowers via the
    /// runtime C glue `ailang_int_to_str` from `runtime/str.c`.
    #[test]
    fn install_int_to_str_signature() {
        let ty = synth_in_builtins_env(&app("int_to_str", vec![lit_int(42)]));
        assert_eq!(ty, Type::str_(), "(int_to_str 42) must type as Str");
    }

    /// Iter 22-floats.3: `is_nan : (Float) -> Bool`. Codegen lowers to
    /// `fcmp uno double %x, %x` in iter 4 — typecheck only validates
    /// the signature here.
    #[test]
    fn install_is_nan_signature() {
        let bits = 1.5_f64.to_bits();
        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 mut free_fn_calls = Vec::new();
        let ret = crate::synth(
            &do_term,
            &env,
            &mut locals,
            &mut effects,
            "<test>",
            &mut subst,
            &mut counter,
            &mut residuals,
            &mut free_fn_calls,
        )
        .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:?}"
        );
    }

    /// Iter 22-floats.3: pattern-matching on Float literals is hard-
    /// rejected at typecheck per spec line 723-735 recommendation (a).
    /// IEEE-`==` semantics make Float patterns semantically dubious
    /// (NaN never matches; equality is bit-exact not approximate).
    /// Surface lex / parser accept the syntax (iter 2); typecheck
    /// surfaces the error here.
    #[test]
    fn reject_float_pattern_in_match() {
        use ailang_core::ast::{Arm, Pattern};
        let bits = 1.5_f64.to_bits();
        let scrut = lit_float(bits);
        let arm = Arm {
            pat: Pattern::Lit { lit: Literal::Float { bits } },
            body: lit_int(0),
        };
        let term = Term::Match {
            scrutinee: Box::new(scrut),
            arms: vec![arm],
        };
        let mut env = Env::default();
        install(&mut env);
        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 mut free_fn_calls = Vec::new();
        let err = crate::synth(
            &term,
            &env,
            &mut locals,
            &mut effects,
            "<test>",
            &mut subst,
            &mut counter,
            &mut residuals,
            &mut free_fn_calls,
        )
        .expect_err("must reject");
        assert!(
            matches!(err, crate::CheckError::FloatPatternNotAllowed),
            "expected FloatPatternNotAllowed, got {err:?}"
        );
    }
}