packages feed

idris-0.9.11: test/buffer001-disabled/buffer001.idr

module Main

import Data.Buffer

em : Buffer 0
em = allocate 4

one : Bits32
one = 1

two : Bits8
two = 2

firstHalf : Buffer 4
firstHalf = appendBits32LE em 1 one

full : Buffer 8
full = appendBits8 firstHalf 4 two

firstByte : Bits8
firstByte = peekBits8 full 0

firstHalfView : Buffer 4
firstHalfView = peekBuffer full 0

firstHalfCopy : Buffer 4
firstHalfCopy = copy firstHalfView

oneFromFirstHalf : Bits32
oneFromFirstHalf = peekBits32LE firstHalf 0

oneFromFirstHalfCopy : Bits32
oneFromFirstHalfCopy = peekBits32LE firstHalfCopy 0

viewsAndCopiesPreserveEquality : Bool
viewsAndCopiesPreserveEquality = ( oneFromFirstHalf == one ) && ( oneFromFirstHalfCopy == one )

secondHalfWord : Bits32
secondHalfWord = peekBits32LE full 4

main : IO ()
main = do
  putStrLn $ show firstByte
  putStrLn $ show viewsAndCopiesPreserveEquality
  putStrLn $ show secondHalfWord