@@ -8,103 +8,160 @@ log2ceil n = let x = log2 n in
11−Bits : Nat -> Type
11+nextBits : Nat -> Type
12−Bits x with (log2ceil x)
12+nextBits x with (log2ceil x)
13 | (S (S (S (S (S (S _)))))) = Bits64
13 | (S (S (S (S (S (S _)))))) = Bits64
14 | (S (S (S (S (S O))))) = Bits32
14 | (S (S (S (S (S O))))) = Bits32
15 | (S (S (S (S O)))) = Bits16
15 | (S (S (S (S O)))) = Bits16
16 | _ = Bits8
16 | _ = Bits8
19+data Bits : Nat -> Type where
20+ MkBits : {n : Nat} -> nextBits n -> Bits n
18−intToBits : {n: Nat} -> Int -> Bits n
22+intToBits' : {n: Nat} -> Int -> nextBits n
19−intToBits {n=n} x with (Bits n)
23+intToBits' {n=n} x with (nextBits n)
20 | Bits8 = prim__intToB8 x
24 | Bits8 = prim__intToB8 x
21 | Bits16 = prim__intToB16 x
25 | Bits16 = prim__intToB16 x
22 | Bits32 = prim__intToB32 x
26 | Bits32 = prim__intToB32 x
23 | Bits64 = prim__intToB64 x
27 | Bits64 = prim__intToB64 x
25−instance Cast Int (Bits n) where
29+public
26− cast = intToBits
30+intToBits : {n : Nat} -> Int -> Bits n
31+intToBits n = MkBits (intToBits' n)
28−bitsShl : {n: Nat} -> Bits n -> Bits n -> Bits n
33+bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
29−bitsShl {n=n} x c with (Bits n)
34+bitsShl' {n=n} x c with (nextBits n)
30 | Bits8 = prim__shlB8 x c
35 | Bits8 = prim__shlB8 x c
31 | Bits16 = prim__shlB16 x c
36 | Bits16 = prim__shlB16 x c
32 | Bits32 = prim__shlB32 x c
37 | Bits32 = prim__shlB32 x c
33 | Bits64 = prim__shlB64 x c
38 | Bits64 = prim__shlB64 x c
41+bitsShl : Bits n -> Bits n -> Bits n
42+bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
35−bitsLShr : {n: Nat} -> Bits n -> Bits n -> Bits n
44+bitsLShr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
36−bitsLShr {n=n} x c with (Bits n)
45+bitsLShr' {n=n} x c with (nextBits n)
37 | Bits8 = prim__lshrB8 x c
46 | Bits8 = prim__lshrB8 x c
38 | Bits16 = prim__lshrB16 x c
47 | Bits16 = prim__lshrB16 x c
39 | Bits32 = prim__lshrB32 x c
48 | Bits32 = prim__lshrB32 x c
40 | Bits64 = prim__lshrB64 x c
49 | Bits64 = prim__lshrB64 x c
52+bitsLShr : Bits n -> Bits n -> Bits n
53+bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
42−bitsAShr : {n: Nat} -> Bits n -> Bits n -> Bits n
55+bitsAShr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
43−bitsAShr {n=n} x c with (Bits n)
56+bitsAShr' {n=n} x c with (nextBits n)
44 | Bits8 = prim__ashrB8 x c
57 | Bits8 = prim__ashrB8 x c
45 | Bits16 = prim__ashrB16 x c
58 | Bits16 = prim__ashrB16 x c
46 | Bits32 = prim__ashrB32 x c
59 | Bits32 = prim__ashrB32 x c
47 | Bits64 = prim__ashrB64 x c
60 | Bits64 = prim__ashrB64 x c
63+bitsAShr : Bits n -> Bits n -> Bits n
64+bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
49−bitsAnd : {n: Nat} -> Bits n -> Bits n -> Bits n
66+bitsAnd' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
50−bitsAnd {n=n} x y with (Bits n)
67+bitsAnd' {n=n} x y with (nextBits n)
51 | Bits8 = prim__andB8 x y
68 | Bits8 = prim__andB8 x y
52 | Bits16 = prim__andB16 x y
69 | Bits16 = prim__andB16 x y
53 | Bits32 = prim__andB32 x y
70 | Bits32 = prim__andB32 x y
54 | Bits64 = prim__andB64 x y
71 | Bits64 = prim__andB64 x y
74+bitsAnd : Bits n -> Bits n -> Bits n
75+bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
56−bitsOr : {n: Nat} -> Bits n -> Bits n -> Bits n
77+bitsOr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
57−bitsOr {n=n} x y with (Bits n)
78+bitsOr' {n=n} x y with (nextBits n)
58 | Bits8 = prim__orB8 x y
79 | Bits8 = prim__orB8 x y
59 | Bits16 = prim__orB16 x y
80 | Bits16 = prim__orB16 x y
60 | Bits32 = prim__orB32 x y
81 | Bits32 = prim__orB32 x y
61 | Bits64 = prim__orB64 x y
82 | Bits64 = prim__orB64 x y
85+bitsOr : Bits n -> Bits n -> Bits n
86+bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
63−bitsXOr : {n: Nat} -> Bits n -> Bits n -> Bits n
88+bitsXOr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
64−bitsXOr {n=n} x y with (Bits n)
89+bitsXOr' {n=n} x y with (nextBits n)
65 | Bits8 = prim__xorB8 x y
90 | Bits8 = prim__xorB8 x y
66 | Bits16 = prim__xorB16 x y
91 | Bits16 = prim__xorB16 x y
67 | Bits32 = prim__xorB32 x y
92 | Bits32 = prim__xorB32 x y
68 | Bits64 = prim__xorB64 x y
93 | Bits64 = prim__xorB64 x y
96+bitsXOr : Bits n -> Bits n -> Bits n
97+bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
70−bitsAdd : {n : Nat} -> Bits n -> Bits n -> Bits n
99+bitsAdd' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
71−bitsAdd {n=n} x y with (Bits n)
100+bitsAdd' {n=n} x y with (nextBits n)
72− | Bits8 = prim__addB8 x y
101+ | Bits8 = let pad = prim__intToB8 (the Int (cast (8-n))) in
73− | Bits16 = prim__addB16 x y
102+ prim__lshrB8 (prim__addB8 (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
74− | Bits32 = prim__addB32 x y
103+ | Bits16 = let pad = prim__intToB16 (the Int (cast (16-n))) in
75− | Bits64 = prim__addB64 x y
104+ prim__lshrB16 (prim__addB16 (prim__shlB16 x pad) (prim__shlB16 y pad)) pad
76−
105+ | Bits32 = let pad = prim__intToB32 (the Int (cast (32-n))) in
106+ prim__lshrB32 (prim__addB32 (prim__shlB32 x pad) (prim__shlB32 y pad)) pad
107+ | Bits64 = let pad = prim__intToB64 (the Int (cast (64-n))) in
108+ prim__lshrB64 (prim__addB64 (prim__shlB64 x pad) (prim__shlB64 y pad)) pad
111+bitsAdd : Bits n -> Bits n -> Bits n
112+bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
77−bitsSub : {n : Nat} -> Bits n -> Bits n -> Bits n
114+bitsSub' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
78−bitsSub {n=n} x y with (Bits n)
115+bitsSub' {n=n} x y with (nextBits n)
79 | Bits8 = prim__subB8 x y
116 | Bits8 = prim__subB8 x y
80 | Bits16 = prim__subB16 x y
117 | Bits16 = prim__subB16 x y
81 | Bits32 = prim__subB32 x y
118 | Bits32 = prim__subB32 x y
82 | Bits64 = prim__subB64 x y
119 | Bits64 = prim__subB64 x y
122+bitsSub : Bits n -> Bits n -> Bits n
123+bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
84−bitsMul : {n : Nat} -> Bits n -> Bits n -> Bits n
125+bitsMul' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
85−bitsMul {n=n} x y with (Bits n)
126+bitsMul' {n=n} x y with (nextBits n)
86 | Bits8 = prim__mulB8 x y
127 | Bits8 = prim__mulB8 x y
87 | Bits16 = prim__mulB16 x y
128 | Bits16 = prim__mulB16 x y
88 | Bits32 = prim__mulB32 x y
129 | Bits32 = prim__mulB32 x y
89 | Bits64 = prim__mulB64 x y
130 | Bits64 = prim__mulB64 x y
133+bitsMul : Bits n -> Bits n -> Bits n
134+bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
91−bitsSDiv : {n : Nat} -> Bits n -> Bits n -> Bits n
136+bitsSDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
92−bitsSDiv {n=n} x y with (Bits n)
137+bitsSDiv' {n=n} x y with (nextBits n)
93 | Bits8 = prim__sdivB8 x y
138 | Bits8 = prim__sdivB8 x y
94 | Bits16 = prim__sdivB16 x y
139 | Bits16 = prim__sdivB16 x y
95 | Bits32 = prim__sdivB32 x y
140 | Bits32 = prim__sdivB32 x y
96 | Bits64 = prim__sdivB64 x y
141 | Bits64 = prim__sdivB64 x y
144+bitsSDiv : Bits n -> Bits n -> Bits n
145+bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
98−bitsUDiv : {n : Nat} -> Bits n -> Bits n -> Bits n
147+bitsUDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
99−bitsUDiv {n=n} x y with (Bits n)
148+bitsUDiv' {n=n} x y with (nextBits n)
100 | Bits8 = prim__udivB8 x y
149 | Bits8 = prim__udivB8 x y
101 | Bits16 = prim__udivB16 x y
150 | Bits16 = prim__udivB16 x y
102 | Bits32 = prim__udivB32 x y
151 | Bits32 = prim__udivB32 x y
103 | Bits64 = prim__udivB64 x y
152 | Bits64 = prim__udivB64 x y
155+bitsUDiv : Bits n -> Bits n -> Bits n
156+bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
105−bitsToStr : {n : Nat} -> Bits n -> String
158+bitsToStr' : {n : Nat} -> nextBits n -> String
106−bitsToStr {n=n} x with (Bits n)
159+bitsToStr' {n=n} x with (nextBits n)
107 | Bits8 = prim__b8ToStr x
160 | Bits8 = prim__b8ToStr x
108 | Bits16 = prim__b16ToStr x
161 | Bits16 = prim__b16ToStr x
109 | Bits32 = prim__b32ToStr x
162 | Bits32 = prim__b32ToStr x
110 | Bits64 = prim__b64ToStr x
163 | Bits64 = prim__b64ToStr x
166+bitsToStr : Bits n -> String
167+bitsToStr (MkBits x) = bitsToStr' x