{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctorsTests where

import Control.Monad.Coroutine.SuspensionFunctors
import Grisette
import Grisette.Lib.Control.Monad.Coroutine.SuspensionFunctors ()
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck

testMergeableSimpleEquivClass ::
  (HasCallStack, Mergeable x, Show x, Eq x) => x -> [DynamicSortedIdx] -> [(SymBool, x, x, x)] -> Assertion
testMergeableSimpleEquivClass x idxs cases = do
  let (idxsT, s) = resolveStrategy rootStrategy x
  case s of
    SimpleStrategy m -> do
      idxsT @=? idxs
      go cases
      where
        go [] = return ()
        go ((c, t, f, r) : xs) = do
          fst (resolveStrategy rootStrategy t) @=? idxs
          fst (resolveStrategy rootStrategy f) @=? idxs
          fst (resolveStrategy rootStrategy r) @=? idxs
          m c t f @=? r
          go xs
    _ -> assertFailure $ "Bad strategy type for " ++ show x

testMergeableSimpleEquivClass' ::
  (HasCallStack, Mergeable x, Show y, Eq y) => (x -> y) -> x -> [DynamicSortedIdx] -> [(SymBool, x, x, x)] -> Assertion
testMergeableSimpleEquivClass' vis x idxs cases = do
  let (idxsT, s) = resolveStrategy rootStrategy x
  case s of
    SimpleStrategy m -> do
      idxsT @=? idxs
      go cases
      where
        go [] = return ()
        go ((c, t, f, r) : xs) = do
          fst (resolveStrategy rootStrategy t) @=? idxs
          fst (resolveStrategy rootStrategy f) @=? idxs
          fst (resolveStrategy rootStrategy r) @=? idxs
          vis (m c t f) @=? vis r
          go xs
    _ -> assertFailure $ "Bad strategy type for " ++ show (vis x)

suspensionFunctorsTests :: TestTree
suspensionFunctorsTests =
  testGroup
    "SuspensionFunctorsSpec"
    [ testGroup
        "Mergeable for suspension functors"
        $ let visYield (Yield a b) = (a, b)
           in [ testProperty "Yield Integer Integer" $
                  ioProperty . \(x :: Integer, y :: Integer) -> do
                    let (idxs, SimpleStrategy s) = resolveStrategy rootStrategy (Yield x y)
                    idxs @=? [DynamicSortedIdx x, DynamicSortedIdx y]
                    visYield (s "a" (Yield x y) (Yield x y)) @=? visYield (Yield x y),
                testCase "Yield SymBool SymBool" $ do
                  testMergeableSimpleEquivClass'
                    (\(Yield a b) -> (a, b))
                    (Yield "a" "b" :: Yield SymBool SymBool)
                    []
                    [ ( "a",
                        Yield "b" "c",
                        Yield "d" "e",
                        Yield (ites "a" "b" "d") (ites "a" "c" "e")
                      )
                    ],
                testCase "Await SymBool SymBool" $ do
                  let SimpleStrategy s = rootStrategy :: MergingStrategy (Await SymBool SymBool)
                  let a1 = Await nots
                  let a2 = Await ("a" &&~)
                  let Await a3 = s "b" a1 a2
                  a3 "c" @=? ites "b" (nots "c") ("a" &&~ "c"),
                testCase "Request SymBool SymBool SymBool" $ do
                  let SimpleStrategy s = rootStrategy :: MergingStrategy (Request SymBool SymBool SymBool)
                  let a1 = Request "a" nots
                  let a2 = Request "b" ("c" &&~)
                  let Request v3 a3 = s "d" a1 a2
                  v3 @=? ites "d" "a" "b"
                  a3 "e" @=? ites "d" (nots "e") ("c" &&~ "e")
              ]
    ]