0 | module Test.DepTyCheck.Gen.Labels
 1 |
 2 | import Control.Monad.State.Interface
 3 | import public Control.Monad.Trans
 4 |
 5 | import Data.String
 6 |
 7 | %default total
 8 |
 9 | -----------------
10 | --- Labelling ---
11 | -----------------
12 |
13 | export
14 | data Label : Type where
15 |   StringLabel : String -> Label
16 |
17 | export %inline
18 | FromString Label where
19 |   fromString = StringLabel
20 |
21 | export %inline
22 | Show Label where
23 |   show (StringLabel x) = x
24 |
25 | export
26 | Eq Label where
27 |   StringLabel x == StringLabel y = x == y
28 |
29 | export
30 | Ord Label where
31 |   compare = comparing $ \(StringLabel x) => x
32 |
33 | --- Labels management interface ---
34 |
35 | public export
36 | interface Monad m => CanManageLabels (0 m : Type -> Type) where
37 |   manageLabel : Label -> m ()
38 |
39 | public export
40 | CanManageLabels m => MonadTrans t => Monad (t m) => CanManageLabels (t m) where
41 |   manageLabel = lift . manageLabel
42 |
43 | export %defaulthint
44 | IgnoreLabels : Monad m => CanManageLabels m
45 | IgnoreLabels = I where
46 |   [I] CanManageLabels m where
47 |     manageLabel _ = pure ()
48 |
49 | export
50 | [PrintAllLabels] HasIO io => CanManageLabels io where
51 |   manageLabel = putStrLn . show
52 |