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
83
84
85
86
87
88
89
90
91
92
93
94
95
96
|
{-# 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
]
|
