2 | import Language.Reflection
3 | import Language.Reflection.TTImp
6 | %language ElabReflection
10 | describe : String -> Spec m a () -> Spec m a ()
11 | describe label body = MkSpec [< Describe label (getSpecTrees body)] ()
15 | context : String -> Spec m a () -> Spec m a ()
21 | it : Applicative m => String -> Lazy (TestResult ()) -> Spec m a ()
22 | it label result = MkSpec [< It label Nothing (\_ => pure result)] ()
26 | itIO : HasIO m => String -> IO (TestResult ()) -> Spec m a ()
27 | itIO label action = MkSpec [< It label Nothing (\_ => liftIO action)] ()
31 | itWith : Applicative m => String -> (a -> TestResult ()) -> Spec m a ()
32 | itWith label f = MkSpec [< It label Nothing (\res => pure (f res))] ()
36 | itIOWith : HasIO m => String -> (a -> IO (TestResult ())) -> Spec m a ()
37 | itIOWith label f = MkSpec [< It label Nothing (\res => liftIO (f res))] ()
44 | itLoc : Applicative m => TTImp -> String -> Lazy (TestResult ()) -> Elab (Spec m a ())
45 | itLoc t label result = do
46 | let loc = fcToSrcLoc (getFC t)
47 | pure $
MkSpec [< It label (Just loc) (\_ => pure result)] ()
53 | itIOLoc : HasIO m => TTImp -> String -> IO (TestResult ()) -> Elab (Spec m a ())
54 | itIOLoc t label action = do
55 | let loc = fcToSrcLoc (getFC t)
56 | pure $
MkSpec [< It label (Just loc) (\_ => liftIO action)] ()
60 | xit : String -> Lazy (TestResult ()) -> Spec m a ()
61 | xit label _ = MkSpec [< Pending label Nothing] ()
65 | xitIO : String -> Lazy (IO (TestResult ())) -> Spec m a ()
66 | xitIO label _ = MkSpec [< Pending label Nothing] ()
71 | pendTree : SpecTree m a -> List (SpecTree m a)
72 | pendTree (It label _ _) = [Pending label Nothing]
73 | pendTree (Describe label cs) = [Describe label (pendTrees cs)]
74 | pendTree (Pending label reason) = [Pending label reason]
75 | pendTree (Focused t) = pendTree t
76 | pendTree (WithCleanup _ cs) = pendTrees cs
78 | pendTrees : List (SpecTree m a) -> List (SpecTree m a)
80 | pendTrees (t :: ts) = pendTree t ++ pendTrees ts
85 | xdescribe : String -> Spec m a () -> Spec m a ()
86 | xdescribe label body = MkSpec [< Describe label (pendTrees (getSpecTrees body))] ()
90 | xcontext : String -> Spec m a () -> Spec m a ()
91 | xcontext = xdescribe
95 | fit : Applicative m => String -> Lazy (TestResult ()) -> Spec m a ()
96 | fit label result = MkSpec [< Focused (It label Nothing (\_ => pure result))] ()
100 | fdescribe : String -> Spec m a () -> Spec m a ()
101 | fdescribe label body = MkSpec [< Focused (Describe label (getSpecTrees body))] ()
105 | fcontext : String -> Spec m a () -> Spec m a ()
106 | fcontext = fdescribe
111 | focus : Spec m a () -> Spec m a ()
112 | focus body = MkSpec (Lin <>< map Focused (getSpecTrees body)) ()