---------------------------------------------------------------------------
Relocation: branches re-encoded against where their targets were placed
the placed program's length and where each op a branch lands on was
placed (`placed` holds the last op first, so an op's position is the count
of the ops before it). Only those ops are recorded: the table stays as
small as the program's loops, and relocation stays linear in its length.
2414def sm121LowerLabelsOf =
2415 (lambda unrestricted placed : (family SM121LowerOps) .
2416 (eliminate
2417 SM121LowerOps
2418 (lambda unrestricted current : (family SM121LowerOps) . (family SM121LowerCounted))
2419 placed
2420 (branch SM121LowerOpsEnd .
2421 (constructor SM121LowerCounted SM121LowerCountedValue zero (constructor SM121LowerLabels SM121LowerLabelsEnd)))
2422 (branch SM121LowerOpsNext last earlier induction .
2423 (eliminate
2424 SM121LowerCounted
2425 (lambda unrestricted current : (family SM121LowerCounted) . (family SM121LowerCounted))
2426 induction
2427 (branch SM121LowerCountedValue count labels .
2428 (eliminate
2429 SM121LowerOp
2430 (lambda unrestricted current : (family SM121LowerOp) . (family SM121LowerCounted))
2431 last
2432 (branch SM121LowerOpValue low high class reads writes predicateReads predicateWrites constantLoad label join target .
2433 (constructor SM121LowerCounted SM121LowerCountedValue
2434 (succ count)
2435 (sm121LowerSelect (family SM121LowerLabels)
2436 (naturalAnd join (naturalIsZero target))
2437 (constructor SM121LowerLabels SM121LowerLabelsNext label count labels)
2438 labels)))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.