a delta accumulated on the word at `offset` (a word the block does not
patch is zero)
594def deviceArenaAccumulate =
595 (lambda unrestricted ordinal : Nat .
596 (lambda unrestricted offset : Nat .
597 (lambda unrestricted delta : Nat .
598 (lambda unrestricted spans : (family DeviceArenaSpans) .
599 (eliminate
600 DeviceArenaSpans
601 (lambda unrestricted current : (family DeviceArenaSpans) . (family DeviceArenaSpans))
602 spans
603 (branch
604 DeviceArenaSpansEnd
605 .
606 (constructor
607 DeviceArenaSpans
608 DeviceArenaSpansNext
609 offset
610 (constructor
611 DeviceArenaIntervals
612 DeviceArenaIntervalsNext
613 0
614 0
615 (constructor DeviceArenaIntervals DeviceArenaIntervalsEnd))
616 (deviceArenaRise delta)
617 (deviceArenaFall delta)
618 (naturalLess ordinal deviceArenaWordMaximum)
619 delta
620 (constructor
621 DeviceArenaOrdinals
622 DeviceArenaOrdinalsNext
623 ordinal
624 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsEnd))
625 spans))
626 (branch
627 DeviceArenaSpansNext
628 at
629 intervals
630 rise
631 fall
632 uniform
633 last
634 ordinals
635 tail
636 induction
637 .
638 (nat-eliminate
639 (lambda unrestricted same : Nat . (family DeviceArenaSpans))
640 (constructor
641 DeviceArenaSpans
642 DeviceArenaSpansNext
643 at
644 intervals
645 rise
646 fall
647 uniform
648 last
649 ordinals
650 induction)
651 (lambda unrestricted q : Nat .
652 (lambda unrestricted ignored : (family DeviceArenaSpans) .
653 (let unrestricted first =
654 (deviceArenaOrdinalsEmpty ordinals)
655 in
656 (constructor
657 DeviceArenaSpans
658 DeviceArenaSpansNext
659 at
660 intervals
661 (deviceArenaSaturatingAdd rise (deviceArenaRise delta))
662 (deviceArenaSaturatingAdd fall (deviceArenaFall delta))
663 (naturalAnd
664 uniform
665 (naturalAnd
666 (naturalLess ordinal deviceArenaWordMaximum)
667 (naturalOr
668 first
669 (naturalAnd
670 (naturalEqual delta last)
671 (naturalIsZero (deviceArenaOrdinalsHas ordinals ordinal))))))
672 delta
673 (constructor DeviceArenaOrdinals DeviceArenaOrdinalsNext ordinal ordinals)
674 tail))))
675 (naturalEqual at offset))))))))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.