retire every barrier the wait mask names by swapping in the shared empty;
barrier 8 is never named, so the never mask passes through
217def sbMasksRetire =
218 (lambda unrestricted mask : Nat .
219 (lambda unrestricted pending : (family ScoreboardMasks) .
220 (nat-eliminate
221 (lambda unrestricted current : Nat . (family ScoreboardMasks))
222 pending
223 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : (family ScoreboardMasks) .
224 (eliminate ScoreboardMasks
225 (lambda unrestricted current : (family ScoreboardMasks) . (family ScoreboardMasks))
226 pending
227 (branch ScoreboardMasksValue b1 b2 b3 b4 b5 b6 bn .
228 (constructor ScoreboardMasks ScoreboardMasksValue
229 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b1 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 1))
230 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b2 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 2))
231 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b3 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 3))
232 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b4 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 4))
233 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b5 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 5))
234 (nat-eliminate (lambda unrestricted current : Nat . Bytes) b6 (lambda unrestricted predecessor : Nat . (lambda unrestricted ignored : Bytes . sbBytesEmpty)) (scoreboardMaskNames mask 6))
235 bn)))))
236 (naturalNonzero mask))))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.