content: module Regression.T7 (test7) where
  
  import Data.Monoid
  import Control.Monad
  
  import Ether
  import qualified Control.Monad.Writer as T
  
  import Test.Tasty
  import Test.Tasty.QuickCheck
  
  data WTag
  
  testEther
    :: Num a
    => T.MonadWriter (Sum a) m
    => MonadWriter WTag (Sum a) m
    => [a] -> m ()
  testEther xs = do
    forM_ xs $ \x -> do
      u1 <- T.tell (Sum x)
      u2 <- tell @WTag (Sum 1)
      when (u1 /= u2) $ error "Impossible"
  
  runner1 :: Num a => [a] -> (a, a)
  runner1 xs =
    let (s, c) = T.runWriter . execWriterT @WTag $ testEther xs
    in (getSum s, getSum c)
  
  runner2 :: Num a => [a] -> (a, a)
  runner2 xs =
    let (c, s) = runWriter @WTag . T.execWriterT $ testEther xs
    in (getSum s, getSum c)
  
  triangular :: Integral a => a -> a
  triangular n = div (n * (n + 1)) 2
  
  test7 :: TestTree
  test7 = testGroup "T7: Triangular via Ether"
    [ testProperty "runner₁ works"
      $ \n -> property
      $ let n' = abs n :: Integer
        in runner1 [1..n'] == (n', triangular n')
    , testProperty "runner₂ works"
      $ \n -> property
      $ let n' = abs n :: Integer
        in runner2 [1..n'] == (n', triangular n')
    , testProperty "runner₁ == runner₂"
      $ \(ns :: [Integer]) -> property
      $ runner1 ns == runner2 ns
    ]
  