0 | module Control.Applicative.Const
  1 |
  2 | import Data.Contravariant
  3 | import Data.Bits
  4 |
  5 | %default total
  6 |
  7 | public export
  8 | record Const (a : Type) (b : Type) where
  9 |   constructor MkConst
 10 |   runConst : a
 11 |
 12 | public export
 13 | Eq a => Eq (Const a b) where
 14 |   (==) = (==) `on` runConst
 15 |
 16 | public export
 17 | Ord a => Ord (Const a b) where
 18 |   compare = compare `on` runConst
 19 |
 20 | export
 21 | Show a => Show (Const a b) where
 22 |   showPrec p (MkConst v) = showCon p "MkConst" (showArg v)
 23 |
 24 | public export
 25 | Semigroup a => Semigroup (Const a b) where
 26 |   MkConst x <+> MkConst y = MkConst (x <+> y)
 27 |
 28 | public export
 29 | Monoid a => Monoid (Const a b) where
 30 |   neutral = MkConst neutral
 31 |
 32 | public export
 33 | Num a => Num (Const a b) where
 34 |   MkConst x + MkConst y = MkConst (x + y)
 35 |   MkConst x * MkConst y = MkConst (x * y)
 36 |   fromInteger = MkConst . fromInteger
 37 |
 38 | public export
 39 | Neg a => Neg (Const a b) where
 40 |   negate (MkConst x)    = MkConst (negate x)
 41 |   MkConst x - MkConst y = MkConst (x - y)
 42 |
 43 | public export
 44 | Abs a => Abs (Const a b) where
 45 |   abs (MkConst x)    = MkConst (abs x)
 46 |
 47 | public export
 48 | Fractional a => Fractional (Const a b) where
 49 |   recip (MkConst x)     = MkConst (recip x)
 50 |   MkConst x / MkConst y = MkConst (x / y)
 51 |
 52 | public export
 53 | Integral a => Integral (Const a b) where
 54 |   MkConst x `div` MkConst y = MkConst (x `div` y)
 55 |   MkConst x `mod` MkConst y = MkConst (x `mod` y)
 56 |
 57 | public export
 58 | Bits a => Bits (Const a b) where
 59 |   Index = Index {a}
 60 |   MkConst x .&. MkConst y = MkConst (x .&. y)
 61 |   MkConst x .|. MkConst y = MkConst (x .|. y)
 62 |   MkConst x `xor` MkConst y = MkConst (x `xor` y)
 63 |   shiftL (MkConst v) ix = MkConst (shiftL v ix)
 64 |   shiftR (MkConst v) ix = MkConst (shiftR v ix)
 65 |   bit = MkConst . bit
 66 |   zeroBits = MkConst zeroBits
 67 |   complement (MkConst v) = MkConst (complement v)
 68 |   oneBits = MkConst oneBits
 69 |   complementBit (MkConst v) ix = MkConst (complementBit v ix)
 70 |   clearBit (MkConst v) ix = MkConst (clearBit v ix)
 71 |   testBit (MkConst v) ix = testBit v ix
 72 |   setBit (MkConst v) ix = MkConst (setBit v ix)
 73 |
 74 | public export
 75 | FromString a => FromString (Const a b) where
 76 |   fromString = MkConst . fromString
 77 |
 78 | public export
 79 | Functor (Const a) where
 80 |   map _ (MkConst v) = MkConst v
 81 |
 82 | public export
 83 | Contravariant (Const a) where
 84 |   contramap _ (MkConst v) = MkConst v
 85 |
 86 | public export
 87 | Monoid a => Applicative (Const a) where
 88 |   pure _ = MkConst neutral
 89 |   MkConst x <*> MkConst y = MkConst (x <+> y)
 90 |
 91 | public export
 92 | Foldable (Const a) where
 93 |   foldr _ acc _ = acc
 94 |   foldl _ acc _ = acc
 95 |   null _ = True
 96 |   toList _ = []
 97 |   foldMap _ _ = neutral
 98 |
 99 | public export
100 | Traversable (Const a) where
101 |   traverse _ (MkConst v) = pure (MkConst v)
102 |
103 | public export
104 | Bifunctor Const where
105 |   bimap f _ (MkConst v) = MkConst (f v)
106 |
107 | public export
108 | Bifoldable Const where
109 |   bifoldr f _ acc (MkConst v) = f v acc
110 |   bifoldl f _ acc (MkConst v) = f acc v
111 |   binull _ = False
112 |
113 | public export
114 | Bitraversable Const where
115 |   bitraverse f _ (MkConst v) = MkConst <$> f v
116 |