From 23b625f32681ea9b08e665431a4b1438d885ae47 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sun, 10 May 2026 17:04:12 +0200 Subject: [PATCH] test: red for Pattern::Lit::Float not rejected through full check pipeline MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Pins fieldtest finding B1 (docs/specs/2026-05-10-fieldtest-floats.md). DESIGN.md and JOURNAL Floats.3 promise that pattern-matching on a Float literal is hard-rejected at typecheck via CheckError::FloatPatternNotAllowed, but the rejection only fires when typecheck is reached directly. The full check pipeline runs ailang_core::desugar::desugar_module first, and build_eq rewrites Pattern::Lit { Literal::Float } arms into (== scrutinee 1.5_FLOAT) before typecheck โ€” so the existing iter-3.4 reject arm at lib.rs:2316 is unreachable on input flowing through check / check_module / check_workspace. The existing reject_float_pattern_in_match test in builtins.rs calls synth(...) directly on a hand-built Term::Match, bypassing desugar; it passes today but does not protect the spec'd property. This new test exercises check(&m) end-to-end and asserts the FloatPatternNotAllowed error โ€” currently fails because check returns Ok(CheckedModule). GREEN side handed off to skills/implement mini-mode. --- crates/ailang-check/src/lib.rs | 63 ++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index b4a1697..9324cd0 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -4468,4 +4468,67 @@ mod tests { ailang_surface::parse_term(rep) .unwrap_or_else(|e| panic!("suggested rewrite must parse: {rep} ({e})")); } + + /// Floats milestone post-fieldtest B1 (RED): pattern-matching on a + /// `Literal::Float` literal must be hard-rejected at typecheck via + /// `CheckError::FloatPatternNotAllowed` per DESIGN.md ยง"Float + /// semantics" โ€” even when the match arm reaches `check` through + /// the *full* check pipeline (which runs `desugar_module` first). + /// + /// The existing `reject_float_pattern_in_match` test in + /// `crates/ailang-check/src/builtins.rs` calls `synth(...)` + /// directly on a hand-built `Term::Match`, bypassing desugar; it + /// passes today but does not protect the property the spec + /// promises. The desugar pass `build_eq` rewrites + /// `Pattern::Lit { lit }` arms (including `Literal::Float`) into + /// `Term::If { cond: (== scrutinee lit), .. }` *before* typecheck + /// runs (see `crates/ailang-core/src/desugar.rs:1056`), so the + /// `Pattern::Lit { lit: Literal::Float { .. } }` arm at + /// `lib.rs:2316` is unreachable on input that flows through + /// `check`/`check_module`/`check_workspace`. This test exercises + /// the full pipeline and pins the Float-pattern hard-reject as + /// a property of the public check API. + #[test] + fn check_rejects_float_pattern_through_full_pipeline() { + // fn classify : (Float) -> Int = \x. match x { 0.0 -> 1; _ -> 0 } + let bits = 0.0_f64.to_bits(); + let m = Module { + schema: SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![fn_def( + "classify", + Type::Fn { + params: vec![Type::float()], + ret: Box::new(Type::int()), + effects: vec![], + param_modes: vec![], + ret_mode: ParamMode::Implicit, + }, + vec!["x"], + Term::Match { + scrutinee: Box::new(Term::Var { name: "x".into() }), + arms: vec![ + Arm { + pat: Pattern::Lit { + lit: Literal::Float { bits }, + }, + body: Term::Lit { lit: Literal::Int { value: 1 } }, + }, + Arm { + pat: Pattern::Wild, + body: Term::Lit { lit: Literal::Int { value: 0 } }, + }, + ], + }, + )], + }; + let err = check(&m).expect_err( + "Pattern::Lit { Literal::Float } must be rejected at typecheck", + ); + assert!( + matches!(err, CheckError::FloatPatternNotAllowed), + "expected CheckError::FloatPatternNotAllowed, got {err:?}" + ); + } }