content: {-# LANGUAGE DeriveAnyClass             #-}
  {-# LANGUAGE DerivingStrategies         #-}
  {-# LANGUAGE FlexibleInstances          #-}
  {-# LANGUAGE LambdaCase                 #-}
  {-# LANGUAGE MultiParamTypeClasses      #-}
  {-# LANGUAGE ScopedTypeVariables        #-}
  {-# LANGUAGE TypeApplications           #-}
  {-# LANGUAGE UndecidableInstances       #-}
  {-# OPTIONS_GHC -Wredundant-constraints #-}
  {-# OPTIONS_GHC -fno-warn-orphans       #-}
  
  module Spec.PropertyTests where
  
  import Control.Applicative
  import Control.Monad
  import Control.Monad.State.Strict (StateT (..))
  import Control.Monad.State.Class
  import Data.Function
  import Data.Functor.Identity
  import Data.Monoid (Sum (..))
  import Refinery.ProofState
  import Refinery.Tactic
  import Refinery.Tactic.Internal
  import Test.Hspec
  import Test.QuickCheck hiding (Failure)
  import Test.QuickCheck.Checkers
  import Test.QuickCheck.Classes
  import Checkers
  import Data.Foldable
  
  testBatch :: TestBatch -> Spec
  testBatch (batchName, tests) = describe ("laws for: " ++ batchName) $
    traverse_ (uncurry it) tests
  
  
  instance (EqProp ext, EqProp meta, EqProp s, EqProp jdg) => EqProp (Proof s meta jdg ext) where
  
  instance (MonadExtract meta ext err s m, EqProp (m (Either [err] [Proof s meta a ext])), Arbitrary s)
        => EqProp (ProofStateT ext ext err s m a) where
    (=-=) a b = property $ do
      s <- arbitrary
      pure $ ((=-=) `on` proofs s) a b
  
  instance ( MonadExtract meta ext err s m
           , Arbitrary jdg
           , EqProp (m (Either [err] [Proof s meta jdg ext]))
           , Show s
           , Arbitrary s
           , Show jdg
           )
        => EqProp (TacticT jdg ext err s m a) where
    (=-=) = (=-=) `on` runTacticT . (() <$)
  
  instance ( Arbitrary jdg
           , EqProp (m (Either [err] [Proof s meta jdg ext]))
           , MonadExtract meta ext err s m
           , Arbitrary s
           , Show s , Show jdg
           )
        => EqProp (RuleT jdg ext err s m ext) where
    (=-=) = (=-=) `on` rule . const
  
  instance MonadExtract Int Int String Int Identity where
    hole = do
      i <- get
      modify (+1)
      pure (i, 0)
    unsolvableHole _ = do
      i <- get
      modify (+1)
      pure (i, 0)
  
  instance ( CoArbitrary ext'
           , Arbitrary ext
           , CoArbitrary err
           , Arbitrary err
           , Arbitrary a
           , Arbitrary (m (ProofStateT ext' ext err s m a))
           , Arbitrary (m err)
           , CoArbitrary s
           , Arbitrary s
           )
        => Arbitrary (ProofStateT ext' ext err s m a) where
    arbitrary = getSize >>= \case
      n | n <= 1 -> oneof small
      _ -> oneof $
        [ Subgoal    <$> decayArbitrary 2 <*> decayArbitrary 2
        , Effect     <$> arbitrary
        , Interleave <$> decayArbitrary 2 <*> decayArbitrary 2
        , Alt        <$> decayArbitrary 2 <*> decayArbitrary 2
        , Stateful   <$> arbitrary
        , Failure    <$> arbitrary <*> decayArbitrary 2
        , Handle     <$> decayArbitrary 2 <*> arbitrary
        ] ++ small
      where
        small =
          [ pure Empty
          , Axiom   <$> arbitrary
          ]
    shrink = genericShrink
  
  instance (Arbitrary (m (a, s)), CoArbitrary s) => Arbitrary (StateT s m a) where
    arbitrary = StateT <$> arbitrary
  
  instance ( CoArbitrary jdg
           , Arbitrary a
           , Arbitrary ext
           , CoArbitrary err
           , Arbitrary err
           , CoArbitrary ext
           , Arbitrary jdg
           , Arbitrary (m (ProofStateT ext ext err s m (a, jdg)))
           , Arbitrary (m err)
           , CoArbitrary s
           , Arbitrary s
           )
        => Arbitrary (TacticT jdg ext err s m a) where
    arbitrary = fmap (TacticT . StateT) arbitrary
    shrink = genericShrink
  
  instance ( Arbitrary a
           , CoArbitrary err
           , Arbitrary err
           , CoArbitrary ext
           , Arbitrary jdg
           , Arbitrary (m (ProofStateT ext a err s m jdg))
           , Arbitrary (m err)
           , CoArbitrary s
           , Arbitrary s
           )
        => Arbitrary (RuleT jdg ext err s m a) where
    arbitrary = fmap RuleT arbitrary
    shrink = genericShrink
  
  decayArbitrary :: Arbitrary a => Int -> Gen a
  decayArbitrary n = scale (`div` n) arbitrary
  
  type ProofStateTest = ProofStateT Int Int String Int Identity
  type RuleTest = RuleT Int Int String Int Identity
  type TacticTest = TacticT (Sum Int) Int String Int Identity
  
  propertyTests :: Spec
  propertyTests = do
    describe "ProofStateT" $ do
      testBatch $ functor     (undefined :: ProofStateTest (Int, Int, Int))
      testBatch $ applicative (undefined :: ProofStateTest (Int, Int, Int))
      testBatch $ alternative (undefined :: ProofStateTest Int)
      testBatch $ monad       (undefined :: ProofStateTest (Int, Int, Int))
      testBatch $ monadPlus   (undefined :: ProofStateTest (Int, Int))
      testBatch $ monadState  (undefined :: ProofStateTest (Int, Int))
      it "distrib put over <|>" $ property $ distribPut (undefined :: ProofStateTest Int)
    describe "RuleT" $ do
      testBatch $ functor     (undefined :: RuleTest (Int, Int, Int))
      testBatch $ applicative (undefined :: RuleTest (Int, Int, Int))
      testBatch $ alternative (undefined :: RuleTest Int)
      testBatch $ monad       (undefined :: RuleTest (Int, Int, Int))
    describe "TacticT" $ do
      testBatch $ functor     (undefined :: TacticTest ((), (), ()))
      testBatch $ applicative (undefined :: TacticTest ((), (), ()))
      testBatch $ alternative (undefined :: TacticTest ())
      testBatch $ monad       (undefined :: TacticTest ((), (), ()))
      testBatch $ monadPlus   (undefined :: TacticTest ((), ()))
      testBatch $ monadState  (undefined :: TacticTest ((), ()))
      it "interleave - mzero" $ property $ interleaveMZero (undefined :: TacticTest Int)
      it "interleave - mplus" $ property $ interleaveMPlus (undefined :: TacticTest Int)
      it "distrib put over <|>" $ property $ distribPut (undefined :: TacticTest ())
      -- it "constant peek" $ property $ peekConst (undefined :: TacticTest ())
  
  leftAltBind
      :: forall m a b
      . (EqProp (m b), Monad m, Alternative m)
      => m a -> m a -> (a -> m b)
      -> Property
  leftAltBind m1 m2 f =
    ((m1 <|> m2) >>= f) =-= ((m1 >>= f) <|> (m2 >>= f))
  
  rightAltBind
      :: forall m a
      . (EqProp (m a), Monad m, Alternative m)
      => m () -> m a -> m a
      -> Property
  rightAltBind m1 m2 m3 =
    (m1 >> (m2 <|> m3)) =-= ((m1 >> m2) <|> (m1 >> m3))
  
  interleaveMZero
      :: forall m a meta jdg ext err s
       . (MonadExtract meta ext err s m
         , EqProp (m (Either [err] [Proof s meta jdg ext]))
         , Show s , Show jdg
         , Arbitrary jdg, Arbitrary s)
      => TacticT jdg ext err s m a  -- ^ proxy
      -> TacticT jdg ext err s m a
      -> Property
  interleaveMZero _ m =
      (mzero <%> m) =-= m
  
  interleaveMPlus
      :: forall m a meta jdg ext err s
       . (MonadExtract meta ext err s m
         , EqProp (m (Either [err] [Proof s meta jdg ext]))
         , Show s , Show jdg
         , Arbitrary jdg, Arbitrary s)
      => TacticT jdg ext err s m a  -- ^ proxy
      -> a
      -> TacticT jdg ext err s m a
      -> TacticT jdg ext err s m a
      -> Property
  interleaveMPlus _ a m1 m2 =
      ((pure a <|> m1) <%> m2) =-= (pure a <|> (m2 <%> m1))
  
  distribPut
      :: forall s m a
       . ( MonadState s m
         , Alternative m
         , EqProp (m a)
         , Arbitrary (m a)
         , Arbitrary s
         , Show s
         , Show (m a)
         )
      => m a -> Property
  distribPut _ = property $ do
    s <- arbitrary @s
    m1 <- arbitrary @(m a)
    m2 <- arbitrary @(m a)
    pure $
      counterexample (show s) $
      counterexample (show m1) $
      counterexample (show m2) $
        (put s >> (m1 <|> m2)) =-= ((put s >> m1) <|> (put s >> m2))
  
  -- peekConst
  --     :: forall m jdg ext err s
  --      . (MonadExtract ext err m
  --        , EqProp (m [Either err (Proof s jdg ext)])
  --        , Show s , Show jdg
  --        , Arbitrary jdg, Arbitrary s)
  --     => TacticT jdg ext err s m ()  -- ^ proxy
  --     -> TacticT jdg ext err s m ()
  --     -> TacticT jdg ext err s m ()
  --     -> Property
  -- peekConst _ t t' =
  --     peek t (const t') =-= (t' >> t)
  