0 | module Web.MVC.Controller.List
  1 |
  2 | import Data.List1
  3 | import Monocle
  4 | import Text.HTML
  5 | import Text.HTML.Class
  6 | import Text.HTML.DomID
  7 | import Web.MVC.Controller
  8 |
  9 | %default total
 10 |
 11 | --------------------------------------------------------------------------------
 12 | -- Utilities
 13 | --------------------------------------------------------------------------------
 14 |
 15 | zipWithIndex : List t -> List (Nat,t)
 16 | zipWithIndex vs = fst (foldl (\(x,n),v => (x:<(n,v),S n)) ([<],Z) vs) <>> []
 17 |
 18 | del : Nat -> List (Nat,t) -> List (Nat,t)
 19 | del n = filter ((n /=) . fst)
 20 |
 21 | nextID : List (Nat,t) -> Nat
 22 | nextID []        = 0
 23 | nextID (x :: xs) = S $ foldl (\x => max x . fst) (fst x) xs
 24 |
 25 | --------------------------------------------------------------------------------
 26 | -- Types
 27 | --------------------------------------------------------------------------------
 28 |
 29 | ||| An event fired when editing a list of items
 30 | public export
 31 | data ListEv : Type -> Type where
 32 |   Add    : ListEv e
 33 |   Del    : (ix  : Nat) -> ListEv e
 34 |   Change : (ix : Nat) -> (ev : e) -> ListEv e
 35 |
 36 | ||| Type alias for editors of lists.
 37 | public export
 38 | 0 ListEditor : (i,s,e,t : Type) -> Type
 39 | ListEditor i s e t = Editor i (List (Nat,s)) (ListEv e) (List t)
 40 |
 41 | ||| Type alias for editors of lists.
 42 | public export
 43 | 0 List1Editor : (i,s,e,t : Type) -> Type
 44 | List1Editor i s e t = Editor i (List (Nat,s)) (ListEv e) (List1 t)
 45 |
 46 | ||| Whether to append or prepend items added to the list
 47 | public export
 48 | data ListMode = Append | Prepend
 49 |
 50 | insert : ListMode -> Nat -> s -> List (Nat,s) -> List (Nat,s)
 51 | insert Append  n v vs = vs ++ [(n,v)]
 52 | insert Prepend n v vs = (n,v) :: vs
 53 |
 54 | insertCmd : Cast i DomID => ListMode -> i -> Node e -> Cmd e
 55 | insertCmd Append  = elemAppend
 56 | insertCmd Prepend = elemPrepend
 57 |
 58 | ||| Environment for setting up the UI elements
 59 | public export
 60 | record ListEnv (i : Type) where
 61 |   [noHints]
 62 |   constructor LI
 63 |   ||| ID for a single row
 64 |   rowID   : i -> Nat -> i
 65 |
 66 |   ||| ID for the whole list base on a parent ID
 67 |   listID  : i -> i
 68 |
 69 |   ||| Class suffix
 70 |   cls     : Class
 71 |
 72 |   ||| Icon used for deleting a row
 73 |   delIcon : {0 e : _} -> e -> Node e
 74 |
 75 |   ||| Icon used for adding a row
 76 |   addIcon : {0 e : _} -> e -> Node e
 77 |
 78 |   ||| Whether to append or prepend new values
 79 |   mode    : ListMode
 80 |
 81 | --------------------------------------------------------------------------------
 82 | -- Editors
 83 | --------------------------------------------------------------------------------
 84 |
 85 | parameters {0 i,s,e,t : Type}
 86 |            {auto cst  : Cast i DomID}
 87 |            (li        : ListEnv i)
 88 |
 89 |   ||| Row for editing a single value in a list of values.
 90 |   export
 91 |   listRow : (i -> s -> Node e) -> i -> (Nat,s) -> Node (ListEv e)
 92 |   listRow f u (n,x) =
 93 |     let lid := li.rowID u n
 94 |      in div [cls (Row :< "list-edit") li.cls, ref lid]
 95 |           [Change n <$> f lid x, li.delIcon (Del n)]
 96 |
 97 |   ||| A widget used for editing lists of values, using another
 98 |   ||| widget for each individual value.
 99 |   export
100 |   values : (i -> s -> Node e) -> i -> List (Nat,s) -> Node (ListEv e)
101 |   values f u ps =
102 |     div [cls (Cell :< "list-edit") li.cls ]
103 |        [ div [cls (Row :< "list-add") li.cls] [li.addIcon Add]
104 |        , div [cls (Lst :< "list-edit") li.cls, ref $ li.listID u]
105 |            (listRow f u <$> ps)
106 |        ]
107 |
108 |   ||| An editor for lists of values, where values can be dynamically
109 |   ||| added or removed.
110 |   export
111 |   list : Editor i s e t -> ListEditor i s e t
112 |   list ed =
113 |     E adj
114 |       (values ed.view)
115 |       (\u => batch . map (\(n,v) => init u n v))
116 |       (traverse (ed.stToNew . snd))
117 |       (maybe [] (zipWithIndex . map (ed.toState . Just)))
118 |
119 |     where
120 |       row : i -> Nat -> s -> Node (ListEv e)
121 |       row u n v = listRow ed.view u (n,v)
122 |
123 |       ctrl : i -> Nat -> Prog e s (Cmd $ ListEv e)
124 |       ctrl u n v = Change n <$$> ed.ctrl (li.rowID u n) v
125 |
126 |       init : i -> Nat -> s -> Cmd (ListEv e)
127 |       init u n v = Change n <$> ed.init (li.rowID u n) v
128 |
129 |       adj : i -> Controller (ListEv e) (List (Nat,s))
130 |       adj u Add = do
131 |         n <- map nextID get
132 |         let s   := ed.toState Nothing
133 |         modify (insert li.mode n s)
134 |         pure $ insertCmd li.mode (li.listID u) (row u n s) <+> init u n s
135 |       adj u (Del n) = modify (del n) $> (removeElem $ li.rowID u n)
136 |       adj u (Change n v) = stO (eqFirst n fst .> snd) (ctrl u n v)
137 |
138 |   export
139 |   list1 : (empty : String) -> Editor i s e t -> List1Editor i s e t
140 |   list1 empty ed =
141 |     let led := list ed
142 |      in E led.ctrl led.view led.init toN (toS led)
143 |
144 |     where
145 |       toS : ListEditor i s e t -> Maybe (List1 t) -> List (Nat,s)
146 |       toS _   Nothing   = [(0,ed.toState Nothing)]
147 |       toS led (Just vs) = led.toState (Just $ forget vs)
148 |
149 |       toN : List (Nat,s) -> Either String (List1 t)
150 |       toN ps =
151 |         case traverse (ed.stToNew . snd) ps of
152 |           Left err => Left err
153 |           Right (h::t) => Right (h:::t)
154 |           Right []     => Left empty
155 |