Repeats must pair and never nest: 0 means balanced, 1 means a repeat is
still open, 2 means an end without a begin or a begin inside a repeat.
704def nativePhysicalRepeatBalance =
705 (lambda unrestricted commands : (family NativePhysicalCommands) .
706 (app
707 (eliminate
708 NativePhysicalCommands
709 (lambda unrestricted current : (family NativePhysicalCommands) .
710 (pi unrestricted open : Nat . Nat))
711 commands
712 (branch NativePhysicalCommandsEnd . (lambda unrestricted open : Nat . open))
713 (branch
714 NativePhysicalCommandsNext
715 head
716 tail
717 induction
718 .
719 (lambda unrestricted open : Nat .
720 (eliminate
721 NativePhysicalCommand
722 (lambda unrestricted current : (family NativePhysicalCommand) . Nat)
723 head
724 (branch
725 NativePhysicalCommandValue
726 operation
727 errorIdentity
728 .
729 (eliminate
730 NativePhysicalOperation
731 (lambda unrestricted current : (family NativePhysicalOperation) . Nat)
732 operation
733 (branch
734 NativePhysicalSystemCall
735 number
736 arguments
737 payload
738 result
739 .
740 (induction open))
741 (branch
742 NativePhysicalCopyPayloadToState
743 destination
744 extent
745 payload
746 .
747 (induction open))
748 (branch NativePhysicalMachineRoutine code arguments result . (induction open))
749 (branch NativePhysicalFencePoll address expected polls . (induction open))
750 (branch NativePhysicalTelemetryAppend path record . (induction open))
751 (branch NativePhysicalAssertEqual left right error . (induction open))
752 (branch NativePhysicalAssertOneOf observed first second error . (induction open))
753 (branch NativePhysicalHaltSuccess . (induction open))
754 (branch
755 NativePhysicalRepeatBegin
756 count
757 .
758 (nat-eliminate
759 (lambda unrestricted current : Nat . Nat)
760 (induction (succ zero))
761 (lambda unrestricted predecessor : Nat .
762 (lambda unrestricted ignored : Nat . 2))
763 open))
764 (branch NativePhysicalSkipUnlessEqual left right count . (induction open))
765 (branch
766 NativePhysicalRepeatEnd
767 .
768 (nat-eliminate
769 (lambda unrestricted current : Nat . Nat)
770 2
771 (lambda unrestricted predecessor : Nat .
772 (lambda unrestricted ignored : Nat .
773 (nat-eliminate
774 (lambda unrestricted current : Nat . Nat)
775 (induction zero)
776 (lambda unrestricted deeper : Nat .
777 (lambda unrestricted ignoredDeeper : Nat . 2))
778 predecessor)))
779 open))
780 (branch
781 NativePhysicalRepeatEndWhen
782 observed
783 expected
784 .
785 (nat-eliminate
786 (lambda unrestricted current : Nat . Nat)
787 2
788 (lambda unrestricted predecessor : Nat .
789 (lambda unrestricted ignored : Nat .
790 (nat-eliminate
791 (lambda unrestricted current : Nat . Nat)
792 (induction zero)
793 (lambda unrestricted deeper : Nat .
794 (lambda unrestricted ignoredDeeper : Nat . 2))
795 predecessor)))
796 open))
797 (branch NativePhysicalStoreWord64 destination value . (induction open))
798 (branch
799 NativePhysicalFenceWait
800 address
801 expected
802 polls
803 interval
804 .
805 (induction open))
806 (branch
807 NativePhysicalRepeatBeginCounted
808 count
809 .
810 (nat-eliminate
811 (lambda unrestricted current : Nat . Nat)
812 (induction (succ zero))
813 (lambda unrestricted predecessor : Nat .
814 (lambda unrestricted ignored : Nat . 2))
815 open))
816 (branch NativePhysicalAddWord64 destination left right . (induction open))
817 (branch NativePhysicalFloat64 operation destination left right . (induction open))))))))
818 zero))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.