diff --git a/crates/ailang-check/src/diagnostic.rs b/crates/ailang-check/src/diagnostic.rs index ea35bbe..2d79964 100644 --- a/crates/ailang-check/src/diagnostic.rs +++ b/crates/ailang-check/src/diagnostic.rs @@ -54,6 +54,14 @@ //! [`SuggestedRewrite`] whose `replacement` is the relaxed //! `(fn-type ...)` in form-A. Pure advisory; the typechecker still //! accepts the original signature. +//! - `empty-suppress-reason` (Iter 19b) — `severity: error`. Emitted +//! by the per-module suppress filter when a `(suppress (code ...) +//! (because ""))` entry on an `FnDef` has an empty or +//! whitespace-only `because`. `ctx`: `{"code": ""}`. +//! Hard-Error: a suppression without a reason is unreviewable, so +//! the build refuses it. Note that an invalid suppression does NOT +//! suppress its target diagnostic — the original still fires +//! alongside this error. use serde::Serialize; diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 106ff7d..8047feb 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -39,6 +39,7 @@ use std::collections::{BTreeMap, BTreeSet}; mod linearity; mod reuse_shape; +mod suppress_filter; pub mod uniqueness; /// Metavariable substitution. Maps fresh metavar ids (from `$m` in @@ -656,8 +657,13 @@ pub fn check_workspace(ws: &Workspace) -> Vec { let m = &ws.modules[name]; let typecheck_errors = check_in_workspace(m, ws, &module_globals); let had_typecheck_errors = !typecheck_errors.is_empty(); + // Per-module diagnostic accumulator. The suppress filter + // (Iter 19b) runs at the end of the per-module block, so + // we keep this module's diagnostics in their own vec while + // accumulating, then merge into the workspace-wide list. + let mut module_diags: Vec = Vec::new(); for e in typecheck_errors { - diagnostics.push(e.to_diagnostic()); + module_diags.push(e.to_diagnostic()); } // Iter 18c.2: linearity check runs only on modules that // typechecked clean. Running it on a body that already has a @@ -667,7 +673,7 @@ pub fn check_workspace(ws: &Workspace) -> Vec { // all-explicit-mode fn are exactly the surface the check is // designed to inspect. if !had_typecheck_errors { - diagnostics.extend(linearity::check_module(m)); + module_diags.extend(linearity::check_module(m)); // Iter 18d.2: reuse-as shape compatibility check. Runs on // the same activation gate as linearity (all-explicit-mode // fns only). The check resolves each `(reuse-as @@ -676,8 +682,15 @@ pub fn check_workspace(ws: &Workspace) -> Vec { // after linearity so its output appears after linearity's // diagnostics for the same def — stable ordering for the // JSON consumer. - diagnostics.extend(reuse_shape::check_module(m)); + module_diags.extend(reuse_shape::check_module(m)); } + // Iter 19b: apply per-fn `suppress` filter. Runs after every + // diagnostic source has appended so any code the author + // listed can actually be matched. Drops matching diagnostics + // and pushes `empty-suppress-reason` (Error) for malformed + // entries. See [`crate::suppress_filter`] for details. + suppress_filter::apply(m, &mut module_diags); + diagnostics.extend(module_diags); } diagnostics } @@ -2056,6 +2069,7 @@ mod tests { ty, params: params.into_iter().map(|s| s.into()).collect(), body, + suppress: vec![], doc: None, }) } @@ -2616,6 +2630,7 @@ mod tests { body: Term::Var { name: "x".into() }, }], }, + suppress: vec![], doc: None, }); // Use unbox at Int and at Bool — both must succeed and not diff --git a/crates/ailang-check/src/lift.rs b/crates/ailang-check/src/lift.rs index 60be9c8..7a37cd4 100644 --- a/crates/ailang-check/src/lift.rs +++ b/crates/ailang-check/src/lift.rs @@ -627,6 +627,7 @@ impl<'a> Lifter<'a> { ty: augmented_ty.clone(), params: augmented_params, body: body_full, + suppress: vec![], doc: Some(doc), })); diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index 34989c4..13cd9f3 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -1007,6 +1007,7 @@ mod tests { }, params: (0..modes.len()).map(|i| format!("p{i}")).collect(), body, + suppress: vec![], doc: None, }) } @@ -1159,6 +1160,7 @@ mod tests { }, params: vec!["xs".into()], body: Term::Lit { lit: Literal::Int { value: 0 } }, + suppress: vec![], doc: None, }); let f_body = Term::App { @@ -1324,6 +1326,7 @@ mod tests { }, params: vec!["xs".into()], body, + suppress: vec![], doc: None, }) } diff --git a/crates/ailang-check/src/reuse_shape.rs b/crates/ailang-check/src/reuse_shape.rs index ff72662..1b18940 100644 --- a/crates/ailang-check/src/reuse_shape.rs +++ b/crates/ailang-check/src/reuse_shape.rs @@ -584,6 +584,7 @@ mod tests { }, params: (0..modes.len()).map(|i| format!("p{i}")).collect(), body, + suppress: vec![], doc: None, }) } diff --git a/crates/ailang-check/src/suppress_filter.rs b/crates/ailang-check/src/suppress_filter.rs new file mode 100644 index 0000000..bcbffc6 --- /dev/null +++ b/crates/ailang-check/src/suppress_filter.rs @@ -0,0 +1,263 @@ +//! Iter 19b: per-module post-process that consumes +//! [`ailang_core::ast::FnDef::suppress`] entries. +//! +//! For each `Def::Fn(f)` and each `Suppress { code, because }` in +//! `f.suppress`: +//! +//! 1. If `because.trim()` is empty, push an `empty-suppress-reason` +//! `Error` diagnostic (the typechecker rejects the suppression +//! itself; the original diagnostic still fires unmasked, because +//! a malformed suppression cannot suppress anything). +//! 2. Otherwise, drop every diagnostic from the accumulated list whose +//! `def == Some(f.name)` AND `code == s.code`. +//! +//! The check runs once per module after every other diagnostic source +//! (typecheck → linearity → reuse-shape) has appended its output. +//! That way every diagnostic the suppression might mask is already in +//! the list when we filter. +//! +//! ## Why a wrong code does not error +//! +//! The diagnostic registry is open-set — codes are added per iter +//! and consumers (LLM tooling, future review tools) treat the set +//! as growing. A `(suppress (code "") ...)` entry simply +//! matches no diagnostic and therefore suppresses nothing; the +//! typechecker stays silent about it. This is intentionally +//! permissive: the cost of a typo is "the warning still fires", not +//! a hard build break, so authors who mis-type a code get the +//! original signal back instead of a confusing meta-error. +//! +//! ## Why empty `because` is hard-Error +//! +//! `because` is the only thing keeping a suppress from being a +//! drive-by silence: without a reason, a future maintainer (likely +//! a future LLM) reading the def has no way to judge whether to +//! keep, tighten, or remove the suppression. Refusing to typecheck +//! the def at all forces the explicit-intent contract. + +use crate::diagnostic::{Diagnostic, Severity}; +use ailang_core::ast::{Def, Module}; + +/// Apply the suppress filter to `diags` (mutates in place) for every +/// `Def::Fn` in `m`. New diagnostics (`empty-suppress-reason`) are +/// pushed onto `diags`. +pub(crate) fn apply(m: &Module, diags: &mut Vec) { + // Walk fns; collect (def_name, code) pairs to drop, plus any + // empty-reason errors to add. We can do this in one pass per fn + // because a wrong code cannot drop anything (no match) and an + // empty reason explicitly does not drop the diagnostic it points + // to (per the module-level rationale). + let mut to_drop: Vec<(String, String)> = Vec::new(); + let mut to_add: Vec = Vec::new(); + for def in &m.defs { + let f = match def { + Def::Fn(f) => f, + _ => continue, + }; + for s in &f.suppress { + if s.because.trim().is_empty() { + to_add.push(make_empty_suppress_reason(&f.name, &s.code)); + // Do NOT add to `to_drop`: an invalid suppression does + // not suppress anything — see module rationale. + } else { + to_drop.push((f.name.clone(), s.code.clone())); + } + } + } + + if !to_drop.is_empty() { + diags.retain(|d| { + let key = match &d.def { + Some(name) => (name.clone(), d.code.clone()), + None => return true, + }; + !to_drop.contains(&key) + }); + } + + diags.extend(to_add); +} + +/// Build the `empty-suppress-reason` diagnostic. Severity is +/// hard-Error: a suppression with no reason is unreviewable, so the +/// build refuses it. The `ctx` carries the `code` string so a tool +/// downstream can see exactly which suppression was malformed +/// (independent of the human-readable `message`). +fn make_empty_suppress_reason(def: &str, code: &str) -> Diagnostic { + let mut d = Diagnostic { + severity: Severity::Error, + code: "empty-suppress-reason".into(), + message: format!( + "suppress entry for diagnostic `{code}` requires a non-empty `because` reason" + ), + def: Some(def.to_string()), + ctx: serde_json::json!({"code": code}), + suggested_rewrites: Vec::new(), + }; + // Defensive: keep the field always-emitted shape (the Diagnostic + // builder also leaves it `[]`, but constructing the struct + // directly above means we set it explicitly here for clarity). + d.suggested_rewrites.clear(); + d +} + +#[cfg(test)] +mod tests { + use super::*; + use ailang_core::ast::{ + Def, FnDef, Literal, Module, ParamMode, Suppress, Term, Type, + }; + + fn module_with_one_fn(name: &str, suppress: Vec) -> Module { + Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![Def::Fn(FnDef { + name: name.into(), + ty: Type::Fn { + params: vec![], + param_modes: vec![], + ret: Box::new(Type::int()), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + params: vec![], + body: Term::Lit { lit: Literal::Int { value: 0 } }, + doc: None, + suppress, + })], + } + } + + /// Iter 19b: a suppress entry with a matching `(def, code)` pair + /// drops the diagnostic from the accumulated list. + #[test] + fn matching_suppress_drops_the_diagnostic() { + let m = module_with_one_fn( + "f", + vec![Suppress { + code: "over-strict-mode".into(), + because: "RC test fixture".into(), + }], + ); + let mut diags = vec![Diagnostic::warning("over-strict-mode", "msg") + .with_def("f")]; + apply(&m, &mut diags); + assert!(diags.is_empty(), "diagnostic should have been dropped: {diags:?}"); + } + + /// Iter 19b: an empty `because` produces an `empty-suppress-reason` + /// Error AND does NOT drop the original diagnostic. + #[test] + fn empty_because_errors_and_does_not_suppress() { + let m = module_with_one_fn( + "f", + vec![Suppress { + code: "over-strict-mode".into(), + because: "".into(), + }], + ); + let mut diags = vec![Diagnostic::warning("over-strict-mode", "msg") + .with_def("f")]; + apply(&m, &mut diags); + // Original diag still present; new error appended. + assert_eq!(diags.len(), 2, "expected original + new error: {diags:?}"); + let has_orig = diags.iter().any(|d| d.code == "over-strict-mode"); + let empty_err: Vec<_> = diags + .iter() + .filter(|d| d.code == "empty-suppress-reason") + .collect(); + assert!(has_orig, "original over-strict-mode must still fire"); + assert_eq!(empty_err.len(), 1, "exactly one empty-suppress-reason"); + assert_eq!(empty_err[0].severity, Severity::Error); + assert_eq!(empty_err[0].def.as_deref(), Some("f")); + assert_eq!( + empty_err[0].ctx, + serde_json::json!({"code": "over-strict-mode"}) + ); + } + + /// Iter 19b: whitespace-only `because` is treated the same as + /// empty — the trimmed text is what matters. + #[test] + fn whitespace_only_because_errors() { + let m = module_with_one_fn( + "f", + vec![Suppress { + code: "over-strict-mode".into(), + because: " \t \n ".into(), + }], + ); + let mut diags = vec![Diagnostic::warning("over-strict-mode", "msg") + .with_def("f")]; + apply(&m, &mut diags); + assert!( + diags + .iter() + .any(|d| d.code == "empty-suppress-reason"), + "whitespace-only because should fire empty-suppress-reason: {diags:?}" + ); + assert!( + diags.iter().any(|d| d.code == "over-strict-mode"), + "original diagnostic must still fire when suppress is invalid" + ); + } + + /// Iter 19b: a suppress entry whose `code` does not match any + /// diagnostic in the list is silently a no-op (the diagnostic + /// registry is open-set; a typo costs "warning still fires", not + /// a meta-error). + #[test] + fn unmatched_code_is_silent_no_op() { + let m = module_with_one_fn( + "f", + vec![Suppress { + code: "type-mismatch".into(), + because: "test".into(), + }], + ); + let mut diags = vec![Diagnostic::warning("over-strict-mode", "msg") + .with_def("f")]; + apply(&m, &mut diags); + // The original is untouched; no empty-suppress-reason is added. + assert_eq!(diags.len(), 1, "{diags:?}"); + assert_eq!(diags[0].code, "over-strict-mode"); + } + + /// Iter 19b: a diagnostic on a *different* def is not affected by + /// a suppression on this fn. + #[test] + fn suppression_only_drops_diagnostics_on_same_def() { + let m = module_with_one_fn( + "f", + vec![Suppress { + code: "over-strict-mode".into(), + because: "test".into(), + }], + ); + let mut diags = vec![ + Diagnostic::warning("over-strict-mode", "f msg").with_def("f"), + Diagnostic::warning("over-strict-mode", "g msg").with_def("g"), + ]; + apply(&m, &mut diags); + assert_eq!(diags.len(), 1, "only `f`'s diagnostic should drop: {diags:?}"); + assert_eq!(diags[0].def.as_deref(), Some("g")); + } + + /// Iter 19b: a diagnostic with `def == None` is never dropped by + /// any suppression (no def-name to match against). + #[test] + fn def_none_diagnostic_is_never_dropped() { + let m = module_with_one_fn( + "f", + vec![Suppress { + code: "over-strict-mode".into(), + because: "test".into(), + }], + ); + let mut diags = vec![Diagnostic::warning("over-strict-mode", "msg")]; + apply(&m, &mut diags); + assert_eq!(diags.len(), 1, "{diags:?}"); + } +} diff --git a/crates/ailang-check/src/uniqueness.rs b/crates/ailang-check/src/uniqueness.rs index daed723..fd219a9 100644 --- a/crates/ailang-check/src/uniqueness.rs +++ b/crates/ailang-check/src/uniqueness.rs @@ -413,6 +413,7 @@ mod tests { }, params: params.into_iter().map(|s| s.to_string()).collect(), body, + suppress: vec![], doc: None, }) } diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs index af5197a..c54baaa 100644 --- a/crates/ailang-check/tests/workspace.rs +++ b/crates/ailang-check/tests/workspace.rs @@ -152,6 +152,7 @@ fn body_errors_accumulate_across_defs() { ], tail: false, }, + suppress: vec![], doc: None, }); let bad_b = Def::Fn(FnDef { @@ -167,6 +168,7 @@ fn body_errors_accumulate_across_defs() { body: Term::Var { name: "this_does_not_exist".into(), }, + suppress: vec![], doc: None, }); @@ -222,6 +224,7 @@ fn use_after_consume_on_own_param_is_reported() { }, params: vec!["ys".into()], body: Term::Lit { lit: Literal::Int { value: 0 } }, + suppress: vec![], doc: None, }); @@ -256,6 +259,7 @@ fn use_after_consume_on_own_param_is_reported() { ], tail: false, }, + suppress: vec![], doc: None, }); @@ -347,6 +351,7 @@ fn consume_while_borrowed_in_sibling_arg_is_reported() { }, params: vec!["a".into(), "b".into()], body: Term::Lit { lit: Literal::Int { value: 0 } }, + suppress: vec![], doc: None, }); @@ -368,6 +373,7 @@ fn consume_while_borrowed_in_sibling_arg_is_reported() { ], tail: false, }, + suppress: vec![], doc: None, }); @@ -505,6 +511,7 @@ fn reuse_as_happy_path_in_map_inc_is_linearity_clean() { ty: map_inc_ty, params: vec!["xs".into()], body: map_inc_body, + suppress: vec![], doc: None, }); @@ -615,6 +622,7 @@ fn reuse_as_shape_mismatch_is_reported_on_cons_to_nil() { ty: f_ty, params: vec!["xs".into()], body, + suppress: vec![], doc: None, }); diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index 1a40afb..5b21d9d 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -849,6 +849,7 @@ impl<'a> Emitter<'a> { ty: mono_ty, params: fdef.params.clone(), body: mono_body, + suppress: vec![], doc: fdef.doc.clone(), }; // Specialised def belongs to the polymorphic def's owner @@ -2582,6 +2583,7 @@ mod tests { ], tail: false, }, + suppress: vec![], doc: None, }), // Entry module needs a `main`, otherwise @@ -2597,6 +2599,7 @@ mod tests { }, params: vec![], body: Term::Lit { lit: Literal::Unit }, + suppress: vec![], doc: None, }), ], @@ -2660,6 +2663,7 @@ mod tests { }), body: Box::new(Term::Lit { lit: Literal::Unit }), }, + suppress: vec![], doc: None, }), ], @@ -2710,6 +2714,7 @@ mod tests { body: Box::new(Term::Lit { lit: Literal::Unit }), }), }, + suppress: vec![], doc: None, })], }; @@ -2742,6 +2747,7 @@ mod tests { body: Term::Lit { lit: Literal::Int { value: 1 }, }, + suppress: vec![], doc: None, })], }; @@ -2811,6 +2817,7 @@ mod tests { }, params: vec![], body: Term::Lit { lit: Literal::Unit }, + suppress: vec![], doc: None, }), ], diff --git a/crates/ailang-core/src/ast.rs b/crates/ailang-core/src/ast.rs index 753f690..94a4260 100644 --- a/crates/ailang-core/src/ast.rs +++ b/crates/ailang-core/src/ast.rs @@ -183,6 +183,41 @@ pub struct FnDef { /// Optional source-level documentation string. #[serde(default, skip_serializing_if = "Option::is_none")] pub doc: Option, + /// Iter 19b: structured-diagnostic suppressions opted into for this + /// fn. Each entry names a diagnostic code and an author-asserted + /// reason. Currently the only consumer is `over-strict-mode` + /// (Iter 19a / 19a.1) but the mechanism is generic across codes. + /// `because` must be non-empty — the typechecker emits + /// `empty-suppress-reason` (Error) otherwise. + /// + /// Serialised with `skip_serializing_if = "Vec::is_empty"` so + /// every pre-19b fixture's canonical-JSON hash stays bit-identical. + /// The same additive-schema pattern is used by [`TypeDef::vars`] + /// (Iter 13a) and [`Type::Con::args`] (Iter 13a). + #[serde(default, skip_serializing_if = "Vec::is_empty")] + pub suppress: Vec, +} + +/// Iter 19b: one entry in [`FnDef::suppress`]. Marks a structured +/// diagnostic the author has consciously decided to allow on this +/// def, with a mandatory reason. +/// +/// `because` is non-empty by schema rule — the typechecker emits +/// `empty-suppress-reason` (Error severity) when it is empty or +/// whitespace-only, and a wrong/unknown `code` simply matches no +/// diagnostic and therefore suppresses nothing (the original +/// diagnostic still fires unmasked). +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct Suppress { + /// The diagnostic code being suppressed (e.g. + /// `"over-strict-mode"`). Matched against + /// [`crate::SCHEMA`]-side codes; an unknown code suppresses + /// nothing but is not itself an error (the diagnostic registry + /// is open-set). + pub code: String, + /// The author's stated reason. Must be non-empty — the + /// typechecker emits `empty-suppress-reason` (Error) otherwise. + pub because: String, } /// A constant (top-level binding to a value). diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index 59ca8b6..7f3485b 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -848,6 +848,7 @@ impl Desugarer { ty: augmented_ty, params: augmented_params, body: body_full, + suppress: vec![], doc: None, })); in_full @@ -1583,6 +1584,7 @@ mod tests { }, params: vec!["xs".into()], body: body_match, + suppress: vec![], doc: None, })], }; @@ -1638,6 +1640,7 @@ mod tests { }, params: vec!["xs".into()], body: original.clone(), + suppress: vec![], doc: None, })], }; @@ -1694,6 +1697,7 @@ mod tests { }, params: vec![], body: fact_letrec_term(), + suppress: vec![], doc: None, })], }; @@ -1781,6 +1785,7 @@ mod tests { tail: false, }), }, + suppress: vec![], doc: None, })], }; @@ -1905,6 +1910,7 @@ mod tests { value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }), body: Box::new(letrec), }, + suppress: vec![], doc: None, })], }; @@ -2018,6 +2024,7 @@ mod tests { }, params: vec!["p".into()], body: outer_body, + suppress: vec![], doc: None, }), ], @@ -2095,6 +2102,7 @@ mod tests { }, params: vec![], body: letrec, + suppress: vec![], doc: None, })], }; @@ -2155,6 +2163,7 @@ mod tests { }, params: vec![], body: letrec, + suppress: vec![], doc: None, })], }; @@ -2291,6 +2300,7 @@ mod tests { }, params: vec!["x".into()], body: letrec, + suppress: vec![], doc: None, })], }; @@ -2392,6 +2402,7 @@ mod tests { }, params: vec!["x".into()], body: letrec, + suppress: vec![], doc: None, })], }; @@ -2472,6 +2483,7 @@ mod tests { }, params: vec![], body: outer, + suppress: vec![], doc: None, })], }; @@ -2551,6 +2563,7 @@ mod tests { }, params: vec![], body: outer, + suppress: vec![], doc: None, })], }; @@ -2671,6 +2684,7 @@ mod tests { }, params: vec!["n".into()], body: body_match, + suppress: vec![], doc: None, })], }; @@ -2743,6 +2757,7 @@ mod tests { }, params: vec!["xs".into()], body: body_match, + suppress: vec![], doc: None, })], }; @@ -2823,6 +2838,7 @@ mod tests { }, params: vec!["n".into()], body: body_match, + suppress: vec![], doc: None, })], }; diff --git a/crates/ailang-core/src/hash.rs b/crates/ailang-core/src/hash.rs index 7480873..96222d1 100644 --- a/crates/ailang-core/src/hash.rs +++ b/crates/ailang-core/src/hash.rs @@ -71,6 +71,7 @@ mod tests { ], tail: false, }, + suppress: vec![], doc: None, }) } @@ -118,4 +119,66 @@ mod tests { let int_list_def = list_mod.defs.iter().find(|d| d.name() == "IntList").unwrap(); assert_eq!(def_hash(int_list_def), "b082192bd0c99202"); } + + /// Iter 19b regression: adding `suppress` to [`crate::ast::FnDef`] + /// must NOT change canonical-JSON hashes of any pre-19b fn whose + /// `suppress` is empty. The `skip_serializing_if = "Vec::is_empty"` + /// predicate on the field is what enforces this; if it is wrong, + /// every existing fixture's hash drifts and `ail diff` / + /// `ail manifest` output breaks. + /// + /// We construct two FnDefs that differ only in `suppress` (one + /// empty, one missing the field). They must hash bit-identically: + /// the canonical-JSON of both is the same byte sequence because + /// the empty Vec is elided. + #[test] + fn iter19b_empty_suppress_preserves_pre_19b_hashes() { + let with_empty_suppress = sample_fn(); + // Mutate the bare sample to set suppress explicitly to a + // non-empty Vec, then mutate it back to empty: two distinct + // construction paths that should still hash identically. + let mut with_explicit_empty = sample_fn(); + if let Def::Fn(ref mut f) = with_explicit_empty { + f.suppress = vec![]; + } + assert_eq!( + def_hash(&with_empty_suppress), + def_hash(&with_explicit_empty), + "two FnDefs with empty suppress must hash identically" + ); + + // And: a FnDef with a *non-empty* suppress hashes + // *differently* (sanity check that the field is in fact in + // the canonical bytes when present). + let mut with_suppress = sample_fn(); + if let Def::Fn(ref mut f) = with_suppress { + f.suppress = vec![crate::ast::Suppress { + code: "over-strict-mode".into(), + because: "test reason".into(), + }]; + } + assert_ne!( + def_hash(&with_empty_suppress), + def_hash(&with_suppress), + "non-empty suppress must produce a distinct hash" + ); + } + + /// Iter 19b: an on-disk pre-19b fixture must still load cleanly + /// (no `suppress` field present in the JSON) and produce its + /// canonical-byte hash unchanged. The hash for `sum.sum` was + /// recorded by the 13a regression and must stay 16 hex chars + /// equal to `db33f57cb329935e` — this test re-asserts it after + /// the 19b schema bump. + #[test] + fn iter19b_schema_extension_preserves_pre_19b_hashes() { + let manifest_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")); + let examples = manifest_dir.join("../../examples"); + + let sum_src = std::fs::read(examples.join("sum.ail.json")) + .expect("examples/sum.ail.json present"); + let sum_mod: crate::ast::Module = serde_json::from_slice(&sum_src).unwrap(); + let sum_def = sum_mod.defs.iter().find(|d| d.name() == "sum").unwrap(); + assert_eq!(def_hash(sum_def), "db33f57cb329935e"); + } } diff --git a/crates/ailang-core/src/pretty.rs b/crates/ailang-core/src/pretty.rs index 2672397..680c458 100644 --- a/crates/ailang-core/src/pretty.rs +++ b/crates/ailang-core/src/pretty.rs @@ -183,6 +183,7 @@ mod tests { ], tail: false, }, + suppress: vec![], doc: None, }), ], diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs index aba87aa..40b1657 100644 --- a/crates/ailang-prose/src/lib.rs +++ b/crates/ailang-prose/src/lib.rs @@ -25,7 +25,8 @@ //! never fails on a well-formed AST. use ailang_core::ast::{ - ConstDef, Ctor, Def, FnDef, Import, Literal, Module, ParamMode, Pattern, Term, Type, TypeDef, + ConstDef, Ctor, Def, FnDef, Import, Literal, Module, ParamMode, Pattern, Suppress, Term, Type, + TypeDef, }; /// Render a [`Module`] as human-readable prose. @@ -79,6 +80,26 @@ fn write_def(out: &mut String, def: &Def, level: usize) { } } +/// Iter 19b: render the [`FnDef::suppress`] list as one +/// `// @suppress : ` line per entry, indented to +/// `level`. Multiple entries stack in declaration order; an empty +/// list produces no output (and therefore no leading blank line). +/// +/// The render is intentionally lossless. The LLM-reader of the +/// prose form needs to see *why* an annotation that looks +/// over-strict is correct on this def; eliding suppressions would +/// hide that contract metadata. +fn write_suppress_lines(out: &mut String, suppress: &[Suppress], level: usize) { + for s in suppress { + indent(out, level); + out.push_str("// @suppress "); + out.push_str(&s.code); + out.push_str(": "); + out.push_str(&s.because); + out.push('\n'); + } +} + fn write_doc(out: &mut String, doc: &Option, level: usize) { if let Some(d) = doc { // Polish 4 (Iter 20b): wrap long lines at 80 columns. @@ -203,6 +224,12 @@ fn write_ctor(out: &mut String, c: &Ctor) { } fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) { + // Iter 19b: render `suppress` entries as `// @suppress : ` + // comment lines **above** the doc string. They are contract metadata + // that the LLM-reader needs to see to understand why an annotation + // that looks over-strict is correct here. One line per entry, in + // declaration order; never elided. + write_suppress_lines(out, &fd.suppress, level); write_doc(out, &fd.doc, level); // The FnDef carries `params` (names) plus the type. The signature // surface combines them slot-for-slot. `fd.ty` is either a @@ -1043,6 +1070,7 @@ mod tests { }, params: vec!["xs".into()], body: Term::Lit { lit: Literal::Int { value: 0 } }, + suppress: vec![], doc: None, }; let mut out = String::new(); @@ -1058,6 +1086,7 @@ mod tests { ty: Type::fn_implicit(vec![], Type::unit(), vec!["IO".into()]), params: vec![], body: Term::Lit { lit: Literal::Unit }, + suppress: vec![], doc: None, }; let mut out = String::new(); @@ -1065,6 +1094,106 @@ mod tests { assert!(out.contains("() -> Unit with IO {"), "got:\n{out}"); } + /// Iter 19b: a FnDef with a single `Suppress` entry renders the + /// `// @suppress : ` line **above** the doc string, + /// preserving both the suppression visibility and the doc content. + /// The suppress line must appear before the `///`-prefixed doc + /// lines, not after; the contract metadata leads. + #[test] + fn fn_def_renders_single_suppress_above_doc() { + let fd = FnDef { + name: "head_or_zero".into(), + ty: Type::Fn { + params: vec![Type::Con { + name: "IntList".into(), + args: vec![], + }], + param_modes: vec![ailang_core::ast::ParamMode::Own], + ret: Box::new(Type::int()), + ret_mode: ailang_core::ast::ParamMode::Implicit, + effects: vec![], + }, + params: vec!["xs".into()], + body: Term::Lit { lit: Literal::Int { value: 0 } }, + suppress: vec![ailang_core::ast::Suppress { + code: "over-strict-mode".into(), + because: "RC codegen test fixture".into(), + }], + doc: Some("Take ownership.".into()), + }; + let mut out = String::new(); + write_fn_def(&mut out, &fd, 0); + // Suppress line is the FIRST line, before the doc. + let first_line = out.lines().next().unwrap(); + assert_eq!( + first_line, "// @suppress over-strict-mode: RC codegen test fixture", + "first line must be the suppress comment; got:\n{out}" + ); + // Doc string follows on the next line. + let lines: Vec<&str> = out.lines().collect(); + assert_eq!(lines[1], "/// Take ownership.", "doc line should follow; got:\n{out}"); + // Fn signature follows the doc. + assert!( + out.contains("fn head_or_zero(xs: own IntList) -> Int"), + "fn signature should follow; got:\n{out}" + ); + } + + /// Iter 19b: multiple `Suppress` entries render as one + /// `// @suppress : ` line each, in declaration + /// order, all above the doc string. + #[test] + fn fn_def_renders_multiple_suppress_in_order() { + let fd = FnDef { + name: "f".into(), + ty: Type::fn_implicit(vec![], Type::int(), vec![]), + params: vec![], + body: Term::Lit { lit: Literal::Int { value: 0 } }, + suppress: vec![ + ailang_core::ast::Suppress { + code: "over-strict-mode".into(), + because: "first reason".into(), + }, + ailang_core::ast::Suppress { + code: "some-other-code".into(), + because: "second reason".into(), + }, + ], + doc: None, + }; + let mut out = String::new(); + write_fn_def(&mut out, &fd, 0); + let lines: Vec<&str> = out.lines().collect(); + assert_eq!(lines[0], "// @suppress over-strict-mode: first reason"); + assert_eq!(lines[1], "// @suppress some-other-code: second reason"); + // Order: declaration order is preserved. + } + + /// Iter 19b: a FnDef with an empty `suppress` Vec emits no + /// `// @suppress` line at all (and therefore no extra leading + /// blank line). Pre-19b prose snapshots stay byte-identical when + /// re-rendered through the 19b code. + #[test] + fn fn_def_with_empty_suppress_emits_no_suppress_lines() { + let fd = FnDef { + name: "f".into(), + ty: Type::fn_implicit(vec![], Type::int(), vec![]), + params: vec![], + body: Term::Lit { lit: Literal::Int { value: 0 } }, + suppress: vec![], + doc: Some("just a doc".into()), + }; + let mut out = String::new(); + write_fn_def(&mut out, &fd, 0); + assert!( + !out.contains("// @suppress"), + "no @suppress line for empty Vec; got:\n{out}" + ); + // The doc still leads. + let first_line = out.lines().next().unwrap(); + assert_eq!(first_line, "/// just a doc"); + } + // ---- Doc string lines ---- #[test] diff --git a/crates/ailang-surface/src/parse.rs b/crates/ailang-surface/src/parse.rs index d72fae4..b4d9d1d 100644 --- a/crates/ailang-surface/src/parse.rs +++ b/crates/ailang-surface/src/parse.rs @@ -14,7 +14,9 @@ //! doc-attr ::= "(" "doc" string ")" //! //! fn-def ::= "(" "fn" ident fn-attr* ")" -//! fn-attr ::= doc-attr | type-attr | params-attr | body-attr +//! fn-attr ::= doc-attr | suppress-attr | type-attr | params-attr | body-attr +//! suppress-attr ::= "(" "suppress" "(" "code" string ")" +//! "(" "because" string ")" ")" //! type-attr ::= "(" "type" type ")" //! params-attr ::= "(" "params" ident* ")" //! body-attr ::= "(" "body" term ")" @@ -83,8 +85,8 @@ //! [`ailang_core::ast::Import::alias`]. use ailang_core::ast::{ - Arm, ConstDef, Ctor, Def, FnDef, Import, Literal, Module, ParamMode, Pattern, Term, Type, - TypeDef, + Arm, ConstDef, Ctor, Def, FnDef, Import, Literal, Module, ParamMode, Pattern, Suppress, Term, + Type, TypeDef, }; use ailang_core::SCHEMA; use thiserror::Error; @@ -474,9 +476,13 @@ impl<'a> Parser<'a> { let mut ty: Option = None; let mut params: Option> = None; let mut body: Option = None; + // Iter 19b: every `(suppress ...)` clause appends one entry. Order + // is preserved (matches the on-disk JSON-AST order). + let mut suppress: Vec = Vec::new(); loop { match self.peek_head_ident() { Some("doc") => doc = Some(self.parse_doc()?), + Some("suppress") => suppress.push(self.parse_suppress_attr()?), Some("type") => { let t = self.parse_type_attr()?; ty = Some(t); @@ -494,7 +500,7 @@ impl<'a> Parser<'a> { return Err(ParseError::Production { production: "fn-def", message: format!( - "unknown fn attribute `{other}`; expected `doc`, `type`, `params`, or `body`" + "unknown fn attribute `{other}`; expected `doc`, `suppress`, `type`, `params`, or `body`" ), pos, }); @@ -524,9 +530,82 @@ impl<'a> Parser<'a> { params, body, doc, + suppress, }) } + /// Iter 19b: parse one `(suppress (code "") (because ""))` + /// clause, returning a [`Suppress`] entry. Unknown sub-keywords + /// inside the clause are rejected with [`ParseError::Production`]. + /// The `because` text is allowed to be empty here (the typechecker + /// emits `empty-suppress-reason` instead of the parser, so the + /// invalid form round-trips through the surface for diagnostic + /// purposes). + fn parse_suppress_attr(&mut self) -> Result { + self.expect_lparen("suppress-attr")?; + self.expect_keyword("suppress")?; + let mut code: Option = None; + let mut because: Option = None; + loop { + match self.peek_head_ident() { + Some("code") => { + self.expect_lparen("suppress.code")?; + self.expect_keyword("code")?; + code = Some(self.expect_string("code body")?); + self.expect_rparen("suppress.code")?; + } + Some("because") => { + self.expect_lparen("suppress.because")?; + self.expect_keyword("because")?; + because = Some(self.expect_string("because body")?); + self.expect_rparen("suppress.because")?; + } + Some(other) => { + let pos = self.peek().map(|t| t.span.start).unwrap_or(0); + return Err(ParseError::Production { + production: "suppress-attr", + message: format!( + "unknown suppress sub-attribute `{other}`; expected `code` or `because`" + ), + pos, + }); + } + None => break, + } + } + self.expect_rparen("suppress-attr")?; + let code = code.ok_or_else(|| ParseError::Production { + production: "suppress-attr", + message: "suppress is missing required `(code ...)`".into(), + pos: 0, + })?; + let because = because.ok_or_else(|| ParseError::Production { + production: "suppress-attr", + message: "suppress is missing required `(because ...)`".into(), + pos: 0, + })?; + Ok(Suppress { code, because }) + } + + /// Iter 19b: helper — consume one string-literal token. Used by + /// [`Self::parse_suppress_attr`]. + fn expect_string(&mut self, ctx: &'static str) -> Result { + match self.peek().cloned() { + Some(Token { tok: Tok::Str(s), .. }) => { + self.cur += 1; + Ok(s) + } + Some(t) => Err(ParseError::Unexpected { + expected: format!("string literal ({ctx})"), + got: tok_label(&t.tok), + pos: t.span.start, + }), + None => Err(ParseError::UnexpectedEof { + expected: format!("string literal ({ctx})"), + }), + } + } + fn parse_type_attr(&mut self) -> Result { self.expect_lparen("type-attr")?; self.expect_keyword("type")?; @@ -1632,4 +1711,133 @@ mod tests { other => panic!("expected LetRec, got {other:?}"), } } + + /// Iter 19b: a `(fn ...)` carrying a single + /// `(suppress (code "...") (because "..."))` clause parses into + /// [`FnDef::suppress`] with the corresponding [`Suppress`] entry. + #[test] + fn parses_single_suppress_clause_on_fn_def() { + let m = crate::parse::parse( + r#" + (module t + (fn f + (suppress (code "over-strict-mode") (because "test reason")) + (type (fn-type (params) (ret (con Int)))) + (params) + (body 0))) + "#, + ) + .unwrap(); + match &m.defs[0] { + Def::Fn(fd) => { + assert_eq!(fd.suppress.len(), 1); + assert_eq!(fd.suppress[0].code, "over-strict-mode"); + assert_eq!(fd.suppress[0].because, "test reason"); + } + _ => panic!("expected fn"), + } + } + + /// Iter 19b: multiple `(suppress ...)` clauses accumulate into + /// `FnDef::suppress` in declaration order. A second clause does + /// NOT overwrite the first. + #[test] + fn parses_multiple_suppress_clauses_in_order() { + let m = crate::parse::parse( + r#" + (module t + (fn f + (suppress (code "over-strict-mode") (because "first")) + (suppress (code "other-code") (because "second")) + (type (fn-type (params) (ret (con Int)))) + (params) + (body 0))) + "#, + ) + .unwrap(); + match &m.defs[0] { + Def::Fn(fd) => { + assert_eq!(fd.suppress.len(), 2); + assert_eq!(fd.suppress[0].code, "over-strict-mode"); + assert_eq!(fd.suppress[0].because, "first"); + assert_eq!(fd.suppress[1].code, "other-code"); + assert_eq!(fd.suppress[1].because, "second"); + } + _ => panic!("expected fn"), + } + } + + /// Iter 19b: a `(fn ...)` without a `(suppress ...)` clause has + /// `FnDef::suppress` empty (the default — round-trip identity + /// with pre-19b fixtures). + #[test] + fn parses_fn_def_without_suppress_has_empty_vec() { + let m = crate::parse::parse( + r#" + (module t + (fn f + (type (fn-type (params) (ret (con Int)))) + (params) + (body 0))) + "#, + ) + .unwrap(); + match &m.defs[0] { + Def::Fn(fd) => { + assert!(fd.suppress.is_empty()); + } + _ => panic!("expected fn"), + } + } + + /// Iter 19b: a `(suppress ...)` with `(because "")` (empty + /// reason) still parses cleanly — the parser is intentionally + /// permissive; the typechecker is what emits + /// `empty-suppress-reason`. This keeps the surface symmetric + /// (a malformed input round-trips through the printer for + /// diagnostic display). + #[test] + fn parses_suppress_with_empty_because_string() { + let m = crate::parse::parse( + r#" + (module t + (fn f + (suppress (code "over-strict-mode") (because "")) + (type (fn-type (params) (ret (con Int)))) + (params) + (body 0))) + "#, + ) + .unwrap(); + match &m.defs[0] { + Def::Fn(fd) => { + assert_eq!(fd.suppress.len(), 1); + assert_eq!(fd.suppress[0].because, ""); + } + _ => panic!("expected fn"), + } + } + + /// Iter 19b: an unknown sub-attribute inside `(suppress ...)` + /// produces a `ParseError::Production` naming the bad keyword and + /// listing the legal ones (`code` / `because`). + #[test] + fn rejects_suppress_with_unknown_subattribute() { + let err = crate::parse::parse( + r#" + (module t + (fn f + (suppress (code "over-strict-mode") (because "ok") (oops "x")) + (type (fn-type (params) (ret (con Int)))) + (params) + (body 0))) + "#, + ) + .unwrap_err(); + let msg = format!("{err}"); + assert!( + msg.contains("oops") && msg.contains("code") && msg.contains("because"), + "error should name the bad keyword and the legal ones; got: {msg}" + ); + } } diff --git a/crates/ailang-surface/src/print.rs b/crates/ailang-surface/src/print.rs index ccac716..f516f9d 100644 --- a/crates/ailang-surface/src/print.rs +++ b/crates/ailang-surface/src/print.rs @@ -8,8 +8,8 @@ //! per level. Comments are NOT emitted. use ailang_core::ast::{ - Arm, ConstDef, Ctor, Def, FnDef, Import, Literal, Module, ParamMode, Pattern, Term, Type, - TypeDef, + Arm, ConstDef, Ctor, Def, FnDef, Import, Literal, Module, ParamMode, Pattern, Suppress, Term, + Type, TypeDef, }; /// Print a module in form (A). @@ -153,6 +153,13 @@ fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) { write_string_lit(out, doc); out.push(')'); } + // Iter 19b: emit one `(suppress ...)` clause per entry, after the + // doc string and before the type. Round-trip stable: parser + // re-reads each clause back into [`FnDef::suppress`]. + for s in &fd.suppress { + out.push('\n'); + write_suppress(out, s, level + 1); + } out.push('\n'); indent(out, level + 1); out.push_str("(type "); @@ -174,6 +181,18 @@ fn write_fn_def(out: &mut String, fd: &FnDef, level: usize) { out.push(')'); } +/// Iter 19b: print one `(suppress (code "") (because ""))` +/// clause. Indentation matches the rest of the fn-def (one level +/// deeper than the `(fn ...)` head). +fn write_suppress(out: &mut String, s: &Suppress, level: usize) { + indent(out, level); + out.push_str("(suppress (code "); + write_string_lit(out, &s.code); + out.push_str(") (because "); + write_string_lit(out, &s.because); + out.push_str("))"); +} + fn write_const_def(out: &mut String, cd: &ConstDef, level: usize) { indent(out, level); out.push_str("(const "); diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 165745d..bc77c29 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -9335,3 +9335,110 @@ real corpus surfaces it. and `over_strict_mode_fires_when_match_arm_binders_unused`. `ailang-check` test count: 53 → 55. Workspace build/test green. + +## 2026-05-08 — Iter 19b: `mode-strict-because` suppression shipped + +The closer to the 19a/19a.1 arc. Corpus signal from 19a.1 +(5/65 fixtures fired `over-strict-mode`, all deliberate RC +codegen-test fixtures) justified shipping the suppress mechanism +end-to-end. + +### Schema + +`Suppress { code, because }` struct in `ailang-core::ast`. New +`FnDef::suppress: Vec` field with +`skip_serializing_if = "Vec::is_empty"` so pre-19b fixtures keep +bit-identical canonical-JSON hashes (regression-pinned by the +existing hash-stability test, plus 2 new ones). + +### Typechecker + +New `suppress_filter` module in `ailang-check`. Per-module +post-pass: + + - For each `Def::Fn` with non-empty `suppress`, drop diagnostics + matching `(def, code)` from the accumulated list. + - Emit `empty-suppress-reason` (Error severity) for any + suppress entry whose `because` is whitespace-only. + - Wrong codes (e.g. suppressing `type-mismatch` when only + `over-strict-mode` would fire) are silent no-ops — open-set + registry rationale documented. + +### Form-A surface + +Grammar: `(suppress (code "...") (because "..."))`, between fn +name and `(type ...)`. Multiple clauses allowed. Round-trip test +pinning (parse → print → re-parse → canonical-byte equality) holds +on all fixtures including the 5 RC ones that gained suppress. + +### Form-B prose + +Renders one `// @suppress : ` line per entry, ABOVE +the doc string. Lossless — contract metadata, not stringency +machinery; the LLM-reader of prose needs to see *why* an +annotation that looks over-strict is correct on this def. + +Concrete shape from `rc_own_param_drop.prose.txt`: + +``` +// @suppress over-strict-mode: RC codegen test: exercises Iter B Own-param dec at fn return +/// Take ownership of an IntList; return its head if Cons, else 0... +fn head_or_zero(xs: own IntList) -> Int { + ... +} +``` + +### Fixture migration + +Five `.ail.json` files gained suppress entries; `.ailx` siblings +regenerated via `ail render`; three of the four pinned `.prose.txt` +snapshots regenerated (the fourth, `bench_list_sum`, has no Own +params and is unchanged). The migration documented per-fixture +reason text matches the codegen-test path each fixture exercises. + +### Corpus signal after migration + +`over-strict-mode` warnings across all 65 fixtures: **5 → 0**. All +five RC codegen-test fixtures now check clean while preserving +their `(own T)` annotation as deliberate test infrastructure. The +lint still fires on any future fn that's accidentally over-strict +without an authored reason. + +### Test counts + +- `ailang-check`: 55 → 61 (6 new `suppress_filter` tests) +- `ailang-core`: 26 → 28 (2 hash-stability tests) +- `ailang-surface`: 21 → 26 (5 parse tests) +- `ailang-prose`: 49 → 52 (3 prose-render tests) +- `e2e`: 70 (unchanged) + +### Known debt + + - **`.ailx` comment headers lost.** The five regenerated `.ailx` + files lost their hand-written comment headers — `ail render`'s + contract excludes comment preservation. If those headers are + needed back, that's a separate iter (probably a comment- + preserving printer mode). + - **Duplicate-attr detection.** `parse_suppress_attr` accepts + `(code …)` and `(because …)` in either order but does not + detect duplicates within a single `(suppress …)` clause; a + second `(code …)` silently overwrites. The canonical printer + emits in fixed order, so the only way to construct duplicates + is hand-writing weird input — bounded. + - **Cross-iter snapshot coupling** (architect's deferred item 3 + from 20e): adding suppress to RC fixtures invalidated three + snapshots. They were already pinned by family 20; this iter + re-rendered them. Same pattern will recur on any future iter + that touches those fixtures. + +### Family / arc state + +The 19a/19a.1/19b arc is now closed: + - 19a: `over-strict-mode` lint + Severity::Warning surface + - 19a.1: precise sub-binder analysis (heap-type filter) + - 19b: `mode-strict-because` suppression + 5-fixture migration + +JOURNAL queue: empty again. Three pre-existing 20b deferrals +(let-inlining, `print` sugar, deeply-nested-match-on-sub-binder +in 19a.1) remain queued; all three need real-corpus signal that +hasn't surfaced. diff --git a/examples/rc_app_let_partial_drop_leak.ail.json b/examples/rc_app_let_partial_drop_leak.ail.json index 36f084b..906991f 100644 --- a/examples/rc_app_let_partial_drop_leak.ail.json +++ b/examples/rc_app_let_partial_drop_leak.ail.json @@ -1 +1 @@ -{"defs":[{"ctors":[{"fields":[{"k":"con","name":"Int"}],"name":"MkWrap"}],"kind":"type","name":"Wrap"},{"ctors":[{"fields":[{"k":"con","name":"Wrap"},{"k":"con","name":"Wrap"}],"name":"MkCell"}],"kind":"type","name":"Cell"},{"ctors":[{"fields":[{"k":"con","name":"Cell"},{"k":"con","name":"Cell"}],"name":"MkPair"}],"kind":"type","name":"Pair"},{"body":{"args":[{"args":[{"args":[{"name":"n","t":"var"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"},{"args":[{"args":[{"lit":{"kind":"int","value":3},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":4},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"kind":"fn","name":"build_pair","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Pair"},"ret_mode":"own"}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"ctor":"MkCell","fields":[{"name":"w1","p":"var"},{"name":"w2","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"c","t":"var"},"t":"match"},"kind":"fn","name":"use_cell","params":["c"],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"Cell"}],"ret":{"k":"con","name":"Int"}}},{"body":{"body":{"args":[{"arms":[{"body":{"args":[{"name":"a","t":"var"}],"fn":{"name":"use_cell","t":"var"},"t":"app"},"pat":{"ctor":"MkPair","fields":[{"name":"a","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"}],"op":"io/print_int","t":"do"},"name":"p","t":"let","value":{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"build_pair","t":"var"},"t":"app"}},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_app_let_partial_drop_leak","schema":"ailang/v0"} \ No newline at end of file +{"defs":[{"ctors":[{"fields":[{"k":"con","name":"Int"}],"name":"MkWrap"}],"kind":"type","name":"Wrap"},{"ctors":[{"fields":[{"k":"con","name":"Wrap"},{"k":"con","name":"Wrap"}],"name":"MkCell"}],"kind":"type","name":"Cell"},{"ctors":[{"fields":[{"k":"con","name":"Cell"},{"k":"con","name":"Cell"}],"name":"MkPair"}],"kind":"type","name":"Pair"},{"body":{"args":[{"args":[{"args":[{"name":"n","t":"var"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"},{"args":[{"args":[{"lit":{"kind":"int","value":3},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":4},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"kind":"fn","name":"build_pair","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Pair"},"ret_mode":"own"}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"ctor":"MkCell","fields":[{"name":"w1","p":"var"},{"name":"w2","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"c","t":"var"},"t":"match"},"kind":"fn","name":"use_cell","params":["c"],"suppress":[{"because":"RC codegen test: shape used to feed App-bound let-close partial-drop into use_cell","code":"over-strict-mode"}],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"Cell"}],"ret":{"k":"con","name":"Int"}}},{"body":{"body":{"args":[{"arms":[{"body":{"args":[{"name":"a","t":"var"}],"fn":{"name":"use_cell","t":"var"},"t":"app"},"pat":{"ctor":"MkPair","fields":[{"name":"a","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"}],"op":"io/print_int","t":"do"},"name":"p","t":"let","value":{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"build_pair","t":"var"},"t":"app"}},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_app_let_partial_drop_leak","schema":"ailang/v0"} diff --git a/examples/rc_app_let_partial_drop_leak.ailx b/examples/rc_app_let_partial_drop_leak.ailx index 5580c0e..c2ac681 100644 --- a/examples/rc_app_let_partial_drop_leak.ailx +++ b/examples/rc_app_let_partial_drop_leak.ailx @@ -1,69 +1,22 @@ -; Iter 18g.tidy.fu2 RED-test fixture 3/3: dynamic-tag partial-drop -; carve-out at let-close for an App-bound binder -; (drop.rs:580 fallback in `emit_inlined_partial_drop`). -; -; Shape: -; - Same `Pair`/`Cell`/`Wrap` types as fixtures 1 and 2. -; - `main` let-binds `p = (app build_pair)` — value is -; `Term::App` (Own-returning), `is_rc_heap_allocated` returns -; true → trackable. -; - Body matches `p` as `MkPair a _` — slot 0 bound, slot 1 wild. -; `moved_slots[p] = {0}`. -; - `a` is consumed by `use_cell` (Own param) → `consume_count[a] -; == 1`, arm-close drop skipped. `use_cell`'s body fully -; destructures `a` and returns Int. -; - At p's let-close: `consume_count[p] == 0`, `moves[p] = {0}` -; non-empty, `value` is `Term::App` (not `Term::Ctor`) → -; `emit_inlined_partial_drop` falls into the non-Ctor branch -; (drop.rs:580) → shallow `ailang_rc_dec(p)`. p's outer cell -; is freed; slot 1 (the second MkCell + its two MkWraps = -; 3 cells) leaks. -; -; Pre-fix: live = 3 (one MkCell + two MkWrap children in slot 1). -; Post-fix: live = 0. - (module rc_app_let_partial_drop_leak - (data Wrap (ctor MkWrap (con Int))) - (data Cell (ctor MkCell (con Wrap) (con Wrap))) - (data Pair (ctor MkPair (con Cell) (con Cell))) - (fn build_pair - (type - (fn-type - (params (con Int)) - (ret (own (con Pair))))) + (type (fn-type (params (con Int)) (ret (own (con Pair))))) (params n) - (body - (term-ctor Pair MkPair - (term-ctor Cell MkCell - (term-ctor Wrap MkWrap n) - (term-ctor Wrap MkWrap 2)) - (term-ctor Cell MkCell - (term-ctor Wrap MkWrap 3) - (term-ctor Wrap MkWrap 4))))) - + (body (term-ctor Pair MkPair (term-ctor Cell MkCell (term-ctor Wrap MkWrap n) (term-ctor Wrap MkWrap 2)) (term-ctor Cell MkCell (term-ctor Wrap MkWrap 3) (term-ctor Wrap MkWrap 4))))) (fn use_cell - (type - (fn-type - (params (own (con Cell))) - (ret (con Int)))) + (suppress (code "over-strict-mode") (because "RC codegen test: shape used to feed App-bound let-close partial-drop into use_cell")) + (type (fn-type (params (own (con Cell))) (ret (con Int)))) (params c) - (body - (match c - (case (pat-ctor MkCell w1 w2) 1)))) - + (body (match c + (case (pat-ctor MkCell w1 w2) 1)))) (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) - (body - (let p (app build_pair 1) - (do io/print_int - (match p - (case (pat-ctor MkPair a _) - (app use_cell a)))))))) + (body (let p (app build_pair 1) (do io/print_int (match p + (case (pat-ctor MkPair a _) (app use_cell a)))))))) diff --git a/examples/rc_app_let_partial_drop_leak.prose.txt b/examples/rc_app_let_partial_drop_leak.prose.txt index 7448e3c..cb95cdc 100644 --- a/examples/rc_app_let_partial_drop_leak.prose.txt +++ b/examples/rc_app_let_partial_drop_leak.prose.txt @@ -10,6 +10,7 @@ fn build_pair(n: Int) -> own Pair { MkPair(MkCell(MkWrap(n), MkWrap(2)), MkCell(MkWrap(3), MkWrap(4))) } +// @suppress over-strict-mode: RC codegen test: shape used to feed App-bound let-close partial-drop into use_cell fn use_cell(c: own Cell) -> Int { match c { MkCell(w1, w2) => 1 diff --git a/examples/rc_drop_iterative_long_list.ail.json b/examples/rc_drop_iterative_long_list.ail.json index 4fac266..cf80367 100644 --- a/examples/rc_drop_iterative_long_list.ail.json +++ b/examples/rc_drop_iterative_long_list.ail.json @@ -1 +1 @@ -{"defs":[{"ctors":[{"fields":[],"name":"INil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"ICons"}],"drop-iterative":true,"kind":"type","name":"IntList"},{"body":{"cond":{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"},"else":{"args":[{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"},{"args":[{"name":"n","t":"var"},{"name":"acc","t":"var"}],"ctor":"ICons","t":"ctor","type":"IntList"}],"fn":{"name":"cons_n_acc","t":"var"},"t":"app","tail":true},"t":"if","then":{"name":"acc","t":"var"}},"doc":"Tail-recursive list builder. acc-prepended.","kind":"fn","name":"cons_n_acc","params":["n","acc"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"IntList"}}},{"body":{"args":[{"name":"n","t":"var"},{"args":[],"ctor":"INil","t":"ctor","type":"IntList"}],"fn":{"name":"cons_n_acc","t":"var"},"t":"app"},"doc":"Build [1, 2, ..., n] :: IntList. Order is reverse of build but immaterial for head/sum.","kind":"fn","name":"cons_n","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"IntList"}}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"INil","fields":[],"p":"ctor"}},{"body":{"name":"h","t":"var"},"pat":{"ctor":"ICons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Take ownership of an IntList; return its head if ICons, else 0. The (own ...) signature signals 18d.4 to emit an Own-param drop at fn return — which under the (drop-iterative) annotation is the iterative-worklist body, freeing the entire chain via the heap-allocated worklist instead of recursive cascade.","kind":"fn","name":"head_or_zero","params":["xs"],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1000000},"t":"lit"}],"fn":{"name":"cons_n","t":"var"},"t":"app"}],"fn":{"name":"head_or_zero","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_drop_iterative_long_list","schema":"ailang/v0"} \ No newline at end of file +{"defs":[{"ctors":[{"fields":[],"name":"INil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"ICons"}],"drop-iterative":true,"kind":"type","name":"IntList"},{"body":{"cond":{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":0},"t":"lit"}],"fn":{"name":"==","t":"var"},"t":"app"},"else":{"args":[{"args":[{"name":"n","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"-","t":"var"},"t":"app"},{"args":[{"name":"n","t":"var"},{"name":"acc","t":"var"}],"ctor":"ICons","t":"ctor","type":"IntList"}],"fn":{"name":"cons_n_acc","t":"var"},"t":"app","tail":true},"t":"if","then":{"name":"acc","t":"var"}},"doc":"Tail-recursive list builder. acc-prepended.","kind":"fn","name":"cons_n_acc","params":["n","acc"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"IntList"}}},{"body":{"args":[{"name":"n","t":"var"},{"args":[],"ctor":"INil","t":"ctor","type":"IntList"}],"fn":{"name":"cons_n_acc","t":"var"},"t":"app"},"doc":"Build [1, 2, ..., n] :: IntList. Order is reverse of build but immaterial for head/sum.","kind":"fn","name":"cons_n","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"IntList"}}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"INil","fields":[],"p":"ctor"}},{"body":{"name":"h","t":"var"},"pat":{"ctor":"ICons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Take ownership of an IntList; return its head if ICons, else 0. The (own ...) signature signals 18d.4 to emit an Own-param drop at fn return — which under the (drop-iterative) annotation is the iterative-worklist body, freeing the entire chain via the heap-allocated worklist instead of recursive cascade.","kind":"fn","name":"head_or_zero","params":["xs"],"suppress":[{"because":"Iter 18e test: forces (drop-iterative) cascade via Own-param drop at fn return","code":"over-strict-mode"}],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1000000},"t":"lit"}],"fn":{"name":"cons_n","t":"var"},"t":"app"}],"fn":{"name":"head_or_zero","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_drop_iterative_long_list","schema":"ailang/v0"} diff --git a/examples/rc_drop_iterative_long_list.ailx b/examples/rc_drop_iterative_long_list.ailx index 6c51042..7b2452a 100644 --- a/examples/rc_drop_iterative_long_list.ailx +++ b/examples/rc_drop_iterative_long_list.ailx @@ -1,93 +1,27 @@ -; Iter 18e fixture: `(drop-iterative)` opt-in annotation drives the -; codegen to emit `drop__IntList` with a worklist body in place -; of the recursive cascade. Without the annotation, freeing a long -; list overflows Linux's default 8MB stack at ~1M cells (one frame -; per recursive `drop__IntList(tail)` call). With it, the chain -; pops through the heap-allocated worklist in O(N) time and O(1) -; stack. -; -; The fixture builds a 100,000-cell IntList tail-recursively, sums -; it into 4_999_950_000 (= N*(N-1)/2 for N=100_000), then `main` -; returns. At process exit the build's `xs` binder is consumed by -; sum_acc (via tail-call), so the iterative drop fires inside -; sum_acc's `Cons` arm — specifically, on every recursive step the -; tail t is bound, then t is consumed by the next iteration's -; tail-app sum_acc, leaving no live cells at termination. -; -; Wait — under the actual emission shape: sum_acc's xs param is -; (own (con IntList)); 18d.4 emits an Own-param drop at fn return. -; On the inductive Cons arm, the fn returns via tail-call into the -; next iteration (musttail), and the Own-param dec on xs at the -; outer fn would normally fire — but tail-call elision means the -; outer frame is gone before any post-tail-call code can run. The -; canonical case for the iterative-drop test is therefore the -; let-close-drop on `xs` in `main` (or the outer-let's drop after -; sum's tail returns). For 18e the load-bearing property is "long -; chains drop without overflowing the stack"; that fires whenever -; ANY drop call against the head IntList runs end-to-end. -; -; To force the issue: `main` builds the list, sums it, prints the -; sum, AND then `let xs = build n in let _ = sum xs in xs` does NOT -; exist as a pattern in AILang. We instead route the list through a -; `head` fn that takes (own IntList) and returns the head Int — -; which transfers ownership and forces the Own-param drop on xs at -; head's return. Because head's body (a match returning Int) cannot -; be tail-called, the drop is emitted in head's epilogue and runs -; in full before head returns to main. -; -; Expected stdout: `1` (the head of [1, 2, ..., 1_000_000]). -; Why 1M and not 100K: at 100K the recursive cascade fits in the 8MB -; default Linux stack (~64B/frame ≈ 6.4MB at 100K), so the test would -; "pass" even without the iterative drop — false-negative on the -; whole point of 18e. At 1M it overflows clean (SIGSEGV in the -; recursive variant; clean exit-0 in the iterative variant). - (module rc_drop_iterative_long_list - (data IntList (ctor INil) (ctor ICons (con Int) (con IntList)) (drop-iterative)) - (fn cons_n_acc (doc "Tail-recursive list builder. acc-prepended.") - (type - (fn-type - (params (con Int) (con IntList)) - (ret (con IntList)))) + (type (fn-type (params (con Int) (con IntList)) (ret (con IntList)))) (params n acc) - (body - (if (app == n 0) - acc - (tail-app cons_n_acc - (app - n 1) - (term-ctor IntList ICons n acc))))) - + (body (if (app == n 0) acc (tail-app cons_n_acc (app - n 1) (term-ctor IntList ICons n acc))))) (fn cons_n (doc "Build [1, 2, ..., n] :: IntList. Order is reverse of build but immaterial for head/sum.") - (type - (fn-type - (params (con Int)) - (ret (con IntList)))) + (type (fn-type (params (con Int)) (ret (con IntList)))) (params n) - (body - (app cons_n_acc n (term-ctor IntList INil)))) - + (body (app cons_n_acc n (term-ctor IntList INil)))) (fn head_or_zero (doc "Take ownership of an IntList; return its head if ICons, else 0. The (own ...) signature signals 18d.4 to emit an Own-param drop at fn return — which under the (drop-iterative) annotation is the iterative-worklist body, freeing the entire chain via the heap-allocated worklist instead of recursive cascade.") - (type - (fn-type - (params (own (con IntList))) - (ret (con Int)))) + (suppress (code "over-strict-mode") (because "Iter 18e test: forces (drop-iterative) cascade via Own-param drop at fn return")) + (type (fn-type (params (own (con IntList))) (ret (con Int)))) (params xs) - (body - (match xs - (case (pat-ctor INil) 0) - (case (pat-ctor ICons h t) h)))) - + (body (match xs + (case (pat-ctor INil) 0) + (case (pat-ctor ICons h t) h)))) (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) - (body - (do io/print_int - (app head_or_zero (app cons_n 1000000)))))) + (body (do io/print_int (app head_or_zero (app cons_n 1000000)))))) diff --git a/examples/rc_match_arm_partial_drop_leak.ail.json b/examples/rc_match_arm_partial_drop_leak.ail.json index f3eb285..f0106ed 100644 --- a/examples/rc_match_arm_partial_drop_leak.ail.json +++ b/examples/rc_match_arm_partial_drop_leak.ail.json @@ -1 +1 @@ -{"defs":[{"ctors":[{"fields":[{"k":"con","name":"Int"}],"name":"MkWrap"}],"kind":"type","name":"Wrap"},{"ctors":[{"fields":[{"k":"con","name":"Wrap"},{"k":"con","name":"Wrap"}],"name":"MkCell"}],"kind":"type","name":"Cell"},{"ctors":[{"fields":[{"k":"con","name":"Cell"},{"k":"con","name":"Cell"}],"name":"MkPair"}],"kind":"type","name":"Pair"},{"body":{"args":[{"args":[{"args":[{"name":"n","t":"var"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"},{"args":[{"args":[{"lit":{"kind":"int","value":3},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":4},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"kind":"fn","name":"build_pair","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Pair"},"ret_mode":"own"}},{"body":{"arms":[{"body":{"arms":[{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"ctor":"MkCell","fields":[{"name":"w1","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"a","t":"var"},"t":"match"},"pat":{"ctor":"MkPair","fields":[{"name":"a","p":"var"},{"name":"b","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"kind":"fn","name":"use_first","params":["p"],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"Pair"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"build_pair","t":"var"},"t":"app"}],"fn":{"name":"use_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_match_arm_partial_drop_leak","schema":"ailang/v0"} \ No newline at end of file +{"defs":[{"ctors":[{"fields":[{"k":"con","name":"Int"}],"name":"MkWrap"}],"kind":"type","name":"Wrap"},{"ctors":[{"fields":[{"k":"con","name":"Wrap"},{"k":"con","name":"Wrap"}],"name":"MkCell"}],"kind":"type","name":"Cell"},{"ctors":[{"fields":[{"k":"con","name":"Cell"},{"k":"con","name":"Cell"}],"name":"MkPair"}],"kind":"type","name":"Pair"},{"body":{"args":[{"args":[{"args":[{"name":"n","t":"var"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"},{"args":[{"args":[{"lit":{"kind":"int","value":3},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":4},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"kind":"fn","name":"build_pair","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Pair"},"ret_mode":"own"}},{"body":{"arms":[{"body":{"arms":[{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"ctor":"MkCell","fields":[{"name":"w1","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"a","t":"var"},"t":"match"},"pat":{"ctor":"MkPair","fields":[{"name":"a","p":"var"},{"name":"b","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"kind":"fn","name":"use_first","params":["p"],"suppress":[{"because":"RC codegen test: exercises Iter A outer-arm-close partial-drop","code":"over-strict-mode"}],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"Pair"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"build_pair","t":"var"},"t":"app"}],"fn":{"name":"use_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_match_arm_partial_drop_leak","schema":"ailang/v0"} diff --git a/examples/rc_match_arm_partial_drop_leak.ailx b/examples/rc_match_arm_partial_drop_leak.ailx index 2395757..4bf6285 100644 --- a/examples/rc_match_arm_partial_drop_leak.ailx +++ b/examples/rc_match_arm_partial_drop_leak.ailx @@ -1,71 +1,22 @@ -; Iter 18g.tidy.fu2 RED-test fixture 2/3: dynamic-tag partial-drop -; carve-out at outer-arm-close pattern-binder dec -; (Iter A / match_lower.rs:839). -; -; Shape: -; - `Pair` carries two `Cell` fields; `Cell` carries two `Wrap` -; fields. (Same types as fixture 1.) -; - `use_first` takes `(own Pair)` and the OUTER match binds both -; slots: `MkPair a b`. -; - The arm body INNER-matches `a` as `MkCell w1 _` — slot 0 of -; a is bound, slot 1 is wildcarded. -; - Inner arm-close drops `w1` properly via `drop__Wrap`. -; Inner match adds slot 0 to `moved_slots[a]`. -; - Outer arm-close drops `a` and `b`. `a` has `moves={0}` -; (non-empty) and `consume_count==0` (only Borrow use as -; scrutinee of inner match) → Iter A's dynamic-tag carve-out -; fires: shallow `ailang_rc_dec(a)`. a's outer Cell is freed, -; but slot 1 (the unbound MkWrap(2) cell) leaks. -; - `b` has `moves={}` and `consume_count==0` → routes through -; `drop__Cell(b)` which cascades through both Wraps. No -; leak from b. -; - At fn return, `p`'s `moves={0,1}` (both slots bound) → Iter -; B carve-out fires too, but with all slots moved, the shallow -; dec is correct (no additional leak from p). -; -; Pre-fix: live = 1 (the unbound MkWrap(2) cell in slot 1 of a). -; Post-fix: live = 0. - (module rc_match_arm_partial_drop_leak - (data Wrap (ctor MkWrap (con Int))) - (data Cell (ctor MkCell (con Wrap) (con Wrap))) - (data Pair (ctor MkPair (con Cell) (con Cell))) - (fn build_pair - (type - (fn-type - (params (con Int)) - (ret (own (con Pair))))) + (type (fn-type (params (con Int)) (ret (own (con Pair))))) (params n) - (body - (term-ctor Pair MkPair - (term-ctor Cell MkCell - (term-ctor Wrap MkWrap n) - (term-ctor Wrap MkWrap 2)) - (term-ctor Cell MkCell - (term-ctor Wrap MkWrap 3) - (term-ctor Wrap MkWrap 4))))) - + (body (term-ctor Pair MkPair (term-ctor Cell MkCell (term-ctor Wrap MkWrap n) (term-ctor Wrap MkWrap 2)) (term-ctor Cell MkCell (term-ctor Wrap MkWrap 3) (term-ctor Wrap MkWrap 4))))) (fn use_first - (type - (fn-type - (params (own (con Pair))) - (ret (con Int)))) + (suppress (code "over-strict-mode") (because "RC codegen test: exercises Iter A outer-arm-close partial-drop")) + (type (fn-type (params (own (con Pair))) (ret (con Int)))) (params p) - (body - (match p - (case (pat-ctor MkPair a b) - (match a - (case (pat-ctor MkCell w1 _) 1)))))) - + (body (match p + (case (pat-ctor MkPair a b) (match a + (case (pat-ctor MkCell w1 _) 1)))))) (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) - (body - (do io/print_int (app use_first (app build_pair 1)))))) + (body (do io/print_int (app use_first (app build_pair 1)))))) diff --git a/examples/rc_match_arm_partial_drop_leak.prose.txt b/examples/rc_match_arm_partial_drop_leak.prose.txt index 036b4c5..11e76df 100644 --- a/examples/rc_match_arm_partial_drop_leak.prose.txt +++ b/examples/rc_match_arm_partial_drop_leak.prose.txt @@ -10,6 +10,7 @@ fn build_pair(n: Int) -> own Pair { MkPair(MkCell(MkWrap(n), MkWrap(2)), MkCell(MkWrap(3), MkWrap(4))) } +// @suppress over-strict-mode: RC codegen test: exercises Iter A outer-arm-close partial-drop fn use_first(p: own Pair) -> Int { match p { MkPair(a, b) => match a { diff --git a/examples/rc_own_param_drop.ail.json b/examples/rc_own_param_drop.ail.json index b51d58f..fc5d8a0 100644 --- a/examples/rc_own_param_drop.ail.json +++ b/examples/rc_own_param_drop.ail.json @@ -1 +1 @@ -{"defs":[{"ctors":[{"fields":[],"name":"Nil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"Cons"}],"doc":"Recursive Int list — boxed.","kind":"type","name":"IntList"},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"name":"h","t":"var"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Take ownership of an IntList; return its head if Cons, else 0. The tail is loaded as a pattern binder but never consumed — iter A dec's it at arm close. The outer cell is dec'd at fn return via iter B's Own-param emission.","kind":"fn","name":"head_or_zero","params":["xs"],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Int"}}},{"body":{"body":{"args":[{"args":[{"name":"xs","t":"var"}],"fn":{"name":"head_or_zero","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"name":"xs","t":"let","value":{"args":[{"lit":{"kind":"int","value":11},"t":"lit"},{"args":[{"lit":{"kind":"int","value":22},"t":"lit"},{"args":[{"lit":{"kind":"int","value":33},"t":"lit"},{"args":[{"lit":{"kind":"int","value":44},"t":"lit"},{"args":[{"lit":{"kind":"int","value":55},"t":"lit"},{"args":[],"ctor":"Nil","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}},"doc":"Build a 5-element IntList; pass to head_or_zero (transferring ownership); print the result.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_own_param_drop","schema":"ailang/v0"} \ No newline at end of file +{"defs":[{"ctors":[{"fields":[],"name":"Nil"},{"fields":[{"k":"con","name":"Int"},{"k":"con","name":"IntList"}],"name":"Cons"}],"doc":"Recursive Int list — boxed.","kind":"type","name":"IntList"},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":0},"t":"lit"},"pat":{"ctor":"Nil","fields":[],"p":"ctor"}},{"body":{"name":"h","t":"var"},"pat":{"ctor":"Cons","fields":[{"name":"h","p":"var"},{"name":"t","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"xs","t":"var"},"t":"match"},"doc":"Take ownership of an IntList; return its head if Cons, else 0. The tail is loaded as a pattern binder but never consumed — iter A dec's it at arm close. The outer cell is dec'd at fn return via iter B's Own-param emission.","kind":"fn","name":"head_or_zero","params":["xs"],"suppress":[{"because":"RC codegen test: exercises Iter B Own-param dec at fn return","code":"over-strict-mode"}],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"IntList"}],"ret":{"k":"con","name":"Int"}}},{"body":{"body":{"args":[{"args":[{"name":"xs","t":"var"}],"fn":{"name":"head_or_zero","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"name":"xs","t":"let","value":{"args":[{"lit":{"kind":"int","value":11},"t":"lit"},{"args":[{"lit":{"kind":"int","value":22},"t":"lit"},{"args":[{"lit":{"kind":"int","value":33},"t":"lit"},{"args":[{"lit":{"kind":"int","value":44},"t":"lit"},{"args":[{"lit":{"kind":"int","value":55},"t":"lit"},{"args":[],"ctor":"Nil","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}],"ctor":"Cons","t":"ctor","type":"IntList"}},"doc":"Build a 5-element IntList; pass to head_or_zero (transferring ownership); print the result.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_own_param_drop","schema":"ailang/v0"} diff --git a/examples/rc_own_param_drop.ailx b/examples/rc_own_param_drop.ailx index 89b6f54..2cf3339 100644 --- a/examples/rc_own_param_drop.ailx +++ b/examples/rc_own_param_drop.ailx @@ -1,62 +1,18 @@ -; Iter 18d.4 — Own-param dec at fn return. -; -; Companion fixture to `alloc_rc_borrow_only_recursive_list_drop`. -; Here the static "caller handed off ownership" signal is the -; explicit `(own (con IntList))` parameter mode on `head_or_zero`. -; Under --alloc=rc, codegen now emits a drop call against the -; param SSA (`%arg_xs`) before the fn's `ret`, closing the -; symmetric debt 18c.3/18c.4 carried. -; -; Fixture shape: -; - `head_or_zero` takes `(own (con IntList))` and returns Int. -; Body destructures via match, returns the head in the Cons -; arm (ignoring the tail) and 0 in the Nil arm. -; - `xs` (the param) has consume_count == 0 (only borrow at -; match scrutinee). Iter B fires: param drop at fn return. -; - `t` (Cons-arm pattern binder) has consume_count == 0 (the -; arm body just returns `h` — `t` is unused). Iter A fires: -; drop__IntList(t) at arm close, freeing the tail chain -; before the fn returns. -; - At fn return, moved_slots[xs] = {1} (Cons.t was moved into -; the arm-bound `t` and dec'd by iter A). Iter B falls back -; to shallow `ailang_rc_dec(%arg_xs)` — the dynamic-tag -; partial-drop case is debt; for the canonical Cons-or-Nil -; dispatch here, dec'ing the outer cell only is correct -; because the active ctor's only ptr field (Cons.tail) is -; already freed by iter A, and Nil has no ptr fields. -; -; Expected stdout under --alloc=rc / --alloc=gc: 11 (head of the -; 5-element list). - (module rc_own_param_drop - (data IntList (doc "Recursive Int list — boxed.") (ctor Nil) (ctor Cons (con Int) (con IntList))) - (fn head_or_zero (doc "Take ownership of an IntList; return its head if Cons, else 0. The tail is loaded as a pattern binder but never consumed — iter A dec's it at arm close. The outer cell is dec'd at fn return via iter B's Own-param emission.") - (type - (fn-type - (params (own (con IntList))) - (ret (con Int)))) + (suppress (code "over-strict-mode") (because "RC codegen test: exercises Iter B Own-param dec at fn return")) + (type (fn-type (params (own (con IntList))) (ret (con Int)))) (params xs) - (body - (match xs - (case (pat-ctor Nil) 0) - (case (pat-ctor Cons h t) h)))) - + (body (match xs + (case (pat-ctor Nil) 0) + (case (pat-ctor Cons h t) h)))) (fn main (doc "Build a 5-element IntList; pass to head_or_zero (transferring ownership); print the result.") (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) - (body - (let xs - (term-ctor IntList Cons 11 - (term-ctor IntList Cons 22 - (term-ctor IntList Cons 33 - (term-ctor IntList Cons 44 - (term-ctor IntList Cons 55 - (term-ctor IntList Nil)))))) - (do io/print_int (app head_or_zero xs)))))) + (body (let xs (term-ctor IntList Cons 11 (term-ctor IntList Cons 22 (term-ctor IntList Cons 33 (term-ctor IntList Cons 44 (term-ctor IntList Cons 55 (term-ctor IntList Nil)))))) (do io/print_int (app head_or_zero xs)))))) diff --git a/examples/rc_own_param_drop.prose.txt b/examples/rc_own_param_drop.prose.txt index dc9e800..db37cd5 100644 --- a/examples/rc_own_param_drop.prose.txt +++ b/examples/rc_own_param_drop.prose.txt @@ -3,6 +3,7 @@ /// Recursive Int list — boxed. data IntList = Nil | Cons(Int, IntList) +// @suppress over-strict-mode: RC codegen test: exercises Iter B Own-param dec at fn return /// Take ownership of an IntList; return its head if Cons, else 0. The tail is /// loaded as a pattern binder but never consumed — iter A dec's it at arm /// close. The outer cell is dec'd at fn return via iter B's Own-param emission. diff --git a/examples/rc_own_param_partial_drop_leak.ail.json b/examples/rc_own_param_partial_drop_leak.ail.json index 0f9fc30..5be8841 100644 --- a/examples/rc_own_param_partial_drop_leak.ail.json +++ b/examples/rc_own_param_partial_drop_leak.ail.json @@ -1 +1 @@ -{"defs":[{"ctors":[{"fields":[{"k":"con","name":"Int"}],"name":"MkWrap"}],"kind":"type","name":"Wrap"},{"ctors":[{"fields":[{"k":"con","name":"Wrap"},{"k":"con","name":"Wrap"}],"name":"MkCell"}],"kind":"type","name":"Cell"},{"ctors":[{"fields":[{"k":"con","name":"Cell"},{"k":"con","name":"Cell"}],"name":"MkPair"}],"kind":"type","name":"Pair"},{"body":{"args":[{"args":[{"args":[{"name":"n","t":"var"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"},{"args":[{"args":[{"lit":{"kind":"int","value":3},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":4},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"kind":"fn","name":"build_pair","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Pair"},"ret_mode":"own"}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"ctor":"MkPair","fields":[{"name":"a","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"kind":"fn","name":"use_first","params":["p"],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"Pair"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"build_pair","t":"var"},"t":"app"}],"fn":{"name":"use_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_own_param_partial_drop_leak","schema":"ailang/v0"} \ No newline at end of file +{"defs":[{"ctors":[{"fields":[{"k":"con","name":"Int"}],"name":"MkWrap"}],"kind":"type","name":"Wrap"},{"ctors":[{"fields":[{"k":"con","name":"Wrap"},{"k":"con","name":"Wrap"}],"name":"MkCell"}],"kind":"type","name":"Cell"},{"ctors":[{"fields":[{"k":"con","name":"Cell"},{"k":"con","name":"Cell"}],"name":"MkPair"}],"kind":"type","name":"Pair"},{"body":{"args":[{"args":[{"args":[{"name":"n","t":"var"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":2},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"},{"args":[{"args":[{"lit":{"kind":"int","value":3},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"},{"args":[{"lit":{"kind":"int","value":4},"t":"lit"}],"ctor":"MkWrap","t":"ctor","type":"Wrap"}],"ctor":"MkCell","t":"ctor","type":"Cell"}],"ctor":"MkPair","t":"ctor","type":"Pair"},"kind":"fn","name":"build_pair","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Pair"},"ret_mode":"own"}},{"body":{"arms":[{"body":{"lit":{"kind":"int","value":1},"t":"lit"},"pat":{"ctor":"MkPair","fields":[{"name":"a","p":"var"},{"p":"wild"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"kind":"fn","name":"use_first","params":["p"],"suppress":[{"because":"RC codegen test: exercises Iter B fn-return dynamic-tag partial-drop","code":"over-strict-mode"}],"type":{"effects":[],"k":"fn","param_modes":["own"],"params":[{"k":"con","name":"Pair"}],"ret":{"k":"con","name":"Int"}}},{"body":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"build_pair","t":"var"},"t":"app"}],"fn":{"name":"use_first","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"rc_own_param_partial_drop_leak","schema":"ailang/v0"} diff --git a/examples/rc_own_param_partial_drop_leak.ailx b/examples/rc_own_param_partial_drop_leak.ailx index 5ee6d4c..2d75ffe 100644 --- a/examples/rc_own_param_partial_drop_leak.ailx +++ b/examples/rc_own_param_partial_drop_leak.ailx @@ -1,65 +1,21 @@ -; Iter 18g.tidy.fu2 RED-test fixture 1/3: dynamic-tag partial-drop -; carve-out at fn-return (Iter B / lib.rs:1093). -; -; Shape: -; - `Pair` carries two `Cell` fields (both pointer-typed). -; - `Cell` carries two `Wrap` fields (both pointer-typed). -; - `use_first` takes `(own Pair)` and pattern-binds the first -; slot only, wildcarding the second. -; - The bound slot's `Cell` is dec'd via `drop__Cell` at the -; outer arm-close (moves[a] empty → field_drop_call routes -; correctly). -; - At fn return, `p`'s `consume_count == 0`, mode = Own, and -; `moved_slots[p] = {0}`. Iter B's drop (lib.rs:1093) hits the -; dynamic-tag carve-out: moves non-empty → shallow -; `ailang_rc_dec(p)`. p's outer cell is freed; slot 1 (the -; wildcarded second Cell + its two MkWrap children = 3 cells) -; leaks. -; -; Pre-fix: live = 3 (one Cell + two MkWrap children). -; Post-fix: live = 0. -; -; This fixture is the cleanest of the three because no inner match -; is involved: the leak surfaces from Iter B alone. - (module rc_own_param_partial_drop_leak - (data Wrap (ctor MkWrap (con Int))) - (data Cell (ctor MkCell (con Wrap) (con Wrap))) - (data Pair (ctor MkPair (con Cell) (con Cell))) - (fn build_pair - (type - (fn-type - (params (con Int)) - (ret (own (con Pair))))) + (type (fn-type (params (con Int)) (ret (own (con Pair))))) (params n) - (body - (term-ctor Pair MkPair - (term-ctor Cell MkCell - (term-ctor Wrap MkWrap n) - (term-ctor Wrap MkWrap 2)) - (term-ctor Cell MkCell - (term-ctor Wrap MkWrap 3) - (term-ctor Wrap MkWrap 4))))) - + (body (term-ctor Pair MkPair (term-ctor Cell MkCell (term-ctor Wrap MkWrap n) (term-ctor Wrap MkWrap 2)) (term-ctor Cell MkCell (term-ctor Wrap MkWrap 3) (term-ctor Wrap MkWrap 4))))) (fn use_first - (type - (fn-type - (params (own (con Pair))) - (ret (con Int)))) + (suppress (code "over-strict-mode") (because "RC codegen test: exercises Iter B fn-return dynamic-tag partial-drop")) + (type (fn-type (params (own (con Pair))) (ret (con Int)))) (params p) - (body - (match p - (case (pat-ctor MkPair a _) 1)))) - + (body (match p + (case (pat-ctor MkPair a _) 1)))) (fn main (type (fn-type (params) (ret (con Unit)) (effects IO))) (params) - (body - (do io/print_int (app use_first (app build_pair 1)))))) + (body (do io/print_int (app use_first (app build_pair 1))))))