A backward branch whose displacement is derived from the body it repeats.
The descriptor is the SM86 BRA ABI; the caller owns the predicate and
must ensure its loop variable advances before the branch. The branch is
relative to its successor, so it crosses the body and itself.
47def sm86ProgramLoopWhileNot =
48 (lambda unrestricted predicate : (family SM86Predicate) .
49 (lambda unrestricted body :
50 (pi unrestricted tail : (family SM86Program) . (family SM86Program)) .
51 (lambda erased admitted :
52 (equal Nat
53 (naturalLess
54 (naturalMultiply sm86InstructionBytes
55 (succ (sm86ProgramCount (body sm86ProgramEmpty))))
56 2147483648) 1) .
57 (lambda unrestricted tail : (family SM86Program) .
58 (let unrestricted distance =
59 (succ (sm86ProgramCount (body sm86ProgramEmpty))) in
60 (body
61 (constructor SM86Program SM86ProgramNext
62 (sm86NegatedPredicatedInstruction predicate
63 (constructor SM86InstructionBody SM86Branch
64 (sm86Unsigned32FromNaturalTruncated
65 (naturalSaturatingSubtract 4294967296 (naturalMultiply sm86InstructionBytes distance)))
66 (sm86Unsigned32 (byte 255) (byte 255) (byte 131) (byte 3))
67 sm86BranchControl))
68 tail)))))))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.