0 | module Web.Async.Form
  1 |
  2 | import Data.List.Quantifiers.Extra
  3 | import Data.SnocList
  4 | import public Control.Barbie
  5 | import public Data.Singleton
  6 | import public Monocle
  7 | import public Web.Async
  8 | import public Web.Async.Widget
  9 | import Text.HTML.DomID
 10 |
 11 | %default total
 12 |
 13 | ||| An editable field in a web form consisting of the field's
 14 | ||| name, the node for data input, and an ID that will be used
 15 | ||| to send validation messages to a label.
 16 | public export
 17 | record FormField where
 18 |   constructor FF
 19 |   name  : String
 20 |   nodes : HTMLNodes
 21 |
 22 | toField : (String,Widget t) -> Maybe FormField
 23 | toField (nm, W [] _) = Nothing
 24 | toField (nm, W ns _) = Just (FF nm ns)
 25 |
 26 | formStream : List (Widget (t -> t)) -> t -> JSStream t
 27 | formStream ws ini = merge (map events ws) |> scanFrom1 ini
 28 |
 29 | parameters {auto loc   : DOMLocal}
 30 |            {0 f        : Type}
 31 |            {auto ipf   : Interpolation f}
 32 |            (0 rec      : (f -> Type) -> Type)
 33 |            (formNode   : FormField -> HTMLNode)
 34 |            {0 g        : f -> Type}
 35 |            {auto sings : rec Singleton}
 36 |            {auto fuc   : FunctorB f rec}
 37 |            {auto app   : ApplicativeB f rec}
 38 |            {auto trv   : TraversableB f rec}
 39 |            {auto rrd   : RecordB f rec}
 40 |
 41 |   -- type of a single form widget: the field's name, the widget itself,
 42 |   -- which emits functions used for updating the barbie record,
 43 |   -- and a label ID used for writing error messages.
 44 |   0 WForm : Type
 45 |   WForm = (String,Widget (rec (EditRes . g) -> rec (EditRes . g)))
 46 |
 47 |   -- Creates the information for editing a single
 48 |   -- field of the record.
 49 |   --
 50 |   -- The properly typed `Singleton` is required to create the
 51 |   -- lens for reading and updating the record field (see interface `RecordB`)
 52 |   editField :
 53 |        {0 v : f}
 54 |     -> Singleton v
 55 |     -> Editor (g v)
 56 |     -> Maybe (rec g)
 57 |     -> Act WForm
 58 |   editField (Val v) (E fun) mrec = do
 59 |     -- create the HTML node and input stream
 60 |     W n s <- fun $ map (field g v).get_ mrec
 61 |
 62 |     -- adjust the input stream so that all input is used to update
 63 |     -- the corresponding field of the barbie
 64 |     let s2 := P.observe (logFormField v) s |> P.mapOutput (set (field' v))
 65 |
 66 |     pure $ (interpolate v, W n s2)
 67 |
 68 |   ||| An editable web form where the different fields of a
 69 |   ||| record can be edited and validated.
 70 |   |||
 71 |   ||| The record in question must be a *barbie*
 72 |   ||| (see the corresponding library), and this function takes as
 73 |   ||| input such a record of editors and returns an editor of
 74 |   ||| the record.
 75 |   |||
 76 |   ||| @ `rec`      : the barbie record type used to group the
 77 |   |||                field values.
 78 |   ||| @ `formNode` : used to group and display the different
 79 |   |||                form fields in a single HTML node.
 80 |   |||
 81 |   ||| Note: For uneditable record fields that should not appear in the
 82 |   |||       user interface, use a `dummy` editor.
 83 |   export
 84 |   form : rec (Editor . g) -> Editor (rec g)
 85 |   form edits =
 86 |        -- convert all value editors to record updaters
 87 |    let eflds   := bzipWith editField sings edits
 88 |
 89 |        -- initial value of the stream: all fields are missing
 90 |        -- (this will automatically be updated with the initial event of every
 91 |        -- input stream when `merge`ing them, so that non-mandatory field values
 92 |        -- will no longer be missing)
 93 |        missAll := the (rec (EditRes . g)) (bpure @{app} Missing)
 94 |     in E $ \recm => do
 95 |          -- sets up (in `io`) all editor widgets by applying
 96 |          -- them to the optional initial record `recm`
 97 |          recw   <- btraverse (flip apply recm) eflds
 98 |
 99 |          -- extract the editor triples as a list for
100 |          let ws   := bfoldMap (Prelude.Lin:<) recw <>> []
101 |
102 |          -- group the editing fields in a single HTML node
103 |              ns   := formNode <$> mapMaybe toField ws
104 |
105 |          pure $ W ns $
106 |               formStream (map snd ws) missAll
107 |            |> mapOutput bsequence
108 |            |> P.observe logFormRes
109 |
110 | parameters {auto loc   : DOMLocal}
111 |            {0 ts       : List Type}
112 |            {auto els   : All (`Elem` ts) ts}
113 |
114 |   0 HForm : Type
115 |   HForm = (Widget (All EditRes ts -> All EditRes ts))
116 |
117 |   hfield : Elem t ts -> Editor t -> Maybe (HList ts) -> Act HForm
118 |   hfield e (E fun) mrec = Prelude.do
119 |     W n s <- fun $ Lens.get_ (prod t) <$> mrec
120 |     pure $ W n
121 |       $ observe (logFormFieldN $ elemToNat e) s |> P.mapOutput (set $ prod t)
122 |
123 |   ||| An editable web form where the different fields of a
124 |   ||| record can be edited and validated.
125 |   |||
126 |   ||| The record in question must be a *barbie*
127 |   ||| (see the corresponding library), and this function takes as
128 |   ||| input such a record of editors and returns an editor of
129 |   ||| the record.
130 |   |||
131 |   ||| @ `rec`      : the barbie record type used to group the
132 |   |||                field values.
133 |   |||
134 |   ||| Note: For uneditable record fields that should not appear in the
135 |   |||       user interface, use a `dummy` editor.
136 |   export
137 |   hform : All Editor ts -> Editor (HList ts)
138 |   hform edits =
139 |    let eflds   := hzipWith hfield els edits
140 |        miss    := mapProperty {q = EditRes} (\_ => Missing) edits
141 |     in E $ \recm => do
142 |          -- sets up (in `io`) all editor widgets by applying
143 |          -- them to the optional initial record `recm`
144 |          recw   <- hsequence $ mapProperty (flip apply recm) eflds
145 |
146 |          let ws   := hfoldMap (Prelude.Lin:<) recw <>> []
147 |
148 |          -- group the editing fields in a single HTML node
149 |              ns   := ws >>= nodes
150 |
151 |          pure $ W ns $
152 |            formStream ws miss |> mapOutput hsequence |> P.observe logFormRes
153 |