@@ -27,59 +27,78 @@ instance showList :: Show a => Show (List a) where
27
27
show x = GShow .genericShow x
28
28
29
29
data SimpleBounded = A | B | C | D
30
+
30
31
derive instance genericSimpleBounded :: G.Generic SimpleBounded _
31
32
instance eqSimpleBounded :: Eq SimpleBounded where
32
33
eq x y = GEq .genericEq x y
34
+
33
35
instance ordSimpleBounded :: Ord SimpleBounded where
34
36
compare x y = GOrd .genericCompare x y
37
+
35
38
instance showSimpleBounded :: Show SimpleBounded where
36
39
show x = GShow .genericShow x
40
+
37
41
instance boundedSimpleBounded :: Bounded SimpleBounded where
38
42
bottom = GBounded .genericBottom
39
43
top = GBounded .genericTop
40
44
41
45
data Option a = None | Some a
46
+
42
47
derive instance genericOption :: G.Generic (Option a ) _
43
48
instance eqOption :: Eq a => Eq (Option a ) where
44
49
eq x y = GEq .genericEq x y
50
+
45
51
instance ordOption :: Ord a => Ord (Option a ) where
46
52
compare x y = GOrd .genericCompare x y
53
+
47
54
instance showOption :: Show a => Show (Option a ) where
48
55
show x = GShow .genericShow x
56
+
49
57
instance boundedOption :: Bounded a => Bounded (Option a ) where
50
58
bottom = GBounded .genericBottom
51
59
top = GBounded .genericTop
52
60
53
61
data Bit = Zero | One
62
+
54
63
derive instance genericBit :: G.Generic Bit _
55
64
instance eqBit :: Eq Bit where
56
65
eq x y = GEq .genericEq x y
66
+
57
67
instance ordBit :: Ord Bit where
58
68
compare x y = GOrd .genericCompare x y
69
+
59
70
instance showBit :: Show Bit where
60
71
show x = GShow .genericShow x
72
+
61
73
instance boundedBit :: Bounded Bit where
62
74
bottom = GBounded .genericBottom
63
75
top = GBounded .genericTop
64
76
65
77
data Pair a b = Pair a b
78
+
66
79
derive instance genericPair :: G.Generic (Pair a b ) _
67
80
instance eqPair :: (Eq a , Eq b ) => Eq (Pair a b ) where
68
81
eq = GEq .genericEq
82
+
69
83
instance ordPair :: (Ord a , Ord b ) => Ord (Pair a b ) where
70
84
compare = GOrd .genericCompare
85
+
71
86
instance showPair :: (Show a , Show b ) => Show (Pair a b ) where
72
87
show = GShow .genericShow
88
+
73
89
instance boundedPair :: (Bounded a , Bounded b ) => Bounded (Pair a b ) where
74
90
bottom = GBounded .genericBottom
75
91
top = GBounded .genericTop
92
+
76
93
instance semiringPair :: (Semiring a , Semiring b ) => Semiring (Pair a b ) where
77
94
add (Pair x1 y1) (Pair x2 y2) = Pair (add x1 x2) (add y1 y2)
78
95
one = Pair one one
79
96
mul (Pair x1 y1) (Pair x2 y2) = Pair (mul x1 x2) (mul y1 y2)
80
97
zero = Pair zero zero
98
+
81
99
instance ringPair :: (Ring a , Ring b ) => Ring (Pair a b ) where
82
100
sub (Pair x1 y1) (Pair x2 y2) = Pair (sub x1 x2) (sub y1 y2)
101
+
83
102
instance heytingAlgebraPair :: (HeytingAlgebra a , HeytingAlgebra b ) => HeytingAlgebra (Pair a b ) where
84
103
tt = Pair tt tt
85
104
ff = Pair ff ff
@@ -88,26 +107,33 @@ instance heytingAlgebraPair :: (HeytingAlgebra a, HeytingAlgebra b) => HeytingAl
88
107
disj (Pair x1 y1) (Pair x2 y2) = Pair (disj x1 x2) (disj y1 y2)
89
108
not (Pair x y) = Pair (not x) (not y)
90
109
91
- data A1 = A1 (Pair (Pair Int { a :: Int } ) { a :: Int } )
110
+ data A1 = A1 (Pair (Pair Int { a :: Int } ) { a :: Int } )
111
+
92
112
derive instance genericA1 :: G.Generic A1 _
93
113
instance eqA1 :: Eq A1 where
94
114
eq a = GEq .genericEq a
115
+
95
116
instance showA1 :: Show A1 where
96
117
show a = GShow .genericShow a
118
+
97
119
instance semiringA1 :: Semiring A1 where
98
120
zero = GSemiring .genericZero
99
121
one = GSemiring .genericOne
100
122
add x y = GSemiring .genericAdd x y
101
123
mul x y = GSemiring .genericMul x y
124
+
102
125
instance ringA1 :: Ring A1 where
103
126
sub x y = GRing .genericSub x y
104
127
105
- data B1 = B1 (Pair (Pair Boolean { a :: Boolean } ) { a :: Boolean } )
128
+ data B1 = B1 (Pair (Pair Boolean { a :: Boolean } ) { a :: Boolean } )
129
+
106
130
derive instance genericB1 :: G.Generic B1 _
107
131
instance eqB1 :: Eq B1 where
108
132
eq a = GEq .genericEq a
133
+
109
134
instance showB1 :: Show B1 where
110
135
show a = GShow .genericShow a
136
+
111
137
instance heytingAlgebraB1 :: HeytingAlgebra B1 where
112
138
ff = GHeytingAlgebra .genericFF
113
139
tt = GHeytingAlgebra .genericTT
@@ -166,31 +192,31 @@ testGenericRep = do
166
192
top == (Pair One D :: Pair Bit SimpleBounded )
167
193
168
194
assert " Checking zero" $
169
- (zero :: A1 ) == A1 (Pair (Pair 0 {a: 0 }) {a: 0 })
195
+ (zero :: A1 ) == A1 (Pair (Pair 0 { a: 0 }) { a: 0 })
170
196
171
197
assert " Checking one" $
172
- (one :: A1 ) == A1 (Pair (Pair 1 {a: 1 }) {a: 1 })
198
+ (one :: A1 ) == A1 (Pair (Pair 1 { a: 1 }) { a: 1 })
173
199
174
200
assert " Checking add" $
175
- A1 (Pair (Pair 100 {a: 10 }) {a: 20 }) + A1 (Pair (Pair 50 {a: 30 }) {a: 40 }) == A1 (Pair (Pair 150 {a: 40 }) {a: 60 })
201
+ A1 (Pair (Pair 100 { a: 10 }) { a: 20 }) + A1 (Pair (Pair 50 { a: 30 }) { a: 40 }) == A1 (Pair (Pair 150 { a: 40 }) { a: 60 })
176
202
177
203
assert " Checking mul" $
178
- A1 (Pair (Pair 100 {a: 10 }) {a: 20 }) * A1 (Pair (Pair 50 {a: 30 }) {a: 40 }) == A1 (Pair (Pair 5000 {a: 300 }) {a: 800 })
204
+ A1 (Pair (Pair 100 { a: 10 }) { a: 20 }) * A1 (Pair (Pair 50 { a: 30 }) { a: 40 }) == A1 (Pair (Pair 5000 { a: 300 }) { a: 800 })
179
205
180
206
assert " Checking sub" $
181
- A1 (Pair (Pair 100 {a: 10 }) {a: 20 }) - A1 (Pair (Pair 50 {a: 30 }) {a: 40 }) == A1 (Pair (Pair 50 {a: -20 }) {a: -20 })
207
+ A1 (Pair (Pair 100 { a: 10 }) { a: 20 }) - A1 (Pair (Pair 50 { a: 30 }) { a: 40 }) == A1 (Pair (Pair 50 { a: -20 }) { a: -20 })
182
208
183
209
assert " Checking ff" $
184
- (ff :: B1 ) == B1 (Pair (Pair false {a: false }) {a: false })
210
+ (ff :: B1 ) == B1 (Pair (Pair false { a: false }) { a: false })
185
211
186
212
assert " Checking tt" $
187
- (tt :: B1 ) == B1 (Pair (Pair true {a: true }) {a: true })
213
+ (tt :: B1 ) == B1 (Pair (Pair true { a: true }) { a: true })
188
214
189
215
assert " Checking conj" $
190
- (B1 (Pair (Pair true {a: false }) {a: true }) && B1 (Pair (Pair false {a: false }) {a: true })) == B1 (Pair (Pair false { a: false }) { a: true })
216
+ (B1 (Pair (Pair true { a: false }) { a: true }) && B1 (Pair (Pair false { a: false }) { a: true })) == B1 (Pair (Pair false { a: false }) { a: true })
191
217
192
218
assert " Checking disj" $
193
- (B1 (Pair (Pair true {a: false }) {a: true }) || B1 (Pair (Pair false {a: false }) {a: true })) == B1 (Pair (Pair true { a: false }) { a: true })
219
+ (B1 (Pair (Pair true { a: false }) { a: true }) || B1 (Pair (Pair false { a: false }) { a: true })) == B1 (Pair (Pair true { a: false }) { a: true })
194
220
195
221
assert " Checking not" $
196
- not B1 (Pair (Pair true {a: false }) {a: true }) == B1 (Pair (Pair false {a: true }) {a: false })
222
+ not B1 (Pair (Pair true { a: false }) { a: true }) == B1 (Pair (Pair false { a: true }) { a: false })
0 commit comments