speculate-0.2.6: tests/test-expr.hs
{-# Language DeriveDataTypeable, StandaloneDeriving #-} -- Travis
{-# LANGUAGE CPP #-}
-- Test library
import Test
import qualified Test.LeanCheck.Utils as LC (comparison)
-- Functions under test
import Test.Speculate.Expr
import Test.Speculate.Utils
import Test.Speculate.Reason (emptyThy)
import Data.List (sort)
import Data.Functor ((<$>)) -- for GHC < 7.10
import Data.Typeable (typeOf)
import Data.Maybe (isJust)
-- for Travis:
deriving instance Typeable Thyght
deriving instance Typeable Equation
main :: IO ()
main = mainTest tests 10000
tests :: Int -> [Bool]
tests n =
[ True
, consts (xx -+- yy) == [plusE]
, consts (xx -+- (yy -+- zz)) == [plusE]
, consts (zero -+- one) =$ sort $= [zero, one, plusE]
, consts ((zero -+- abs' zero) -+- (ord' aa -+- ord' cc))
=$ sort $= [zero, aa, absE, plusE, ordE]
, holds n $ \e1 e2 -> timesE `elem` consts (e1 -*- e2)
, arity zero == 0
, arity xx == 0
, arity absE == 1
, arity plusE == 2
, arity timesE == 2
, holds n $ okEqOrd -:> expr
, holds n $ okEqOrd -:> (undefined :: Instance)
, holds n $ compare ==== compareComplexity
, holds n $ LC.comparison lexicompare
, holds n $ LC.comparison compareComplexity
, holds n $ \(FunE e1) (FunE e2) e3 -> let cmp = lexicompare
in typ e1 == typ e2 && isJust (e1 $$ e3) && isJust (e2 $$ e3)
==> e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)
, holds n $ \(FunE e1) (FunE e2) e3 -> let cmp = lexicompareBy (flip compare)
in typ e1 == typ e2 && isJust (e1 $$ e3) && isJust (e2 $$ e3)
==> e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)
, holds n $ equivalence (eqExprCommuting [plusE])
, holds n $ equivalence (eqExprCommuting [timesE])
, holds n $ equivalence (eqExprCommuting [plusE,timesE])
, xx -+- yy == xx -+- yy
, xx -+- yy /= yy -+- xx
, not $ eqExprCommuting [timesE] (xx -+- yy) (yy -+- xx)
, eqExprCommuting [plusE] (xx -+- yy) (yy -+- xx)
, eqExprCommuting [plusE] (zz -+- (xx -+- yy)) ((yy -+- xx) -+- zz)
, eqExprCommuting [plusE,timesE] (zz -+- (xx -*- yy)) ((yy -*- xx) -+- zz)
-- Holes < Values < Apps
, xx < zero
, zero < zero -+- one
, xx < xx -+- yy
, zero < xx -+- yy
-- Less arity is less
, zero < absE
, absE < timesE
, aa < ordE
, ordE < timesE
-- precedent types
, pp < xx
, cc < xx
, pp < cc
, xx < xxs
, aa < zero
, Test.true < zero
, Test.true < aa
, zero < ll
-- further precedent types
, constant "xx" xx < zero
, constant "xxeqxx" (Equation xx xx) < constant "xx" xx
, constant "xx" xx < constant "emptyThyght" (Thyght emptyThy)
, unfoldApp (abs' xx) == [absE, xx]
, unfoldApp (abs' (xx -+- yy)) == [absE, xx -+- yy]
, unfoldApp (xx -+- abs' xx) == [plusE, xx, abs' xx]
, holds n $ \e -> renameBy id e == e
, holds n $ \e -> renameBy tail (renameBy ('x':) e) == e
, renameBy (++ "1") (xx -+- yy) == (var "x1" int -+- var "y1" int)
, renameBy (\(c:cs) -> succ c:cs) ((xx -+- yy) -+- ord' cc)
== ((yy -+- zz) -+- ord' dd)
, canonicalize (xx -+- yy)
== (xx -+- yy)
, canonicalize (jj -+- (ii -+- ii))
== (xx -+- (yy -+- yy))
, canonicalize ((jj -+- ii) -+- (xx -+- xx))
== ((xx -+- yy) -+- (zz -+- zz))
, typ zero == typ one
, typ zero == typ xx
, typ zero == typ ii
, typ xx /= typ cc
, typ xx == typ (ord' cc)
, holds n $ \(SameTypeE e1 e2) -> typ e1 == typ e2
, holds n $ \(IntE e) -> typ e == typ i_
, holds n $ \(BoolE e) -> typ e == typ b_
, holds n $ \(CharE e) -> typ e == typ c_
, holds n $ \(ListE e) -> typ e == typ xxs
, etyp (xx :$ yy) == Left (i_ :$ i_)
, etyp (xx :$ (cc :$ yy)) == Left (i_ :$ (c_ :$ i_))
, etyp (ff xx :$ (ord' cc :$ gg yy)) == Left (i_ :$ (i_ :$ i_))
, holds n $ \(SameTypeE ef eg) (SameTypeE ex ey) -> (etyp (ef :$ ex) == etyp (eg :$ ey))
, holds n $ \ef eg ex ey -> (etyp ef == etyp eg && etyp ex == etyp ey)
== (etyp (ef :$ ex) == etyp (eg :$ ey))
, holds n $ \e -> case etyp e of
Right t -> t == typ e
Left _ -> error "Either Listable Expr is generating ill typed expressions or etyp is wrong!"
, lengthE zero == 1
, depthE zero == 1
, lengthE one == 1
, depthE one == 1
, lengthE (zero -+- one) == 3
, depthE (zero -+- one) == 2
, lengthE (zero -+- (xx -+- yy)) == 5
, depthE (zero -+- (xx -+- yy)) == 3
, lengthE (((xx -+- yy) -*- zz) -==- ((xx -*- zz) -+- (yy -*- zz))) == 13
, depthE (((xx -+- yy) -*- zz) -==- ((xx -*- zz) -+- (yy -*- zz))) == 4
, depthE (xx -*- yy -+- xx -*- zz -==- xx -*- (yy -+- zz)) == 4
, lengthE (xx -*- yy -+- xx -*- zz -==- xx -*- (yy -+- zz)) == 13
, depthE (xx -*- yy -+- xx -*- zz) == 3
, depthE (xx -*- (yy -+- zz)) == 3
, allUnique (take (n`div`10) list :: [Expr])
, allUnique (take (n`div`10) $ map unSameTypeE list)
, allUnique (take (n`div`10) $ map unIntE list)
, holds n $ \(IntE e) -> e `isInstanceOf` xx
, holds n $ \(IntE e) -> abs' e `isInstanceOf` abs' xx
, holds n $ \(IntE e) -> (e -+- e) `isInstanceOf` (xx -+- xx)
, holds n $ \(IntE e1) (IntE e2) -> (e1 -+- e2) `isInstanceOf` (xx -+- yy)
, holds n $ \(IntE e1) (IntE e2) -> e1 /= e2 ==> not ((e1 -+- e2) `isInstanceOf` (xx -+- xx))
, holds n $ \e -> e /= zero ==> not (e `isInstanceOf` zero)
, (zero -+- one) `isInstanceOf` (xx -+- yy)
, (zero -+- zero) `isInstanceOf` (xx -+- yy)
, (yy -+- xx) `isInstanceOf` (xx -+- yy)
, (zero -+- zero) `isInstanceOf` (xx -+- xx)
, not $ (zero -+- one) `isInstanceOf` (xx -+- xx)
, zero `isInstanceOf` xx
, not $ xx `isInstanceOf` zero
, (xx -+- (yy -+- xx)) `isInstanceOf` (xx -+- yy)
, (xx -+- (xx -+- xx)) `isInstanceOf` (xx -+- yy)
, not $ (xx -+- (xx -+- xx)) `isInstanceOf` (xx -+- xx)
, vars (xx -+- yy) == [(intTy,"x"),(intTy,"y")]
, vars (xx -+- xx) == [(intTy,"x")]
, vars (xx -+- xx -+- yy) == [(intTy,"x"),(intTy,"y")]
, vars (yy -+- xx -+- yy) == [(intTy,"x"),(intTy,"y")]
, (xx -+- xx) < (xx -+- (xx -+- xx))
, ((xx -+- xx) -+- xx) > (xx -+- (xx -+- xx))
, xx < yy
, zero < one
, xx < zero
-- If those two ever fail, it is because the instance for Ord TypeRep in
-- Data.Typeable has changed. I do rely on this for a "nice" knuth-bendix
-- order (by prefering less arity). If this ever changes, I will have to
-- explicitly compare type arity on Ord Expr.
-- (update: haha! It has changed from before, and twice!)
-- TODO: fix order under GHC <= 7.8
#if __GLASGOW_HASKELL__ < 706
, typeOf ((+) :: Int -> Int -> Int) > typeOf (abs :: Int -> Int)
, typeOf (abs :: Int -> Int) < typeOf (0 :: Int)
#elif __GLASGOW_HASKELL__ < 800
, typeOf ((+) :: Int -> Int -> Int) < typeOf (abs :: Int -> Int)
, typeOf (abs :: Int -> Int) < typeOf (0 :: Int)
#else
, typeOf ((+) :: Int -> Int -> Int) > typeOf (abs :: Int -> Int)
, typeOf (abs :: Int -> Int) > typeOf (0 :: Int)
#endif
, holds n $ \e1 e2 -> e1 `isSub` e2 == (e1 `elem` subexprsV e2)
, show (emptyString) == "\"\" :: [Char]"
, show (space -:- emptyString) == "\" \" :: [Char]"
, show (space -:- ccs) == "' ':cs :: [Char]"
, show (aa -:- bb -:- emptyString) == "\"ab\" :: [Char]"
, show (aa -:- bb -:- ccs) == "'a':'b':cs :: [Char]"
, show (aa -:- space -:- bb -:- lineBreak -:- emptyString) == "\"a b\\n\" :: [Char]"
, show (cc -:- space -:- dd -:- lineBreak -:- emptyString) == "c:' ':d:\"\\n\" :: [Char]"
, show (cc -:- space -:- dd -:- lineBreak -:- ccs) == "c:' ':d:'\\n':cs :: [Char]"
, show (cc -:- aa -:- bb -:- emptyString) == "c:\"ab\" :: [Char]"
, show (cc -:- aa -:- bb -:- space -:- aa -:- bb -:- emptyString) == "c:\"ab ab\" :: [Char]"
, show one == "1 :: Int"
, show (minusOne) == "-1 :: Int"
, show (one -+- one) == "1 + 1 :: Int"
, show (minusOne -+- minusOne) == "(-1) + (-1) :: Int"
, show (zero -.- one) == "(0,1) :: (Int,Int)"
, show (minusOne -.- minusOne) == "(-1,-1) :: (Int,Int)"
, show (one -:- ll) == "[1] :: [Int]"
, show (zero -:- one -:- ll) == "[0,1] :: [Int]"
, show (minusOne -:- ll) == "[-1] :: [Int]"
, show (minusOne -:- minusTwo -:- ll) == "[-1,-2] :: [Int]"
, show (xx -:- minusTwo -:- yy -:- ll) == "[x,-2,y] :: [Int]"
, show (xx -:- minusTwo -:- yy -:- xxs) == "x:(-2):y:xs :: [Int]"
, show (ffE -$- zero) == "f $ 0 :: Int"
, show (ggE -$- xx) == "g $ x :: Int"
, show (ffE -$- minusOne) == "f $ (-1) :: Int"
]