{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications    #-}

{-# OPTIONS_GHC -Wno-unused-top-binds #-}
{-# OPTIONS_GHC -Wno-unused-imports #-}

module Property
    ( propertyTests
    )
where

import           Data.Either             (either, isRight)
import qualified Data.Graph.Inductive    as G
import           Data.Text               (Text)
import           Hedgehog                (Gen, Property, (===))
import qualified Hedgehog                as Hog
import           Hedgehog.Function       (Arg, Vary)
import qualified Hedgehog.Function       as Hog
import qualified Hedgehog.Gen            as Hog
import qualified Hedgehog.Range          as Hog
import           Parser                  (parserTests)
import           Test.Tasty
import           Test.Tasty.Hedgehog
import           Text.Parsec
import           VeriFuzz
import           VeriFuzz.Result
import           VeriFuzz.Verilog.Lex
import           VeriFuzz.Verilog.Parser

randomDAG' :: Gen Circuit
randomDAG' = Hog.resize 30 randomDAG

acyclicGraph :: Property
acyclicGraph = Hog.property $ do
    xs <- Hog.forAllWith (const "") randomDAG'
    Hog.assert $ simp xs
  where
    simp g =
        (== G.noNodes (getCircuit g))
            . sum
            . fmap length
            . G.scc
            . getCircuit
            $ g

type GenFunctor f a b c =
    ( Functor f
    , Show (f a)
    , Show a, Arg a, Vary a
    , Show b, Arg b, Vary b
    , Show c
    , Eq (f c)
    , Show (f c)
    )

mapCompose
    :: forall f a b c
     . GenFunctor f a b c
    => (forall x . Gen x -> Gen (f x))
    -> Gen a
    -> Gen b
    -> Gen c
    -> Property
mapCompose genF genA genB genC = Hog.property $ do
    g  <- Hog.forAllFn $ Hog.fn @a genB
    f  <- Hog.forAllFn $ Hog.fn @b genC
    xs <- Hog.forAll $ genF genA
    fmap (f . g) xs === fmap f (fmap g xs)

propertyResultInterrupted :: Property
propertyResultInterrupted = do
    mapCompose genResult
               (Hog.int (Hog.linear 0 100))
               (Hog.int (Hog.linear 0 100))
               (Hog.int (Hog.linear 0 100))
  where
    genResult :: Gen a -> Gen (Result Text a)
    genResult a = Hog.choice
        [Pass <$> a, Fail <$> Hog.text (Hog.linear 1 100) Hog.unicode]

propertyTests :: TestTree
propertyTests = testGroup
    "Property Tests"
    [ testProperty "acyclic graph generation check" acyclicGraph
    , testProperty "fmap for Result"                propertyResultInterrupted
    , parserTests
    ]