fcf-containers-0.8.1: test/Test/Data/Set.hs
{-# LANGUAGE CPP #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Werror=incomplete-patterns #-}
module Test.Data.Set where
import Data.Proxy
import Data.Type.Equality ((:~:)(Refl))
import Test.Hspec (describe, it, shouldBe, Spec)
import qualified Data.Set as DS
import Fcf (Eval, type (=<<), Map)
import Fcf.Data.Nat
import Fcf.Data.Set
import Fcf.Data.Reflect (fromType)
import Fcf.Alg.Sort
--------------------------------------------------------------------------------
-- > :kind! Eval (Size =<< FromList '[5, 3])
-- Eval (Size =<< FromList '[5, 3]) :: TL.Natural
-- = 2
spec :: Spec
spec = describe "Set" $ do
it "PowerSet" $ do
let test :: forall r. (r ~ Eval (PowerSet =<< FromList '[1,2,9,5])) => DS.Set (DS.Set Int)
test = fromType (Proxy @r)
test
`shouldBe`
DS.powerSet (DS.fromList [1,2,9,5])
it "Size" $ do
let test :: forall r. (r ~ Eval (Size =<< FromList '[5,3])) => Int
test = fromType (Proxy @r)
test `shouldBe` 2
--------------------------------------------------------------------------------
-- This module won't compile, if the Refl doesn't give the correct answer.
--
-- > :kind! (Eval Empty :: Set Nat)
-- (Eval Empty :: Set Nat) :: Set TL.Natural
-- = 'Set '[]
_ = Refl :: (Eval Empty :: Set Nat)
:~: 'Set '[]
-- This module won't compile, if the Refl doesn't give the correct answer.
--
-- > :kind! Eval (Singleton 1)
-- Eval (Singleton 1) :: Set TL.Natural
-- = 'Set '[1]
_ = Refl :: Eval (Singleton 1)
:~: 'Set '[1]
-- > :kind! Eval (Insert 3 =<< FromList '[1, 2])
-- Eval (Insert 3 =<< FromList '[1, 2]) :: Set TL.Natural
-- = 'Set '[3, 1, 2]
_ = Refl :: Eval (Insert 3 =<< FromList '[1, 2])
:~: 'Set '[3, 1, 2]
-- > :kind! Eval (Insert 2 =<< FromList '[1, 2])
-- Eval (Insert 2 =<< FromList '[1, 2]) :: Set TL.Natural
-- = 'Set '[1, 2]
_ = Refl :: Eval (Insert 2 =<< FromList '[1, 2])
:~: 'Set '[1, 2]
-- > :kind! Eval (Delete 5 =<< FromList '[5, 3])
-- Eval (Delete 5 =<< FromList '[5, 3]) :: Set TL.Natural
-- = 'Set '[3]
_ = Refl :: Eval (Delete 5 =<< FromList '[5, 3])
:~: 'Set '[3]
-- > :kind! Eval (Delete 7 =<< FromList '[5, 3])
-- Eval (Delete 7 =<< FromList '[5, 3]) :: Set TL.Natural
-- = 'Set '[5, 3]
_ = Refl :: Eval (Delete 7 =<< FromList '[5, 3])
:~: 'Set '[5, 3]
-- > :kind! Eval (Member 5 =<< FromList '[5, 3])
-- Eval (Member 5 =<< FromList '[5, 3]) :: Bool
-- = 'True
_ = Refl :: Eval (Member 5 =<< FromList '[5, 3])
:~: 'True
-- > :kind! Eval (Member 7 =<< FromList '[5, 3])
-- Eval (Member 7 =<< FromList '[5, 3]) :: Bool
-- = 'False
_ = Refl :: Eval (Member 7 =<< FromList '[5, 3])
:~: 'False
-- > :kind! Eval (NotMember 5 =<< FromList '[5, 3])
-- Eval (NotMember 5 =<< FromList '[5, 3]) :: Bool
-- = 'False
_ = Refl :: Eval (NotMember 5 =<< FromList '[5, 3])
:~: 'False
-- > :kind! Eval (NotMember 7 =<< FromList '[5, 3])
-- Eval (NotMember 7 =<< FromList '[5, 3]) :: Bool
-- = 'True
_ = Refl :: Eval (NotMember 7 =<< FromList '[5, 3])
:~: 'True
-- > :kind! Eval (Null =<< FromList '[5, 3])
-- Eval (Null =<< FromList '[5, 3]) :: Bool
-- = 'False
_ = Refl :: Eval (Null =<< FromList '[5, 3])
:~: 'False
-- > :kind! Eval (Null =<< Empty)
-- Eval (Null =<< Empty) :: Bool
-- = 'True
_ = Refl :: Eval (Null =<< Empty)
:~: 'True
-- > :kind! Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))
-- Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4])) :: Bool
-- = 'True
_ = Refl :: Eval (IsSubsetOf ('Set '[]) ('Set '[0,1,2,3,4]))
:~: 'True
-- > :kind! Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))
-- Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4])) :: Bool
-- = 'True
_ = Refl :: Eval (IsSubsetOf ('Set '[0,1]) ('Set '[0,1,2,3,4]))
:~: 'True
-- > :kind! Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4]))
-- Eval (IsSubsetOf ('Set '[0,2,1,3,4]) ('Set '[0,1,2,3,4])) :: Bool
-- = 'True
_ = Refl :: Eval (IsSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
:~: 'True
-- > :kind! Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))
-- Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4])) :: Bool
-- = 'False
_ = Refl :: Eval (IsSubsetOf ('Set '[0,1,2,3,4,5]) ('Set '[0,1,2,3,4]))
:~: 'False
-- > :kind! Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
-- Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4])) :: Bool
-- = 'False
_ = Refl :: Eval (IsProperSubsetOf ('Set '[0,1,2,3,4]) ('Set '[0,1,2,3,4]))
:~: 'False
-- > :kind! Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))
-- Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4])) :: Bool
-- = 'True
_ = Refl :: Eval (IsProperSubsetOf ('Set '[0,2,1,3]) ('Set '[0,1,2,3,4]))
:~: 'True
-- > :kind! Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )
-- Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) ) :: Set
-- TL.Natural
-- = 'Set '[7, 5, 3]
_ = Refl :: Eval (Union (Eval (FromList '[5, 3])) (Eval (FromList '[5, 7])) )
:~: 'Set '[7, 5, 3]
-- > :kind! Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
-- Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set
-- TL.Natural
-- = 'Set '[3]
_ = Refl :: Eval (Difference (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
:~: 'Set '[3]
-- > :kind! Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
-- Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7]))) :: Set
-- TL.Natural
-- = 'Set '[5]
_ = Refl :: Eval (Intersection (Eval (FromList '[3, 5])) (Eval (FromList '[5, 7])))
:~: 'Set '[5]
-- > :kind! Eval (PowerSet =<< FromList '["a", "b", "c"])
-- Eval (PowerSet =<< FromList '["a", "b", "c"]) :: Set
-- (Set TL.Symbol)
-- = 'Set
-- '[ 'Set '[], 'Set '["c"], 'Set '["b"], 'Set '["b", "c"],
-- 'Set '["a"], 'Set '["a", "b"], 'Set '["a", "c"],
-- 'Set '["a", "b", "c"]]
--
-- > :kind! Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])
-- Eval (PowerSet =<< FromList '[Int, Char, Maybe Int]) :: Set
-- (Set (*))
-- = 'Set
-- '[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char],
-- 'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],
-- 'Set '[Int, Maybe Int], 'Set '[Int, Char, Maybe Int]]
_ = Refl :: Eval (PowerSet =<< FromList '[Int, Char, Maybe Int])
:~: 'Set
'[ 'Set '[], 'Set '[Maybe Int], 'Set '[Char],
'Set '[Char, Maybe Int], 'Set '[Int], 'Set '[Int, Char],
'Set '[Int, Maybe Int], 'Set '[Int, Char, Maybe Int]]
-- > :kind! Eval (FromList '[1, 2])
-- Eval (FromList '[1, 2]) :: Set TL.Natural
-- = 'Set '[1, 2]
_ = Refl :: Eval (FromList '[1, 2])
:~: 'Set '[1, 2]
-- > :kind! Eval (ToList =<< PowerSet =<< FromList '[1,2,3])
-- Eval (ToList =<< PowerSet =<< FromList '[1,2,3]) :: [Set
-- TL.Natural]
-- = '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],
-- 'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]
_ = Refl :: Eval (ToList =<< PowerSet =<< FromList '[1,2,3])
:~: '[ 'Set '[], 'Set '[3], 'Set '[2], 'Set '[2, 3], 'Set '[1],
'Set '[1, 2], 'Set '[1, 3], 'Set '[1, 2, 3]]
-- > :kind! Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])
-- Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3]) :: [[TL.Natural]]
-- = '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]
_ = Refl :: Eval (Qsort NatListOrd =<< Map ToList =<< ToList =<< PowerSet =<< FromList '[1,2,3])
:~: '[ '[], '[1], '[1, 2], '[1, 2, 3], '[1, 3], '[2], '[2, 3], '[3]]