0 | module Control.Eff.Writer
 1 |
 2 | import Control.Eff.Internal
 3 |
 4 | %default total
 5 |
 6 | public export
 7 | data WriterL : (lbl : k) -> (w : Type) -> (a : Type) -> Type where
 8 |   [search lbl]
 9 |   Tell : (vw : w) -> WriterL lbl w ()
10 |
11 | public export
12 | Writer : (w,a : Type) -> Type
13 | Writer = WriterL ()
14 |
15 | export
16 | tellAt : (0 lbl : k) -> Has (WriterL lbl w) fs => w -> Eff fs ()
17 | tellAt lbl vw = send $ Tell {lbl} vw
18 |
19 | export %inline
20 | tell : Has (Writer w) fs => w -> Eff fs ()
21 | tell = tellAt ()
22 |
23 | --------------------------------------------------------------------------------
24 | --          Running Writer
25 | --------------------------------------------------------------------------------
26 |
27 | export
28 | handleWriter :
29 |      {0 m : Type -> Type}
30 |   -> (tell : w -> m ())
31 |   -> WriterL lbl w a
32 |   -> m a
33 | handleWriter tell (Tell vw) = tell vw
34 |
35 | unWriter : u -> (u -> w -> u) -> WriterL lbl w a -> (a,u)
36 | unWriter vu f (Tell vw) = ((), f vu vw)
37 |
38 | export
39 | foldWriterAt :
40 |      (0 lbl : k)
41 |   -> {auto _ : Has (WriterL lbl w) fs}
42 |   -> u
43 |   -> (u -> w -> u)
44 |   -> Eff fs t
45 |   -> Eff (fs - WriterL lbl w) (t,u)
46 | foldWriterAt _ vu acc =
47 |   handleRelayS vu (\x,y => pure (y,x)) $ \vu2,w,f =>
48 |     let (vv,vu3) := unWriter vu2 acc w
49 |      in f vu3 vv
50 |
51 | export %inline
52 | foldWriter :
53 |      {auto _ : Has (Writer w) fs}
54 |   -> u
55 |   -> (u -> w -> u)
56 |   -> Eff fs t
57 |   -> Eff (fs - Writer w) (t,u)
58 | foldWriter = foldWriterAt ()
59 |
60 | export
61 | runWriterAt :
62 |      (0 lbl : k)
63 |   -> {auto _ : Has (WriterL lbl w) fs}
64 |   -> {auto _ : Monoid w}
65 |   -> Eff fs t
66 |   -> Eff (fs - WriterL lbl w) (t,w)
67 | runWriterAt lbl = foldWriterAt lbl neutral (<+>)
68 |
69 | export %inline
70 | runWriter :
71 |   Has (Writer w) fs => Monoid w => Eff fs t -> Eff (fs - Writer w) (t,w)
72 | runWriter = runWriterAt ()
73 |