Skip to content
This repository was archived by the owner on Mar 25, 2021. It is now read-only.

Commit 0294627

Browse files
hdgarroodhdgarrood
authored
Merge branch 'master' into add-guide
2 parents fc72865 + 3bd3379 commit 0294627

File tree

5 files changed

+213
-2
lines changed

5 files changed

+213
-2
lines changed

‎README.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,5 +81,6 @@ API documentation is [published on Pursuit](http://pursuit.purescript.org/packag
8181

8282
## Related libraries
8383

84+
* The [documentation for the simple-json library](https://purescript-simple-json.readthedocs.io/en/latest/generics-rep.html) includes a tutorial for using this library.
8485
* Generic deriving of codecs for `Foreign` values: [purescript-foreign-generic](https://github.com/paf31/purescript-foreign-generic)
8586
* Generic deriving of codecs for purescript-argonaut: [purescript-argonaut-generic](https://github.com/purescript-contrib/purescript-argonaut-generic)

‎src/Data/Generic/Rep/HeytingAlgebra.purs‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
module Data.Generic.Rep.HeytingAlgebra where
2+
3+
import Prelude
4+
5+
import Data.Generic.Rep (class Generic, Argument(..), Constructor(..), NoArguments(..), Product(..), from, to)
6+
import Data.HeytingAlgebra (ff, implies, tt)
7+
8+
class GenericHeytingAlgebra a where
9+
genericFF' :: a
10+
genericTT' :: a
11+
genericImplies' :: a -> a -> a
12+
genericConj' :: a -> a -> a
13+
genericDisj' :: a -> a -> a
14+
genericNot' :: a -> a
15+
16+
instance genericHeytingAlgebraNoArguments :: GenericHeytingAlgebra NoArguments where
17+
genericFF' = NoArguments
18+
genericTT' = NoArguments
19+
genericImplies' _ _ = NoArguments
20+
genericConj' _ _ = NoArguments
21+
genericDisj' _ _ = NoArguments
22+
genericNot' _ = NoArguments
23+
24+
instance genericHeytingAlgebraArgument :: HeytingAlgebra a => GenericHeytingAlgebra (Argument a) where
25+
genericFF' = Argument ff
26+
genericTT' = Argument tt
27+
genericImplies' (Argument x) (Argument y) = Argument (implies x y)
28+
genericConj' (Argument x) (Argument y) = Argument (conj x y)
29+
genericDisj' (Argument x) (Argument y) = Argument (disj x y)
30+
genericNot' (Argument x) = Argument (not x)
31+
32+
instance genericHeytingAlgebraProduct :: (GenericHeytingAlgebra a, GenericHeytingAlgebra b) => GenericHeytingAlgebra (Product a b) where
33+
genericFF' = Product genericFF' genericFF'
34+
genericTT' = Product genericTT' genericTT'
35+
genericImplies' (Product a1 b1) (Product a2 b2) = Product (genericImplies' a1 a2) (genericImplies' b1 b2)
36+
genericConj' (Product a1 b1) (Product a2 b2) = Product (genericConj' a1 a2) (genericConj' b1 b2)
37+
genericDisj' (Product a1 b1) (Product a2 b2) = Product (genericDisj' a1 a2) (genericDisj' b1 b2)
38+
genericNot' (Product a b) = Product (genericNot' a) (genericNot' b)
39+
40+
instance genericHeytingAlgebraConstructor :: GenericHeytingAlgebra a => GenericHeytingAlgebra (Constructor name a) where
41+
genericFF' = Constructor genericFF'
42+
genericTT' = Constructor genericTT'
43+
genericImplies' (Constructor a1) (Constructor a2) = Constructor (genericImplies' a1 a2)
44+
genericConj' (Constructor a1) (Constructor a2) = Constructor (genericConj' a1 a2)
45+
genericDisj' (Constructor a1) (Constructor a2) = Constructor (genericDisj' a1 a2)
46+
genericNot' (Constructor a) = Constructor (genericNot' a)
47+
48+
-- | A `Generic` implementation of the `ff` member from the `HeytingAlgebra` type class.
49+
genericFF :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a
50+
genericFF = to genericFF'
51+
52+
-- | A `Generic` implementation of the `tt` member from the `HeytingAlgebra` type class.
53+
genericTT :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a
54+
genericTT = to genericTT'
55+
56+
-- | A `Generic` implementation of the `implies` member from the `HeytingAlgebra` type class.
57+
genericImplies :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a -> a -> a
58+
genericImplies x y = to $ from x `genericImplies'` from y
59+
60+
-- | A `Generic` implementation of the `conj` member from the `HeytingAlgebra` type class.
61+
genericConj :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a -> a -> a
62+
genericConj x y = to $ from x `genericConj'` from y
63+
64+
-- | A `Generic` implementation of the `disj` member from the `HeytingAlgebra` type class.
65+
genericDisj :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a -> a -> a
66+
genericDisj x y = to $ from x `genericDisj'` from y
67+
68+
-- | A `Generic` implementation of the `not` member from the `HeytingAlgebra` type class.
69+
genericNot :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a -> a
70+
genericNot x = to $ genericNot' (from x)

