0 | module Web.Async.Widget
  1 |
  2 | import Data.Linear.Unique
  3 | import Derive.Prelude
  4 | import Monocle
  5 | import Text.HTML
  6 | import Text.HTML.DomID
  7 | import Text.HTML.Select
  8 | import Web.Async.Util
  9 | import Web.Async.View
 10 | import Web.Internal.Types
 11 |
 12 | %default total
 13 | %language ElabReflection
 14 | %hide Text.HTML.Node.a
 15 | %hide Types.SelectionMode.Select
 16 |
 17 | --------------------------------------------------------------------------------
 18 | -- EditRes
 19 | --------------------------------------------------------------------------------
 20 |
 21 | ||| Result of editing some kind of input element.
 22 | |||
 23 | ||| Input is either missing, invalid, or valid.
 24 | public export
 25 | data EditRes : Type -> Type where
 26 |   Missing : EditRes t
 27 |   Invalid : (err : String) -> EditRes t
 28 |   Valid   : (val : t) -> EditRes t
 29 |
 30 | %runElab derive "EditRes" [Show,Eq]
 31 |
 32 | export
 33 | toEither : EditRes t -> Either String ()
 34 | toEither (Invalid s) = Left s
 35 | toEither _           = Right ()
 36 |
 37 | export
 38 | toMaybe : EditRes t -> Maybe t
 39 | toMaybe (Valid v) = Just v
 40 | toMaybe _         = Nothing
 41 |
 42 | export
 43 | isValid : EditRes t -> Bool
 44 | isValid (Valid _) = True
 45 | isValid _         = False
 46 |
 47 | export
 48 | Functor EditRes where
 49 |   map f Missing     = Missing
 50 |   map f (Invalid v) = Invalid v
 51 |   map f (Valid v)   = Valid $ f v
 52 |
 53 | export
 54 | Applicative EditRes where
 55 |   pure = Valid
 56 |   Valid f   <*> v  = map f v
 57 |   Invalid x <*> _  = Invalid x
 58 |   Missing   <*> _  = Missing
 59 |
 60 | export
 61 | Monad EditRes where
 62 |   Missing   >>= _ = Missing
 63 |   Invalid x >>= _ = Invalid x
 64 |   Valid x   >>= f = f x
 65 |
 66 | --------------------------------------------------------------------------------
 67 | -- Widgets
 68 | --------------------------------------------------------------------------------
 69 |
 70 | ||| A `Widget e` is an interactive UI element that emits
 71 | ||| events of type `e`.
 72 | public export
 73 | record Widget e where
 74 |   constructor W
 75 |   node   : HTMLNode
 76 |   events : JSStream e
 77 |
 78 | export
 79 | adjNode : (HTMLNode -> HTMLNode) -> Widget e -> Widget e
 80 | adjNode f = {node $= f}
 81 |
 82 | ||| A dummy widget without a node representation that keeps
 83 | ||| producing the given value.
 84 | export
 85 | constant : t -> Widget t
 86 | constant = W Empty . fill
 87 |
 88 | ||| A dummy widget without a node representation that
 89 | ||| never fires an event.
 90 | export
 91 | empty : Widget t
 92 | empty = W Empty (pure ())
 93 |
 94 | ||| A dummy widget without a node representation that
 95 | ||| fires the given event exactly once.
 96 | export
 97 | once : t -> Widget t
 98 | once = W Empty . emit
 99 |
