From d58d6b30f13ac48bfeb5ebb0f29144f7e52568df Mon Sep 17 00:00:00 2001 From: Marcin Szamotulski Date: Mon, 2 Sep 2019 21:51:44 +0200 Subject: [PATCH] Basic tests of Cat and friends --- free-category.cabal | 1 + src/Control/Category/Free.hs | 6 + test/Main.hs | 2 + test/Test/Cat.hs | 233 +++++++++++++++++++++++++++++++++++ 4 files changed, 242 insertions(+) create mode 100644 test/Test/Cat.hs diff --git a/free-category.cabal b/free-category.cabal index 5c4a11c..525a9e1 100644 --- a/free-category.cabal +++ b/free-category.cabal @@ -53,6 +53,7 @@ test-suite test-cats main-is: Main.hs other-modules: + Test.Cat Test.Queue default-language: Haskell2010 build-depends: diff --git a/src/Control/Category/Free.hs b/src/Control/Category/Free.hs index 4675294..fd0e59d 100644 --- a/src/Control/Category/Free.hs +++ b/src/Control/Category/Free.hs @@ -123,6 +123,12 @@ foldCat nat (Cat q0 (Op tr0)) = {-# INLINE foldCat #-} -- TODO: add a proof that unsafeCoerce is safe +-- > op Id = Id -- this is ok +-- > op (Cat q (Op tr)) +-- > = tr₀@(Cat emptyQ (Op tr)) . foldNatQ unDual q +-- -- we assume that q contains Op (Op tr₁),…, Op (Op trₙ) +-- > = tr₀ . tr₁@(Cat q₁` tr₁`) . ⋯ . trₙ@(Cat qₙ` trₙ`) +-- > = Cat (qₙ` :> trₙ₋₁ :> ⋯ :> tr₀) trₙ` op :: forall (f :: k -> k -> *) x y. Cat f x y -> Cat (Op f) y x diff --git a/test/Main.hs b/test/Main.hs index d76b3c7..b68517d 100644 --- a/test/Main.hs +++ b/test/Main.hs @@ -3,6 +3,7 @@ module Main (main) where import Test.Tasty import qualified Test.Queue +import qualified Test.Cat main :: IO () main = defaultMain tests @@ -12,4 +13,5 @@ tests = testGroup "free-categories" -- data structures [ Test.Queue.tests + , Test.Cat.tests ] diff --git a/test/Test/Cat.hs b/test/Test/Cat.hs new file mode 100644 index 0000000..ba4d905 --- /dev/null +++ b/test/Test/Cat.hs @@ -0,0 +1,233 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE GADTs #-} +#if __GLASGOW_HASKELL__ >= 806 +{-# LANGUAGE QuantifiedConstraints #-} +#endif +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-orphans #-} + +module Test.Cat (tests) where + +import Prelude hiding ((.), id) +import Control.Category +import Text.Show.Functions () +import Numeric.Natural (Natural) + +import Control.Algebra.Free2 + +import Control.Category.Free + +import Test.QuickCheck +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck (testProperty) + +tests :: TestTree +tests = + testGroup "Control.Category.Free" + [ testProperty "Cat" prop_Cat + , testProperty "CatL" prop_CatL + , testProperty "C" prop_C + ] + + +data Tr a b where + -- Num transition + NumTr :: Num a => (a -> a) -> Tr a a + FromInteger :: Num b => Tr Integer b + + -- Integral transition + ToInteger :: Integral a => Tr a Integer + + +interpretTr :: Tr a b -> a -> b +interpretTr (NumTr f) = f +interpretTr FromInteger = fromInteger +interpretTr ToInteger = toInteger + + +instance (Show a, Show b) => Show (Tr a b) where + show (NumTr f) = "NumTr " ++ show f + show FromInteger = "FromInteger" + show ToInteger = "ToInteger" + + +data SomeNumTr f a where + SomeNumTr :: Num a + => f Tr a a + -> SomeNumTr f a + +instance Show (f Tr a a) => Show (SomeNumTr f a) where + show (SomeNumTr f) = "SomeNumTr " ++ show f + + +data SomeIntegralTr f a where + SomeIntegralTr :: Integral a + => f Tr a a + -> SomeIntegralTr f a + +instance Show (f Tr a a) => Show (SomeIntegralTr f a) where + show (SomeIntegralTr f) = "SomeIntegralTr " ++ show f + + +-- A 'fromIntegral' transition in any free category @f@. +fromIntegralTr :: ( Integral a + , Num b + , Category (f Tr) + , AlgebraType0 f Tr + , FreeAlgebra2 f + ) => f Tr a b +fromIntegralTr = liftFree2 FromInteger . liftFree2 ToInteger + + +data Sing a where + SInt :: Sing Int + SInteger :: Sing Integer + SNatural :: Sing Natural + +instance Show (Sing a) where + show SInt = "SInt" + show SInteger = "SInteger" + show SNatural = "SNatural" + +data AnySing where + AnySing :: Eq a => Sing a -> AnySing + +instance Eq AnySing where + AnySing SInt == AnySing SInt = True + AnySing SInteger == AnySing SInteger = True + AnySing SNatural == AnySing SNatural = True + _ == _ = False + +instance Show AnySing where + show (AnySing sing) = show sing + +instance Arbitrary AnySing where + arbitrary = oneof + [ pure $ AnySing SInt + , pure $ AnySing SInteger + , pure $ AnySing SNatural + ] + + +instance Arbitrary Natural where + arbitrary = + fromIntegral . getPositive <$> (arbitrary :: Gen (Positive Integer)) + +instance CoArbitrary Natural where + coarbitrary a = variant (fromIntegral a :: Int) + +data AnyListTr b where + AnyListTr :: Eq c => ListTr Tr b c -> Sing c -> AnyListTr b + + +genNextTr :: Sing b + -> Gen (AnyListTr b) +genNextTr b = do + AnySing c <- arbitrary + case (b, c) of + (SInt, SInt) -> + (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary + (SInteger, SInteger) -> + (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary + (SNatural, SNatural) -> + (\f -> AnyListTr (ConsTr (NumTr f) NilTr) c) <$> arbitrary + + (SInt, SInteger) -> + pure $ AnyListTr fromIntegralTr c + (SInt, SNatural) -> + pure $ AnyListTr (fromIntegralTr . liftFree2 (NumTr abs)) c + (SInteger, SInt) -> + pure $ AnyListTr fromIntegralTr c + (SNatural, SInt) -> + pure $ AnyListTr fromIntegralTr c + (SNatural, SInteger) -> + pure $ AnyListTr fromIntegralTr c + (SInteger, SNatural) -> + pure $ AnyListTr (fromIntegralTr . liftFree2 (NumTr abs)) c + + +data ArbListTr where + ArbListTr :: Eq b => ListTr Tr a b -> Sing a -> Sing b -> ArbListTr + +#if __GLASGOW_HASKELL__ >= 806 +instance (forall x y. Show (Tr x y)) => Show ArbListTr where + show (ArbListTr listTr a b) = + "ArbListTr " + ++ show a + ++ " -> " + ++ show b + ++ " " + ++ show listTr +#else +instance Show ArbListTr where + show (ArbListTr _listTr a b) = + "ArbListTr " + ++ show a + ++ " -> " + ++ show b +#endif + +instance Arbitrary ArbListTr where + arbitrary = sized $ \n -> do + k <- choose (0, n) + AnySing a <- arbitrary + go k a (AnyListTr NilTr a) + where + go 0 a (AnyListTr ab b) = pure $ ArbListTr ab a b + go n a (AnyListTr ab b) = do + AnyListTr bc c <- genNextTr b + -- (.) can be used as (++) for ListTr + go (n - 1) a $ AnyListTr (bc . ab) c + + +-- +-- test 'Cat', 'CatL' and 'C' treating 'ListTr' as a model to compare to. +-- +prop_Cat, prop_CatL, prop_C + :: Blind ArbListTr -> Bool + + +prop_Cat (Blind (ArbListTr listTr SInt _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0 + == + foldNatFree2 interpretTr listTr 0 +prop_Cat (Blind (ArbListTr listTr SInteger _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0 + == + foldNatFree2 interpretTr listTr 0 +prop_Cat (Blind (ArbListTr listTr SNatural _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @Cat listTr) 0 + == + foldNatFree2 interpretTr listTr 0 + + +prop_CatL (Blind (ArbListTr listTr SInt _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @CatL listTr) 0 + == + foldNatFree2 interpretTr listTr 0 +prop_CatL (Blind (ArbListTr listTr SInteger _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @CatL listTr) 0 + == + foldNatFree2 interpretTr listTr 0 +prop_CatL (Blind (ArbListTr listTr SNatural _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @CatL listTr) 0 + == + foldNatFree2 interpretTr listTr 0 + + +prop_C (Blind (ArbListTr listTr SInt _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0 + == + foldNatFree2 interpretTr listTr 0 +prop_C (Blind (ArbListTr listTr SInteger _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0 + == + foldNatFree2 interpretTr listTr 0 +prop_C (Blind (ArbListTr listTr SNatural _)) = + foldNatFree2 interpretTr (hoistFreeH2 @_ @C listTr) 0 + == + foldNatFree2 interpretTr listTr 0