module Data.Bytes

import Data.ByteArray as BA

%access public export
%default total

-- Structure of the allocated ByteArray
--   [used_size][.....data.....]
-- used_size is an int and it takes up BA.bytesPerInt bytes
-- at the beginning of the array

export
record Bytes where
  constructor B
  arr : ByteArray
  ofs : Int
  end : Int  -- first offset not included in the array

minimalCapacity : Int
minimalCapacity = 16

private
dataOfs : Int
dataOfs = 1 * BA.bytesPerInt

private
allocate : Int -> IO Bytes
allocate capacity = do
  arr <- BA.allocate (BA.bytesPerInt + capacity)
  BA.pokeInt 0 dataOfs arr
  BA.fill dataOfs capacity 0 arr  -- zero the array
  return $ B arr dataOfs dataOfs

export
length : Bytes -> Int
length (B arr ofs end) = end - ofs

export
empty : Bytes
empty = unsafePerformIO $ allocate minimalCapacity

export
null : Bytes -> Bool
null (B arr ofs end) = (ofs == end)

%freeze empty

-- factor=1 ~ copy
-- factor=2 ~ grow
private
grow : Int -> Bytes -> IO Bytes
grow factor (B arr ofs end) = do
  maxUsed <- BA.peekInt 0 arr
  let bytesUsed = end - ofs
  let bytesAvailable =
        if maxUsed > end
          then bytesUsed
          else BA.size arr - ofs
  B arr' ofs' end' <- allocate $ (factor*bytesAvailable) `max` minimalCapacity
  BA.copy (arr, ofs) (arr', ofs') bytesUsed
  return $ B arr' ofs' (ofs' + bytesUsed)

%assert_total
export
snoc : Bytes -> Byte -> Bytes
snoc bs@(B arr ofs end) byte
    = if end >= BA.size arr
        then unsafePerformIO $ do  -- need more space
          grown <- grow 2 bs
          return $ snoc grown byte
        else unsafePerformIO $ do
          maxUsed <- BA.peekInt 0 arr
          if maxUsed > end
            then do  -- someone already took the headroom, need copying
              copy <- grow 2 bs
              return $ snoc copy byte
            else do  -- can mutate
              BA.pokeInt 0 (end+1) arr
              BA.poke end byte arr
              return $ B arr ofs (end+1)

infixl 7 |>
export
(|>) : Bytes -> Byte -> Bytes
(|>) = snoc

namespace SnocView
  data SnocView : Type where
    Nil : SnocView
    Snoc : (bs : Bytes) -> (b : Byte) -> SnocView

  export
  snocView : Bytes -> SnocView
  snocView (B arr ofs end) =
    if end == ofs
      then SnocView.Nil
      else unsafePerformIO $ do
        last <- BA.peek (end-1) arr
        return $ SnocView.Snoc (B arr ofs (end-1)) last

namespace ConsView
  data ConsView : Type where
    Nil : ConsView
    Cons : (b : Byte) -> (bs : Bytes) -> ConsView

  export
  consView : Bytes -> ConsView
  consView (B arr ofs end) =
    if end == ofs
      then ConsView.Nil
      else unsafePerformIO $ do
        first <- BA.peek ofs arr
        return $ ConsView.Cons first (B arr (ofs+1) end)

infixr 7 ++
%assert_total
export
(++) : Bytes -> Bytes -> Bytes
(++) bsL@(B arrL ofsL endL) bsR@(B arrR ofsR endR)
  = let countR = endR - ofsR in
      if endL + countR > BA.size arrL
        then unsafePerformIO $ do  -- need more space
          grown <- grow 2 bsL
          return $ grown ++ bsR
        else unsafePerformIO $ do
          maxUsedL <- BA.peekInt 0 arrL
          if maxUsedL > endL
            then do  -- headroom taken
              copyL <- grow 2 bsL
              return $ copyL ++ bsR
            else do  -- can mutate
              BA.pokeInt 0 (endL + countR) arrL
              BA.copy (arrR, ofsR) (arrL, endL) countR
              return $ B arrL ofsL (endL + countR)

export
dropPrefix : Int -> Bytes -> Bytes
dropPrefix n (B arr ofs end) = B arr (((ofs + n) `min` end) `max` dataOfs) end

export
takePrefix : Int -> Bytes -> Bytes
takePrefix n (B arr ofs end) = B arr ofs (((ofs + n) `min` end) `max` dataOfs)

export
pack : List Byte -> Bytes
pack = fromList empty
  where
    fromList : Bytes -> List Byte -> Bytes
    fromList bs []        = bs
    fromList bs (x :: xs) = fromList (bs `snoc` x) xs

export
unpack : Bytes -> List Byte
unpack bs with (consView bs)
  | Nil       = []
  | Cons x xs = x :: unpack (assert_smaller bs xs)

export
slice : Int -> Int -> Bytes -> Bytes
slice ofs' end' (B arr ofs end)
  = B arr
        (((ofs + ofs') `min` end) `max` dataOfs)
        (((ofs + end') `min` end) `max` dataOfs)

-- Folds with early exit.
-- If Bytes were a Functor, this would be equivalent
-- to a Traversable implementation interpreted in the Either monad.
data Result : Type -> Type where
  Stop : (result : a) -> Result a
  Cont : (acc : a) -> Result a

export
iterateR : (Byte -> a -> Result a) -> a -> Bytes -> a
iterateR f acc bs with (snocView bs)
  | Nil       = acc
  | Snoc ys y with (f y acc)
    | Stop result = result
    | Cont acc'   = iterateR f acc' (assert_smaller bs ys)

export
iterateL : (a -> Byte -> Result a) -> a -> Bytes -> a
iterateL f acc bs with (consView bs)
  | Nil       = acc
  | Cons y ys with (f acc y)
    | Stop result = result
    | Cont acc'   = iterateL f acc' (assert_smaller bs ys)

infixl 3 .:
private
(.:) : (a -> b) -> (c -> d -> a) -> (c -> d -> b)
(.:) g f x y = g (f x y)

export
foldr : (Byte -> a -> a) -> a -> Bytes -> a
foldr f = iterateR (Cont .: f)

export
foldl : (a -> Byte -> a) -> a -> Bytes -> a
foldl f = iterateL (Cont .: f)

export
spanLength : (Byte -> Bool) -> Bytes -> Int
spanLength p = iterateL step 0
  where
    step : Int -> Byte -> Result Int
    step n b with (p b)
      | True  = Cont (1 + n)
      | False = Stop n

find : Byte -> Bytes -> Maybe Int
find b (B arr ofs end) = unsafePerformIO $ BA.find b arr ofs end

export
splitAt : Int -> Bytes -> (Bytes, Bytes)
splitAt n bs = (takePrefix n bs, dropPrefix n bs)

export
splitOn : Byte -> Bytes -> (Bytes, Bytes)
splitOn b bs with (find b bs)
  | Nothing  = (bs, empty)
  | Just ofs = (takePrefix ofs bs, dropPrefix (ofs+1) bs)

export
splitsOn : Byte -> Bytes -> List Bytes
splitsOn b bs with (find b bs)
  | Nothing  = [bs]
  | Just ofs = takePrefix ofs bs :: splitsOn b (assert_smaller bs $ dropPrefix (ofs+1) bs)

export
asciiLines : Bytes -> List Bytes
asciiLines = splitsOn 0x0A

export
span : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
span p bs = splitAt (spanLength p bs) bs

export
break : (Byte -> Bool) -> Bytes -> (Bytes, Bytes)
break p bs = span (not . p) bs

private
cmp : Bytes -> Bytes -> Ordering
cmp (B arrL ofsL endL) (B arrR ofsR endR) = unsafePerformIO $ do
    let countL = endL - ofsL
    let countR = endR - ofsR
    let commonCount = countL `min` countR
    result <- BA.compare (arrL, ofsL) (arrR, ofsR) commonCount
    return $
      if result /= 0
        then i2o result
        else compare countL countR
  where
    i2o : Int -> Ordering
    i2o 0 = EQ
    i2o i = if i < 0 then LT else GT

implementation Eq Bytes where
  xs == ys = (Bytes.cmp xs ys == EQ)

implementation Ord Bytes where
  compare = Bytes.cmp

export
toString : Bytes -> String
toString = foldr (strCons . chr . toInt) ""

export
fromString : String -> Bytes
fromString = foldl (\bs, c => bs |> fromInt (ord c)) empty . unpack

implementation Show Bytes where
  show = ("b" ++) . show . toString

implementation Semigroup Bytes where
  (<+>) = (++)

implementation Monoid Bytes where
  neutral = empty

-- todo:
--
-- make indices Nats
-- Build a ByteString on top of Bytes?
-- migrate to (Bits 8)?
--
-- bidirectional growth?