packages feed

idris-0.12.3: test/primitives006/load-test.idr

module Main

import Data.Bytes as B
import Data.ByteArray as BA

-- %flag C "-g3 -ggdb -O0"
%link C "array.o"

initialBuf : Bytes
initialBuf = pack . concat $ replicate 128 block
  where
    block : List Byte
    block = [10,32,1,10,100,32,1,10,255,32,1,10,1,10,255,32,1,10,255,32,1,10,255,32,1,10]

unRLE : Bytes -> Bytes
unRLE = fst . iterateL phi (empty, Nothing)
  where
    phi : (Bytes, Maybe Byte) -> Byte -> Result (Bytes, Maybe Byte)
    phi (bs, Nothing)  b = Cont (bs, Just b)
    phi (bs, Just cnt) b = Cont (bs ++ pack (replicate (cast $ prim__zextB8_Int cnt) b), Nothing)

unit : Int -> Byte -> IO ()
unit n b =
    let expanded = unRLE initialBuf
      in let elines = map (flip snoc b) (asciiLines expanded)
        in printLn $ (show b ++ "/" ++ show n, length expanded, length elines)

alloc : Int -> Int -> IO Int
alloc x 0 = pure x
alloc x i = do
  -- allocate an array
  arr <- BA.allocate (64 * 1024 * 1024)
  -- write "i" at offset 63M
  BA.pokeInt (63*1024*1024) i arr
  -- read number from offset 63M
  j <- BA.peekInt (63*1024*1024) arr
  -- count matches
  alloc (x + if i == j then 1 else 0) (i - 1)

main : IO ()
main = do
    -- First allocate 1024 64M arrays to break the C heap if there's a bug
    alloc 0 1024 >>= printLn

    -- Then, test Bytes
    traverse_ (unit n . prim__truncInt_B8) [1..n]
  where
    n = 8