packages feed

extrapolate 0.3.2 → 0.3.3

raw patch · 102 files changed

+5302/−2 lines, 102 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

+ .gitignore view
@@ -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
+ .travis.yml view
@@ -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 <rudy@matela.com.br>++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
+ Makefile view
@@ -0,0 +1,180 @@+# Makefile for Extrapolate+#+# Copyright:   (c) 2015-2018 Rudy Matela+# License:     3-Clause BSD  (see the file LICENSE)+# Maintainer:  Rudy Matela <rudy@matela.com.br>+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
+ bench/diff.hs view
@@ -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.
+ bench/eq.hs view
@@ -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.
+ bench/false.hs view
@@ -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 ""
+ bench/lazy-sc/Makefile view
@@ -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
+ bench/lazy-sc/calculator.hs view
@@ -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
+ bench/lazy-sc/list.hs view
@@ -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])
+ bench/lazy-sc/overflow.hs view
@@ -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
+ bench/lazy-sc/parser.hs view
@@ -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
+ bench/lazy-sc/revision.txt view
@@ -0,0 +1,2 @@+b5d9b460833ca34b1b57d5578cb57ee70905a0af+2014-07-07 15:44:24 +0100
+ bench/lazy-sc/sorting.hs view
@@ -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)
+ bench/lazy-sc/word-refinements.hs view
@@ -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
+ bench/ord.hs view
@@ -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 ""
+ bench/runtime/oubli/bench/diff.runtime view
@@ -0,0 +1,1 @@+16.30
+ bench/runtime/oubli/bench/eq.runtime view
@@ -0,0 +1,1 @@+1.02
+ bench/runtime/oubli/bench/false.runtime view
@@ -0,0 +1,1 @@+2.90
+ bench/runtime/oubli/bench/ord.runtime view
@@ -0,0 +1,1 @@+6.29
+ bench/runtime/oubli/bench/true.runtime view
@@ -0,0 +1,1 @@+0.18
+ bench/runtime/oubli/eg/calculator.runtime view
@@ -0,0 +1,1 @@+1.60
+ bench/runtime/oubli/eg/gencalc.runtime view
@@ -0,0 +1,1 @@+1.95
+ bench/runtime/oubli/eg/heap.runtime view
@@ -0,0 +1,1 @@+7.02
+ bench/runtime/oubli/eg/int.runtime view
@@ -0,0 +1,1 @@+0.48
+ bench/runtime/oubli/eg/list.runtime view
@@ -0,0 +1,1 @@+4.06
+ bench/runtime/oubli/eg/overflow.runtime view
@@ -0,0 +1,1 @@+0.18
+ bench/runtime/oubli/eg/overflow8.runtime view
@@ -0,0 +1,1 @@+17.21
+ bench/runtime/oubli/eg/parser.runtime view
@@ -0,0 +1,1 @@+1.80
+ bench/runtime/oubli/eg/redblack.runtime view
@@ -0,0 +1,1 @@+0.09
+ bench/runtime/oubli/eg/sorting.runtime view
@@ -0,0 +1,1 @@+13.48
+ bench/runtime/oubli/eg/word-refinements.runtime view
@@ -0,0 +1,1 @@+41.38
+ bench/runtime/zero/bench/diff.runtime view
@@ -0,0 +1,1 @@+7.05
+ bench/runtime/zero/bench/eq.runtime view
@@ -0,0 +1,1 @@+27.25
+ bench/runtime/zero/bench/false.runtime view
@@ -0,0 +1,1 @@+6.47
+ bench/runtime/zero/bench/ord.runtime view
@@ -0,0 +1,1 @@+13.25
+ bench/runtime/zero/bench/true.runtime view
@@ -0,0 +1,1 @@+0.08
+ bench/runtime/zero/eg/calculator.runtime view
@@ -0,0 +1,1 @@+0.79
+ bench/runtime/zero/eg/gencalc.runtime view
@@ -0,0 +1,1 @@+0.71
+ bench/runtime/zero/eg/heap.runtime view
@@ -0,0 +1,1 @@+4.29
+ bench/runtime/zero/eg/int.runtime view
@@ -0,0 +1,1 @@+4.18
+ bench/runtime/zero/eg/list.runtime view
@@ -0,0 +1,1 @@+10.17
+ bench/runtime/zero/eg/overflow.runtime view
@@ -0,0 +1,1 @@+0.21
+ bench/runtime/zero/eg/overflow8.runtime view
@@ -0,0 +1,1 @@+7.16
+ bench/runtime/zero/eg/parser.runtime view
@@ -0,0 +1,1 @@+8.91
+ bench/runtime/zero/eg/redblack.runtime view
@@ -0,0 +1,1 @@+0.02
+ bench/runtime/zero/eg/sorting.runtime view
@@ -0,0 +1,1 @@+12.02
+ bench/runtime/zero/eg/word-refinements.runtime view
@@ -0,0 +1,1 @@+11.42
+ bench/smartcheck/Makefile view
@@ -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
+ bench/smartcheck/bin/count-cons view
@@ -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
+ bench/smartcheck/bin/ncons-overflow view
@@ -0,0 +1,7 @@+#!/bin/bash+tail -n -1 -q overflow-out/* |+#wc -w; exit+while read s+do+	echo $s | wc -w+done
+ bench/smartcheck/bin/nvars-overflow view
@@ -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
+ bench/smartcheck/bin/sort-stats view
@@ -0,0 +1,4 @@+#!/bin/bash+#+# stats for sort+tail -qn -1 sorting-uncurry-out/* | sed -e "s/[^:]//g" | sort
+ bench/smartcheck/div0-main.hs view
@@ -0,0 +1,4 @@+-- main function for Div0++main :: IO ()+main = divTest
+ bench/smartcheck/list.hs view
@@ -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])
+ bench/smartcheck/overflow-main.hs view
@@ -0,0 +1,8 @@+-- main for paperExample1++instance SubTypes I+instance SubTypes T++main :: IO ()+main = do+  smartCheck scStdArgs{format = PrintString} prop
+ bench/smartcheck/parser-main.hs view
@@ -0,0 +1,4 @@+-- parse main++main :: IO ()+main = smartCheck scargs prop_parse
+ bench/smartcheck/revision.txt view
@@ -0,0 +1,2 @@+86bfe4a3f61bfd74fa79e1afb9b5a77d4ad58efb+2017-08-11 13:08:58 -0700
+ bench/smartcheck/sorting.hs view
@@ -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)
+ bench/smartcheck/word-refinements.hs view
@@ -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
+ bench/true.hs view
@@ -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 ""
+ eg/RedBlackSet.hs view
@@ -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')
+ eg/calculator.hs view
@@ -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.
+ eg/gencalc.hs view
@@ -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.
+ eg/heap.hs view
@@ -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)
+ eg/int.hs view
@@ -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)
+ eg/list.hs view
@@ -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])
+ eg/overflow.hs view
@@ -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
+ eg/overflow8.hs view
@@ -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
+ eg/parser.hs view
@@ -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
+ eg/redblack.hs view
@@ -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)
+ eg/sorting.hs view
@@ -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
+ eg/word-refinements.hs view
@@ -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
+ eg/xmonad/Makefile view
@@ -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
+ eg/xmonad/extrapolate.hs view
@@ -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))
+ eg/xmonad/revision.txt view
@@ -0,0 +1,2 @@+10b843ad21614994b7e12fafaf300f4267aa9e40+2017-04-10 16:58:45 -0700
+ eg/xmonad/xmonad.cabal view
@@ -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
extrapolate.cabal view
@@ -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
+ mk/All.hs view
@@ -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
+ mk/Toplibs.hs view
@@ -0,0 +1,4 @@+-- Using ghc --make in this module trigger compilation of all modules+module Toplibs () where++import Test.Extrapolate
+ mk/depend.mk view
@@ -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
+ mk/ghcdeps view
@@ -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 <<LIST+#   program.hs+#   Library.hs+#   Path/To/Library.hs+#   LIST+#   program: ...+#   Library.o: ...+#   Path/To/Library.o: ...+#+# Or:+#   $ find -name \*.hs -o -name \*.lhs | ghcdeps [GHCFLAGS]+#   ...+#+# Note that when using find, you have to remember to exclude unecessary files,+# e.g.:  dist, Setup.hs+#+# Yes, this is hacky.  But hey, it works.+while read fn+do+	ghc "$@" -dep-suffix=. -dep-makefile=tmp.mk -M "$fn" ||+	exit 1+	deps="`cat tmp.mk |+	       grep "hs$" |+	       sort |+	       sed -e "s/.*: //" |+	       tac |+	       tr '\n' ' ' |+	       sed -e "s/ $//"`"+	obj=`echo $fn | sed -e 's,^\./,,;s/\.hs$/.o/'`+	bin=`echo $fn | sed -e 's,^\./,,;s/\.hs$//'`+	echo "$obj: $deps"+	grep -q "main" "$fn" && echo "$bin: `echo $deps | sed -e 's|[^ ]*src[^ ]*||g'` mk/toplibs"+	rm -f tmp.mk+done |+sort |+sed -e 's,  *, \\\n  ,g'
+ mk/haddock-i view
@@ -0,0 +1,24 @@+#!/bin/bash+#+# haddock-i: list haddock's -i parameters.+#+# Copyright (c) 2015-2017 Rudy Matela.+# Distributed under the 3-Clause BSD licence.+#+# $ haddock-i <package1> <package2> ... <packageN>+#+# 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 <files>+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/"
+ mk/haskell.mk view
@@ -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)
+ stack.yaml view
@@ -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: []
+ tests/model/bench/diff.out view
@@ -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++
+ tests/model/bench/eq.out view
@@ -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'++
+ tests/model/bench/false.out view
@@ -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:+_ _ _++
+ tests/model/bench/ord.out view
@@ -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'++
+ tests/model/bench/true-false.out view
@@ -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++
+ tests/model/bench/true.out view
@@ -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.++
+ tests/model/eg/calculator.out view
@@ -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
+ tests/model/eg/gencalc.out view
@@ -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
+ tests/model/eg/heap.out view
@@ -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+
+ tests/model/eg/int.out view
@@ -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)+
+ tests/model/eg/list.out view
@@ -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.+
+ tests/model/eg/overflow.out view
@@ -0,0 +1,3 @@+*** Failed! Falsifiable (after 8792 tests):+T [] [] [] [-1] [-32768]+
+ tests/model/eg/overflow8.out view
@@ -0,0 +1,6 @@+*** Failed! Falsifiable (after 896 tests):+T [-1] [-128]++Conditional Generalization:+T ((-1):xs) ((-128):xs)  when  0 == sum xs+
+ tests/model/eg/parser.out view
@@ -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+
+ tests/model/eg/redblack.out view
@@ -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.+
+ tests/model/eg/sorting.out view
@@ -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+
+ tests/model/eg/word-refinements.out view
@@ -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.+
+ tests/test-sdist view
@@ -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