0 | module Test.Async.Spec.TestResult
  1 |
  2 | import Derive.Prelude
  3 | import IO.Async
  4 | import Text.Show.Diff
  5 |
  6 | %language ElabReflection
  7 | %default total
  8 |
  9 | ||| The difference between some expected and actual value.
 10 | public export
 11 | record Diff where
 12 |   constructor MkDiff
 13 |   diffPrefix  : String
 14 |   diffRemoved : String
 15 |   diffInfix   : String
 16 |   diffAdded   : String
 17 |   diffSuffix  : String
 18 |   diffValue   : ValueDiff
 19 |
 20 | %runElab derive "TestResult.Diff" [Show,Eq]
 21 |
 22 | public export
 23 | data TestResult : Type where
 24 |   Failure : Maybe Diff -> String -> TestResult
 25 |   Success : TestResult
 26 |
 27 | %runElab derive "TestResult" [Show,Eq]
 28 |
 29 | public export
 30 | 0 Test : Type -> Type
 31 | Test e = Async e [] TestResult
 32 |
 33 | dummy : Test e
 34 | dummy = pure Success
 35 |
 36 | public export
 37 | data TestTree : Type -> Type where
 38 |   Node : (name : String) -> List (TestTree e) -> TestTree e
 39 |   Leaf : (desc : String) -> Test e -> TestTree e
 40 |
 41 | public export
 42 | data Pre : Type where
 43 |   It   : Pre
 44 |   They : Pre
 45 |   Desc : String -> Pre
 46 |
 47 | export %inline
 48 | FromString Pre where fromString = Desc
 49 |
 50 | export %inline
 51 | it : Pre
 52 | it = It
 53 |
 54 | export %inline
 55 | they : Pre
 56 | they = They
 57 |
 58 | export
 59 | record Post e where
 60 |   constructor At
 61 |   desc : String
 62 |   test : Test e
 63 |
 64 | export %inline
 65 | at : String -> Test e -> Post e
 66 | at = At
 67 |
 68 | ||| Operator version of `at`
 69 | export %inline
 70 | (!:) : String -> Test e -> Post e
 71 | (!:) = At
 72 |
 73 | export
 74 | data Verb = Should | Can | Must
 75 |
 76 | export
 77 | Interpolation Verb where
 78 |   interpolate Should = "should"
 79 |   interpolate Can    = "can"
 80 |   interpolate Must   = "must"
 81 |
 82 | export %inline
 83 | leaf : Verb -> Post e -> TestTree e
 84 | leaf v (At d t) = Leaf "\{v} \{d}" t
 85 |
 86 | public export
 87 | record FlatSpecInstr e where
 88 |   constructor FSI
 89 |   verb : Verb
 90 |   pre  : Pre
 91 |   post : Post e
 92 |
 93 | export infixr 5 `should`,`at`,`must`,`can`,!:
 94 |
 95 | public export %inline
 96 | should : (pre : Pre) -> (post : Post e) -> FlatSpecInstr e
 97 | should = FSI Should
 98 |
 99 | public export %inline
100 | must : (pre : Pre) -> (post : Post e) -> FlatSpecInstr e
101 | must = FSI Must
102 |
103 | public export %inline
104 | can : (pre : Pre) -> (post : Post e) -> FlatSpecInstr e
105 | can = FSI Can
106 |
107 | public export
108 | data ValidInstrs : (is : List (FlatSpecInstr e)) -> Type where
109 |   IsValidInstrs :
110 |        {0 e : Type}
111 |     -> {0 v : Verb}
112 |     -> {0 s : String}
113 |     -> {0 p : Post e}
114 |     -> {0 t : List (FlatSpecInstr e)}
115 |     -> ValidInstrs (FSI v (Desc s) p :: t)
116 |
117 | export
118 | flatSpec :
119 |      (title : String)
120 |   -> (is    : List (FlatSpecInstr e))
121 |   -> {auto 0 prf : ValidInstrs is}
122 |   -> TestTree e
123 | flatSpec ttl (FSI v (Desc s) p :: t) @{IsValidInstrs} =
124 |   Node ttl (go [<] s [< leaf v p] t)
125 |
126 |   where
127 |     go :
128 |          SnocList (TestTree e)
129 |       -> String
130 |       -> SnocList (TestTree e)
131 |       -> List (FlatSpecInstr e)
132 |       -> List (TestTree e)
133 |     go sx s sy []                       = sx <>> [Node s $ sy <>> []]
134 |     go sx s sy (FSI v It       p :: xs) = go sx s (sy :< leaf v p) xs
135 |     go sx s sy (FSI v They     p :: xs) = go sx s (sy :< leaf v p) xs
136 |     go sx s sy (FSI v (Desc n) p :: xs) =
137 |       go (sx :< Node s (sy <>> [])) n [< leaf v p] xs
138 |
139 | --------------------------------------------------------------------------------
140 | -- Examples
141 | --------------------------------------------------------------------------------
142 |
143 | spec1 : List (FlatSpecInstr e)
144 | spec1 =
145 |   [ "an empty list" `should` "have length 0" `at` dummy
146 |   ,   it `should` "return Nothing on pop" `at` dummy
147 |   ,   it `should` "return a value on pop after pushing to it" !: dummy
148 |   , "a non-empty list" `should` "have length > 0" `at` dummy
149 |   ,   it `should` "return a Just on pop" `at` dummy
150 |   ]
151 |