0 | module Evince.Core
  1 |
  2 | import Data.SnocList
  3 | import public Decidable.Equality
  4 | import public Evince.SrcLoc
  5 | import public Control.Monad.Trans
  6 | import public Control.Monad.Identity
  7 |
  8 | %default total
  9 |
 10 | public export
 11 | data FailureInfo : Type where
 12 |   ExpectedButGot  : (reason : String) -> (expected : String) -> (actual : String) -> FailureInfo
 13 |   PredicateFailed : (reason : String) -> (actual : String) -> FailureInfo
 14 |   Reason          : (message : String) -> FailureInfo
 15 |
 16 | export
 17 | Show FailureInfo where
 18 |   show (ExpectedButGot reason expected actual) =
 19 |     reason ++ "\nexpected: " ++ expected ++ "\n  actual: " ++ actual
 20 |   show (PredicateFailed reason actual) =
 21 |     reason ++ "\n  value: " ++ actual
 22 |   show (Reason message) = message
 23 |
 24 | export
 25 | DecEq FailureInfo where
 26 |   decEq (ExpectedButGot r1 e1 a1) (ExpectedButGot r2 e2 a2) =
 27 |     case (decEq r1 r2, decEq e1 e2, decEq a1 a2) of
 28 |       (Yes Refl, Yes Refl, Yes Refl) => Yes Refl
 29 |       (No c, _, _) => No $ \case Refl => c Refl
 30 |       (_, No c, _) => No $ \case Refl => c Refl
 31 |       (_, _, No c) => No $ \case Refl => c Refl
 32 |   decEq (PredicateFailed r1 a1) (PredicateFailed r2 a2) =
 33 |     case (decEq r1 r2, decEq a1 a2) of
 34 |       (Yes Refl, Yes Refl) => Yes Refl
 35 |       (No c, _) => No $ \case Refl => c Refl
 36 |       (_, No c) => No $ \case Refl => c Refl
 37 |   decEq (Reason m1) (Reason m2) = case decEq m1 m2 of
 38 |     Yes Refl => Yes Refl
 39 |     No c     => No $ \case Refl => c Refl
 40 |   decEq (ExpectedButGot _ _ _) (PredicateFailed _ _) = No $ \case Refl impossible
 41 |   decEq (ExpectedButGot _ _ _) (Reason _)            = No $ \case Refl impossible
 42 |   decEq (PredicateFailed _ _)  (ExpectedButGot _ _ _) = No $ \case Refl impossible
 43 |   decEq (PredicateFailed _ _)  (Reason _)            = No $ \case Refl impossible
 44 |   decEq (Reason _)             (ExpectedButGot _ _ _) = No $ \case Refl impossible
 45 |   decEq (Reason _)             (PredicateFailed _ _) = No $ \case Refl impossible
 46 |
 47 | -- Short-circuit on Fail/Skip: once a failure occurs, subsequent
 48 | -- expectations in a do-block are skipped.
 49 | public export
 50 | data TestResult : Type -> Type where
 51 |   Pass : a -> TestResult a
 52 |   Fail : FailureInfo -> TestResult a
 53 |   Skip : (reason : Maybe String) -> TestResult a
 54 |
 55 | export
 56 | Show a => Show (TestResult a) where
 57 |   show (Pass x)      = "Pass " ++ show x
 58 |   show (Fail info)   = "Fail (" ++ show info ++ ")"
 59 |   show (Skip reason) = "Skip " ++ show reason
 60 |
 61 | export
 62 | DecEq a => DecEq (TestResult a) where
 63 |   decEq (Pass x) (Pass y) = case decEq x y of
 64 |     Yes Refl => Yes Refl
 65 |     No c     => No $ \case Refl => c Refl
 66 |   decEq (Fail i1) (Fail i2) = case decEq i1 i2 of
 67 |     Yes Refl => Yes Refl
 68 |     No c     => No $ \case Refl => c Refl
 69 |   decEq (Skip r1) (Skip r2) = case decEq r1 r2 of
 70 |     Yes Refl => Yes Refl
 71 |     No c     => No $ \case Refl => c Refl
 72 |   decEq (Pass _) (Fail _)   = No $ \case Refl impossible
 73 |   decEq (Pass _) (Skip _)   = No $ \case Refl impossible
 74 |   decEq (Fail _) (Pass _)   = No $ \case Refl impossible
 75 |   decEq (Fail _) (Skip _)   = No $ \case Refl impossible
 76 |   decEq (Skip _) (Pass _)   = No $ \case Refl impossible
 77 |   decEq (Skip _) (Fail _)   = No $ \case Refl impossible
 78 |
 79 | export
 80 | Functor TestResult where
 81 |   map f (Pass x)      = Pass (f x)
 82 |   map f (Fail info)   = Fail info
 83 |   map f (Skip reason) = Skip reason
 84 |
 85 | export
 86 | Applicative TestResult where
 87 |   pure = Pass
 88 |   (Pass f)      <*> x = map f x
 89 |   (Fail info)   <*> _ = Fail info
 90 |   (Skip reason) <*> _ = Skip reason
 91 |
 92 | export
 93 | Monad TestResult where
 94 |   (Pass x)      >>= f = f x
 95 |   (Fail info)   >>= _ = Fail info
 96 |   (Skip reason) >>= _ = Skip reason
 97 |
 98 | ||| A chain of expectations in an inner monad `m`: `>>=` stops at the first
 99 | ||| `Fail` or `Skip`, so a test body of several expectations reports its
