!import "base.tri" !Local
!import "list.tri" !Local

nothing = t
just = x : t x

bytesIsNil = emptyList?

bytesHead = matchList nothing (h _ : just h)

bytesTail = matchList nothing (_ r : just r)

byteEq = equal?
bytesLength = length
bytesAppend = append

bytesTake_ = y (self n i remaining :
  matchBool
    t
    (matchList
      t
      (h r : pair h (self n (succ i) r))
      remaining)
    (equal? i n))

bytesTake = n bytes : bytesTake_ n 0 bytes

bytesDrop_ = y (self n i remaining :
  matchBool
    remaining
    (matchList
      t
      (_ r : self n (succ i) r)
      remaining)
    (equal? i n))

bytesDrop = n bytes : bytesDrop_ n 0 bytes

bytesSplitAt = n bytes : pair (bytesTake n bytes) (bytesDrop n bytes)

bytesEq = y (self xs ys :
  matchList
    (matchList true (_ _ : false) ys)
    (xh xt :
      matchList
        false
        (yh yt : and? (byteEq xh yh) (self xt yt))
        ys)
    xs)