`low` and `high` of a branch with its displacement set to `words` words of
4 bytes from the next instruction, given as `forward` words ahead or
`backward` words back (one of them zero), in sm_121's placement.
1455def sm121LowerWithDisplacement =
1456 (lambda unrestricted forward : Nat .
1457 (lambda unrestricted backward : Nat .
1458 (lambda unrestricted low : Nat .
1459 (lambda unrestricted high : Nat .
1460 (let unrestricted encoded =
1461 (nat-modulo (nat-subtract (nat-add forward sm121LowerBranchWordSpan) backward) sm121LowerBranchWordSpan) in
1462 (let unrestricted cleared =
1463 (sm121LowerWithField
1464 (sm121LowerWithField low sm121LowerBranchLowPlace sm121LowerRegisterSpan
1465 (nat-modulo encoded sm121LowerRegisterSpan))
1466 sm121LowerBranchOffsetPlace sm121LowerHalfWordSpan zero) in
1467 (constructor SM121LowerWords SM121LowerWordsValue
1468 (sm121LowerWithField cleared sm121LowerBranchMiddlePlace sm121LowerBranchMiddleSpan
1469 (nat-divide encoded sm121LowerRegisterSpan))
1470 (sm121LowerWithField high 1 sm121LowerBranchHighSpan
1471 (nat-divide encoded (nat-multiply sm121LowerRegisterSpan sm121LowerBranchMiddleSpan))))))))))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.