0 | module Hedgehog.Internal.Terminal
 1 |
 2 | import Control.Monad.Writer.Interface
 3 |
 4 | import Text.ANSI.CSI
 5 | import Data.IORef
 6 | import Data.String
 7 | import System.File
 8 |
 9 | ||| Interface showing that in the given monadic context `m` user can
10 | ||| initialise terminal and use it for printing temporary and permanent info.
11 | public export
12 | interface HasTerminal m where
13 |
14 |   ||| Type of initialised terminal
15 |   0 TermTy : Type
16 |
17 |   ||| Return new initialised terminal
18 |   |||
19 |   ||| Notice that usage of several initalised terminals is not supposed
20 |   ||| and may lead to unexpected behaviour.
21 |   console  : m TermTy
22 |
23 |   ||| Put temporary info into the terminal
24 |   |||
25 |   ||| Any successive putting temporary or permanent info into the terminal
26 |   ||| makes any previously put temporary info disappear.
27 |   putTmp   : TermTy -> String -> m ()
28 |
29 |   ||| Put permanent info into the terminal
30 |   |||
31 |   ||| This action makes previously put temporary info disappear
32 |   putOut   : TermTy -> String -> m ()
33 |
34 | ||| Returns the type of initialised terminal
35 | ||| for the explicitly given context `m`
36 | public export
37 | 0 Terminal : (0 m : _) -> HasTerminal m => Type
38 | Terminal m = TermTy {m}
39 |
40 | putStrErr : HasIO io => String -> io ()
41 | putStrErr s = fPutStr stderr s $> ()
42 |
43 | replicate : Monoid m => Nat -> m -> m
44 | replicate Z     x = neutral
45 | replicate (S n) x = x <+> replicate n x
46 |
47 | clearIOTmp : IORef Nat -> IO ()
48 | clearIOTmp tmp = do
49 |   linesCnt <- readIORef tmp
50 |   putStrErr $ Terminal.replicate linesCnt $ cursorUp1 <+> eraseLine End
51 |   writeIORef tmp 0
52 |
53 | ||| Uses system stdout for permanent printing and stderr for temporary printing
54 | export
55 | HasIO io => HasTerminal io where
56 |   TermTy  = IORef Nat
57 |   console = liftIO $ newIORef 0
58 |   putTmp t str = liftIO $ do
59 |     clearIOTmp t
60 |     writeIORef t $ length $ lines str
61 |     putStrErr str
62 |   putOut t str = liftIO $ clearIOTmp t *> putStr str
63 |
64 | ||| Uses monadic writer to remember everything
65 | ||| written permanently to the terminal
66 | |||
67 | ||| This implementation does not use any type of actual printing to any
68 | ||| real terminal, this is completely pure.
69 | export
70 | [StdoutOnly] MonadWriter (List String) m => HasTerminal m where
71 |   TermTy       = Unit
72 |   console      = pure ()
73 |   putTmp _ _   = pure ()
74 |   putOut _ str = tell [str]
75 |
76 | public export
77 | data StdoutOrTmp = Stdout | Tmp
78 |
79 | ||| Uses monadic writer to remember everything
80 | ||| written temporarily and permanently to the terminal
81 | |||
82 | ||| The order of writes is completely preserved.
83 | ||| Type of the write is determined by the `StdoutOrTmp` discriminator.
84 | |||
85 | ||| This implementation does not use any type of actual printing to any
86 | ||| real terminal, this is completely pure.
87 | export
88 | [StdoutAndTmp] MonadWriter (List (StdoutOrTmp, String)) m => HasTerminal m where
89 |   TermTy       = Unit
90 |   console      = pure ()
91 |   putTmp _ str = tell [(Tmp, str)]
92 |   putOut _ str = tell [(Stdout, str)]
93 |