‎src/Data/Generic/Rep/Ring.purs‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
module Data.Generic.Rep.Ring where
2+
3+
import Prelude
4+
5+
import Data.Generic.Rep (class Generic, Argument(..), Constructor(..), NoArguments(..), Product(..), from, to)
6+
7+
class GenericRing a where
8+
genericSub' :: a -> a -> a
9+
10+
instance genericRingNoArguments :: GenericRing NoArguments where
11+
genericSub' _ _ = NoArguments
12+
13+
instance genericRingArgument :: Ring a => GenericRing (Argument a) where
14+
genericSub' (Argument x) (Argument y) = Argument (sub x y)
15+
16+
instance genericRingProduct :: (GenericRing a, GenericRing b) => GenericRing (Product a b) where
17+
genericSub' (Product a1 b1) (Product a2 b2) = Product (genericSub' a1 a2) (genericSub' b1 b2)
18+
19+
instance genericRingConstructor :: GenericRing a => GenericRing (Constructor name a) where
20+
genericSub' (Constructor a1) (Constructor a2) = Constructor (genericSub' a1 a2)
21+
22+
-- | A `Generic` implementation of the `sub` member from the `Ring` type class.
23+
genericSub :: forall a rep. Generic a rep => GenericRing rep => a -> a -> a
24+
genericSub x y = to $ from x `genericSub'` from y

‎src/Data/Generic/Rep/Semiring.purs‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
module Data.Generic.Rep.Semiring where
2+
3+
import Prelude
4+
5+
import Data.Generic.Rep (class Generic, Argument(..), Constructor(..), NoArguments(..), Product(..), from, to)
6+
7+
class GenericSemiring a where
8+
genericAdd' :: a -> a -> a
9+
genericZero' :: a
10+
genericMul' :: a -> a -> a
11+
genericOne' :: a
12+
13+
instance genericSemiringNoArguments :: GenericSemiring NoArguments where
14+
genericAdd' _ _ = NoArguments
15+
genericZero' = NoArguments
16+
genericMul' _ _ = NoArguments
17+
genericOne' = NoArguments
18+
19+
instance genericSemiringArgument :: Semiring a => GenericSemiring (Argument a) where
20+
genericAdd' (Argument x) (Argument y) = Argument (add x y)
21+
genericZero' = Argument zero
22+
genericMul' (Argument x) (Argument y) = Argument (mul x y)
23+
genericOne' = Argument one
24+
25+
instance genericSemiringProduct :: (GenericSemiring a, GenericSemiring b) => GenericSemiring (Product a b) where
26+
genericAdd' (Product a1 b1) (Product a2 b2) = Product (genericAdd' a1 a2) (genericAdd' b1 b2)
27+
genericZero' = Product genericZero' genericZero'
28+
genericMul' (Product a1 b1) (Product a2 b2) = Product (genericMul' a1 a2) (genericMul' b1 b2)
29+
genericOne' = Product genericOne' genericOne'
30+
31+
instance genericSemiringConstructor :: GenericSemiring a => GenericSemiring (Constructor name a) where
32+
genericAdd' (Constructor a1) (Constructor a2) = Constructor (genericAdd' a1 a2)
33+
genericZero' = Constructor genericZero'
34+
genericMul' (Constructor a1) (Constructor a2) = Constructor (genericMul' a1 a2)
35+
genericOne' = Constructor genericOne'
36+
37+
-- | A `Generic` implementation of the `zero` member from the `Semiring` type class.
38+
genericZero :: forall a rep. Generic a rep => GenericSemiring rep => a
39+
genericZero = to genericZero'
40+
41+
-- | A `Generic` implementation of the `one` member from the `Semiring` type class.
42+
genericOne :: forall a rep. Generic a rep => GenericSemiring rep => a
43+
genericOne = to genericOne'
44+
45+
-- | A `Generic` implementation of the `add` member from the `Semiring` type class.
46+
genericAdd :: forall a rep. Generic a rep => GenericSemiring rep => a -> a -> a
47+
genericAdd x y = to $ from x `genericAdd'` from y
48+
49+
-- | A `Generic` implementation of the `mul` member from the `Semiring` type class.
50+
genericMul :: forall a rep. Generic a rep => GenericSemiring rep => a -> a -> a
51+
genericMul x y = to $ from x `genericMul'` from y

‎test/Main.purs‎

Lines changed: 67 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,16 +2,21 @@ module Test.Main where
22

33
import Prelude
44

