git.iko.soy/Idris-dev
on master help sign in
Merge pull request #2052 from canndrew/partial-div-mod

Partial div mod

commitb450502f917dc40f172984cb3209b3e2e9ffaadc authorEdwin Brady <edwin.brady@gmail.com> dateTue 14 Apr 2015, 20:19 (12 years ago) parent12b3fa2d79053d
5 files changed+70−44
compare with master
unifiedsplit
libs/base/Data/Bits.idr+5−10 libs/contrib/Network/Cgi.idr+1−1 libs/prelude/Prelude.idr+4−4 libs/prelude/Prelude/Classes.idr+24−12 libs/prelude/Prelude/Nat.idr+36−17
libs/base/Data/Bits.idr+5−10
@@ -4,21 +4,16 @@ import Data.Fin
44
55%default total
66
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−
127nextPow2 : Nat -> Nat
138nextPow2 Z = Z
14−nextPow2 x = if x == (2 `power` l2x)
15− then l2x
16− else S l2x
9+nextPow2 (S x) = if (S x) == (2 `power` l2x)
10+ then l2x
11+ else S l2x
1712 where
18− l2x = log2 x
13+ l2x = log2NZ (S x) SIsNotZ
1914
2015nextBytes : Nat -> Nat
21−nextBytes bits = (nextPow2 (bits `divCeil` 8))
16+nextBytes bits = (nextPow2 (divCeilNZ bits 8 SIsNotZ))
2217
2318machineTy : Nat -> Type
2419machineTy Z = Bits8
libs/contrib/Network/Cgi.idr+1−1
@@ -108,7 +108,7 @@ getVars seps query = mapMaybe readVar (split (\x => elem x seps) query)
108108 | _ = Nothing
109109
110110getContent : Int -> IO String
111−getContent x = getC (toNat x) "" where
111+getContent x = getC (cast x) "" where
112112 getC : Nat -> String -> IO String
113113 getC Z acc = return $ reverse acc
114114 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
242242total natEnumFromTo : Nat -> Nat -> List Nat
243243natEnumFromTo n m = map (plus n) (natRange ((S m) - n))
244244total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat
245−natEnumFromThenTo _ Z _ = []
246−natEnumFromThenTo n inc m = map (plus n . (* inc)) (natRange (S ((m - n) `div` inc)))
245+natEnumFromThenTo _ Z _ = []
246+natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (m - n) (S inc) SIsNotZ)))
247247
248248class Enum a where
249249 total pred : a -> a
@@ -282,7 +282,7 @@ instance Enum Integer where
282282 go [] = []
283283 go (x :: xs) = n + cast x :: go xs
284284 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)))
286286 where go : List Nat -> List Integer
287287 go [] = []
288288 go (x :: xs) = n + (cast x * inc) :: go xs
@@ -302,7 +302,7 @@ instance Enum Int where
302302 go acc (S k) m = go (m :: acc) k (m - 1)
303303 enumFromThen n inc = n :: enumFromThen (inc + n) inc
304304 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)))
306306 where go : List Nat -> List Int
307307 go [] = []
308308 go (x :: xs) = n + (cast x * inc) :: go xs
libs/prelude/Prelude/Classes.idr+24−12
@@ -315,10 +315,12 @@ class Integral a where
315315
316316-- ---------------------------------------------------------------- [ Integers ]
317317divBigInt : Integer -> Integer -> Integer
318−divBigInt = prim__sdivBigInt
318+divBigInt x y = case y == 0 of
319+ False => prim__sdivBigInt x y
319320
320321modBigInt : Integer -> Integer -> Integer
321−modBigInt = prim__sremBigInt
322+modBigInt x y = case y == 0 of
323+ False => prim__sremBigInt x y
322324
323325instance Integral Integer where
324326 div = divBigInt
@@ -327,10 +329,12 @@ instance Integral Integer where
327329-- --------------------------------------------------------------------- [ Int ]
328330
329331divInt : Int -> Int -> Int
330−divInt = prim__sdivInt
332+divInt x y = case y == 0 of
333+ False => prim__sdivInt x y
331334
332335modInt : Int -> Int -> Int
333−modInt = prim__sremInt
336+modInt x y = case y == 0 of
337+ False => prim__sremInt x y
334338
335339instance Integral Int where
336340 div = divInt
@@ -338,10 +342,12 @@ instance Integral Int where
338342
339343-- ------------------------------------------------------------------- [ Bits8 ]
340344divB8 : Bits8 -> Bits8 -> Bits8
341−divB8 = prim__sdivB8
345+divB8 x y = case y == 0 of
346+ False => prim__sdivB8 x y
342347
343348modB8 : Bits8 -> Bits8 -> Bits8
344−modB8 = prim__sremB8
349+modB8 x y = case y == 0 of
350+ False => prim__sremB8 x y
345351
346352instance Integral Bits8 where
347353 div = divB8
@@ -349,10 +355,12 @@ instance Integral Bits8 where
349355
350356-- ------------------------------------------------------------------ [ Bits16 ]
351357divB16 : Bits16 -> Bits16 -> Bits16
352−divB16 = prim__sdivB16
358+divB16 x y = case y == 0 of
359+ False => prim__sdivB16 x y
353360
354361modB16 : Bits16 -> Bits16 -> Bits16
355−modB16 = prim__sremB16
362+modB16 x y = case y == 0 of
363+ False => prim__sremB16 x y
356364
357365instance Integral Bits16 where
358366 div = divB16
@@ -360,10 +368,12 @@ instance Integral Bits16 where
360368
361369-- ------------------------------------------------------------------ [ Bits32 ]
362370divB32 : Bits32 -> Bits32 -> Bits32
363−divB32 = prim__sdivB32
371+divB32 x y = case y == 0 of
372+ False => prim__sdivB32 x y
364373
365374modB32 : Bits32 -> Bits32 -> Bits32
366−modB32 = prim__sremB32
375+modB32 x y = case y == 0 of
376+ False => prim__sremB32 x y
367377
368378instance Integral Bits32 where
369379 div = divB32
@@ -371,10 +381,12 @@ instance Integral Bits32 where
371381
372382-- ------------------------------------------------------------------ [ Bits64 ]
373383divB64 : Bits64 -> Bits64 -> Bits64
374−divB64 = prim__sdivB64
384+divB64 x y = case y == 0 of
385+ False => prim__sdivB64 x y
375386
376387modB64 : Bits64 -> Bits64 -> Bits64
377−modB64 = prim__sremB64
388+modB64 x y = case y == 0 of
389+ False => prim__sremB64 x y
378390
379391instance Integral Bits64 where
380392 div = divB64
libs/prelude/Prelude/Nat.idr+36−17
@@ -288,10 +288,12 @@ fact (S n) = (S n) * fact n
288288-- Division and modulus
289289--------------------------------------------------------------------------------
290290
291−total
292−modNat : Nat -> Nat -> Nat
293−modNat left Z = left
294−modNat left (S right) = mod' left left right
291+SIsNotZ : {x: Nat} -> (S x = Z) -> Void
292+SIsNotZ Refl impossible
293+
294+modNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
295+modNatNZ left Z p = void (p Refl)
296+modNatNZ left (S right) _ = mod' left left right
295297 where
296298 total mod' : Nat -> Nat -> Nat -> Nat
297299 mod' Z centre right = centre
@@ -301,10 +303,13 @@ modNat left (S right) = mod' left left right
301303 else
302304 mod' left (centre - (S right)) right
303305
304−total
305−divNat : Nat -> Nat -> Nat
306−divNat left Z = S left -- div by zero
307−divNat left (S right) = div' left left right
306+partial
307+modNat : Nat -> Nat -> Nat
308+modNat left (S right) = modNatNZ left (S right) SIsNotZ
309+
310+divNatNZ : Nat -> (y: Nat) -> Not (y = Z) -> Nat
311+divNatNZ left Z p = void (p Refl)
312+divNatNZ left (S right) _ = div' left left right
308313 where
309314 total div' : Nat -> Nat -> Nat -> Nat
310315 div' Z centre right = Z
@@ -314,23 +319,42 @@ divNat left (S right) = div' left left right
314319 else
315320 S (div' left (centre - (S right)) right)
316321
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+
317335instance Integral Nat where
318336 div = divNat
319337 mod = modNat
320338
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
321345log2 : Nat -> Nat
322−log2 Z = Z
323−log2 (S Z) = Z
324−log2 n = S (log2 (assert_smaller n (n `divNat` 2)))
346+log2 (S n) = log2NZ (S n) SIsNotZ
325347
326348--------------------------------------------------------------------------------
327349-- GCD and LCM
328350--------------------------------------------------------------------------------
351+partial
329352gcd : Nat -> Nat -> Nat
330353gcd a Z = a
331354gcd a b = assert_total (gcd b (a `modNat` b))
332355
333−total lcm : Nat -> Nat -> Nat
356+partial
357+lcm : Nat -> Nat -> Nat
334358lcm _ Z = Z
335359lcm Z _ = Z
336360lcm x y = divNat (x * y) (gcd x y)
@@ -724,11 +748,6 @@ total sucMinR : (l : Nat) -> minimum l (S l) = l
724748sucMinR Z = Refl
725749sucMinR (S l) = cong (sucMinR l)
726750
727−-- div and mod
728−total modZeroZero : (n : Nat) -> mod 0 n = Z
729−modZeroZero Z = Refl
730−modZeroZero (S n) = Refl
731−
732751--------------------------------------------------------------------------------
733752-- Proofs
734753--------------------------------------------------------------------------------