git.iko.soy/Idris-dev
on 7afa310 help sign in
Idris-dev/test/buffer001-disabled/buffer001.idr
45 lines 870 B history raw
1module Main
3import Data.Buffer
5em : Buffer 0
6em = allocate 4
8one : Bits32
9one = 1
11two : Bits8
12two = 2
14firstHalf : Buffer 4
15firstHalf = appendBits32LE em 1 one
17full : Buffer 8
18full = appendBits8 firstHalf 4 two
20firstByte : Bits8
21firstByte = peekBits8 full 0
23firstHalfView : Buffer 4
24firstHalfView = peekBuffer full 0
26firstHalfCopy : Buffer 4
27firstHalfCopy = copy firstHalfView
29oneFromFirstHalf : Bits32
30oneFromFirstHalf = peekBits32LE firstHalf 0
32oneFromFirstHalfCopy : Bits32
33oneFromFirstHalfCopy = peekBits32LE firstHalfCopy 0
35viewsAndCopiesPreserveEquality : Bool
36viewsAndCopiesPreserveEquality = ( oneFromFirstHalf == one ) && ( oneFromFirstHalfCopy == one )
38secondHalfWord : Bits32
39secondHalfWord = peekBits32LE full 4
41main : IO ()
42main = do
43 putStrLn $ show firstByte
44 putStrLn $ show viewsAndCopiesPreserveEquality
45 putStrLn $ show secondHalfWord