Finalization is separate from feeding so segment boundaries cannot reset
sequence state, footer count, or the first diagnostic. Tail is its original
byte extent, including a deliberately opaque oversized unfinished frame.
784def aosFinishStreamScan =
785 (lambda unrestricted lines : Nat .
786 (lambda unrestricted tailBytes : Nat .
787 (lambda unrestricted walk : (family AosWalk) .
788 (eliminate
789 AosWalk
790 (lambda unrestricted current : (family AosWalk) . (family AosStreamVerdict))
791 walk
792 (branch
793 AosWalkValue
794 problem
795 line
796 code
797 producers
798 footer
799 complete
800 events
801 unknown
802 .
803 (let unrestricted gaps =
804 (aosSumGaps producers 0)
805 in
806 (let unrestricted unaccounted =
807 (aosSumGaps producers 1)
808 in
809 (let unrestricted drops =
810 (aosSumDrops producers)
811 in
812 (let unrestricted verdict =
813 (lambda unrestricted status : Nat .
814 (lambda unrestricted found : Nat .
815 (constructor
816 AosStreamVerdict
817 AosStreamVerdictValue
818 status
819 found
820 line
821 code
822 lines
823 events
824 unknown
825 tailBytes
826 gaps
827 drops)))
828 in
829 (aosChoose
830 (family AosStreamVerdict)
831 problem
832 (verdict 2 problem)
833 (aosChoose
834 (family AosStreamVerdict)
835 (naturalIsZero lines)
836 (verdict 2 1)
837 (aosChoose
838 (family AosStreamVerdict)
839 tailBytes
840 (verdict 1 9)
841 (aosChoose
842 (family AosStreamVerdict)
843 (naturalIsZero footer)
844 (verdict 1 7)
845 (aosChoose
846 (family AosStreamVerdict)
847 (naturalIsZero complete)
848 (verdict 1 8)
849 (aosChoose
850 (family AosStreamVerdict)
851 unaccounted
852 (verdict 1 10)
853 (verdict 0 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.