git.iko.soy/Idris-dev
on master help sign in
Port Haskell's Bounded class

This is useful for avoiding magic numbers.

commit5c1d7576112e51df904fd211097f6d98dae8a4b3 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 21 Feb 2014, 14:47 (13 years ago) parent0fa9239
5 files changed+52
compare with master
unifiedsplit
libs/prelude/Prelude/Classes.idr+27 libs/prelude/Prelude/Fin.idr+5 test/bounded001/bounded001.idr+10 test/bounded001/expected+6 test/bounded001/run+4
libs/prelude/Prelude/Classes.idr+27
@@ -242,6 +242,33 @@ instance Ord Bits64 where
242242 else if l > r then GT
243243 else EQ
244244
245+-- ------------------------------------------------------------- [ Bounded ]
246+
247+-- | Names the upper and lower elements of a type. Ord is not a superclass of
248+-- Bounded since types that are not totally ordered may also have upper and
249+-- lower bounds.
250+class Bounded b where
251+ -- | The lower bound for the type
252+ minBound : b
253+ -- | The upper bound for the type
254+ maxBound : b
255+
256+instance Bounded () where
257+ minBound = ()
258+ maxBound = ()
259+
260+instance Bounded Bits16 where
261+ minBound = 0x0
262+ maxBound = 0xffff
263+
264+instance Bounded Bits32 where
265+ minBound = 0x0
266+ maxBound = 0xffffffff
267+
268+instance Bounded Bits64 where
269+ minBound = 0x0
270+ maxBound = 0xffffffffffffffff
271+
245272
246273-- ------------------------------------------------------------- [ Fractionals ]
247274
libs/prelude/Prelude/Fin.idr+5
@@ -61,6 +61,11 @@ total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
6161fSinjective refl = refl
6262
6363
64+instance Bounded (Fin (S n)) where
65+ minBound = fZ
66+ maxBound = last
67+
68+
6469-- Construct a Fin from an integer literal which must fit in the given Fin
6570
6671natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
test/bounded001/bounded001.idrnew file+10
@@ -0,0 +1,10 @@
1+module Main
2+
3+-- Test wraparound from upper bounds of Bits types
4+main : IO ()
5+main = do putStrLn (show $ the Bits16 maxBound)
6+ putStrLn (show $ the Bits16 maxBound + 1)
7+ putStrLn (show $ the Bits32 maxBound)
8+ putStrLn (show $ the Bits32 maxBound + 1)
9+ putStrLn (show $ the Bits64 maxBound)
10+ putStrLn (show $ the Bits64 maxBound + 1)
test/bounded001/expectednew file+6
@@ -0,0 +1,6 @@
1+FFFF
2+0000
3+FFFFFFFF
4+00000000
5+FFFFFFFFFFFFFFFF
6+0000000000000000
test/bounded001/runnew file+4
@@ -0,0 +1,4 @@
1+#!/usr/bin/env bash
2+idris $@ bounded001.idr -o bounded001
3+./bounded001
4+rm -f bounded001 *.ibc