0 | module Web.MVC.Controller.Form
 1 |
 2 | import Data.List.Quantifiers.Extra
 3 | import Text.HTML
 4 | import Web.MVC.Controller
 5 |
 6 | ||| A heterogeneous list of editors.
 7 | |||
 8 | ||| These can be used to create UI forms from single - but
 9 | ||| arbitrarily complex - widgets.
10 | public export
11 | data Editors : (i : Type) -> (sts,evs,news : List Type) -> Type where
12 |   Nil  : Editors i [] [] []
13 |   (::) :
14 |        Editor i s e n
15 |     -> Editors i ss es ns
16 |     -> Editors i (s::ss) (e::es) (n::ns)
17 |
18 | ||| Converts a list of editors to a list of controllers.
19 | public export
20 | toProgs : Editors i ss es ns -> i -> Progs es ss
21 | toProgs []      vi = []
22 | toProgs (x::xs) vi = x.ctrl vi :: toProgs xs vi
23 |
24 | ||| Initial commands from a list of editors and a heterogeneous list of
25 | ||| initial states.
26 | export
27 | toInit : Editors i ss es ns -> i -> HList ss -> Cmd (HSum es)
28 | toInit []      vi []      = neutral
29 | toInit (x::xs) vi (y::ys) =
30 |   map Here (x.init vi y) <+> map There (toInit xs vi ys)
31 |
32 | toNew : Editors i ss es ns -> HList ss -> Either String (HList ns)
33 | toNew []      []      = Right []
34 | toNew (x::xs) (y::ys) = [| stToNew x y :: toNew xs ys |]
35 |
36 | toStNothing : Editors i ss es ns -> HList ss
37 | toStNothing []      = []
38 | toStNothing (x::xs) = x.toState Nothing :: toStNothing xs
39 |
40 | toSt : Editors i ss es ns -> HList ns -> HList ss
41 | toSt []      []      = []
42 | toSt (x::xs) (y::ys) = x.toState (Just y) :: toSt xs ys
43 |
44 | views : Editors i ss es ns -> i -> HList ss -> List (Node $ HSum es)
45 | views []      vi []      = []
46 | views (x::xs) vi (y::ys) =
47 |   Prelude.map Here (view x vi y) :: map (Prelude.map There) (views xs vi ys)
48 |
49 | ||| Converts a heterogeneous list of editors into a single editor,
50 | ||| similar in concept to a form of widgets.
51 | export
52 | form :
53 |      (List (Node $ HSum es) -> Node (HSum es))
54 |   -> Editors i ss es ns
55 |   -> Editor i (HList ss) (HSum es) (HList ns)
56 | form wrapNodes eds =
57 |   E { ctrl    = progs . toProgs eds
58 |     , view    = \vi => wrapNodes . views eds vi
59 |     , init    = toInit eds
60 |     , stToNew = toNew eds
61 |     , toState = maybe (toStNothing eds) (toSt eds)
62 |     }
63 |