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