0 | module Web.MVC.Widget
 1 |
 2 | import Web.MVC
 3 |
 4 | %default total
 5 |
 6 | --------------------------------------------------------------------------------
 7 | --          Widgets
 8 | --------------------------------------------------------------------------------
 9 |
10 |
11 | ||| A `Widget` is a standalone UI element that manages its own
12 | ||| state. It packages up all aspects of an MVC component into a
13 | ||| single piece of data that can be passed around and transformed,
14 | ||| before finally turned into a runnable program with `runWidget`.
15 | |||
16 | ||| See the various parameters of `Web.MVC.runMVC` for further
17 | ||| explanation.
18 | public export
19 | record Widget where
20 |   constructor MkWidget
21 |
22 |   ||| The internal state of the widget (model)
23 |   0 St : Type
24 |   ||| Event type
25 |   0 Ev : Type
26 |   ||| Initial state
27 |   init : St
28 |   ||| Given the initial state, set up the  UI
29 |   setup : St -> Cmd Ev
30 |   ||| Update the state based on the latest event
31 |   update : Ev -> St -> St
32 |   ||| Update the UI based on the latest event and the current state
33 |   display : Ev -> St -> Cmd Ev
34 |
35 | ||| `w1 <+> w2` is the independent composition of widgets `w1` and
36 | ||| `w2`, with the product state and the sum events.
37 | public export
38 | Semigroup Widget where
39 |   w1 <+> w2 = MkWidget
40 |     { St = (w1.St, w2.St)
41 |     , Ev = Either w1.Ev w2.Ev
42 |     , init = (w1.init, w2.init)
43 |     , setup = \(s1, s2) => batch
44 |         [ Left <$> w1.setup s1
45 |         , Right <$> w2.setup s2
46 |         ]
47 |     , update = \ev, (s1, s2) => case ev of
48 |         Left  ev1 => (w1.update ev1 s1, s2)
49 |         Right ev2 => (s1, w2.update ev2 s2)
50 |     , display = \ev, (s1, s2) => case ev of
51 |         Left ev  => Left <$> w1.display ev s1
52 |         Right ev => Right <$> w2.display ev s2
53 |     }
54 |
55 | ||| `neutral` is the trivial widget with trivial state and no events
56 | public export
57 | Monoid Widget where
58 |   neutral = MkWidget
59 |     { St = ()
60 |     , Ev = Void
61 |     , init = ()
62 |     , setup = neutral
63 |     , update = absurd
64 |     , display = \_, _ => neutral
65 |     }
66 |
67 | ||| Run a `Widget`. This is basically `runMVC` with the arguments
68 | ||| constructed from the fields of `Widget`. Since this function
69 | ||| produces no result, there's no going back from here: all `Widget`
70 | ||| composition and transformation must be done beforehand.
71 | export
72 | covering
73 | runWidget : (JSErr -> IO ()) -> Widget -> IO ()
74 | runWidget onError w = runMVC update display onError Nothing w.init
75 |   where
76 |     update : Maybe w.Ev -> w.St -> w.St
77 |     update Nothing = id
78 |     update (Just ev) = w.update ev
79 |
80 |     display : Maybe w.Ev -> w.St -> Cmd (Maybe w.Ev)
81 |     display ev s = Just <$> maybe w.setup w.display ev s
82 |