100 | ||| first failure. Plain `m` actions enter via `lift`/`liftIO`, a plain
101 | ||| `TestResult` via `liftResult`; `runTestResultT` runs the chain.
102 | public export
103 | data TestResultT : (Type -> Type) -> Type -> Type where
104 |   MkTestResultT : m (TestResult a) -> TestResultT m a
105 |
106 | ||| Run a chain in its inner monad, producing its final result.
107 | export
108 | runTestResultT : TestResultT m a -> m (TestResult a)
109 | runTestResultT (MkTestResultT x) = x
110 |
111 | export
112 | Functor m => Functor (TestResultT m) where
113 |   map f (MkTestResultT x) = MkTestResultT (map (map f) x)
114 |
115 | export
116 | Monad m => Applicative (TestResultT m) where
117 |   pure = MkTestResultT . pure . Pass
118 |   (MkTestResultT mf) <*> (MkTestResultT mx) = MkTestResultT $ do
119 |     Pass f <- mf
120 |       | Fail i => pure (Fail i)
121 |       | Skip r => pure (Skip r)
122 |     map (map f) mx
123 |
124 | export
125 | Monad m => Monad (TestResultT m) where
126 |   (MkTestResultT mx) >>= f = MkTestResultT $ do
127 |     Pass x <- mx
128 |       | Fail i => pure (Fail i)
129 |       | Skip r => pure (Skip r)
130 |     runTestResultT (f x)
131 |
132 | export
133 | MonadTrans TestResultT where
134 |   lift = MkTestResultT . map Pass
135 |
136 | export
137 | HasIO m => HasIO (TestResultT m) where
138 |   liftIO = lift . liftIO
139 |
140 | ||| Run a chain that performs no effects, e.g. to compare a custom
141 | ||| expectation's result against `Pass`, `Fail` or `Skip`.
142 | export
143 | runPure : TestResultT Identity a -> TestResult a
144 | runPure = runIdentity . runTestResultT
145 |
146 | ||| Lift a plain result into a chain, e.g. a custom expectation built from
147 | ||| `Pass` and `Fail`.
148 | export
149 | liftResult : Applicative m => TestResult a -> TestResultT m a
150 | liftResult = MkTestResultT . pure
151 |
152 | ||| Lift an `IO` chain into a chain over any monad that can run IO.
153 | export
154 | hoistIO : HasIO m => TestResultT IO a -> TestResultT m a
155 | hoistIO = MkTestResultT . liftIO . runTestResultT
156 |
157 | ||| Lifts a body written in monad `n` into a spec over monad `m`. A chain in
158 | ||| the spec's own monad runs as it is, an `IO` chain through `liftIO`, and a
159 | ||| body whose monad nothing else fixes runs in the spec's monad.
160 | public export
161 | interface Hoist (0 n : Type -> Type) (0 m : Type -> Type) where
162 |   hoistChain : TestResultT n a -> TestResultT m a
163 |
164 | public export
165 | HasIO m => Hoist IO m where
166 |   hoistChain = hoistIO
167 |
168 | ||| The fallback that runs a body in the spec's own monad.
169 | %defaulthint
170 | public export
171 | SameMonad : Hoist m m
172 | SameMonad = Same
173 |   where
174 |     [Same] Hoist m m where
175 |       hoistChain = id
176 |
177 | -- `m` is the test-action monad.
178 | public export
179 | data SpecTree : (m : Type -> Type) -> Type -> Type where
180 |   Describe    : (label : String) -> (children : List (SpecTree m a)) -> SpecTree m a
181 |   It          : (label : String) -> (loc : Maybe SrcLoc) -> (test : a -> m (TestResult ())) -> SpecTree m a
182 |   Pending     : (label : String) -> (reason : Maybe String) -> SpecTree m a
183 |   Focused     : SpecTree m a -> SpecTree m a
184 |   WithCleanup : (cleanup : m ()) -> (children : List (SpecTree m a)) -> SpecTree m a
185 |
186 | -- SnocList gives O(1) appending per describe/it in a do-block.
187 | public export
188 | data Spec : (m : Type -> Type) -> Type -> Type -> Type where
189 |   MkSpec : SnocList (SpecTree m a) -> b -> Spec m a b
190 |
191 | export
192 | Functor (Spec m a) where
193 |   map f (MkSpec trees x) = MkSpec trees (f x)
194 |
195 | export
196 | Applicative (Spec m a) where
197 |   pure x = MkSpec [<] x
198 |   (MkSpec ts1 f) <*> (MkSpec ts2 x) = MkSpec (ts1 ++ ts2) (f x)
199 |
200 | export
201 | Monad (Spec m a) where
202 |   (MkSpec ts1 x) >>= f = let (MkSpec ts2 y) = f x in MkSpec (ts1 ++ ts2) y
203 |
204 | ||| Extract the tree list from a completed spec.
205 | export
206 | getSpecTrees : Spec m a () -> List (SpecTree m a)
207 | getSpecTrees (MkSpec trees ()) = trees <>> []
208 |
209 | public export
210 | record Summary where
211 |   constructor MkSummary
212 |   passed   : Nat
213 |   failed   : Nat
214 |   pending  : Nat
215 |   duration : Integer
216 |
217 | export
218 | Semigroup Summary where
219 |   (MkSummary p1 f1 pn1 d1) <+> (MkSummary p2 f2 pn2 d2) =
220 |     MkSummary (p1 + p2) (f1 + f2) (pn1 + pn2) (d1 + d2)
221 |
222 | export
223 | Monoid Summary where
224 |   neutral = MkSummary 0 0 0 0
225 |
226 | export
227 | Show Summary where
228 |   show s = show s.passed ++ " passing, "
229 |         ++ show s.failed ++ " failing, "
230 |         ++ show s.pending ++ " pending"
231 |
232 | export
233 | totalCount : Summary -> Nat
234 | totalCount s = s.passed + s.failed + s.pending
235 |
236 | public export
237 | record RunConfig where
238 |   constructor MkRunConfig
239 |   failFast    : Bool
240 |   showTiming  : Bool
241 |   match       : Maybe String
242 |   skip        : Maybe String
243 |   randomize   : Bool
244 |   seed        : Maybe Nat
245 |   junitOutput : Maybe String
246 |   rerun       : Bool
247 |   jobs        : Nat
248 |   color       : Bool
249 |
250 | ||| Default configuration: no fail-fast, no timing, no filters, colored output.
251 | export
252 | defaultConfig : RunConfig
253 | defaultConfig = MkRunConfig False False Nothing Nothing False Nothing Nothing False 0 True
254 |