{-# LANGUAGE CPP #-}
module UVMHS.Lib.Testing 
  ( module UVMHS.Lib.Testing
  ) where

import UVMHS.Core
import UVMHS.Lib.Pretty
import UVMHS.Lib.TreeNested

import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Syntax as TH

data Test = Test
  { Test -> Doc
testSrcLoc ∷ Doc
  , Test -> Doc
testSrcShow ∷ Doc
  , Test -> Word64
testValIter ∷ ℕ64
  , Test -> IO (Doc ∧ (() -> 𝔹))
testResult ∷ IO (Doc ∧ (() → 𝔹))
  }

eqTest ∷ (Eq a,Pretty a) ⇒ 𝐿 𝕊 → 𝕊 → 𝕊 → 𝕊 → a → a → 𝑇D Test
eqTest :: forall a.
(Eq a, Pretty a) =>
𝐿 𝕊 -> 𝕊 -> 𝕊 -> 𝕊 -> a -> a -> 𝑇D Test
eqTest 𝐿 𝕊
tags 𝕊
lS 𝕊
xS 𝕊
yS a
x a
y =
  let lD :: Doc
lD = 𝕊 -> Doc
ppString 𝕊
lS
      srcD :: Doc
srcD = Doc -> Doc
forall a. Pretty a => a -> Doc
pretty (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
        [ 𝕊 -> Doc -> Doc
ppCxt 𝕊
"L" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
xS
        , 𝕊 -> Doc -> Doc
ppCxt 𝕊
"R" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
yS
        ]
      valD :: Doc
valD = Doc -> Doc
forall a. Pretty a => a -> Doc
pretty (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
        [ 𝕊 -> Doc -> Doc
ppCxt 𝕊
"L" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
x
        , 𝕊 -> Doc -> Doc
ppCxt 𝕊
"R" (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. Pretty a => a -> Doc
pretty a
y
        ]
  in 𝐿 𝕊 -> 𝑇D Test -> 𝑇D Test
forall a. 𝐿 𝕊 -> 𝑇D a -> 𝑇D a
keys𝑇D 𝐿 𝕊
tags (𝑇D Test -> 𝑇D Test) -> 𝑇D Test -> 𝑇D Test
forall a b. (a -> b) -> a -> b
$ Test -> 𝑇D Test
forall a. a -> 𝑇D a
val𝑇D (Test -> 𝑇D Test) -> Test -> 𝑇D Test
forall a b. (a -> b) -> a -> b
$ Doc -> Doc -> Word64 -> IO (Doc ∧ (() -> 𝔹)) -> Test
Test Doc
lD Doc
srcD Word64
1 (IO (Doc ∧ (() -> 𝔹)) -> Test) -> IO (Doc ∧ (() -> 𝔹)) -> Test
forall a b. (a -> b) -> a -> b
$ (Doc ∧ (() -> 𝔹)) -> IO (Doc ∧ (() -> 𝔹))
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return ((Doc ∧ (() -> 𝔹)) -> IO (Doc ∧ (() -> 𝔹)))
-> (Doc ∧ (() -> 𝔹)) -> IO (Doc ∧ (() -> 𝔹))
forall a b. (a -> b) -> a -> b
$ Doc
valD Doc -> (() -> 𝔹) -> Doc ∧ (() -> 𝔹)
forall a b. a -> b -> a ∧ b
:* (\ () → a
x a -> a -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ a
y)

fuzzTest ∷ (Pretty a) ⇒ 𝐿 𝕊 → 𝕊 → 𝕊 → 𝕊 → ℕ64 → IO a → (a → 𝔹) → 𝑇D Test
fuzzTest :: forall a.
Pretty a =>
𝐿 𝕊 -> 𝕊 -> 𝕊 -> 𝕊 -> Word64 -> IO a -> (a -> 𝔹) -> 𝑇D Test
fuzzTest 𝐿 𝕊
tags 𝕊
lS 𝕊
xS 𝕊
pS Word64
k IO a
xM a -> 𝔹
p = do
  let lD :: Doc
lD = 𝕊 -> Doc
ppString 𝕊
lS
      srcD :: Doc
srcD = 𝑇D Doc -> Doc
forall a. Pretty a => a -> Doc
pretty (𝑇D Doc -> Doc) -> 𝑇D Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [𝑇D Doc] -> 𝑇D Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ 𝕊 -> 𝑇D Doc -> 𝑇D Doc
forall a. 𝕊 -> 𝑇D a -> 𝑇D a
key𝑇D 𝕊
"X" (𝑇D Doc -> 𝑇D Doc) -> 𝑇D Doc -> 𝑇D Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝑇D Doc
forall a. a -> 𝑇D a
val𝑇D (Doc -> 𝑇D Doc) -> Doc -> 𝑇D Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
xS
        , 𝕊 -> 𝑇D Doc -> 𝑇D Doc
forall a. 𝕊 -> 𝑇D a -> 𝑇D a
key𝑇D 𝕊
"P" (𝑇D Doc -> 𝑇D Doc) -> 𝑇D Doc -> 𝑇D Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝑇D Doc
forall a. a -> 𝑇D a
val𝑇D (Doc -> 𝑇D Doc) -> Doc -> 𝑇D Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
pS
        ]
      valD :: p -> Doc
valD p
x = 𝑇D Doc -> Doc
forall a. Pretty a => a -> Doc
pretty (𝑇D Doc -> Doc) -> 𝑇D Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [𝑇D Doc] -> 𝑇D Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ 𝕊 -> 𝑇D Doc -> 𝑇D Doc
forall a. 𝕊 -> 𝑇D a -> 𝑇D a
key𝑇D 𝕊
"X" (𝑇D Doc -> 𝑇D Doc) -> 𝑇D Doc -> 𝑇D Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝑇D Doc
forall a. a -> 𝑇D a
val𝑇D (Doc -> 𝑇D Doc) -> Doc -> 𝑇D Doc
forall a b. (a -> b) -> a -> b
$ p -> Doc
forall a. Pretty a => a -> Doc
pretty p
x
        ]
  𝐿 𝕊 -> 𝑇D Test -> 𝑇D Test
forall a. 𝐿 𝕊 -> 𝑇D a -> 𝑇D a
keys𝑇D 𝐿 𝕊
tags (𝑇D Test -> 𝑇D Test) -> 𝑇D Test -> 𝑇D Test
forall a b. (a -> b) -> a -> b
$ Test -> 𝑇D Test
forall a. a -> 𝑇D a
val𝑇D (Test -> 𝑇D Test) -> Test -> 𝑇D Test
forall a b. (a -> b) -> a -> b
$ Doc -> Doc -> Word64 -> IO (Doc ∧ (() -> 𝔹)) -> Test
Test Doc
lD Doc
srcD Word64
k (IO (Doc ∧ (() -> 𝔹)) -> Test) -> IO (Doc ∧ (() -> 𝔹)) -> Test
forall a b. (a -> b) -> a -> b
$ do
    a
x ← IO a
xM
    (Doc ∧ (() -> 𝔹)) -> IO (Doc ∧ (() -> 𝔹))
forall a. a -> IO a
forall (m :: * -> *) a. Return m => a -> m a
return ((Doc ∧ (() -> 𝔹)) -> IO (Doc ∧ (() -> 𝔹)))
-> (Doc ∧ (() -> 𝔹)) -> IO (Doc ∧ (() -> 𝔹))
forall a b. (a -> b) -> a -> b
$ a -> Doc
forall a. Pretty a => a -> Doc
valD a
x Doc -> (() -> 𝔹) -> Doc ∧ (() -> 𝔹)
forall a b. a -> b -> a ∧ b
:* (\ () → a -> 𝔹
p a
x)

data TestsOut = TestsOut
  { TestsOut -> 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
testsOutFailures ∷ 𝐿 𝕊 ⇰ 𝐼 (Doc ∧ Doc ∧ Doc)
  , TestsOut -> 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
testsOutMetrics ∷ 𝐿 𝕊 ⇰ ℕ ∧ ℕ
  }

instance Null TestsOut where
  null :: TestsOut
null = (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut
TestsOut 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
forall a. Null a => a
null 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
forall a. Null a => a
null
instance Append TestsOut where
  TestsOut 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
f₁ 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
m₁ ⧺ :: TestsOut -> TestsOut -> TestsOut
⧺ TestsOut 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
f₂ 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
m₂ = (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut
TestsOut (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
f₁ (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc))
-> (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
forall a. Append a => a -> a -> a
⧺ 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
f₂) ((𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut) -> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut
forall a b. (a -> b) -> a -> b
$ 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
m₁ (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
forall a. Append a => a -> a -> a
⧺ 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
m₂
instance Monoid TestsOut

runTests ∷ 𝔹 → 𝑇D Test → IO ()
runTests :: 𝔹 -> 𝑇D Test -> IO ()
runTests 𝔹
verb 𝑇D Test
tests = do
  Doc -> IO ()
forall a. Pretty a => a -> IO ()
pprint (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppComment 𝕊
"running tests…"
  IO ()
oflush
  let fₗ :: 𝐼 Test -> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
fₗ 𝐼 Test
ts = ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
-> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
forall (m :: * -> *). m () -> MU m
MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
 -> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO)))
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
-> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
forall a b. (a -> b) -> a -> b
$ 𝐼 Test
-> (Test -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
t -> (a -> m ()) -> m ()
eachOn 𝐼 Test
ts ((Test -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> (Test -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ \ (Test Doc
lD Doc
srcD Word64
k IO (Doc ∧ (() -> 𝔹))
valdpIO) → do
        𝐼 Word64
-> (Word64 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall (m :: * -> *) a t.
(Monad m, ToIter a t) =>
t -> (a -> m ()) -> m ()
eachOn (Word64 -> 𝐼 Word64
forall n. (Eq n, Zero n, One n, Plus n) => n -> 𝐼 n
upto Word64
k) ((Word64 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> (Word64 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
-> Word64 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. a -> b -> a
const (ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
 -> Word64 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
-> Word64
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ do
          Doc
valD :* () -> 𝔹
p ← IO (Doc ∧ (() -> 𝔹))
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) (Doc ∧ (() -> 𝔹))
forall a. IO a -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Doc ∧ (() -> 𝔹))
 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) (Doc ∧ (() -> 𝔹)))
-> IO (Doc ∧ (() -> 𝔹))
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) (Doc ∧ (() -> 𝔹))
forall a b. (a -> b) -> a -> b
$ IO (Doc ∧ (() -> 𝔹))
valdpIO
          let b :: 𝔹
b = () -> 𝔹
p ()
          𝐿 𝕊
tags ← 𝐼 𝕊 -> 𝐿 𝕊
forall a t. ToIter a t => t -> 𝐿 a
list (𝐼 𝕊 -> 𝐿 𝕊) -> (𝐿 𝕊 -> 𝐼 𝕊) -> 𝐿 𝕊 -> 𝐿 𝕊
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ 𝐿 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => t -> 𝐼 a
reverse (𝐿 𝕊 -> 𝐿 𝕊)
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) (𝐿 𝕊)
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) (𝐿 𝕊)
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ ReaderT (𝐿 𝕊) (WriterT TestsOut IO) (𝐿 𝕊)
forall (m :: * -> *) r. (Monad m, MonadReader r m) => m r
ask
          if 𝔹
b 
          then do
            𝔹
-> (() -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall (m :: * -> *). Return m => 𝔹 -> (() -> m ()) -> m ()
when 𝔹
verb ((() -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> (() -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ \ () →
              IO () -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a. IO a -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> IO () -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ Doc -> IO ()
forall a. Pretty a => a -> IO ()
pprint (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal
                [ Color -> Doc -> Doc
ppFG Color
teal (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
ppBD (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 𝕊 -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 𝕊 -> 𝕊) -> 𝐼 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝐿 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween 𝕊
":" 𝐿 𝕊
tags
                , Color -> Doc -> Doc
ppFG Color
green (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
"PASS" 
                , Color -> Doc -> Doc
ppFG Color
grayDark Doc
lD
                ]
            TestsOut -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell (TestsOut -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> TestsOut -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut
TestsOut 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
forall a. Null a => a
null ((𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut) -> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut
forall a b. (a -> b) -> a -> b
$ 𝐿 𝕊
tags 𝐿 𝕊 -> (ℕ ∧ ℕ) -> 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
forall a. 𝐿 𝕊 -> a -> 𝐿 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ (ℕ
forall a. One a => a
one ℕ -> ℕ -> ℕ ∧ ℕ
forall a b. a -> b -> a ∧ b
:* ℕ
forall a. Zero a => a
zero)
          else do
            𝔹
-> (() -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall (m :: * -> *). Return m => 𝔹 -> (() -> m ()) -> m ()
when 𝔹
verb ((() -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> (() -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ \ () → 
              IO () -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a. IO a -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> IO () -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ Doc -> IO ()
forall a. Pretty a => a -> IO ()
pprint (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal
                [ Color -> Doc -> Doc
ppFG Color
teal (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
ppBD (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 𝕊 -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 𝕊 -> 𝕊) -> 𝐼 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝐿 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween 𝕊
":" 𝐿 𝕊
tags
                , Color -> Doc -> Doc
ppFG Color
red (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
"FAIL"
                , Color -> Doc -> Doc
ppFG Color
grayDark Doc
lD
                ]
            TestsOut -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall o (m :: * -> *). MonadWriter o m => o -> m ()
tell (TestsOut -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> TestsOut -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut
TestsOut (𝐿 𝕊
tags 𝐿 𝕊 -> 𝐼 ((Doc ∧ Doc) ∧ Doc) -> 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
forall a. 𝐿 𝕊 -> a -> 𝐿 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ ((Doc ∧ Doc) ∧ Doc) -> 𝐼 ((Doc ∧ Doc) ∧ Doc)
forall a t. Single a t => a -> t
single (Doc
lD Doc -> Doc -> Doc ∧ Doc
forall a b. a -> b -> a ∧ b
:* Doc
srcD (Doc ∧ Doc) -> Doc -> (Doc ∧ Doc) ∧ Doc
forall a b. a -> b -> a ∧ b
:* Doc
valD)) ((𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut) -> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> TestsOut
forall a b. (a -> b) -> a -> b
$ 𝐿 𝕊
tags 𝐿 𝕊 -> (ℕ ∧ ℕ) -> 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
forall a. 𝐿 𝕊 -> a -> 𝐿 𝕊 ⇰ a
forall k s (d :: * -> *) a. Dict k s d => k -> a -> d a
↦ (ℕ
forall a. Zero a => a
zero ℕ -> ℕ -> ℕ ∧ ℕ
forall a b. a -> b -> a ∧ b
:* ℕ
forall a. One a => a
one)
      fₙ :: p -> MU m -> MU m
fₙ p
gr MU m
uM = m () -> MU m
forall (m :: * -> *). m () -> MU m
MU (m () -> MU m) -> m () -> MU m
forall a b. (a -> b) -> a -> b
$ (𝐿 p -> 𝐿 p) -> m () -> m ()
forall (m :: * -> *) r a.
(Monad m, MonadReader r m) =>
(r -> r) -> m a -> m a
mapEnv (p
gr p -> 𝐿 p -> 𝐿 p
forall a. a -> 𝐿 a -> 𝐿 a
:&) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ MU m -> m ()
forall (m :: * -> *). MU m -> m ()
unMU MU m
uM
  TestsOut
o ← WriterT TestsOut IO TestsOut -> IO TestsOut
forall o (m :: * -> *) a. Functor m => WriterT o m a -> m a
evalWriterT (WriterT TestsOut IO TestsOut -> IO TestsOut)
-> WriterT TestsOut IO TestsOut -> IO TestsOut
forall a b. (a -> b) -> a -> b
$ 𝐿 𝕊
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) TestsOut
-> WriterT TestsOut IO TestsOut
forall {k} r (m :: k -> *) (a :: k). r -> ReaderT r m a -> m a
runReaderT 𝐿 𝕊
forall a. 𝐿 a
Nil (ReaderT (𝐿 𝕊) (WriterT TestsOut IO) TestsOut
 -> WriterT TestsOut IO TestsOut)
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) TestsOut
-> WriterT TestsOut IO TestsOut
forall a b. (a -> b) -> a -> b
$ ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) TestsOut
forall o (m :: * -> *) a. (Monad m, MonadWriter o m) => m a -> m o
retOut (ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) TestsOut)
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) TestsOut
forall a b. (a -> b) -> a -> b
$ MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall (m :: * -> *). MU m -> m ()
unMU (MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
 -> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ())
-> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
-> ReaderT (𝐿 𝕊) (WriterT TestsOut IO) ()
forall a b. (a -> b) -> a -> b
$ 𝑇D Test
-> (𝐼 Test -> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO)))
-> (𝕊
    -> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
    -> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO)))
-> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
forall b a. Monoid b => 𝑇D a -> (𝐼 a -> b) -> (𝕊 -> b -> b) -> b
fold𝑇DOn 𝑇D Test
tests 𝐼 Test -> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
fₗ 𝕊
-> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
-> MU (ReaderT (𝐿 𝕊) (WriterT TestsOut IO))
forall {m :: * -> *} {p}.
(Monad m, MonadReader (𝐿 p) m) =>
p -> MU m -> MU m
fₙ
  Doc -> IO ()
forall a. Pretty a => a -> IO ()
pprint (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
    [ 𝕊 -> Doc
ppHeader 𝕊
"TEST METRICS"
    , 𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical (𝐼 Doc -> Doc) -> 𝐼 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝐿 𝕊 ∧ (ℕ ∧ ℕ)) -> ((𝐿 𝕊 ∧ (ℕ ∧ ℕ)) -> Doc) -> 𝐼 Doc
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> 𝐼 (𝐿 𝕊 ∧ (ℕ ∧ ℕ))
forall a t. ToIter a t => t -> 𝐼 a
iter ((𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> 𝐼 (𝐿 𝕊 ∧ (ℕ ∧ ℕ)))
-> (𝐿 𝕊 ⇰ (ℕ ∧ ℕ)) -> 𝐼 (𝐿 𝕊 ∧ (ℕ ∧ ℕ))
forall a b. (a -> b) -> a -> b
$ TestsOut -> 𝐿 𝕊 ⇰ (ℕ ∧ ℕ)
testsOutMetrics TestsOut
o) (((𝐿 𝕊 ∧ (ℕ ∧ ℕ)) -> Doc) -> 𝐼 Doc)
-> ((𝐿 𝕊 ∧ (ℕ ∧ ℕ)) -> Doc) -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ \ (𝐿 𝕊
tags :* (ℕ
p :* ℕ
f)) →
        let src :: 𝕊
src = 𝐼 𝕊 -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 𝕊 -> 𝕊) -> 𝐼 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝐿 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween 𝕊
":" 𝐿 𝕊
tags
        in 𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical (𝐼 Doc -> Doc) -> 𝐼 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [𝐼 Doc] -> 𝐼 Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
          [ if ℕ
p ℕ -> ℕ -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ
0 then 𝐼 Doc
forall a. 𝐼 a
null𝐼 else Doc -> 𝐼 Doc
forall a t. Single a t => a -> t
single (Doc -> 𝐼 Doc) -> Doc -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$
              [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal 
                [ Color -> Doc -> Doc
ppFG Color
green (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
"PASSED"
                , Doc -> Doc
ppBD (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Color -> Doc -> Doc
ppFG Color
green (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝕊 -> 𝕊
alignRight (ℕ -> ℕ
𝕟 ℕ
3) (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℕ
p
                , 𝕊 -> Doc
ppPun (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊
"» ",𝕊
src]
                ]
          , if ℕ
f ℕ -> ℕ -> 𝔹
forall a. Eq a => a -> a -> 𝔹
≡ ℕ
0 then 𝐼 Doc
forall a. Null a => a
null else Doc -> 𝐼 Doc
forall a t. Single a t => a -> t
single (Doc -> 𝐼 Doc) -> Doc -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ 
              [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal 
                [ Color -> Doc -> Doc
ppFG Color
red (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
"FAILED"
                , Doc -> Doc
ppBD (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Color -> Doc -> Doc
ppFG Color
red (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝕊 -> 𝕊
alignRight (ℕ -> ℕ
𝕟 ℕ
3) (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ ℕ -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℕ
f
                , 𝕊 -> Doc
ppPun (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊
"» ",𝕊
src]
                ]
          ]
       
    ]
  𝔹 -> (() -> IO ()) -> IO ()
forall (m :: * -> *). Return m => 𝔹 -> (() -> m ()) -> m ()
when (𝔹 -> 𝔹
not (𝔹 -> 𝔹) -> 𝔹 -> 𝔹
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty (𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝔹)
-> 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝔹
forall a b. (a -> b) -> a -> b
$ (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc))
forall a t. ToIter a t => t -> 𝐼 a
iter ((𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc)))
-> (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc))
forall a b. (a -> b) -> a -> b
$ TestsOut -> 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
testsOutFailures TestsOut
o) ((() -> IO ()) -> IO ()) -> (() -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \ () →
    Doc -> IO ()
forall a. Pretty a => a -> IO ()
pprint (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical
      [ 𝕊 -> Doc
ppHeader 𝕊
"FAILED TESTS"
      , 𝑇A Doc -> Doc
forall a. Pretty a => a -> Doc
pretty (𝑇A Doc -> Doc) -> 𝑇A Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝑇A Doc) -> 𝑇A Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 (𝑇A Doc) -> 𝑇A Doc) -> 𝐼 (𝑇A Doc) -> 𝑇A Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc))
-> ((𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝑇A Doc) -> 𝐼 (𝑇A Doc)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc))
forall a t. ToIter a t => t -> 𝐼 a
iter ((𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc)))
-> (𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝐼 (𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc))
forall a b. (a -> b) -> a -> b
$ TestsOut -> 𝐿 𝕊 ⇰ 𝐼 ((Doc ∧ Doc) ∧ Doc)
testsOutFailures TestsOut
o) (((𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝑇A Doc) -> 𝐼 (𝑇A Doc))
-> ((𝐿 𝕊 ∧ 𝐼 ((Doc ∧ Doc) ∧ Doc)) -> 𝑇A Doc) -> 𝐼 (𝑇A Doc)
forall a b. (a -> b) -> a -> b
$ \ (𝐿 𝕊
tags :* 𝐼 ((Doc ∧ Doc) ∧ Doc)
lsds) → 
          𝐼 (𝑇A Doc) -> 𝑇A Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 (𝑇A Doc) -> 𝑇A Doc) -> 𝐼 (𝑇A Doc) -> 𝑇A Doc
forall a b. (a -> b) -> a -> b
$ 𝐼 ((Doc ∧ Doc) ∧ Doc)
-> (((Doc ∧ Doc) ∧ Doc) -> 𝑇A Doc) -> 𝐼 (𝑇A Doc)
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐼 ((Doc ∧ Doc) ∧ Doc)
lsds ((((Doc ∧ Doc) ∧ Doc) -> 𝑇A Doc) -> 𝐼 (𝑇A Doc))
-> (((Doc ∧ Doc) ∧ Doc) -> 𝑇A Doc) -> 𝐼 (𝑇A Doc)
forall a b. (a -> b) -> a -> b
$ \ (Doc
lD :* Doc
srcD :* Doc
valD) → 
            𝕊 -> 𝑇A Doc -> 𝑇A Doc
forall a. 𝕊 -> 𝑇A a -> 𝑇A a
key𝑇A (𝐼 𝕊 -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 𝕊 -> 𝕊) -> 𝐼 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝐿 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween 𝕊
":" 𝐿 𝕊
tags) (𝑇A Doc -> 𝑇A Doc) -> 𝑇A Doc -> 𝑇A Doc
forall a b. (a -> b) -> a -> b
$ [𝑇A Doc] -> 𝑇A Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
              [ 𝕊 -> 𝑇A Doc -> 𝑇A Doc
forall a. 𝕊 -> 𝑇A a -> 𝑇A a
key𝑇A 𝕊
"loc" (𝑇A Doc -> 𝑇A Doc) -> 𝑇A Doc -> 𝑇A Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝑇A Doc
forall a. a -> 𝑇A a
val𝑇A (Doc -> 𝑇A Doc) -> Doc -> 𝑇A Doc
forall a b. (a -> b) -> a -> b
$ Color -> Doc -> Doc
ppFG Color
grayDark Doc
lD
              , 𝕊 -> 𝑇A Doc -> 𝑇A Doc
forall a. 𝕊 -> 𝑇A a -> 𝑇A a
key𝑇A 𝕊
"src" (𝑇A Doc -> 𝑇A Doc) -> 𝑇A Doc -> 𝑇A Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝑇A Doc
forall a. a -> 𝑇A a
val𝑇A Doc
srcD
              , 𝕊 -> 𝑇A Doc -> 𝑇A Doc
forall a. 𝕊 -> 𝑇A a -> 𝑇A a
key𝑇A 𝕊
"val" (𝑇A Doc -> 𝑇A Doc) -> 𝑇A Doc -> 𝑇A Doc
forall a b. (a -> b) -> a -> b
$ Doc -> 𝑇A Doc
forall a. a -> 𝑇A a
val𝑇A Doc
valD
              ]
      ]

𝔱 ∷ 𝕊 → TH.Q TH.Exp → TH.Q TH.Exp → TH.Q [TH.Dec]
#ifdef UVMHS_TESTS
𝔱 tag xEQ yEQ = 𝔱T @() tag (TH.Code $ TH.TExp ^$ xEQ) (TH.Code $ TH.TExp ^$ yEQ)
#else
𝔱 :: 𝕊 -> Q Exp -> Q Exp -> Q [Dec]
𝔱 𝕊
_ Q Exp
_ Q Exp
_ = [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Return m => a -> m a
return []
#endif

𝔱T ∷ (Eq a,Pretty a) ⇒ 𝕊 → TH.Code TH.Q a → TH.Code TH.Q a → TH.Q [TH.Dec]
𝔱T :: forall a. (Eq a, Pretty a) => 𝕊 -> Code Q a -> Code Q a -> Q [Dec]
𝔱T 𝕊
tag Code Q a
xEQ Code Q a
yEQ = do
  Loc
l ← Q Loc
TH.location
  let lS :: 𝕊
lS = [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat [[ℂ] -> 𝕊
frhsChars ([ℂ] -> 𝕊) -> [ℂ] -> 𝕊
forall a b. (a -> b) -> a -> b
$ Loc -> [ℂ]
TH.loc_module Loc
l,𝕊
":",ℤ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 (ℤ64 -> 𝕊) -> ℤ64 -> 𝕊
forall a b. (a -> b) -> a -> b
$ (ℤ64 ∧ ℤ64) -> ℤ64
forall a b. (a ∧ b) -> a
fst ((ℤ64 ∧ ℤ64) -> ℤ64) -> (ℤ64 ∧ ℤ64) -> ℤ64
forall a b. (a -> b) -> a -> b
$ CharPos -> ℤ64 ∧ ℤ64
forall a b. CHS a b => b -> a
frhs (CharPos -> ℤ64 ∧ ℤ64) -> CharPos -> ℤ64 ∧ ℤ64
forall a b. (a -> b) -> a -> b
$ Loc -> CharPos
TH.loc_start Loc
l]
  Exp
xE ← Code Q a -> Q Exp
forall a (m :: * -> *). Quote m => Code m a -> m Exp
TH.unTypeCode Code Q a
xEQ
  Exp
yE ← Code Q a -> Q Exp
forall a (m :: * -> *). Quote m => Code m a -> m Exp
TH.unTypeCode Code Q a
yEQ
  let tags :: 𝐿 𝕊
tags = 𝐼 𝕊 -> 𝐿 𝕊
forall a t. ToIter a t => t -> 𝐿 a
list (𝐼 𝕊 -> 𝐿 𝕊) -> 𝐼 𝕊 -> 𝐿 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝕊 -> 𝐼 𝕊
splitOn𝕊 𝕊
":" 𝕊
tag
      xS :: 𝕊
xS = Word64 -> 𝕊 -> 𝕊 -> 𝕊
truncate𝕊 (ℕ -> Word64
𝕟64 ℕ
80) 𝕊
"…" (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ [ℂ] -> 𝕊
frhsChars ([ℂ] -> 𝕊) -> [ℂ] -> 𝕊
forall a b. (a -> b) -> a -> b
$ Exp -> [ℂ]
forall a. Ppr a => a -> [ℂ]
TH.pprint Exp
xE
      yS :: 𝕊
yS = Word64 -> 𝕊 -> 𝕊 -> 𝕊
truncate𝕊 (ℕ -> Word64
𝕟64 ℕ
80) 𝕊
"…" (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ [ℂ] -> 𝕊
frhsChars ([ℂ] -> 𝕊) -> [ℂ] -> 𝕊
forall a b. (a -> b) -> a -> b
$ Exp -> [ℂ]
forall a. Ppr a => a -> [ℂ]
TH.pprint Exp
yE
  𝐼 (Code Q (𝑇D Test))
tests ← 𝐼 (Code Q (𝑇D Test))
-> 𝑂 (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test))
forall a. a -> 𝑂 a -> a
ifNone 𝐼 (Code Q (𝑇D Test))
forall a. Null a => a
null (𝑂 (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test)))
-> (Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝑂 (𝐼 (Code Q (𝑇D Test))))
-> Maybe (𝐼 (Code Q (𝑇D Test)))
-> 𝐼 (Code Q (𝑇D Test))
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝑂 (𝐼 (Code Q (𝑇D Test)))
forall a. Maybe a -> 𝑂 a
frhs𝑂 (Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test)))
-> Q (Maybe (𝐼 (Code Q (𝑇D Test)))) -> Q (𝐼 (Code Q (𝑇D Test)))
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ forall a. Typeable a => Q (Maybe a)
TH.getQ @(𝐼 (TH.Code TH.Q (𝑇D Test)))
  let t :: Code Q (𝑇D Test)
t = [|| 𝐿 𝕊 -> 𝕊 -> 𝕊 -> 𝕊 -> a -> a -> 𝑇D Test
forall a.
(Eq a, Pretty a) =>
𝐿 𝕊 -> 𝕊 -> 𝕊 -> 𝕊 -> a -> a -> 𝑇D Test
eqTest 𝐿 a
tags a
lS 𝕊
xS 𝕊
yS $$Code Q a
xEQ $$Code Q a
yEQ ||]
      tests' :: 𝐼 (Code Q (𝑇D Test))
tests' = 𝐼 (Code Q (𝑇D Test))
tests 𝐼 (Code Q (𝑇D Test))
-> 𝐼 (Code Q (𝑇D Test)) -> 𝐼 (Code Q (𝑇D Test))
forall a. Append a => a -> a -> a
⧺ Code Q (𝑇D Test) -> 𝐼 (Code Q (𝑇D Test))
forall a t. Single a t => a -> t
single Code Q (𝑇D Test)
t
  forall a. Typeable a => a -> Q ()
TH.putQ @(𝐼 (TH.Code TH.Q (𝑇D Test))) 𝐼 (Code Q (𝑇D Test))
tests'
  [d| |]

𝔣 ∷ 𝕊 → ℕ64 → TH.Q TH.Exp → TH.Q TH.Exp → TH.Q [TH.Dec]
#ifdef UVMHS_TESTS
𝔣 tag k xEQ pEQ = 𝔣T @() tag k (TH.Code $ TH.TExp ^$ xEQ) (TH.Code $ TH.TExp ^$ pEQ)
#else
𝔣 :: 𝕊 -> Word64 -> Q Exp -> Q Exp -> Q [Dec]
𝔣 𝕊
_ Word64
_ Q Exp
_ Q Exp
_ = [Dec] -> Q [Dec]
forall a. a -> Q a
forall (m :: * -> *) a. Return m => a -> m a
return []
#endif

𝔣T ∷ (Pretty a) ⇒ 𝕊 → ℕ64 → TH.Code TH.Q (IO a) → TH.Code TH.Q (a → 𝔹) → TH.Q [TH.Dec]
𝔣T :: forall a.
Pretty a =>
𝕊 -> Word64 -> Code Q (IO a) -> Code Q (a -> 𝔹) -> Q [Dec]
𝔣T 𝕊
tag Word64
k Code Q (IO a)
xEQ Code Q (a -> 𝔹)
pEQ = do
  Loc
l ← Q Loc
TH.location
  let lS :: 𝕊
lS = [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat
        [ [ℂ] -> 𝕊
frhsChars ([ℂ] -> 𝕊) -> [ℂ] -> 𝕊
forall a b. (a -> b) -> a -> b
$ Loc -> [ℂ]
TH.loc_module Loc
l
        , 𝕊
":"
        , ℤ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 (ℤ64 -> 𝕊) -> ℤ64 -> 𝕊
forall a b. (a -> b) -> a -> b
$ (ℤ64 ∧ ℤ64) -> ℤ64
forall a b. (a ∧ b) -> a
fst ((ℤ64 ∧ ℤ64) -> ℤ64) -> (ℤ64 ∧ ℤ64) -> ℤ64
forall a b. (a -> b) -> a -> b
$ CharPos -> ℤ64 ∧ ℤ64
forall a b. CHS a b => b -> a
frhs (CharPos -> ℤ64 ∧ ℤ64) -> CharPos -> ℤ64 ∧ ℤ64
forall a b. (a -> b) -> a -> b
$ Loc -> CharPos
TH.loc_start Loc
l
        ]
  Exp
xE ← Code Q (IO a) -> Q Exp
forall a (m :: * -> *). Quote m => Code m a -> m Exp
TH.unTypeCode Code Q (IO a)
xEQ
  Exp
pE ← Code Q (a -> 𝔹) -> Q Exp
forall a (m :: * -> *). Quote m => Code m a -> m Exp
TH.unTypeCode Code Q (a -> 𝔹)
pEQ
  let tags :: 𝐿 𝕊
tags = 𝐼 𝕊 -> 𝐿 𝕊
forall a t. ToIter a t => t -> 𝐿 a
list (𝐼 𝕊 -> 𝐿 𝕊) -> 𝐼 𝕊 -> 𝐿 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝕊 -> 𝐼 𝕊
splitOn𝕊 𝕊
":" 𝕊
tag
      xS :: 𝕊
xS = Word64 -> 𝕊 -> 𝕊 -> 𝕊
truncate𝕊 (ℕ -> Word64
𝕟64 ℕ
80) 𝕊
"…" (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ [ℂ] -> 𝕊
frhsChars ([ℂ] -> 𝕊) -> [ℂ] -> 𝕊
forall a b. (a -> b) -> a -> b
$ Exp -> [ℂ]
forall a. Ppr a => a -> [ℂ]
TH.pprint Exp
xE
      pS :: 𝕊
pS = Word64 -> 𝕊 -> 𝕊 -> 𝕊
truncate𝕊 (ℕ -> Word64
𝕟64 ℕ
80) 𝕊
"…" (𝕊 -> 𝕊) -> 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ [ℂ] -> 𝕊
frhsChars ([ℂ] -> 𝕊) -> [ℂ] -> 𝕊
forall a b. (a -> b) -> a -> b
$ Exp -> [ℂ]
forall a. Ppr a => a -> [ℂ]
TH.pprint Exp
pE
  𝐼 (Code Q (𝑇D Test))
tests ← 𝐼 (Code Q (𝑇D Test))
-> 𝑂 (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test))
forall a. a -> 𝑂 a -> a
ifNone 𝐼 (Code Q (𝑇D Test))
forall a. Null a => a
null (𝑂 (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test)))
-> (Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝑂 (𝐼 (Code Q (𝑇D Test))))
-> Maybe (𝐼 (Code Q (𝑇D Test)))
-> 𝐼 (Code Q (𝑇D Test))
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝑂 (𝐼 (Code Q (𝑇D Test)))
forall a. Maybe a -> 𝑂 a
frhs𝑂 (Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test)))
-> Q (Maybe (𝐼 (Code Q (𝑇D Test)))) -> Q (𝐼 (Code Q (𝑇D Test)))
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ forall a. Typeable a => Q (Maybe a)
TH.getQ @(𝐼 (TH.Code TH.Q (𝑇D Test)))
  let t' :: Code Q (𝑇D Test)
t' = [|| 𝐿 𝕊 -> 𝕊 -> 𝕊 -> 𝕊 -> Word64 -> IO a -> (a -> 𝔹) -> 𝑇D Test
forall a.
Pretty a =>
𝐿 𝕊 -> 𝕊 -> 𝕊 -> 𝕊 -> Word64 -> IO a -> (a -> 𝔹) -> 𝑇D Test
fuzzTest 𝐿 a
tags a
lS 𝕊
xS 𝕊
pS Word64
k $$Code Q (IO a)
xEQ $$Code Q (a -> 𝔹)
pEQ ||]
      tests' :: 𝐼 (Code Q (𝑇D Test))
tests' = 𝐼 (Code Q (𝑇D Test))
tests 𝐼 (Code Q (𝑇D Test))
-> 𝐼 (Code Q (𝑇D Test)) -> 𝐼 (Code Q (𝑇D Test))
forall a. Append a => a -> a -> a
⧺ Code Q (𝑇D Test) -> 𝐼 (Code Q (𝑇D Test))
forall a t. Single a t => a -> t
single Code Q (𝑇D Test)
t'
  forall a. Typeable a => a -> Q ()
TH.putQ @(𝐼 (TH.Code TH.Q (𝑇D Test))) 𝐼 (Code Q (𝑇D Test))
tests'
  [d| |]

buildTests ∷ TH.Q [TH.Dec]
buildTests :: Q [Dec]
buildTests = do
  𝐼 (Code Q (𝑇D Test))
testEQs ← 𝐼 (Code Q (𝑇D Test))
-> 𝑂 (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test))
forall a. a -> 𝑂 a -> a
ifNone 𝐼 (Code Q (𝑇D Test))
forall a. Null a => a
null (𝑂 (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test)))
-> (Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝑂 (𝐼 (Code Q (𝑇D Test))))
-> Maybe (𝐼 (Code Q (𝑇D Test)))
-> 𝐼 (Code Q (𝑇D Test))
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝑂 (𝐼 (Code Q (𝑇D Test)))
forall a. Maybe a -> 𝑂 a
frhs𝑂 (Maybe (𝐼 (Code Q (𝑇D Test))) -> 𝐼 (Code Q (𝑇D Test)))
-> Q (Maybe (𝐼 (Code Q (𝑇D Test)))) -> Q (𝐼 (Code Q (𝑇D Test)))
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ forall a. Typeable a => Q (Maybe a)
TH.getQ @(𝐼 (TH.Code TH.Q (𝑇D Test)))
  Loc
l ← Q Loc
TH.location
  let modNameS :: 𝕊
modNameS = [ℂ] -> 𝕊
frhsChars ([ℂ] -> 𝕊) -> [ℂ] -> 𝕊
forall a b. (a -> b) -> a -> b
$ Loc -> [ℂ]
TH.loc_module Loc
l 
      testsNameS :: 𝕊
testsNameS = 𝕊
"g__TESTS__" 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊 -> 𝕊 -> 𝕊 -> 𝕊
replace𝕊 𝕊
"." 𝕊
"__" 𝕊
modNameS
      testsName :: Name
testsName = [ℂ] -> Name
TH.mkName ([ℂ] -> Name) -> [ℂ] -> Name
forall a b. (a -> b) -> a -> b
$ 𝕊 -> [ℂ]
tohsChars 𝕊
testsNameS
      testEQs' ∷ TH.Code TH.Q [𝑇D Test]
      testEQs' :: Code Q [𝑇D Test]
testEQs' = Q (TExp [𝑇D Test]) -> Code Q [𝑇D Test]
forall (m :: * -> *) a. m (TExp a) -> Code m a
TH.Code (Q (TExp [𝑇D Test]) -> Code Q [𝑇D Test])
-> Q (TExp [𝑇D Test]) -> Code Q [𝑇D Test]
forall a b. (a -> b) -> a -> b
$ Exp -> TExp [𝑇D Test]
forall a. Exp -> TExp a
TH.TExp (Exp -> TExp [𝑇D Test]) -> Q Exp -> Q (TExp [𝑇D Test])
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ [Q Exp] -> Q Exp
forall (m :: * -> *). Quote m => [m Exp] -> m Exp
TH.listE ([Q Exp] -> Q Exp) -> [Q Exp] -> Q Exp
forall a b. (a -> b) -> a -> b
$ 𝐼 (Q Exp) -> [Q Exp]
forall a t. ToIter a t => t -> [a]
lazyList (𝐼 (Q Exp) -> [Q Exp]) -> 𝐼 (Q Exp) -> [Q Exp]
forall a b. (a -> b) -> a -> b
$ (Code Q (𝑇D Test) -> Q Exp) -> 𝐼 (Code Q (𝑇D Test)) -> 𝐼 (Q Exp)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map Code Q (𝑇D Test) -> Q Exp
forall a (m :: * -> *). Quote m => Code m a -> m Exp
TH.unTypeCode 𝐼 (Code Q (𝑇D Test))
testEQs
      testsEQ ∷ TH.Code TH.Q (𝑇D Test)
      testsEQ :: Code Q (𝑇D Test)
testsEQ = [|| t -> a
forall a t. (Monoid a, ToIter a t) => t -> a
concat $$Code Q [𝑇D Test]
testEQs' ||]
  [[Dec]] -> [Dec]
forall a t. (Monoid a, ToIter a t) => t -> a
concat ([[Dec]] -> [Dec]) -> Q [[Dec]] -> Q [Dec]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ [Q [Dec]] -> Q [[Dec]]
forall (t :: * -> *) (m :: * -> *) a.
(FunctorM t, Monad m) =>
t (m a) -> m (t a)
exchange ([Q [Dec]] -> Q [[Dec]]) -> [Q [Dec]] -> Q [[Dec]]
forall a b. (a -> b) -> a -> b
$
    [ Dec -> [Dec]
forall a t. Single a t => a -> t
single (Dec -> [Dec]) -> Q Dec -> Q [Dec]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ Name -> Q Type -> Q Dec
forall (m :: * -> *). Quote m => Name -> m Type -> m Dec
TH.sigD Name
testsName [t| 𝑇D Test |]
    , [d| $(Name -> Q Pat
forall (m :: * -> *). Quote m => Name -> m Pat
TH.varP Name
testsName) = $(Code Q (𝑇D Test) -> Q Exp
forall a (m :: * -> *). Quote m => Code m a -> m Exp
TH.unTypeCode Code Q (𝑇D Test)
testsEQ) |]
    ]
    
testModules ∷ 𝔹 → [𝕊] → TH.Code TH.Q (IO ())
testModules :: 𝔹 -> [𝕊] -> Code Q (IO ())
testModules 𝔹
verb [𝕊]
nsS =
  let nss :: [𝐼 𝕊]
nss = (𝕊 -> 𝐼 𝕊) -> [𝕊] -> [𝐼 𝕊]
forall a b. (a -> b) -> [a] -> [b]
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝕊 -> 𝕊 -> 𝐼 𝕊
splitOn𝕊 𝕊
":") [𝕊]
nsS
      testsNamesS :: [𝕊]
testsNamesS = [𝐼 𝕊] -> (𝐼 𝕊 -> 𝕊) -> [𝕊]
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn [𝐼 𝕊]
nss ((𝐼 𝕊 -> 𝕊) -> [𝕊]) -> (𝐼 𝕊 -> 𝕊) -> [𝕊]
forall a b. (a -> b) -> a -> b
$ \ 𝐼 𝕊
ns → 
        𝐼 𝕊 -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 𝕊 -> 𝕊) -> 𝐼 𝕊 -> 𝕊
forall a b. (a -> b) -> a -> b
$ 𝕊 -> 𝐼 𝕊 -> 𝐼 𝕊
forall a t. ToIter a t => a -> t -> 𝐼 a
inbetween 𝕊
"." (𝐼 𝕊 -> 𝐼 𝕊) -> 𝐼 𝕊 -> 𝐼 𝕊
forall a b. (a -> b) -> a -> b
$ 𝐼 𝕊 -> (𝕊 -> 𝕊) -> 𝐼 𝕊
forall a t. ToIter a t => t -> (a -> a) -> 𝐼 a
mapLastOn 𝐼 𝕊
ns ((𝕊 -> 𝕊) -> 𝐼 𝕊) -> (𝕊 -> 𝕊) -> 𝐼 𝕊
forall a b. (a -> b) -> a -> b
$ \ 𝕊
n → 𝕊
"g__TESTS__" 𝕊 -> 𝕊 -> 𝕊
forall a. Append a => a -> a -> a
⧺ 𝕊 -> 𝕊 -> 𝕊 -> 𝕊
replace𝕊 𝕊
"." 𝕊
"__" 𝕊
n
      testsNames :: [Name]
testsNames = [𝕊] -> (𝕊 -> Name) -> [Name]
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn [𝕊]
testsNamesS ((𝕊 -> Name) -> [Name]) -> (𝕊 -> Name) -> [Name]
forall a b. (a -> b) -> a -> b
$ \ 𝕊
testsNameS → [ℂ] -> Name
TH.mkName ([ℂ] -> Name) -> [ℂ] -> Name
forall a b. (a -> b) -> a -> b
$ 𝕊 -> [ℂ]
tohsChars 𝕊
testsNameS
      testNamesE :: [Q Exp]
testNamesE = [Name] -> (Name -> Q Exp) -> [Q Exp]
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn [Name]
testsNames ((Name -> Q Exp) -> [Q Exp]) -> (Name -> Q Exp) -> [Q Exp]
forall a b. (a -> b) -> a -> b
$ \ Name
testsName → Name -> Q Exp
forall (m :: * -> *). Quote m => Name -> m Exp
TH.varE Name
testsName
      testsEQ ∷ TH.Code TH.Q [𝑇D Test]
      testsEQ :: Code Q [𝑇D Test]
testsEQ = Q (TExp [𝑇D Test]) -> Code Q [𝑇D Test]
forall (m :: * -> *) a. m (TExp a) -> Code m a
TH.Code (Q (TExp [𝑇D Test]) -> Code Q [𝑇D Test])
-> Q (TExp [𝑇D Test]) -> Code Q [𝑇D Test]
forall a b. (a -> b) -> a -> b
$ Exp -> TExp [𝑇D Test]
forall a. Exp -> TExp a
TH.TExp (Exp -> TExp [𝑇D Test]) -> Q Exp -> Q (TExp [𝑇D Test])
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
^$ [Q Exp] -> Q Exp
forall (m :: * -> *). Quote m => [m Exp] -> m Exp
TH.listE ([Q Exp] -> Q Exp) -> [Q Exp] -> Q Exp
forall a b. (a -> b) -> a -> b
$ [Q Exp] -> [Q Exp]
forall a t. ToIter a t => t -> [a]
lazyList [Q Exp]
testNamesE
  in
  [|| 𝔹 -> 𝑇D Test -> IO ()
runTests 𝔹
verb (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ t -> a
forall a t. (Monoid a, ToIter a t) => t -> a
concat $$Code Q [𝑇D Test]
testsEQ ||]