0 | module Web.Async.Widget.Types
  1 |
  2 | import Derive.Prelude
  3 | import Monocle
  4 | import Text.HTML
  5 | import Web.Async.Util
  6 | import Web.Internal.Types
  7 |
  8 | %default total
  9 | %language ElabReflection
 10 | %hide Data.Linear.(.)
 11 | %hide Text.HTML.Node.a
 12 |
 13 | --------------------------------------------------------------------------------
 14 | -- EditRes
 15 | --------------------------------------------------------------------------------
 16 |
 17 | ||| Result of editing some kind of input element.
 18 | |||
 19 | ||| Input is either missing, invalid, or valid.
 20 | public export
 21 | data EditRes : Type -> Type where
 22 |   Missing : EditRes t
 23 |   Invalid : (err : String) -> EditRes t
 24 |   Valid   : (val : t) -> EditRes t
 25 |
 26 | %runElab derive "EditRes" [Show,Eq]
 27 |
 28 | export
 29 | toEither : EditRes t -> Either String ()
 30 | toEither (Invalid s) = Left s
 31 | toEither _           = Right ()
 32 |
 33 | export
 34 | toMaybe : EditRes t -> Maybe t
 35 | toMaybe (Valid v) = Just v
 36 | toMaybe _         = Nothing
 37 |
 38 | export
 39 | isValid : EditRes t -> Bool
 40 | isValid (Valid _) = True
 41 | isValid _         = False
 42 |
 43 | export
 44 | Functor EditRes where
 45 |   map f Missing     = Missing
 46 |   map f (Invalid v) = Invalid v
 47 |   map f (Valid v)   = Valid $ f v
 48 |
 49 | export
 50 | Applicative EditRes where
 51 |   pure = Valid
 52 |   Valid f   <*> v  = map f v
 53 |   Invalid x <*> _  = Invalid x
 54 |   Missing   <*> _  = Missing
 55 |
 56 | export
 57 | Monad EditRes where
 58 |   Missing   >>= _ = Missing
 59 |   Invalid x >>= _ = Invalid x
 60 |   Valid x   >>= f = f x
 61 |
 62 | validityTag : EditRes s -> String
 63 | validityTag Missing     = "missing"
 64 | validityTag (Invalid _) = "invalid"
 65 | validityTag (Valid _)   = "valid"
 66 |
 67 | export %inline
 68 | validity : EditRes s -> Attribute t
 69 | validity = Str "data-validity" . validityTag
 70 |
 71 | --------------------------------------------------------------------------------
 72 | -- Widgets
 73 | --------------------------------------------------------------------------------
 74 |
 75 | ||| A `Widget e` is an interactive UI element that emits
 76 | ||| events of type `e`.
 77 | public export
 78 | record Widget e where
 79 |   constructor W
 80 |   nodes  : HTMLNodes
 81 |   events : JSStream e
 82 |
 83 | export
 84 | adjNodes : (HTMLNodes -> HTMLNodes) -> Widget e -> Widget e
 85 | adjNodes f = {nodes $= f}
 86 |
 87 | ||| A dummy widget without a node representation that keeps
 88 | ||| producing the given value.
 89 | export
 90 | constant : t -> Widget t
 91 | constant = W [] . fill
 92 |
 93 | ||| A dummy widget without a node representation that
 94 | ||| never fires an event.
 95 | export
 96 | empty : Widget t
 97 | empty = W [] (pure ())
 98 |
 99 | ||| A dummy widget without a node representation that
