diff --git a/.gitignore b/.gitignore new file mode 100644 --- /dev/null +++ b/.gitignore @@ -0,0 +1,86 @@ +# .gitignore for Extrapolate +**/.cabal-sandbox +**/cabal.sandbox.config +**/idx/ +**/dist/ +**/log/ +etc +.stack-work + +**.hspp +**.swp +**.hi +**.o +**.dyn_hi +**.dyn_o +**.hpc +**.hpc-* +**.tix +**~ + +**/TAGS +**/tags + +doc +README.html + +mk/toplibs +tests/test-extrapolate +tests/test-utils +tests/test-derive +tests/test-step-by-step +tests/test-new +eg/sorting +eg/list +eg/int +eg/arith +eg/calculator +eg/parser +eg/gencalc +eg/overflow +eg/overflow8 +eg/heap +eg/redblack +eg/word-refinements +eg/*.runtime +bench/*.runtime +bench/true-false +bench/true +bench/false +bench/eq +bench/diff +bench/ord +bench/lazy-sc/list +bench/lazy-sc/sorting +bench/lazy-sc/int +bench/lazy-sc/arith +bench/lazy-sc/calculator +bench/lazy-sc/parser +bench/lazy-sc/gencalc +bench/lazy-sc/word-refinements +bench/lazy-sc/overflow +bench/lazy-sc/heap +bench/lazy-sc/redblack +bench/lazy-sc/lazysmallcheck2012 +bench/smartcheck/smartcheck +bench/smartcheck/div0 +bench/smartcheck/div0.hs +bench/smartcheck/parser +bench/smartcheck/parser.hs +bench/smartcheck/sorting +bench/smartcheck/word-refinements +bench/smartcheck/overflow +bench/smartcheck/overflow.hs +bench/smartcheck/list +bench/smartcheck/*-out +bench/smartcheck/*.runtime +eg/xmonad/xmonad +eg/RedBlackSetBalanceBug.hs +eg/RedBlackSetDeleteBug.hs +eg/RedBlackSetRemoveBug.hs +eg/redblack-balance-bug +eg/redblack-balance-bug.hs +eg/redblack-delete-bug +eg/redblack-delete-bug.hs +eg/redblack-remove-bug +eg/redblack-remove-bug.hs diff --git a/.travis.yml b/.travis.yml new file mode 100644 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,75 @@ +# .travis.yml file for Extrapolate +# +# Copyright: (c) 2017-2018 Rudy Matela +# License: 3-Clause BSD (see the file LICENSE) +# Maintainer: Rudy Matela + +language: c # not really + +notifications: + email: + on_failure: change + +sudo: false + +cache: + directories: + - $HOME/.ghc + - $HOME/.cabal + - $HOME/.stack + +before_install: +- export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH +- ghc --version +- cabal --version +- rm -f ~/.cabal/config && cabal update +# Download and unpack the stack executable +# "Once Travis whitelists the stack.dev files," simply include stack in the +# addons section. -- https://docs.haskellstack.org/en/stable/travis_ci/ +- mkdir -p ~/.local/bin +- export PATH=$HOME/.local/bin:$PATH +- travis_retry curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack' +- stack config set system-ghc --global true +- stack --version +- cabal install leancheck speculate + +script: +- make && make test +- make haddock HADDOCKFLAGS= +#- travis_wait 30 cabal test +- stack $STACKR --no-terminal --skip-ghc-check test + +matrix: + allow_failures: + - ghc: 'head' + include: + - ghc: 'head' + env: GHCVER=head CABALVER=head + addons: {apt: {packages: [ghc-head, cabal-install-head], sources: hvr-ghc}} + - ghc: '8.4' + env: GHCVER=8.4.2 CABALVER=2.2 + addons: {apt: {packages: [ghc-8.4.2, cabal-install-2.2], sources: hvr-ghc}} + - ghc: '8.2' + env: GHCVER=8.2.2 CABALVER=2.0 + addons: {apt: {packages: [ghc-8.2.2, cabal-install-2.0], sources: hvr-ghc}} + - ghc: '8.0' + env: GHCVER=8.0.2 CABALVER=1.24 + addons: {apt: {packages: [ghc-8.0.2, cabal-install-1.24], sources: hvr-ghc}} + - ghc: '7.10' + env: GHCVER=7.10.3 CABALVER=1.22 STACKR=--resolver=lts-11.11 + addons: {apt: {packages: [ghc-7.10.3, cabal-install-1.22], sources: hvr-ghc}} + # we only support stack with GHC >= 7.10 + - ghc: '7.8' + env: GHCVER=7.8.4 CABALVER=1.18 + addons: {apt: {packages: [ghc-7.8.4, cabal-install-1.18], sources: hvr-ghc}} + before_install: + - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH + - ghc --version + - cabal --version + - rm -f ~/.cabal/config && cabal update + - cabal install Cabal==1.18.* + - cabal install leancheck speculate + script: + - make && make test + - make haddock HADDOCKFLAGS= + - cabal test diff --git a/Makefile b/Makefile new file mode 100644 --- /dev/null +++ b/Makefile @@ -0,0 +1,180 @@ +# Makefile for Extrapolate +# +# Copyright: (c) 2015-2018 Rudy Matela +# License: 3-Clause BSD (see the file LICENSE) +# Maintainer: Rudy Matela +TESTS = \ + tests/test-derive \ + tests/test-utils \ + tests/test-new \ + tests/test-step-by-step \ + tests/test-extrapolate +QUICKEG = \ + eg/int \ + eg/list \ + eg/calculator \ + eg/gencalc \ + eg/parser \ + eg/heap \ + eg/redblack \ + eg/word-refinements \ + eg/sorting +EG = \ + bench/true \ + bench/false \ + bench/eq \ + bench/diff \ + bench/ord \ + eg/overflow \ + eg/overflow8 \ + $(QUICKEG) +GHCIMPORTDIRS = src:tests:eg +GHCEXTRAFLAGS = #-prof -fprof-auto #-caf-all +# When profiling is enabled, to get the cost centres with more than 6% time: +# $ ./eg/sorting +RTS -p -RTS +# $ cat sorting.prof | grep -v ' [0-5].[0-9] ......$' +GHCFLAGS = -O2 $(GHCEXTRAFLAGS) \ + $(shell grep -q "Arch Linux" /etc/lsb-release && echo -dynamic) +HADDOCKFLAGS = --no-print-missing-docs + +all: mk/toplibs + +all-all: mk/All.hs + +test: $(patsubst %,%.test,$(TESTS)) diff-test + +diff-test: $(patsubst %,%.diff-test,$(EG)) + +quick-test: $(patsubst %,%.test,$(TESTS)) quick-diff-test + +quick-diff-test: $(patsubst %,%.diff-test,$(QUICKEG)) + +update-diff-test: $(patsubst %,%.update-diff-test,$(EG)) + +egs: $(EG) + +%.test: tests/test-% + ./$< + +%.test: % + ./$< + +%.diff-test: % + ./$< | diff -rud tests/model/$<.out - + +%.update-diff-test: % + ./$< > tests/model/$<.out + +test-sdist: + ./tests/test-sdist + +bench: $(patsubst %,%.bench,$(EG)) + +.PHONY: %.bench +%.bench: % + @mkdir -p bench/runtime/$$HOSTNAME + @printf "%-18s " $< + @/usr/bin/time -f%e ./$< 2>&1 >/dev/null | tee bench/runtime/$$HOSTNAME/$<.runtime + +clean: clean-hi-o clean-haddock + rm -f $(TESTS) $(EG) mk/toplibs + rm -f eg/redblack-*-bug* eg/RedBlackSet*Bug.* + +ghci: mk/All.ghci + +ghci-test: tests/Test.ghci + +ghci-7.10: GHC=ghc-7.10 +ghci-7.10: mk/All.ghci + +ghci-7.8: GHC=ghc-7.8 +ghci-7.8: mk/All.ghci + +install: + @echo "use \`cabal install' instead" + +legacy-test: # needs ghc-8.2 .. ghc-7.8 installed as such + make clean && make test -j8 GHC=ghc-8.2 GHCFLAGS="-Werror -dynamic" + make clean && make test -j8 GHC=ghc-8.0 GHCFLAGS="-Werror -dynamic" + make clean && make test -j8 GHC=ghc-7.10 GHCFLAGS="-Werror -dynamic" + make clean && make test -j8 GHC=ghc-7.8 GHCFLAGS="-Werror -dynamic" + make clean && make test -j8 + +legacy-test-via-cabal: # needs similarly named cabal wrappers + cabal clean && cabal-ghc-8.2 configure && cabal-ghc-8.2 test + cabal clean && cabal-ghc-8.0 configure && cabal-ghc-8.0 test + cabal clean && cabal-ghc-7.10 configure && cabal-ghc-7.10 test + cabal clean && cabal-ghc-7.8 configure && cabal-ghc-7.8 test + cabal clean && cabal test + +prepare-legacy-test: \ + prepare-legacy-test-8.2 \ + prepare-legacy-test-8.0 \ + prepare-legacy-test-7.10 \ + prepare-legacy-test-7.8 + +prepare-legacy-test-8.2: + cabal-ghc-8.2 --ignore-sandbox install leancheck speculate + +prepare-legacy-test-8.0: + cabal-ghc-8.0 --ignore-sandbox install leancheck speculate + +prepare-legacy-test-7.10: + cabal-ghc-7.10 --ignore-sandbox install leancheck speculate + +prepare-legacy-test-7.8: + cabal-ghc-7.8 --ignore-sandbox install leancheck speculate + +hlint: + hlint \ + --ignore "Use import/export shortcut" \ + --ignore "Redundant bracket" \ + src eg/sorting.hs eg/list.hs eg/word-refinements.hs + +markdown: + pandoc README.md -o README.html + +# NOTE: (very hacky!) the following target allows parallel compilation (-jN) of +# eg and tests programs so long as they don't share dependencies _not_ stored +# in src/ and tests/. Runnable binaries should depend on mk/toplibs instead of +# actual Haskell source files +mk/toplibs: mk/Toplibs.o + touch mk/toplibs + +include mk/haskell.mk + + +eg/RedBlackSetRemoveBug.hspp: eg/RedBlackSet.hs + $(GHCCMD) -DREMOVE_BUG -E $< -o $@ + +eg/RedBlackSetRemoveBug.hs: eg/RedBlackSetRemoveBug.hspp + sed -e "s/module RedBlackSet/&RemoveBug/" $< > $@ + +eg/redblack-remove-bug.hs: eg/redblack.hs + sed -e "s/import RedBlackSet/&RemoveBug/" $< > $@ + +eg/redblack-remove-bug: eg/redblack-remove-bug.hs eg/RedBlackSetRemoveBug.hs mk/toplibs + + +eg/RedBlackSetDeleteBug.hspp: eg/RedBlackSet.hs + $(GHCCMD) -DDELETE_BUG -E $< -o $@ + +eg/RedBlackSetDeleteBug.hs: eg/RedBlackSetDeleteBug.hspp + sed -e "s/module RedBlackSet/&DeleteBug/" $< > $@ + +eg/redblack-delete-bug.hs: eg/redblack.hs + sed -e "s/import RedBlackSet/&DeleteBug/" $< > $@ + +eg/redblack-delete-bug: eg/redblack-delete-bug.hs eg/RedBlackSetDeleteBug.hs mk/toplibs + + +eg/RedBlackSetBalanceBug.hspp: eg/RedBlackSet.hs + $(GHCCMD) -DBALANCE_BUG -E $< -o $@ + +eg/RedBlackSetBalanceBug.hs: eg/RedBlackSetBalanceBug.hspp + sed -e "s/module RedBlackSet/&BalanceBug/" $< > $@ + +eg/redblack-balance-bug.hs: eg/redblack.hs + sed -e "s/import RedBlackSet/&BalanceBug/" $< > $@ + +eg/redblack-balance-bug: eg/redblack-balance-bug.hs eg/RedBlackSetBalanceBug.hs mk/toplibs diff --git a/bench/diff.hs b/bench/diff.hs new file mode 100644 --- /dev/null +++ b/bench/diff.hs @@ -0,0 +1,51 @@ +import Test.Extrapolate +import Data.List +import Data.Typeable (typeOf) + +main :: IO () +main = do + ch () + ch bool + ch int + ch integer + ch char + ch ordering + + ch [()] + ch [bool] + ch [int] + ch [integer] + ch [char] + ch [ordering] + + ch ((),int) + ch (bool,char) + ch (int,(),bool) + ch (ordering,char,integer) + + ch (mayb ()) + ch (mayb int) + + ch (eith () bool) + ch (eith int char) + +-- TODO: find out why output for the following is different across diff GHCs +-- see: https://travis-ci.org/rudymatela/extrapolate/jobs/263425540 +-- ch (char,int,bool,ordering) + +-- For some reason, output for the following funky types is different across +-- different versions of GHC, see: +-- https://travis-ci.org/rudymatela/extrapolate/builds/262325825 +-- I don't have time to investigate now, but it might be good to check why. +--ch (eith integer ordering,mayb (int,(),bool),mayb (char,())) +--ch (eith (integer,mayb (int,(),bool),mayb (char,())) (int,char)) + + +ch :: (Eq a, Generalizable a) => a -> IO () +ch x = do + putStrLn $ "checks :: " ++ show (typeOf x) ++ "\n" + check `withConditionSize` 3 $ (/=) -:> x + putStrLn "" +-- The following makes everything too slow +--check $ (\x y z -> x /= y && y /= z && z /= x) -:> x +-- maybe in a future faster version we can uncomment those above. diff --git a/bench/eq.hs b/bench/eq.hs new file mode 100644 --- /dev/null +++ b/bench/eq.hs @@ -0,0 +1,52 @@ +import Test.Extrapolate +import Data.List +import Data.Typeable (typeOf) + +main :: IO () +main = do + ch () + ch bool + ch int + ch integer + ch char + ch ordering + + ch [()] + ch [bool] + ch [int] + ch [integer] + ch [char] + ch [ordering] + + ch ((),int) + ch (bool,char) + ch (int,(),bool) + ch (ordering,char,integer) + + ch (mayb ()) + ch (mayb int) + + ch (eith () bool) + ch (eith int char) + +-- TODO: find out why output for the following is different across diff GHCs +-- see: https://travis-ci.org/rudymatela/extrapolate/jobs/263425540 +-- ch (char,int,bool,ordering) + +-- For some reason, output for the following funky types is different across +-- different versions of GHC, see: +-- https://travis-ci.org/rudymatela/extrapolate/builds/262325825 +-- I don't have time to investigate now, but it might be good to check why. +--ch (eith integer ordering,mayb (int,(),bool),mayb (char,())) +--ch (eith (integer,mayb (int,(),bool),mayb (char,())) (int,char)) + + +ch :: (Eq a, Generalizable a) => a -> IO () +ch x = do + putStrLn $ "checks :: " ++ show (typeOf x) ++ "\n" + check $ (==) -:> x + putStrLn "" +-- The following makes everything too slow +--check $ (\x y z -> x == y && y == z) -:> x +--check $ (\x y z w -> x == y || z == w) -:> x ->>:> x +-- maybe in a future faster version we can uncomment those above. diff --git a/bench/false.hs b/bench/false.hs new file mode 100644 --- /dev/null +++ b/bench/false.hs @@ -0,0 +1,50 @@ +import Test.Extrapolate +import Data.List +import Data.Typeable (typeOf) + +main :: IO () +main = do + ch () + ch bool + ch int + ch integer + ch char + ch ordering + +--ch [()] +--ch [bool] +--ch [int] + ch [integer] +--ch [char] +--ch [ordering] + +--ch ((),int) +--ch (bool,char) +--ch (int,(),bool) +--ch (ordering,char,integer) + +--ch (mayb ()) + ch (mayb int) + +--ch (eith () bool) + ch (eith int char) + +-- TODO: find out why output for the following is different across diff GHCs +-- see: https://travis-ci.org/rudymatela/extrapolate/jobs/263425540 +-- ch (char,int,bool,ordering) + +-- For some reason, output for the following funky types is different across +-- different versions of GHC, see: +-- https://travis-ci.org/rudymatela/extrapolate/builds/262325825 +-- I don't have time to investigate now, but it might be good to check why. +--ch (eith integer ordering,mayb (int,(),bool),mayb (char,())) +--ch (eith (integer,mayb (int,(),bool),mayb (char,())) (int,char)) + + +ch :: (Eq a, Generalizable a) => a -> IO () +ch x = do + putStrLn $ "checks :: " ++ show (typeOf x) ++ "\n" + check `withConditionSize` 3 $ const False -:> x + check `withConditionSize` 3 $ (\x y -> False) -:> x ->:> x + check `withConditionSize` 3 $ (\x y z -> False) -:> x ->:> x ->>:> x + putStrLn "" diff --git a/bench/lazy-sc/Makefile b/bench/lazy-sc/Makefile new file mode 100644 --- /dev/null +++ b/bench/lazy-sc/Makefile @@ -0,0 +1,35 @@ +GHC=ghc-7.8 +BENCH= \ + sorting \ + calculator \ + parser \ + overflow \ + word-refinements \ + list +TYM= \ + /usr/bin/time "-f%e %M" + +all: $(BENCH) + +bench: all + @- $(TYM) ./list + @- $(TYM) ./sorting + @- $(TYM) ./calculator + @- $(TYM) ./parser + @- $(TYM) ./word-refinements + +%: %.hs + $(GHC) -dynamic -O2 -package-db .cabal-sandbox/*-$(GHC).*-packages.conf.d $< && touch $@ + +prepare: + cabal sandbox init + git clone https://github.com/UoYCS-plasma/LazySmallCheck2012 lazysmallcheck2012 + git -C lazysmallcheck2012 show -s --format="%H%n%ci" | tee revision.txt + cabal sandbox add-source lazysmallcheck2012 + cabal-$(GHC) install lazysmallcheck2012 + +clean: + rm -f $(BENCH) *.hi *.o + +clean-prepare: + rm -rf .cabal-sandbox cabal.sandbox.config lazysmallcheck2012 diff --git a/bench/lazy-sc/calculator.hs b/bench/lazy-sc/calculator.hs new file mode 100644 --- /dev/null +++ b/bench/lazy-sc/calculator.hs @@ -0,0 +1,42 @@ +-- Example taken from Lee Pike's SmartCheck: +-- https://github.com/leepike/SmartCheck/blob/master/paper/paper.pdf +-- https://github.com/leepike/smartcheck +-- The version here is the one from the paper (similar to the one in the README +-- file). I chose the one in the paper as it is clearer. +{-# Language TemplateHaskell, DeriveDataTypeable #-} +import Control.Monad +import Data.Maybe +import Test.LazySmallCheck2012 +import Test.LazySmallCheck2012.TH +import Data.Typeable +import Data.Data + +data Exp = C Int + | Add Exp Exp + | Div Exp Exp + deriving (Eq, Ord, Show, Data, Typeable) + +eval :: Exp -> Maybe Int +eval (C i) = Just i +eval (Add e0 e1) = + liftM2 (+) (eval e0) (eval e1) +eval (Div e0 e1) = + let e = eval e1 in + if e == Just 0 then Nothing + else liftM2 div (eval e0) e + +-- originally called divSubTerms by Pike +noDiv0 :: Exp -> Bool +noDiv0 (C _) = True +noDiv0 (Div _ (C 0)) = False +noDiv0 (Add e0 e1) = noDiv0 e0 && noDiv0 e1 +noDiv0 (Div e0 e1) = noDiv0 e0 && noDiv0 e1 + +prop_div :: Exp -> Bool +prop_div e = noDiv0 e ==> eval e /= Nothing + +deriveSerial ''Exp + +main :: IO () +main = do + test prop_div diff --git a/bench/lazy-sc/list.hs b/bench/lazy-sc/list.hs new file mode 100644 --- /dev/null +++ b/bench/lazy-sc/list.hs @@ -0,0 +1,12 @@ +import Test.LazySmallCheck2012 +import Data.List + +main :: IO () +main = do + test $ \xs xs' -> (xs++xs' :: [Int]) `isPrefixOf` xs + +-- not lazy, so no generalization with Lazy SmallCheck 2012 +-- > test $ \xs -> nub xs == (xs :: [Int]) + +-- not lazy as well: +-- > test $ \xs ys -> xs `union` ys == ys `union` (xs :: [Int]) diff --git a/bench/lazy-sc/overflow.hs b/bench/lazy-sc/overflow.hs new file mode 100644 --- /dev/null +++ b/bench/lazy-sc/overflow.hs @@ -0,0 +1,30 @@ +{-# LANGUAGE TemplateHaskell, DeriveDataTypeable #-} +import Test.LazySmallCheck2012 +import Test.LazySmallCheck2012.TH +import Data.Int +import Data.Data +import Data.Typeable + +type I = [Int16] +data T = T I I I I I + deriving (Show, Data, Typeable) + +toList :: T -> [[Int16]] +toList (T i j k l m) = [i,j,k,l,m] + +pre :: T -> Bool +pre t = all ((< 256) . sum) (toList t) + +post :: T -> Bool +post t = (sum . concat) (toList t) < 5 * 256 + +prop :: T -> Bool +prop t = pre t ==> post t + +instance Serial Int16 where + series = drawnFrom $ \d -> map fromIntegral [(-d)..d] + +deriveSerial ''T + +main :: IO () +main = test prop diff --git a/bench/lazy-sc/parser.hs b/bench/lazy-sc/parser.hs new file mode 100644 --- /dev/null +++ b/bench/lazy-sc/parser.hs @@ -0,0 +1,328 @@ +-- Example taken from Lee Pike's SmartCheck: +-- https://github.com/leepike/SmartCheck/blob/master/paper/paper.pdf +-- https://github.com/leepike/smartcheck +{-# LANGUAGE CPP #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} + +-- | Toy "parser"/"serializer" (with a bug) in And parsing. + +module Main where + +import Prelude hiding (showList, mod) + +import Test.LazySmallCheck2012 +import Test.LazySmallCheck2012.TH + +import System.Environment + +import Data.List + +import GHC.Generics +import Data.Typeable +import Control.Applicative + +import Control.Monad.Trans.State +import Data.Char + +import Data.Data +import Data.Typeable + +----------------------------------------------------------------- + +-- Let's make up a toy language. + +data Lang = Lang + { modules :: [Mod] + , funcs :: [Func] + } deriving (Show, Read, Data, Typeable, Generic, Eq, Ord) + +newtype Var = Var String + deriving (Show, Read, Data, Typeable, Generic, Eq, Ord) + +data Mod = Mod + { imports :: [Var] + , exports :: [Var] + } deriving (Show, Read, Data, Typeable, Generic, Eq, Ord) + +data Func = Func + { fnName :: Var + , args :: [Exp] + , stmts :: [Stmt] + } deriving (Show, Read, Data, Typeable, Generic, Eq, Ord) + +data Stmt = Assign Var Exp + | Alloc Var Exp + | Return Exp + -- | Ref Exp + -- | Deref Exp + -- | Assert Exp + -- | Loop Exp [Stmt] + -- | IfTE Exp [Stmt] [Stmt] + deriving (Show, Read, Data, Typeable, Generic, Eq, Ord) + +data Exp = Int Int + | Bool Bool + | Add Exp Exp + | Sub Exp Exp + | Mul Exp Exp + | Div Exp Exp + | Not Exp + | And Exp Exp + | Or Exp Exp + deriving (Show, Read, Data, Typeable, Generic, Eq, Ord) + +-------------------------------------------------------------------------------- + +instance Serial Var where + series = drawnFrom $ \d -> take (d + 1) $ map (Var . (:[])) ['a'..'z'] + +deriveSerial ''Lang +deriveSerial ''Mod +deriveSerial ''Func +deriveSerial ''Exp +deriveSerial ''Stmt + +-------------------------------------------------------------------------------- +-- "serializer" + +parens :: String -> String +parens a = '(' : a ++ ")" + +showList :: Show' a => Char -> [a] -> String +showList sep ls = parens $ concat $ intersperse [sep] $ map show' ls + +class Show a => Show' a where + show' :: a -> String + show' = show + +instance Show' Char +instance Show' Int +instance Show' Bool + +instance Show' Lang where + show' (Lang m f) = unwords + [ "Lang" + , showList ';' m + , showList ';' f + ] + +instance Show' Mod where + show' (Mod i e) = unwords + [ "Mod" + , showList ':' i + , showList ':' e + ] + +instance Show' Func where + show' (Func f a s) = unwords + [ "Func" + , show' f + , showList ',' a + , showList ',' s + ] + +instance Show' Var where + show' (Var v) = v + +instance Show' Stmt where + show' stmt = unwords $ case stmt of + Assign v e -> ["Assign", show' v, parens $ show' e] + Alloc v e -> ["Alloc" , show' v, parens $ show' e] + Return e -> ["Return", parens $ show' e] + +instance Show' Exp where + show' e = unwords $ case e of + Int i -> ["Int" , show' i] + Bool b -> ["Bool", show' b] + Add e0 e1 -> ["Add" , parens $ show' e0, parens $ show' e1] + Sub e0 e1 -> ["Sub" , parens $ show' e0, parens $ show' e1] + Mul e0 e1 -> ["Mul" , parens $ show' e0, parens $ show' e1] + Div e0 e1 -> ["Div" , parens $ show' e0, parens $ show' e1] + Not e0 -> ["Not" , parens $ show' e0] + And e0 e1 -> ["And" , parens $ show' e0, parens $ show' e1] + Or e0 e1 -> ["Or" , parens $ show' e0, parens $ show' e1] + +-------------------------------------------------------------------------------- +-- "parser" + +class Read a => Read' a where + read' :: String -> a + read' = read + +instance Read' Lang where + read' str = run str $ do + modify (strip "Lang") + m <- state unparens + let ms = map read' (fromSeps ';' m) + f <- state unparens + let fs = map read' (fromSeps ';' f) + return (Lang ms fs) + +instance Read' Mod where + read' mod = run mod $ do + modify (strip "Mod") + m <- state unparens + let i = fromSeps ':' m + es <- state unparens + let e = fromSeps ':' es + return (Mod (map Var i) (map Var e)) + +instance Read' Func where + read' f = run f $ do + modify (strip "Func") + n <- state (procWord id) + as <- state unparens + let ars = map read' (fromSeps ',' as) + ss <- state unparens + let sts = map read' (fromSeps ',' ss) + return (Func (Var n) ars sts) + +instance Read' Stmt where + read' stmt | isPrefixOf "Assign" stmt = run stmt $ do + modify (strip "Assign") + v <- state (procWord id) + e <- state (procParens read') + return (Assign (Var v) e) + | isPrefixOf "Alloc" stmt = run stmt $ do + modify (strip "Alloc") + v <- state (procWord id) + e <- state (procParens read') + return (Alloc (Var v) e) + | isPrefixOf "Return" stmt = run stmt $ do + modify (strip "Return") + e <- state (procParens read') + return (Return e) + | otherwise = error $ "Couldn't match stmt " ++ stmt + +instance Read' Exp where + read' e | isPrefixOf "Int" e = Int (read $ strip "Int" e) + | isPrefixOf "Bool" e = Bool (read $ strip "Bool" e) + | isPrefixOf "Add" e = run e $ do + modify (strip "Add") + e0 <- state (procParens read') + e1 <- state (procParens read') + return (Add e0 e1) + + | isPrefixOf "Sub" e = run e $ do + modify (strip "Sub") + e0 <- state (procParens read') + e1 <- state (procParens read') + return (Sub e0 e1) + + | isPrefixOf "Mul" e = run e $ do + modify (strip "Mul") + e0 <- state (procParens read') + e1 <- state (procParens read') + return (Mul e0 e1) + + | isPrefixOf "Div" e = run e $ do + modify (strip "Div") + e0 <- state (procParens read') + e1 <- state (procParens read') + return (Div e0 e1) + + | isPrefixOf "Not" e = run e $ do + modify (strip "Not") + e0 <- state (procParens read') + return (Not e0) + + | isPrefixOf "And" e = run e $ do + modify (strip "And") + e0 <- state (procParens read') + e1 <- state (procParens read') + -- XXX Bug! + return (And e1 e0) + | isPrefixOf "Or" e = run e $ do + modify (strip "Or") + e0 <- state (procParens read') + e1 <- state (procParens read') + -- XXX Bug! + return (And e1 e0) + | otherwise = error $ "Couldn't match exp " ++ e + +-------------------------------------------------------------------------------- + +run :: s -> State s a -> a +run e m = (flip evalState) e m + +-- strip a prefix and a space from a string. Return the remainder of the +-- string. +strip :: String -> String -> String +strip pre str = case stripPrefix pre str of + Nothing -> error $ "Couldn't strip " ++ pre ++ " from " ++ str + Just rst -> if null rst then rst else tail rst + +-- Strip the next word. +stripWord :: String -> (String, String) +stripWord str = let strs = words str in + (head strs, unwords (tail strs)) + + +procWord :: (String -> a) -> String -> (a, String) +procWord = runProc stripWord + +-- Return a prefix inside parens and the remainder of a string. +unparens :: String -> (String, String) +unparens ('(':str) = unparens' (1::Integer) [] str + where + unparens' n s ('(':r) = unparens' (n+1) ('(':s) r + unparens' n s (')':r) | n == 1 = (reverse s, strip "" r) + | otherwise = unparens' (n-1) (')':s) r + unparens' _ _ [] = error $ "End of string reached in unparens" + unparens' n s (c:r) = unparens' n (c:s) r +unparens str = error $ "Unparsens couldn't parse " ++ str + +procParens :: (String -> a) -> String -> (a, String) +procParens = runProc unparens + +-- Parse up to a sep +fromSep :: Char -> String -> (String, String) +fromSep sep str = let pre = takeWhile (/= sep) str in + let post = drop (length pre + 1) str in + (pre, post) + +fromSeps :: Char -> String -> [String] +fromSeps _ [] = [] +fromSeps sep str = let (a, b) = fromSep sep str in + let as = fromSeps sep b in + a:as + +runProc :: (String -> (String, String)) + -> (String -> a) + -> String + -> (a, String) +runProc t f s = let (a, b) = t s in (f a, b) + +-------------------------------------------------------------------------------- + +size :: Lang -> Int +size (Lang m f) = sumit sizem m + sumit sizef f + where + sizem (Mod is es) = length is + length es + sizef (Func _ as sts) = sumit sizee as + sumit sizes sts + sizes stmt = case stmt of + Assign _ e -> 1 + sizee e + Alloc _ e -> 1 + sizee e + Return e -> 1 + sizee e + sizee e = case e of + Int _ -> 1 + Bool _ -> 1 + Add e0 e1 -> 1 + sizee e0 + sizee e1 + Sub e0 e1 -> 1 + sizee e0 + sizee e1 + Mul e0 e1 -> 1 + sizee e0 + sizee e1 + Div e0 e1 -> 1 + sizee e0 + sizee e1 + Not e0 -> 1 + sizee e0 + And e0 e1 -> 1 + sizee e0 + sizee e1 + Or e0 e1 -> 1 + sizee e0 + sizee e1 + sumit sz ls = sum (map sz ls) + +-------------------------------------------------------------------------------- + +prop_parse :: Lang -> Bool +prop_parse e = read' (show' e) == e + +main :: IO () +main = do + test prop_parse diff --git a/bench/lazy-sc/revision.txt b/bench/lazy-sc/revision.txt new file mode 100644 --- /dev/null +++ b/bench/lazy-sc/revision.txt @@ -0,0 +1,2 @@ +b5d9b460833ca34b1b57d5578cb57ee70905a0af +2014-07-07 15:44:24 +0100 diff --git a/bench/lazy-sc/sorting.hs b/bench/lazy-sc/sorting.hs new file mode 100644 --- /dev/null +++ b/bench/lazy-sc/sorting.hs @@ -0,0 +1,23 @@ +import Test.LazySmallCheck2012 + +sort :: Ord a => [a] -> [a] +sort [] = [] +sort (x:xs) = sort (filter (< x) xs) + ++ [x] + ++ sort (filter (> x) xs) + +prop_sortOrdered :: Ord a => [a] -> Bool +prop_sortOrdered xs = ordered (sort xs) + where + ordered (x:y:xs) = x <= y && ordered (y:xs) + ordered _ = True + +prop_sortCount :: Ord a => a -> [a] -> Bool +prop_sortCount x xs = count x (sort xs) == count x xs + +count :: Eq a => a -> [a] -> Int +count x = length . filter (== x) + +main :: IO () +main = do + test (prop_sortCount :: Int -> [Int] -> Bool) diff --git a/bench/lazy-sc/word-refinements.hs b/bench/lazy-sc/word-refinements.hs new file mode 100644 --- /dev/null +++ b/bench/lazy-sc/word-refinements.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE DeriveDataTypeable #-} +-- Copyright (c) 2017 Colin Runciman and Rudy Matela Braquehais. +-- Distributed under the 3-Clause BSD licence (see the file LICENSE). +import Test.LazySmallCheck2012 +import Test.LazySmallCheck2012.TH +import Data.Data +import Data.Typeable + +import Data.List +import Data.Char + +-- LazySmallCheck2012's Char enumeration does not contain spaces. So we have +-- to create types to manually include them. + +newtype CharS = CharS { unCharS :: Char } + deriving (Eq, Ord, Data, Typeable) + +newtype StringS = StringS { unStringS :: String } + deriving (Eq, Ord, Data, Typeable) + +instance Show CharS where + show (CharS c) = show c + +instance Show StringS where + show (StringS s) = show s + +instance Serial CharS where + series = drawnFrom $ \d -> map CharS . take (d + 1) $ ' ':['a'..] + +instance Serial StringS where + series = (StringS . map unCharS) <$> series + +prop_lengthWords0 :: String -> Bool +prop_lengthWords0 s = s /= "" + ==> length (words s) == length (filter isSpace s) + 1 + +prop_lengthWords1 :: String -> Bool +prop_lengthWords1 s = s /= "" && not (isSpace (head s)) + && not (isSpace (last s)) + ==> length (words s) == length (filter isSpace s) + 1 + +prop_lengthWords2 :: String -> Bool +prop_lengthWords2 s = noLeadingTrailingOrDoubleSpace s + ==> length (words s) == length (filter isSpace s) + 1 + where + noLeadingTrailingOrDoubleSpace s = and [ not (isSpace a && isSpace b) + | let s' = " " ++ s ++ " " + , (a,b) <- zip s' (tail s') ] + +main :: IO () +main = do + test (prop_lengthWords0 . unStringS) +--test (prop_lengthWords1 . unStringS) +--test prop_lengthWords0 +--test prop_lengthWords1 diff --git a/bench/ord.hs b/bench/ord.hs new file mode 100644 --- /dev/null +++ b/bench/ord.hs @@ -0,0 +1,66 @@ +import Test.Extrapolate +import Data.List +import Data.Typeable (typeOf) + +main :: IO () +main = do + ch () + ch bool + ch int + ch integer + ch char + ch ordering + +--ch [()] + ch [bool] +--chint + ch [integer] +--ch [char] +--ch [ordering] + +--ch ((),int) + ch (bool,char) +--ch (int,(),bool) + ch (ordering,char,integer) + + ch (mayb ()) + ch (mayb int) + + ch (eith () bool) + ch (eith int char) + +-- TODO: find out why output for the following is different across diff GHCs +-- see: https://travis-ci.org/rudymatela/extrapolate/jobs/263425540 +-- ch (char,int,bool,ordering) + +-- For some reason, output for the following funky types is different across +-- different versions of GHC, see: +-- https://travis-ci.org/rudymatela/extrapolate/builds/262325825 +-- I don't have time to investigate now, but it might be good to check why. +--ch (eith integer ordering,mayb (int,(),bool),mayb (char,())) +--ch (eith (integer,mayb (int,(),bool),mayb (char,())) (int,char)) + +ch :: (Ord a, Generalizable a) => a -> IO () +ch x = do + putStrLn $ "checks :: " ++ show (typeOf x) ++ "\n" + check `withConditionSize` 3 $ (<) -:> x + check `withConditionSize` 3 $ (>) -:> x + check `withConditionSize` 3 $ (<=) -:> x + check `withConditionSize` 3 $ (>=) -:> x + putStrLn "" + +chint :: IO () +chint = do + -- TODO: make the following work on GHC >= 8.2 + -- see https://travis-ci.org/rudymatela/extrapolate/jobs/266773179 + -- possible less temporary solution: + -- * Add (==) (/=) (<=) (<) (>=) (>) to list background. + -- update, adding the above on background does not seem to solve the problem. + -- maybe after improving the algorithm to generate the *weakest* condition, + -- instead of just the first with 10% truth. + -- ch [int] + putStrLn $ "checks :: " ++ show (typeOf [int]) ++ "\n" + check `withConditionSize` 3 $ (<) -:> [int] + check `withConditionSize` 3 $ (>) -:> [int] + check `withConditionSize` 3 $ (>=) -:> [int] + putStrLn "" diff --git a/bench/runtime/oubli/bench/diff.runtime b/bench/runtime/oubli/bench/diff.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/bench/diff.runtime @@ -0,0 +1,1 @@ +16.30 diff --git a/bench/runtime/oubli/bench/eq.runtime b/bench/runtime/oubli/bench/eq.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/bench/eq.runtime @@ -0,0 +1,1 @@ +1.02 diff --git a/bench/runtime/oubli/bench/false.runtime b/bench/runtime/oubli/bench/false.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/bench/false.runtime @@ -0,0 +1,1 @@ +2.90 diff --git a/bench/runtime/oubli/bench/ord.runtime b/bench/runtime/oubli/bench/ord.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/bench/ord.runtime @@ -0,0 +1,1 @@ +6.29 diff --git a/bench/runtime/oubli/bench/true.runtime b/bench/runtime/oubli/bench/true.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/bench/true.runtime @@ -0,0 +1,1 @@ +0.18 diff --git a/bench/runtime/oubli/eg/calculator.runtime b/bench/runtime/oubli/eg/calculator.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/calculator.runtime @@ -0,0 +1,1 @@ +1.60 diff --git a/bench/runtime/oubli/eg/gencalc.runtime b/bench/runtime/oubli/eg/gencalc.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/gencalc.runtime @@ -0,0 +1,1 @@ +1.95 diff --git a/bench/runtime/oubli/eg/heap.runtime b/bench/runtime/oubli/eg/heap.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/heap.runtime @@ -0,0 +1,1 @@ +7.02 diff --git a/bench/runtime/oubli/eg/int.runtime b/bench/runtime/oubli/eg/int.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/int.runtime @@ -0,0 +1,1 @@ +0.48 diff --git a/bench/runtime/oubli/eg/list.runtime b/bench/runtime/oubli/eg/list.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/list.runtime @@ -0,0 +1,1 @@ +4.06 diff --git a/bench/runtime/oubli/eg/overflow.runtime b/bench/runtime/oubli/eg/overflow.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/overflow.runtime @@ -0,0 +1,1 @@ +0.18 diff --git a/bench/runtime/oubli/eg/overflow8.runtime b/bench/runtime/oubli/eg/overflow8.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/overflow8.runtime @@ -0,0 +1,1 @@ +17.21 diff --git a/bench/runtime/oubli/eg/parser.runtime b/bench/runtime/oubli/eg/parser.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/parser.runtime @@ -0,0 +1,1 @@ +1.80 diff --git a/bench/runtime/oubli/eg/redblack.runtime b/bench/runtime/oubli/eg/redblack.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/redblack.runtime @@ -0,0 +1,1 @@ +0.09 diff --git a/bench/runtime/oubli/eg/sorting.runtime b/bench/runtime/oubli/eg/sorting.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/sorting.runtime @@ -0,0 +1,1 @@ +13.48 diff --git a/bench/runtime/oubli/eg/word-refinements.runtime b/bench/runtime/oubli/eg/word-refinements.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/oubli/eg/word-refinements.runtime @@ -0,0 +1,1 @@ +41.38 diff --git a/bench/runtime/zero/bench/diff.runtime b/bench/runtime/zero/bench/diff.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/diff.runtime @@ -0,0 +1,1 @@ +7.05 diff --git a/bench/runtime/zero/bench/eq.runtime b/bench/runtime/zero/bench/eq.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/eq.runtime @@ -0,0 +1,1 @@ +27.25 diff --git a/bench/runtime/zero/bench/false.runtime b/bench/runtime/zero/bench/false.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/false.runtime @@ -0,0 +1,1 @@ +6.47 diff --git a/bench/runtime/zero/bench/ord.runtime b/bench/runtime/zero/bench/ord.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/ord.runtime @@ -0,0 +1,1 @@ +13.25 diff --git a/bench/runtime/zero/bench/true.runtime b/bench/runtime/zero/bench/true.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/true.runtime @@ -0,0 +1,1 @@ +0.08 diff --git a/bench/runtime/zero/eg/calculator.runtime b/bench/runtime/zero/eg/calculator.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/calculator.runtime @@ -0,0 +1,1 @@ +0.79 diff --git a/bench/runtime/zero/eg/gencalc.runtime b/bench/runtime/zero/eg/gencalc.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/gencalc.runtime @@ -0,0 +1,1 @@ +0.71 diff --git a/bench/runtime/zero/eg/heap.runtime b/bench/runtime/zero/eg/heap.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/heap.runtime @@ -0,0 +1,1 @@ +4.29 diff --git a/bench/runtime/zero/eg/int.runtime b/bench/runtime/zero/eg/int.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/int.runtime @@ -0,0 +1,1 @@ +4.18 diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/list.runtime @@ -0,0 +1,1 @@ +10.17 diff --git a/bench/runtime/zero/eg/overflow.runtime b/bench/runtime/zero/eg/overflow.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/overflow.runtime @@ -0,0 +1,1 @@ +0.21 diff --git a/bench/runtime/zero/eg/overflow8.runtime b/bench/runtime/zero/eg/overflow8.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/overflow8.runtime @@ -0,0 +1,1 @@ +7.16 diff --git a/bench/runtime/zero/eg/parser.runtime b/bench/runtime/zero/eg/parser.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/parser.runtime @@ -0,0 +1,1 @@ +8.91 diff --git a/bench/runtime/zero/eg/redblack.runtime b/bench/runtime/zero/eg/redblack.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/redblack.runtime @@ -0,0 +1,1 @@ +0.02 diff --git a/bench/runtime/zero/eg/sorting.runtime b/bench/runtime/zero/eg/sorting.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/sorting.runtime @@ -0,0 +1,1 @@ +12.02 diff --git a/bench/runtime/zero/eg/word-refinements.runtime b/bench/runtime/zero/eg/word-refinements.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/word-refinements.runtime @@ -0,0 +1,1 @@ +11.42 diff --git a/bench/smartcheck/Makefile b/bench/smartcheck/Makefile new file mode 100644 --- /dev/null +++ b/bench/smartcheck/Makefile @@ -0,0 +1,102 @@ +GHC=ghc +GHCI=ghci +BENCH= \ + sorting \ + parser \ + list \ + overflow \ + word-refinements \ + div0 +TYM= \ + /usr/bin/time "-f%e %M" +SMARTCHECK=https://github.com/leepike/SmartCheck +#SMARTCHECK=$(HOME)/prj/smartcheck + +all: $(BENCH) + +bench: all + @- yes | $(TYM) ./div0 + @- yes | $(TYM) ./parser + @- yes | $(TYM) ./sorting + @- yes | $(TYM) ./list + @- yes | $(TYM) ./overflow + @- yes | $(TYM) ./word-refinements + +bench-sorting: sorting + mkdir -p $<-out + for i in {00..99}; do \ + yes | \ + /usr/bin/time "-f%e %M" ./$< > $<-out/$$i; \ + done 2> $<.runtime + +bench-sorting-swap: sorting + mkdir -p $<-swap-out + for i in {00..99}; do \ + yes | \ + /usr/bin/time "-f%e %M" ./$< swap > $<-swap-out/$$i; \ + done 2> $<-swap.runtime + +bench-sorting-uncurry: sorting + mkdir -p $<-uncurry-out + for i in {000..999}; do \ + yes | \ + /usr/bin/time "-f%e %M" ./$< uncurry | \ + grep -A2 -E "(^forall values|OK, passed)" > $<-uncurry-out/$$i; \ + done 2> $<-uncurry.runtime + +bench-parser: parser + mkdir -p $<-out + for i in {000..999}; do \ + yes | \ + /usr/bin/time "-f%e %M" ./$< | \ + grep "^Lang" > $<-out/$$i; \ + done 2> $<.runtime + +bench-overflow: overflow + mkdir -p $<-out + for i in {000..999}; do \ + yes | \ + /usr/bin/time "-f%e %M" ./$< | \ + grep -A2 "^forall values" > $<-out/$$i; \ + done 2> $<.runtime + +bench-div0: div0 + mkdir -p div0-out + for i in {000..999}; do yes | /usr/bin/time "-f%e %M" ./div0 | grep -A3 forall > div0-out/$$i; done 2> div0.runtime + +bench-word-refinements: word-refinements + mkdir -p $<-out + for i in {000..999}; do \ + yes | /usr/bin/time "-f%e %M" ./$< | \ + grep -A2 -E "(^forall values|OK, passed)" > $<-out/$$i; \ + done 2> $<.runtime + +div0.hs: div0-main.hs smartcheck/regression/Div0/Div0.hs + cat smartcheck/regression/Div0/Div0.hs div0-main.hs > div0.hs + +parser.hs: parser-main.hs smartcheck/regression/Parser/Parser.hs + cat smartcheck/regression/Parser/Parser.hs parser-main.hs > parser.hs + +overflow.hs: overflow-main.hs smartcheck/regression/PaperExample1/PaperExample1.hs + cat smartcheck/regression/PaperExample1/PaperExample1.hs overflow-main.hs > overflow.hs + +overflow: overflow.hs + +%: %.hs + $(GHC) -dynamic -O2 -ignore-package QuickCheck-2.10.1 -package-db .cabal-sandbox/*-$(GHC)*-packages.conf.d $< && touch $@ + +%.ghci: %.hs + $(GHCI) -dynamic -package-db .cabal-sandbox/*-$(GHC)*-packages.conf.d $< + +prepare: + git clone $(SMARTCHECK) smartcheck + git -C smartcheck show -s --format="%H%n%ci" | tee revision.txt + cabal sandbox init + cabal sandbox add-source smartcheck + cabal install smartcheck + +clean: + rm -f $(BENCH) *.hi *.o div0.hs parser.hs overflow.hs + +clean-prepare: + rm -rf .cabal-sandbox cabal.sandbox.config smartcheck diff --git a/bench/smartcheck/bin/count-cons b/bench/smartcheck/bin/count-cons new file mode 100644 --- /dev/null +++ b/bench/smartcheck/bin/count-cons @@ -0,0 +1,29 @@ +#!/bin/bash +# +# counts the number of constructors for the parser eg +cat parser-out/* | +sed "s/[{,][a-zA-Z ]*=//g;s/}//g" | # remove record notation +# cat; exit # for things without record notation +sed "s/[()]//g" | # remove parentheses +sed "s/\[]/Nil/g" | # [] becomes Nil +sed "s/\[/[ /g;s/]/ ]/g;s/,/ , /g" | # spaces around [ , ] +sed 's/\\[0-9]*/0/g' | # \123 becomes 0 +sed 's/""/E/g' | # "" becomes E +sed 's/"."/C : E/g' | # "c" becomes C : E +sed 's/".."/C : C : E/g' | # "cc" becomes C : C : E +sed 's/"..."/C : C : C : E/g' | +sed 's/"...."/C : C : C : C : E/g' | +sed 's/"....."/C : C : C : C : C : E/g' | +sed 's/"......"/C : C : C : C : C : C : E/g' | +sed 's/"......."/C : C : C : C : C : C : C : E/g' | +sed 's/"........"/C : C : C : C : C : C : C : C : E/g' | +sed 's/"........."/C : C : C : C : C : C : C : C : C : E/g' | +sed 's/".........."/C : C : C : C : C : C : C : C : C : C : E/g' | +sed 's/"..........."/C : C : C : C : C : C : C : C : C : C : C : E/g' | +sed 's/"............"/C : C : C : C : C : C : C : C : C : C : C : C : E/g' | +sed 's/"............."/C : C : C : C : C : C : C : C : C : C : C : C : C : E/g' | +#wc -w; exit # for total count of words (divide by 100 for the mean) +while read conses +do + echo $conses | wc -w +done diff --git a/bench/smartcheck/bin/ncons-overflow b/bench/smartcheck/bin/ncons-overflow new file mode 100644 --- /dev/null +++ b/bench/smartcheck/bin/ncons-overflow @@ -0,0 +1,7 @@ +#!/bin/bash +tail -n -1 -q overflow-out/* | +#wc -w; exit +while read s +do + echo $s | wc -w +done diff --git a/bench/smartcheck/bin/nvars-overflow b/bench/smartcheck/bin/nvars-overflow new file mode 100644 --- /dev/null +++ b/bench/smartcheck/bin/nvars-overflow @@ -0,0 +1,8 @@ +#!/bin/bash +head -1 -q overflow-out/* | +sed -e "s/forall values//" | +#wc -w; exit +while read s +do + echo $s | wc -w +done diff --git a/bench/smartcheck/bin/sort-stats b/bench/smartcheck/bin/sort-stats new file mode 100644 --- /dev/null +++ b/bench/smartcheck/bin/sort-stats @@ -0,0 +1,4 @@ +#!/bin/bash +# +# stats for sort +tail -qn -1 sorting-uncurry-out/* | sed -e "s/[^:]//g" | sort diff --git a/bench/smartcheck/div0-main.hs b/bench/smartcheck/div0-main.hs new file mode 100644 --- /dev/null +++ b/bench/smartcheck/div0-main.hs @@ -0,0 +1,4 @@ +-- main function for Div0 + +main :: IO () +main = divTest diff --git a/bench/smartcheck/list.hs b/bench/smartcheck/list.hs new file mode 100644 --- /dev/null +++ b/bench/smartcheck/list.hs @@ -0,0 +1,8 @@ +import Test.SmartCheck +import Test.QuickCheck +import Data.List + +main :: IO () +main = do + quickCheck $ \xs -> nub xs == (xs :: [Int]) + smartCheck scStdArgs{format = PrintString} $ \xs -> nub xs == (xs :: [Int]) diff --git a/bench/smartcheck/overflow-main.hs b/bench/smartcheck/overflow-main.hs new file mode 100644 --- /dev/null +++ b/bench/smartcheck/overflow-main.hs @@ -0,0 +1,8 @@ +-- main for paperExample1 + +instance SubTypes I +instance SubTypes T + +main :: IO () +main = do + smartCheck scStdArgs{format = PrintString} prop diff --git a/bench/smartcheck/parser-main.hs b/bench/smartcheck/parser-main.hs new file mode 100644 --- /dev/null +++ b/bench/smartcheck/parser-main.hs @@ -0,0 +1,4 @@ +-- parse main + +main :: IO () +main = smartCheck scargs prop_parse diff --git a/bench/smartcheck/revision.txt b/bench/smartcheck/revision.txt new file mode 100644 --- /dev/null +++ b/bench/smartcheck/revision.txt @@ -0,0 +1,2 @@ +86bfe4a3f61bfd74fa79e1afb9b5a77d4ad58efb +2017-08-11 13:08:58 -0700 diff --git a/bench/smartcheck/sorting.hs b/bench/smartcheck/sorting.hs new file mode 100644 --- /dev/null +++ b/bench/smartcheck/sorting.hs @@ -0,0 +1,35 @@ +import Test.SmartCheck +import System.Environment (getArgs) + +sort :: Ord a => [a] -> [a] +sort [] = [] +sort (x:xs) = sort (filter (< x) xs) + ++ [x] + ++ sort (filter (> x) xs) + +prop_sortOrdered :: Ord a => [a] -> Bool +prop_sortOrdered xs = ordered (sort xs) + where + ordered (x:y:xs) = x <= y && ordered (y:xs) + ordered _ = True + +prop_sortCount :: Ord a => a -> [a] -> Bool +prop_sortCount x xs = count x (sort xs) == count x xs + +count :: Eq a => a -> [a] -> Int +count x = length . filter (== x) + +main :: IO () +main = do + as <- getArgs + case as of + ("uncurry":_) -> smartCheck scStdArgs { format = PrintString + , runExists = False } + (uncurry prop_sortCount :: (Int,[Int]) -> Bool) + ("swap":_) -> smartCheck scStdArgs { format = PrintString + , runExists = False } + (flip prop_sortCount :: [Int] -> Int -> Bool) + _ -> putStrLn "no longer works... (see source)" +-- _ -> smartCheck scStdArgs { format = PrintString +-- , runExists = False } +-- (prop_sortCount :: Int -> [Int] -> Bool) diff --git a/bench/smartcheck/word-refinements.hs b/bench/smartcheck/word-refinements.hs new file mode 100644 --- /dev/null +++ b/bench/smartcheck/word-refinements.hs @@ -0,0 +1,28 @@ +-- Copyright (c) 2017 Colin Runciman and Rudy Matela Braquehais. +-- Distributed under the 3-Clause BSD licence (see the file LICENSE). +import Test.SmartCheck +import Test.QuickCheck +import Data.List +import Data.Char + +prop_lengthWords0 :: String -> Property +prop_lengthWords0 s = s /= "" + ==> length (words s) == length (filter isSpace s) + 1 + +prop_lengthWords1 :: String -> Property +prop_lengthWords1 s = s /= "" && not (isSpace (head s)) + && not (isSpace (last s)) + ==> length (words s) == length (filter isSpace s) + 1 + +prop_lengthWords2 :: String -> Property +prop_lengthWords2 s = noLeadingTrailingOrDoubleSpace s + ==> length (words s) == length (filter isSpace s) + 1 + where + noLeadingTrailingOrDoubleSpace s = and [ not (isSpace a && isSpace b) + | let s' = " " ++ s ++ " " + , (a,b) <- zip s' (tail s') ] + +main :: IO () +main = do + smartCheck scStdArgs{format = PrintString} prop_lengthWords0 +--smartCheck scStdArgs{format = PrintString} prop_lengthWords1 diff --git a/bench/true.hs b/bench/true.hs new file mode 100644 --- /dev/null +++ b/bench/true.hs @@ -0,0 +1,50 @@ +import Test.Extrapolate +import Data.List +import Data.Typeable (typeOf) + +main :: IO () +main = do + ch () + ch bool + ch int + ch integer + ch char + ch ordering + + ch [()] + ch [bool] + ch [int] + ch [integer] + ch [char] + ch [ordering] + + ch ((),int) + ch (bool,char) + ch (int,(),bool) + ch (ordering,char,integer) + + ch (mayb ()) + ch (mayb int) + + ch (eith () bool) + ch (eith int char) + +-- TODO: find out why output for the following is different across diff GHCs +-- see: https://travis-ci.org/rudymatela/extrapolate/jobs/263425540 +-- ch (char,int,bool,ordering) + +-- For some reason, output for the following funky types is different across +-- different versions of GHC, see: +-- https://travis-ci.org/rudymatela/extrapolate/builds/262325825 +-- I don't have time to investigate now, but it might be good to check why. +--ch (eith integer ordering,mayb (int,(),bool),mayb (char,())) +--ch (eith (integer,mayb (int,(),bool),mayb (char,())) (int,char)) + + +ch :: (Eq a, Generalizable a) => a -> IO () +ch x = do + putStrLn $ "checks :: " ++ show (typeOf x) ++ "\n" + check $ const True -:> x + check $ (\x y -> True) -:> x ->:> x + check $ (\x y z -> True) -:> x ->:> x ->>:> x + putStrLn "" diff --git a/eg/RedBlackSet.hs b/eg/RedBlackSet.hs new file mode 100644 --- /dev/null +++ b/eg/RedBlackSet.hs @@ -0,0 +1,177 @@ +-- Copyright (c) 2011, IIJ Innovation Institute Inc. +-- All rights reserved. +-- +-- Licensed under a BSD3 style license: +-- https://github.com/kazu-yamamoto/llrbtree +-- https://hackage.haskell.org/package/llrbtree +-- +-- Original implementation by Chris Okasaki. +{-# LANGUAGE DeriveDataTypeable, CPP #-} + +module RedBlackSet where + +import Data.Typeable + +import Prelude hiding (max) + +data Color = + R -- red + | B -- black + | BB -- double black + | NB -- negative black + deriving (Show, Read, Typeable) + +data RBSet a = + E -- black leaf + | EE -- double black leaf + | T Color (RBSet a) a (RBSet a) + deriving (Show, Read, Typeable) + + -- Private auxiliary functions -- + +redden :: RBSet a -> RBSet a +redden E = error "cannot redden empty tree" +redden EE = error "cannot redden empty tree" +redden (T _ a x b) = T R a x b + +blacken :: RBSet a -> RBSet a +blacken E = E +blacken EE = E +blacken (T _ a x b) = T B a x b + +isBB :: RBSet a -> Bool +isBB EE = True +isBB (T BB _ _ _) = True +isBB _ = False + +blacker :: Color -> Color +blacker NB = R +blacker R = B +blacker B = BB +blacker BB = error "too black" + +redder :: Color -> Color +redder NB = error "not black enough" +redder R = NB +redder B = R +redder BB = B + +blacker' :: RBSet a -> RBSet a +blacker' E = EE +blacker' (T c l x r) = T (blacker c) l x r + +redder' :: RBSet a -> RBSet a +redder' EE = E +redder' (T c l x r) = T (redder c) l x r + + -- `balance` rotates away coloring conflicts: +balance :: Color -> RBSet a -> a -> RBSet a -> RBSet a + + -- Okasaki's original cases: +balance B (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d) +balance B (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d) +balance B a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d) +#ifdef BALANCE_BUG +-- even with 2000111 tests, LeanCheck cannot find a counterexample to: +balance B a x (T R b y (T R c z d)) = T R (T B a x b) y (T B d z c) +#else +balance B a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d) +#endif + + -- Six cases for deletion: +balance BB (T R (T R a x b) y c) z d = T B (T B a x b) y (T B c z d) +balance BB (T R a x (T R b y c)) z d = T B (T B a x b) y (T B c z d) +balance BB a x (T R (T R b y c) z d) = T B (T B a x b) y (T B c z d) +balance BB a x (T R b y (T R c z d)) = T B (T B a x b) y (T B c z d) + +balance BB a x (T NB (T B b y c) z d@(T B _ _ _)) + = T B (T B a x b) y (balance B c z (redden d)) +balance BB (T NB a@(T B _ _ _) x (T B b y c)) z d + = T B (balance B (redden a) x b) y (T B c z d) + +balance color a x b = T color a x b + + -- `bubble` "bubbles" double-blackness upward: +bubble :: Color -> RBSet a -> a -> RBSet a -> RBSet a +bubble color l x r + | isBB(l) || isBB(r) = balance (blacker color) (redder' l) x (redder' r) + | otherwise = balance color l x r + + + + + -- Public operations -- + +empty :: RBSet a +empty = E + + +member :: (Ord a) => a -> RBSet a -> Bool +member x E = False +member x (T _ l y r) | x < y = member x l + | x > y = member x r + | otherwise = True + +max :: RBSet a -> a +max E = error "no largest element" +max (T _ _ x E) = x +max (T _ _ x r) = max r + + + -- Insertion: + +insert :: (Ord a) => a -> RBSet a -> RBSet a +insert x s = blacken (ins s) + where ins E = T R E x E + ins s@(T color a y b) | x < y = balance color (ins a) y b + | x > y = balance color a y (ins b) + | otherwise = s + + + -- Deletion: + +delete :: (Ord a,Show a) => a -> RBSet a -> RBSet a +#ifdef DELETE_BUG +delete x s = T B a y b + where del E = E + del s@(T color a y b) | x < y = bubble color (del a) y b + | x > y = bubble color a y (del b) + | otherwise = remove s + T _ a y b = del s +#else +delete x s = blacken(del s) + where del E = E + del s@(T color a y b) | x < y = bubble color (del a) y b + | x > y = bubble color a y (del b) + | otherwise = remove s +#endif + +remove :: RBSet a -> RBSet a +remove E = E +remove (T R E _ E) = E +remove (T B E _ E) = EE +remove (T B E _ (T R a x b)) = T B a x b +remove (T B (T R a x b) _ E) = T B a x b +#ifdef REMOVE_BUG +remove (T color l@(T R a x b) y r) = bubble color l' mx r +#else +remove (T color l y r) = bubble color l' mx r +#endif + where mx = max l + l' = removeMax l + +removeMax :: RBSet a -> RBSet a +removeMax E = error "no maximum to remove" +removeMax s@(T _ _ _ E) = remove s +removeMax s@(T color l x r) = bubble color l x (removeMax r) + + -- Conversion: + +toAscList :: RBSet a -> [a] +toAscList E = [] +toAscList (T _ l x r) = (toAscList l) ++ [x] ++ (toAscList r) + + -- Equality + +instance Eq a => Eq (RBSet a) where + rb == rb' = (toAscList rb) == (toAscList rb') diff --git a/eg/calculator.hs b/eg/calculator.hs new file mode 100644 --- /dev/null +++ b/eg/calculator.hs @@ -0,0 +1,69 @@ +{-# LANGUAGE DeriveDataTypeable, StandaloneDeriving, CPP #-} -- for GHC <= 7.8 +-- Example taken from Lee Pike's SmartCheck: +-- https://github.com/leepike/SmartCheck/blob/master/paper/paper.pdf +-- https://github.com/leepike/smartcheck +-- The version here is the one from the paper (similar to the one in the README +-- file). I chose the one in the paper as it is clearer. +import Control.Monad +import Test.Extrapolate hiding (eval) +import Data.Maybe +import qualified Test.LeanCheck as Lean + +#if __GLASGOW_HASKELL__ < 710 +import Data.Typeable (Typeable) +deriving instance Typeable Exp +#endif + +data Exp = C Int + | Add Exp Exp + | Div Exp Exp + deriving (Eq, Ord, Show) + +eval :: Exp -> Maybe Int +eval (C i) = Just i +eval (Add e0 e1) = + liftM2 (+) (eval e0) (eval e1) +eval (Div e0 e1) = + let e = eval e1 in + if e == Just 0 then Nothing + else liftM2 div (eval e0) e + +-- originally called divSubTerms by Pike +noDiv0 :: Exp -> Bool +noDiv0 (C _) = True +noDiv0 (Div _ (C 0)) = False +noDiv0 (Add e0 e1) = noDiv0 e0 && noDiv0 e1 +noDiv0 (Div e0 e1) = noDiv0 e0 && noDiv0 e1 + +prop_div :: Exp -> Bool +prop_div e = noDiv0 e ==> eval e /= Nothing + +instance Listable Exp where + tiers = cons1 C + \/ cons2 Add + \/ cons2 Div + +-- deriveGeneralizable ''Exp +-- {- +instance Generalizable Exp where + name _ = "e1" + expr (C i) = constant "C" C :$ expr i + expr (Add e1 e2) = constant "Add" Add :$ expr e1 :$ expr e2 + expr (Div e1 e2) = constant "Div" Div :$ expr e1 :$ expr e2 + background e = [ constant "eval" eval + , constant "noDiv0" noDiv0 ] + instances e = this e $ instances (undefined :: Int) +-- -} + + +main :: IO () +main = do + check prop_div + check (isJust . eval) + -- The following generalized counter-example from the paper is wrong! + -- > forall x. Div x (Add (C (-5)) (C 5)) + print $ prop_div (Div (C 0) (C 0 `Add` C 0)) + -- setting x to (Div (C 0) (C 0)) makes the property pass + print $ prop_div (Div (C 0 `Div` C 0) (C 0 `Add` C 0)) + -- As Lee Pike points out, SmartCheck's algorithm is unsound anyway, + -- sometimes returning generalized counter-examples that are *too* general. diff --git a/eg/gencalc.hs b/eg/gencalc.hs new file mode 100644 --- /dev/null +++ b/eg/gencalc.hs @@ -0,0 +1,70 @@ +{-# Language TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable, StandaloneDeriving, CPP #-} -- for GHC <= 7.8 +-- Example taken from Lee Pike's SmartCheck: +-- https://github.com/leepike/SmartCheck/blob/master/paper/paper.pdf +-- https://github.com/leepike/smartcheck +-- The version here is the one from the paper (similar to the one in the README +-- file). I chose the one in the paper as it is clearer. +import Control.Monad +import Test.Extrapolate hiding (eval) +import Data.Maybe + + +#if __GLASGOW_HASKELL__ < 710 +import Data.Typeable (Typeable) +deriving instance Typeable Exp +#endif + +data Exp a = C a + | Add (Exp a) (Exp a) + | Div (Exp a) (Exp a) + deriving (Eq, Ord, Show) + +eval :: Integral a => Exp a -> Maybe a +eval (C i) = Just i +eval (Add e0 e1) = + liftM2 (+) (eval e0) (eval e1) +eval (Div e0 e1) = + let e = eval e1 in + if e == Just 0 then Nothing + else liftM2 div (eval e0) e + +-- originally called divSubTerms by Pike +noDiv0 :: Integral a => Exp a -> Bool +noDiv0 (C _) = True +noDiv0 (Div _ (C 0)) = False +noDiv0 (Add e0 e1) = noDiv0 e0 && noDiv0 e1 +noDiv0 (Div e0 e1) = noDiv0 e0 && noDiv0 e1 + +prop_div :: Integral a => Exp a -> Bool +prop_div e = noDiv0 e ==> eval e /= Nothing + +instance Listable a => Listable (Exp a) where + tiers = cons1 C + \/ cons2 Add + \/ cons2 Div + +-- deriveGeneralizable ''Exp +-- {- +instance Generalizable a => Generalizable (Exp a) where + name _ = "e1" + expr e@(C i) = constant "C" (C ->: e) :$ expr i + expr e@(Add e1 e2) = constant "Add" (Add ->>: e) :$ expr e1 :$ expr e2 + expr e@(Div e1 e2) = constant "Div" (Div ->>: e) :$ expr e1 :$ expr e2 + instances e = this e $ (let C i = C undefined `asTypeOf` e in instances i) +-- -} + +argTypeOf :: (a -> b) -> a -> (a -> b) +argTypeOf f x = f + +main :: IO () +main = do + check (prop_div :: Exp Int -> Bool) + check ((isJust . eval) :: Exp Int -> Bool) + -- The following generalized counter-example from the paper is wrong! + -- > forall x. Div x (Add (C (-5)) (C 5)) + print $ prop_div (Div (C 0) (C 0 `Add` C 0)) + -- setting x to (Div (C 0) (C 0)) makes the property pass + print $ prop_div (Div (C 0 `Div` C 0) (C 0 `Add` C 0)) + -- As Lee Pike points out, SmartCheck's algorithm is unsound anyway, + -- sometimes returning generalized counter-examples that are *too* general. diff --git a/eg/heap.hs b/eg/heap.hs new file mode 100644 --- /dev/null +++ b/eg/heap.hs @@ -0,0 +1,181 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable, StandaloneDeriving, CPP #-} -- for GHC <= 7.8 + +-- Copied from SmartCheck's examples, +-- Which in turn was, +-- Copied from QuickCheck2's examples. + +import System.Environment +import Data.List (sort) +import Data.Typeable +import Test.Extrapolate +import qualified Test.LeanCheck as Lean +import Test.LeanCheck.Utils + +#if __GLASGOW_HASKELL__ < 710 +import Data.Typeable (Typeable) +deriving instance Typeable Heap +deriving instance Typeable HeapP +deriving instance Typeable HeapPP +#endif + + +instance (Ord a, Listable a) => Listable (Heap a) where + tiers = cons1 heap + +instance (Ord a, Generalizable a) => Generalizable (Heap a) where + name _ = "h" + expr h = constant "fromList" (fromList ->: h) :$ expr (toList h) + background h = [ constant "size" $ size -:> h ] + instances h = this h $ instances (toList h) + + +data Heap a + = Node a (Heap a) (Heap a) + | Nil + deriving (Eq, Ord, Show, Read) + +empty :: Heap a +empty = Nil + +isEmpty :: Heap a -> Bool +isEmpty Nil = True +isEmpty _ = False + +unit :: a -> Heap a +unit x = Node x empty empty + +size :: Heap a -> Int +size Nil = 0 +size (Node _ h1 h2) = 1 + size h1 + size h2 + +insert :: Ord a => a -> Heap a -> Heap a +insert x h = unit x `merge` h + +removeMin :: Ord a => Heap a -> Maybe (a, Heap a) +removeMin Nil = Nothing +removeMin (Node x h1 h2) = Just (x, h1 `merge` h2) + +merge :: Ord a => Heap a -> Heap a -> Heap a +h1 `merge` Nil = h1 +Nil `merge` h2 = h2 +h1@(Node x h11 h12) `merge` h2@(Node y h21 h22) + | x <= y = Node x (h12 `merge` h2) h11 + | otherwise = Node y (h22 `merge` h1) h21 + +fromList :: Ord a => [a] -> Heap a +fromList xs = merging [ unit x | x <- xs ] + where + merging [] = empty + merging [h] = h + merging hs = merging (sweep hs) + + sweep [] = [] + sweep [h] = [h] + sweep (h1:h2:hs) = (h1 `merge` h2) : sweep hs + +toList :: Heap a -> [a] +toList h = toList' [h] + where + toList' [] = [] + toList' (Nil : hs) = toList' hs + toList' (Node x h1 h2 : hs) = x : toList' (h1:h2:hs) + +toSortedList :: Ord a => Heap a -> [a] +toSortedList Nil = [] +toSortedList (Node x h1 h2) = x : toList (h1 `merge` h2) +-- above, toList should instead read toSortedList + + +data HeapP a + = Empty + | Unit a + | Insert a (HeapP a) + | SafeRemoveMin (HeapP a) + | Merge (HeapP a) (HeapP a) + | FromList [a] + deriving (Show, Read) + +heap :: Ord a => HeapP a -> Heap a +heap Empty = empty +heap (Unit x) = unit x +heap (Insert x p) = insert x (heap p) +heap (SafeRemoveMin p) = case removeMin (heap p) of + Nothing -> empty -- arbitrary choice + Just (_,h) -> h +heap (Merge p q) = heap p `merge` heap q +heap (FromList xs) = fromList xs + +instance (Listable a) => Listable (HeapP a) where + tiers = cons0 Empty + \/ cons1 Unit + \/ cons2 Insert + \/ cons1 SafeRemoveMin + \/ cons2 Merge + \/ cons1 FromList + +instance (Generalizable a, Typeable a) => Generalizable (HeapP a) where + name _ = "p" + expr p'@Empty = constant "Empty" (Empty -: p') + expr p'@(Unit x) = constant "Unit" (Unit ->: p') :$ expr x + expr p'@(Insert x p) = constant "Insert" (Insert ->>: p') :$ expr x :$ expr p + expr p'@(SafeRemoveMin x) = constant "SafeRemoveMin" (SafeRemoveMin ->: p') :$ expr x + expr p'@(Merge p q) = constant "Merge" (Merge ->>: p') :$ expr p :$ expr q + expr p'@(FromList xs) = constant "FromList" (FromList ->: p') :$ expr xs + instances p = this p + $ let Unit x = Unit undefined `asTypeOf` p + in instances x + + + +data HeapPP a = HeapPP { program :: (HeapP a) + , theHeap :: (Heap a) } + deriving (Show, Read) + +instance (Ord a, Listable a) => Listable (HeapPP a) where + tiers = cons1 heappp + +heappp :: Ord a => HeapP a -> HeapPP a +heappp p = HeapPP p (heap p) + +instance (Ord a, Generalizable a) => Generalizable (HeapPP a) where + name _ = "hpp" + expr (HeapPP p _) = constant "heappp" (heappp -:> p) :$ expr p + background hpp = [ constant "program" $ program -:> hpp + , constant "theHeap" $ theHeap -:> hpp + ] + instances hpp = this hpp + $ let HeapPP p h = HeapPP undefined undefined `asTypeOf` hpp + in instances p . instances h + + +(==?) :: Ord a => Heap a -> [a] -> Bool +h ==? xs = sort (toList h) == sort xs + +prop_ToSortedList :: Ord a => HeapPP a -> Bool +prop_ToSortedList (HeapPP _ h) = + h ==? xs && xs == sort xs + where + xs = toSortedList h + +sizePP :: HeapPP a -> Int +sizePP (HeapPP h0 h1) = sizeP h0 + sizeH h1 + +sizeP :: HeapP a -> Int +sizeP hp = case hp of + Empty -> 1 + Unit _ -> 1 + Insert _ h -> 1 + sizeP h + SafeRemoveMin h -> 1 + sizeP h + Merge h0 h1 -> 1 + sizeP h0 + sizeP h1 + FromList ls -> 1 + length ls + +sizeH :: Heap a -> Int +sizeH hp = case hp of + Node a h0 h1 -> 1 + sizeH h0 + sizeH h1 + Nil -> 1 + +main :: IO () +main = do + Lean.checkFor 1080 (prop_ToSortedList :: HeapPP Int -> Bool) + check `for` 1080 $ (prop_ToSortedList :: HeapPP Int -> Bool) diff --git a/eg/int.hs b/eg/int.hs new file mode 100644 --- /dev/null +++ b/eg/int.hs @@ -0,0 +1,18 @@ +import Test.Extrapolate + +main :: IO () +main = do + putStrLn "Properties that should be OK:" + check $ \x y -> x + y == y + (x :: Int) + check $ \x y -> x * y == y * (x :: Int) + check $ \x y z -> x + (y + z) == (x + y) + (z :: Int) + check $ \x y z -> x * (y * z) == (x * y) * (z :: Int) + putStrLn "" + + putStrLn "Properties that should fail:" + check $ \x -> x + 1 == (x :: Int) + check $ \x -> x /= (x :: Int) + check $ \x y -> x /= (y :: Int) + check $ \x y z -> x /= y && y /= (z :: Int) + check $ \(x,y) -> x /= (y :: Int) + check $ \(x,y,z) -> x /= y && y /= (z :: Int) diff --git a/eg/list.hs b/eg/list.hs new file mode 100644 --- /dev/null +++ b/eg/list.hs @@ -0,0 +1,12 @@ +import Test.Extrapolate +import Data.List + +main :: IO () +main = do + check $ \xs -> sort (sort xs :: [Int]) == sort xs + check $ \xs ys -> xs `union` ys == ys `union` (xs :: [Int]) + check $ \xs -> reverse xs == (xs :: [Int]) + check `for` 1080 $ \xs -> nub xs == (xs :: [Int]) + check $ \xs -> null (xs :: [Int]) + check $ \xs xs' -> (xs++xs' :: [Int]) `isPrefixOf` xs + check $ \xs xs' -> xs `isPrefixOf` (xs++xs' :: [Int]) diff --git a/eg/overflow.hs b/eg/overflow.hs new file mode 100644 --- /dev/null +++ b/eg/overflow.hs @@ -0,0 +1,55 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable, StandaloneDeriving, CPP #-} -- for GHC <= 7.8 +import Test.Extrapolate +import Test.LeanCheck.Utils +import qualified Test.LeanCheck as Lean +import Data.Int + +#if __GLASGOW_HASKELL__ < 710 +import Data.Typeable (Typeable) +deriving instance Typeable T +#endif + +type I = [Int16] +data T = T I I I I I + deriving Show + +toList :: T -> [[Int16]] +toList (T i j k l m) = [i,j,k,l,m] + +pre :: T -> Bool +pre t = all ((< 256) . sum) (toList t) + +post :: T -> Bool +post t = (sum . concat) (toList t) < 5 * 256 + +prop :: T -> Bool +prop t = pre t ==> post t + +instance Listable Int16 where + list = map unX list + +instance Generalizable Int16 where + name _ = "x" + expr = showConstant + instances x = this x id + background x = bgOrd x + +{- +instance Listable T where + tiers = cons5 makeT + where + makeT (Xs i) (Xs j) (Xs k) (Xs l) (Xs m) = T i j k l m +-} + +deriveListable ''T +deriveGeneralizable ''T + +main :: IO () +main = do + check `for` 10000 + `withConditionSize` 2 +-- NOTE: it takes 25m to run with the following two lines uncommented +-- `withBackground` [constant "sum" (sum :: [Int16] -> Int16)] +-- `withConditionSize` 4 + $ prop diff --git a/eg/overflow8.hs b/eg/overflow8.hs new file mode 100644 --- /dev/null +++ b/eg/overflow8.hs @@ -0,0 +1,47 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable, StandaloneDeriving, CPP #-} -- for GHC <= 7.8 +import Test.Extrapolate +import Test.LeanCheck.Utils +import qualified Test.LeanCheck as Lean +import Data.Int + +#if __GLASGOW_HASKELL__ < 710 +import Data.Typeable (Typeable) +deriving instance Typeable T +#endif + +type I = [Int8] +data T = T I I{- I-} + deriving Show + +toList :: T -> [[Int8]] +toList (T i j{- k-}) = [i,j{-,k-}] + +pre :: T -> Bool +pre t = all ((< 16) . sum) (toList t) + +post :: T -> Bool +post t = (sum . concat) (toList t) < 2 * 16 -- 3 * 16 + +prop :: T -> Bool +prop t = pre t ==> post t + +instance Listable Int8 where + list = map unX list + +instance Generalizable Int8 where + name _ = "x" + expr = showConstant + instances x = this x id + background x = bgOrd x + +deriveListable ''T +deriveGeneralizable ''T + +main :: IO () +main = do + check `for` 1080 -- 2160 + `withBackground` [constant "sum" (sum :: [Int8] -> Int8)] + `withConditionSize` 4 + $ prop +-- NOTE: with T defined as a triple, this takes 25s to run diff --git a/eg/parser.hs b/eg/parser.hs new file mode 100644 --- /dev/null +++ b/eg/parser.hs @@ -0,0 +1,406 @@ +-- Example taken from Lee Pike's SmartCheck: +-- https://github.com/leepike/SmartCheck/blob/master/paper/paper.pdf +-- https://github.com/leepike/smartcheck +{-# LANGUAGE CPP #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} + +-- | Toy "parser"/"serializer" (with a bug) in And parsing. + +module Main where + +import Prelude hiding (showList, mod) + +--import Test.LeanCheck +import Test.Extrapolate hiding (Var) +import qualified Test.LeanCheck as Lean +import Test.LeanCheck.Utils ((-:>)) + +import System.Environment + +import Data.List + +import GHC.Generics +import Data.Typeable +import Control.Applicative + +import Control.Monad.Trans.State +import Data.Char + +----------------------------------------------------------------- + +-- Let's make up a toy language. + +data Lang = Lang + { modules :: [Mod] + , funcs :: [Func] + } deriving (Show, Read, Typeable, Generic, Eq, Ord) + +newtype Var = Var String + deriving (Show, Read, Typeable, Generic, Eq, Ord) + +data Mod = Mod + { imports :: [Var] + , exports :: [Var] + } deriving (Show, Read, Typeable, Generic, Eq, Ord) + +data Func = Func + { fnName :: Var + , args :: [Exp] + , stmts :: [Stmt] + } deriving (Show, Read, Typeable, Generic, Eq, Ord) + +data Stmt = Assign Var Exp + | Alloc Var Exp + | Return Exp + -- | Ref Exp + -- | Deref Exp + -- | Assert Exp + -- | Loop Exp [Stmt] + -- | IfTE Exp [Stmt] [Stmt] + deriving (Show, Read, Typeable, Generic, Eq, Ord) + +data Exp = Int Int + | Bool Bool + | Add Exp Exp + | Sub Exp Exp + | Mul Exp Exp + | Div Exp Exp + | Not Exp + | And Exp Exp + | Or Exp Exp + deriving (Show, Read, Typeable, Generic, Eq, Ord) + +deriveListable ''Lang +--deriveListable ''Var +deriveListable ''Mod +deriveListable ''Func +deriveListable ''Stmt +deriveListable ''Exp + +-------------------------------------------------------------------------------- + +instance Listable Var where + tiers = cons1 Var `suchThat` (\(Var s) -> all isAlphaNum s && not (null s)) + +{- +instance Listable Lang where + tiers = undefined + +instance Listable Mod where + tiers = undefined + +instance Listable Func where + tiers = undefined + +instance Listable Stmt where + tiers = undefined + +instance Listable Exp where + tiers = undefined +-} + +{- Alternative: +deriveGeneralizable ''Var +deriveGeneralizable ''Lang +deriveGeneralizable ''Mod +deriveGeneralizable ''Func +deriveGeneralizable ''Exp +deriveGeneralizable ''Stmt +-} +-- {- +instance Generalizable Var where + name _ = "v" + expr (Var v) = constant "Var" Var :$ expr v + instances v = this v $ instances (undefined :: [String]) + +instance Generalizable Lang where + name _ = "l" + expr (Lang ms fs) = constant "Lang" Lang :$ expr ms :$ expr fs + instances l = this l $ instances (undefined :: [Mod]) + . instances (undefined :: [Func]) + +instance Generalizable Mod where + name _ = "m" + expr (Mod is es) = constant "Mod" Mod :$ expr is :$ expr es + instances m = this m $ instances (undefined :: Var) + +instance Generalizable Func where + name _ = "f" + expr (Func n as ss) = constant "Func" Func :$ expr n :$ expr as :$ expr ss + instances f = this f $ instances (undefined :: Var) + . instances (undefined :: [Exp]) + . instances (undefined :: [Stmt]) + +instance Generalizable Exp where + name _ = "e" + expr (Int i) = constant "Int" Int :$ expr i + expr (Bool p) = constant "Bool" Bool :$ expr p + expr (Add e1 e2) = constant "Add" Add :$ expr e1 :$ expr e2 + expr (Sub e1 e2) = constant "Sub" Sub :$ expr e1 :$ expr e2 + expr (Mul e1 e2) = constant "Mul" Mul :$ expr e1 :$ expr e2 + expr (Div e1 e2) = constant "Div" Div :$ expr e1 :$ expr e2 + expr (Not e) = constant "Not" Not :$ expr e + expr (And e1 e2) = constant "And" And :$ expr e1 :$ expr e2 + expr (Or e1 e2) = constant "Or " Or :$ expr e1 :$ expr e2 + background e = [ constant "==" ((==) -:> e) + , constant "/=" ((/=) -:> e) ] + instances e = this e + $ instances (undefined :: Var) + . instances (undefined :: Int) + . instances (undefined :: Bool) + +instance Generalizable Stmt where + name _ = "stmt" + expr (Assign v e) = constant "Assign" Assign :$ expr v :$ expr e + expr (Alloc v e) = constant "Alloc" Alloc :$ expr v :$ expr e + expr (Return e) = constant "Return" Return :$ expr e + instances s = this s $ instances (undefined :: Var) + . instances (undefined :: Exp) +-- -} + + +-------------------------------------------------------------------------------- +-- "serializer" + +parens :: String -> String +parens a = '(' : a ++ ")" + +showList :: Show' a => Char -> [a] -> String +showList sep ls = parens $ concat $ intersperse [sep] $ map show' ls + +class Show a => Show' a where + show' :: a -> String + show' = show + +instance Show' Char +instance Show' Int +instance Show' Bool + +instance Show' Lang where + show' (Lang m f) = unwords + [ "Lang" + , showList ';' m + , showList ';' f + ] + +instance Show' Mod where + show' (Mod i e) = unwords + [ "Mod" + , showList ':' i + , showList ':' e + ] + +instance Show' Func where + show' (Func f a s) = unwords + [ "Func" + , show' f + , showList ',' a + , showList ',' s + ] + +instance Show' Var where + show' (Var v) = v + +instance Show' Stmt where + show' stmt = unwords $ case stmt of + Assign v e -> ["Assign", show' v, parens $ show' e] + Alloc v e -> ["Alloc" , show' v, parens $ show' e] + Return e -> ["Return", parens $ show' e] + +instance Show' Exp where + show' e = unwords $ case e of + Int i -> ["Int" , show' i] + Bool b -> ["Bool", show' b] + Add e0 e1 -> ["Add" , parens $ show' e0, parens $ show' e1] + Sub e0 e1 -> ["Sub" , parens $ show' e0, parens $ show' e1] + Mul e0 e1 -> ["Mul" , parens $ show' e0, parens $ show' e1] + Div e0 e1 -> ["Div" , parens $ show' e0, parens $ show' e1] + Not e0 -> ["Not" , parens $ show' e0] + And e0 e1 -> ["And" , parens $ show' e0, parens $ show' e1] + Or e0 e1 -> ["Or" , parens $ show' e0, parens $ show' e1] + +-------------------------------------------------------------------------------- +-- "parser" + +class Read a => Read' a where + read' :: String -> a + read' = read + +instance Read' Lang where + read' str = run str $ do + modify (strip "Lang") + m <- state unparens + let ms = map read' (fromSeps ';' m) + f <- state unparens + let fs = map read' (fromSeps ';' f) + return (Lang ms fs) + +instance Read' Mod where + read' mod = run mod $ do + modify (strip "Mod") + m <- state unparens + let i = fromSeps ':' m + es <- state unparens + let e = fromSeps ':' es + return (Mod (map Var i) (map Var e)) + +instance Read' Func where + read' f = run f $ do + modify (strip "Func") + n <- state (procWord id) + as <- state unparens + let ars = map read' (fromSeps ',' as) + ss <- state unparens + let sts = map read' (fromSeps ',' ss) + return (Func (Var n) ars sts) + +instance Read' Stmt where + read' stmt | isPrefixOf "Assign" stmt = run stmt $ do + modify (strip "Assign") + v <- state (procWord id) + e <- state (procParens read') + return (Assign (Var v) e) + | isPrefixOf "Alloc" stmt = run stmt $ do + modify (strip "Alloc") + v <- state (procWord id) + e <- state (procParens read') + return (Alloc (Var v) e) + | isPrefixOf "Return" stmt = run stmt $ do + modify (strip "Return") + e <- state (procParens read') + return (Return e) + | otherwise = error $ "Couldn't match stmt " ++ stmt + +instance Read' Exp where + read' e | isPrefixOf "Int" e = Int (read $ strip "Int" e) + | isPrefixOf "Bool" e = Bool (read $ strip "Bool" e) + | isPrefixOf "Add" e = run e $ do + modify (strip "Add") + e0 <- state (procParens read') + e1 <- state (procParens read') + return (Add e0 e1) + + | isPrefixOf "Sub" e = run e $ do + modify (strip "Sub") + e0 <- state (procParens read') + e1 <- state (procParens read') + return (Sub e0 e1) + + | isPrefixOf "Mul" e = run e $ do + modify (strip "Mul") + e0 <- state (procParens read') + e1 <- state (procParens read') + return (Mul e0 e1) + + | isPrefixOf "Div" e = run e $ do + modify (strip "Div") + e0 <- state (procParens read') + e1 <- state (procParens read') + return (Div e0 e1) + + | isPrefixOf "Not" e = run e $ do + modify (strip "Not") + e0 <- state (procParens read') + return (Not e0) + + | isPrefixOf "And" e = run e $ do + modify (strip "And") + e0 <- state (procParens read') + e1 <- state (procParens read') + -- XXX Bug! + return (And e1 e0) + | isPrefixOf "Or" e = run e $ do + modify (strip "Or") + e0 <- state (procParens read') + e1 <- state (procParens read') + -- XXX Bug! + return (And e1 e0) + | otherwise = error $ "Couldn't match exp " ++ e + +-------------------------------------------------------------------------------- + +run :: s -> State s a -> a +run e m = (flip evalState) e m + +-- strip a prefix and a space from a string. Return the remainder of the +-- string. +strip :: String -> String -> String +strip pre str = case stripPrefix pre str of + Nothing -> error $ "Couldn't strip " ++ pre ++ " from " ++ str + Just rst -> if null rst then rst else tail rst + +-- Strip the next word. +stripWord :: String -> (String, String) +stripWord str = let strs = words str in + (head strs, unwords (tail strs)) + + +procWord :: (String -> a) -> String -> (a, String) +procWord = runProc stripWord + +-- Return a prefix inside parens and the remainder of a string. +unparens :: String -> (String, String) +unparens ('(':str) = unparens' (1::Integer) [] str + where + unparens' n s ('(':r) = unparens' (n+1) ('(':s) r + unparens' n s (')':r) | n == 1 = (reverse s, strip "" r) + | otherwise = unparens' (n-1) (')':s) r + unparens' _ _ [] = error $ "End of string reached in unparens" + unparens' n s (c:r) = unparens' n (c:s) r +unparens str = error $ "Unparsens couldn't parse " ++ str + +procParens :: (String -> a) -> String -> (a, String) +procParens = runProc unparens + +-- Parse up to a sep +fromSep :: Char -> String -> (String, String) +fromSep sep str = let pre = takeWhile (/= sep) str in + let post = drop (length pre + 1) str in + (pre, post) + +fromSeps :: Char -> String -> [String] +fromSeps _ [] = [] +fromSeps sep str = let (a, b) = fromSep sep str in + let as = fromSeps sep b in + a:as + +runProc :: (String -> (String, String)) + -> (String -> a) + -> String + -> (a, String) +runProc t f s = let (a, b) = t s in (f a, b) + +-------------------------------------------------------------------------------- + +size :: Lang -> Int +size (Lang m f) = sumit sizem m + sumit sizef f + where + sizem (Mod is es) = length is + length es + sizef (Func _ as sts) = sumit sizee as + sumit sizes sts + sizes stmt = case stmt of + Assign _ e -> 1 + sizee e + Alloc _ e -> 1 + sizee e + Return e -> 1 + sizee e + sizee e = case e of + Int _ -> 1 + Bool _ -> 1 + Add e0 e1 -> 1 + sizee e0 + sizee e1 + Sub e0 e1 -> 1 + sizee e0 + sizee e1 + Mul e0 e1 -> 1 + sizee e0 + sizee e1 + Div e0 e1 -> 1 + sizee e0 + sizee e1 + Not e0 -> 1 + sizee e0 + And e0 e1 -> 1 + sizee e0 + sizee e1 + Or e0 e1 -> 1 + sizee e0 + sizee e1 + sumit sz ls = sum (map sz ls) + +-------------------------------------------------------------------------------- + +prop_parse :: Lang -> Bool +prop_parse e = read' (show' e) == e + +main :: IO () +main = do + Lean.check prop_parse + check prop_parse diff --git a/eg/redblack.hs b/eg/redblack.hs new file mode 100644 --- /dev/null +++ b/eg/redblack.hs @@ -0,0 +1,137 @@ +-- Copyright 2016--2017, Matt Might and Lee Pike. +-- +-- Adapted from a SmartCheck example: +-- https://github.com/leepike/SmartCheck/tree/master/examples/RedBlackTreesh +-- which in turn was adapted from: +-- http://matt.might.net/articles/quick-quickcheck/ +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE DeriveGeneric #-} + + -- Note from Matt Might: + -- Note: Benjamin Pierce's lecture notes are where I learned to + -- generate properly ordered binary search trees: + + -- http://www.seas.upenn.edu/~cis552/12fa/lectures/stub/BST.html + +import RedBlackSet +import Control.Monad + +import Test.Extrapolate +import Data.Typeable + + +instance (Ord a, Listable a) => Listable (RBSet a) where + tiers = cons1 fromList + +-- transforms a list into an RBSet. +fromList :: Ord a => [a] -> RBSet a +fromList = foldr insert empty + + -- Count the black depth of a red-black tree: +blackDepth :: RBSet a -> Maybe Int +blackDepth (E) = Just(1) +blackDepth (T R l _ r) = case (blackDepth(l),blackDepth(r)) of + (Just(n),Just(m)) -> if n == m then Just(n) else Nothing + (_,_) -> Nothing +blackDepth (T B l _ r) = case (blackDepth(l),blackDepth(r)) of + (Just(n),Just(m)) -> if n == m then Just(1+n) else Nothing + (_,_) -> Nothing + + -- Check for red-red violations: +prop_NoRedRed :: RBSet Int -> Bool +prop_NoRedRed E = True +prop_NoRedRed (T R (T R _ _ _) _ _) = False +prop_NoRedRed (T R _ _ (T R _ _ _)) = False +prop_NoRedRed (T _ l x r) = (prop_NoRedRed l) && (prop_NoRedRed r) + + + -- Check for black-balanced violations: +prop_BlackBalanced :: RBSet Int -> Bool +prop_BlackBalanced t = + case blackDepth(t) of + Just _ -> True + Nothing -> False + + + -- Check for ordering violations: +prop_OrderedList :: Ord a => [a] -> Bool +prop_OrderedList [] = True +prop_OrderedList [x] = True +prop_OrderedList (x:y:tl) = (x < y) && (prop_OrderedList(y:tl)) + +prop_Ordered :: RBSet Int -> Bool +prop_Ordered t = prop_OrderedList (toAscList t) + + -- Check for the validity of a red-black tree: +prop_RBValid :: RBSet Int -> Bool +prop_RBValid t = prop_NoRedRed t && prop_BlackBalanced t && prop_Ordered t + + + -- Insertion properties: +prop_Create5 :: Int -> Int -> Int -> Int -> Int -> Bool +prop_Create5 a b c d e = + ((foldr insert empty) [a,b,c,d,e]) == + ((foldr insert empty) [b,c,d,e,a]) + +prop_InsertValid :: RBSet Int -> Int -> Bool +prop_InsertValid t x = prop_RBValid(insert x t) + +prop_InsertMember :: RBSet Int -> Int -> Bool +prop_InsertMember t x = member x (insert x t) + +prop_InsertSafe :: RBSet Int -> Int -> Int -> Bool +prop_InsertSafe t x y = member x t ==> (member x (insert y t)) + +prop_NoInsertPhantom :: RBSet Int -> Int -> Int -> Bool +prop_NoInsertPhantom t x y = + not (member x t) && x /= y ==> not (member x (insert y t)) + + -- Deletion properties: +prop_InsertDeleteValid :: RBSet Int -> Int -> Bool +prop_InsertDeleteValid t x = prop_RBValid(delete x (insert x t)) + +prop_DeleteValid :: RBSet Int -> Int -> Bool +prop_DeleteValid t x = prop_RBValid(delete x t) + +prop_MemberDelete :: RBSet Int -> Int -> Bool +prop_MemberDelete t x = member x t ==> not (member x (delete x t)) + +prop_DeletePreserve :: RBSet Int -> Int -> Int -> Bool +prop_DeletePreserve t x y = x /= y ==> (member y t) == (member y (delete x t)) + +main :: IO () +main = do + chk prop_BlackBalanced + + -- {- + -- Insertion tests: + chk prop_Create5 + chk prop_InsertValid + chk prop_InsertSafe + chk prop_NoInsertPhantom + chk prop_InsertMember + + -- Deletion tests: + chk prop_InsertDeleteValid + chk prop_DeleteValid + chk prop_MemberDelete + chk prop_DeletePreserve + -- -} + where + chk :: Testable a => a -> IO () + chk = check `for` 1080 + +instance Listable Color where + tiers = [[R, B], [BB, NB]] + +instance (Ord a, Generalizable a) => Generalizable (RBSet a) where + name _ = "h" + expr t = constant "fromList" (fromList ->: t) :$ expr (toAscList t) + instances h = this h + $ instances (toAscList h) + +-- TODO: make LeanCheck find a counter-example to prop_BlackBalanced +-- when -DBALANCE_BUG is active or find out why it cannot find it. + +-- TODO: somehow make "./eg/redblack-remove-bug" run faster. +-- (currently, it takes 2 minutes to run) diff --git a/eg/sorting.hs b/eg/sorting.hs new file mode 100644 --- /dev/null +++ b/eg/sorting.hs @@ -0,0 +1,33 @@ +import Test.Extrapolate +import Test.LeanCheck.Utils +import qualified Test.LeanCheck as Lean + +sort :: Ord a => [a] -> [a] +sort [] = [] +sort (x:xs) = sort (filter (< x) xs) + ++ [x] + ++ sort (filter (> x) xs) + +prop_sortOrdered :: Ord a => [a] -> Bool +prop_sortOrdered xs = ordered (sort xs) + where + ordered (x:y:xs) = x <= y && ordered (y:xs) + ordered _ = True + +prop_sortCount :: Ord a => a -> [a] -> Bool +prop_sortCount x xs = count x (sort xs) == count x xs + +count :: Eq a => a -> [a] -> Int +count x = length . filter (== x) + +main :: IO () +main = do + chk $ prop_sortOrdered -:> [int] + chk $ prop_sortCount -:> int + check $ prop_sortCount -:> int + chk `for` 99 $ prop_sortOrdered -:> [bool] + chk `for` 99 $ prop_sortCount -:> bool + where + chk :: Testable a => a -> IO () + chk = check `withBackground` [ constant "count" $ count -:> int ] + `withConditionSize` 6 diff --git a/eg/word-refinements.hs b/eg/word-refinements.hs new file mode 100644 --- /dev/null +++ b/eg/word-refinements.hs @@ -0,0 +1,34 @@ +-- Refinements of a property about Data.List.words +-- +-- Copyright (c) 2017 Colin Runciman and Rudy Matela Braquehais. +-- Distributed under the 3-Clause BSD licence (see the file LICENSE). +import Test.Extrapolate +import Data.List +import Data.Char + +prop_lengthWords0 :: String -> Bool +prop_lengthWords0 s = s /= "" + ==> length (words s) == length (filter isSpace s) + 1 + +prop_lengthWords1 :: String -> Bool +prop_lengthWords1 s = s /= "" && not (isSpace (head s)) + && not (isSpace (last s)) + ==> length (words s) == length (filter isSpace s) + 1 + +prop_lengthWords2 :: String -> Bool +prop_lengthWords2 s = noDoubleSpace (" " ++ s ++ " ") + ==> length (words s) == length (filter isSpace s) + 1 + where + noDoubleSpace s = and [ not (isSpace a && isSpace b) + | (a,b) <- zip s (tail s) ] + +main :: IO () +main = do + check prop_lengthWords0 + let check1 = check `withBackground` [constant "isSpace" isSpace] + check1 prop_lengthWords0 + check1 prop_lengthWords1 + let check2 = check `withBackground` [ constant "`isInfixOf`" $ isInfixOf -:> string + , showConstant " " ] + check2 prop_lengthWords0 -- a step back, note the *zero* + check prop_lengthWords2 diff --git a/eg/xmonad/Makefile b/eg/xmonad/Makefile new file mode 100644 --- /dev/null +++ b/eg/xmonad/Makefile @@ -0,0 +1,26 @@ +XMONAD=https://github.com/xmonad/xmonad +#XMONAD=$(HOME)/prj/xmonad + +all: xmonad/dist/build/extrapolate/extrapolate + +bench: all + /usr/bin/time "-f%e %M" ./xmonad/dist/build/extrapolate/extrapolate + +xmonad/tests/extrapolate.hs: extrapolate.hs + cp $< $@ + +xmonad/dist/build/extrapolate/extrapolate: xmonad/tests/extrapolate.hs + cd xmonad; cabal build extrapolate + +prepare: + git clone $(XMONAD) xmonad + git -C xmonad show -s --format="%H%n%ci" | tee revision.txt + cat xmonad.cabal >> xmonad/xmonad.cabal + sed -i -e 's,\(removeFromWorkspace.*filter\) (/=w),\1 (==w),' xmonad/src/XMonad/StackSet.hs + cd xmonad; cabal configure --enable-tests --ghc-options=-dynamic + +clean: + cd xmonad; cabal clean + +clean-prepare: + rm -rf xmonad diff --git a/eg/xmonad/extrapolate.hs b/eg/xmonad/extrapolate.hs new file mode 100644 --- /dev/null +++ b/eg/xmonad/extrapolate.hs @@ -0,0 +1,35 @@ +{-# LANGUAGE TemplateHaskell #-} +import qualified Test.LeanCheck as Lean +import Test.Extrapolate as Extra + +import Data.Map (Map) +import XMonad.StackSet + +deriveListableCascading ''StackSet + +instance (Generalizable a, Generalizable b) => Generalizable (Map a b) where + expr = showConstant + name xys = name (argTy1of2 xys) ++ name (argTy2of2 xys) ++ "s" + instances xys = this xys id + +deriveGeneralizableCascading ''StackSet + +main :: IO () +main = do + putStrLn "LeanCheck:" + Lean.check prop_delete + putStrLn "" + + putStrLn "Extrapolate" + check prop_delete + putStrLn "" + +type Tag = Int +type Window = Char +type T = StackSet Tag Int Window Int Int + +prop_delete :: T -> Bool +prop_delete x = + case peek x of + Nothing -> True + Just i -> not (member i (delete i x)) diff --git a/eg/xmonad/revision.txt b/eg/xmonad/revision.txt new file mode 100644 --- /dev/null +++ b/eg/xmonad/revision.txt @@ -0,0 +1,2 @@ +10b843ad21614994b7e12fafaf300f4267aa9e40 +2017-04-10 16:58:45 -0700 diff --git a/eg/xmonad/xmonad.cabal b/eg/xmonad/xmonad.cabal new file mode 100644 --- /dev/null +++ b/eg/xmonad/xmonad.cabal @@ -0,0 +1,12 @@ + +-- to be appended to xmonad.cabal +test-suite extrapolate + type: exitcode-stdio-1.0 + hs-source-dirs: tests + build-depends: base, + containers, + leancheck, + extrapolate, + X11, + xmonad + main-is: extrapolate.hs diff --git a/extrapolate.cabal b/extrapolate.cabal --- a/extrapolate.cabal +++ b/extrapolate.cabal @@ -1,5 +1,5 @@ name: extrapolate -version: 0.3.2 +version: 0.3.3 synopsis: generalize counter-examples of test properties description: Extrapolate is a tool able to provide generalized counter-examples of test @@ -22,6 +22,48 @@ extra-doc-files: README.md , TODO.md +extra-source-files: .gitignore + , .travis.yml + , Makefile + , bench/diff.hs + , bench/eq.hs + , bench/false.hs + , bench/lazy-sc/*.hs + , bench/lazy-sc/Makefile + , bench/lazy-sc/revision.txt + , bench/ord.hs + , bench/runtime/oubli/bench/*.runtime + , bench/runtime/oubli/eg/*.runtime + , bench/runtime/zero/bench/*.runtime + , bench/runtime/zero/eg/*.runtime + , bench/smartcheck/*.txt + , bench/smartcheck/Makefile + , bench/smartcheck/bin/count-cons + , bench/smartcheck/bin/ncons-overflow + , bench/smartcheck/bin/nvars-overflow + , bench/smartcheck/bin/sort-stats + , bench/smartcheck/div0-main.hs + , bench/smartcheck/list.hs + , bench/smartcheck/overflow-main.hs + , bench/smartcheck/parser-main.hs + , bench/smartcheck/sorting.hs + , bench/smartcheck/word-refinements.hs + , bench/true.hs + , eg/*.hs + , eg/xmonad/Makefile + , eg/xmonad/extrapolate.hs + , eg/xmonad/revision.txt + , eg/xmonad/xmonad.cabal + , mk/All.hs + , mk/Toplibs.hs + , mk/depend.mk + , mk/ghcdeps + , mk/haddock-i + , mk/haskell.mk + , stack.yaml + , tests/model/bench/*.out + , tests/model/eg/*.out + , tests/test-sdist tested-with: GHC==8.4, GHC==8.2, GHC==8.0, GHC==7.10, GHC==7.8 source-repository head @@ -31,7 +73,7 @@ source-repository this type: git location: https://github.com/rudymatela/extrapolate - tag: v0.3.2 + tag: v0.3.3 library exposed-modules: Test.Extrapolate diff --git a/mk/All.hs b/mk/All.hs new file mode 100644 --- /dev/null +++ b/mk/All.hs @@ -0,0 +1,22 @@ +module All + ( module Test.Extrapolate + , module Test.Extrapolate.Basic + , module Test.Extrapolate.Core + , module Test.Extrapolate.Derive + , module Test.Extrapolate.Exprs + , module Test.Extrapolate.IO + , module Test.Extrapolate.TypeBinding + , module Test.Extrapolate.Utils + , module Test.Extrapolate.New + ) +where + +import Test.Extrapolate +import Test.Extrapolate.Basic +import Test.Extrapolate.Core +import Test.Extrapolate.Derive +import Test.Extrapolate.Exprs +import Test.Extrapolate.IO +import Test.Extrapolate.TypeBinding +import Test.Extrapolate.Utils +import Test.Extrapolate.New diff --git a/mk/Toplibs.hs b/mk/Toplibs.hs new file mode 100644 --- /dev/null +++ b/mk/Toplibs.hs @@ -0,0 +1,4 @@ +-- Using ghc --make in this module trigger compilation of all modules +module Toplibs () where + +import Test.Extrapolate diff --git a/mk/depend.mk b/mk/depend.mk new file mode 100644 --- /dev/null +++ b/mk/depend.mk @@ -0,0 +1,390 @@ +bench/diff: \ + bench/diff.hs \ + mk/toplibs +bench/diff.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + bench/diff.hs +bench/eq: \ + bench/eq.hs \ + mk/toplibs +bench/eq.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + bench/eq.hs +bench/false: \ + bench/false.hs \ + mk/toplibs +bench/false.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + bench/false.hs +bench/ord: \ + bench/ord.hs \ + mk/toplibs +bench/ord.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + bench/ord.hs +bench/true: \ + bench/true.hs \ + mk/toplibs +bench/true.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + bench/true.hs +eg/calculator: \ + eg/calculator.hs \ + mk/toplibs +eg/calculator.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/calculator.hs +eg/gencalc: \ + eg/gencalc.hs \ + mk/toplibs +eg/gencalc.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/gencalc.hs +eg/heap: \ + eg/heap.hs \ + mk/toplibs +eg/heap.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/heap.hs +eg/int: \ + eg/int.hs \ + mk/toplibs +eg/int.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/int.hs +eg/list: \ + eg/list.hs \ + mk/toplibs +eg/list.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/list.hs +eg/overflow8: \ + eg/overflow8.hs \ + mk/toplibs +eg/overflow8.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/overflow8.hs +eg/overflow: \ + eg/overflow.hs \ + mk/toplibs +eg/overflow.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/overflow.hs +eg/parser: \ + eg/parser.hs \ + mk/toplibs +eg/parser.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/parser.hs +eg/redblack: \ + eg/RedBlackSet.hs \ + eg/redblack.hs \ + mk/toplibs +eg/redblack.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/RedBlackSet.hs \ + eg/redblack.hs +eg/RedBlackSet.o: \ + eg/RedBlackSet.hs +eg/sorting: \ + eg/sorting.hs \ + mk/toplibs +eg/sorting.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/sorting.hs +eg/word-refinements: \ + eg/word-refinements.hs \ + mk/toplibs +eg/word-refinements.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + eg/word-refinements.hs +mk/All.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + mk/All.hs +mk/Toplibs.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs \ + mk/Toplibs.hs +src/Test/Extrapolate/Basic.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs +src/Test/Extrapolate/Core.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Core.hs +src/Test/Extrapolate/Derive.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs +src/Test/Extrapolate/Exprs.o: \ + src/Test/Extrapolate/Exprs.hs +src/Test/Extrapolate/IO.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Core.hs +src/Test/Extrapolate/New.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Core.hs +src/Test/Extrapolate.o: \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs +src/Test/Extrapolate/TypeBinding.o: \ + src/Test/Extrapolate/TypeBinding.hs +src/Test/Extrapolate/Utils.o: \ + src/Test/Extrapolate/Utils.hs +tests/test-derive.o: \ + tests/Test.hs \ + tests/test-derive.hs \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs +tests/test-derive: \ + tests/Test.hs \ + tests/test-derive.hs \ + mk/toplibs +tests/test-extrapolate.o: \ + tests/Test.hs \ + tests/test-extrapolate.hs \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs +tests/test-extrapolate: \ + tests/Test.hs \ + tests/test-extrapolate.hs \ + mk/toplibs +tests/test-new.o: \ + tests/Test.hs \ + tests/test-new.hs \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs +tests/test-new: \ + tests/Test.hs \ + tests/test-new.hs \ + mk/toplibs +tests/Test.o: \ + tests/Test.hs \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs +tests/test-step-by-step.o: \ + tests/test-step-by-step.hs \ + tests/Test.hs \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs +tests/test-step-by-step: \ + tests/test-step-by-step.hs \ + tests/Test.hs \ + mk/toplibs +tests/Test: \ + tests/Test.hs \ + mk/toplibs +tests/test-utils.o: \ + tests/test-utils.hs \ + tests/Test.hs \ + src/Test/Extrapolate/Utils.hs \ + src/Test/Extrapolate/TypeBinding.hs \ + src/Test/Extrapolate.hs \ + src/Test/Extrapolate/New.hs \ + src/Test/Extrapolate/IO.hs \ + src/Test/Extrapolate/Exprs.hs \ + src/Test/Extrapolate/Derive.hs \ + src/Test/Extrapolate/Core.hs \ + src/Test/Extrapolate/Basic.hs +tests/test-utils: \ + tests/test-utils.hs \ + tests/Test.hs \ + mk/toplibs diff --git a/mk/ghcdeps b/mk/ghcdeps new file mode 100644 --- /dev/null +++ b/mk/ghcdeps @@ -0,0 +1,49 @@ +#!/bin/bash +# +# ghcdeps: generate Haskell make dependencies for compiling with GHC. +# +# Copyright (c) 2015-2017 Rudy Matela. +# Distributed under the 3-Clause BSD licence. +# +# From a list of files provided on standard input, +# generate flat make dependencies. +# +# Transitive relations are repeated. +# +# Usage: +# $ ghcdeps -isomedir:someother < ... +# +# will print -i parameters necessary for haddock to link to Haddock +# documentation installed on your system, so you can: +# +# $ haddock-i base template-haskell | xargs haddock +errxit() { + echo "$@" > /dev/stderr + exit 1 +} + +for pkg in "$@"; do + ghc-pkg field $pkg haddock-html,haddock-interfaces || + errxit "error: haddock-i: cannot find package $pkg (ghc-pkg)" +done | +sed "s/.*: //" | +sed "N;s/\n/,/;s/^/-i/" diff --git a/mk/haskell.mk b/mk/haskell.mk new file mode 100644 --- /dev/null +++ b/mk/haskell.mk @@ -0,0 +1,110 @@ +# Implicit rules for compiling Haskell code. +# +# Copyright (c) 2015-2018 Rudy Matela. +# Distributed under the 3-Clause BSD licence. +# +# You can optionally configure the "Configuration variables" below in your main +# makefile, e.g.: +# +# GHCIMPORTDIRS = path/to/dir:path/to/another/dir +# GHCFLAGS = -O2 -dynamic +# GHC = ghc-7.6 +# include haskell.mk + + + +# Configuration variables + +# GHC Parameters +GHCIMPORTDIRS ?= +GHCFLAGS ?= +GHC ?= ghc +GHCCMD = $(GHC) -i$(GHCIMPORTDIRS) $(GHCFLAGS) + +# Hugs Parameters +HUGSIMPORTDIRS ?= "/usr/lib/hugs/packages/*" +HUGSFLAGS ?= +CPPHS_HUGS ?= cpphs-hugs --noline -D__HUGS__ +HUGS ?= hugs +RUNHUGS ?= runhugs +HUGSCMD = $(HUGS) -F"$(CPPHS_HUGS)" -P$(HUGSIMPORTDIRS) $(HUGSFLAGS) +RUNHUGSCMD = $(RUNHUGS) -F"$(CPPHS_HUGS)" -P$(HUGSIMPORTDIRS) $(HUGSFLAGS) + + +# Makefile where to keep the dependencies +DEPMK ?= mk/depend.mk + +# LIB_HSS: all library Haskell files +# ALL_HSS: all Haskell files +# You can override ALL/LIB_HSS in your main Makefile +LIST_LIB_HSS ?= find src -name "*.hs" +LIST_ALL_HSS ?= find \( -path "./dist" -o -path "./.stack-work" \) -prune \ + -o -name "*.*hs" -print +LIB_HSS ?= $(shell $(LIST_LIB_HSS)) +ALL_HSS ?= $(shell $(LIST_ALL_HSS)) + +PKGNAME = $(shell cat *.cabal | grep "^name:" | sed -e "s/name: *//") + + +# Implicit rules +%.hi %.o: %.hs + $(GHCCMD) $< && touch $@ + +%: %.hs + $(GHCCMD) $< && touch $@ + +.PHONY: %.ghci +%.ghci: %.hs + $(GHCCMD) -O0 --interactive $< + +.PHONY: %.hugs +%.hugs: %.hs + $(HUGSCMD) $< + +.PHONY: %.runhugs +%.runhugs: %.hs + $(RUNHUGSCMD) $< + + +# Cleaning rule (add as a clean dependency) +.PHONY: clean-hi-o +clean-hi-o: + find $(ALL_HSS) | sed -e 's/hs$$/o/' | xargs rm -f + find $(ALL_HSS) | sed -e 's/hs$$/hi/' | xargs rm -f + find $(ALL_HSS) | sed -e 's/hs$$/dyn_o/' | xargs rm -f + find $(ALL_HSS) | sed -e 's/hs$$/dyn_hi/' | xargs rm -f + + +# Update dependency file +.PHONY: depend +depend: + find $(ALL_HSS) | ./mk/ghcdeps -i$(GHCIMPORTDIRS) $(GHCFLAGS) > $(DEPMK) + +# haddock rules +haddock: doc/index.html + +clean-haddock: + rm -f doc/*.{html,css,js,png,gif,json} README.html + +upload-haddock: + @echo "use \`cabal upload -d' instead" + @echo "(but 1st: cabal install --only-dependencies --enable-documentation)" + @echo "(to just compile docs: cabal haddock --for-hackage)" + @echo "(on Arch Linux, use: cabal haddock --for-hackage --haddock-options=--optghc=-dynamic)" + +doc/index.html: $(LIB_HSS) + ./mk/haddock-i base template-haskell | xargs \ + haddock --html -odoc $(LIB_HSS) $(HADDOCKFLAGS) --title=$(PKGNAME) + +# lists all Haskell source files +list-all-hss: + @find $(ALL_HSS) + +# lists library Haskell source files +list-lib-hss: + @find $(LIB_HSS) + +show-pkgname: + @echo $(PKGNAME) + +include $(DEPMK) diff --git a/stack.yaml b/stack.yaml new file mode 100644 --- /dev/null +++ b/stack.yaml @@ -0,0 +1,17 @@ +# stack.yaml docs: +# https://docs.haskellstack.org/en/stable/yaml_configuration/ + +# resolver: nightly-2015-09-21 +# resolver: ghc-7.10.2 +resolver: lts-12.7 + +packages: +- . + +extra-deps: +- leancheck-0.7.3 +- speculate-0.3.5 + +flags: {} + +extra-package-dbs: [] diff --git a/tests/model/bench/diff.out b/tests/model/bench/diff.out new file mode 100644 --- /dev/null +++ b/tests/model/bench/diff.out @@ -0,0 +1,180 @@ +checks :: () + +*** Failed! Falsifiable (after 1 tests): +() () + +Generalization: +_ _ + + +checks :: Bool + +*** Failed! Falsifiable (after 1 tests): +False False + +Generalization: +p p + + +checks :: Int + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + + +checks :: Integer + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + + +checks :: Char + +*** Failed! Falsifiable (after 1 tests): +'a' 'a' + +Generalization: +c c + + +checks :: Ordering + +*** Failed! Falsifiable (after 1 tests): +LT LT + +Generalization: +o o + + +checks :: [()] + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +us us + + +checks :: [Bool] + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +ps ps + + +checks :: [Int] + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +xs xs + + +checks :: [Integer] + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +xs xs + + +checks :: [Char] + +*** Failed! Falsifiable (after 1 tests): +"" "" + +Generalization: +cs cs + + +checks :: [Ordering] + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +os os + + +checks :: ((),Int) + +*** Failed! Falsifiable (after 1 tests): +((),0) ((),0) + +Generalization: +ux ux + + +checks :: (Bool,Char) + +*** Failed! Falsifiable (after 1 tests): +(False,'a') (False,'a') + +Generalization: +pc pc + + +checks :: (Int,(),Bool) + +*** Failed! Falsifiable (after 1 tests): +(0,(),False) (0,(),False) + +Generalization: +xup xup + + +checks :: (Ordering,Char,Integer) + +*** Failed! Falsifiable (after 1 tests): +(LT,'a',0) (LT,'a',0) + +Generalization: +ocx ocx + + +checks :: Maybe () + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +mu mu + + +checks :: Maybe Int + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +mx mx + + +checks :: Either () Bool + +*** Failed! Falsifiable (after 1 tests): +(Left ()) (Left ()) + +Generalization: +eup eup + + +checks :: Either Int Char + +*** Failed! Falsifiable (after 1 tests): +(Left 0) (Left 0) + +Generalization: +exc exc + + diff --git a/tests/model/bench/eq.out b/tests/model/bench/eq.out new file mode 100644 --- /dev/null +++ b/tests/model/bench/eq.out @@ -0,0 +1,209 @@ +checks :: () + ++++ OK, passed 1 tests (exhausted). + + +checks :: Bool + +*** Failed! Falsifiable (after 2 tests): +False True + + +checks :: Int + +*** Failed! Falsifiable (after 2 tests): +0 1 + +Conditional Generalization: +x y when x /= y + + +checks :: Integer + +*** Failed! Falsifiable (after 2 tests): +0 1 + +Conditional Generalization: +x y when x /= y + + +checks :: Char + +*** Failed! Falsifiable (after 2 tests): +'a' ' ' + +Conditional Generalization: +c d when c /= d + + +checks :: Ordering + +*** Failed! Falsifiable (after 2 tests): +LT EQ + +Conditional Generalization: +o p when o /= p + + +checks :: [()] + +*** Failed! Falsifiable (after 2 tests): +[] [()] + +Generalization: +us (_:us) + +Conditional Generalization: +[] us when 0 /= length us + + +checks :: [Bool] + +*** Failed! Falsifiable (after 2 tests): +[] [False] + +Generalization: +ps (_:ps) + +Conditional Generalization: +ps qs when ps /= qs + + +checks :: [Int] + +*** Failed! Falsifiable (after 2 tests): +[] [0] + +Generalization: +xs (_:xs) + +Conditional Generalization: +xs ys when xs /= ys + + +checks :: [Integer] + +*** Failed! Falsifiable (after 2 tests): +[] [0] + +Generalization: +xs (_:xs) + +Conditional Generalization: +xs ys when xs /= ys + + +checks :: [Char] + +*** Failed! Falsifiable (after 2 tests): +"" "a" + +Generalization: +cs (_:cs) + +Conditional Generalization: +cs ds when cs /= ds + + +checks :: [Ordering] + +*** Failed! Falsifiable (after 2 tests): +[] [LT] + +Generalization: +os (_:os) + +Conditional Generalization: +os ps when os /= ps + + +checks :: ((),Int) + +*** Failed! Falsifiable (after 2 tests): +((),0) ((),1) + +Generalization: +(_,0) (_,1) + +Conditional Generalization: +(_,x) (_,y) when x /= y + + +checks :: (Bool,Char) + +*** Failed! Falsifiable (after 2 tests): +(False,'a') (True,'a') + +Generalization: +(False,_) (True,_) + +Conditional Generalization: +pc pc' when pc /= pc' + + +checks :: (Int,(),Bool) + +*** Failed! Falsifiable (after 2 tests): +(0,(),False) (0,(),True) + +Generalization: +(_,_,False) (_,_,True) + +Conditional Generalization: +(x,_,_) (y,_,_) when x /= y + + +checks :: (Ordering,Char,Integer) + +*** Failed! Falsifiable (after 2 tests): +(LT,'a',0) (EQ,'a',0) + +Generalization: +(LT,_,_) (EQ,_,_) + +Conditional Generalization: +ocx ocx' when ocx /= ocx' + + +checks :: Maybe () + +*** Failed! Falsifiable (after 2 tests): +Nothing (Just ()) + +Generalization: +Nothing (Just _) + + +checks :: Maybe Int + +*** Failed! Falsifiable (after 2 tests): +Nothing (Just 0) + +Generalization: +Nothing (Just _) + +Conditional Generalization: +mx mx' when mx /= mx' + + +checks :: Either () Bool + +*** Failed! Falsifiable (after 2 tests): +(Left ()) (Right False) + +Generalization: +(Left _) (Right _) + + +checks :: Either Int Char + +*** Failed! Falsifiable (after 2 tests): +(Left 0) (Right 'a') + +Generalization: +(Left _) (Right _) + +Conditional Generalization: +exc exc' when exc /= exc' + + diff --git a/tests/model/bench/false.out b/tests/model/bench/false.out new file mode 100644 --- /dev/null +++ b/tests/model/bench/false.out @@ -0,0 +1,189 @@ +checks :: () + +*** Failed! Falsifiable (after 1 tests): +() + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +() () + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +() () () + +Generalization: +_ _ _ + + +checks :: Bool + +*** Failed! Falsifiable (after 1 tests): +False + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +False False + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +False False False + +Generalization: +_ _ _ + + +checks :: Int + +*** Failed! Falsifiable (after 1 tests): +0 + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +0 0 0 + +Generalization: +_ _ _ + + +checks :: Integer + +*** Failed! Falsifiable (after 1 tests): +0 + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +0 0 0 + +Generalization: +_ _ _ + + +checks :: Char + +*** Failed! Falsifiable (after 1 tests): +'a' + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +'a' 'a' + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +'a' 'a' 'a' + +Generalization: +_ _ _ + + +checks :: Ordering + +*** Failed! Falsifiable (after 1 tests): +LT + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +LT LT + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +LT LT LT + +Generalization: +_ _ _ + + +checks :: [Integer] + +*** Failed! Falsifiable (after 1 tests): +[] + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +[] [] [] + +Generalization: +_ _ _ + + +checks :: Maybe Int + +*** Failed! Falsifiable (after 1 tests): +Nothing + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing Nothing + +Generalization: +_ _ _ + + +checks :: Either Int Char + +*** Failed! Falsifiable (after 1 tests): +Left 0 + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +(Left 0) (Left 0) + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +(Left 0) (Left 0) (Left 0) + +Generalization: +_ _ _ + + diff --git a/tests/model/bench/ord.out b/tests/model/bench/ord.out new file mode 100644 --- /dev/null +++ b/tests/model/bench/ord.out @@ -0,0 +1,454 @@ +checks :: () + +*** Failed! Falsifiable (after 1 tests): +() () + +Generalization: +_ _ + +*** Failed! Falsifiable (after 1 tests): +() () + +Generalization: +_ _ + ++++ OK, passed 1 tests (exhausted). + ++++ OK, passed 1 tests (exhausted). + + +checks :: Bool + +*** Failed! Falsifiable (after 1 tests): +False False + +Generalization: +p p + +*** Failed! Falsifiable (after 1 tests): +False False + +Generalization: +p p + +*** Failed! Falsifiable (after 3 tests): +True False + +*** Failed! Falsifiable (after 2 tests): +False True + + +checks :: Int + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + +Conditional Generalization: +y x when x <= y + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + +Conditional Generalization: +x y when x <= y + +*** Failed! Falsifiable (after 3 tests): +1 0 + +Conditional Generalization: +y x when x < y + +*** Failed! Falsifiable (after 2 tests): +0 1 + +Conditional Generalization: +x y when x < y + + +checks :: Integer + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + +Conditional Generalization: +y x when x <= y + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + +Conditional Generalization: +x y when x <= y + +*** Failed! Falsifiable (after 3 tests): +1 0 + +Conditional Generalization: +y x when x < y + +*** Failed! Falsifiable (after 2 tests): +0 1 + +Conditional Generalization: +x y when x < y + + +checks :: Char + +*** Failed! Falsifiable (after 1 tests): +'a' 'a' + +Generalization: +c c + +Conditional Generalization: +d c when c <= d + +*** Failed! Falsifiable (after 1 tests): +'a' 'a' + +Generalization: +c c + +Conditional Generalization: +c d when c <= d + +*** Failed! Falsifiable (after 2 tests): +'a' ' ' + +Conditional Generalization: +d c when c < d + +*** Failed! Falsifiable (after 3 tests): +' ' 'a' + +Conditional Generalization: +c d when c < d + + +checks :: Ordering + +*** Failed! Falsifiable (after 1 tests): +LT LT + +Generalization: +o o + +Conditional Generalization: +p o when o <= p + +*** Failed! Falsifiable (after 1 tests): +LT LT + +Generalization: +o o + +Conditional Generalization: +o p when o <= p + +*** Failed! Falsifiable (after 4 tests): +EQ LT + +Conditional Generalization: +p o when o < p + +*** Failed! Falsifiable (after 2 tests): +LT EQ + +Conditional Generalization: +o p when o < p + + +checks :: [Bool] + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +ps ps + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +ps ps + +*** Failed! Falsifiable (after 4 tests): +[False] [] + +Generalization: +(_:_) [] + +Conditional Generalization: +ps [] when ps /= [] + +*** Failed! Falsifiable (after 2 tests): +[] [False] + +Generalization: +[] (_:_) + +Conditional Generalization: +[] ps when ps /= [] + + +checks :: [Integer] + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +xs xs + +Conditional Generalization: +ys xs when xs <= ys + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +xs xs + +Conditional Generalization: +xs ys when xs <= ys + +*** Failed! Falsifiable (after 3 tests): +[0] [] + +Generalization: +(_:_) [] + +Conditional Generalization: +ys xs when xs < ys + +*** Failed! Falsifiable (after 2 tests): +[] [0] + +Generalization: +[] (_:_) + +Conditional Generalization: +xs ys when xs < ys + + +checks :: (Bool,Char) + +*** Failed! Falsifiable (after 1 tests): +(False,'a') (False,'a') + +Generalization: +pc pc + +Conditional Generalization: +(p,d) (p,c) when c <= d + +*** Failed! Falsifiable (after 1 tests): +(False,'a') (False,'a') + +Generalization: +pc pc + +Conditional Generalization: +(p,c) (p,d) when c <= d + +*** Failed! Falsifiable (after 3 tests): +(True,'a') (False,'a') + +Generalization: +(True,_) (False,_) + +Conditional Generalization: +(p,d) (p,c) when c < d + +*** Failed! Falsifiable (after 2 tests): +(False,'a') (True,'a') + +Generalization: +(False,_) (True,_) + +Conditional Generalization: +(p,c) (p,d) when c < d + + +checks :: (Ordering,Char,Integer) + +*** Failed! Falsifiable (after 1 tests): +(LT,'a',0) (LT,'a',0) + +Generalization: +ocx ocx + +Conditional Generalization: +ocx' ocx when ocx <= ocx' + +*** Failed! Falsifiable (after 1 tests): +(LT,'a',0) (LT,'a',0) + +Generalization: +ocx ocx + +Conditional Generalization: +ocx ocx' when ocx <= ocx' + +*** Failed! Falsifiable (after 4 tests): +(EQ,'a',0) (LT,'a',0) + +Generalization: +(EQ,_,_) (LT,_,_) + +Conditional Generalization: +ocx' ocx when ocx < ocx' + +*** Failed! Falsifiable (after 2 tests): +(LT,'a',0) (EQ,'a',0) + +Generalization: +(LT,_,_) (EQ,_,_) + +Conditional Generalization: +ocx ocx' when ocx < ocx' + + +checks :: Maybe () + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +mu mu + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +mu mu + +*** Failed! Falsifiable (after 3 tests): +(Just ()) Nothing + +Generalization: +(Just _) Nothing + +*** Failed! Falsifiable (after 2 tests): +Nothing (Just ()) + +Generalization: +Nothing (Just _) + + +checks :: Maybe Int + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +mx mx + +Conditional Generalization: +mx' mx when mx <= mx' + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +mx mx + +Conditional Generalization: +mx mx' when mx <= mx' + +*** Failed! Falsifiable (after 3 tests): +(Just 0) Nothing + +Generalization: +(Just _) Nothing + +Conditional Generalization: +mx' mx when mx < mx' + +*** Failed! Falsifiable (after 2 tests): +Nothing (Just 0) + +Generalization: +Nothing (Just _) + +Conditional Generalization: +mx mx' when mx < mx' + + +checks :: Either () Bool + +*** Failed! Falsifiable (after 1 tests): +(Left ()) (Left ()) + +Generalization: +eup eup + +*** Failed! Falsifiable (after 1 tests): +(Left ()) (Left ()) + +Generalization: +eup eup + +*** Failed! Falsifiable (after 4 tests): +(Right False) (Left ()) + +Generalization: +(Right _) (Left _) + +*** Failed! Falsifiable (after 2 tests): +(Left ()) (Right False) + +Generalization: +(Left _) (Right _) + + +checks :: Either Int Char + +*** Failed! Falsifiable (after 1 tests): +(Left 0) (Left 0) + +Generalization: +exc exc + +Conditional Generalization: +exc' exc when exc <= exc' + +*** Failed! Falsifiable (after 1 tests): +(Left 0) (Left 0) + +Generalization: +exc exc + +Conditional Generalization: +exc exc' when exc <= exc' + +*** Failed! Falsifiable (after 3 tests): +(Right 'a') (Left 0) + +Generalization: +(Right _) (Left _) + +Conditional Generalization: +exc' exc when exc < exc' + +*** Failed! Falsifiable (after 2 tests): +(Left 0) (Right 'a') + +Generalization: +(Left _) (Right _) + +Conditional Generalization: +exc exc' when exc < exc' + + diff --git a/tests/model/bench/true-false.out b/tests/model/bench/true-false.out new file mode 100644 --- /dev/null +++ b/tests/model/bench/true-false.out @@ -0,0 +1,439 @@ +checks :: () + ++++ OK, passed 1 tests (exhausted). + +*** Failed! Falsifiable (after 1 tests): +() + +Generalization: +_ + ++++ OK, passed 1 tests (exhausted). + +*** Failed! Falsifiable (after 1 tests): +() () + +Generalization: +_ _ + + +checks :: Bool + ++++ OK, passed 2 tests (exhausted). + +*** Failed! Falsifiable (after 1 tests): +False + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +False True + +*** Failed! Falsifiable (after 1 tests): +False False + +Generalization: +p p + + +checks :: Int + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +0 + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +0 1 + +Conditional Generalization: +x y when x /= y + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + + +checks :: Integer + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +0 + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +0 1 + +Conditional Generalization: +x y when x /= y + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + + +checks :: Char + ++++ OK, passed 97 tests (exhausted). + +*** Failed! Falsifiable (after 1 tests): +'a' + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +'a' ' ' + +Conditional Generalization: +c d when c /= d + +*** Failed! Falsifiable (after 1 tests): +'a' 'a' + +Generalization: +c c + + +checks :: Ordering + ++++ OK, passed 3 tests (exhausted). + +*** Failed! Falsifiable (after 1 tests): +LT + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +LT EQ + +*** Failed! Falsifiable (after 1 tests): +LT LT + +Generalization: +o o + + +checks :: [()] + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +[] + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +[] [()] + +Generalization: +us (_:us) + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +us us + + +checks :: [Bool] + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +[] + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +[] [False] + +Generalization: +ps (_:ps) + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +ps ps + + +checks :: [Int] + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +[] + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +[] [0] + +Generalization: +xs (_:xs) + +Conditional Generalization: +xs ys when length xs /= length ys + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +xs xs + + +checks :: [Integer] + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +[] + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +[] [0] + +Generalization: +xs (_:xs) + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +xs xs + + +checks :: [Char] + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +"" + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +"" "a" + +Generalization: +cs (_:cs) + +*** Failed! Falsifiable (after 1 tests): +"" "" + +Generalization: +cs cs + + +checks :: [Ordering] + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +[] + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +[] [LT] + +Generalization: +os (_:os) + +*** Failed! Falsifiable (after 1 tests): +[] [] + +Generalization: +os os + + +checks :: ((),Int) + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +((),0) + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +((),0) ((),1) + +Generalization: +(_,0) (_,1) + +Conditional Generalization: +(_,x) (_,y) when x /= y + +*** Failed! Falsifiable (after 1 tests): +((),0) ((),0) + +Generalization: +ux ux + + +checks :: (Bool,Char) + ++++ OK, passed 194 tests (exhausted). + +*** Failed! Falsifiable (after 1 tests): +(False,'a') + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +(False,'a') (True,'a') + +Generalization: +(False,_) (True,_) + +Conditional Generalization: +(_,c) (_,d) when c /= d + +*** Failed! Falsifiable (after 1 tests): +(False,'a') (False,'a') + +Generalization: +pc pc + + +checks :: (Int,(),Bool) + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +(0,(),False) + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +(0,(),False) (0,(),True) + +Generalization: +(_,_,False) (_,_,True) + +Conditional Generalization: +(x,_,_) (y,_,_) when x /= y + +*** Failed! Falsifiable (after 1 tests): +(0,(),False) (0,(),False) + +Generalization: +xup xup + + +checks :: Maybe () + ++++ OK, passed 2 tests (exhausted). + +*** Failed! Falsifiable (after 1 tests): +Nothing + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +Nothing (Just ()) + +Generalization: +Nothing (Just _) + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +mu mu + + +checks :: Maybe Int + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +Nothing + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +Nothing (Just 0) + +Generalization: +Nothing (Just _) + +*** Failed! Falsifiable (after 1 tests): +Nothing Nothing + +Generalization: +mx mx + + +checks :: Either () Bool + ++++ OK, passed 3 tests (exhausted). + +*** Failed! Falsifiable (after 1 tests): +Left () + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +(Left ()) (Right False) + +Generalization: +(Left _) (Right _) + +*** Failed! Falsifiable (after 1 tests): +(Left ()) (Left ()) + +Generalization: +eup eup + + +checks :: Either Int Char + ++++ OK, passed 360 tests. + +*** Failed! Falsifiable (after 1 tests): +Left 0 + +Generalization: +_ + +*** Failed! Falsifiable (after 2 tests): +(Left 0) (Right 'a') + +Generalization: +(Left _) (Right _) + +*** Failed! Falsifiable (after 1 tests): +(Left 0) (Left 0) + +Generalization: +exc exc + + diff --git a/tests/model/bench/true.out b/tests/model/bench/true.out new file mode 100644 --- /dev/null +++ b/tests/model/bench/true.out @@ -0,0 +1,180 @@ +checks :: () + ++++ OK, passed 1 tests (exhausted). + ++++ OK, passed 1 tests (exhausted). + ++++ OK, passed 1 tests (exhausted). + + +checks :: Bool + ++++ OK, passed 2 tests (exhausted). + ++++ OK, passed 4 tests (exhausted). + ++++ OK, passed 8 tests (exhausted). + + +checks :: Int + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: Integer + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: Char + ++++ OK, passed 97 tests (exhausted). + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: Ordering + ++++ OK, passed 3 tests (exhausted). + ++++ OK, passed 9 tests (exhausted). + ++++ OK, passed 27 tests (exhausted). + + +checks :: [()] + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: [Bool] + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: [Int] + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: [Integer] + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: [Char] + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: [Ordering] + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: ((),Int) + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: (Bool,Char) + ++++ OK, passed 194 tests (exhausted). + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: (Int,(),Bool) + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: (Ordering,Char,Integer) + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: Maybe () + ++++ OK, passed 2 tests (exhausted). + ++++ OK, passed 4 tests (exhausted). + ++++ OK, passed 8 tests (exhausted). + + +checks :: Maybe Int + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +checks :: Either () Bool + ++++ OK, passed 3 tests (exhausted). + ++++ OK, passed 9 tests (exhausted). + ++++ OK, passed 27 tests (exhausted). + + +checks :: Either Int Char + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + diff --git a/tests/model/eg/calculator.out b/tests/model/eg/calculator.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/calculator.out @@ -0,0 +1,20 @@ +*** Failed! Falsifiable (after 20 tests): +Div (C 0) (Add (C 0) (C 0)) + +Generalization: +Div (C _) (Add (C 0) (C 0)) + +Conditional Generalization: +Div e1 (Add (C 0) (C 0)) when noDiv0 e1 + +*** Failed! Falsifiable (after 5 tests): +Div (C 0) (C 0) + +Generalization: +Div _ (C 0) + +Conditional Generalization: +e1 when not (noDiv0 e1) + +False +True diff --git a/tests/model/eg/gencalc.out b/tests/model/eg/gencalc.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/gencalc.out @@ -0,0 +1,14 @@ +*** Failed! Falsifiable (after 20 tests): +Div (C 0) (Add (C 0) (C 0)) + +Generalization: +Div (C _) (Add (C 0) (C 0)) + +*** Failed! Falsifiable (after 5 tests): +Div (C 0) (C 0) + +Generalization: +Div _ (C 0) + +False +True diff --git a/tests/model/eg/heap.out b/tests/model/eg/heap.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/heap.out @@ -0,0 +1,8 @@ +*** Failed! Falsifiable (after 1053 tests): +(HeapPP {program = Insert 0 (Insert 1 (Insert 0 (Unit 0))), theHeap = Node 0 (Node 0 (Node 1 Nil Nil) (Node 0 Nil Nil)) Nil}) +*** Failed! Falsifiable (after 1053 tests): +heappp (Insert 0 (Insert 1 (Insert 0 (Unit 0)))) + +Conditional Generalization: +heappp (Insert x (Insert y (Insert x (Unit x)))) when x < y + diff --git a/tests/model/eg/int.out b/tests/model/eg/int.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/int.out @@ -0,0 +1,47 @@ +Properties that should be OK: ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + ++++ OK, passed 500 tests. + + +Properties that should fail: +*** Failed! Falsifiable (after 1 tests): +0 + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +0 + +Generalization: +_ + +*** Failed! Falsifiable (after 1 tests): +0 0 + +Generalization: +x x + +*** Failed! Falsifiable (after 1 tests): +0 0 0 + +Generalization: +_ x x + +*** Failed! Falsifiable (after 1 tests): +(0,0) + +Generalization: +(x,x) + +*** Failed! Falsifiable (after 1 tests): +(0,0,0) + +Generalization: +(_,x,x) + diff --git a/tests/model/eg/list.out b/tests/model/eg/list.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/list.out @@ -0,0 +1,46 @@ ++++ OK, passed 500 tests. + +*** Failed! Falsifiable (after 4 tests): +[] [0,0] + +Generalization: +xs (x:x:xs) + +Conditional Generalization: +xs (_:xs) when xs /= [] + +*** Failed! Falsifiable (after 6 tests): +[0,1] + +Conditional Generalization: +[x,y] when x /= y + +*** Failed! Falsifiable (after 3 tests): +[0,0] + +Generalization: +x:x:_ + +Conditional Generalization: +x:xs when elem x xs + +*** Failed! Falsifiable (after 2 tests): +[0] + +Generalization: +_:_ + +Conditional Generalization: +xs when xs /= [] + +*** Failed! Falsifiable (after 2 tests): +[] [0] + +Generalization: +_ (_:_) + +Conditional Generalization: +_ xs when xs /= [] + ++++ OK, passed 500 tests. + diff --git a/tests/model/eg/overflow.out b/tests/model/eg/overflow.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/overflow.out @@ -0,0 +1,3 @@ +*** Failed! Falsifiable (after 8792 tests): +T [] [] [] [-1] [-32768] + diff --git a/tests/model/eg/overflow8.out b/tests/model/eg/overflow8.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/overflow8.out @@ -0,0 +1,6 @@ +*** Failed! Falsifiable (after 896 tests): +T [-1] [-128] + +Conditional Generalization: +T ((-1):xs) ((-128):xs) when 0 == sum xs + diff --git a/tests/model/eg/parser.out b/tests/model/eg/parser.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/parser.out @@ -0,0 +1,11 @@ +*** Failed! Falsifiable (after 96 tests): +(Lang {modules = [], funcs = [Func {fnName = Var "a", args = [And (Int 0) (Bool False)], stmts = []}]}) +*** Failed! Falsifiable (after 96 tests): +Lang [] [Func (Var "a") [And (Int 0) (Bool False)] []] + +Generalization: +Lang _ (Func _ (And (Int _) (Bool _):_) _:_) + +Conditional Generalization: +Lang _ (Func _ (And e f:_) _:_) when e /= f + diff --git a/tests/model/eg/redblack.out b/tests/model/eg/redblack.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/redblack.out @@ -0,0 +1,20 @@ ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + ++++ OK, passed 1080 tests. + diff --git a/tests/model/eg/sorting.out b/tests/model/eg/sorting.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/sorting.out @@ -0,0 +1,31 @@ ++++ OK, passed 500 tests. + +*** Failed! Falsifiable (after 4 tests): +0 [0,0] + +Generalization: +x (x:x:_) + +Conditional Generalization: +x xs when count x xs > 1 + +*** Failed! Falsifiable (after 4 tests): +0 [0,0] + +Generalization: +x (x:x:_) + +Conditional Generalization: +x (x:xs) when elem x xs + ++++ OK, passed 99 tests. + +*** Failed! Falsifiable (after 7 tests): +False [False,False] + +Generalization: +p (p:p:_) + +Conditional Generalization: +p (p:ps) when elem p ps + diff --git a/tests/model/eg/word-refinements.out b/tests/model/eg/word-refinements.out new file mode 100644 --- /dev/null +++ b/tests/model/eg/word-refinements.out @@ -0,0 +1,35 @@ +*** Failed! Falsifiable (after 4 tests): +" " + +Generalization: +' ':_ + +Conditional Generalization: +c:_ when c <= ' ' + +*** Failed! Falsifiable (after 4 tests): +" " + +Generalization: +' ':_ + +Conditional Generalization: +c:_ when isSpace c + +*** Failed! Falsifiable (after 43 tests): +"a a" + +Conditional Generalization: +c:' ':' ':c:"" when not (isSpace c) + +*** Failed! Falsifiable (after 4 tests): +" " + +Generalization: +' ':_ + +Conditional Generalization: +cs when " " `isInfixOf` cs + ++++ OK, passed 500 tests. + diff --git a/tests/test-sdist b/tests/test-sdist new file mode 100644 --- /dev/null +++ b/tests/test-sdist @@ -0,0 +1,28 @@ +#!/bin/bash +# +# test-sdist: tests the package generated by "cabal sdist". +# +# Copyright (c) 2015-2018 Rudy Matela. +# Distributed under the 3-Clause BSD licence. +pkgver=` cat *.cabal | grep "^version:" | sed -e "s/version: *//"` +pkgname=`cat *.cabal | grep "^name:" | sed -e "s/name: *//"` +pkg=$pkgname-$pkgver +set -x +cabal sdist && +cd dist && +if [ -d ../.git ] +then + # on git repo, test if files are the same + git -C .. ls-files | sort > ls-git && + tar -tf $pkg.tar.gz | grep -v "/$" | sed -e "s,$pkg/,," | sort > ls-cabal && + diff -rud ls-git ls-cabal && + rm -f ls-git ls-cabal +else + # outside of git repo, test build + rm -rf $pkg/ && + tar -xzf $pkg.tar.gz && + cd $pkg/ && + cabal configure --enable-tests --enable-benchmarks && + cabal build && + cabal test +fi