1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
|
{-# OPTIONS --guardedness #-}
module Main where
open import Agda.Builtin.FromNat
open import Data.Bytestring.Base as Bytestring
open import Data.Bytestring.Builder.Base
open import Data.List.Base using ([]; _∷_)
import Data.Nat.Literals; instance numberNat = Data.Nat.Literals.number
open import Data.Product.Base using (_×_; _,_)
open import Data.String using (String; _++_; fromVec)
open import Data.Unit.Base using (⊤; tt)
import Data.Vec.Base as Vec
open import Data.Word8.Base as Word8
import Data.Word8.Show as Word8
import Data.Word8.Literals; instance numberWord8 = Data.Word8.Literals.number
open import Data.Word64.Base as Word64 using (Word64)
import Data.Word64.Unsafe as Word64
import Data.Word64.Show as Word64
import Data.Word64.Literals; instance numberWord64 = Data.Word64.Literals.number
open import Function.Base using (_$_)
open import IO.Base
open import IO.Finite
1⋯3 : Bytestring
1⋯3 = toBytestring
$ List.concat
$ word8 1
∷ word64LE 2
∷ word64BE 3
∷ []
1,⋯,3 : Word8 × Word64 × Word64
1,⋯,3 = getWord8 1⋯3 0
, getWord64LE 1⋯3 1
, getWord64BE 1⋯3 9
main : Main
main = run $ do
let separation = fromVec (Vec.replicate 72 '-')
putStrLn (Bytestring.show 1⋯3)
putStrLn separation
let (one , two , three) = 1,⋯,3
let word8test : Word8 → IO _
word8test w = do
putStrLn (Word8.show w ++ " = " ++ Word8.showBits w)
putStrLn (Word8.show w ++ " = " ++ Word8.showHexa w)
putStrLn (Word8.show w ++ " = " ++ Word8.show (Word8.fromBits (Word8.toBits w)))
let word64test : Word64 → IO _
word64test w = do
putStrLn separation
putStrLn (Word64.show w ++ " = " ++ Word64.showBits w)
putStrLn (Word64.show w ++ " = " ++ Word64.showHexa w)
putStrLn (Word64.show w ++ " = " ++ Word64.show (Word64.fromBits (Word64.toBits w)))
word8test one
word8test (Word8.fromℕ 144)
word64test two
word64test three
word64test (Word64.fromℕ 2024)
|
