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
|
{-# 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
]
|
