Added HeytingAlgebra, Semiring, Ring

src/Data/Generic/Rep/HeytingAlgebra.purs

@@ -0,0 +1,70 @@
+module Data.Generic.Rep.HeytingAlgebra where
+
+import Prelude
+
+import Data.Generic.Rep (class Generic, Argument(..), Constructor(..), NoArguments(..), Product(..), from, to)
+import Data.HeytingAlgebra (ff, implies, tt)
+
+class GenericHeytingAlgebra a where
+  genericFF' :: a
+  genericTT' :: a
+  genericImplies' :: a -> a -> a
+  genericConj' :: a -> a -> a
+  genericDisj' :: a -> a -> a
+  genericNot' :: a -> a
+
+instance genericHeytingAlgebraNoArguments :: GenericHeytingAlgebra NoArguments where
+  genericFF' = NoArguments
+  genericTT' = NoArguments
+  genericImplies' _ _ = NoArguments
+  genericConj' _ _ = NoArguments
+  genericDisj' _ _ = NoArguments
+  genericNot' _ = NoArguments
+
+instance genericHeytingAlgebraArgument :: HeytingAlgebra a => GenericHeytingAlgebra (Argument a) where
+  genericFF' = Argument ff
+  genericTT' = Argument tt
+  genericImplies' (Argument x) (Argument y) = Argument (implies x y)
+  genericConj' (Argument x) (Argument y) = Argument (conj x y)
+  genericDisj' (Argument x) (Argument y) = Argument (disj x y)
+  genericNot' (Argument x) = Argument (not x)
+
+instance genericHeytingAlgebraProduct :: (GenericHeytingAlgebra a, GenericHeytingAlgebra b) => GenericHeytingAlgebra (Product a b) where
+  genericFF' = Product genericFF' genericFF'
+  genericTT' = Product genericTT' genericTT'
+  genericImplies' (Product a1 b1) (Product a2 b2) = Product (genericImplies' a1 a2) (genericImplies' b1 b2)
+  genericConj' (Product a1 b1) (Product a2 b2) = Product (genericConj' a1 a2) (genericConj' b1 b2)
+  genericDisj' (Product a1 b1) (Product a2 b2) = Product (genericDisj' a1 a2) (genericDisj' b1 b2)
+  genericNot' (Product a b) = Product (genericNot' a) (genericNot' b)
+
+instance genericHeytingAlgebraConstructor :: GenericHeytingAlgebra a => GenericHeytingAlgebra (Constructor name a) where
+  genericFF' = Constructor genericFF'
+  genericTT' = Constructor genericTT'
+  genericImplies' (Constructor a1) (Constructor a2) = Constructor (genericImplies' a1 a2)
+  genericConj' (Constructor a1) (Constructor a2) = Constructor (genericConj' a1 a2)
+  genericDisj' (Constructor a1) (Constructor a2) = Constructor (genericDisj' a1 a2)
+  genericNot' (Constructor a) = Constructor (genericNot' a)
+
+-- | A `Generic` implementation of the `ff` member from the `HeytingAlgebra` type class.
+genericFF :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a
+genericFF = to genericFF'
+
+-- | A `Generic` implementation of the `tt` member from the `HeytingAlgebra` type class.
+genericTT :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a
+genericTT = to genericTT'
+
+-- | A `Generic` implementation of the `implies` member from the `HeytingAlgebra` type class.
+genericImplies :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a -> a -> a
+genericImplies x y = to $ from x `genericImplies'` from y
+
+-- | A `Generic` implementation of the `conj` member from the `HeytingAlgebra` type class.
+genericConj :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a -> a -> a
+genericConj x y = to $ from x `genericConj'` from y
+
+-- | A `Generic` implementation of the `disj` member from the `HeytingAlgebra` type class.
+genericDisj :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a -> a -> a
+genericDisj x y = to $ from x `genericDisj'` from y
+
+-- | A `Generic` implementation of the `not` member from the `HeytingAlgebra` type class.
+genericNot :: forall a rep. Generic a rep => GenericHeytingAlgebra rep => a -> a
+genericNot x = to $ genericNot' (from x)

src/Data/Generic/Rep/Ring.purs

