the full chunks, as runs in order (built last run first, from the last
chunk back: a chunk joins the run after it when that run's first entry is
one stride past its own)
329def coppeliusGatherRuns =
330 (lambda unrestricted entries : Bytes .
331 (let unrestricted stride = (coppeliusGatherStride entries) in
332 (nat-eliminate
333 (lambda unrestricted current : Nat . (family StdList (family CoppeliusGatherRun)))
334 (constructor StdList StdListEmpty (family CoppeliusGatherRun))
335 (lambda unrestricted p : Nat .
336 (lambda unrestricted later : (family StdList (family CoppeliusGatherRun)) .
337 (let unrestricted chunk = (naturalSaturatingSubtract (naturalSaturatingSubtract coppeliusFullChunks 1) p) in
338 (let unrestricted alone = (constructor StdList StdListCons (family CoppeliusGatherRun)
339 (constructor CoppeliusGatherRun CoppeliusGatherRunValue chunk 1) later) in
340 (eliminate StdList (lambda unrestricted current : (family StdList (family CoppeliusGatherRun)) . (family StdList (family CoppeliusGatherRun))) later
341 (branch StdListEmpty . alone)
342 (branch StdListCons run rest induction .
343 (eliminate CoppeliusGatherRun (lambda unrestricted current : (family CoppeliusGatherRun) . (family StdList (family CoppeliusGatherRun))) run
344 (branch CoppeliusGatherRunValue first length .
345 (nat-eliminate (lambda unrestricted current : Nat . (family StdList (family CoppeliusGatherRun)))
346 alone
347 (lambda unrestricted q : Nat . (lambda unrestricted ignored : (family StdList (family CoppeliusGatherRun)) .
348 (constructor StdList StdListCons (family CoppeliusGatherRun)
349 (constructor CoppeliusGatherRun CoppeliusGatherRunValue chunk (succ length)) rest)))
350 (naturalEqual (coppeliusGatherEntry entries first) (naturalAdd (coppeliusGatherEntry entries chunk) stride)))))))))))
351 coppeliusFullChunks)))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.