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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
{-# OPTIONS_GHC -fno-warn-deprecations #-}
{-# OPTIONS_GHC -fno-warn-unused-imports #-}
import Data.Functor
import Data.Maybe
import Data.Typeable
import Test.QuickCheck.All (quickCheckAll)
import Test.QuickCheck hiding ((===))
import Test.Feat
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NEL
import Data.Monoid.Action
import Data.Semigroup
import Data.Tree.DUAL
data DUALTreeExpr d u a l =
EEmpty
| ELeaf u l
| ELeafU u
| EConcat (NonEmpty (DUALTreeExpr d u a l))
| EAct d (DUALTreeExpr d u a l)
| EAnnot a (DUALTreeExpr d u a l)
deriving (Show, Typeable)
deriveEnumerable ''NonEmpty
deriveEnumerable ''DUALTreeExpr
buildTree :: (Semigroup u, Semigroup d, Action d u)
=> DUALTreeExpr d u a l -> DUALTree d u a l
buildTree EEmpty = empty
buildTree (ELeaf u l) = leaf u l
buildTree (ELeafU u) = leafU u
buildTree (EConcat ts) = sconcat (NEL.map buildTree ts)
buildTree (EAct d t) = applyD d (buildTree t)
buildTree (EAnnot a t) = annot a (buildTree t)
-- buildTree' :: DUALTreeExpr D U () Bool -> DUALTree D U () Bool
-- buildTree' = buildTree
instance Num a => Action (Product a) (Sum a) where
act (Product p) (Sum s) = Sum (p * s)
type U = Sum Int
type D = Product Int
deriving instance Typeable Sum
deriving instance Typeable Product
deriveEnumerable ''Sum
deriveEnumerable ''Product
type T = DUALTree D U Bool Bool
instance Arbitrary T where
arbitrary = buildTree <$> sized uniform
prop_leaf_u :: U -> Bool
prop_leaf_u u = getU (leaf u ()) == Just u
prop_leafU_u :: U -> Bool
prop_leafU_u u = getU (leafU u) == Just u
prop_applyUpre :: U -> T -> Bool
prop_applyUpre u t = getU (applyUpre u t) == Just (u <> fromMaybe mempty (getU t))
prop_applyUpost :: U -> T -> Bool
prop_applyUpost u t = getU (applyUpost u t) == Just (fromMaybe mempty (getU t) <> u)
--------------------------------------------------
-- Monoid laws
--------------------------------------------------
prop_mempty_idL :: T -> Bool
prop_mempty_idL t = mempty <> t == t
prop_mempty_idR :: T -> Bool
prop_mempty_idR t = t <> mempty == t
infix 4 ===
t1 === t2 = flatten t1 == flatten t2
-- mappend is associative up to flattening.
prop_mappend_assoc :: T -> T -> T -> Bool
prop_mappend_assoc t1 t2 t3 = (t1 <> t2) <> t3 === t1 <> (t2 <> t3)
--------------------------------------------------
-- Action laws
--------------------------------------------------
prop_mempty_act :: T -> Bool
prop_mempty_act t = applyD mempty t === t
prop_mappend_act :: D -> D -> T -> Bool
prop_mappend_act d1 d2 t = applyD d1 (applyD d2 t) == applyD (d1 <> d2) t
prop_act_mempty :: D -> Bool
prop_act_mempty d = applyD d (mempty :: T) == mempty
prop_act_mappend :: D -> T -> T -> Bool
prop_act_mappend d t1 t2 = applyD d (t1 <> t2) === applyD d t1 <> applyD d t2
return []
main = $quickCheckAll
|
