@@ -10,16 +10,18 @@ log2ceil n = let x = log2 n in
1010 then x+1
1111 else x
1212
13−nextBits : Nat -> Type
14−nextBits x with (log2ceil x)
15− | (S (S (S (S (S (S _)))))) = Bits64
16− | (S (S (S (S (S O))))) = Bits32
17− | (S (S (S (S O)))) = Bits16
18− | _ = Bits8
13+log2Bytes : Nat -> Nat
14+log2Bytes bits = (log2ceil (bits `div` 8))
15+
16+machineTy : Nat -> Type
17+machineTy O = Bits8
18+machineTy (S O) = Bits16
19+machineTy (S (S O)) = Bits32
20+machineTy (S (S (S _))) = Bits64
1921
2022public
2123data Bits : Nat -> Type where
22− MkBits : {n : Nat} -> nextBits n -> Bits n
24+ MkBits : {n : Nat} -> machineTy (log2Bytes n) -> Bits n
2325
2426pad8 : Nat -> (Bits8 -> Bits8 -> Bits8) -> Bits8 -> Bits8 -> Bits8
2527pad8 n f x y = prim__lshrB8 (f (prim__shlB8 x pad) (prim__shlB8 y pad)) pad
@@ -69,16 +71,16 @@ pow x y = if y > 0
6971 else 1
7072
7173%assert_total
72−intToBits' : {n : Nat} -> Int -> nextBits n
73−intToBits' {n=n} x with (nextBits n)
74− | Bits8 = let pad = (prim__intToB8 (cast (8-n))) in
75− prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
76− | Bits16 = let pad = (prim__intToB16 (cast (16-n))) in
77− prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
78− | Bits32 = let pad = (prim__intToB32 (cast (32-n))) in
79− prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
80− | Bits64 = let pad = (prim__intToB64 (cast (64-n))) in
81− prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
74+intToBits' : {n : Nat} -> Int -> machineTy (log2Bytes n)
75+intToBits' {n=n} x with (log2Bytes n)
76+ | O = let pad = (prim__intToB8 (cast (8-n))) in
77+ prim__lshrB8 (prim__shlB8 (prim__intToB8 x) pad) pad
78+ | S O = let pad = (prim__intToB16 (cast (16-n))) in
79+ prim__lshrB16 (prim__shlB16 (prim__intToB16 x) pad) pad
80+ | S (S O) = let pad = (prim__intToB32 (cast (32-n))) in
81+ prim__lshrB32 (prim__shlB32 (prim__intToB32 x) pad) pad
82+ | S (S (S _)) = let pad = (prim__intToB64 (cast (64-n))) in
83+ prim__lshrB64 (prim__shlB64 (prim__intToB64 x) pad) pad
8284
8385public
8486intToBits : {n : Nat} -> Int -> Bits n
@@ -87,215 +89,215 @@ intToBits n = MkBits (intToBits' n)
8789instance Cast Int (Bits n) where
8890 cast = intToBits
8991
90−unsafeBitsToInt' : {n : Nat} -> nextBits n -> Int
91−unsafeBitsToInt' {n=n} x with (nextBits n)
92− | Bits8 = prim__B32ToInt (prim__zextB8_32 x)
93− | Bits16 = prim__B32ToInt (prim__zextB16_32 x)
94− | Bits32 = prim__B32ToInt x
95− | Bits64 = prim__B32ToInt (prim__truncB64_32 x)
92+unsafeBitsToInt' : {n : Nat} -> machineTy (log2Bytes n) -> Int
93+unsafeBitsToInt' {n=n} x with (log2Bytes n)
94+ | O = prim__B32ToInt (prim__zextB8_32 x)
95+ | S O = prim__B32ToInt (prim__zextB16_32 x)
96+ | S (S O) = prim__B32ToInt x
97+ | S (S (S _)) = prim__B32ToInt (prim__truncB64_32 x)
9698
9799public
98100unsafeBitsToInt : Bits n -> Int
99101unsafeBitsToInt (MkBits x) = unsafeBitsToInt' x
100102
101−bitsShl' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
102−bitsShl' {n=n} x c with (nextBits n)
103− | Bits8 = pad8' n prim__shlB8 x c
104− | Bits16 = pad16' n prim__shlB16 x c
105− | Bits32 = pad32' n prim__shlB32 x c
106− | Bits64 = pad64' n prim__shlB64 x c
103+bitsShl' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
104+bitsShl' {n=n} x c with (log2Bytes n)
105+ | O = pad8' n prim__shlB8 x c
106+ | S O = pad16' n prim__shlB16 x c
107+ | S (S O) = pad32' n prim__shlB32 x c
108+ | S (S (S _)) = pad64' n prim__shlB64 x c
107109
108110public
109111bitsShl : Bits n -> Bits n -> Bits n
110112bitsShl (MkBits x) (MkBits y) = MkBits (bitsShl' x y)
111113
112−bitsLShr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
113−bitsLShr' {n=n} x c with (nextBits n)
114− | Bits8 = prim__lshrB8 x c
115− | Bits16 = prim__lshrB16 x c
116− | Bits32 = prim__lshrB32 x c
117− | Bits64 = prim__lshrB64 x c
114+bitsLShr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
115+bitsLShr' {n=n} x c with (log2Bytes n)
116+ | O = prim__lshrB8 x c
117+ | S O = prim__lshrB16 x c
118+ | S (S O) = prim__lshrB32 x c
119+ | S (S (S _)) = prim__lshrB64 x c
118120
119121public
120122bitsLShr : Bits n -> Bits n -> Bits n
121123bitsLShr (MkBits x) (MkBits y) = MkBits (bitsLShr' x y)
122124
123−bitsAShr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
124−bitsAShr' {n=n} x c with (nextBits n)
125− | Bits8 = prim__ashrB8 x c
126− | Bits16 = prim__ashrB16 x c
127− | Bits32 = prim__ashrB32 x c
128− | Bits64 = prim__ashrB64 x c
125+bitsAShr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
126+bitsAShr' {n=n} x c with (log2Bytes n)
127+ | O = prim__ashrB8 x c
128+ | S O = prim__ashrB16 x c
129+ | S (S O) = prim__ashrB32 x c
130+ | S (S (S _)) = prim__ashrB64 x c
129131
130132public
131133bitsAShr : Bits n -> Bits n -> Bits n
132134bitsAShr (MkBits x) (MkBits y) = MkBits (bitsAShr' x y)
133135
134−bitsAnd' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
135−bitsAnd' {n=n} x y with (nextBits n)
136− | Bits8 = prim__andB8 x y
137− | Bits16 = prim__andB16 x y
138− | Bits32 = prim__andB32 x y
139− | Bits64 = prim__andB64 x y
136+bitsAnd' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
137+bitsAnd' {n=n} x y with (log2Bytes n)
138+ | O = prim__andB8 x y
139+ | S O = prim__andB16 x y
140+ | S (S O) = prim__andB32 x y
141+ | S (S (S _)) = prim__andB64 x y
140142
141143public
142144bitsAnd : Bits n -> Bits n -> Bits n
143145bitsAnd (MkBits x) (MkBits y) = MkBits (bitsAnd' x y)
144146
145−bitsOr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
146−bitsOr' {n=n} x y with (nextBits n)
147− | Bits8 = prim__orB8 x y
148− | Bits16 = prim__orB16 x y
149− | Bits32 = prim__orB32 x y
150− | Bits64 = prim__orB64 x y
147+bitsOr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
148+bitsOr' {n=n} x y with (log2Bytes n)
149+ | O = prim__orB8 x y
150+ | S O = prim__orB16 x y
151+ | S (S O) = prim__orB32 x y
152+ | S (S (S _)) = prim__orB64 x y
151153
152154public
153155bitsOr : Bits n -> Bits n -> Bits n
154156bitsOr (MkBits x) (MkBits y) = MkBits (bitsOr' x y)
155157
156−bitsXOr' : {n: Nat} -> nextBits n -> nextBits n -> nextBits n
157−bitsXOr' {n=n} x y with (nextBits n)
158− | Bits8 = prim__xorB8 x y
159− | Bits16 = prim__xorB16 x y
160− | Bits32 = prim__xorB32 x y
161− | Bits64 = prim__xorB64 x y
158+bitsXOr' : {n: Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
159+bitsXOr' {n=n} x y with (log2Bytes n)
160+ | O = prim__xorB8 x y
161+ | S O = prim__xorB16 x y
162+ | S (S O) = prim__xorB32 x y
163+ | S (S (S _)) = prim__xorB64 x y
162164
163165public
164166bitsXOr : Bits n -> Bits n -> Bits n
165167bitsXOr (MkBits x) (MkBits y) = MkBits (bitsXOr' x y)
166168
167−bitsAdd' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
168−bitsAdd' {n=n} x y with (nextBits n)
169− | Bits8 = pad8 n prim__addB8 x y
170− | Bits16 = pad16 n prim__addB16 x y
171− | Bits32 = pad32 n prim__addB32 x y
172− | Bits64 = pad64 n prim__addB64 x y
169+bitsAdd' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
170+bitsAdd' {n=n} x y with (log2Bytes n)
171+ | O = pad8 n prim__addB8 x y
172+ | S O = pad16 n prim__addB16 x y
173+ | S (S O) = pad32 n prim__addB32 x y
174+ | S (S (S _)) = pad64 n prim__addB64 x y
173175
174176public
175177bitsAdd : Bits n -> Bits n -> Bits n
176178bitsAdd (MkBits x) (MkBits y) = MkBits (bitsAdd' x y)
177179
178−bitsSub' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
179−bitsSub' {n=n} x y with (nextBits n)
180− | Bits8 = pad8 n prim__subB8 x y
181− | Bits16 = pad16 n prim__subB16 x y
182− | Bits32 = pad32 n prim__subB32 x y
183− | Bits64 = pad64 n prim__subB64 x y
180+bitsSub' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
181+bitsSub' {n=n} x y with (log2Bytes n)
182+ | O = pad8 n prim__subB8 x y
183+ | S O = pad16 n prim__subB16 x y
184+ | S (S O) = pad32 n prim__subB32 x y
185+ | S (S (S _)) = pad64 n prim__subB64 x y
184186
185187public
186188bitsSub : Bits n -> Bits n -> Bits n
187189bitsSub (MkBits x) (MkBits y) = MkBits (bitsSub' x y)
188190
189−bitsMul' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
190−bitsMul' {n=n} x y with (nextBits n)
191− | Bits8 = pad8 n prim__mulB8 x y
192− | Bits16 = pad16 n prim__mulB16 x y
193− | Bits32 = pad32 n prim__mulB32 x y
194− | Bits64 = pad64 n prim__mulB64 x y
191+bitsMul' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
192+bitsMul' {n=n} x y with (log2Bytes n)
193+ | O = pad8 n prim__mulB8 x y
194+ | S O = pad16 n prim__mulB16 x y
195+ | S (S O) = pad32 n prim__mulB32 x y
196+ | S (S (S _)) = pad64 n prim__mulB64 x y
195197
196198public
197199bitsMul : Bits n -> Bits n -> Bits n
198200bitsMul (MkBits x) (MkBits y) = MkBits (bitsMul' x y)
199201
200202partial
201−bitsSDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
202−bitsSDiv' {n=n} x y with (nextBits n)
203− | Bits8 = prim__sdivB8 x y
204− | Bits16 = prim__sdivB16 x y
205− | Bits32 = prim__sdivB32 x y
206− | Bits64 = prim__sdivB64 x y
203+bitsSDiv' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
204+bitsSDiv' {n=n} x y with (log2Bytes n)
205+ | O = prim__sdivB8 x y
206+ | S O = prim__sdivB16 x y
207+ | S (S O) = prim__sdivB32 x y
208+ | S (S (S _)) = prim__sdivB64 x y
207209
208210public partial
209211bitsSDiv : Bits n -> Bits n -> Bits n
210212bitsSDiv (MkBits x) (MkBits y) = MkBits (bitsSDiv' x y)
211213
212214partial
213−bitsUDiv' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
214−bitsUDiv' {n=n} x y with (nextBits n)
215− | Bits8 = prim__udivB8 x y
216− | Bits16 = prim__udivB16 x y
217− | Bits32 = prim__udivB32 x y
218− | Bits64 = prim__udivB64 x y
215+bitsUDiv' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
216+bitsUDiv' {n=n} x y with (log2Bytes n)
217+ | O = prim__udivB8 x y
218+ | S O = prim__udivB16 x y
219+ | S (S O) = prim__udivB32 x y
220+ | S (S (S _)) = prim__udivB64 x y
219221
220222public partial
221223bitsUDiv : Bits n -> Bits n -> Bits n
222224bitsUDiv (MkBits x) (MkBits y) = MkBits (bitsUDiv' x y)
223225
224226partial
225−bitsSRem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
226−bitsSRem' {n=n} x y with (nextBits n)
227− | Bits8 = prim__sremB8 x y
228− | Bits16 = prim__sremB16 x y
229− | Bits32 = prim__sremB32 x y
230− | Bits64 = prim__sremB64 x y
227+bitsSRem' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
228+bitsSRem' {n=n} x y with (log2Bytes n)
229+ | O = prim__sremB8 x y
230+ | S O = prim__sremB16 x y
231+ | S (S O) = prim__sremB32 x y
232+ | S (S (S _)) = prim__sremB64 x y
231233
232234public partial
233235bitsSRem : Bits n -> Bits n -> Bits n
234236bitsSRem (MkBits x) (MkBits y) = MkBits (bitsSRem' x y)
235237
236238partial
237−bitsURem' : {n : Nat} -> nextBits n -> nextBits n -> nextBits n
238−bitsURem' {n=n} x y with (nextBits n)
239− | Bits8 = prim__uremB8 x y
240− | Bits16 = prim__uremB16 x y
241− | Bits32 = prim__uremB32 x y
242− | Bits64 = prim__uremB64 x y
239+bitsURem' : {n : Nat} -> machineTy (log2Bytes n) -> machineTy (log2Bytes n) -> machineTy (log2Bytes n)
240+bitsURem' {n=n} x y with (log2Bytes n)
241+ | O = prim__uremB8 x y
242+ | S O = prim__uremB16 x y
243+ | S (S O) = prim__uremB32 x y
244+ | S (S (S _)) = prim__uremB64 x y
243245
244246public partial
245247bitsURem : Bits n -> Bits n -> Bits n
246248bitsURem (MkBits x) (MkBits y) = MkBits (bitsURem' x y)
247249
248250-- TODO: Proofy comparisons via postulates
249−bitsLt' : (x : nextBits n) -> (y : nextBits n) -> Int
250−bitsLt' {n=n} x y with (nextBits n)
251− | Bits8 = prim__ltB8 x y
252− | Bits16 = prim__ltB16 x y
253− | Bits32 = prim__ltB32 x y
254− | Bits64 = prim__ltB64 x y
251+bitsLt' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
252+bitsLt' {n=n} x y with (log2Bytes n)
253+ | O = prim__ltB8 x y
254+ | S O = prim__ltB16 x y
255+ | S (S O) = prim__ltB32 x y
256+ | S (S (S _)) = prim__ltB64 x y
255257
256258public
257259bitsLt : (x : Bits n) -> (y : Bits n) -> Bool
258260bitsLt (MkBits x) (MkBits y) = bitsLt' x y /= 0
259261
260−bitsLte' : (x : nextBits n) -> (y : nextBits n) -> Int
261−bitsLte' {n=n} x y with (nextBits n)
262− | Bits8 = prim__lteB8 x y
263− | Bits16 = prim__lteB16 x y
264− | Bits32 = prim__lteB32 x y
265− | Bits64 = prim__lteB64 x y
262+bitsLte' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
263+bitsLte' {n=n} x y with (log2Bytes n)
264+ | O = prim__lteB8 x y
265+ | S O = prim__lteB16 x y
266+ | S (S O) = prim__lteB32 x y
267+ | S (S (S _)) = prim__lteB64 x y
266268
267269public
268270bitsLte : (x : Bits n) -> (y : Bits n) -> Bool
269271bitsLte (MkBits x) (MkBits y) = bitsLte' x y /= 0
270272
271−bitsEq' : (x : nextBits n) -> (y : nextBits n) -> Int
272−bitsEq' {n=n} x y with (nextBits n)
273− | Bits8 = prim__eqB8 x y
274− | Bits16 = prim__eqB16 x y
275− | Bits32 = prim__eqB32 x y
276− | Bits64 = prim__eqB64 x y
273+bitsEq' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
274+bitsEq' {n=n} x y with (log2Bytes n)
275+ | O = prim__eqB8 x y
276+ | S O = prim__eqB16 x y
277+ | S (S O) = prim__eqB32 x y
278+ | S (S (S _)) = prim__eqB64 x y
277279
278280public
279281bitsEq : (x : Bits n) -> (y : Bits n) -> Bool
280282bitsEq (MkBits x) (MkBits y) = bitsEq' x y /= 0
281283
282−bitsGte' : (x : nextBits n) -> (y : nextBits n) -> Int
283−bitsGte' {n=n} x y with (nextBits n)
284− | Bits8 = prim__gteB8 x y
285− | Bits16 = prim__gteB16 x y
286− | Bits32 = prim__gteB32 x y
287− | Bits64 = prim__gteB64 x y
284+bitsGte' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
285+bitsGte' {n=n} x y with (log2Bytes n)
286+ | O = prim__gteB8 x y
287+ | S O = prim__gteB16 x y
288+ | S (S O) = prim__gteB32 x y
289+ | S (S (S _)) = prim__gteB64 x y
288290
289291public
290292bitsGte : (x : Bits n) -> (y : Bits n) -> Bool
291293bitsGte (MkBits x) (MkBits y) = bitsGte' x y /= 0
292294
293−bitsGt' : (x : nextBits n) -> (y : nextBits n) -> Int
294−bitsGt' {n=n} x y with (nextBits n)
295− | Bits8 = prim__gtB8 x y
296− | Bits16 = prim__gtB16 x y
297− | Bits32 = prim__gtB32 x y
298− | Bits64 = prim__gtB64 x y
295+bitsGt' : (x : machineTy (log2Bytes n)) -> (y : machineTy (log2Bytes n)) -> Int
296+bitsGt' {n=n} x y with (log2Bytes n)
297+ | O = prim__gtB8 x y
298+ | S O = prim__gtB16 x y
299+ | S (S O) = prim__gtB32 x y
300+ | S (S (S _)) = prim__gtB64 x y
299301
300302public
301303bitsGt : (x : Bits n) -> (y : Bits n) -> Bool