git.iko.soy/Idris-dev
on master help sign in
Merge pull request #917 from david-christiansen/bounded

Add type classes for bounded things

commit101a8d33a3b033e4b7d6e9b5092b206c0474b574 authorEdwin Brady <edwin.brady@gmail.com> dateSat 22 Feb 2014, 12:18 (13 years ago) parent9c0581eea98726
6 files changed+58
compare with master
unifiedsplit
libs/prelude/Prelude/Classes.idr+28 libs/prelude/Prelude/Fin.idr+7 libs/prelude/Prelude/Nat.idr+3 test/bounded001/bounded001.idr+10 test/bounded001/expected+6 test/bounded001/run+4
libs/prelude/Prelude/Classes.idr+28
@@ -242,6 +242,34 @@ instance Ord Bits64 where
242242 else if l > r then GT
243243 else EQ
244244
245+-- ------------------------------------------------------------- [ Bounded ]
246+
247+class MinBound b where
248+ -- | The lower bound for the type
249+ minBound : b
250+
251+class MaxBound b where
252+ -- | The upper bound for the type
253+ maxBound : b
254+
255+instance MinBound Bits16 where
256+ minBound = 0x0
257+
258+instance MaxBound Bits16 where
259+ maxBound = 0xffff
260+
261+instance MinBound Bits32 where
262+ minBound = 0x0
263+
264+instance MaxBound Bits32 where
265+ maxBound = 0xffffffff
266+
267+instance MinBound Bits64 where
268+ minBound = 0x0
269+
270+instance MaxBound Bits64 where
271+ maxBound = 0xffffffffffffffff
272+
245273
246274-- ------------------------------------------------------------- [ Fractionals ]
247275
libs/prelude/Prelude/Fin.idr+7
@@ -61,6 +61,13 @@ total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
6161fSinjective refl = refl
6262
6363
64+instance MinBound (Fin (S n)) where
65+ minBound = fZ
66+
67+instance MaxBound (Fin (S n)) where
68+ maxBound = last
69+
70+
6471-- Construct a Fin from an integer literal which must fit in the given Fin
6572
6673natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
libs/prelude/Prelude/Nat.idr+3
@@ -142,6 +142,9 @@ instance Num Nat where
142142
143143 fromInteger = fromIntegerNat
144144
145+instance MinBound Nat where
146+ minBound = Z
147+
145148instance Cast Integer Nat where
146149 cast = fromInteger
147150
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