Iter 18e: (drop-iterative) annotation + worklist allocator
Closes the 18-arc's stack-recursion limit. Recursive drop cascades from 18c.4 overflow on long ADT chains (Linux's 8 MB default stack maxes out around 1M cells of List). The new opt-in (drop-iterative) annotation on a Def::Type switches the synthesised drop_<m>_<T> body from recursive to iterative-with- explicit-worklist for that type. Schema: - TypeDef.drop_iterative: bool. Default false; serde-skip when false so existing fixtures' canonical JSON hashes stay stable. - Form-A: (drop-iterative) clause inside (data T ...). Worklist runtime (4 new ABI symbols in runtime/rc.c): - ailang_drop_worklist_new(initial_capacity) - ailang_drop_worklist_push(wl, ptr) - ailang_drop_worklist_pop(wl) -> ptr - ailang_drop_worklist_free(wl) Heap stretchy buffer, doubling on overflow, null-filtering on push. Lean 4 / Roc precedent documented in the runtime; the slot-repurposing strategy was considered and rejected because not every box has a free pointer-typed slot to thread the worklist through (Cons head is i64, slot 1 is ptr but it's the field we're following — no free slot). Codegen (emit_iterative_drop_fn_for_type): for a drop_iterative type, drop_<m>_<T>(ptr %p) emits a worklist loop. Fields of the SAME annotated type push onto the worklist (mono-typed); fields of DIFFERENT types call their own drop fn directly (recursive on those, but only if THEY are themselves recursive — i.e. one level of cascade jump maximum). Mono-typed-worklist is sound for the deep-self- recursion case the iter targets (List of List of T just needs the spine flattened). Tests: - examples/rc_drop_iterative_long_list — 1M-cell List of Int with (drop-iterative) annotation. - alloc_rc_drop_iterative_handles_million_cell_list E2E — builds + runs under --alloc=rc, asserts clean exit. With annotation: exits 0. Without annotation (control): SIGSEGV at exit code 139 (verified by hand). Worklist is load- bearing. - iter18e_drop_iterative_emits_worklist_body_no_self_recursion IR-shape: worklist body has br to loop_head AND no direct recursive call into drop_<m>_<T>. - iter18e_no_annotation_keeps_recursive_drop_body — control: unannotated variant still emits the 18c.4 recursive shape. - 3 surface parse-tests for the annotation round-trip. Test deltas: e2e 58 -> 61 (+3), surface 18 -> 21 (+3). All other buckets unchanged. cargo test --workspace green. Known debt (deliberate): - Mono-typed worklist: cross-type drop-iterative fields call the other type's drop fn directly. A heterogeneous worklist would be more general but adds tag tracking complexity for a case (drop-iterative T containing drop-iterative T') that's narrower than the deep-self- recursion target. Documented in emit_iterative_drop_fn_for_type's doc. - Closure / Type::Var / Type::Forall fields fall back to shallow ailang_rc_dec via field_drop_call — same as the recursive variant. - Dynamic-tag partial-drop fallback (head_or_zero epilogue shallow dec when moved_slots non-empty) — out of scope per brief.
This commit is contained in:
@@ -129,8 +129,26 @@ pub struct TypeDef {
|
||||
/// Optional source-level documentation string.
|
||||
#[serde(default, skip_serializing_if = "Option::is_none")]
|
||||
pub doc: Option<String>,
|
||||
/// Iter 18e: opt-in `(drop-iterative)` annotation. When `true`,
|
||||
/// codegen emits `drop_<m>_<T>` with an iterative worklist body
|
||||
/// instead of the recursive cascade — chosen by the LLM-author when
|
||||
/// the type is expected to form long chains (millions of cells)
|
||||
/// that would overflow the C stack on free.
|
||||
///
|
||||
/// Serialised as `"drop-iterative": true` (kebab-case) when set;
|
||||
/// the field is omitted when `false` so canonical-JSON hashes of
|
||||
/// every pre-18e fixture remain bit-stable. See the regression
|
||||
/// test `iter18e_drop_iterative_default_preserves_hashes` in
|
||||
/// [`crate::hash`].
|
||||
#[serde(
|
||||
default,
|
||||
rename = "drop-iterative",
|
||||
skip_serializing_if = "is_false"
|
||||
)]
|
||||
pub drop_iterative: bool,
|
||||
}
|
||||
|
||||
|
||||
/// A single constructor of a [`TypeDef`].
|
||||
///
|
||||
/// `fields` is the constructor's positional argument list as types;
|
||||
|
||||
@@ -1959,6 +1959,7 @@ mod tests {
|
||||
],
|
||||
}],
|
||||
doc: None,
|
||||
drop_iterative: false,
|
||||
};
|
||||
let letrec = Term::LetRec {
|
||||
name: "helper".into(),
|
||||
|
||||
Reference in New Issue
Block a user