git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2052 from canndrew/partial-div-mod
b450502Edwin Brady
libs/base/Data/Bits.idr+5−10
compare with master
unifiedsplit
@@ -4,21 +4,16 @@ import Data.Fin
4
4
5%default total
5%default total
6
6
7−divCeil : Nat -> Nat -> Nat
8−divCeil x y = case x `mod` y of
9− Z => x `div` y
10− S _ => S (x `div` y)
11−
12nextPow2 : Nat -> Nat
7nextPow2 : Nat -> Nat
13nextPow2 Z = Z
8nextPow2 Z = Z
14−nextPow2 x = if x == (2 `power` l2x)
9+nextPow2 (S x) = if (S x) == (2 `power` l2x)
15− then l2x
10+ then l2x
16− else S l2x
11+ else S l2x
17 where
12 where
18− l2x = log2 x
13+ l2x = log2NZ (S x) SIsNotZ
19
14
20nextBytes : Nat -> Nat
15nextBytes : Nat -> Nat
21−nextBytes bits = (nextPow2 (bits `divCeil` 8))
16+nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
22
17
23machineTy : Nat -> Type
18machineTy : Nat -> Type
24machineTy Z = Bits8
19machineTy Z = Bits8
libs/contrib/Network/Cgi.idr+1−1
@@ -108,7 +108,7 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
108 | _ = Nothing
108 | _ = Nothing
109
109
110getContent : Int -> IO String
110getContent : Int -> IO String
111−getContent x = getC (toNat x) "" where
111+getContent x = getC (cast x) "" where
112 getC : Nat -> String -> IO String
112 getC : Nat -> String -> IO String
113 getC Z acc = return $ reverse acc
113 getC Z acc = return $ reverse acc
114 getC (S k) acc = do x <- getChar
114 getC (S k) acc = do x <- getChar
libs/prelude/Prelude.idr+4−4
@@ -242,8 +242,8 @@ natEnumFromThen n inc = n :: natEnumFromThen (inc + n) inc
242total natEnumFromTo : Nat -> Nat -> List Nat
242total natEnumFromTo : Nat -> Nat -> List Nat
243natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
243natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
244total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
244total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
245−natEnumFromThenTo _ Z _ = []
245+natEnumFromThenTo _ Z _ = []
246−natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
246+natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))
247
247
248class Enum a where
248class Enum a where
249 total pred : a -> a
249 total pred : a -> a
@@ -282,7 +282,7 @@ instance Enum Integer where
282 go [] = []
282 go [] = []
283 go (x :: xs) = n + cast x :: go xs
283 go (x :: xs) = n + cast x :: go xs
284 enumFromThenTo _ 0 _ = []
284 enumFromThenTo _ 0 _ = []
285− enumFromThenTo n inc m = go (natRange (S (fromInteger (abs (m - n)) `div` fromInteger (abs inc))))
285+ enumFromThenTo n inc m = go (natRange (S (divNatNZ (fromInteger (abs (m - n))) (S (fromInteger ((abs inc) - 1))) SIsNotZ)))
286 where go : List Nat -> List Integer
286 where go : List Nat -> List Integer
287 go [] = []
287 go [] = []
288 go (x :: xs) = n + (cast x * inc) :: go xs
288 go (x :: xs) = n + (cast x * inc) :: go xs
@@ -302,7 +302,7 @@ instance Enum Int where
302 go acc (S k) m = go (m :: acc) k (m - 1)
302 go acc (S k) m = go (m :: acc) k (m - 1)
303 enumFromThen n inc = n :: enumFromThen (inc + n) inc
303 enumFromThen n inc = n :: enumFromThen (inc + n) inc
304 enumFromThenTo _ 0 _ = []
304 enumFromThenTo _ 0 _ = []
305− enumFromThenTo n inc m = go (natRange (S (cast {to=Nat} (abs (m - n)) `div` cast {to=Nat} (abs inc))))
305+ enumFromThenTo n inc m = go (natRange (S (divNatNZ (cast {to=Nat} (abs (m - n))) (S (cast {to=Nat} ((abs inc) - 1))) SIsNotZ)))
306 where go : List Nat -> List Int
306 where go : List Nat -> List Int
307 go [] = []
307 go [] = []
308 go (x :: xs) = n + (cast x * inc) :: go xs
308 go (x :: xs) = n + (cast x * inc) :: go xs
libs/prelude/Prelude/Classes.idr+24−12
@@ -315,10 +315,12 @@ class Integral a where
315
315
316-- ---------------------------------------------------------------- [ Integers ]
316-- ---------------------------------------------------------------- [ Integers ]
317divBigInt : Integer -> Integer -> Integer
317divBigInt : Integer -> Integer -> Integer
318+divBigInt x y = case y == 0 of
318−divBigInt = prim__sdivBigInt
319+ False => prim__sdivBigInt x y
319
320
320modBigInt : Integer -> Integer -> Integer
321modBigInt : Integer -> Integer -> Integer
322+modBigInt x y = case y == 0 of
321−modBigInt = prim__sremBigInt
323+ False => prim__sremBigInt x y
322
324
323instance Integral Integer where
325instance Integral Integer where
324 div = divBigInt
326 div = divBigInt
@@ -327,10 +329,12 @@ instance Integral Integer where
327-- --------------------------------------------------------------------- [ Int ]
329-- --------------------------------------------------------------------- [ Int ]
328
330
329divInt : Int -> Int -> Int
331divInt : Int -> Int -> Int
332+divInt x y = case y == 0 of
330−divInt = prim__sdivInt
333+ False => prim__sdivInt x y
331
334
332modInt : Int -> Int -> Int
335modInt : Int -> Int -> Int
336+modInt x y = case y == 0 of
333−modInt = prim__sremInt
337+ False => prim__sremInt x y
334
338
335instance Integral Int where
339instance Integral Int where
336 div = divInt
340 div = divInt
@@ -338,10 +342,12 @@ instance Integral Int where
338
342
339-- ------------------------------------------------------------------- [ Bits8 ]
343-- ------------------------------------------------------------------- [ Bits8 ]
340divB8 : Bits8 -> Bits8 -> Bits8
344divB8 : Bits8 -> Bits8 -> Bits8
345+divB8 x y = case y == 0 of
341−divB8 = prim__sdivB8
346+ False => prim__sdivB8 x y
342
347
343modB8 : Bits8 -> Bits8 -> Bits8
348modB8 : Bits8 -> Bits8 -> Bits8
349+modB8 x y = case y == 0 of
344−modB8 = prim__sremB8
350+ False => prim__sremB8 x y
345
351
346instance Integral Bits8 where
352instance Integral Bits8 where
347 div = divB8
353 div = divB8
@@ -349,10 +355,12 @@ instance Integral Bits8 where
349
355
350-- ------------------------------------------------------------------ [ Bits16 ]
356-- ------------------------------------------------------------------ [ Bits16 ]
351divB16 : Bits16 -> Bits16 -> Bits16
357divB16 : Bits16 -> Bits16 -> Bits16
358+divB16 x y = case y == 0 of
352−divB16 = prim__sdivB16
359+ False => prim__sdivB16 x y
353
360
354modB16 : Bits16 -> Bits16 -> Bits16
361modB16 : Bits16 -> Bits16 -> Bits16
362+modB16 x y = case y == 0 of
355−modB16 = prim__sremB16
363+ False => prim__sremB16 x y
356
364
357instance Integral Bits16 where
365instance Integral Bits16 where
358 div = divB16
366 div = divB16
@@ -360,10 +368,12 @@ instance Integral Bits16 where
360
368
361-- ------------------------------------------------------------------ [ Bits32 ]
369-- ------------------------------------------------------------------ [ Bits32 ]
362divB32 : Bits32 -> Bits32 -> Bits32
370divB32 : Bits32 -> Bits32 -> Bits32
371+divB32 x y = case y == 0 of
363−divB32 = prim__sdivB32
372+ False => prim__sdivB32 x y
364
373
365modB32 : Bits32 -> Bits32 -> Bits32
374modB32 : Bits32 -> Bits32 -> Bits32
375+modB32 x y = case y == 0 of
366−modB32 = prim__sremB32
376+ False => prim__sremB32 x y
367
377
368instance Integral Bits32 where
378instance Integral Bits32 where
369 div = divB32
379 div = divB32
@@ -371,10 +381,12 @@ instance Integral Bits32 where
371
381
372-- ------------------------------------------------------------------ [ Bits64 ]
382-- ------------------------------------------------------------------ [ Bits64 ]
373divB64 : Bits64 -> Bits64 -> Bits64
383divB64 : Bits64 -> Bits64 -> Bits64
384+divB64 x y = case y == 0 of
374−divB64 = prim__sdivB64
385+ False => prim__sdivB64 x y
375
386
376modB64 : Bits64 -> Bits64 -> Bits64
387modB64 : Bits64 -> Bits64 -> Bits64
388+modB64 x y = case y == 0 of
377−modB64 = prim__sremB64
389+ False => prim__sremB64 x y
378
390
379instance Integral Bits64 where
391instance Integral Bits64 where
380 div = divB64
392 div = divB64
libs/prelude/Prelude/Nat.idr+36−17
@@ -288,10 +288,12 @@ fact (S n) = (S n) * fact n
288-- Division and modulus
288-- Division and modulus
289--------------------------------------------------------------------------------
289--------------------------------------------------------------------------------
290
290
291−total
291+SIsNotZ : {x: Nat} -> (S x = Z) -> Void
292+SIsNotZ Refl impossible
293+
292−modNat : Nat -> Nat -> Nat
294+modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
293−modNat left Z = left
295+modNatNZ left Z p = void (p Refl)
294−modNat left (S right) = mod' left left right
296+modNatNZ left (S right) _ = mod' left left right
295 where
297 where
296 total mod' : Nat -> Nat -> Nat -> Nat
298 total mod' : Nat -> Nat -> Nat -> Nat
297 mod' Z centre right = centre
299 mod' Z centre right = centre
@@ -301,10 +303,13 @@ modNat left (S right) = mod' left left right
301 else
303 else
302 mod' left (centre - (S right)) right
304 mod' left (centre - (S right)) right
303
305
304−total
306+partial
307+modNat : Nat -> Nat -> Nat
308+modNat left (S right) = modNatNZ left (S right) SIsNotZ
309+
305−divNat : Nat -> Nat -> Nat
310+divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
306−divNat left Z = S left -- div by zero
311+divNatNZ left Z p = void (p Refl)
307−divNat left (S right) = div' left left right
312+divNatNZ left (S right) _ = div' left left right
308 where
313 where
309 total div' : Nat -> Nat -> Nat -> Nat
314 total div' : Nat -> Nat -> Nat -> Nat
310 div' Z centre right = Z
315 div' Z centre right = Z
@@ -314,23 +319,42 @@ divNat left (S right) = div' left left right
314 else
319 else
315 S (div' left (centre - (S right)) right)
320 S (div' left (centre - (S right)) right)
316
321
322+partial
323+divNat : Nat -> Nat -> Nat
324+divNat left (S right) = divNatNZ left (S right) SIsNotZ
325+
326+divCeilNZ : Nat -> (y: Nat) -> Not (y = 0) -> Nat
327+divCeilNZ x y p = case (modNatNZ x y p) of
328+ Z => divNatNZ x y p
329+ S _ => S (divNatNZ x y p)
330+
331+partial
332+divCeil : Nat -> Nat -> Nat
333+divCeil x (S y) = divCeilNZ x (S y) SIsNotZ
334+
317instance Integral Nat where
335instance Integral Nat where
318 div = divNat
336 div = divNat
319 mod = modNat
337 mod = modNat
320
338
339+log2NZ : (x: Nat) -> Not (x = Z) -> Nat
340+log2NZ Z p = void (p Refl)
341+log2NZ (S Z) _ = Z
342+log2NZ (S (S n)) _ = S (log2NZ (assert_smaller (S (S n)) (S (divNatNZ n 2 SIsNotZ))) SIsNotZ)
343+
344+partial
321log2 : Nat -> Nat
345log2 : Nat -> Nat
322−log2 Z = Z
346+log2 (S n) = log2NZ (S n) SIsNotZ
323−log2 (S Z) = Z
324−log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
325
347
326--------------------------------------------------------------------------------
348--------------------------------------------------------------------------------
327-- GCD and LCM
349-- GCD and LCM
328--------------------------------------------------------------------------------
350--------------------------------------------------------------------------------
351+partial
329gcd : Nat -> Nat -> Nat
352gcd : Nat -> Nat -> Nat
330gcd a Z = a
353gcd a Z = a
331gcd a b = assert_total (gcd b (a `modNat` b))
354gcd a b = assert_total (gcd b (a `modNat` b))
332
355
356+partial
333−total lcm : Nat -> Nat -> Nat
357+lcm : Nat -> Nat -> Nat
334lcm _ Z = Z
358lcm _ Z = Z
335lcm Z _ = Z
359lcm Z _ = Z
336lcm x y = divNat (x * y) (gcd x y)
360lcm x y = divNat (x * y) (gcd x y)
@@ -724,11 +748,6 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l
724sucMinR Z = Refl
748sucMinR Z = Refl
725sucMinR (S l) = cong (sucMinR l)
749sucMinR (S l) = cong (sucMinR l)
726
750
727−-- div and mod
728−total modZeroZero : (n : Nat) -> mod 0 n = Z
729−modZeroZero Z = Refl
730−modZeroZero (S n) = Refl
731−
732--------------------------------------------------------------------------------
751--------------------------------------------------------------------------------
733-- Proofs
752-- Proofs
734--------------------------------------------------------------------------------
753--------------------------------------------------------------------------------