git.iko.soy/Idris-dev
on master help sign in
Add *NZ functions
commitd79053d862e0580b17677a5746a3c35676501962 authorAndrew Cann <shum@canndrew.org> dateThu 2 Apr 2015, 17:23 (12 years ago) parentb9f0b7e
4 files changed+45−32
compare with master
unifiedsplit
libs/base/Data/Bits.idr+5−13 libs/contrib/Data/Hash.idr+3−7 libs/prelude/Prelude.idr+6−5 libs/prelude/Prelude/Nat.idr+31−7
libs/base/Data/Bits.idr+5−13
@@ -4,24 +4,16 @@ import Data.Fin
44
55%default total
66
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
147nextPow2 : Nat -> Nat
158nextPow2 Z = Z
16−nextPow2 x = if x == (2 `power` l2x)
17− then l2x
18− else S l2x
9+nextPow2 (S x) = if (S x) == (2 `power` l2x)
10+ then l2x
11+ else S l2x
1912 where
20− l2x = log2 x
13+ l2x = log2NZ (S x) SIsNotZ
2114
22−%assert_total
2315nextBytes : Nat -> Nat
24−nextBytes bits = (nextPow2 (bits `divCeil` 8))
16+nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
2517
2618machineTy : Nat -> Type
2719machineTy Z = Bits8
libs/contrib/Data/Hash.idr+3−7
@@ -40,14 +40,10 @@ private
4040mod64 : Integer -> Bits64
4141mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)
4242
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−
4943instance 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
5147
5248instance Hashable Integer where
5349 saltedHash64 i = saltedHash64 (mod64 i)
libs/prelude/Prelude.idr+6−5
@@ -335,8 +335,9 @@ total natEnumFromThen : Nat -> Nat -> Stream Nat
335335natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
336336total natEnumFromTo : Nat -> Nat -> List Nat
337337natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
338−partial natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
339−natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
338+total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
339+natEnumFromThenTo _ Z _ = []
340+natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))
340341
341342class Enum a where
342343 total pred : a -> a
@@ -350,7 +351,7 @@ class Enum a where
350351 enumFromThen x y = map fromNat (natEnumFromThen (toNat x) (toNat y))
351352 total enumFromTo : a -> a -> List a
352353 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
354355 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))
355356
356357instance Enum Nat where
@@ -375,7 +376,7 @@ instance Enum Integer where
375376 go [] = []
376377 go (x :: xs) = n + cast x :: go xs
377378 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)))
379380 where go : List Nat -> List Integer
380381 go [] = []
381382 go (x :: xs) = n + (cast x * inc) :: go xs
@@ -395,7 +396,7 @@ instance Enum Int where
395396 go acc (S k) m = go (m :: acc) k (m - 1)
396397 enumFromThen n inc = n :: enumFromThen (inc + n) inc
397398 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)))
399400 where go : List Nat -> List Int
400401 go [] = []
401402 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
274274-- Division and modulus
275275--------------------------------------------------------------------------------
276276
277−partial
278−modNat : Nat -> Nat -> Nat
279−modNat left (S right) = mod' left left right
277+SIsNotZ : {x: Nat} -> (S x = Z) -> Void
278+SIsNotZ Refl impossible
279+
280+modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
281+modNatNZ left Z p = void (p Refl)
282+modNatNZ left (S right) _ = mod' left left right
280283 where
281284 total mod' : Nat -> Nat -> Nat -> Nat
282285 mod' Z centre right = centre
@@ -287,8 +290,12 @@ modNat left (S right) = mod' left left right
287290 mod' left (centre - (S right)) right
288291
289292partial
290−divNat : Nat -> Nat -> Nat
291−divNat left (S right) = div' left left right
293+modNat : Nat -> Nat -> Nat
294+modNat left (S right) = modNatNZ left (S right) SIsNotZ
295+
296+divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
297+divNatNZ left Z p = void (p Refl)
298+divNatNZ left (S right) _ = div' left left right
292299 where
293300 total div' : Nat -> Nat -> Nat -> Nat
294301 div' Z centre right = Z
@@ -298,14 +305,31 @@ divNat left (S right) = div' left left right
298305 else
299306 S (div' left (centre - (S right)) right)
300307
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+
301321instance Integral Nat where
302322 div = divNat
303323 mod = modNat
304324
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+
305330partial
306331log2 : Nat -> Nat
307−log2 (S Z) = Z
308−log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
332+log2 (S n) = log2NZ (S n) SIsNotZ
309333
310334--------------------------------------------------------------------------------
311335-- GCD and LCM