The first event that breaks the order, counted from 1 (one past the last
when the end does: a submission never awaited, or a write never
consumed), or 0 when none does. The walk carries the first hazard found
and makes one recursive call per event (a choice between two
continuations would be evaluated on both sides by the build's evaluator).
150def arenaScheduleHazard =
151 (lambda unrestricted count : Nat .
152 (lambda unrestricted events : (family ArenaEvents) .
153 (app (app (app (app
154 (eliminate ArenaEvents
155 (lambda unrestricted current : (family ArenaEvents) .
156 (pi unrestricted index : Nat . (pi unrestricted last : Nat . (pi unrestricted pending : (family ArenaRanges) . (pi unrestricted hazard : Nat . Nat)))))
157 events
158 (branch ArenaEventsEnd .
159 (lambda unrestricted index : Nat . (lambda unrestricted last : Nat . (lambda unrestricted pending : (family ArenaRanges) . (lambda unrestricted hazard : Nat .
160 (naturalSelect hazard hazard
161 (naturalSelect (naturalAnd (naturalEqual last count) (arenaRangesEmpty pending)) 0 index)))))))
162 (branch ArenaEventsNext event rest induction .
163 (lambda unrestricted index : Nat . (lambda unrestricted last : Nat . (lambda unrestricted pending : (family ArenaRanges) . (lambda unrestricted hazard : Nat .
164 (let unrestricted found = (lambda unrestricted failed : Nat . (naturalSelect hazard hazard (naturalSelect failed index 0)))
165 in (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . Nat) event
166 (branch ArenaHostWrite offset extent .
167 (let unrestricted meets = (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending))
168 in (induction (succ index) last
169 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
170 pending
171 (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) .
172 (constructor ArenaRanges ArenaRangesNext offset (naturalAdd offset extent) pending)))
173 (naturalAnd (naturalNonzero extent) (naturalIsZero meets)))
174 (found meets))))
175 (branch ArenaHostRead offset extent .
176 (induction (succ index) last pending
177 (found (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending)))))
178 (branch ArenaAwait generation .
179 (let unrestricted fresh = (naturalLess last generation)
180 in (induction (succ index) (naturalSelect fresh generation last)
181 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
182 pending
183 (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) . arenaRangesNone))
184 fresh)
185 (found (naturalIsZero fresh)))))
186 (branch ArenaObserve generation .
187 (induction (succ index) last pending
188 (found (naturalIsZero (naturalAnd (naturalNonzero generation) (naturalLessOrEqual generation last))))))))))))))
189 1) 0) arenaRangesNone) 0)))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.