Brummel
a4be1e58a3
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. Specfda9b78, planbc9f512.
44 lines
1.3 KiB
Plaintext
44 lines
1.3 KiB
Plaintext
; Iter it.2 positive (spec D1, DD-3): mutual structural recursion
|
|
; over one ADT family. `Tree` references `Forest` (the `Node` field)
|
|
; and `Forest` references `Tree` and `Forest` (the `Cons` fields), so
|
|
; the union-find of the ADT type-reference graph puts {Tree, Forest}
|
|
; in a single connected component. `tree_size` recurses into
|
|
; `forest_size` on the `Node`-bound `f` (structurally smaller); each
|
|
; `forest_size` self/cross call passes a `Cons`-bound sub-component.
|
|
; The whole mutual group is structural: pure, total, Diverge-free,
|
|
; no `tail-app` markers.
|
|
|
|
(module struct_rec_tree_forest
|
|
|
|
(data Tree
|
|
(ctor Node (con Int) (con Forest)))
|
|
|
|
(data Forest
|
|
(ctor FNil)
|
|
(ctor FCons (con Tree) (con Forest)))
|
|
|
|
(fn tree_size
|
|
(doc "Node count of a tree; recurses into forest_size on the Node forest.")
|
|
(type
|
|
(fn-type
|
|
(params (con Tree))
|
|
(ret (con Int))))
|
|
(params tr)
|
|
(body
|
|
(match tr
|
|
(case (pat-ctor Node v f)
|
|
(app + 1 (app forest_size f))))))
|
|
|
|
(fn forest_size
|
|
(doc "Node count of a forest; mutual with tree_size, self on the tail.")
|
|
(type
|
|
(fn-type
|
|
(params (con Forest))
|
|
(ret (con Int))))
|
|
(params fo)
|
|
(body
|
|
(match fo
|
|
(case (pat-ctor FNil) 0)
|
|
(case (pat-ctor FCons t rest)
|
|
(app + (app tree_size t) (app forest_size rest)))))))
|