leancheck-1.0.4: test/derive.hs

-- Copyright (c) 2015-2025 Rudy Matela.
-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
{-# LANGUAGE TemplateHaskell, CPP #-}
import Test
-- import Test.LeanCheck -- already exported by Test
import Test.LeanCheck.Derive
import Test.LeanCheck.Utils
import Data.List (sort, isPrefixOf)

-- replication of Haskell's built-in data types
-- in the order of the Haskell98 standard
-- https://www.haskell.org/onlinereport/basic.html
-- with Peanos as a numeric type.
data  Peano  =  Zero | Succ Peano  deriving (Eq, Ord, Show)
data  Choice  =  Yes | No  deriving (Eq, Ord, Show)
data  Lst a  =  a :- Lst a | Nil  deriving (Eq, Ord, Show)
data  Duo a b  =  a :+ b  deriving (Eq, Ord, Show)
data  Unit  =  Unit  deriving (Eq, Ord, Show)
data  Perhaps a  =  Naught | Precisely a  deriving (Eq, Ord, Show)
data  Alternatively a b  =  Sinister a | Dexter b  deriving (Eq, Ord, Show)
data  Relation  =  Smaller | Same | Bigger  deriving (Eq, Ord, Show)
data  Trio a b c  =  Trio a b c  deriving (Eq, Ord, Show)

infixr 5 :-

deriveListable ''Peano
deriveListable ''Choice
deriveListable ''Lst
deriveListable ''Duo
deriveListable ''Unit
deriveListable ''Perhaps
deriveListable ''Alternatively
deriveListable ''Relation
deriveListable ''Trio

-- tree types
data Tree a  =  Node (Tree a) a (Tree a) | Null  deriving (Eq, Ord, Show)
data Bush a  =  Bush a :-: Bush a | Leaf a  deriving (Eq, Ord, Show)

deriveListable ''Tree
deriveListable ''Bush

-- mutually recursive types
data Mutual    =  Munil | Mutual CoMutual  deriving (Eq, Ord, Show)
data CoMutual  =  CoMunil | CoMutual Mutual  deriving (Eq, Ord, Show)

deriveListableCascading ''Mutual

-- newtypes, type synonyms, inner/outer
newtype  Novel a  =  Novel a  deriving (Eq, Ord, Show)
data  Inner  =  I  deriving (Eq, Ord, Show)
data  Outer  =  O Inner  deriving (Eq, Ord, Show)
type  Nouter  =  Novel Outer
deriveListableCascading ''Nouter


-- Complex nested datatype cascade
data Nested  =  Nested N0 (N1 Int) (N2 Int Int)
newtype N0   =  R0 Int
newtype N1 a =  R1 a
data N2 a b  =  R2 a b
deriveListableCascading ''Nested

-- Complex recursive nested datatype cascade
data RN       =  RN RN0 (RN1 Int) (RN2 Int RN)
data RN0      =  Nest0 Int | Recurse0 RN
data RN1 a    =  Nest1 a   | Recurse1 RN
data RN2 a b  =  Nest2 a b | Recurse2 RN
deriveListableCascading ''RN

-- Those should have no effect (instance already exists):
{- uncommenting those should generate warnings
deriveListable ''Bool
deriveListable ''Maybe
deriveListable ''Either
-}

-- Those should not generate warnings
deriveListableIfNeeded ''Bool
deriveListableIfNeeded ''Maybe
deriveListableIfNeeded ''Either

main :: IO ()
main  =  mainTest tests 200

tests :: Int -> [Bool]
tests n  =
  [ True

  , [ Zero
    , Succ Zero
    , Succ (Succ Zero)
    , Succ (Succ (Succ Zero))
    ] `isPrefixOf` list

  , [Yes, No] == list

  , [ Nil
    , Unit :- Nil
    , Unit :- Unit :- Nil
    , Unit :- Unit :- Unit :- Nil
    ] `isPrefixOf` list

  , [ Nil
    , Zero :- Nil
    , Zero :- (Zero :- Nil)
    , Succ Zero :- Nil
    , Zero :- (Zero :- (Zero :- Nil))
    , Zero :- (Succ Zero :- Nil)
    ] `isPrefixOf` list

  , list == [Yes :+ Yes, Yes :+ No, No :+ Yes, No :+ No]

  , [ Zero :+ Zero
    , Zero :+ Succ Zero
    , Succ Zero :+ Zero
    , Zero :+ Succ (Succ Zero)
    , Succ Zero :+ Succ Zero
    ] `isPrefixOf` list

  , list == [Unit]

  , list == [Naught, Precisely Unit]

  , list == [Naught, Precisely Yes, Precisely No]

  , list == [Sinister Yes, Sinister No, Dexter Yes, Dexter No]

  , [ Sinister Zero
    , Dexter Zero
    , Sinister (Succ Zero)
    , Dexter (Succ Zero)
    , Sinister (Succ (Succ Zero))
    , Dexter (Succ (Succ Zero))
    ] `isPrefixOf` list

  , list == [Smaller, Same, Bigger]

  , list == [Trio Unit Unit Unit]

  , [ Null
    , Node Null False Null
    , Node Null True Null
    , Node Null False (Node Null False Null)
    , Node Null False (Node Null True Null)
    , Node Null True (Node Null False Null)
    ] `isPrefixOf` list

  , [ Leaf False
    , Leaf True
    , Leaf False :-: Leaf False
    , Leaf False :-: Leaf True
    , Leaf True :-: Leaf False
    , Leaf True :-: Leaf True
    ] `isPrefixOf` list

  , [ Munil
    , Mutual CoMunil
    , Mutual (CoMutual Munil)
    , Mutual (CoMutual (Mutual CoMunil))
    , Mutual (CoMutual (Mutual (CoMutual Munil)))
    , Mutual (CoMutual (Mutual (CoMutual (Mutual CoMunil))))
    ] `isPrefixOf` list

  , list == [I]
  , list == [O I]
  , list == [Novel (O I) :: Nouter]

  , map (\Unit -> ()) list =| n |= list

  , map (\(Novel x) -> x) list == (list :: [()])
  , map (\(Novel x) -> x) list == (list :: [Bool])
  , map (\(Novel x) -> x) list =| n |= (list :: [Int])

  , map (\(x :+ y) -> (x,y)) list == (list :: [((),())])
  , map (\(x :+ y) -> (x,y)) list == (list :: [(Bool,Bool)])
  , map (\(x :+ y) -> (x,y)) list =| n |= (list :: [(Int,Int)])

  , map (\(Trio x y z) -> (x,y,z)) list == (list :: [((),(),())])
  , map (\(Trio x y z) -> (x,y,z)) list == (list :: [(Bool,Bool,Bool)])
  , map (\(Trio x y z) -> (x,y,z)) list =| n |= (list :: [(Int,Int,Int)])

  , map peanoToNat list =| n |= list
  , map listLst list =| n |= (list :: [[Bool]])
  , map listLst list =| n |= (list :: [[Int]])

  , mapT peanoToNat tiers =| 6 |= tiers
  , mapT listLst tiers =| 6 |= (tiers :: [[ [Bool] ]])
  , mapT listLst tiers =| 6 |= (tiers :: [[ [Int] ]])

  , (tiers :: [[ Bool       ]]) =| 6 |= $(deriveTiers ''Bool)
  , (tiers :: [[ [Int]      ]]) =| 6 |= $(deriveTiers ''[])
  , (tiers :: [[ [Bool]     ]]) =| 6 |= $(deriveTiers ''[])
  , (tiers :: [[ Maybe Int  ]]) =| 6 |= $(deriveTiers ''Maybe)
  , (tiers :: [[ Maybe Bool ]]) =| 6 |= $(deriveTiers ''Maybe)
  , (tiers :: [[Either Bool Int]])
    =$ map sort . take 6 $= $(deriveTiers ''Either)

  , (list :: [ Bool       ]) =| n |= $(deriveList ''Bool)
  , (list :: [ [Int]      ]) =| n |= $(deriveList ''[])
  , (list :: [ [Bool]     ]) =| n |= $(deriveList ''[])
  , (list :: [ Maybe Int  ]) =| n |= $(deriveList ''Maybe)
  , (list :: [ Maybe Bool ]) =| n |= $(deriveList ''Maybe)

  , map length (take 6 $ tiers :: [[Unit]]) == [1]
  , map length (take 6 $ tiers :: [[Novel Peano]]) == [1,1,1,1,1,1]
  , map length (take 6 $ tiers :: [[Duo Peano Peano]]) == [1,2,3,4,5,6]
  , map length (take 6 $ tiers :: [[Trio Int Int Int]]) == [1,3,6,10,15,21]
  , map length (take 6 $ tiers :: [[Novel Choice]]) == [2]
  , map length (take 6 $ tiers :: [[Duo Choice Choice]]) == [4]
  , map length (take 6 $ tiers :: [[Trio Choice Choice Choice]]) == [8]

  , map length (take 6 $ tiers :: [[ [Novel Int] ]]) == [1,1,2,4,8,16]
  , map length (take 6 $ tiers :: [[ [Novel Bool] ]]) == [1,2,4,8,16,32]
  , map length (take 6 $ tiers :: [[ [Duo Int Int] ]]) == [1,1,3,8,21,55]

  , map length (take 6 $ tiers :: [[ Lst Int ]]) == [1,1,2,4,8,16]
  , map length (take 6 $ tiers :: [[ Lst Bool ]]) == [1,2,4,8,16,32]

  , map length (take 6 $ tiers :: [[ Mutual ]]) == [1,1,1,1,1,1]
  , map length (take 6 $ tiers :: [[ Nouter ]]) == [1]
  , map length (take 6 $ tiers :: [[ Outer ]]) == [1]
  , map length (take 6 $ tiers :: [[ Inner ]]) == [1]
  ]

peanoToNat :: Peano -> Nat
peanoToNat Zero  =  0
peanoToNat (Succ n)  =  1 + peanoToNat n

listLst :: Lst a -> [a]
listLst Nil  =  []
listLst (x :- xs)  =  x : listLst xs