88def encodeValidatedSM86ControlLE =
89 (lambda unrestricted control : (family SM86Control) .
90 (eliminate
91 SM86Control
92 (lambda unrestricted value : (family SM86Control) . Bytes)
93 control
94 (branch
95 SM86ControlValue
96 stall
97 yieldMode
98 writeBarrier
99 readBarrier
100 waitMask
101 reuseMask
102 .
103 (app
104 (lambda unrestricted stallNatural : Nat .
105 (lambda unrestricted yieldNatural : Nat .
106 (lambda unrestricted writeNatural : Nat .
107 (lambda unrestricted readNatural : Nat .
108 (lambda unrestricted waitNatural : Nat .
109 (lambda unrestricted reuseNatural : Nat .
110 (app
111 (lambda unrestricted waitHigh : Nat .
112 (lambda unrestricted waitLow : Nat .
113 (bytes
114 (nat-to-byte
115 (sm86NaturalAdd
116 stallNatural
117 (sm86NaturalAdd
118 (sm86NaturalTimesSixteen yieldNatural)
119 (sm86NaturalTimesThirtyTwo writeNatural))))
120 (nat-to-byte
121 (sm86NaturalAdd readNatural (sm86NaturalTimesEight waitLow)))
122 (nat-to-byte
123 (sm86NaturalAdd waitHigh (sm86NaturalDouble reuseNatural)))
124 (byte 0))))
125 (nat-less-than (byte-to-nat (byte 31)) waitNatural)
126 (sm86NaturalSelect
127 (nat-less-than (byte-to-nat (byte 31)) waitNatural)
128 (sm86NaturalSubtract waitNatural (byte-to-nat (byte 32)))
129 waitNatural))))))))
130 (byte-to-nat stall)
131 (sm86YieldBit yieldMode)
132 (sm86BarrierCode writeBarrier)
133 (sm86BarrierCode readBarrier)
134 (byte-to-nat waitMask)
135 (byte-to-nat reuseMask)))))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.