0 | module Web.Async.List
  1 |
  2 | import Data.Linear.Traverse1
  3 | import Data.Linear.Unique
  4 | import Data.List1
  5 | import Derive.Prelude
  6 | import Text.HTML.DomID
  7 | import Web.Async.Form
  8 |
  9 | %default total
 10 | %language ElabReflection
 11 |
 12 | --------------------------------------------------------------------------------
 13 | -- List Event
 14 | --------------------------------------------------------------------------------
 15 |
 16 | public export
 17 | data ListEv = Prepend | Append
 18 |
 19 | %runElab derive "ListEv" [Show,Eq,Ord]
 20 |
 21 | --------------------------------------------------------------------------------
 22 | -- List Updates
 23 | --------------------------------------------------------------------------------
 24 |
 25 | 0 ST : Type -> Type
 26 | ST t = List (Token World, EditRes t)
 27 |
 28 | missing : ST t -> EditRes (List t)
 29 | missing []        = Missing
 30 | missing (x :: xs) =
 31 |   case snd x of
 32 |     Invalid err => Invalid err
 33 |     _           => missing xs
 34 |
 35 | travres : SnocList t -> ST t -> EditRes (List t)
 36 | travres sx []        = Valid $ sx <>> []
 37 | travres sx (x :: xs) =
 38 |   case snd x of
 39 |     Missing     => missing xs
 40 |     Invalid err => Invalid err
 41 |     Valid val   => travres (sx :< val) xs
 42 |
 43 | del : Token World -> ST t -> ST t
 44 | del n = filter ((n /=) . fst)
 45 |
 46 | upd : Token World -> EditRes t -> ST t -> ST t
 47 | upd tok res = map (\p => if fst p == tok then (tok,res) else p)
 48 |
 49 | new : Token World -> ListEv -> ST t -> ST t
 50 | new tok Prepend xs = (tok,Missing)::xs
 51 | new tok Append  xs = xs ++ [(tok,Missing)]
 52 |
 53 | --------------------------------------------------------------------------------
 54 | -- List Editor
 55 | --------------------------------------------------------------------------------
 56 |
 57 | delete : Token World -> JSStream () -> Ref Void -> JSStream (ST t -> ST t)
 58 | delete t us r = P.take 1 us |> P.evalMap (\_ => remove r $> del t)
 59 |
 60 | initial : Maybe (List t) -> IO1 (List (Token World, t))
 61 | initial Nothing   = ([] #)
 62 | initial (Just ts) =
 63 |   traverse1 (\v,t => let tok # t := token1 t in (tok,v) # t) ts
 64 |
 65 | parameters {default 0xffff_fffe limit : Nat}
 66 |            (parent : Act (Ref Void, HTMLNodes -> Widget ListEv))
 67 |            (row    : HTMLNode -> Act (Ref Void, Widget ()))
 68 |            (ed     : Editor t)
 69 |
 70 |   rw : Token World -> Maybe t -> Act (Widget $ ST t -> ST t)
 71 |   rw tok ini = do
 72 |     W n s           <- ed.widget ini
 73 |     (rid, W n2 del) <- row n
 74 |     pure $ W n2 $ mergeHaltL (delete tok del rid) (P.mapOutput (upd tok) s)
 75 |
 76 |   add : Ref Void -> ListEv -> Act (JSStream (ST t -> ST t))
 77 |   add rpar le = do
 78 |     tok   <- token
 79 |     W n s <- rw tok Nothing
 80 |     if le == Append then append rpar n else prepend rpar n
 81 |     pure $ emit (new tok le) <+> s
 82 |
 83 |   ||| An editor for lists of values.
 84 |   |||
 85 |   ||| This uses `row` to wrap a node for editing a single value
 86 |   ||| in a node with some kind of *delete* or *remove* function.
 87 |   |||
 88 |   ||| All rows are displayed in the `parent` node.
 89 |   export
 90 |   editList : Editor (List t)
 91 |   editList =
 92 |     E $ \m => do
 93 |       (ref, makeW) <- parent
 94 |       ini          <- lift1 $ initial m
 95 |       rows         <- traverseList (\(t,v) => rw t (Just v)) ini
 96 |       let W n listEvs := makeW (map node rows)
 97 |       pure $ W n $
 98 |         (emits (map events rows) <+> evalMap (add ref) listEvs)
 99 |         |> parJoin (S limit)
100 |         |> scanFrom1 (map2 Valid ini)
101 |         |> P.mapOutput (travres [<])
102 |
103 | ||| Like `editList` but for non-empty lists.
104 | export
105 | editList1 : Editor (List t) -> Editor (List1 t)
106 | editList1 =
107 |   refineEdit (Just . forget) $ \case
108 |     x::xs => Valid $ x:::xs
109 |     []    => Missing
110 |