@@ -0,0 +1,24 @@
+module Data.Generic.Rep.Ring where
+
+import Prelude
+
+import Data.Generic.Rep (class Generic, Argument(..), Constructor(..), NoArguments(..), Product(..), from, to)
+
+class GenericRing a where
+  genericSub' :: a -> a -> a
+
+instance genericRingNoArguments :: GenericRing NoArguments where
+  genericSub' _ _ = NoArguments
+
+instance genericRingArgument :: Ring a => GenericRing (Argument a) where
+  genericSub' (Argument x) (Argument y) = Argument (sub x y)
+
+instance genericRingProduct :: (GenericRing a, GenericRing b) => GenericRing (Product a b) where
+  genericSub' (Product a1 b1) (Product a2 b2) = Product (genericSub' a1 a2) (genericSub' b1 b2)
+
+instance genericRingConstructor :: GenericRing a => GenericRing (Constructor name a) where
+  genericSub' (Constructor a1) (Constructor a2) = Constructor (genericSub' a1 a2)
+
+-- | A `Generic` implementation of the `sub` member from the `Ring` type class.
+genericSub :: forall a rep. Generic a rep => GenericRing rep => a -> a -> a
+genericSub x y = to $ from x `genericSub'` from y

src/Data/Generic/Rep/Semiring.purs

@@ -0,0 +1,51 @@
+module Data.Generic.Rep.Semiring where
+
+import Prelude
+
+import Data.Generic.Rep (class Generic, Argument(..), Constructor(..), NoArguments(..), Product(..), from, to)
+
+class GenericSemiring a where
+  genericAdd'  :: a -> a -> a
+  genericZero' :: a
+  genericMul'  :: a -> a -> a
+  genericOne'  :: a
+
+instance genericSemiringNoArguments :: GenericSemiring NoArguments where
+  genericAdd' _ _ = NoArguments
+  genericZero' = NoArguments
+  genericMul' _ _ = NoArguments
+  genericOne' = NoArguments
+
+instance genericSemiringArgument :: Semiring a => GenericSemiring (Argument a) where
+  genericAdd' (Argument x) (Argument y) = Argument (add x y)
+  genericZero' = Argument zero
+  genericMul' (Argument x) (Argument y) = Argument (mul x y)
+  genericOne' = Argument one
+
+instance genericSemiringProduct :: (GenericSemiring a, GenericSemiring b) => GenericSemiring (Product a b) where
+  genericAdd' (Product a1 b1) (Product a2 b2) = Product (genericAdd' a1 a2) (genericAdd' b1 b2)
+  genericZero' = Product genericZero' genericZero'
+  genericMul' (Product a1 b1) (Product a2 b2) = Product (genericMul' a1 a2) (genericMul' b1 b2)
+  genericOne' = Product genericOne' genericOne'
+
+instance genericSemiringConstructor :: GenericSemiring a => GenericSemiring (Constructor name a) where
+  genericAdd' (Constructor a1) (Constructor a2) = Constructor (genericAdd' a1 a2)
+  genericZero' = Constructor genericZero'
+  genericMul' (Constructor a1) (Constructor a2) = Constructor (genericMul' a1 a2)
+  genericOne' = Constructor genericOne'
+
+-- | A `Generic` implementation of the `zero` member from the `Semiring` type class.
+genericZero :: forall a rep. Generic a rep => GenericSemiring rep => a
+genericZero = to genericZero'
+
+-- | A `Generic` implementation of the `one` member from the `Semiring` type class.
+genericOne :: forall a rep. Generic a rep => GenericSemiring rep => a
+genericOne = to genericOne'
+
+-- | A `Generic` implementation of the `add` member from the `Semiring` type class.
+genericAdd :: forall a rep. Generic a rep => GenericSemiring rep => a -> a -> a
+genericAdd x y = to $ from x `genericAdd'` from y
+
+-- | A `Generic` implementation of the `mul` member from the `Semiring` type class.
+genericMul :: forall a rep. Generic a rep => GenericSemiring rep => a -> a -> a
+genericMul x y = to $ from x `genericMul'` from y

test/Main.purs

@@ -2,16 +2,21 @@ module Test.Main where
 
 import Prelude
 
