Skip to content

Commit 1407e08

Browse files
authored
Add Test.Injection (#1865)
* Add Test.Injection * Test.Injection: Export module Hedgehog * Test Injection instances of SomeVariableName
1 parent 7e44a8b commit 1407e08

File tree

2 files changed

+66
-0
lines changed

2 files changed

+66
-0
lines changed

kore/test/Test/Injection.hs

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
{-# LANGUAGE AllowAmbiguousTypes #-}
2+
3+
module Test.Injection
4+
( hpropInjection
5+
, hprop_Injection_Maybe
6+
, hprop_Injection_Dynamic
7+
-- * Re-exports
8+
, module Hedgehog
9+
, Int8
10+
, genInt8
11+
) where
12+
13+
import Prelude
14+
15+
import Hedgehog hiding
16+
( test
17+
)
18+
import qualified Hedgehog.Gen as Gen
19+
20+
import Data.Dynamic
21+
( Dynamic
22+
)
23+
import Data.Int
24+
( Int8
25+
)
26+
27+
import Injection
28+
29+
{- | Create a property test for an 'Injection' instance.
30+
31+
Only the "left identity" property is tested; as long as the instance is not
32+
partial, this property implies all others.
33+
34+
Note: The @into@ type parameter *must* be specified by type application.
35+
36+
-}
37+
hpropInjection
38+
:: forall into from
39+
. (Eq from, Show from)
40+
=> Injection into from
41+
=> Gen from -> Property
42+
hpropInjection genFrom =
43+
property $ do
44+
from <- forAll genFrom
45+
let into = inject @into from
46+
retract into === Just from
47+
48+
genInt8 :: MonadGen m => m Int8
49+
genInt8 = Gen.enumBounded
50+
51+
hprop_Injection_Maybe :: Property
52+
hprop_Injection_Maybe = hpropInjection @(Maybe Int8) genInt8
53+
54+
hprop_Injection_Dynamic :: Property
55+
hprop_Injection_Dynamic = hpropInjection @Dynamic genInt8

kore/test/Test/Kore/Syntax/Variable.hs

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
11
module Test.Kore.Syntax.Variable
22
( test_isSetVariable
33
, test_isElementVariable
4+
, hprop_instance_Injection_SomeVariableName_ElementVariableName
5+
, hprop_instance_Injection_SomeVariableName_SetVariableName
46
-- * Re-exports
57
, module Kore.Syntax.Variable
68
) where
@@ -11,6 +13,7 @@ import Test.Tasty
1113

1214
import Kore.Syntax.Variable
1315

16+
import Test.Injection
1417
import Test.Kore
1518
( testId
1619
)
@@ -54,3 +57,11 @@ test_isElementVariable =
5457
testCase name $ do
5558
let actual = isElementVariable input
5659
assertEqual "" expect actual
60+
61+
hprop_instance_Injection_SomeVariableName_ElementVariableName :: Property
62+
hprop_instance_Injection_SomeVariableName_ElementVariableName =
63+
hpropInjection @(SomeVariableName Int8) (ElementVariableName <$> genInt8)
64+
65+
hprop_instance_Injection_SomeVariableName_SetVariableName :: Property
66+
hprop_instance_Injection_SomeVariableName_SetVariableName =
67+
hpropInjection @(SomeVariableName Int8) (SetVariableName <$> genInt8)

0 commit comments

Comments
 (0)