an event: its sequence must exceed every earlier one of its producer epoch
286def aosWalkEvent =
287 (lambda unrestricted walk : (family AosWalk) .
288 (lambda unrestricted n : Nat .
289 (lambda unrestricted record : (family JSON) .
290 (let unrestricted identity =
291 (aosMemberValue b"event_id" record)
292 in
293 (let unrestricted key =
294 (aosProducerKeyOf identity)
295 in
296 (let unrestricted sequence =
297 (aosDecimalOf b"sequence" identity)
298 in
299 (eliminate
300 AosWalk
301 (lambda unrestricted current : (family AosWalk) . (family AosWalk))
302 walk
303 (branch
304 AosWalkValue
305 problem
306 line
307 code
308 producers
309 footer
310 complete
311 events
312 unknown
313 .
314 (let unrestricted outOfOrder =
315 (eliminate
316 AosFound
317 (lambda unrestricted current : (family AosFound) . Nat)
318 (aosFind key producers)
319 (branch AosFoundNone . 0)
320 (branch
321 AosFoundSome
322 producer
323 .
324 (eliminate
325 AosProducer
326 (lambda unrestricted current : (family AosProducer) . Nat)
327 producer
328 (branch
329 AosProducerValue
330 k
331 next
332 seen
333 drops
334 covered
335 excluded
336 mode
337 .
338 (naturalOr (naturalLess sequence next) (naturalLess sequence covered))))))
339 in
340 (aosChoose
341 (family AosWalk)
342 outOfOrder
343 (aosWalkFail walk 6 n 0)
344 (constructor
345 AosWalk
346 AosWalkValue
347 problem
348 line
349 code
350 (aosUpsert
351 key
352 (lambda unrestricted found : (family AosFound) .
353 (eliminate
354 AosFound
355 (lambda unrestricted current : (family AosFound) .
356 (family AosProducer))
357 found
358 (branch
359 AosFoundNone
360 .
361 (constructor
362 AosProducer
363 AosProducerValue
364 key
365 (succ sequence)
366 1
367 0
368 0
369 0
370 0))
371 (branch
372 AosFoundSome
373 producer
374 .
375 (eliminate
376 AosProducer
377 (lambda unrestricted current : (family AosProducer) .
378 (family AosProducer))
379 producer
380 (branch
381 AosProducerValue
382 k
383 next
384 seen
385 drops
386 covered
387 excluded
388 mode
389 .
390 (constructor
391 AosProducer
392 AosProducerValue
393 key
394 (succ sequence)
395 (succ seen)
396 drops
397 covered
398 excluded
399 mode))))))
400 producers)
401 footer
402 complete
403 (succ events)
404 unknown)))))))))))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.