iter it.2: structural-guardedness checker + first real Diverge effect

Iteration-discipline milestone, 2 of 3. Strictly additive (nothing
tail-related removed; that is it.3). New whole-body pass
verify_structural_recursion sibling of verify_tail_positions
(DD-1): smaller-set algorithm with implicit candidate inference +
unconstrained accumulators (DD-2, foldl=structural), self/mutual
via inline ADT-family union-find (DD-3), it.2-only tail==false
grandfather. CheckError::NonStructuralRecursion. term_contains_loop
(stops at Term::Lam, DD-4) injects Diverge so existing
UndeclaredEffect enforces it, no new variant; lam-arrow + LetRec
sub-effect sites wired. DESIGN.md Decision 3 synced. Four it.1
loop fixtures gained !Diverge.

Two spec-premise boundary defects surfaced + resolved within the
additive invariant (corpus clean, check not weakened), recorded as
corrected it.3 corpus-migration scope: (1) the "21 tail-app
fixtures" grandfather premise under-counts the corpus —
no-ADT-candidate counter recursions have no structural position to
verify, deferred to it.3; (2) two RC-regression fixtures joined the
spec's transitional tail-app grandfather as the other 20 do (RC==GC
guards verified still green). cargo test --workspace 622/0; 9
acceptance pins non-vacuous. Spec fda9b78, plan bc9f512.
This commit is contained in:
2026-05-15 15:29:43 +02:00
parent bc9f512003
commit a4be1e58a3
22 changed files with 1402 additions and 22 deletions
+9 -1
View File
@@ -59,6 +59,14 @@
(case (pat-ctor TLeaf) 0)
(case (pat-ctor TNode v l r) 1)))))
; Iter it.2: integer-counter recursion holding the ADT param `t`
; constant — non-structural by the it.2 guardedness check (D2). The
; recursive call is in tail position, so it joins the transitional
; `tail-app` grandfather (spec it.2 "Transitional grandfather") as
; the rest of the corpus does until it.3 migrates such recursions
; to `(loop …)`. The 18g let-alias-mode regression this fixture
; guards lives in `pin_aliased`'s match arm-close, unaffected by
; this tail marking.
(fn loop
(type
(fn-type
@@ -69,7 +77,7 @@
(if (app == n 0)
0
(let _v (app pin_aliased t)
(app loop (app - n 1) t)))))
(tail-app loop (app - n 1) t)))))
(fn main
(type (fn-type (params) (ret (con Unit)) (effects IO)))