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 | public export
 97 | data SpecTree : Type -> Type where
 98 |   Describe    : (label : String) -> (children : List (SpecTree a)) -> SpecTree a
 99 |   It          : (label : String) -> (loc : Maybe SrcLoc) -> (test : a -> IO (TestResult ())) -> SpecTree a
100 |   Pending     : (label : String) -> (reason : Maybe String) -> SpecTree a
101 |   Focused     : SpecTree a -> SpecTree a
102 |   WithCleanup : (cleanup : IO ()) -> (children : List (SpecTree a)) -> SpecTree a
103 |
104 | -- SnocList gives O(1) appending per describe/it in a do-block.
105 | -- Idris 2 resolves the correct monad (Spec vs TestResult) via
106 | -- type-directed elaboration based on the expected return type.
107 | public export
108 | data Spec : Type -> Type -> Type where
109 |   MkSpec : SnocList (SpecTree a) -> b -> Spec a b
110 |
111 | export
112 | Functor (Spec a) where
113 |   map f (MkSpec trees x) = MkSpec trees (f x)
114 |
115 | export
116 | Applicative (Spec a) where
117 |   pure x = MkSpec [<] x
118 |   (MkSpec ts1 f) <*> (MkSpec ts2 x) = MkSpec (ts1 ++ ts2) (f x)
119 |
120 | export
121 | Monad (Spec a) where
122 |   (MkSpec ts1 x) >>= f = let (MkSpec ts2 y) = f x in MkSpec (ts1 ++ ts2) y
123 |
124 | ||| Extract the tree list from a completed spec.
125 | export
126 | getSpecTrees : Spec a () -> List (SpecTree a)
127 | getSpecTrees (MkSpec trees ()) = trees <>> []
128 |
129 | public export
130 | record Summary where
131 |   constructor MkSummary
132 |   passed   : Nat
133 |   failed   : Nat
134 |   pending  : Nat
135 |   duration : Integer
136 |
137 | export
138 | Semigroup Summary where
139 |   (MkSummary p1 f1 d1 t1) <+> (MkSummary p2 f2 d2 t2) =
140 |     MkSummary (p1 + p2) (f1 + f2) (d1 + d2) (t1 + t2)
141 |
142 | export
143 | Monoid Summary where
144 |   neutral = MkSummary 0 0 0 0
145 |
146 | export
147 | Show Summary where
148 |   show s = show s.passed ++ " passing, "
149 |         ++ show s.failed ++ " failing, "
150 |         ++ show s.pending ++ " pending"
151 |
152 | export
153 | totalCount : Summary -> Nat
154 | totalCount s = s.passed + s.failed + s.pending
155 |
156 | public export
157 | record RunConfig where
158 |   constructor MkRunConfig
159 |   failFast    : Bool
160 |   showTiming  : Bool
161 |   match       : Maybe String
162 |   skip        : Maybe String
163 |   randomize   : Bool
164 |   seed        : Maybe Nat
165 |   junitOutput : Maybe String
166 |   rerun       : Bool
167 |   jobs        : Nat
168 |
169 | ||| Default configuration: no fail-fast, no timing, no filters.
170 | export
171 | defaultConfig : RunConfig
172 | defaultConfig = MkRunConfig False False Nothing Nothing False Nothing Nothing False 0
173 |