0 | module Web.MVC.Controller
  1 |
  2 | import Data.Either
  3 | import Data.List.Quantifiers.Extra
  4 | import Monocle
  5 | import Text.HTML.DomID
  6 | import Web.MVC
  7 | import public Control.Monad.State
  8 | import public Web.MVC.Cmd
  9 |
 10 | %default total
 11 |
 12 | --------------------------------------------------------------------------------
 13 | --          Prog and Controller
 14 | --------------------------------------------------------------------------------
 15 |
 16 | export infixr 4 <$$>
 17 |
 18 | ||| A `Prog` controls some state of type `s` acting on events of
 19 | ||| type `e`.
 20 | |||
 21 | ||| Based on an event and the current state, the controller produces a new
 22 | ||| state and a result (typically a command), which usually updates the
 23 | ||| UI in such a way that it can fire more events.
 24 | public export
 25 | 0 Prog : (e,s,t : Type) -> Type
 26 | Prog e s t = e -> State s t
 27 |
 28 | public export
 29 | 0 Controller : (e,s : Type) -> Type
 30 | Controller e s = Prog e s (Cmd e)
 31 |
 32 | export %inline
 33 | (<$$>) : (x -> y) -> State s (Cmd x) -> State s (Cmd y)
 34 | (<$$>) = map . map
 35 |
 36 | export %inline
 37 | map2 : (x -> y) -> State s (Cmd x) -> State s (Cmd y)
 38 | map2 = map . map
 39 |
 40 | export %inline
 41 | Semigroup (State s $ Cmd e) where x <+> y = [| x <+> y |]
 42 |
 43 | export %inline
 44 | Monoid (State s $ Cmd e) where neutral = pure neutral
 45 |
 46 | ||| On an event, replaces the current state with the event's
 47 | ||| value without emitting a command.
 48 | export %inline
 49 | direct : Monoid t => Prog e e t
 50 | direct v = put v $> neutral
 51 |
 52 | ||| Same as `direct` but for optional states.
 53 | export %inline
 54 | directM : Monoid t => Prog e (Maybe e) t
 55 | directM v = put (Just v) $> neutral
 56 |
 57 | ||| A controller that replaces the state with the current event
 58 | ||| and display the new state.
 59 | export %inline
 60 | displayEv : (s -> Cmd t) -> Prog s s (Cmd t)
 61 | displayEv disp v = put v $> disp v
 62 |
 63 | ||| Update the state with the given function, the run a command
 64 | ||| derived from the new state.
 65 | export %inline
 66 | updateDisp : (e -> s -> s) -> (e -> s -> Cmd t) -> Prog e s (Cmd t)
 67 | updateDisp f g ev = modify (f ev) >> map (g ev) get
 68 |
 69 | public export
 70 | data Progs : (evs : List Type) -> (sts : List Type) -> Type where
 71 |   Nil  : Progs Nil Nil
 72 |   (::) : Prog e s (Cmd e) -> Progs es ss -> Progs (e::es) (s::ss)
 73 |
 74 | ||| A list of controllers can be converted to a controller over
 75 | ||| a heterogeneous sum as the event type and a heterogeneous list
 76 | ||| as the state type.
 77 | export
 78 | progs : Progs es ss -> Controller (HSum es) (HList ss)
 79 | progs []      ev = absurd ev
 80 | progs (c::cs) (Here x)  = Here  <$$> stL allHead (c x)
 81 | progs (c::cs) (There x) = There <$$> stL allTail (progs cs x)
 82 |
 83 | export covering %inline
 84 | run : Prog e s (Cmd e) -> (initEv : e) -> (initST : s) -> IO ()
 85 | run f = runController (\ev,st => runState st (f ev)) (putStrLn . dispErr)
 86 |
 87 | --------------------------------------------------------------------------------
 88 | --          Editor
 89 | --------------------------------------------------------------------------------
 90 |
 91 | ||| An `Editor` describes how to "pop-up" new interactive DOM elements that
 92 | ||| typically serve as a form of (validated) user input. It consists of a
 93 | ||| `Controller` for the interactive element(s), but also describes an initial
 94 | ||| view to display and command to emit, based on the current state.
 95 | |||
 96 | ||| An editor and its corresponding widgets can be something simple like a
 97 | ||| text input field or a `<select>` element, or it can be highly complex
 98 | ||| like a canvas and a group of DOM elements for editing molecules.
 99 | |||
