-- Copyright (c) 2017 Rudy Matela. -- Distributed under the 3-Clause BSD licence (see the file LICENSE). module Test ( module Test.Extrapolate , module Test.Extrapolate.Core , module Test.LeanCheck.Utils.Operators , reportTests , getMaxTestsFromArgs , mainTest , printLines , (-:-), ll, llb, llmi , (-+-) , _i, xx, yy , _is, xxs, yys , _b, pp, qq , _mi, mxx , zero, one , false, true , not' , notE , elem', length' , elemE, lengthE , nothing, nothingBool, just , comma , operatorE , (-==-) , (-/=-) , (-<-) , (-<=-) -- * Properties and Tests , generalizableOK , exprOK , idExprEval, showOK , instancesOK , namesOK, sameNamesIn, namesIn , tiersOK, sameTiersIn, tiersIn , bgEqOK, bgEqOrdOK , subset, bgSubset , instancesSubset ) where import System.Exit (exitFailure) import Data.List (elemIndices) import System.Environment (getArgs) import Test.Speculate.Expr (typ) import Test.Speculate.Expr.Instance as I import Data.Typeable (typeOf) import Data.List (isPrefixOf, sort) import Data.Maybe (fromMaybe) import Test.Speculate.Reason import Test.Speculate.Reason.Order import Test.Extrapolate import Test.Extrapolate.Utils import Test.Extrapolate.Core hiding (false, true, lengthE) import qualified Test.Extrapolate.Core as Core import Test.LeanCheck.Utils.Operators reportTests :: [Bool] -> IO () reportTests tests = case elemIndices False tests of [] -> putStrLn "Tests passed!" is -> do putStrLn ("Failed tests:" ++ show is) exitFailure getMaxTestsFromArgs :: Int -> IO Int getMaxTestsFromArgs n = do as <- getArgs return $ case as of (s:_) -> read s _ -> n mainTest :: (Int -> [Bool]) -> Int -> IO () mainTest tests n' = do n <- getMaxTestsFromArgs n' reportTests (tests n) printLines :: Show a => [a] -> IO () printLines = putStrLn . unlines . map show (-:-) :: Expr -> Expr -> Expr x -:- xs = consE :$ x :$ xs where consE = case show $ typ x of "Int" -> consEint "Bool" -> consEbool "Maybe Int" -> consEmint t -> error $ "(-:-): unhandled type " ++ t consEint = constant ":" ((:) -:> int) consEbool = constant ":" ((:) -:> bool) consEmint = constant ":" ((:) -:> mayb int) infixr 5 -:- ll :: Expr ll = expr ([] :: [Int]) _i, xx, yy :: Expr _i = var "" int xx = var "x" int yy = var "y" int _is, xxs, yys :: Expr _is = var "" [int] xxs = var "xs" [int] yys = var "ys" [int] _mi, mxx :: Expr _mi = var "" (mayb int) mxx = var "mx" (mayb int) _b, pp, qq :: Expr _b = var "" bool pp = var "p" bool qq = var "q" bool zero :: Expr zero = expr (0 :: Int) one :: Expr one = expr (1 :: Int) llb :: Expr llb = expr ([] :: [Bool]) llmi :: Expr llmi = expr ([] :: [Maybe Int]) false :: Expr false = expr False true :: Expr true = expr True nothing :: Expr nothing = constant "Nothing" (Nothing :: Maybe Int) nothingBool :: Expr nothingBool = constant "Nothing" (Nothing :: Maybe Bool) elem' :: Expr -> Expr -> Expr elem' x xs = elemE :$ x :$ xs elemE :: Expr elemE = constant "elem" (elem :: Int -> [Int] -> Bool) length' :: Expr -> Expr length' xs = lengthE :$ xs lengthE = constant "length" (length :: [Int] -> Int) not' :: Expr -> Expr not' p = notE :$ p notE :: Expr notE = constant "not" not just :: Expr -> Expr just x = justE :$ x where justE = case show $ typ x of "Int" -> justEint "Bool" -> justEbool t -> error $ "(-:-): unhandled type " ++ t justEint = constant "Just" (Just -:> int) justEbool = constant "Just" (Just -:> bool) comma :: Expr -> Expr -> Expr comma x y = commaE :$ x :$ y where commaE = case (show $ typ x, show $ typ y) of ("Int", "Int") -> commaEii ("Int", "Bool") -> commaEib ("Bool","Int") -> commaEbi ("Bool","Bool") -> commaEbb (t,t') -> error $ "(-:-): unhandled types " ++ t ++ " " ++ t' commaEii = constant "," ((,) ->>: (int,int)) commaEib = constant "," ((,) ->>: (int,bool)) commaEbi = constant "," ((,) ->>: (bool,int)) commaEbb = constant "," ((,) ->>: (bool,bool)) (-+-) :: Expr -> Expr -> Expr e1 -+- e2 = plusE :$ e1 :$ e2 infixl 6 -+- plusE :: Expr plusE = constant "+" ((+) :: Int -> Int -> Int) operatorE :: Expr -> Expr operatorE ((opE :$ _) :$ _) = opE (-==-) :: Expr -> Expr -> Expr e1 -==- e2 = fromMaybe (error $ "(-==-): cannot equate " ++ show e1 ++ " and " ++ show e2) (equation preludeInstances e1 e2) infix 4 -==- (-/=-) :: Expr -> Expr -> Expr e1 -/=- e2 = fromMaybe (error $ "(-/=-): cannot inequate " ++ show e1 ++ " and " ++ show e2) (inequality preludeInstances e1 e2) infix 4 -/=- (-<=-) :: Expr -> Expr -> Expr e1 -<=- e2 = fromMaybe (error $ "(-<=-): cannot lessEq " ++ show e1 ++ " and " ++ show e2) (comparisonLE preludeInstances e1 e2) infix 4 -<=- (-<-) :: Expr -> Expr -> Expr e1 -<- e2 = fromMaybe (error $ "(-<-): cannot less " ++ show e1 ++ " and " ++ show e2) (comparisonLT preludeInstances e1 e2) infix 4 -<- -- Properties and tests -- generalizableOK :: (Eq a, Show a, Generalizable a) => Int -> a -> Bool generalizableOK n x = holds n (exprOK -:> x) && instancesOK (und -: x) where und = error "generalizableOK: this should not get evaluated" exprOK :: (Eq a, Show a, Generalizable a) => a -> Bool exprOK = idExprEval &&& showOK idExprEval :: (Eq a, Generalizable a) => a -> Bool idExprEval x = eval (error "idExprEval: could not eval") (expr x) == x showOK :: (Show a, Generalizable a) => a -> Bool showOK x = show x == dropType (show (expr x)) where dropType :: String -> String dropType cs | " :: " `isPrefixOf` cs = "" dropType "" = "" dropType (c:cs) = c : dropType cs instancesOK :: (Eq a, Generalizable a) => a -> Bool instancesOK = namesOK &&& tiersOK namesOK :: Generalizable a => a -> Bool namesOK x = Core.name x == head (x `namesIn` x) && x `sameNamesIn` [x] && x `sameNamesIn` [[x]] && x `sameNamesIn` mayb x && x `sameNamesIn` (x,x) && x `sameNamesIn` (x,()) && x `sameNamesIn` ((),x) && x `sameNamesIn` (x,(),()) && x `sameNamesIn` ((),x,()) && x `sameNamesIn` ((),(),x) sameNamesIn :: (Generalizable a, Generalizable b) => a -> b -> Bool x `sameNamesIn` c = x `namesIn` x =| 12 |= x `namesIn` c namesIn :: (Generalizable a, Generalizable b) => a -> b -> [String] x `namesIn` c = I.names (instances c []) (typeOf x) tiersOK :: (Eq a, Generalizable a) => a -> Bool tiersOK x = x `sameTiersIn` x && x `sameTiersIn` [x] && x `sameTiersIn` [[x]] && x `sameTiersIn` (mayb x) && x `sameTiersIn` (x,x) && x `sameTiersIn` (x,()) && x `sameTiersIn` ((),x) && x `sameTiersIn` (x,(),()) && x `sameTiersIn` ((),x,()) && x `sameTiersIn` ((),(),x) bgEqOK :: (Eq a, Generalizable a) => a -> a -> Bool bgEqOK = (*==*) ==== (==) &&&& (*/=*) ==== (/=) bgEqOrdOK :: (Eq a, Ord a, Generalizable a) => a -> a -> Bool bgEqOrdOK = bgEqOK &&&& (*<=*) ==== (<=) &&&& (*<*) ==== (<) sameTiersIn :: (Eq a, Generalizable a, Generalizable b) => a -> b -> Bool x `sameTiersIn` cx = isListable (instances cx []) (typeOf x) && (tiers -: [[x]]) =| 6 |= tiersIn cx tiersIn :: (Generalizable a, Generalizable b) => b -> [[a]] tiersIn c = ret where ret = mapT (eval . error $ "tiersIn: the imposible happened") $ tiersE (instances c []) (typeOf (head (head ret))) subset :: Ord a => [a] -> [a] -> Bool xs `subset` ys = sort xs `isSubsequenceOf` sort ys bgSubset :: (Generalizable a, Generalizable b) => a -> b -> Bool x `bgSubset` y = backgroundOf x `subset` backgroundOf y instancesSubset :: (Eq a, Eq b, Generalizable a, Generalizable b) => a -> b -> Bool x `instancesSubset` y = x `bgSubset` y && x `sameTiersIn` y && x `sameNamesIn` y -- available on Data.List since GHC >= 8.0 isSubsequenceOf :: Eq a => [a] -> [a] -> Bool isSubsequenceOf [] _ = True isSubsequenceOf (_:_) [] = False isSubsequenceOf (x:xs) (y:ys) | x == y = xs `isSubsequenceOf` ys | otherwise = (x:xs) `isSubsequenceOf` ys -- Quick and Dirty! instance Show Thy where show Thy { rules = rs , equations = eqs , canReduceTo = (->-) , closureLimit = cl , keepE = keep } = "Thy { rules = " ++ drop 14 (indent 14 . listLines $ map showEquation rs) ++ " , equations = " ++ drop 18 (indent 18 . listLines $ map showEquation eqs) ++ " , canReduceTo = " ++ showCanReduceTo (->-) ++ "\n" ++ " , closureLimit = " ++ show cl ++ "\n" ++ " , keepE = " ++ showKeepE keep ++ "\n" ++ " }" where showEquation (e1,e2) = showExpr e1 ++ " == " ++ showExpr e2 listLines [] = "[]" listLines ss = '[':(tail . unlines $ map (", " ++) ss) ++ "]" showCanReduceTo (->-) = "(??)" showKeepE keep = "\\e -> ??" indent :: Int -> String -> String indent n = unlines . map (replicate n ' ' ++) . lines