0 | module Data.MSF.Event
  1 |
  2 | import public Data.List.Elem
  3 | import public Data.List.Quantifiers.Extra
  4 |
  5 | %default total
  6 |
  7 | --------------------------------------------------------------------------------
  8 | --          Event
  9 | --------------------------------------------------------------------------------
 10 |
 11 | ||| A data type isomorphic to `Maybe` used to signal
 12 | ||| occurences of discrete events.
 13 | public export
 14 | data Event : (a : Type) -> Type where
 15 |   NoEv : Event a
 16 |   Ev   : (v : a) -> Event a
 17 |
 18 | --------------------------------------------------------------------------------
 19 | --          Utilities
 20 | --------------------------------------------------------------------------------
 21 |
 22 | ||| Try to extract a value from an n-ary sum.
 23 | public export
 24 | project : (0 k : _) -> Elem k ks => Any f ks -> Event (f k)
 25 | project _ @{Here}    (Here p)  = Ev p
 26 | project v @{There _} (There p) = project v p
 27 | project _            _         = NoEv
 28 |
 29 | public export
 30 | maybeToEvent : Maybe a -> Event a
 31 | maybeToEvent Nothing  = NoEv
 32 | maybeToEvent (Just x) = Ev x
 33 |
 34 | public export
 35 | eventToMaybe : Event a -> Maybe a
 36 | eventToMaybe NoEv   = Nothing
 37 | eventToMaybe (Ev v) = Just v
 38 |
 39 | public export
 40 | fromEvent : Lazy a -> Event a -> a
 41 | fromEvent x NoEv   = x
 42 | fromEvent _ (Ev v) = v
 43 |
 44 | public export
 45 | toEvent : Bool -> Lazy a -> Event a
 46 | toEvent False _  = NoEv
 47 | toEvent True  va = Ev va
 48 |
 49 | public export
 50 | event : Lazy b -> Lazy (a -> b) -> Event a -> b
 51 | event v _ NoEv   = v
 52 | event _ f (Ev x) = f x
 53 |
 54 | public export
 55 | unionL : Event a -> Event a -> Event a
 56 | unionL (Ev x) _ = Ev x
 57 | unionL _      y = y
 58 |
 59 | public export
 60 | unionR : Event a -> Event a -> Event a
 61 | unionR _ (Ev y) = Ev y
 62 | unionR x _      = x
 63 |
 64 | public export
 65 | unionWith : (a -> a -> a) -> Event a -> Event a -> Event a
 66 | unionWith f (Ev x) (Ev y) = Ev $ f x y
 67 | unionWith _ x      y      = unionL x y
 68 |
 69 | public export
 70 | filter : (a -> Bool) -> Event a -> Event a
 71 | filter f NoEv    = NoEv
 72 | filter f (Ev va) = if f va then Ev va else NoEv
 73 |
 74 | --------------------------------------------------------------------------------
 75 | --          Interface Implementations
 76 | --------------------------------------------------------------------------------
 77 |
 78 | export
 79 | Show a => Show (Event a) where
 80 |   showPrec p NoEv   = "NoEv"
 81 |   showPrec p (Ev v) = showCon p "Ev" $ showArg v
 82 |
 83 | public export
 84 | Eq a => Eq (Event a) where
 85 |   NoEv == NoEv = True
 86 |   Ev x == Ev y = x == y
 87 |   _    == _    = False
 88 |
 89 | public export
 90 | Ord a => Ord (Event a) where
 91 |   compare NoEv   NoEv   = EQ
 92 |   compare NoEv   (Ev _) = LT
 93 |   compare (Ev _) NoEv   = GT
 94 |   compare (Ev x) (Ev y) = compare x y
 95 |
 96 | public export
 97 | Functor Event where
 98 |   map _ NoEv   = NoEv
 99 |   map f (Ev a) = Ev $ f a
100 |
101 | public export
102 | Applicative Event where
103 |   pure = Ev
104 |   Ev f <*> Ev a = Ev $ f a
105 |   _    <*> _    = NoEv
106 |
107 | public export
108 | Monad Event where
109 |   NoEv >>= _ = NoEv
110 |   Ev a >>= f = f a
111 |
112 | public export
113 | Foldable Event where
114 |   foldr _ v NoEv   = v
115 |   foldr f v (Ev a) = f a v
116 |
117 |   foldl _ v NoEv   = v
118 |   foldl f v (Ev a) = f v a
119 |
120 |   foldMap _ NoEv   = neutral
121 |   foldMap f (Ev a) = f a
122 |
123 |   null NoEv   = True
124 |   null (Ev a) = False
125 |
126 | public export %inline
127 | Traversable Event where
128 |   traverse _ NoEv   = pure NoEv
129 |   traverse f (Ev a) = Ev <$> f a
130 |
131 | public export %inline
132 | Alternative Event where
133 |   empty = NoEv
134 |   x <|> y = unionL x y
135 |
136 | public export %inline
137 | Semigroup a => Semigroup (Event a) where
138 |   (<+>) = unionWith (<+>)
139 |
140 | public export %inline
141 | Semigroup a => Monoid (Event a) where
142 |   neutral = NoEv
143 |
144 | --------------------------------------------------------------------------------
145 | --          More Utilities
146 | --------------------------------------------------------------------------------
147 |
148 | public export
149 | mapMaybe : (a -> Maybe b) -> Event a -> Event b
150 | mapMaybe f ev = ev >>= maybeToEvent . f
151 |