169def arenaScheduleRun =
170 (lambda unrestricted state : (family ArenaScheduleState) .
171 (lambda unrestricted events : (family ArenaEvents) .
172 (app
173 (eliminate ArenaEvents
174 (lambda unrestricted current : (family ArenaEvents) .
175 (pi unrestricted at : (family ArenaScheduleState) . (family ArenaScheduleState)))
176 events
177 (branch ArenaEventsEnd . (lambda unrestricted at : (family ArenaScheduleState) . at))
178 (branch ArenaEventsNext event rest induction .
179 (lambda unrestricted at : (family ArenaScheduleState) .
180 (let unrestricted index = (arenaStateIndexOf at) in
181 (let unrestricted last = (arenaStateLastOf at) in
182 (let unrestricted pending = (arenaStatePendingOf at) in
183 (let unrestricted hazard = (arenaStateHazardOf at) in
184 (let unrestricted found = (lambda unrestricted failed : Nat . (naturalSelect hazard hazard (naturalSelect failed index 0))) in
185 (let unrestricted next = (lambda unrestricted newLast : Nat . (lambda unrestricted newPending : (family ArenaRanges) .
186 (lambda unrestricted newHazard : Nat .
187 (constructor ArenaScheduleState ArenaScheduleStateValue (succ index) newLast newPending newHazard)))) in
188 (induction
189 (eliminate ArenaEvent (lambda unrestricted current : (family ArenaEvent) . (family ArenaScheduleState)) event
190 (branch ArenaHostWrite offset extent .
191 (let unrestricted meets = (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending))
192 in (next last
193 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
194 pending
195 (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) .
196 (constructor ArenaRanges ArenaRangesNext offset (naturalAdd offset extent) pending)))
197 (naturalAnd (naturalNonzero extent) (naturalIsZero meets)))
198 (found meets))))
199 (branch ArenaHostRead offset extent .
200 (next last pending
201 (found (naturalAnd (naturalNonzero extent) (arenaRangesMeet offset (naturalAdd offset extent) pending)))))
202 (branch ArenaAwait generation .
203 (let unrestricted fresh = (naturalLess last generation)
204 in (next (naturalSelect fresh generation last)
205 (nat-eliminate (lambda unrestricted current : Nat . (family ArenaRanges))
206 pending
207 (lambda unrestricted predecessor : Nat . (lambda unrestricted unused : (family ArenaRanges) . arenaRangesNone))
208 fresh)
209 (found (naturalIsZero fresh)))))
210 (branch ArenaObserve generation .
211 (next last pending
212 (found (naturalIsZero (naturalAnd (naturalNonzero generation) (naturalLessOrEqual generation last)))))))))))))))))
213 state)))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.