{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Unused LANGUAGE pragma" #-}

-- {-# OPTIONS_GHC -ddump-splices #-}

module Grisette.Unified.UnifiedClassesTest (unifiedClassesTest) where

import Control.Monad.Except (ExceptT, MonadError (throwError))
import Control.Monad.Identity (Identity (Identity))
import qualified Data.Text as T
import GHC.TypeNats (KnownNat, type (<=))
import Grisette
  ( Mergeable,
    SymBool,
    SymEq,
    SymInteger,
    SymWordN,
    Union,
    WordN,
    deriveWith,
    mrgReturn,
    symAnd,
  )
import qualified Grisette
import Grisette.Internal.TH.Derivation.Common
  ( DeriveConfig
      ( bitSizePositions,
        evalModeConfig,
        needExtraMergeableUnderEvalMode
      ),
    EvalModeConfig (EvalModeConstraints),
  )
import Grisette.TestUtil.SymbolicAssertion ((.@?=))
import Grisette.Unified
  ( BaseMonad,
    EvalModeBV,
    EvalModeBase,
    EvalModeInteger,
    GetBool,
    GetData,
    GetInteger,
    GetWordN,
    UnifiedBranching,
    UnifiedSymEq,
    UnifiedSymEq1,
    mrgIf,
    (.==),
  )
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.HUnit ((@?=))

type M mode = ExceptT T.Text (BaseMonad mode)

testBranching ::
  forall mode m.
  ( EvalModeBase mode,
    EvalModeInteger mode,
    UnifiedBranching mode m,
    MonadError T.Text m
  ) =>
  GetInteger mode ->
  m (GetInteger mode)
testBranching x =
  mrgIf (x .== 1 :: GetBool mode) (return x) (throwError "err")

testBranchingBase ::
  forall mode.
  (EvalModeBase mode, EvalModeInteger mode) =>
  GetInteger mode ->
  M mode (GetInteger mode)
testBranchingBase x =
  mrgIf (x .== 1 :: GetBool mode) (return x) (throwError "err")

data X mode n f a
  = X
      (GetBool mode)
      [GetWordN mode n]
      (GetData mode (X mode n f a))
      [GetData mode (X mode n f a)]
      a
      (f a)
  | XNil

#if MIN_VERSION_base(4,16,0)
deriveWith
  ( mempty
      { evalModeConfig =
          [(0, EvalModeConstraints [''EvalModeBV, ''EvalModeBase])],
        bitSizePositions = [1],
        needExtraMergeableUnderEvalMode = True
      }
  )
  [''X]
  [ ''Mergeable,
    ''Eq,
    ''SymEq,
    ''UnifiedSymEq
  ]

testSEq ::
  forall mode n f a.
  ( EvalModeBase mode,
    EvalModeBV mode,
    1 <= n,
    KnownNat n,
    UnifiedSymEq1 mode f,
    UnifiedSymEq mode a
  ) =>
  X mode n f a ->
  X mode n f a ->
  GetBool mode
testSEq = (.==)

unifiedClassesTest :: Test
unifiedClassesTest =
  testGroup
    "UnifiedClasses"
    [ testGroup
        "UnifiedBranching"
        [ testCase "branchingBase 'Con" $
            testBranchingBase (1 :: Integer) @?= return 1,
          testCase "branchingBase 'Sym" $ do
            let a = "a" :: SymInteger
            let expected =
                  Grisette.mrgIf
                    (a Grisette..== 1)
                    (return a)
                    (throwError "err")
            testBranchingBase a .@?= expected,
          testCase "branching 'Con" $
            testBranching 1 @?= (return 1 :: Either T.Text Integer),
          testCase "branching 'Sym" $
            testBranching 1 .@?= (return 1 :: ExceptT T.Text Union SymInteger)
        ],
      testGroup
        "UnifiedSEq"
        [ testCase "testSEq 'Con" $ do
            let x1 = X True [1 :: WordN 8] (Identity XNil) [Identity XNil] (1 :: Integer) [1]
            let x2 = X False [1 :: WordN 8] (Identity XNil) [Identity XNil] (1 :: Integer) [2]
            testSEq x1 x1 .@?= True
            testSEq x1 x2 .@?= False,
          testCase "testSEq 'Sym" $ do
            let x1 =
                  X
                    "a"
                    [1 :: SymWordN 8]
                    (mrgReturn XNil)
                    [mrgReturn XNil]
                    ("x" :: SymInteger)
                    ["w"]
            let x2 =
                  X
                    "b"
                    [1 :: SymWordN 8]
                    (mrgReturn XNil)
                    [mrgReturn XNil]
                    ("y" :: SymInteger)
                    ["z"]
            testSEq x1 x2
              .@?= symAnd
                [ (("a" :: SymBool) .== "b"),
                  (("x" :: SymInteger) .== "y"),
                  (("w" :: SymInteger) .== "z")
                ]
        ]
    ]

#else
unifiedClassesTest :: Test
unifiedClassesTest = testGroup "UnifiedClasses" []
#endif