diff --git a/src/Data/Bounded/Generic.purs b/src/Data/Bounded/Generic.purs new file mode 100644 index 00000000..c7e2e2ed --- /dev/null +++ b/src/Data/Bounded/Generic.purs @@ -0,0 +1,56 @@ +module Data.Bounded.Generic + ( class GenericBottom + , genericBottom' + , genericBottom + , class GenericTop + , genericTop' + , genericTop + ) where + +import Data.Generic.Rep + +import Data.Bounded (class Bounded, bottom, top) + +class GenericBottom a where + genericBottom' :: a + +instance genericBottomNoArguments :: GenericBottom NoArguments where + genericBottom' = NoArguments + +instance genericBottomArgument :: Bounded a => GenericBottom (Argument a) where + genericBottom' = Argument bottom + +instance genericBottomSum :: GenericBottom a => GenericBottom (Sum a b) where + genericBottom' = Inl genericBottom' + +instance genericBottomProduct :: (GenericBottom a, GenericBottom b) => GenericBottom (Product a b) where + genericBottom' = Product genericBottom' genericBottom' + +instance genericBottomConstructor :: GenericBottom a => GenericBottom (Constructor name a) where + genericBottom' = Constructor genericBottom' + +class GenericTop a where + genericTop' :: a + +instance genericTopNoArguments :: GenericTop NoArguments where + genericTop' = NoArguments + +instance genericTopArgument :: Bounded a => GenericTop (Argument a) where + genericTop' = Argument top + +instance genericTopSum :: GenericTop b => GenericTop (Sum a b) where + genericTop' = Inr genericTop' + +instance genericTopProduct :: (GenericTop a, GenericTop b) => GenericTop (Product a b) where + genericTop' = Product genericTop' genericTop' + +instance genericTopConstructor :: GenericTop a => GenericTop (Constructor name a) where + genericTop' = Constructor genericTop' + +-- | A `Generic` implementation of the `bottom` member from the `Bounded` type class. +genericBottom :: forall a rep. Generic a rep => GenericBottom rep => a +genericBottom = to genericBottom' + +-- | A `Generic` implementation of the `top` member from the `Bounded` type class. +genericTop :: forall a rep. Generic a rep => GenericTop rep => a +genericTop = to genericTop' diff --git a/src/Data/Eq/Generic.purs b/src/Data/Eq/Generic.purs new file mode 100644 index 00000000..1c9e1386 --- /dev/null +++ b/src/Data/Eq/Generic.purs @@ -0,0 +1,35 @@ +module Data.Eq.Generic + ( class GenericEq + , genericEq' + , genericEq + ) where + +import Prelude (class Eq, (==), (&&)) +import Data.Generic.Rep + +class GenericEq a where + genericEq' :: a -> a -> Boolean + +instance genericEqNoConstructors :: GenericEq NoConstructors where + genericEq' _ _ = true + +instance genericEqNoArguments :: GenericEq NoArguments where + genericEq' _ _ = true + +instance genericEqSum :: (GenericEq a, GenericEq b) => GenericEq (Sum a b) where + genericEq' (Inl a1) (Inl a2) = genericEq' a1 a2 + genericEq' (Inr b1) (Inr b2) = genericEq' b1 b2 + genericEq' _ _ = false + +instance genericEqProduct :: (GenericEq a, GenericEq b) => GenericEq (Product a b) where + genericEq' (Product a1 b1) (Product a2 b2) = genericEq' a1 a2 && genericEq' b1 b2 + +instance genericEqConstructor :: GenericEq a => GenericEq (Constructor name a) where + genericEq' (Constructor a1) (Constructor a2) = genericEq' a1 a2 + +instance genericEqArgument :: Eq a => GenericEq (Argument a) where + genericEq' (Argument a1) (Argument a2) = a1 == a2 + +-- | A `Generic` implementation of the `eq` member from the `Eq` type class. +genericEq :: forall a rep. Generic a rep => GenericEq rep => a -> a -> Boolean +genericEq x y = genericEq' (from x) (from y) diff --git a/src/Data/Generic/Rep.purs b/src/Data/Generic/Rep.purs new file mode 100644 index 00000000..45c4570e --- /dev/null +++ b/src/Data/Generic/Rep.purs @@ -0,0 +1,36 @@ +module Data.Generic.Rep + ( class Generic + , to + , from + , NoConstructors + , NoArguments(..) + , Sum(..) + , Product(..) + , Constructor(..) + , Argument(..) + ) where + +-- | A representation for types with no constructors. +data NoConstructors + +-- | A representation for constructors with no arguments. +data NoArguments = NoArguments + +-- | A representation for types with multiple constructors. +data Sum a b = Inl a | Inr b + +-- | A representation for constructors with multiple fields. +data Product a b = Product a b + +-- | A representation for constructors which includes the data constructor name +-- | as a type-level string. +newtype Constructor (name :: Symbol) a = Constructor a + +-- | A representation for an argument in a data constructor. +newtype Argument a = Argument a + +-- | The `Generic` class asserts the existence of a type function from types +-- | to their representations using the type constructors defined in this module. +class Generic a rep | a -> rep where + to :: rep -> a + from :: a -> rep diff --git a/src/Data/HeytingAlgebra/Generic.purs b/src/Data/HeytingAlgebra/Generic.purs new file mode 100644 index 00000000..d42e0b65 --- /dev/null +++ b/src/Data/HeytingAlgebra/Generic.purs @@ -0,0 +1,70 @@ +module Data.HeytingAlgebra.Generic 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) \ No newline at end of file diff --git a/src/Data/Monoid/Generic.purs b/src/Data/Monoid/Generic.purs new file mode 100644 index 00000000..a73232df --- /dev/null +++ b/src/Data/Monoid/Generic.purs @@ -0,0 +1,27 @@ +module Data.Monoid.Generic + ( class GenericMonoid + , genericMempty' + , genericMempty + ) where + +import Data.Monoid (class Monoid, mempty) +import Data.Generic.Rep + +class GenericMonoid a where + genericMempty' :: a + +instance genericMonoidNoArguments :: GenericMonoid NoArguments where + genericMempty' = NoArguments + +instance genericMonoidProduct :: (GenericMonoid a, GenericMonoid b) => GenericMonoid (Product a b) where + genericMempty' = Product genericMempty' genericMempty' + +instance genericMonoidConstructor :: GenericMonoid a => GenericMonoid (Constructor name a) where + genericMempty' = Constructor genericMempty' + +instance genericMonoidArgument :: Monoid a => GenericMonoid (Argument a) where + genericMempty' = Argument mempty + +-- | A `Generic` implementation of the `mempty` member from the `Monoid` type class. +genericMempty :: forall a rep. Generic a rep => GenericMonoid rep => a +genericMempty = to genericMempty' diff --git a/src/Data/Ord/Generic.purs b/src/Data/Ord/Generic.purs new file mode 100644 index 00000000..c47aada4 --- /dev/null +++ b/src/Data/Ord/Generic.purs @@ -0,0 +1,39 @@ +module Data.Ord.Generic + ( class GenericOrd + , genericCompare' + , genericCompare + ) where + +import Prelude (class Ord, compare, Ordering(..)) +import Data.Generic.Rep + +class GenericOrd a where + genericCompare' :: a -> a -> Ordering + +instance genericOrdNoConstructors :: GenericOrd NoConstructors where + genericCompare' _ _ = EQ + +instance genericOrdNoArguments :: GenericOrd NoArguments where + genericCompare' _ _ = EQ + +instance genericOrdSum :: (GenericOrd a, GenericOrd b) => GenericOrd (Sum a b) where + genericCompare' (Inl a1) (Inl a2) = genericCompare' a1 a2 + genericCompare' (Inr b1) (Inr b2) = genericCompare' b1 b2 + genericCompare' (Inl b1) (Inr b2) = LT + genericCompare' (Inr b1) (Inl b2) = GT + +instance genericOrdProduct :: (GenericOrd a, GenericOrd b) => GenericOrd (Product a b) where + genericCompare' (Product a1 b1) (Product a2 b2) = + case genericCompare' a1 a2 of + EQ -> genericCompare' b1 b2 + other -> other + +instance genericOrdConstructor :: GenericOrd a => GenericOrd (Constructor name a) where + genericCompare' (Constructor a1) (Constructor a2) = genericCompare' a1 a2 + +instance genericOrdArgument :: Ord a => GenericOrd (Argument a) where + genericCompare' (Argument a1) (Argument a2) = compare a1 a2 + +-- | A `Generic` implementation of the `compare` member from the `Ord` type class. +genericCompare :: forall a rep. Generic a rep => GenericOrd rep => a -> a -> Ordering +genericCompare x y = genericCompare' (from x) (from y) diff --git a/src/Data/Ring/Generic.purs b/src/Data/Ring/Generic.purs new file mode 100644 index 00000000..27c38fd6 --- /dev/null +++ b/src/Data/Ring/Generic.purs @@ -0,0 +1,24 @@ +module Data.Ring.Generic 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 \ No newline at end of file diff --git a/src/Data/Semigroup/Generic.purs b/src/Data/Semigroup/Generic.purs new file mode 100644 index 00000000..5591903d --- /dev/null +++ b/src/Data/Semigroup/Generic.purs @@ -0,0 +1,31 @@ +module Data.Semigroup.Generic + ( class GenericSemigroup + , genericAppend' + , genericAppend + ) where + +import Prelude (class Semigroup, append) +import Data.Generic.Rep + +class GenericSemigroup a where + genericAppend' :: a -> a -> a + +instance genericSemigroupNoConstructors :: GenericSemigroup NoConstructors where + genericAppend' a _ = a + +instance genericSemigroupNoArguments :: GenericSemigroup NoArguments where + genericAppend' a _ = a + +instance genericSemigroupProduct :: (GenericSemigroup a, GenericSemigroup b) => GenericSemigroup (Product a b) where + genericAppend' (Product a1 b1) (Product a2 b2) = + Product (genericAppend' a1 a2) (genericAppend' b1 b2) + +instance genericSemigroupConstructor :: GenericSemigroup a => GenericSemigroup (Constructor name a) where + genericAppend' (Constructor a1) (Constructor a2) = Constructor (genericAppend' a1 a2) + +instance genericSemigroupArgument :: Semigroup a => GenericSemigroup (Argument a) where + genericAppend' (Argument a1) (Argument a2) = Argument (append a1 a2) + +-- | A `Generic` implementation of the `append` member from the `Semigroup` type class. +genericAppend :: forall a rep. Generic a rep => GenericSemigroup rep => a -> a -> a +genericAppend x y = to (genericAppend' (from x) (from y)) diff --git a/src/Data/Semiring/Generic.purs b/src/Data/Semiring/Generic.purs new file mode 100644 index 00000000..578023e7 --- /dev/null +++ b/src/Data/Semiring/Generic.purs @@ -0,0 +1,51 @@ +module Data.Semiring.Generic 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 \ No newline at end of file diff --git a/src/Data/Show/Generic.js b/src/Data/Show/Generic.js new file mode 100644 index 00000000..53338044 --- /dev/null +++ b/src/Data/Show/Generic.js @@ -0,0 +1,14 @@ +"use strict"; + +exports.intercalate = function (separator) { + return function (xs) { + var len = xs.length; + if (len === 0) return ""; + + var res = xs[0]; + for (var i = 1; i < len; i++) { + res = res + separator + xs[i]; + } + return res; + }; +}; diff --git a/src/Data/Show/Generic.purs b/src/Data/Show/Generic.purs new file mode 100644 index 00000000..5a5f08fa --- /dev/null +++ b/src/Data/Show/Generic.purs @@ -0,0 +1,53 @@ +module Data.Show.Generic + ( class GenericShow + , genericShow' + , genericShow + , class GenericShowArgs + , genericShowArgs + ) where + +import Prelude (class Show, show, (<>)) +import Data.Generic.Rep +import Data.Symbol (class IsSymbol, reflectSymbol) +import Type.Proxy (Proxy(..)) + +class GenericShow a where + genericShow' :: a -> String + +class GenericShowArgs a where + genericShowArgs :: a -> Array String + +instance genericShowNoConstructors :: GenericShow NoConstructors where + genericShow' a = genericShow' a + +instance genericShowArgsNoArguments :: GenericShowArgs NoArguments where + genericShowArgs _ = [] + +instance genericShowSum :: (GenericShow a, GenericShow b) => GenericShow (Sum a b) where + genericShow' (Inl a) = genericShow' a + genericShow' (Inr b) = genericShow' b + +instance genericShowArgsProduct + :: (GenericShowArgs a, GenericShowArgs b) + => GenericShowArgs (Product a b) where + genericShowArgs (Product a b) = genericShowArgs a <> genericShowArgs b + +instance genericShowConstructor + :: (GenericShowArgs a, IsSymbol name) + => GenericShow (Constructor name a) where + genericShow' (Constructor a) = + case genericShowArgs a of + [] -> ctor + args -> "(" <> intercalate " " ([ctor] <> args) <> ")" + where + ctor :: String + ctor = reflectSymbol (Proxy :: Proxy name) + +instance genericShowArgsArgument :: Show a => GenericShowArgs (Argument a) where + genericShowArgs (Argument a) = [show a] + +-- | A `Generic` implementation of the `show` member from the `Show` type class. +genericShow :: forall a rep. Generic a rep => GenericShow rep => a -> String +genericShow x = genericShow' (from x) + +foreign import intercalate :: String -> Array String -> String diff --git a/test/Data/Generic/Rep.purs b/test/Data/Generic/Rep.purs new file mode 100644 index 00000000..385807a3 --- /dev/null +++ b/test/Data/Generic/Rep.purs @@ -0,0 +1,187 @@ +module Test.Data.Generic.Rep where + +import Prelude + +import Data.Generic.Rep as G +import Data.Bounded.Generic as GBounded +import Data.Eq.Generic as GEq +import Data.HeytingAlgebra.Generic as GHeytingAlgebra +import Data.Ord.Generic as GOrd +import Data.Ring.Generic as GRing +import Data.Semiring.Generic as GSemiring +import Data.Show.Generic as GShow +import Data.HeytingAlgebra (ff, tt, implies) +import Test.Utils (AlmostEff, assert) + +data List a = Nil | Cons { head :: a, tail :: List a } + +cons :: forall a. a -> List a -> List a +cons head tail = Cons { head, tail } + +derive instance genericList :: G.Generic (List a) _ + +instance eqList :: Eq a => Eq (List a) where + eq x y = GEq.genericEq x y + +instance showList :: Show a => Show (List a) where + show x = GShow.genericShow x + +data SimpleBounded = A | B | C | D +derive instance genericSimpleBounded :: G.Generic SimpleBounded _ +instance eqSimpleBounded :: Eq SimpleBounded where + eq x y = GEq.genericEq x y +instance ordSimpleBounded :: Ord SimpleBounded where + compare x y = GOrd.genericCompare x y +instance showSimpleBounded :: Show SimpleBounded where + show x = GShow.genericShow x +instance boundedSimpleBounded :: Bounded SimpleBounded where + bottom = GBounded.genericBottom + top = GBounded.genericTop + +data Option a = None | Some a +derive instance genericOption :: G.Generic (Option a) _ +instance eqOption :: Eq a => Eq (Option a) where + eq x y = GEq.genericEq x y +instance ordOption :: Ord a => Ord (Option a) where + compare x y = GOrd.genericCompare x y +instance showOption :: Show a => Show (Option a) where + show x = GShow.genericShow x +instance boundedOption :: Bounded a => Bounded (Option a) where + bottom = GBounded.genericBottom + top = GBounded.genericTop + +data Bit = Zero | One +derive instance genericBit :: G.Generic Bit _ +instance eqBit :: Eq Bit where + eq x y = GEq.genericEq x y +instance ordBit :: Ord Bit where + compare x y = GOrd.genericCompare x y +instance showBit :: Show Bit where + show x = GShow.genericShow x +instance boundedBit :: Bounded Bit where + bottom = GBounded.genericBottom + top = GBounded.genericTop + +data Pair a b = Pair a b +derive instance genericPair :: G.Generic (Pair a b) _ +instance eqPair :: (Eq a, Eq b) => Eq (Pair a b) where + eq = GEq.genericEq +instance ordPair :: (Ord a, Ord b) => Ord (Pair a b) where + compare = GOrd.genericCompare +instance showPair :: (Show a, Show b) => Show (Pair a b) where + show = GShow.genericShow +instance boundedPair :: (Bounded a, Bounded b) => Bounded (Pair a b) where + bottom = GBounded.genericBottom + top = GBounded.genericTop +instance semiringPair :: (Semiring a, Semiring b) => Semiring (Pair a b) where + add (Pair x1 y1) (Pair x2 y2) = Pair (add x1 x2) (add y1 y2) + one = Pair one one + mul (Pair x1 y1) (Pair x2 y2) = Pair (mul x1 x2) (mul y1 y2) + zero = Pair zero zero +instance ringPair :: (Ring a, Ring b) => Ring (Pair a b) where + sub (Pair x1 y1) (Pair x2 y2) = Pair (sub x1 x2) (sub y1 y2) +instance heytingAlgebraPair :: (HeytingAlgebra a, HeytingAlgebra b) => HeytingAlgebra (Pair a b) where + tt = Pair tt tt + ff = Pair ff ff + implies (Pair x1 y1) (Pair x2 y2) = Pair (x1 `implies` x2) (y1 `implies` y2) + conj (Pair x1 y1) (Pair x2 y2) = Pair (conj x1 x2) (conj y1 y2) + disj (Pair x1 y1) (Pair x2 y2) = Pair (disj x1 x2) (disj y1 y2) + not (Pair x y) = Pair (not x) (not y) + +data A1 = A1 (Pair (Pair 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 (Pair (Pair 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 + +testGenericRep :: AlmostEff +testGenericRep = do + assert "Checking show" $ + show (cons 1 (cons 2 Nil)) == "(Cons { head: 1, tail: (Cons { head: 2, tail: Nil }) })" + + assert "Checking equality" $ + cons 1 (cons 2 Nil) == cons 1 (cons 2 Nil) + + assert "Checking inequality" $ + cons 1 (cons 2 Nil) /= cons 1 Nil + + assert "Checking comparison EQ" $ + (Pair Zero (Some One) `compare` Pair Zero (Some One)) == EQ + + assert "Checking comparison GT" $ + (Pair (Some One) Zero `compare` Pair (Some Zero) Zero) == GT + + assert "Checking comparison LT" $ + (Pair Zero One `compare` Pair One One) == LT + + assert "Checking simple bottom" $ + bottom == A + + assert "Checking simple top" $ + top == D + + assert "Checking composite bottom" $ + bottom == (None :: Option SimpleBounded) + + assert "Checking composite top" $ + top == Some D + + assert "Checking product bottom" $ + bottom == (Pair Zero A :: Pair Bit SimpleBounded) + + assert "Checking product top" $ + top == (Pair One D :: Pair Bit SimpleBounded) + + assert "Checking zero" $ + (zero :: A1) == A1 (Pair (Pair 0 {a: 0}) {a: 0}) + + assert "Checking one" $ + (one :: A1) == A1 (Pair (Pair 1 {a: 1}) {a: 1}) + + assert "Checking add" $ + A1 (Pair (Pair 100 {a: 10}) {a: 20}) + A1 (Pair (Pair 50 {a: 30}) {a: 40}) == A1 (Pair (Pair 150 {a: 40}) {a: 60}) + + assert "Checking mul" $ + A1 (Pair (Pair 100 {a: 10}) {a: 20}) * A1 (Pair (Pair 50 {a: 30}) {a: 40}) == A1 (Pair (Pair 5000 {a: 300}) {a: 800}) + + assert "Checking sub" $ + A1 (Pair (Pair 100 {a: 10}) {a: 20}) - A1 (Pair (Pair 50 {a: 30}) {a: 40}) == A1 (Pair (Pair 50 {a: -20}) {a: -20}) + + assert "Checking ff" $ + (ff :: B1) == B1 (Pair (Pair false {a: false}) {a: false}) + + assert "Checking tt" $ + (tt :: B1) == B1 (Pair (Pair true {a: true}) {a: true}) + + assert "Checking conj" $ + (B1 (Pair (Pair true {a: false}) {a: true}) && B1 (Pair (Pair false {a: false}) {a: true})) == B1 (Pair (Pair false { a: false }) { a: true }) + + assert "Checking disj" $ + (B1 (Pair (Pair true {a: false}) {a: true}) || B1 (Pair (Pair false {a: false}) {a: true})) == B1 (Pair (Pair true { a: false }) { a: true }) + + assert "Checking not" $ + not B1 (Pair (Pair true {a: false}) {a: true}) == B1 (Pair (Pair false {a: true}) {a: false}) diff --git a/test/Test/Main.js b/test/Test/Main.js index 296fe776..f3989122 100644 --- a/test/Test/Main.js +++ b/test/Test/Main.js @@ -42,9 +42,3 @@ exports.testNumberShow = function(showNumber) { ]); }; }; - -exports.throwErr = function(msg) { - return function() { - throw new Error(msg); - } -} diff --git a/test/Test/Main.purs b/test/Test/Main.purs index 45c7a34a..a3c0a806 100644 --- a/test/Test/Main.purs +++ b/test/Test/Main.purs @@ -3,8 +3,8 @@ module Test.Main where import Prelude import Data.HeytingAlgebra (ff, tt, implies) import Data.Ord (abs) - -type AlmostEff = Unit -> Unit +import Test.Data.Generic.Rep (testGenericRep) +import Test.Utils (AlmostEff, assert) main :: AlmostEff main = do @@ -14,13 +14,9 @@ main = do testIntDivMod testIntDegree testRecordInstances + testGenericRep foreign import testNumberShow :: (Number -> String) -> AlmostEff -foreign import throwErr :: String -> AlmostEff - - -assert :: String -> Boolean -> AlmostEff -assert msg condition = if condition then const unit else throwErr msg testOrd :: forall a. Ord a => Show a => a -> a -> Ordering -> AlmostEff testOrd x y ord = diff --git a/test/Test/Utils.js b/test/Test/Utils.js new file mode 100644 index 00000000..bea69b25 --- /dev/null +++ b/test/Test/Utils.js @@ -0,0 +1,7 @@ +"use strict"; + +exports.throwErr = function(msg) { + return function() { + throw new Error(msg); + }; +}; diff --git a/test/Test/Utils.purs b/test/Test/Utils.purs new file mode 100644 index 00000000..e58e4968 --- /dev/null +++ b/test/Test/Utils.purs @@ -0,0 +1,10 @@ +module Test.Utils where + +import Prelude + +type AlmostEff = Unit -> Unit + +assert :: String -> Boolean -> AlmostEff +assert msg condition = if condition then const unit else throwErr msg + +foreign import throwErr :: String -> AlmostEff