100 | ||| fires the given event exactly once.
101 | export
102 | once : t -> Widget t
103 | once = W [] . emit
104 |
105 | export
106 | Functor Widget where
107 |   map f (W ns p) = W ns $ mapOutput f p
108 |
109 | --------------------------------------------------------------------------------
110 | -- File Input
111 | --------------------------------------------------------------------------------
112 |
113 | public export
114 | record FileEv where
115 |   constructor FE
116 |   file : File
117 |   name : String
118 |
119 | --------------------------------------------------------------------------------
120 | -- Editor
121 | --------------------------------------------------------------------------------
122 |
123 | parameters {auto ff : Functor f}
124 |            {auto fg : Functor g}
125 |
126 |   export %inline
127 |   map2 : (x -> y) -> f (g x) -> f (g y)
128 |   map2 = map . map
129 |
130 |   export %inline
131 |   map3 : Functor h => (x -> y) -> f (g (h x)) -> f (g (h y))
132 |   map3 = map . map . map
133 |
134 | ||| An `Editor` describes how to create new interactive DOM elements that
135 | ||| typically serve as a form of (validated) user input. It consists of an
136 | ||| `HTMLNode` for displaying the editing form plus a stream of validated
137 | ||| input data.
138 | |||
139 | ||| An editor and its corresponding widgets can be something simple like a
140 | ||| text input field or a `<select>` element, or it can be highly complex
141 | ||| like a canvas and a group of DOM elements for editing molecules.
142 | |||
143 | ||| A couple of notes about how an editor is supposed to behave:
144 | |||   * If the initial value used for creating the widget is a `Nothing`,
145 | |||     the stream of values produced by the widget *may* already hold
146 | |||     a valid default value. In case no sensible default is available,
147 | |||     the stream's initial value *should* be `Missing`.
148 | |||   * If the initial value used for creating the widget is a `Just`,
149 | |||     the stream of values produced by the widget *must* emit a `Valid`
150 | |||     wrapping the provided initial value as its first output.
151 | |||
152 | ||| The above two rules make sure an editor behaves as expected, especially
153 | ||| when combining several editors in a form, or using the experimental
154 | ||| `bindEd` combinator.
155 | public export
156 | record Editor (t : Type) where
157 |   constructor E
158 |   ||| Create a node and stream of values from an optional initial value.
159 |   widget : Maybe t -> Act (Widget $ EditRes t)
160 |
161 | export
162 | adjWidget :
163 |      (Maybe a -> Maybe b)
164 |   -> (Widget (EditRes b) -> Widget (EditRes a))
165 |   -> Editor b
166 |   -> Editor a
167 | adjWidget adjm adjw ed = E $ map adjw . ed.widget . adjm
168 |
169 | export %inline
170 | edNodes : (HTMLNodes -> HTMLNodes) -> Editor t -> Editor t
171 | edNodes = adjWidget id . adjNodes
172 |
173 | export %inline
174 | adjEditor :
175 |      (Maybe a -> Maybe b)
176 |   -> (EditRes b -> EditRes a)
177 |   -> Editor b
178 |   -> Editor a
179 | adjEditor adjm adjres =
180 |   adjWidget adjm $ {events $= P.mapOutput adjres}
181 |
182 | ||| Views an editor through an isomorphism.
183 | export
184 | editI : Iso' t1 t2 -> Editor t1 -> Editor t2
185 | editI i (E f) = E $ map3 i.get_ . f . map i.reverseGet
186 |
187 | ||| Views the `new` values of an editor through a prism.
188 | export
189 | editP : Prism' t2 t1 -> Editor t1 -> Editor t2
190 | editP p (E f) = E $ map3 p.reverseGet . f . (>>= first p)
191 |
192 | ||| Refines an editor to produce values of a more restricted type.
193 | export
194 | refineEdit :
195 |      (t2 -> Maybe t1)
196 |   -> (refine : t1 -> EditRes t2)
197 |   -> Editor t1
198 |   -> Editor t2
199 | refineEdit ini f (E w) = E $ \m => map (>>= f) <$> w (m >>= ini)
200 |
201 | export %inline
202 | mapEvents : (JSStream (EditRes t) -> JSStream (EditRes t)) -> Editor t -> Editor t
203 | mapEvents f (E w) = E $ map {events $= f} . w
204 |
205 | ||| A dummy `Editor` for uneditable values.
206 | |||
207 | ||| The given value is fired exactly once.
208 | public export
209 | dummy : t -> Editor t
210 | dummy v = E $ \_ => pure (once (Valid v))
211 |