0 | module Evince.Core
  1 |
  2 | import Data.SnocList
  3 | import public Decidable.Equality
  4 | import public Evince.SrcLoc
  5 |
  6 | %default total
  7 |
  8 | public export
  9 | data FailureInfo : Type where
 10 |   ExpectedButGot  : (reason : String) -> (expected : String) -> (actual : String) -> FailureInfo
 11 |   PredicateFailed : (reason : String) -> (actual : String) -> FailureInfo
 12 |   Reason          : (message : String) -> FailureInfo
 13 |
 14 | export
 15 | Show FailureInfo where
 16 |   show (ExpectedButGot reason expected actual) =
 17 |     reason ++ "\nexpected: " ++ expected ++ "\n  actual: " ++ actual
 18 |   show (PredicateFailed reason actual) =
 19 |     reason ++ "\n  value: " ++ actual
 20 |   show (Reason message) = message
 21 |
 22 | export
 23 | DecEq FailureInfo where
 24 |   decEq (ExpectedButGot r1 e1 a1) (ExpectedButGot r2 e2 a2) =
 25 |     case (decEq r1 r2, decEq e1 e2, decEq a1 a2) of
 26 |       (Yes Refl, Yes Refl, Yes Refl) => Yes Refl
 27 |       (No c, _, _) => No $ \case Refl => c Refl
 28 |       (_, No c, _) => No $ \case Refl => c Refl
 29 |       (_, _, No c) => No $ \case Refl => c Refl
 30 |   decEq (PredicateFailed r1 a1) (PredicateFailed r2 a2) =
 31 |     case (decEq r1 r2, decEq a1 a2) of
 32 |       (Yes Refl, Yes Refl) => Yes Refl
 33 |       (No c, _) => No $ \case Refl => c Refl
 34 |       (_, No c) => No $ \case Refl => c Refl
 35 |   decEq (Reason m1) (Reason m2) = case decEq m1 m2 of
 36 |     Yes Refl => Yes Refl
 37 |     No c     => No $ \case Refl => c Refl
 38 |   decEq (ExpectedButGot _ _ _) (PredicateFailed _ _) = No $ \case Refl impossible
 39 |   decEq (ExpectedButGot _ _ _) (Reason _)            = No $ \case Refl impossible
 40 |   decEq (PredicateFailed _ _)  (ExpectedButGot _ _ _) = No $ \case Refl impossible
 41 |   decEq (PredicateFailed _ _)  (Reason _)            = No $ \case Refl impossible
 42 |   decEq (Reason _)             (ExpectedButGot _ _ _) = No $ \case Refl impossible
 43 |   decEq (Reason _)             (PredicateFailed _ _) = No $ \case Refl impossible
 44 |
 45 | -- Short-circuit on Fail/Skip: once a failure occurs, subsequent
 46 | -- expectations in a do-block are skipped.
 47 | public export
 48 | data TestResult : Type -> Type where
 49 |   Pass : a -> TestResult a
 50 |   Fail : FailureInfo -> TestResult a
 51 |   Skip : (reason : Maybe String) -> TestResult a
 52 |
 53 | export
 54 | Show a => Show (TestResult a) where
 55 |   show (Pass x)      = "Pass " ++ show x
 56 |   show (Fail info)   = "Fail (" ++ show info ++ ")"
 57 |   show (Skip reason) = "Skip " ++ show reason
 58 |
 59 | export
 60 | DecEq a => DecEq (TestResult a) where
 61 |   decEq (Pass x) (Pass y) = case decEq x y of
 62 |     Yes Refl => Yes Refl
 63 |     No c     => No $ \case Refl => c Refl
 64 |   decEq (Fail i1) (Fail i2) = case decEq i1 i2 of
 65 |     Yes Refl => Yes Refl
 66 |     No c     => No $ \case Refl => c Refl
 67 |   decEq (Skip r1) (Skip r2) = case decEq r1 r2 of
 68 |     Yes Refl => Yes Refl
 69 |     No c     => No $ \case Refl => c Refl
 70 |   decEq (Pass _) (Fail _)   = No $ \case Refl impossible
 71 |   decEq (Pass _) (Skip _)   = No $ \case Refl impossible
 72 |   decEq (Fail _) (Pass _)   = No $ \case Refl impossible
 73 |   decEq (Fail _) (Skip _)   = No $ \case Refl impossible
 74 |   decEq (Skip _) (Pass _)   = No $ \case Refl impossible
 75 |   decEq (Skip _) (Fail _)   = No $ \case Refl impossible
 76 |
 77 | export
 78 | Functor TestResult where
 79 |   map f (Pass x)      = Pass (f x)
 80 |   map f (Fail info)   = Fail info
 81 |   map f (Skip reason) = Skip reason
 82 |
 83 | export
 84 | Applicative TestResult where
 85 |   pure = Pass
 86 |   (Pass f)      <*> x = map f x
 87 |   (Fail info)   <*> _ = Fail info
 88 |   (Skip reason) <*> _ = Skip reason
 89 |
 90 | export
 91 | Monad TestResult where
 92 |   (Pass x)      >>= f = f x
 93 |   (Fail info)   >>= _ = Fail info
 94 |   (Skip reason) >>= _ = Skip reason
 95 |
 96 | -- `m` is the test-action monad.
 97 | public export
 98 | data SpecTree : (m : Type -> Type) -> Type -> Type where
 99 |   Describe    : (label : String) -> (children : List (SpecTree m a)) -> SpecTree m a
