-- Copyright (C) 2021 Rudy Matela
-- Distributed under the 3-Clause BSD licence (see the file LICENSE).
import Test
import Conjure.Defn
import Test.LeanCheck.Error (errorToLeft)
import Data.Express.Fixtures
main :: IO ()
main = mainTest tests 5040
tests :: Int -> [Bool]
tests n =
[ True
, dvl sumDefn (sumV :$ val [1,2,3,11::Int]) == (17 :: Int)
, dvl sumDefn (sumV :$ val [1,2,3::Int]) == ( 6 :: Int)
, dvl sumDefn (sumV :$ val [1,2,3,4::Int]) == (10 :: Int)
, dvl andDefn (andV :$ val [False,False]) == False
, dvl andDefn (andV :$ val [False,True]) == False
, dvl andDefn (andV :$ val [True,True]) == True
, dvl andDefn (andV :$ val [True,False,True]) == False
, dvl orDefn (orV :$ val [False,False]) == False
, dvl orDefn (orV :$ val [False,True]) == True
, dvl orDefn (orV :$ val [True,True]) == True
, dvl orDefn (orV :$ val [True,False,True]) == True
, dvl and1Defn (andV :$ val [False,False]) == False
, dvl and1Defn (andV :$ val [False,True]) == False
, dvl and1Defn (andV :$ val [True,True]) == True
, dvl and1Defn (andV :$ val [True,False,True]) == False
, dvl or1Defn (orV :$ val [False,False]) == False
, dvl or1Defn (orV :$ val [False,True]) == True
, dvl or1Defn (orV :$ val [True,True]) == True
, dvl or1Defn (orV :$ val [True,False,True]) == True
, dvl factDefn (factV :$ val (0 :: Int)) == (1 :: Int)
, dvl factDefn (factV :$ val (1 :: Int)) == (1 :: Int)
, dvl factDefn (factV :$ val (2 :: Int)) == (2 :: Int)
, dvl factDefn (factV :$ val (3 :: Int)) == (6 :: Int)
, dvl factDefn (factV :$ val (4 :: Int)) == (24 :: Int)
, dvl factDefn (factV :$ val (9 :: Int)) == (362880 :: Int)
, errorToLeft (dvl factDefn (factV :$ val (10 :: Int)))
== Right (3628800 :: Int)
, errorToLeft (dvl factDefn (factV :$ val (11 :: Int)) == (39916800 :: Int))
== Left "toDynamicWithDefn: recursion limit reached"
, dvl fact1Defn (factV :$ val (0 :: Int)) == (1 :: Int)
, dvl fact1Defn (factV :$ val (1 :: Int)) == (1 :: Int)
, dvl fact1Defn (factV :$ val (2 :: Int)) == (2 :: Int)
, dvl fact1Defn (factV :$ val (3 :: Int)) == (6 :: Int)
, dvl fact1Defn (factV :$ val (4 :: Int)) == (24 :: Int)
, dvl fact1Defn (factV :$ val (9 :: Int)) == (362880 :: Int)
, errorToLeft (dvl fact1Defn (factV :$ val (10 :: Int)))
== Right (3628800 :: Int)
, errorToLeft (dvl fact1Defn (factV :$ val (11 :: Int)) == (39916800 :: Int))
== Left "toDynamicWithDefn: recursion limit reached"
, dvl isZeroDefn (isZeroV :$ val (0 :: Int)) == True
, dvl isZeroDefn (isZeroV :$ val (1 :: Int)) == False
, dvl isOneDefn (isOneV :$ val (0 :: Int)) == False
, dvl isOneDefn (isOneV :$ val (1 :: Int)) == True
, dvl nullDefn (nullV :$ val [0,1,2,3::Int]) == False
, dvl nullDefn (nullV :$ val ([] :: [Int])) == True
, holds n $ cevl 60 sumDefn === (sum :: [Int] -> Int)
, holds n $ cevl 60 andDefn === (and :: [Bool] -> Bool)
, holds n $ cevl 60 orDefn === (or :: [Bool] -> Bool)
, holds n $ cevl 60 isZeroDefn === ((==0) :: Int -> Bool)
, holds n $ cevl 60 isOneDefn === ((==1) :: Int -> Bool)
, holds n $ cevl 60 nullDefn === (null :: [Int] -> Bool)
, holds n $ cevl 60 appendDefn ==== ((++) :: [Int] -> [Int] -> [Int])
-- evaluating at the incorrect types should return Nothing
, isNothing (cevaluate 60 sumDefn :: Maybe ([Bool] -> Bool))
, isNothing (cevaluate 60 andDefn :: Maybe ([Int] -> Int))
, isNothing (cevaluate 60 nullDefn :: Maybe ([Int] -> Int))
]
dvl :: Typeable a => Defn -> Expr -> a
dvl = devl exprExpr 11
sumV, factV, nullV, isZeroV :: Expr
factV = var "fact" (undefined :: Int -> Int)
sumV = var "sum" (undefined :: [Int] -> Int)
andV = var "and" (undefined :: [Bool] -> Bool)
orV = var "or" (undefined :: [Bool] -> Bool)
isZeroV = var "isZero" (undefined :: Int -> Bool)
isOneV = var "isOne" (undefined :: Int -> Bool)
nullV = var "null" (undefined :: [Int] -> Bool)
appendV = var "++" (undefined :: [Int] -> [Int] -> [Int])
-- NOTE: a hack for testing needs all types that are Express as arguments of
-- undefined.
exprExpr :: Expr -> Expr
exprExpr = conjureExpress (undefined :: Bool -> [Bool] -> Int -> [Int] -> ())
sumDefn :: Defn
sumDefn = [ sum' nil =- zero
, sum' (xx -:- xxs) =- xx -+- (sumV :$ xxs)
] where sum' e = sumV :$ e
factDefn :: Defn
factDefn = [ fact' zero =- one
, fact' xx =- xx -*- (factV :$ (xx -+- minusOne))
] where fact' e = factV :$ e
fact1Defn :: Defn
fact1Defn = [ fact' xx =- if' (xx -==- zero) (one) (xx -*- (factV :$ (minus :$ xx :$ one)))
] where fact' e = factV :$ e
nullDefn :: Defn
nullDefn = [ null' nil =- true
, null' (xx -:- xxs) =- false
] where null' e = nullV :$ e
isZeroDefn :: Defn
isZeroDefn = [ isZero' zero =- true
, isZero' xx =- false
] where isZero' e = isZeroV :$ e
isOneDefn :: Defn
isOneDefn = [ isOne' xx =- xx -==- one ]
where isOne' e = isOneV :$ e
andDefn :: Defn
andDefn = [ and' nilBool =- true
, and' (pp -:- pps) =- pp -&&- (andV :$ pps)
] where and' e = andV :$ e
orDefn :: Defn
orDefn = [ or' nilBool =- false
, or' (pp -:- pps) =- pp -||- (orV :$ pps)
] where or' e = orV :$ e
and1Defn :: Defn
and1Defn = [ and' pps =- null' pps -||- head' pps -&&- and' (tail' pps)
] where and' e = andV :$ e
or1Defn :: Defn
or1Defn = [ or' pps =- not' (null' pps) -&&- (head' pps -||- or' (tail' pps))
] where or' e = orV :$ e
appendDefn :: Defn
appendDefn = [ nil -++- xxs =- xxs
, (xx -:- xxs) -++- yys =- xx -:- (xxs -++- yys)
] where exs -++- eys = appendV :$ exs :$ eys
(=-) = (,)
infixr 0 =-