100 | ||| Since an `Editor` describes a set of DOM elements that can potentially
101 | ||| appear several times in a web page (for instance, when editing a list of
102 | ||| values), its functions take a `DomID` as additional input, to distinguish
103 | ||| between the different versions of the widget that are around.
104 | |||
105 | ||| @i   : The ID type used to identify DOM elements
106 | |||
107 | ||| @st  : The type used to internally store the current widget state
108 | |||
109 | ||| @ev  : The event type the widget fires.
110 | |||
111 | ||| @new : The type of data we can extract from the widget's internal state.
112 | public export
113 | record Editor (i,st,ev,new : Type) where
114 |   constructor E
115 |   ||| Update the inner state based on the current event.
116 |   ctrl  : i -> Controller ev st
117 |
118 |   ||| Create a widget from a unique identifier and the initial state.
119 |   view  : i -> st -> Node ev
120 |
121 |   ||| The initial command use to properly setup the view. This is used
122 |   ||| for initial validation or for drawing molecules to the canvas when
123 |   ||| editing starts. It is invoked after setting up the view.
124 |   init  : i -> st -> Cmd ev
125 |
126 |   ||| Try to convert the current state to a value of type `new` we can
127 |   ||| send to the server. This implements client-side validation, therefore,
128 |   ||| it returns an `Either`.
129 |   stToNew : st -> Either String new
130 |
131 |   ||| Create an initial state from an optional value of type `new`
132 |   toState : Maybe new -> st
133 |
134 | ||| View an editor through an isomorphism.
135 | export
136 | newIso : Iso' n1 n2 -> Editor i st ev n1 -> Editor i st ev n2
137 | newIso i = {stToNew $= (map i.get_ .), toState $= (. map i.reverseGet)}
138 |
139 | ||| Utility for editors without initial command.
140 | export %inline
141 | noInit : i -> s -> Cmd e
142 | noInit _ _ = neutral
143 |
144 | ||| Tries to convert the current (optional) state of an editor to
145 | ||| an updated value.
146 | export
147 | toNewM : Editor i st ev new -> Maybe st -> Maybe new
148 | toNewM ed = (>>= eitherToMaybe . ed.stToNew)
149 |
150 | ||| Views the `new` values of an editor through a prism.
151 | export
152 | newP : Prism' t s -> Editor i st ev s -> Editor i st ev t
153 | newP p ed =
154 |   { stToNew := map p.reverseGet . ed.stToNew
155 |   , toState := \x => ed.toState $ x >>= first p
156 |   } ed
157 |
158 | ||| A dummy `Editor` for uneditable values.
159 | public export
160 | dummy : n -> Editor i () Void n
161 | dummy v =
162 |   E (\_,_ => neutral) (\_,_ => Empty) (\_,_ => neutral) (\_ => Right v) (\_ => ())
163 |
164 | --------------------------------------------------------------------------------
165 | --          Utilities
166 | --------------------------------------------------------------------------------
167 |
168 | export %inline
169 | elemChildren : Cast t DomID => t -> List (Node e) -> Cmd e
170 | elemChildren = children . elemRef
171 |
172 | export %inline
173 | elemChild : Cast t DomID => t -> Node e -> Cmd e
174 | elemChild = child . elemRef
175 |
176 | export %inline
177 | elemAppend : Cast t DomID => t -> Node e -> Cmd e
178 | elemAppend = append . elemRef
179 |
180 | export %inline
181 | elemPrepend : Cast t DomID => t -> Node e -> Cmd e
182 | elemPrepend = prepend . elemRef
183 |
184 | export %inline
185 | clearElem : Cast t DomID => t -> Cmd e
186 | clearElem v = elemChildren v []
187 |
188 | export %inline
189 | removeElem : Cast t DomID => t -> Cmd e
190 | removeElem = remove . elemRef
191 |
192 | export %inline
193 | replaceElem : Cast t DomID => t -> Node e -> Cmd e
194 | replaceElem = replace . elemRef
195 |
196 | export %inline
197 | btnAttr : Cast t DomID => t -> Attribute Tag.Button e -> Cmd e
198 | btnAttr v = attr (btnRef v)
199 |