100 | ||| Adjusts a widget in such a way that its input streams ends
101 | ||| as soon as its node is removed from the DOM.
102 | |||
103 | ||| This is used in utilities such as `bindEd` or `Web.Async.List`, where
104 | ||| external events decide when a node is removed from the UI.
105 | export
106 | endOnRemove : Widget t -> JS es (Widget t)
107 | endOnRemove (W (El t as ns) es) = Prelude.do
108 |   E end <- event ()
109 |   pure $ W (El t (onRemove () :: as) ns) (haltOn end es)
110 | endOnRemove (W (EEl t as) es) = Prelude.do
111 |   E end <- event ()
112 |   pure $ W (EEl t $ onRemove () :: as) (haltOn end es)
113 | endOnRemove w = pure w
114 |
115 | export
116 | Functor Widget where
117 |   map f (W n p) = W n $ mapOutput f p
118 |
119 | ||| Sets the `disabled` attribute of the given element
120 | ||| if the given values is not a `Valid`.
121 | |||
122 | ||| This is useful for disabling components such as buttons
123 | ||| in the UI in case of invalid user input.
124 | export %inline
125 | disabledEdit : {0 a : _} -> Has JSErr es => Ref t -> EditRes a -> JS es ()
126 | disabledEdit r = disabled r . not . isValid
127 |
128 | --------------------------------------------------------------------------------
129 | -- Text Widgets
130 | --------------------------------------------------------------------------------
131 |
132 | export
133 | voidRef : Ref t -> Ref Void
134 | voidRef (Id id)  = Elem id
135 | voidRef (Elem s) = Elem s
136 | voidRef Body     = Body
137 | voidRef Document = Document
138 | voidRef Window   = Window
139 |
140 | ||| Adds a unique ID to the given list of attributes if it does not yet
141 | ||| already have an ID attribute, and returns the updated list plus the ID.
142 | export
143 | attributesWithID :
144 |      {auto lio : LIO io}
145 |   -> {s   : _}
146 |   -> (0 t : HTMLTag s)
147 |   -> List (Attribute t)
148 |   -> io (Ref t, List (Attribute t))
149 | attributesWithID t attrs =
150 |   case attrID attrs of
151 |     Nothing => map (\i => (tagRef t i, ref i :: attrs)) uniqueID
152 |     Just x  => pure (x, attrs)
153 |
154 | ||| Adds a unique ID to the given HTML node if it does not yet
155 | ||| already have an ID and returns the updated node plus its ID.
156 | |||
157 | ||| Returns `Nothing` in case the node in question is a `Raw` node
158 | ||| or a `Text` node.
159 | export
160 | nodeWithID : LIO io => HTMLNode -> io (Maybe (Ref Void, HTMLNode))
161 | nodeWithID (El t x y) =
162 |   (\(i,a) => Just (voidRef i,El t a y)) <$> attributesWithID t x
163 | nodeWithID (EEl t x)  =
164 |   (\(i,a) => Just (voidRef i,EEl t a)) <$> attributesWithID t x
165 | nodeWithID (Raw _)    = pure Nothing
166 | nodeWithID (Text _)   = pure Nothing
167 | nodeWithID Empty      = pure Nothing
168 |
169 | parameters (tpe      : InputType)
170 |            (attrs    : List (Attribute Tag.Input))
171 |
172 |   textInP : String -> JS es (Ref Tag.Input, Widget String)
173 |   textInP v = do
174 |     E es   <- eventFrom v
175 |     (i,as) <- attributesWithID Tag.Input attrs
176 |     pure (i, W (input $ [value v, type tpe, onInput Prelude.id] ++ as) es)
177 |
178 |   ||| An input element that emits `String` events.
179 |   export
180 |   textIn : String -> JS es (Widget String)
181 |   textIn v = snd <$> textInP v
182 |
183 |   ||| A validated input element that emits events of type
184 |   ||| `EditRes e`.
185 |   |||
186 |   ||| A custom validity message is set in case of invalid input.
187 |   export
188 |   valIn : String -> (String -> EditRes e) -> JS es (Widget $ EditRes e)
189 |   valIn v f = do
190 |     (r, W n evs) <- textInP v
191 |     pure $ W n (observe (validate r . toEither) (mapOutput f evs))
192 |
193 | public export
194 | record FileEv where
195 |   constructor FE
196 |   file : File
197 |   name : String
198 |
199 | fakeBody : String -> String
200 | fakeBody s =
201 |   case [<] <>< forget (split ('\\' ==) s) of
202 |     _ :< p => p
203 |     _      => ""
204 |
205 | toFile : InputInfo -> Maybe FileEv
206 | toFile (MkInputInfo p [f] _) = Just (FE f (fakeBody p))
207 | toFile _                     = Nothing
208 |
209 | export
210 | onFileIn : Sink e => (f : FileEv -> e) -> Attribute Tag.Input
211 | onFileIn f = Event (Input $ map f . toFile)
212 |
213 | export
214 | fileIn : Attributes Tag.Input -> JS es (Widget $ EditRes FileEv)
215 | fileIn as = do
216 |   E es   <- eventFrom Missing
217 |   pure $ W (input $ [type File, onFileIn Valid] ++ as) es
218 |
219 | --------------------------------------------------------------------------------
220 | -- Select Widgets
221 | --------------------------------------------------------------------------------
222 |
223 | listInit : Maybe t -> (v -> t) -> List v -> Maybe t
224 | listInit (Just x) f xs     = Just x
225 | listInit Nothing  f (x::_) = Just (f x)
226 | listInit _        _ _      = Nothing
227 |
228 | entriesInit : List (SelectEntry t) -> Maybe t
229 | entriesInit []                = Nothing
230 | entriesInit (Title _   :: xs) = entriesInit xs
231 | entriesInit (Entry v _ :: xs) = Just v
232 |
233 | parameters {auto eq  : Eq t}
234 |
235 |   ||| A select element displaying the values of type `v`
236 |   ||| shown in the given list.
237 |   |||
238 |   ||| It fires events of type `t`, and uses two functions, one for
239 |   ||| converting elements to events and one for displaying elements.
240 |   export
241 |   sel :
242 |        (v -> t)
243 |     -> (v -> String)
244 |     -> List v
245 |     -> List (Attribute Select)
246 |     -> Maybe t
247 |     -> JS es (Widget (EditRes t))
248 |   sel f g vs as m = do
249 |     let ini := listInit m f vs
250 |     E es <- eventFrom (maybe Missing Valid ini)
251 |     pure $ W (selectFromListBy vs ((ini ==) . Just . f) g (Valid . f) as) es
252 |
253 |   ||| A select element displaying the values of type `v`
254 |   ||| shown in the given list.
255 |   |||
256 |   ||| It fires events of type `t`, and uses two functions, one for
257 |   ||| converting elements to events and one for displaying elements.
258 |   export
259 |   selEntries :
260 |        List (SelectEntry t)
261 |     -> List (Attribute Select)
262 |     -> Maybe t
263 |     -> JS es (Widget (EditRes t))
264 |   selEntries vs as m = do
265 |     let ini := m <|> entriesInit vs
266 |     E es <- eventFrom (maybe Missing Valid ini)
267 |     pure $ W (selectEntries vs ((ini ==) . Just) Valid as) es
268 |
269 | --------------------------------------------------------------------------------
270 | -- Editor
271 | --------------------------------------------------------------------------------
272 |
273 | parameters {auto ff : Functor f}
274 |            {auto fg : Functor g}
275 |
276 |   export %inline
277 |   map2 : (x -> y) -> f (g x) -> f (g y)
278 |   map2 = map . map
279 |
280 |   export %inline
281 |   map3 : Functor h => (x -> y) -> f (g (h x)) -> f (g (h y))
282 |   map3 = map . map . map
283 |
284 | ||| An `Editor` describes how to create new interactive DOM elements that
285 | ||| typically serve as a form of (validated) user input. It consists of an
286 | ||| `HTMLNode` for displaying the editing form plus a stream of validated
287 | ||| input data.
288 | |||
289 | ||| An editor and its corresponding widgets can be something simple like a
290 | ||| text input field or a `<select>` element, or it can be highly complex
291 | ||| like a canvas and a group of DOM elements for editing molecules.
292 | |||
293 | ||| A couple of notes about how an editor is supposed to behave:
294 | |||   * If the initial value used for creating the widget is a `Nothing`,
295 | |||     the stream of values produced by the widget *may* already hold
296 | |||     a valid default value. In case no sensible default is available,
297 | |||     the stream's initial value *should* be `Missing`.
298 | |||   * If the initial value used for creating the widget is a `Just`,
299 | |||     the stream of values produced by the widget *must* emit a `Valid`
300 | |||     wrapping the provided initial value as its first output.
301 | |||
302 | ||| The above two rules make sure an editor behaves as expected, especially
303 | ||| when combining several editors in a form, or using the experimental
304 | ||| `bindEd` combinator.
305 | public export
306 | record Editor (t : Type) where
307 |   constructor E
308 |   ||| Create a node and stream of values from an optional initial value.
309 |   widget : Maybe t -> Act (Widget $ EditRes t)
310 |
311 | export
312 | adjEditor :
313 |      (Maybe a -> Maybe b)
314 |   -> (EditRes b -> EditRes a)
315 |   -> Editor b
316 |   -> Editor a
317 | adjEditor adjm adjres ed =
318 |   E $ \mb => Prelude.do
319 |     W n bs <- ed.widget (adjm mb)
320 |     pure $ W n $ P.mapOutput adjres bs
321 |
322 | ||| Views an editor through an isomorphism.
323 | export
324 | editI : Iso' t1 t2 -> Editor t1 -> Editor t2
325 | editI i (E f) = E $ map3 i.get_ . f . map i.reverseGet
326 |
327 | ||| Views the `new` values of an editor through a prism.
328 | export
329 | editP : Prism' t2 t1 -> Editor t1 -> Editor t2
330 | editP p (E f) = E $ map3 p.reverseGet . f . (>>= first p)
331 |
332 | ||| Refines an editor to produce values of a more restricted type.
333 | export
334 | refineEdit :
335 |      (t2 -> Maybe t1)
336 |   -> (refine : t1 -> EditRes t2)
337 |   -> Editor t1
338 |   -> Editor t2
339 | refineEdit ini f (E w) = E $ \m => map (>>= f) <$> w (m >>= ini)
340 |
341 | export %inline
342 | mapEvents : (JSStream (EditRes t) -> JSStream (EditRes t)) -> Editor t -> Editor t
343 | mapEvents f (E w) = E $ map {events $= f} . w
344 |
345 | ||| A dummy `Editor` for uneditable values.
346 | |||
347 | ||| The given value is fired exactly once.
348 | public export
349 | dummy : t -> Editor t
350 | dummy v = E $ \_ => pure (once (Valid v))
351 |
352 | export %inline
353 | txtEdit :
354 |      (parse : String -> EditRes t)
355 |   -> (tpe   : InputType)
356 |   -> (ini   : Maybe t -> String)
357 |   -> (attrs : List (Attribute Tag.Input))
358 |   -> Editor t
359 | txtEdit parse tpe ini as = E $ \m => valIn tpe as (ini m) parse
360 |
361 | export %inline
362 | selEdit :
363 |      {auto ip : Interpolation t}
364 |   -> {auto eq : Eq t}
365 |   -> (values  : List t)
366 |   -> (attrs   : List (Attribute Select))
367 |   -> Editor t
368 | selEdit vs = E . sel id interpolate vs
369 |
370 | export
371 | bindEd :
372 |      (cls  : Class)
373 |   -> (wrap : (fst,snd : HTMLNode) -> HTMLNode)
374 |   -> (a -> Editor b)
375 |   -> (Maybe b -> a)
376 |   -> Editor a
377 |   -> Editor b
378 | bindEd cls wrap f fromB (E w) =
379 |   E $ \mb => Prelude.do
380 |     i       <- uniqueID
381 |     W na as <- w (Just $ fromB mb)
382 |     W nb bs <- widget (f $ fromB mb) mb >>= wdgt i
383 |     pure $ W (wrap na nb) $
384 |       switchMap id $ cons bs $
385 |         P.tail as |> P.mapMaybe toMaybe |> P.evalMap (adj i)
386 |
387 |   where
388 |     wdgt : {0 t : _} -> DomID -> Widget t -> Act (Widget t)
389 |     wdgt i = endOnRemove . adjNode (\n => div [ref i, class cls] [n])
390 |
391 |     adj : DomID -> a -> Act (JSStream (EditRes b))
392 |     adj i va  = Prelude.do
393 |       W nb xs  <- widget (f va) Nothing >>= wdgt i
394 |       replace (elemRef i) nb
395 |       pure xs
396 |