100 |   It          : (label : String) -> (loc : Maybe SrcLoc) -> (test : a -> m (TestResult ())) -> SpecTree m a
101 |   Pending     : (label : String) -> (reason : Maybe String) -> SpecTree m a
102 |   Focused     : SpecTree m a -> SpecTree m a
103 |   WithCleanup : (cleanup : m ()) -> (children : List (SpecTree m a)) -> SpecTree m a
104 |
105 | -- SnocList gives O(1) appending per describe/it in a do-block.
106 | -- Idris 2 resolves the correct monad (Spec vs TestResult) via
107 | -- type-directed elaboration based on the expected return type.
108 | public export
109 | data Spec : (m : Type -> Type) -> Type -> Type -> Type where
110 |   MkSpec : SnocList (SpecTree m a) -> b -> Spec m a b
111 |
112 | export
113 | Functor (Spec m a) where
114 |   map f (MkSpec trees x) = MkSpec trees (f x)
115 |
116 | export
117 | Applicative (Spec m a) where
118 |   pure x = MkSpec [<] x
119 |   (MkSpec ts1 f) <*> (MkSpec ts2 x) = MkSpec (ts1 ++ ts2) (f x)
120 |
121 | export
122 | Monad (Spec m a) where
123 |   (MkSpec ts1 x) >>= f = let (MkSpec ts2 y) = f x in MkSpec (ts1 ++ ts2) y
124 |
125 | ||| Extract the tree list from a completed spec.
126 | export
127 | getSpecTrees : Spec m a () -> List (SpecTree m a)
128 | getSpecTrees (MkSpec trees ()) = trees <>> []
129 |
130 | public export
131 | record Summary where
132 |   constructor MkSummary
133 |   passed   : Nat
134 |   failed   : Nat
135 |   pending  : Nat
136 |   duration : Integer
137 |
138 | export
139 | Semigroup Summary where
140 |   (MkSummary p1 f1 pn1 d1) <+> (MkSummary p2 f2 pn2 d2) =
141 |     MkSummary (p1 + p2) (f1 + f2) (pn1 + pn2) (d1 + d2)
142 |
143 | export
144 | Monoid Summary where
145 |   neutral = MkSummary 0 0 0 0
146 |
147 | export
148 | Show Summary where
149 |   show s = show s.passed ++ " passing, "
150 |         ++ show s.failed ++ " failing, "
151 |         ++ show s.pending ++ " pending"
152 |
153 | export
154 | totalCount : Summary -> Nat
155 | totalCount s = s.passed + s.failed + s.pending
156 |
157 | public export
158 | record RunConfig where
159 |   constructor MkRunConfig
160 |   failFast    : Bool
161 |   showTiming  : Bool
162 |   match       : Maybe String
163 |   skip        : Maybe String
164 |   randomize   : Bool
165 |   seed        : Maybe Nat
166 |   junitOutput : Maybe String
167 |   rerun       : Bool
168 |   jobs        : Nat
169 |   color       : Bool
170 |
171 | ||| Default configuration: no fail-fast, no timing, no filters, colored output.
172 | export
173 | defaultConfig : RunConfig
174 | defaultConfig = MkRunConfig False False Nothing Nothing False Nothing Nothing False 0 True
175 |