0 | module Collie.Error
 1 |
 2 | import Data.List1
 3 | import Data.String
 4 | import System
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | data ErrorMsg : Type where
10 |   CouldNotParse    : String -> ErrorMsg
11 |   MissingOption    : String -> ErrorMsg
12 |   MissingArgument  : ErrorMsg
13 |   OptionSetTwice   : String -> ErrorMsg
14 |   TooManyArguments : ErrorMsg
15 |   MissingOptArg    : String -> ErrorMsg
16 |
17 | -- TODO: use an accumulating error monad instead
18 | public export
19 | data Error : Type -> Type where
20 |   Fail : List1 ErrorMsg -> Error a
21 |   Pure : a -> Error a
22 |
23 | export
24 | throwE : ErrorMsg -> Error a
25 | throwE err = Fail (err ::: [])
26 |
27 | export
28 | fromEither : Either ErrorMsg a -> Error a
29 | fromEither (Left err) = throwE err
30 | fromEither (Right a)  = Pure a
31 |
32 | export
33 | Functor Error where
34 |   map f (Fail err) = Fail err
35 |   map f (Pure a) = Pure (f a)
36 |
37 | export
38 | Applicative Error where
39 |   pure = Pure
40 |   Pure f   <*> Pure x   = Pure (f x)
41 |   Fail es1 <*> Fail es2 = Fail (es1 ++ es2)
42 |   Fail es1 <*> Pure x   = Fail es1
43 |   Pure f   <*> Fail es2 = Fail es2
44 |
45 | export
46 | (>>=) : Error a -> (a -> Error b) -> Error b
47 | Fail es >>= _ = Fail es
48 | Pure x  >>= f = f x
49 |
50 | export
51 | Show ErrorMsg where
52 |
53 |   show (CouldNotParse str) = "Could not parse argument: \{str}"
54 |   show (MissingOption str) = "Missing required modifier: \{str}"
55 |   show MissingArgument     = "Missing required argument"
56 |   show (OptionSetTwice nm) = "Option \{nm} set twice"
57 |   show TooManyArguments    = "Too many arguments, only one expected"
58 |   show (MissingOptArg nm)  = "Missing argument for option \{nm}"
59 |
60 |
61 | export
62 | Show a => Show (Error a) where
63 |   show (Pure a) = show a
64 |   show (Fail (err ::: [])) = "*** Error: " ++ show err
65 |   show (Fail errs) = unlines
66 |                    $ "*** Errors:"
67 |                    :: map (("  " ++) . show) (forget errs)
68 |
69 | export
70 | exitWith : List1 ErrorMsg -> IO a
71 | exitWith errs
72 |   = do putStr (show $ the (Error ()) $ Fail errs)
73 |        exitFailure
74 |