module Runtime.MemoryCopyRoutine

import Data.Bytes

-- Forward byte copy between caller-owned live ranges. Length zero performs no
-- memory access; overlapping ranges are not a memmove contract. The target's
-- step loads and stores one byte, advances both pointers and decrements the
-- 64-bit count. The shared loop tests the full count and returns status zero.
-- No allocation, IO or implicit extent admission occurs in this primitive.
def nativeMemoryRoutineLabelEntry : Bytes =
  b"mem-entry"

def nativeMemoryRoutineLabelLoop : Bytes =
  b"mem-loop"

def nativeMemoryRoutineLabelDone : Bytes =
  b"mem-done"

def memoryCopyAssemblyFor =
  (lambda erased A : Type 0 .
    (lambda unrestricted step : (pi unrestricted tail : A . A) .
      (lambda unrestricted testCount : (pi unrestricted tail : A . A) .
        (lambda unrestricted jumpZero : (pi unrestricted label : Bytes . (pi unrestricted tail : A . A)) .
          (lambda unrestricted jumpNotZero : (pi unrestricted label : Bytes . (pi unrestricted tail : A . A)) .
            (lambda unrestricted label : (pi unrestricted name : Bytes . (pi unrestricted tail : A . A)) .
              (lambda unrestricted returnZero : (pi unrestricted tail : A . A) .
                (lambda unrestricted end : A .
                  (label
                    nativeMemoryRoutineLabelEntry
                    (testCount
                      (jumpZero
                        nativeMemoryRoutineLabelDone
                        (label
                          nativeMemoryRoutineLabelLoop
                          (step
                            (testCount
                              (jumpNotZero
                                nativeMemoryRoutineLabelLoop
                                (label nativeMemoryRoutineLabelDone (returnZero end)))))))))))))))))