git.iko.soy/Idris-dev
on master help sign in
Merge pull request #917 from david-christiansen/bounded
101a8d3Edwin Brady
libs/prelude/Prelude/Classes.idr+28
compare with master
unifiedsplit
@@ -242,6 +242,34 @@ instance Ord Bits64 where
242 else if l > r then GT
242 else if l > r then GT
243 else EQ
243 else EQ
244
244
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+
245
273
246-- ------------------------------------------------------------- [ Fractionals ]
274-- ------------------------------------------------------------- [ Fractionals ]
247
275
libs/prelude/Prelude/Fin.idr+7
@@ -61,6 +61,13 @@ total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
61fSinjective refl = refl
61fSinjective refl = refl
62
62
63
63
64+instance MinBound (Fin (S n)) where
65+ minBound = fZ
66+
67+instance MaxBound (Fin (S n)) where
68+ maxBound = last
69+
70+
64-- Construct a Fin from an integer literal which must fit in the given Fin
71-- Construct a Fin from an integer literal which must fit in the given Fin
65
72
66natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
73natToFin : Nat -> (n : Nat) -> Maybe (Fin n)
libs/prelude/Prelude/Nat.idr+3
@@ -142,6 +142,9 @@ instance Num Nat where
142
142
143 fromInteger = fromIntegerNat
143 fromInteger = fromIntegerNat
144
144
145+instance MinBound Nat where
146+ minBound = Z
147+
145instance Cast Integer Nat where
148instance Cast Integer Nat where
146 cast = fromInteger
149 cast = fromInteger
147
150
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