diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index cdf75b3..7f1cb17 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -1137,3 +1137,29 @@ fn unreachable_demo() { let lines: Vec<&str> = stdout.lines().collect(); assert_eq!(lines, vec!["4", "5"]); } + +/// Iter 16e: polymorphic `==`. Properties protected: +/// (1) `==` typechecks at Int / Bool / Str / Unit (the fixture +/// uses every supported case directly via `(app == ...)`); +/// (2) codegen dispatches each arg-type to the right LLVM shape +/// — `icmp eq i64`, `icmp eq i1`, `@strcmp + icmp eq i32 0`, +/// constant `i1 true` — and the binary's stdout matches the +/// boolean truth-table for those operators; +/// (3) 16c's `build_eq` desugar of `(pat-lit "hi")` over a `Str` +/// scrutinee now goes through, since `==` no longer rejects +/// non-Int args at typecheck. +#[test] +fn eq_demo() { + let stdout = build_and_run("eq_demo.ail.json"); + let lines: Vec<&str> = stdout.lines().collect(); + assert_eq!( + lines, + vec![ + "true", "false", // == on Int + "false", "true", // == on Bool + "true", "false", // == on Str + "true", // == on Unit + "1", "2", "0", // classify_str: Str lit-pattern desugar + ] + ); +} diff --git a/crates/ail/tests/snapshots/hello.ll b/crates/ail/tests/snapshots/hello.ll index ae8533b..8748a32 100644 --- a/crates/ail/tests/snapshots/hello.ll +++ b/crates/ail/tests/snapshots/hello.ll @@ -7,6 +7,7 @@ target triple = "" declare i32 @printf(ptr, ...) declare i32 @puts(ptr) declare ptr @GC_malloc(i64) +declare i32 @strcmp(ptr, ptr) @ail_hello_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_hello_main_adapter, ptr null } define i8 @ail_hello_main() { diff --git a/crates/ail/tests/snapshots/list.ll b/crates/ail/tests/snapshots/list.ll index d913c15..cdd4b06 100644 --- a/crates/ail/tests/snapshots/list.ll +++ b/crates/ail/tests/snapshots/list.ll @@ -7,6 +7,7 @@ target triple = "" declare i32 @printf(ptr, ...) declare i32 @puts(ptr) declare ptr @GC_malloc(i64) +declare i32 @strcmp(ptr, ptr) @ail_list_sum_list_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_sum_list_adapter, ptr null } @ail_list_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_main_adapter, ptr null } diff --git a/crates/ail/tests/snapshots/max3.ll b/crates/ail/tests/snapshots/max3.ll index c5755c1..1801959 100644 --- a/crates/ail/tests/snapshots/max3.ll +++ b/crates/ail/tests/snapshots/max3.ll @@ -7,6 +7,7 @@ target triple = "" declare i32 @printf(ptr, ...) declare i32 @puts(ptr) declare ptr @GC_malloc(i64) +declare i32 @strcmp(ptr, ptr) @ail_max3_max_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max_adapter, ptr null } @ail_max3_max3_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max3_adapter, ptr null } diff --git a/crates/ail/tests/snapshots/sum.ll b/crates/ail/tests/snapshots/sum.ll index 1b27760..9a65908 100644 --- a/crates/ail/tests/snapshots/sum.ll +++ b/crates/ail/tests/snapshots/sum.ll @@ -7,6 +7,7 @@ target triple = "" declare i32 @printf(ptr, ...) declare i32 @puts(ptr) declare ptr @GC_malloc(i64) +declare i32 @strcmp(ptr, ptr) @ail_sum_sum_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_sum_adapter, ptr null } @ail_sum_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_main_adapter, ptr null } diff --git a/crates/ail/tests/snapshots/ws_main.ll b/crates/ail/tests/snapshots/ws_main.ll index a93a013..2952389 100644 --- a/crates/ail/tests/snapshots/ws_main.ll +++ b/crates/ail/tests/snapshots/ws_main.ll @@ -7,6 +7,7 @@ target triple = "" declare i32 @printf(ptr, ...) declare i32 @puts(ptr) declare ptr @GC_malloc(i64) +declare i32 @strcmp(ptr, ptr) @ail_ws_lib_add_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_lib_add_adapter, ptr null } @ail_ws_main_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_main_main_adapter, ptr null } diff --git a/crates/ailang-check/src/builtins.rs b/crates/ailang-check/src/builtins.rs index a3cea88..531128e 100644 --- a/crates/ailang-check/src/builtins.rs +++ b/crates/ailang-check/src/builtins.rs @@ -61,9 +61,30 @@ pub fn install(env: &mut crate::Env) { for op in ["+", "-", "*", "/", "%"] { env.globals.insert(op.into(), int_int_int.clone()); } - for op in ["==", "!=", "<", "<=", ">", ">="] { + for op in ["!=", "<", "<=", ">", ">="] { env.globals.insert(op.into(), int_int_bool.clone()); } + + // Iter 16e: `==` 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`. ADT/Fn equality is rejected at codegen + // with a clear "== not supported for type X" error. The other + // comparison ops (`<`, `<=`, `>`, `>=`, `!=`) stay Int-only. + env.globals.insert( + "==".into(), + Type::Forall { + vars: vec!["a".into()], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::bool_()), + effects: vec![], + }), + }, + ); env.globals.insert( "not".into(), Type::Fn { @@ -137,7 +158,7 @@ pub fn list() -> Vec<(&'static str, &'static str)> { ("*", "(Int, Int) -> Int"), ("/", "(Int, Int) -> Int"), ("%", "(Int, Int) -> Int"), - ("==", "(Int, Int) -> Bool"), + ("==", "forall a. (a, a) -> Bool"), ("!=", "(Int, Int) -> Bool"), ("<", "(Int, Int) -> Bool"), ("<=", "(Int, Int) -> Bool"), diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 84c925d..317e9e9 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -3556,4 +3556,92 @@ mod tests { vec!["k".to_string(), "x".to_string(), "z".to_string()] ); } + + /// Iter 16e: helper that wraps `body` in a fn whose return type is + /// `Bool`, runs `check`, and returns the diagnostics. Used by the + /// polymorphic-`==` typecheck tests below. + fn check_eq_body_returns_bool(body: Term) -> Vec { + let m = Module { + schema: SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![fn_def( + "f", + Type::Fn { + params: vec![], + ret: Box::new(Type::bool_()), + effects: vec![], + }, + vec![], + body, + )], + }; + check_module(&m) + } + + fn eq_app(a: Term, b: Term) -> Term { + Term::App { + callee: Box::new(Term::Var { name: "==".into() }), + args: vec![a, b], + tail: false, + } + } + + /// Iter 16e: `==` accepts Int args (regression — the pre-16e + /// behaviour stays identical). + #[test] + fn eq_typechecks_at_int() { + let body = eq_app( + Term::Lit { lit: Literal::Int { value: 1 } }, + Term::Lit { lit: Literal::Int { value: 2 } }, + ); + assert!(check_eq_body_returns_bool(body).is_empty()); + } + + /// Iter 16e: `==` accepts Bool args. Pre-16e this was a typecheck + /// error because `==` was declared `(Int, Int) -> Bool`. + #[test] + fn eq_typechecks_at_bool() { + let body = eq_app( + Term::Lit { lit: Literal::Bool { value: true } }, + Term::Lit { lit: Literal::Bool { value: false } }, + ); + assert!(check_eq_body_returns_bool(body).is_empty()); + } + + /// Iter 16e: `==` accepts Str args. Same story as Bool. + #[test] + fn eq_typechecks_at_str() { + let body = eq_app( + Term::Lit { lit: Literal::Str { value: "hi".into() } }, + Term::Lit { lit: Literal::Str { value: "ho".into() } }, + ); + assert!(check_eq_body_returns_bool(body).is_empty()); + } + + /// Iter 16e: `==` accepts Unit args. + #[test] + fn eq_typechecks_at_unit() { + let body = eq_app( + Term::Lit { lit: Literal::Unit }, + Term::Lit { lit: Literal::Unit }, + ); + assert!(check_eq_body_returns_bool(body).is_empty()); + } + + /// Iter 16e: `==`'s type still demands the two sides to agree — + /// `(== 1 true)` must fail to unify the second arg's `Bool` + /// against the metavar already pinned to `Int` by the first. + #[test] + fn eq_rejects_mixed_int_bool() { + let body = eq_app( + Term::Lit { lit: Literal::Int { value: 1 } }, + Term::Lit { lit: Literal::Bool { value: true } }, + ); + let diags = check_eq_body_returns_bool(body); + assert!( + !diags.is_empty(), + "(== 1 true) must fail to typecheck; got no diagnostics" + ); + } } diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 9be8cc8..c2e6fe2 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -351,7 +351,11 @@ pub fn lower_workspace(ws: &Workspace) -> Result { out.push_str("declare i32 @printf(ptr, ...)\n"); out.push_str("declare i32 @puts(ptr)\n"); - out.push_str("declare ptr @GC_malloc(i64)\n\n"); + out.push_str("declare ptr @GC_malloc(i64)\n"); + // Iter 16e: `==` on `Str` lowers to `@strcmp` followed by + // `icmp eq i32 0`. NUL-terminated strings make this a one-liner; + // libc supplies `strcmp` so no extra link flag is needed. + out.push_str("declare i32 @strcmp(ptr, ptr)\n\n"); out.push_str(&header); out.push_str(&body); @@ -1500,6 +1504,25 @@ impl<'a> Emitter<'a> { } fn lower_app(&mut self, name: &str, args: &[Term], tail: bool) -> Result<(String, String)> { + // Iter 16e: `==` is polymorphic (`forall a. (a, a) -> Bool`). + // Dispatch on the resolved AIL arg type — the LLVM `ptr` shape + // aliases multiple AIL types (Str vs ADT vs Fn), so we cannot + // dispatch on the LLVM type alone. ADT/Fn equality is rejected + // here with a clear error; `Unit` evaluates both sides for + // their side effects then returns constant `i1 1`. + if name == "==" { + if args.len() != 2 { + return Err(CodegenError::Internal( + "builtin `==` expected 2 args".into(), + )); + } + let arg_ty = self.synth_arg_type(&args[0])?; + let (a, a_ll) = self.lower_term(&args[0])?; + let (b, _b_ll) = self.lower_term(&args[1])?; + let _ = tail; + return self.lower_eq(&arg_ty, &a, &b, &a_ll); + } + // Built-in arithmetic / comparison. if let Some((instr, ret_ty)) = builtin_binop(name) { if args.len() != 2 { @@ -2330,6 +2353,80 @@ impl<'a> Emitter<'a> { } } + /// Iter 16e: lower a `==` call after the two operands have been + /// emitted. Dispatches on the resolved AIL type of the arg side + /// (both sides have the same type after typecheck). The `_a_ll` + /// hint is the LLVM type the lowering produced for `a`; we use + /// it as a sanity check against `arg_ty`'s expected LLVM shape. + /// + /// Supported: + /// - `Int` → `icmp eq i64` + /// - `Bool` → `icmp eq i1` + /// - `Str` → `@strcmp` then `icmp eq i32 0` + /// - `Unit` → constant `i1 true` (both sides already evaluated + /// for any side effects; Unit has a single inhabitant). + /// + /// Rejected with `CodegenError::Internal` for ADT, `Fn`, and any + /// other type — those would need either a structural-equality + /// scheme (ADT) or a fn-pointer compare (Fn) that the language + /// does not yet specify. + fn lower_eq( + &mut self, + arg_ty: &Type, + a: &str, + b: &str, + _a_ll: &str, + ) -> Result<(String, String)> { + match arg_ty { + Type::Con { name, .. } => match name.as_str() { + "Int" => { + let dst = self.fresh_ssa(); + self.body.push_str(&format!( + " {dst} = icmp eq i64 {a}, {b}\n" + )); + Ok((dst, "i1".into())) + } + "Bool" => { + let dst = self.fresh_ssa(); + self.body.push_str(&format!( + " {dst} = icmp eq i1 {a}, {b}\n" + )); + Ok((dst, "i1".into())) + } + "Str" => { + let cmp = self.fresh_ssa(); + self.body.push_str(&format!( + " {cmp} = call i32 @strcmp(ptr {a}, ptr {b})\n" + )); + let dst = self.fresh_ssa(); + self.body.push_str(&format!( + " {dst} = icmp eq i32 {cmp}, 0\n" + )); + Ok((dst, "i1".into())) + } + "Unit" => { + // Both sides have already been evaluated above for + // any side effects; Unit has a single inhabitant, + // so equality is `true` by definition. + let _ = a; + let _ = b; + Ok(("true".into(), "i1".into())) + } + other => Err(CodegenError::Internal(format!( + "`==` not supported for type `{other}` \ + (ADT and user-defined types lack a structural-equality scheme)" + ))), + }, + Type::Fn { .. } => Err(CodegenError::Internal( + "`==` not supported for function types (no canonical fn-pointer equality)".into(), + )), + other => Err(CodegenError::Internal(format!( + "`==` not supported for type `{}`", + ailang_core::pretty::type_to_string(other) + ))), + } + } + fn fresh_ssa(&mut self) -> String { self.counter += 1; format!("%v{}", self.counter) @@ -2640,7 +2737,23 @@ fn builtin_ail_type(name: &str) -> Option { }; Some(match name { "+" | "-" | "*" | "/" | "%" => int_int_int(), - "==" | "!=" | "<" | "<=" | ">" | ">=" => int_int_bool(), + "!=" | "<" | "<=" | ">" | ">=" => int_int_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 + // right LLVM instruction (icmp eq i64 / i1, @strcmp, or + // constant i1 1) on those resolved types. + "==" => Type::Forall { + vars: vec!["a".into()], + body: Box::new(Type::Fn { + params: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "a".into() }, + ], + ret: Box::new(Type::bool_()), + effects: vec![], + }), + }, "not" => Type::Fn { params: vec![Type::bool_()], ret: Box::new(Type::bool_()), @@ -3108,6 +3221,111 @@ mod tests { ); } + /// Iter 16e: codegen rejects `==` on ADT-typed args with a clear + /// error. The typechecker accepts the call (the rigid var of + /// `forall a. (a, a) -> Bool` unifies with the ADT type), so the + /// rejection has to happen here. The diagnostic must mention the + /// `==` symbol and the ADT type name. + #[test] + fn eq_on_adt_rejected_at_codegen() { + // Tiny ADT `data K = Mk` (nullary). + let mk = Term::Ctor { + type_name: "K".into(), + ctor: "Mk".into(), + args: vec![], + }; + let m = Module { + schema: SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![ + Def::Type(TypeDef { + name: "K".into(), + vars: vec![], + ctors: vec![Ctor { + name: "Mk".into(), + fields: vec![], + }], + doc: None, + }), + Def::Fn(FnDef { + name: "main".into(), + ty: Type::Fn { + params: vec![], + ret: Box::new(Type::unit()), + effects: vec![], + }, + params: vec![], + body: Term::Let { + name: "_b".into(), + value: Box::new(Term::App { + callee: Box::new(Term::Var { name: "==".into() }), + args: vec![mk.clone(), mk], + tail: false, + }), + body: Box::new(Term::Lit { lit: Literal::Unit }), + }, + doc: None, + }), + ], + }; + let err = emit_ir(&m).expect_err( + "`==` on ADT must be rejected at codegen; emit_ir succeeded", + ); + let msg = format!("{err:?}"); + assert!( + msg.contains("==") && msg.contains("not supported"), + "expected error mentioning `==` not supported; got: {msg}" + ); + } + + /// Iter 16e: same negative-path guard for function-typed args. + /// `==` on `Fn` is rejected with a "not supported for function + /// types" message. + #[test] + fn eq_on_fn_rejected_at_codegen() { + // `let f = main in (== f f)` — `main` is in scope as a fn-value. + let m = Module { + schema: SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![Def::Fn(FnDef { + name: "main".into(), + ty: Type::Fn { + params: vec![], + ret: Box::new(Type::unit()), + effects: vec![], + }, + params: vec![], + body: Term::Let { + name: "f".into(), + value: Box::new(Term::Var { name: "main".into() }), + body: Box::new(Term::Let { + name: "_b".into(), + value: Box::new(Term::App { + callee: Box::new(Term::Var { name: "==".into() }), + args: vec![ + Term::Var { name: "f".into() }, + Term::Var { name: "f".into() }, + ], + tail: false, + }), + body: Box::new(Term::Lit { lit: Literal::Unit }), + }), + }, + doc: None, + })], + }; + let err = emit_ir(&m).expect_err( + "`==` on Fn must be rejected at codegen; emit_ir succeeded", + ); + let msg = format!("{err:?}"); + assert!( + msg.contains("==") && msg.contains("function"), + "expected error mentioning `==` and function types; got: {msg}" + ); + } + #[test] fn missing_entry_main_is_error() { let m = Module { diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 8439bda..d8bab3a 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -773,7 +773,11 @@ collector wired up in Iter 14f, see Decision 9); nested constructor sub-patterns inside `match` (lifted in Iter 16a via the desugar pass); literal sub-patterns inside a Ctor pattern (lifted in Iter 16c — the desugar pass rewrites every `Pattern::Lit` to a `Term::If` on `==`, -both at the top level of an arm and inside a Ctor sub-pattern). +both at the top level of an arm and inside a Ctor sub-pattern); +`==` extended from Int-only to a polymorphic +`forall a. (a, a) -> Bool` over `Int`/`Bool`/`Str`/`Unit` (lifted +in Iter 16e — codegen monomorphises and dispatches on the +resolved arg type; ADT/Fn arg types are rejected at codegen). - No effect handlers — only the built-in IO and Diverge ops. - No refinements / SMT escalation. @@ -798,19 +802,39 @@ What **is** supported (and used as the smoke test for the pipeline): - `if`, `let`, function calls, recursion. - Effects on function signatures, with `do op(args)` for direct effect ops (`io/print_int`, `io/print_bool`, `io/print_str`). -- **Builtins.** Arithmetic and comparison operators (`+`, `-`, `*`, - `/`, `%`, `==`, `!=`, `<`, `<=`, `>`, `>=`) of type - `(Int, Int) -> Int` / `Bool`; logical `not : (Bool) -> Bool`; the - IO effect ops listed above; and **`__unreachable__ : forall a. a`** - (Iter 16d). The latter is a polymorphic bottom value: a use of - `__unreachable__` typechecks against any expected type at the use - site and codegens to the LLVM `unreachable` instruction (UB if - ever executed). It is the chain machinery's deepest fall-through - for matches that the typechecker proved exhaustive, and it is - available to user code as an explicit panic primitive - (`(if cond __unreachable__ ...)` for assertions or impossible - branches). Reference site is `Term::Var { name = "__unreachable__" }` - / form-A bare `__unreachable__`. +- **Builtins.** Arithmetic operators (`+`, `-`, `*`, `/`, `%`) of + type `(Int, Int) -> Int`; ordering operators and `!=` (`!=`, + `<`, `<=`, `>`, `>=`) of type `(Int, Int) -> Bool`; logical + `not : (Bool) -> Bool`; the IO effect ops listed above; + **`==` : forall a. (a, a) -> Bool** (Iter 16e); and + **`__unreachable__ : forall a. a`** (Iter 16d). + - **`==` is polymorphic** (Iter 16e). The typechecker accepts + `==` at any type whose two sides agree (the rigid `a` of the + `Forall` is unified by HM at the use site). Codegen + monomorphises and dispatches on the resolved AIL arg type: + `Int` → `icmp eq i64`; `Bool` → `icmp eq i1`; + `Str` → `call @strcmp(ptr, ptr)` then `icmp eq i32 0` + (`@strcmp` is declared in the LLVM IR header alongside + `@printf` / `@GC_malloc`); `Unit` → constant `i1 true` + (Unit has a single inhabitant; both sides are still + evaluated for any side effects). ADT and `Fn` arg types are + rejected at codegen with a `CodegenError::Internal` + mentioning `==` and the offending type — neither has a + canonical structural-equality scheme yet, and the language + deliberately does not silently elide the check. The other + comparison ops stay Int-only; their codegen path emits + `icmp s{lt,le,gt,ge,ne}` over `i64`. + - **`__unreachable__`** is a polymorphic bottom value: a use of + `__unreachable__` typechecks against any expected type at + the use site and codegens to the LLVM `unreachable` + instruction (UB if ever executed). It is the chain + machinery's deepest fall-through for matches that the + typechecker proved exhaustive, and it is available to user + code as an explicit panic primitive + (`(if cond __unreachable__ ...)` for assertions or + impossible branches). Reference site is + `Term::Var { name = "__unreachable__" }` / form-A bare + `__unreachable__`. - **ADTs + pattern matching** (Iter 3, extended in Iter 16a/16c). Sub-patterns of a Ctor pattern may be `Var`, `Wild`, another `Ctor` (Iter 16a), or a literal (Iter 16c). The desugar pass flattens @@ -820,10 +844,10 @@ What **is** supported (and used as the smoke test for the pipeline): - Literal patterns at top level and inside Ctor sub-patterns (Iter 16c, via desugar). `(pat-lit 0)` and `(pat-ctor Cons (pat-lit 0) _)` both parse and lower; the rewrite is to `Term::If { cond = (== sv lit) }`, - so any literal kind whose `==` is supported by the typechecker is - authorable. Today that means `Int`; `Bool`/`Str`/`Unit` lit patterns - are accepted by desugar but reach typecheck as a type error because - `==` is `(Int, Int) -> Bool` only. + so any literal kind whose `==` is supported is authorable. After + Iter 16e (`==` polymorphic over `Int`/`Bool`/`Str`/`Unit`), that + covers every lit kind the AST ships — including `(pat-lit "hi")` + over a `Str` scrutinee, exercised by `examples/eq_demo.ail.json`. - **Imports + qualified cross-module references** via dotted names (Iter 5). Extends to **types and constructors** (Iter 14h): a foreign module's ADT is referenced as `(con std_pair.Pair a b)`, its ctors as diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 3d47354..9b0ee61 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -4646,3 +4646,208 @@ addresses, not 16d. Bool/Str/Unit — surfaced by 16c, unchanged); 17a (per-fn arena, gated — unchanged); 16c-aux (`std_list::take`/`drop` refactor onto lit patterns — unchanged). + +## Iter 16e — `==` extends to Bool/Str/Unit (polymorphic dispatch) + +**Goal.** Lift the last gate the 16c entry left open: `==` was +declared `(Int, Int) -> Bool`, so 16c's `build_eq` rewrite of a +non-Int `Pattern::Lit` (`(pat-lit "hi")`, `(pat-lit true)`, etc.) +desugared to a well-formed AST but failed at typecheck because +the `==` call's arg types could not unify with `Int`. 16e +extends `==` to a polymorphic operator usable on the four +language-level scalar types — `Int`, `Bool`, `Str`, `Unit` — +and cleans the gap left by 16c so every `Literal` kind that +the AST ships is now usable in a `(pat-lit ...)` position. + +**Pre-16e state.** From the 16d journal: `==` lived as +`("==", "(Int, Int) -> Bool")` in `ailang-check::builtins` (line +~140). 16c's `build_eq` already produced `(app == lhs rhs)` for +every non-Unit literal kind; for `Unit` it short-circuited to +`Term::Lit { Bool { true } }` (every `()` is equal). Without +16e, the codegen rejection of non-Int `==` was preceded by a +typecheck rejection: `forall a. (a, a) -> Bool` was simply not +the declared type, so unification of `Bool` against `Int` (via +`int_int_bool`) blew up first. Iter 16d's `categorize_first` +fixture sidestepped the issue by using only Int lit patterns; +no shipped fixture used a `Bool`/`Str`/`Unit` lit pattern. + +**Architectural decision (binding, by orchestrator).** + +- `==`'s declared type becomes + `Forall(["a"], Fn([Var("a"), Var("a")], Bool, []))` — + `forall a. (a, a) -> Bool`. The polymorphic-builtin pattern + mirrors `__unreachable__` from 16d (which is a `Forall`-typed + value rather than a `Forall`-typed fn, but lives in the same + `env.globals` slot and the same `builtin_ail_type` mirror in + codegen). User-facing surface stays one symbol; the existing + `(app == ...)` shape carries every supported type. +- Codegen monomorphises like any polymorphic builtin and + dispatches on the resolved AIL arg type at the call site. + The dispatch table (one row per supported type): + + | AIL type | LLVM lowering | + |----------|------------------------------------------------| + | `Int` | `icmp eq i64` | + | `Bool` | `icmp eq i1` | + | `Str` | `call i32 @strcmp(ptr, ptr)` then `icmp eq i32 0` | + | `Unit` | constant `i1 true` (single-inhabitant) | + | ADT/Fn | rejected with `CodegenError::Internal` | + +- Unit's lowering still evaluates both operands above the + comparison (preserving any side effects), then ignores the + resulting SSA values and returns the constant `true`. This + matches the standard pattern (eval-both-then-fold) and keeps + `Unit` `==` semantics-preserving in the presence of an + effectful sub-expression (none of the shipped fixtures + exercise that, but the invariant is documented in + `lower_eq`'s rustdoc). +- ADT and `Fn` arg types fall to a clear codegen error message + (`==` not supported for type X / function types`). Two design + reasons: (a) ADT structural equality requires either a derived + per-type equality fn or runtime field-by-field walk — neither + is in 16e's scope; (b) `Fn`-pointer equality on a closure pair + is meaningless without a normalisation pass (two thunks may + represent the same lambda). Either is its own iter, queued + outside this one. The negative path is gated by two new + codegen unit tests (`eq_on_adt_rejected_at_codegen`, + `eq_on_fn_rejected_at_codegen`). + +**Why polymorphic `==` over per-type `==int`/`==bool`/`==str`.** +Mirrors `__unreachable__`'s precedent (one polymorphic name in +`env.globals`, instantiated by the typechecker at every use +site). Three concrete benefits over the alternative: +(i) `build_eq` from 16c stays as-is — it already produces a +single `(app == lhs rhs)` term, type-driven; (ii) authoring +surface stays one symbol, no `==str` lookup table for the LLM +to memorise; (iii) the existing `Forall` instantiation +machinery (`maybe_instantiate` in `ailang-check`) does the +work — no new typechecker code path. + +**The `@strcmp` extern.** `Str` `==` lowers to libc's +`strcmp(ptr, ptr) -> i32`. Strings are NUL-terminated literals +in the AILang ABI (see `io/print_str` lowering, which calls +`@puts`), so `strcmp` is a one-liner. Declared in the LLVM IR +header next to `@printf` / `@puts` / `@GC_malloc`. No extra +clang link flag needed — `strcmp` is in libc. + +**What shipped.** + +- `crates/ailang-check/src/builtins.rs` (+22, of which ~10 + doc): `==` is hoisted out of the `int_int_bool` shape branch + into a dedicated `Forall` registration; the `list()` row + becomes `("==", "forall a. (a, a) -> Bool")` (consumed by the + `ail builtins` CLI subcommand). Other comparison ops (`<`, + `<=`, `>`, `>=`, `!=`) keep their Int-only registration + unchanged — extending those is queued separately if ever + needed (`!=` would be a one-line change after this iter). +- `crates/ailang-codegen/src/lib.rs` (+~110, of which ~50 + doc): (a) IR header gains `declare i32 @strcmp(ptr, ptr)`; + (b) `lower_app` short-circuits `name == "=="` before the + `builtin_binop` block, calling a new `lower_eq` helper that + takes the resolved `Type` of the first arg (via + `synth_arg_type`) and dispatches by `Type::Con.name`; + (c) `builtin_ail_type` mirror gets the `Forall` form for + `==` so the mono pipeline's arg-type inference still + resolves the symbol. The old `("==", "icmp eq", "i1")` row + in `builtin_binop` stays — `is_static_callee` queries the + table to decide whether `==` is a direct callee, and the + early-return in `lower_app` ensures the `i64`-emission code + is never reached. +- `examples/eq_demo.ailx` + `examples/eq_demo.ail.json`: new + fixture exercising `==` at all four supported types directly + via `(app == ...)` and indirectly via 16c's lit-pattern + desugar over a `Str` scrutinee. Drives `io/print_bool` for + the boolean results and `io/print_int` for the `classify_str` + fn (a 3-arm `(match s ... (case (pat-lit "hi") 1) ...)`). + Output (one per line): `true`, `false` (Int); + `false`, `true` (Bool); `true`, `false` (Str); `true` + (Unit); `1`, `2`, `0` (`classify_str` over `"hi"`/`"ho"`/ + `"??"`). The Str lit-pattern arm is the smoking gun for + 16c+16e working together — pre-16e, that `(pat-lit "hi")` + desugared to `(if (== sv "hi") 1 fall_k)` and the `==` call + failed to typecheck. +- `crates/ail/tests/e2e.rs`: new `eq_demo` test (+25 incl. + doc), e2e count 46 → 47. +- `crates/ailang-check/src/lib.rs` (+~85 incl. doc): five new + unit tests in the `tests` module — `eq_typechecks_at_int` + (regression), `eq_typechecks_at_bool`, `eq_typechecks_at_str`, + `eq_typechecks_at_unit` (positive), and + `eq_rejects_mixed_int_bool` (negative — confirms the rigid + var still demands the two sides agree). +- `crates/ailang-codegen/src/lib.rs` tests: two new unit tests + (`eq_on_adt_rejected_at_codegen`, + `eq_on_fn_rejected_at_codegen`) that drive `emit_ir` past + typecheck and assert a clear error message mentions `==` and + the offending type kind. ADT case constructs a tiny `data K = + Mk` and compares two `Mk` ctors; Fn case binds `f = main` and + compares the fn-value with itself. +- `crates/ail/tests/snapshots/*.ll`: the IR header in every + snapshot now contains `declare i32 @strcmp(ptr, ptr)`; the + five existing snapshots (`hello`, `list`, `max3`, `sum`, + `ws_main`) were refreshed via `UPDATE_SNAPSHOTS=1`. Body of + every `define` block is byte-identical to pre-16e — the + header is the only diff. +- `docs/DESIGN.md`: Builtins bullet rewritten to call out the + polymorphic `==` and the dispatch table; the lit-pattern + bullet updated to drop the "today that means Int" caveat; + the "Recently lifted gates" preamble extended. + +**What deliberately did NOT change.** + +- The other comparison ops (`<`, `<=`, `>`, `>=`, `!=`) stay + Int-only. `!=` could be made polymorphic by the same recipe + (one row in `builtins.rs`, one branch in `lower_app`), but + staying in scope for this iter — queued. +- Codegen `unreachable!` arms for `Term::LetRec` STAY + (architectural rule from the iter brief, unchanged from + 16b.x). +- ADT structural equality and `Fn`-pointer equality stay + rejected at codegen. Either could be lifted later, but + needs its own design. +- `==` at the LetRec / closure-pair / lambda boundary is + unchanged: those still produce `Fn` arg types and now hit + the codegen-level rejection with a clearer error message + than the pre-16e "wrong LLVM type for icmp" garble. + +**Hash determinism.** The ten fixtures listed in the iter +brief (`local_rec_demo`, `lit_pat`, `local_rec_capture`, +`local_rec_let_capture`, `local_rec_match_capture`, +`local_rec_as_value`, `local_rec_as_value_capture`, +`poly_rec_capture`, `nested_let_rec`, `unreachable_demo`) +all produce identical `ail manifest` output to their pre-16e +forms — verified via direct manifest dump. No fixture's +canonical JSON changed; no def hash changed. The new +`eq_demo` fixture introduces two new hashes (`classify_str`, +`main`) that obviously did not exist before. + +**Tests: 125 → 133 (+8).** + +- e2e: 46 → 47 (`eq_demo`). +- `ailang-check::tests`: 29 → 34 (five new `eq_*` tests). +- `ailang-codegen::tests`: 2 → 4 (two negative-path tests). +- All other crates unchanged. +- IR snapshot tests: 5 → 5 (unchanged count; bytes refreshed + for the new `@strcmp` header line). + +**Cumulative state, post-16e.** + +- Stdlib unchanged (5 modules, 29 combinators). +- `Term`/`Pattern`/`Literal` enums unchanged. The change is + entirely a builtin-registration shift (`Fn` → `Forall` + in `env.globals`) plus a codegen dispatch site — no AST + shape changed and no schema bump. +- 16a desugar pass keeps its four-job role from 16d. 16e's + contribution is a pre-existing desugar output (`(app == + s_var lit)` from 16c's `build_eq`) suddenly being typeable + for non-Int literals. +- Compiler bugs surfaced and fixed in dogfood since 14a: 5/5 + (unchanged). + +**Queue update post-16e.** 16e done. Open: `closure-of-self` +(informally 16b.5-body — unchanged); `closure-poly` +(informally 16b.5b — unchanged); 17a (per-fn arena, gated on +user GC discussion — unchanged); 16c-aux (`std_list::take`/ +`drop` refactor onto lit patterns — unchanged); a low-priority +follow-up that mirrors 16e for `!=` (one-line change in +`builtins.rs` plus a one-line dispatch arm in `lower_app`, +queued without a number). diff --git a/examples/eq_demo.ail.json b/examples/eq_demo.ail.json new file mode 100644 index 0000000..0a9782d --- /dev/null +++ b/examples/eq_demo.ail.json @@ -0,0 +1 @@ +{"defs":[{"body":{"arms":[{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"lit":{"kind":"str","value":"hi"},"p":"lit"}},{"body":{"lit":{"kind":"int","value":2},"t":"lit"},"pat":{"lit":{"kind":"str","value":"ho"},"p":"lit"}},{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"p":"wild"}}],"scrutinee":{"name":"s","t":"var"},"t":"match"},"doc":"Lit-pattern over Str; exercises 16c's build_eq for non-Int.","kind":"fn","name":"classify_str","params":["s"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Str"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":5},"t":"lit"},{"lit":{"kind":"int","value":5},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":5},"t":"lit"},{"lit":{"kind":"int","value":6},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"bool","value":true},"t":"lit"},{"lit":{"kind":"bool","value":false},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"bool","value":true},"t":"lit"},{"lit":{"kind":"bool","value":true},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"str","value":"hi"},"t":"lit"},{"lit":{"kind":"str","value":"hi"},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"str","value":"hi"},"t":"lit"},{"lit":{"kind":"str","value":"ho"},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"unit"},"t":"lit"},{"lit":{"kind":"unit"},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"}],"op":"io/print_bool","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"str","value":"hi"},"t":"lit"}],"fn":{"name":"classify_str","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"str","value":"ho"},"t":"lit"}],"fn":{"name":"classify_str","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"lit":{"kind":"str","value":"??"},"t":"lit"}],"fn":{"name":"classify_str","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"t":"seq"},"doc":"Drive == at Int/Bool/Str/Unit; then drive classify_str.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"eq_demo","schema":"ailang/v0"} \ No newline at end of file diff --git a/examples/eq_demo.ailx b/examples/eq_demo.ailx new file mode 100644 index 0000000..8ba6f86 --- /dev/null +++ b/examples/eq_demo.ailx @@ -0,0 +1,56 @@ +; Iter 16e — `==` extends from Int-only to Int/Bool/Str/Unit (polymorphic +; dispatch). The builtin's declared type became +; forall a. (a, a) -> Bool +; and codegen monomorphises on the resolved arg type: +; Int → icmp eq i64 +; Bool → icmp eq i1 +; Str → @strcmp + icmp eq i32 0 +; Unit → constant i1 true (single-inhabitant type) +; ADT/Fn → rejected at codegen with a clear error. +; +; This fixture exercises all four supported types, both directly via +; `(app == ...)` and indirectly via 16c's lit-pattern desugar (which +; rewrites `(pat-lit "hi")` → `(if (== sv "hi") body fall_k)` and +; therefore inherits 16e's polymorphic `==`). +; +; Expected stdout (one per line): +; true ; (== 5 5) +; false ; (== 5 6) +; false ; (== true false) +; true ; (== true true) +; true ; (== "hi" "hi") +; false ; (== "hi" "ho") +; true ; (== () ()) +; 1 ; classify_str "hi" (lit-pattern hits 1 arm) +; 2 ; classify_str "ho" (lit-pattern hits 2 arm) +; 0 ; classify_str "??" (default arm) +; +; Driver lowers via io/print_bool / io/print_int. + +(module eq_demo + + (fn classify_str + (doc "Lit-pattern over Str; exercises 16c's build_eq for non-Int.") + (type (fn-type (params (con Str)) (ret (con Int)))) + (params s) + (body + (match s + (case (pat-lit "hi") 1) + (case (pat-lit "ho") 2) + (case _ 0)))) + + (fn main + (doc "Drive == at Int/Bool/Str/Unit; then drive classify_str.") + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (seq (do io/print_bool (app == 5 5)) + (seq (do io/print_bool (app == 5 6)) + (seq (do io/print_bool (app == true false)) + (seq (do io/print_bool (app == true true)) + (seq (do io/print_bool (app == "hi" "hi")) + (seq (do io/print_bool (app == "hi" "ho")) + (seq (do io/print_bool (app == (lit-unit) (lit-unit))) + (seq (do io/print_int (app classify_str "hi")) + (seq (do io/print_int (app classify_str "ho")) + (do io/print_int (app classify_str "??"))))))))))))))