2452def sm121LowerRelocateWith =
2453 (lambda unrestricted labels : (family SM121LowerLabels) .
2454 (lambda unrestricted placed : (family SM121LowerOps) .
2455 (eliminate
2456 SM121LowerOps
2457 (lambda unrestricted current : (family SM121LowerOps) . (family SM121LowerRelocation))
2458 placed
2459 (branch SM121LowerOpsEnd .
2460 (constructor SM121LowerRelocation SM121LowerRelocated zero (constructor SM121LowerOps SM121LowerOpsEnd)))
2461 (branch SM121LowerOpsNext last earlier induction .
2462 (eliminate
2463 SM121LowerRelocation
2464 (lambda unrestricted current : (family SM121LowerRelocation) . (family SM121LowerRelocation))
2465 induction
2466 (branch SM121LowerRelocated count ops .
2467 (eliminate
2468 SM121LowerOp
2469 (lambda unrestricted current : (family SM121LowerOp) . (family SM121LowerRelocation))
2470 last
2471 (branch SM121LowerOpValue low high class reads writes predicateReads predicateWrites constantLoad label join target .
2472 (let unrestricted found = (sm121LowerFind labels target) in
2473 (let unrestricted place = (nat-subtract found 1) in
2474 (let unrestricted ahead = (nat-less-than count place) in
2475 (sm121LowerSelect (family SM121LowerRelocation)
2476 (naturalIsZero target)
2477 (constructor SM121LowerRelocation SM121LowerRelocated (succ count) (sm121LowerPush last ops))
2478 (sm121LowerSelect (family SM121LowerRelocation)
2479 (naturalIsZero found)
2480 (constructor SM121LowerRelocation SM121LowerRelocationRefused)
2481 (eliminate
2482 SM121LowerWords
2483 (lambda unrestricted current : (family SM121LowerWords) . (family SM121LowerRelocation))
2484 (sm121LowerWithDisplacement
2485 (naturalSelect ahead (nat-multiply sm121LowerBranchUnit (nat-subtract place (succ count))) zero)
2486 (naturalSelect ahead zero (nat-multiply sm121LowerBranchUnit (nat-subtract (succ count) place)))
2487 low high)
2488 (branch SM121LowerWordsValue newLow newHigh .
2489 (constructor SM121LowerRelocation SM121LowerRelocated (succ count)
2490 (sm121LowerPush
2491 (constructor SM121LowerOp SM121LowerOpValue newLow newHigh class reads writes
2492 predicateReads predicateWrites constantLoad label join target)
2493 ops))))))))))))
2494 (branch SM121LowerRelocationRefused . induction))))))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.