fix: freeVars, toSKIDB
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
This commit is contained in:
@@ -1,94 +1,52 @@
|
||||
# Recursive Consumer Argument Order
|
||||
|
||||
## Core issue
|
||||
## Rule
|
||||
|
||||
Partial application is generally fine in tricu. The problem appears with recursive consumer functions when loop-control arguments are known before the consumed data is available.
|
||||
Put consumed data first in recursive workers.
|
||||
|
||||
The concrete case was `readBytes`.
|
||||
*AVOID* this shape:
|
||||
|
||||
This worked:
|
||||
|
||||
```tricu
|
||||
(readBytes 2) [(1) (2) (3)]
|
||||
```text
|
||||
worker control state input
|
||||
```
|
||||
|
||||
This used to explode in space:
|
||||
*USE* this shape:
|
||||
|
||||
```tricu
|
||||
readBytes 2
|
||||
```text
|
||||
worker input control state
|
||||
```
|
||||
|
||||
At first this looked like a general partial-application problem, but it was not. Other partial applications, such as partially applying `map`, normalized safely. The issue was the argument order and recursive shape of `readBytes_`.
|
||||
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.
|
||||
|
||||
## What went wrong
|
||||
## Bad shape
|
||||
|
||||
The original worker had loop-control arguments before the byte stream:
|
||||
The original `readBytes_` worker put loop-control arguments before the byte stream:
|
||||
|
||||
```tricu
|
||||
readBytes_ = y (self n i bs original acc : ...)
|
||||
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)
|
||||
```
|
||||
|
||||
After partially applying:
|
||||
With a partial application like:
|
||||
|
||||
```tricu
|
||||
readBytes 2
|
||||
```
|
||||
|
||||
the evaluator knew:
|
||||
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.
|
||||
|
||||
```text
|
||||
n = 2
|
||||
i = 0
|
||||
```
|
||||
## Good shape
|
||||
|
||||
but did not know:
|
||||
|
||||
```text
|
||||
bs
|
||||
original
|
||||
acc
|
||||
```
|
||||
|
||||
Because the counter values were known, the evaluator could reduce checks like:
|
||||
|
||||
```tricu
|
||||
equal? i n
|
||||
```
|
||||
|
||||
and begin unrolling recursion symbolically before the byte stream existed. That produced a large residual tree describing possible stream cases, rests, and accumulated values.
|
||||
|
||||
The bug was not recursion itself. The bug was allowing counters to drive recursion while the consumed structure was still abstract.
|
||||
|
||||
## Why `map`-style partial application is safe
|
||||
|
||||
A partially-applied list consumer such as:
|
||||
|
||||
```tricu
|
||||
map (i : append i " world!")
|
||||
```
|
||||
|
||||
is safe because recursion is blocked on the missing list argument. The function cannot recurse until it sees whether the list is empty or a cons cell.
|
||||
|
||||
Safe shape:
|
||||
|
||||
```text
|
||||
waiting for input
|
||||
recursion blocked until input is supplied
|
||||
```
|
||||
|
||||
Unsafe shape:
|
||||
|
||||
```text
|
||||
waiting for input
|
||||
known counters still allow symbolic recursion
|
||||
```
|
||||
|
||||
## Fix
|
||||
|
||||
Put the consumed data first in the recursive worker and make the first major operation inspect that data.
|
||||
|
||||
Corrected shape:
|
||||
The corrected worker takes the byte stream first and immediately case-analyzes it:
|
||||
|
||||
```tricu
|
||||
readBytes_ = y (self bs n i original acc :
|
||||
@@ -113,155 +71,11 @@ Now:
|
||||
readBytes 2
|
||||
```
|
||||
|
||||
becomes:
|
||||
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.
|
||||
|
||||
```tricu
|
||||
bs : readBytes_ bs 2 0 bs t
|
||||
```
|
||||
|
||||
Since `bs` is abstract and the worker immediately performs:
|
||||
|
||||
```tricu
|
||||
matchList ... bs
|
||||
```
|
||||
|
||||
evaluation blocks at the data boundary instead of unrolling the counter loop.
|
||||
|
||||
## General rule
|
||||
|
||||
For recursive consumers, the consumed structure should drive evaluation.
|
||||
|
||||
Prefer:
|
||||
|
||||
```tricu
|
||||
worker = y (self input control state :
|
||||
matchInput
|
||||
baseCase
|
||||
(piece rest : ... self rest control nextState ...)
|
||||
input)
|
||||
```
|
||||
|
||||
Avoid:
|
||||
|
||||
```tricu
|
||||
worker = y (self control state input :
|
||||
if controlDone
|
||||
done
|
||||
(... self nextControl nextState rest ...))
|
||||
```
|
||||
|
||||
In practice:
|
||||
## Takeaway
|
||||
|
||||
```text
|
||||
worker input control state
|
||||
```
|
||||
|
||||
is safer than:
|
||||
|
||||
```text
|
||||
worker control state input
|
||||
```
|
||||
|
||||
## Accumulators
|
||||
|
||||
Be careful not to finalize or transform an abstract accumulator too early.
|
||||
|
||||
For example:
|
||||
|
||||
```tricu
|
||||
ok (reverse acc) bs
|
||||
```
|
||||
|
||||
is fine when reached after concrete input has driven the recursion, but it can become pathological if reached while `acc` is still abstract.
|
||||
|
||||
Guidelines:
|
||||
|
||||
- Accumulate cheaply during recursion.
|
||||
- Finalize, reverse, or validate only after input has forced the function to a concrete success point.
|
||||
- Do not let counters select a success branch while the accumulator is still abstract.
|
||||
|
||||
## Parser guidance
|
||||
|
||||
For byte or parser consumers, prefer streaming over global slicing of unknown input.
|
||||
|
||||
Prefer:
|
||||
|
||||
```tricu
|
||||
read one byte
|
||||
compare or accumulate
|
||||
recurse on rest
|
||||
```
|
||||
|
||||
Avoid relying on:
|
||||
|
||||
```tricu
|
||||
taken = bytesTake n bs
|
||||
rest = bytesDrop n bs
|
||||
enough = bytesLength taken == n
|
||||
```
|
||||
|
||||
The slice-based version may be correct on concrete input but can behave badly when partially applied over abstract input.
|
||||
|
||||
Streaming alone is not enough; the recursive worker must also be data-first.
|
||||
|
||||
## Checklist
|
||||
|
||||
When writing a recursive consumer, ask:
|
||||
|
||||
1. What structure is consumed?
|
||||
2. What argument should block recursion when unknown?
|
||||
3. Are counters available before the consumed structure?
|
||||
4. Could partial application specialize the loop before data arrives?
|
||||
5. Does any branch process an abstract accumulator or rest value?
|
||||
6. Does the worker put consumed data before counters and state?
|
||||
|
||||
## Safe and unsafe examples
|
||||
|
||||
Safe:
|
||||
|
||||
```tricu
|
||||
readU8
|
||||
bs : readU8 bs
|
||||
readBytes 2 [(1) (2) (3)]
|
||||
(readBytes 2) [(1) (2) (3)]
|
||||
map (i : append i " world!")
|
||||
```
|
||||
|
||||
Previously unsafe before the data-first rewrite:
|
||||
|
||||
```tricu
|
||||
readBytes 2
|
||||
readBytes_ 2 0
|
||||
```
|
||||
|
||||
## Implication for Arborix
|
||||
|
||||
Arborix parsers will include many recursive consumers:
|
||||
|
||||
- read N bytes
|
||||
- read N section records
|
||||
- scan records for an ID
|
||||
- parse node records
|
||||
- validate closures
|
||||
|
||||
These should use data-first recursive workers.
|
||||
|
||||
Avoid:
|
||||
|
||||
```tricu
|
||||
readSectionRecords_ count index bs acc
|
||||
```
|
||||
|
||||
Prefer:
|
||||
|
||||
```tricu
|
||||
readSectionRecords_ bs count index acc
|
||||
```
|
||||
|
||||
## Short rule
|
||||
|
||||
```text
|
||||
Put consumed data first in recursive workers.
|
||||
Let data shape drive recursion.
|
||||
Let consumed data drive recursion.
|
||||
Do not let counters unroll over abstract input.
|
||||
```
|
||||
|
||||
13
src/Eval.hs
13
src/Eval.hs
@@ -223,6 +223,9 @@ freeVars (SVar v Nothing) = Set.singleton v
|
||||
freeVars (SVar v (Just _)) = Set.singleton v
|
||||
freeVars (SApp t u) = Set.union (freeVars t) (freeVars u)
|
||||
freeVars (SLambda vs body) = Set.difference (freeVars body) (Set.fromList vs)
|
||||
freeVars (TStem t) = freeVars t
|
||||
freeVars (TFork t u) = Set.union (freeVars t) (freeVars u)
|
||||
freeVars (SList xs) = foldMap freeVars xs
|
||||
freeVars _ = Set.empty
|
||||
|
||||
reorderDefs :: Env -> [TricuAST] -> [TricuAST]
|
||||
@@ -394,12 +397,10 @@ toSKIDB t
|
||||
| not (dependsOnLevel 0 t) = SApp _K (fromDBClosed t)
|
||||
toSKIDB (BVar 0) = _I
|
||||
toSKIDB (BApp n u) = SApp (SApp _S (toSKIDB n)) (toSKIDB u)
|
||||
toSKIDB (BList xs) =
|
||||
let anyUses = any (dependsOnLevel 0) xs
|
||||
in if not anyUses
|
||||
then SApp _K (SList (map fromDBClosed xs))
|
||||
else SList (map toSKIDB xs)
|
||||
toSKIDB _other = _K `SApp` TLeaf
|
||||
toSKIDB (BStem t) = toSKIDB (BApp BLeaf t)
|
||||
toSKIDB (BFork l r) = toSKIDB (BApp (BApp BLeaf l) r)
|
||||
toSKIDB (BList xs) = toSKIDB (foldr (\m r -> BApp (BApp BLeaf m) r) BLeaf xs)
|
||||
toSKIDB other = error $ "toSKIDB: unsupported DB term: " ++ show other
|
||||
|
||||
app2 :: TricuAST -> TricuAST -> TricuAST
|
||||
app2 f x = SApp f x
|
||||
|
||||
Reference in New Issue
Block a user