0 | module Hedgehog.Internal.Util
  1 |
  2 | import Data.DPair
  3 | import Data.List
  4 | import Data.Colist
  5 |
  6 | %default total
  7 |
  8 | --------------------------------------------------------------------------------
  9 | --          SafeDiv
 10 | --------------------------------------------------------------------------------
 11 |
 12 | ||| Interface providing a safe (total) division operation
 13 | ||| by proving that the divisor is non-zero.
 14 | public export
 15 | interface Neg a => SafeDiv (0 a : Type) (0 pred : a -> Type) | a where
 16 |   total safeDiv' : (n,d : a) -> (0 prf : pred d) -> a
 17 |
 18 | public export
 19 | SafeDiv Int (\d => d == 0 = False) where
 20 |   safeDiv' n d _ = n `div` d
 21 |
 22 | public export
 23 | SafeDiv Integer (\d => d == 0 = False) where
 24 |   safeDiv' n d _ = n `div` d
 25 |
 26 | public export
 27 | SafeDiv Double (\d => d == 0 = False) where
 28 |   safeDiv' n d _ = n / d
 29 |
 30 | public export total
 31 | safeDiv : SafeDiv a pred => (n,d : a) -> {auto 0 ok : pred d} -> a
 32 | safeDiv n d = safeDiv' n d ok
 33 |
 34 | public export total
 35 | fromPred : (a -> Bool) -> a -> Maybe a
 36 | fromPred p a = guard (p a) $> a
 37 |
 38 | --------------------------------------------------------------------------------
 39 | --          ToInteger
 40 | --------------------------------------------------------------------------------
 41 |
 42 | public export
 43 | interface Num a => ToInteger a where
 44 |   toInteger : a -> Integer
 45 |
 46 |   toNat : a -> Nat
 47 |   toNat = integerToNat . toInteger
 48 |
 49 | public export
 50 | ToInteger Integer where toInteger = id
 51 |
 52 | public export
 53 | ToInteger Int8 where toInteger = cast
 54 |
 55 | public export
 56 | ToInteger Int16 where toInteger = cast
 57 |
 58 | public export
 59 | ToInteger Int32 where toInteger = cast
 60 |
 61 | public export
 62 | ToInteger Int64 where toInteger = cast
 63 |
 64 | public export
 65 | ToInteger Int where toInteger = cast
 66 |
 67 | public export
 68 | ToInteger Bits8 where toInteger = cast
 69 |
 70 | public export
 71 | ToInteger Bits16 where toInteger = cast
 72 |
 73 | public export
 74 | ToInteger Bits32 where toInteger = cast
 75 |
 76 | public export
 77 | ToInteger Bits64 where toInteger = cast
 78 |
 79 | public export
 80 | ToInteger Nat where
 81 |   toInteger = cast
 82 |   toNat = id
 83 |
 84 | public export
 85 | ToInteger Double where toInteger = cast
 86 |
 87 | public export
 88 | fromIntegral : ToInteger a => Num b => a -> b
 89 | fromIntegral = fromInteger . toInteger
 90 |
 91 | public export
 92 | round : Num a => Double -> a
 93 | round v =
 94 |   let f  := floor v
 95 |       v' := if v - f < 0.5 then f else ceiling v
 96 |    in fromInteger $ cast v'
 97 |
 98 | --------------------------------------------------------------------------------
 99 | --          (Lazy) List Utilities
100 | --------------------------------------------------------------------------------
101 |
102 | public export
103 | iterateBefore : (p : a -> Bool) -> (a -> a) -> (v : a) -> Colist a
104 | iterateBefore p f = takeBefore p . iterate f
105 |
106 | public export
107 | iterateBefore0 : Eq a => Num a => (a -> a) -> (start : a) -> Colist a
108 | iterateBefore0 = iterateBefore (0 ==)
109 |
110 | ||| Prepends the first list in reverse order to the
111 | ||| second list.
112 | public export
113 | prepRev : List a -> List a -> List a
114 | prepRev []        ys = ys
115 | prepRev (x :: xs) ys = prepRev xs (x :: ys)
116 |
117 | public export
118 | signum : Ord a => Neg a => a -> a
119 | signum x =
120 |   if x < 0 then (-1) else if x == 0 then 0 else 1
121 |
122 | --------------------------------------------------------------------------------
123 | --          Colists
124 | --------------------------------------------------------------------------------
125 |
126 | ||| Cons an element on to the front of a list unless it is already there.
127 | public export total
128 | consNub : Eq a => a -> Colist a -> Colist a
129 | consNub x []          = [x]
130 | consNub x l@(y :: xs) = if x == y then l else x :: l
131 |
132 | public export
133 | concatColist : Colist (Colist a) -> Colist a
134 | concatColist ((x :: xs) :: ys)       = x :: concatColist (xs :: ys)
135 | concatColist ([] :: (x :: xs) :: ys) = x :: concatColist (xs :: ys)
136 | concatColist _                       = []
137 |
138 | public export
139 | concatMapColist : (a -> Colist b) -> Colist a -> Colist b
140 | concatMapColist f = concatColist . map f
141 |
142 | public export
143 | fromFoldable : Foldable f => f a -> Colist a
144 | fromFoldable = fromList . toList
145 |