One step of an in-place list reversal driven by a first-order state VALUE:
move the head of `remaining` onto `accumulated`. Empty `remaining` is a fixed
point, so surplus fuel is harmless. The `eliminate` ignores its induction, so
the reference machine does not fold the tail: each step is O(1).
663def utf8CodepointsReverseStep =
664 (lambda unrestricted state : (family UTF8CodepointsReverseState) .
665 (eliminate
666 UTF8CodepointsReverseState
667 (lambda unrestricted current : (family UTF8CodepointsReverseState) .
668 (family UTF8CodepointsReverseState))
669 state
670 (branch
671 UTF8CodepointsReverseStateValue
672 remaining
673 accumulated
674 .
675 (eliminate
676 UTF8Codepoints
677 (lambda unrestricted current : (family UTF8Codepoints) .
678 (family UTF8CodepointsReverseState))
679 remaining
680 (branch
681 UTF8CodepointsEnd
682 .
683 (constructor
684 UTF8CodepointsReverseState
685 UTF8CodepointsReverseStateValue
686 (constructor UTF8Codepoints UTF8CodepointsEnd)
687 accumulated))
688 (branch
689 UTF8CodepointsNext
690 head
691 tail
692 nodeInduction
693 .
694 (constructor
695 UTF8CodepointsReverseState
696 UTF8CodepointsReverseStateValue
697 tail
698 (constructor UTF8Codepoints UTF8CodepointsNext head accumulated)))))))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.