James Eversole
1d84bf7cfa
freeVars did not descend into TStem, TFork, or SList, so dependency analysis under structural nodes and lists was silently missed. toSKIDB's _other = _K `SApp` TLeaf fallback returned a constant leaf when the binder occurred under a structural node, losing the abstraction entirely. Replace with explicit lowering: BStem/BFork/BList are converted to application form before SKI abstraction, and any other unsupported DB term errors explicitly
82 lines
1.8 KiB
Markdown
82 lines
1.8 KiB
Markdown
# Recursive Consumer Argument Order
|
|
|
|
## Rule
|
|
|
|
Put consumed data first in recursive workers.
|
|
|
|
*AVOID* this shape:
|
|
|
|
```text
|
|
worker control state input
|
|
```
|
|
|
|
*USE* this shape:
|
|
|
|
```text
|
|
worker input control state
|
|
```
|
|
|
|
The consumed structure should block recursion when it is unknown. Counters, indexes, lengths, and accumulator state should not be able to drive recursion over abstract input.
|
|
|
|
## Bad shape
|
|
|
|
The original `readBytes_` worker put loop-control arguments before the byte stream:
|
|
|
|
```tricu
|
|
readBytes_ = y (self n i bs original acc :
|
|
matchBool
|
|
(ok (reverse acc) bs)
|
|
(matchResult
|
|
(code rest : err code original)
|
|
(actual rest :
|
|
self n (succ i) rest original (pair actual acc))
|
|
(readU8 bs))
|
|
(equal? i n))
|
|
|
|
readBytes = (n bs : readBytes_ n 0 bs bs t)
|
|
```
|
|
|
|
With a partial application like:
|
|
|
|
```tricu
|
|
readBytes 2
|
|
```
|
|
|
|
the evaluator knows `n = 2` and `i = 0`, but `bs` is still abstract. That lets the counter check drive recursive specialization before the byte stream is available, which can build a huge symbolic residual tree. This has been proven; do not reason about it further.
|
|
|
|
## Good shape
|
|
|
|
The corrected worker takes the byte stream first and immediately case-analyzes it:
|
|
|
|
```tricu
|
|
readBytes_ = y (self bs n i original acc :
|
|
matchList
|
|
(matchBool
|
|
(ok (reverse acc) bs)
|
|
(err errUnexpectedEof original)
|
|
(equal? i n))
|
|
(h r :
|
|
matchBool
|
|
(ok (reverse acc) bs)
|
|
(self r n (succ i) original (pair h acc))
|
|
(equal? i n))
|
|
bs)
|
|
|
|
readBytes = (n bs : readBytes_ bs n 0 bs t)
|
|
```
|
|
|
|
Now:
|
|
|
|
```tricu
|
|
readBytes 2
|
|
```
|
|
|
|
becomes a function waiting on `bs`. Since the worker immediately performs `matchList ... bs`, evaluation blocks on the missing input instead of unrolling the counter loop.
|
|
|
|
## Takeaway
|
|
|
|
```text
|
|
Let consumed data drive recursion.
|
|
Do not let counters unroll over abstract input.
|
|
```
|