1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
{-# 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
simpleGraph :: Property
simpleGraph = Hog.property $ do
xs <- Hog.forAllWith (const "") randomDAG'
Hog.assert $ simp xs
where simp = G.isSimple . getCircuit
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 "simple graph generation check" simpleGraph
, testProperty "fmap for Result" propertyResultInterrupted
, parserTests
]
|