5-
import Effect (Effect)
6-
import Effect.Console (log, logShow)
75
import Data.Enum (class BoundedEnum, class Enum, Cardinality(..), cardinality, fromEnum, pred, succ, toEnum, enumFromTo)
86
import Data.Generic.Rep as G
97
import Data.Generic.Rep.Bounded as GBounded
108
import Data.Generic.Rep.Enum as GEnum
119
import Data.Generic.Rep.Eq as GEq
10+
import Data.Generic.Rep.HeytingAlgebra as GHeytingAlgebra
1211
import Data.Generic.Rep.Ord as GOrd
12+
import Data.Generic.Rep.Ring as GRing
13+
import Data.Generic.Rep.Semiring as GSemiring
1314
import Data.Generic.Rep.Show as GShow
15+
import Data.HeytingAlgebra (ff, tt)
1416
import Data.Maybe (Maybe(..))
17+
import Data.Tuple (Tuple(..))
18+
import Effect (Effect)
19+
import Effect.Console (log, logShow)
1520
import Test.Assert (assert)
1621

1722
data List a = Nil | Cons { head :: a, tail :: List a }
@@ -103,6 +108,36 @@ instance boundedEnumPair :: (BoundedEnum a, BoundedEnum b) => BoundedEnum (Pair
103108
toEnum = GEnum.genericToEnum
104109
fromEnum = GEnum.genericFromEnum
105110

111+
data A1 = A1 (Tuple (Tuple Int {a :: Int}) {a :: Int})
112+
derive instance genericA1 :: G.Generic A1 _
113+
instance eqA1 :: Eq A1 where
114+
eq a = GEq.genericEq a
115+
instance showA1 :: Show A1 where
116+
show a = GShow.genericShow a
117+
instance semiringA1 :: Semiring A1 where
118+
zero = GSemiring.genericZero
119+
one = GSemiring.genericOne
120+
add x y = GSemiring.genericAdd x y
121+
mul x y = GSemiring.genericMul x y
122+
instance ringA1 :: Ring A1 where
123+
sub x y = GRing.genericSub x y
124+
125+
data B1 = B1 (Tuple (Tuple Boolean {a :: Boolean}) {a :: Boolean})
126+
derive instance genericB1 :: G.Generic B1 _
127+
instance eqB1 :: Eq B1 where
128+
eq a = GEq.genericEq a
129+
instance showB1 :: Show B1 where
130+
show a = GShow.genericShow a
131+
instance heytingAlgebraB1 :: HeytingAlgebra B1 where
132+
ff = GHeytingAlgebra.genericFF
133+
tt = GHeytingAlgebra.genericTT
134+
implies x y = GHeytingAlgebra.genericImplies x y
135+
conj x y = GHeytingAlgebra.genericConj x y
136+
disj x y = GHeytingAlgebra.genericDisj x y
137+
not x = GHeytingAlgebra.genericNot x
138+
139+
instance booleanAlgebraB1 :: BooleanAlgebra B1
140+
106141
main :: Effect Unit
107142
main = do
108143
logShow (cons 1 (cons 2 Nil))
@@ -196,3 +231,33 @@ main = do
196231
log "Checking product toEnum/fromEnum roundtrip"
197232
assert $ let allPairs = enumFromTo bottom top :: Array (Pair Bit SimpleBounded)
198233
in (toEnum <<< fromEnum <$> allPairs) == (Just <$> allPairs)
234+
235+
log "Checking zero"
236+
assert $ (zero :: A1) == A1 (Tuple (Tuple 0 {a: 0}) {a: 0})
237+
238+
log "Checking one"
239+
assert $ (one :: A1) == A1 (Tuple (Tuple 1 {a: 1}) {a: 1})
240+
241+
log "Checking add"
242+
assert $ A1 (Tuple (Tuple 100 {a: 10}) {a: 20}) + A1 (Tuple (Tuple 50 {a: 30}) {a: 40}) == A1 (Tuple (Tuple 150 {a: 40}) {a: 60})
243+
244+
log "Checking mul"
245+
assert $ A1 (Tuple (Tuple 100 {a: 10}) {a: 20}) * A1 (Tuple (Tuple 50 {a: 30}) {a: 40}) == A1 (Tuple (Tuple 5000 {a: 300}) {a: 800})
246+
247+
log "Checking sub"
248+
assert $ A1 (Tuple (Tuple 100 {a: 10}) {a: 20}) - A1 (Tuple (Tuple 50 {a: 30}) {a: 40}) == A1 (Tuple (Tuple 50 {a: -20}) {a: -20})
249+
250+
log "Checking ff"
251+
assert $ (ff :: B1) == B1 (Tuple (Tuple false {a: false}) {a: false})
252+
253+
log "Checking tt"
254+
assert $ (tt :: B1) == B1 (Tuple (Tuple true {a: true}) {a: true})
255+
256+
log "Checking conj"
257+
assert $ (B1 (Tuple (Tuple true {a: false}) {a: true}) && B1 (Tuple (Tuple false {a: false}) {a: true})) == B1 (Tuple (Tuple false { a: false }) { a: true })
258+
259+
log "Checking disj"
260+
assert $ (B1 (Tuple (Tuple true {a: false}) {a: true}) || B1 (Tuple (Tuple false {a: false}) {a: true})) == B1 (Tuple (Tuple true { a: false }) { a: true })
261+
262+
log "Checking not"
263+
assert $ not B1 (Tuple (Tuple true {a: false}) {a: true}) == B1 (Tuple (Tuple false {a: true}) {a: false})

0 commit comments

Comments
 (0)