test: red for Pattern::Lit::Float not rejected through full check pipeline
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.
This commit is contained in:
@@ -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:?}"
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user