git.iko.soy/Idris-dev
on master help sign in
Add *NZ functions
d79053dAndrew Cann
libs/base/Data/Bits.idr+5−13
compare with master
unifiedsplit
@@ -4,24 +4,16 @@ import Data.Fin
4
4
5%default total
5%default total
6
6
7−partial
8−divCeil : Nat -> Nat -> Nat
9−divCeil x y = case x `mod` y of
10− Z => x `div` y
11− S _ => S (x `div` y)
12−
13−%assert_total
14nextPow2 : Nat -> Nat
7nextPow2 : Nat -> Nat
15nextPow2 Z = Z
8nextPow2 Z = Z
16−nextPow2 x = if x == (2 `power` l2x)
9+nextPow2 (S x) = if (S x) == (2 `power` l2x)
17− then l2x
10+ then l2x
18− else S l2x
11+ else S l2x
19 where
12 where
20− l2x = log2 x
13+ l2x = log2NZ (S x) SIsNotZ
21
14
22−%assert_total
23nextBytes : Nat -> Nat
15nextBytes : Nat -> Nat
24−nextBytes bits = (nextPow2 (bits `divCeil` 8))
16+nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
25
17
26machineTy : Nat -> Type
18machineTy : Nat -> Type
27machineTy Z = Bits8
19machineTy Z = Bits8
libs/contrib/Data/Hash.idr+3−7
@@ -40,14 +40,10 @@ private
40mod64 : Integer -> Bits64
40mod64 : Integer -> Bits64
41mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)
41mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)
42
42
43−%assert_total
44−saltedHash64Bits64 : Bits64 -> Bits64 -> Bits64
45−saltedHash64Bits64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)
46− salt
47− [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto
48−
49instance Hashable Bits64 where
43instance Hashable Bits64 where
50− saltedHash64 = saltedHash64Bits64
44+ saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)
45+ salt
46+ [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto
51
47
52instance Hashable Integer where
48instance Hashable Integer where
53 saltedHash64 i = saltedHash64 (mod64 i)
49 saltedHash64 i = saltedHash64 (mod64 i)
libs/prelude/Prelude.idr+6−5
@@ -335,8 +335,9 @@ total natEnumFromThen : Nat -> Nat -> Stream Nat
335natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
335natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
336total natEnumFromTo : Nat -> Nat -> List Nat
336total natEnumFromTo : Nat -> Nat -> List Nat
337natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
337natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
338−partial natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
338+total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
339+natEnumFromThenTo _ Z _ = []
339−natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
340+natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))
340
341
341class Enum a where
342class Enum a where
342 total pred : a -> a
343 total pred : a -> a
@@ -350,7 +351,7 @@ class Enum a where
350 enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))
351 enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))
351 total enumFromTo : a -> a -> List a
352 total enumFromTo : a -> a -> List a
352 enumFromTo x y = map fromNat (natEnumFromTo (toNat x) (toNat y))
353 enumFromTo x y = map fromNat (natEnumFromTo (toNat x) (toNat y))
353− partial enumFromThenTo : a -> a -> a -> List a
354+ total enumFromThenTo : a -> a -> a -> List a
354 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
355 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
355
356
356instance Enum Nat where
357instance Enum Nat where
@@ -375,7 +376,7 @@ instance Enum Integer where
375 go [] = []
376 go [] = []
376 go (x :: xs) = n + cast x :: go xs
377 go (x :: xs) = n + cast x :: go xs
377 enumFromThenTo _ 0 _ = []
378 enumFromThenTo _ 0 _ = []
378− enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc))))
379+ enumFromThenTo n inc m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs inc) - 1))) SIsNotZ)))
379 where go : List Nat -> List Integer
380 where go : List Nat -> List Integer
380 go [] = []
381 go [] = []
381 go (x :: xs) = n + (cast x * inc) :: go xs
382 go (x :: xs) = n + (cast x * inc) :: go xs
@@ -395,7 +396,7 @@ instance Enum Int where
395 go acc (S k) m = go (m :: acc) k (m - 1)
396 go acc (S k) m = go (m :: acc) k (m - 1)
396 enumFromThen n inc = n :: enumFromThen (inc + n) inc
397 enumFromThen n inc = n :: enumFromThen (inc + n) inc
397 enumFromThenTo _ 0 _ = []
398 enumFromThenTo _ 0 _ = []
398− enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
399+ enumFromThenTo n inc m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs inc) - 1))) SIsNotZ)))
399 where go : List Nat -> List Int
400 where go : List Nat -> List Int
400 go [] = []
401 go [] = []
401 go (x :: xs) = n + (cast x * inc) :: go xs
402 go (x :: xs) = n + (cast x * inc) :: go xs
libs/prelude/Prelude/Nat.idr+31−7
@@ -274,9 +274,12 @@ fact (S n) = (S n) * fact n
274-- Division and modulus
274-- Division and modulus
275--------------------------------------------------------------------------------
275--------------------------------------------------------------------------------
276
276
277−partial
277+SIsNotZ : {x: Nat} -> (S x = Z) -> Void
278+SIsNotZ Refl impossible
279+
278−modNat : Nat -> Nat -> Nat
280+modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
281+modNatNZ left Z p = void (p Refl)
279−modNat left (S right) = mod' left left right
282+modNatNZ left (S right) _ = mod' left left right
280 where
283 where
281 total mod' : Nat -> Nat -> Nat -> Nat
284 total mod' : Nat -> Nat -> Nat -> Nat
282 mod' Z centre right = centre
285 mod' Z centre right = centre
@@ -287,8 +290,12 @@ modNat left (S right) = mod' left left right
287 mod' left (centre - (S right)) right
290 mod' left (centre - (S right)) right
288
291
289partial
292partial
293+modNat : Nat -> Nat -> Nat
294+modNat left (S right) = modNatNZ left (S right) SIsNotZ
295+
290−divNat : Nat -> Nat -> Nat
296+divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
297+divNatNZ left Z p = void (p Refl)
291−divNat left (S right) = div' left left right
298+divNatNZ left (S right) _ = div' left left right
292 where
299 where
293 total div' : Nat -> Nat -> Nat -> Nat
300 total div' : Nat -> Nat -> Nat -> Nat
294 div' Z centre right = Z
301 div' Z centre right = Z
@@ -298,14 +305,31 @@ divNat left (S right) = div' left left right
298 else
305 else
299 S (div' left (centre - (S right)) right)
306 S (div' left (centre - (S right)) right)
300
307
308+partial
309+divNat : Nat -> Nat -> Nat
310+divNat left (S right) = divNatNZ left (S right) SIsNotZ
311+
312+divCeilNZ : Nat -> (y: Nat) -> Not (y = 0) -> Nat
313+divCeilNZ x y p = case (modNatNZ x y p) of
314+ Z => divNatNZ x y p
315+ S _ => S (divNatNZ x y p)
316+
317+partial
318+divCeil : Nat -> Nat -> Nat
319+divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
320+
301instance Integral Nat where
321instance Integral Nat where
302 div = divNat
322 div = divNat
303 mod = modNat
323 mod = modNat
304
324
325+log2NZ : (x: Nat) -> Not (x = Z) -> Nat
326+log2NZ Z p = void (p Refl)
327+log2NZ (S Z) _ = Z
328+log2NZ (S (S n)) _ = S (log2NZ (assert_smaller (S (S n)) (S (divNatNZ n 2 SIsNotZ))) SIsNotZ)
329+
305partial
330partial
306log2 : Nat -> Nat
331log2 : Nat -> Nat
307−log2 (S Z) = Z
332+log2 (S n) = log2NZ (S n) SIsNotZ
308−log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
309
333
310--------------------------------------------------------------------------------
334--------------------------------------------------------------------------------
311-- GCD and LCM
335-- GCD and LCM