-import Effect (Effect)
-import Effect.Console (log, logShow)
 import Data.Enum (class BoundedEnum, class Enum, Cardinality(..), cardinality, fromEnum, pred, succ, toEnum, enumFromTo)
 import Data.Generic.Rep as G
 import Data.Generic.Rep.Bounded as GBounded
 import Data.Generic.Rep.Enum as GEnum
 import Data.Generic.Rep.Eq as GEq
+import Data.Generic.Rep.HeytingAlgebra as GHeytingAlgebra
 import Data.Generic.Rep.Ord as GOrd
+import Data.Generic.Rep.Ring as GRing
+import Data.Generic.Rep.Semiring as GSemiring
 import Data.Generic.Rep.Show as GShow
+import Data.HeytingAlgebra (ff, tt)
 import Data.Maybe (Maybe(..))
+import Data.Tuple (Tuple(..))
+import Effect (Effect)
+import Effect.Console (log, logShow)
 import Test.Assert (assert)
 
 data List a = Nil | Cons { head :: a, tail :: List a }
@@ -103,6 +108,36 @@ instance boundedEnumPair :: (BoundedEnum a, BoundedEnum b) => BoundedEnum (Pair
   toEnum = GEnum.genericToEnum
   fromEnum = GEnum.genericFromEnum
 
+data A1 = A1 (Tuple (Tuple Int {a :: Int}) {a :: Int})
+derive instance genericA1 :: G.Generic A1 _
+instance eqA1 :: Eq A1 where
+  eq a = GEq.genericEq a
+instance showA1 :: Show A1 where
+  show a = GShow.genericShow a
+instance semiringA1 :: Semiring A1 where
+  zero = GSemiring.genericZero
+  one = GSemiring.genericOne
+  add x y = GSemiring.genericAdd x y
+  mul x y = GSemiring.genericMul x y
+instance ringA1 :: Ring A1 where
+  sub x y = GRing.genericSub x y
+
+data B1 = B1 (Tuple (Tuple Boolean {a :: Boolean}) {a :: Boolean})
+derive instance genericB1 :: G.Generic B1 _
+instance eqB1 :: Eq B1 where
+  eq a = GEq.genericEq a
+instance showB1 :: Show B1 where
+  show a = GShow.genericShow a
+instance heytingAlgebraB1 :: HeytingAlgebra B1 where
+  ff = GHeytingAlgebra.genericFF
+  tt = GHeytingAlgebra.genericTT
+  implies x y = GHeytingAlgebra.genericImplies x y
+  conj x y = GHeytingAlgebra.genericConj x y
+  disj x y = GHeytingAlgebra.genericDisj x y
+  not x = GHeytingAlgebra.genericNot x
+
+instance booleanAlgebraB1 :: BooleanAlgebra B1
+
 main :: Effect Unit
 main = do
   logShow (cons 1 (cons 2 Nil))
@@ -196,3 +231,33 @@ main = do
   log "Checking product toEnum/fromEnum roundtrip"
   assert $ let allPairs = enumFromTo bottom top :: Array (Pair Bit SimpleBounded)
            in (toEnum <<< fromEnum <$> allPairs) == (Just <$> allPairs)
+
+  log "Checking zero"
+  assert $ (zero :: A1) == A1 (Tuple (Tuple 0 {a: 0}) {a: 0})
+
+  log "Checking one"
+  assert $ (one :: A1) == A1 (Tuple (Tuple 1 {a: 1}) {a: 1})
+
+  log "Checking add"
+  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})
+
+  log "Checking mul"
+  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})
+
+  log "Checking sub"
+  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})  
+
+  log "Checking ff"
+  assert $ (ff :: B1) == B1 (Tuple (Tuple false {a: false}) {a: false})
+
+  log "Checking tt"
+  assert $ (tt :: B1) == B1 (Tuple (Tuple true {a: true}) {a: true})
+
+  log "Checking conj"
+  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 })
+
+  log "Checking disj"
+  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 })
+
+  log "Checking not"
+  assert $ not B1 (Tuple (Tuple true {a: false}) {a: true}) == B1 (Tuple (Tuple false {a: true}) {a: false})