speculate 0.4.1 → 0.4.2
raw patch · 24 files changed
+293/−243 lines, 24 filesdep ~expressdep ~leancheckPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: express, leancheck
API changes (from Hackage documentation)
+ Test.Speculate.Expr.Core: fastCompare :: Expr -> Expr -> Ordering
+ Test.Speculate.Reason.Order: funny :: Expr -> Bool
+ Test.Speculate.Reason.Order: serious :: Expr -> Bool
Files
- .gitignore +2/−0
- .travis.yml +23/−13
- Makefile +8/−12
- TODO.md +0/−2
- bench/runtime-zero +30/−30
- eg/algebraic-graphs.hs +4/−5
- eg/pretty-compact.hs +2/−2
- mk/ghcdeps +1/−1
- mk/haddock-i +1/−1
- mk/haskell.mk +3/−3
- mk/install-on +30/−0
- speculate.cabal +8/−12
- src/Test/Speculate/Expr/Core.hs +11/−0
- src/Test/Speculate/Reason.hs +6/−5
- src/Test/Speculate/Reason/Order.hs +25/−1
- stack.yaml +3/−7
- test/model/algebraic-graphs-s4.out +30/−33
- test/model/algebraic-graphs.out +34/−38
- test/model/pretty-compact-s4.out +8/−4
- test/model/pretty-compact.out +8/−4
- test/order.hs +14/−24
- test/reason.hs +9/−20
- test/sdist +31/−24
- test/utils.hs +2/−2
.gitignore view
@@ -3,8 +3,10 @@ **/cabal.sandbox.config **/idx/ **/dist/+dist-newstyle **/log/ .stack-work+stack.yaml.lock doc/**/*.html doc/**/*.css
.travis.yml view
@@ -1,6 +1,6 @@ # .travis.yml file for Speculate #-# Copyright: (c) 2017-2018 Rudy Matela+# Copyright: (c) 2017-2020 Rudy Matela # License: 3-Clause BSD (see the file LICENSE) # Maintainer: Rudy Matela <rudy@matela.com.br> @@ -22,6 +22,9 @@ - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH - ghc --version - cabal --version+- haddock --version+- du -hd3 ~/.cabal ~/.ghc || true+- du -hd4 ~/.stack || true - rm -f ~/.cabal/config && cabal update # Download and unpack the stack executable # "Once Travis whitelists the stack.dev files," simply include stack in the@@ -31,36 +34,42 @@ - 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 express cmdargs+- cabal install leancheck express cmdargs || cabal install leancheck express cmdargs --lib script:-- make && make test-without-extra-deps+- make && make test - make haddock - make test-sdist-- travis_wait 40 cabal test expr --ghc-option=-O0-- travis_wait 40 stack $STACKR --no-terminal --skip-ghc-check test speculate:test:expr --ghc-options=-O0+- cabal test expr --ghc-option=-O0+- stack --resolver $STACKVER --no-terminal --skip-ghc-check test speculate:test:expr --ghc-options=-O0 matrix: allow_failures: - ghc: 'head' include: - ghc: 'head'- env: GHCVER=head CABALVER=head+ env: GHCVER=head CABALVER=head STACKVER=nightly-2020-03-28 addons: {apt: {packages: [ghc-head, cabal-install-head], sources: hvr-ghc}}+ - ghc: '8.10'+ env: GHCVER=8.10.1 CABALVER=3.2 STACKVER=nightly-2020-03-28+ addons: {apt: {packages: [ghc-8.10.1, cabal-install-3.2], sources: hvr-ghc}}+ - ghc: '8.8'+ env: GHCVER=8.8.3 CABALVER=3.0 STACKVER=lts-15.5+ addons: {apt: {packages: [ghc-8.8.3, cabal-install-3.0], sources: hvr-ghc}} - ghc: '8.6'- env: GHCVER=8.6.1 CABALVER=2.4- addons: {apt: {packages: [ghc-8.6.1, cabal-install-2.4], sources: hvr-ghc}}+ env: GHCVER=8.6.5 CABALVER=2.4 STACKVER=lts-14.27+ addons: {apt: {packages: [ghc-8.6.5, cabal-install-2.4], sources: hvr-ghc}} - ghc: '8.4'- env: GHCVER=8.4.4 CABALVER=2.2+ env: GHCVER=8.4.4 CABALVER=2.2 STACKVER=lts-12.26 addons: {apt: {packages: [ghc-8.4.4, cabal-install-2.2], sources: hvr-ghc}} - ghc: '8.2'- env: GHCVER=8.2.2 CABALVER=2.0+ env: GHCVER=8.2.2 CABALVER=2.0 STACKVER=lts-11.22 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+ env: GHCVER=8.0.2 CABALVER=1.24 STACKVER=lts-9.21 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+ env: GHCVER=7.10.3 CABALVER=1.22 STACKVER=lts-6.35 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'@@ -70,11 +79,12 @@ - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH - ghc --version - cabal --version+ - haddock --version - rm -f ~/.cabal/config && cabal update - cabal install Cabal==1.18.* - cabal install leancheck express cmdargs script:- - make && make test-without-extra-deps+ - make && make test - make haddock HADDOCKFLAGS= - make test-sdist - cabal test
Makefile view
@@ -24,7 +24,7 @@ test/reason \ test/utils \ test/stats-MOSTEG = \+EG = \ eg/arith \ eg/arith-negate-abs \ eg/bool \@@ -48,13 +48,12 @@ eg/tauts \ eg/monad \ eg/tuples \+ eg/speculate-reason \ bench/arithficial \ bench/nord \ bench/unit-EG = $(MOSTEG) \+EXTRAEG = \ eg/regexes \- eg/speculate-reason-EXTRAEG = $(EG) \ eg/pretty-compact \ eg/algebraic-graphs # regexes needs regex-tdfa, which may break the build@@ -82,11 +81,8 @@ $(patsubst %,%.run,$(TESTS)) \ $(patsubst %,%.diff-test,$(EG) $(wildcard bench/*-c)) -test-without-extra-deps: all $(patsubst %,%.run,$(TESTS)) \- $(patsubst %,%.diff-test,$(MOSTEG) $(wildcard bench/*-c))--test-extra-deps: all $(patsubst %,%.run,$(TESTS)) \- $(patsubst %,%.diff-test,$(EXTRAEG) $(wildcard bench/*-c))+test-with-extra-deps: all test test-sdist \+ $(patsubst %,%.diff-test,$(EXTRAEG) $(wildcard bench/*-c)) test-sdist: ./test/sdist@@ -171,13 +167,13 @@ update-slow-diff-test: $(patsubst %,%.update-slow-diff-test,$(EG) $(wildcard bench/*-c)) -bench: all+bench: all $(EG) ./test/benchmark-cmp $(EG) bench/*-c -save-bench: all+save-bench: all $(EG) ./test/benchmark-save $(EG) bench/*-c -memory-benchmark: all+memory-benchmark: all $(EG) ./test/memory-benchmark $(EG) bench/*-c qs-bench:
TODO.md view
@@ -10,8 +10,6 @@ I can use a custom data structure that computes matches all at once while traversing an expression. -* fix issues with Dershowitz and Knuth-Bendix orders.- * (code readability) review and document code * (code readability) rename semi to inqualities everywhere.
bench/runtime-zero view
@@ -1,35 +1,35 @@ GHC 8.6.5-express-0.1.0+express-0.1.1 leancheck-0.9.1 arith 0.260-arith-c 0.610-arithficial 0.976-arith-negate-abs 1.823-binarytree 1.793-binarytree0 0.533-bool 1.950-bool-c 1.753-colour 2.206-digraphs 1.603-fun 1.243-insertsort 8.320-insertsort0 1.000-length 0.640-list 2.730-list-c 1.673-minus 0.580-minus-c 0.966-monad 0.653+arith-c 0.603+arithficial 0.966+arith-negate-abs 1.846+binarytree 1.753+binarytree0 0.520+bool 1.983+bool-c 1.723+colour 2.130+digraphs 1.560+fun 1.190+insertsort 8.593+insertsort0 0.996+length 0.646+list 2.826+list-c 1.770+minus 0.603+minus-c 0.996+monad 0.690 nord 0.010-oddeven 6.930-plus-abs 3.866-pretty 9.183-ratio 9.320-regexes 8.300-sets 7.610-speculate-reason 3.710-string 0.953-tauts 4.466-tuples 1.313+oddeven 7.340+plus-abs 3.786+pretty 9.080+ratio 9.300+regexes 8.013+sets 7.696+speculate-reason 3.300+string 0.950+tauts 4.286+tuples 1.286 unit 0.010-zip 2.490+zip 2.463
eg/algebraic-graphs.hs view
@@ -1,14 +1,10 @@ {-# LANGUAGE TemplateHaskell #-} import Test.Speculate-import Test.Speculate.Expr.Instance (name) import Data.Function (on) import Control.Monad (unless) import Algebra.Graph -instance Ord a => Ord (Graph a) where- (<=) = isSubgraphOf- -- deriveListable ''Graph {- instance (Ord a, Listable a) => Listable (Graph a) where tiers = concatMapT graphs $ setsOf tiers@@ -18,8 +14,12 @@ fromAdjList :: [(a,[a])] -> Graph a fromAdjList ness = graph [n | (n,_) <- ness] [(n1,n2) | (n1,n2s) <- ness, n2 <- n2s]+ graph vs es = foldr overlay empty $ map vertex vs ++ map (uncurry edge) es -- -} +instance Name Nat3 where name _ = "x"+instance Name (Graph a) where name _ = "g1"+ main :: IO () main = do unless (listableGraphOK 180 a) $@@ -41,7 +41,6 @@ , constant "overlay" (overlay -:> gr a) , constant "connect" (connect -:> gr a) , constant "edge" (edge -:> a)- , constant "length" (length -:> gr a) , constant "size" (size -:> gr a) ] , showConditions = False
eg/pretty-compact.hs view
@@ -34,11 +34,11 @@ da :: Doc Any da = undefined -instance Name Doc where name _ = "d1"+instance Name (Doc a) where name _ = "d1" main :: IO () main = speculate args- { instances = [reifyInstances "d1" da]+ { instances = [reifyInstances da] , showConditions = False , maxSize = 4 , maxTests = 360
mk/ghcdeps view
@@ -2,7 +2,7 @@ # # ghcdeps: generate Haskell make dependencies for compiling with GHC. #-# Copyright (c) 2015-2019 Rudy Matela.+# Copyright (c) 2015-2020 Rudy Matela. # Distributed under the 3-Clause BSD licence. # # From a list of files provided on standard input,
mk/haddock-i view
@@ -2,7 +2,7 @@ # # haddock-i: list haddock's -i parameters. #-# Copyright (c) 2015-2019 Rudy Matela.+# Copyright (c) 2015-2020 Rudy Matela. # Distributed under the 3-Clause BSD licence. # # $ haddock-i <package1> <package2> ... <packageN>
mk/haskell.mk view
@@ -1,6 +1,6 @@ # Implicit rules for compiling Haskell code. #-# Copyright (c) 2015-2019 Rudy Matela.+# Copyright (c) 2015-2020 Rudy Matela. # Distributed under the 3-Clause BSD licence. # # You can optionally configure the "Configuration variables" below in your main@@ -39,7 +39,7 @@ # 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 \+LIST_ALL_HSS ?= find \( -path "./dist*" -o -path "./.stack-work" -o -path "./Setup.hs" \) -prune \ -o -name "*.*hs" -print LIB_HSS ?= $(shell $(LIST_LIB_HSS)) ALL_HSS ?= $(shell $(LIST_ALL_HSS))@@ -97,7 +97,7 @@ haddock: doc/index.html clean-haddock:- rm -f doc/*.{html,css,js,png,gif,json} doc/src/*.{html,css,js} README.html+ rm -f doc/*.{html,css,js,png,gif,json} doc/src/* README.html upload-haddock: @echo "use \`cabal upload -d' instead"
+ mk/install-on view
@@ -0,0 +1,30 @@+#!/bin/bash+#+# mk/install-on: install or updates the mk folder on a Haskell project+#+# usage: ./mk/install-on path/to/project+#+# This assumes a few things:+#+# * tests are stored in a "test/" folder+# * sources are stored in a "src/" folder+set -e++errxit() {+ echo "$@" > /dev/stderr+ exit 1+}++src=`dirname $0`/..+dst="$1"++[ -n "$dst" ] || errxit "destination folder not provided"++mkdir -p $dst/mk+mkdir -p $dst/test++cp $src/mk/ghcdeps $dst/mk/ghcdeps+cp $src/mk/haddock-i $dst/mk/haddock-i+cp $src/mk/haskell.mk $dst/mk/haskell.mk+cp $src/mk/install-on $dst/mk/install-on+cp $src/test/sdist $dst/test/sdist
speculate.cabal view
@@ -1,5 +1,5 @@ name: speculate-version: 0.4.1+version: 0.4.2 synopsis: discovery of properties about Haskell functions description: Speculate automatically discovers laws about Haskell functions.@@ -57,6 +57,7 @@ , mk/ghcdeps , mk/haddock-i , mk/haskell.mk+ , mk/install-on , stack.yaml , test/benchmark , test/benchmark-cmp@@ -67,7 +68,9 @@ , test/update-diff , test/sdist -tested-with: GHC==8.6+tested-with: GHC==8.10+ , GHC==8.8+ , GHC==8.6 , GHC==8.4 , GHC==8.2 , GHC==8.0@@ -81,7 +84,7 @@ source-repository this type: git location: https://github.com/rudymatela/speculate- tag: v0.4.1+ tag: v0.4.2 library@@ -117,8 +120,8 @@ , Test.Speculate.Utils.Timeout , Test.Speculate.Utils.Tuple build-depends: base >= 4 && < 5- , leancheck >= 0.9.1- , express >= 0.1.1+ , leancheck >= 0.9.3+ , express >= 0.1.3 , cmdargs , containers hs-source-dirs: src@@ -177,13 +180,6 @@ other-modules: Test, Test.ListableExpr hs-source-dirs: test build-depends: base >= 4 && < 5, leancheck, express, speculate- default-language: Haskell2010- type: exitcode-stdio-1.0--benchmark plus-abs- main-is: plus-abs.hs- hs-source-dirs: eg- build-depends: base >= 4 && < 5, speculate default-language: Haskell2010 type: exitcode-stdio-1.0
src/Test/Speculate/Expr/Core.hs view
@@ -14,6 +14,7 @@ -- * Order , lexicompare , lexicompareBy+ , fastCompare -- * Properties , isConstantNamed@@ -37,6 +38,16 @@ import Test.Speculate.Utils.List import Data.Monoid ((<>)) import Data.Functor ((<$>)) -- for GHC <= 7.8++-- faster comparison, to be used when nubSorting Expr values+fastCompare :: Expr -> Expr -> Ordering+fastCompare = cmp+ where+ (f :$ x) `cmp` (g :$ y) = f `cmp` g <> x `cmp` y+ (_ :$ _) `cmp` _ = GT+ _ `cmp` (_ :$ _) = LT+ x@(Value n1 _) `cmp` y@(Value n2 _) = typ x `compareTy` typ y+ <> n1 `compare` n2 lexicompare :: Expr -> Expr -> Ordering lexicompare = lexicompareBy compare
src/Test/Speculate/Reason.hs view
@@ -208,22 +208,23 @@ $ criticalPairs thy criticalPairs :: Thy -> [(Expr,Expr)]-criticalPairs thy@Thy {rules = rs, compareE = cmp} =- nubMerges [r `criticalPairsWith` s | r <- rs, s <- rs]+criticalPairs thy@Thy{rules = rs} =+ nubMergesBy fastCompareEqn [r `criticalPairsWith` s | r <- rs, s <- rs] where criticalPairsWith :: Rule -> Rule -> [(Expr,Expr)] r1@(e1,_) `criticalPairsWith` r2@(e2,_) =- nubSortBy (compareEqn thy)+ nubSortBy fastCompareEqn . map sortuple . filter (uncurry (/=)) . concatMap (\e -> (e `reductions1` r1) ** (e `reductions1` r2))- . nubSortBy cmp+ . nubSortBy fastCompare $ overlaps e1 e2 xs ** ys = [(x,y) | x <- xs, y <- ys] sortuple (x,y) | x < y = (y,x) | otherwise = (x,y)+ fastCompareEqn = fastCompare `on` foldPair (<) :: Expr -> Expr -> Bool- e1 < e2 = e1 `cmp` e2 == LT+ e1 < e2 = e1 `fastCompare` e2 == LT -- Warning: will have to also be applied in reverse to get all overlaps. --
src/Test/Speculate/Reason/Order.hs view
@@ -16,6 +16,8 @@ , weight , weightExcept , gtExcept+ , funny+ , serious ) where @@ -47,7 +49,6 @@ (>|) :: Expr -> Expr -> Bool (>|) = kboBy weight (>) infix 4 >|--- TODO: FIXME: this KBO is not closed under substitution! kboBy :: (Expr -> Int) -> (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool kboBy w (->-) e1 e2 = e1 >=\/ e2@@ -123,6 +124,8 @@ -- -- > x - y |> x + negate y -- as (-) > (+) -- > negate x + y |> negate (x + negate y) -- as (+) > negate, as I->I->I > I->I+--+-- This is not a simplification order on 'funny' 'Expr's. (|>) :: Expr -> Expr -> Bool (|>) = dwoBy (>) infix 4 |>@@ -130,6 +133,8 @@ -- | Dershowitz reduction order as defined in TRAAT -- -- @|>@ a "D" for Dershowitz+--+-- This is not a simplification order on 'funny' 'Expr's. dwoBy :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Bool dwoBy (>) = (|>) where@@ -147,6 +152,25 @@ e1 |>= e2 = e1 == e2 || e1 |> e2 +-- | Returns 'True' when an 'Expr'ession has either+-- a functional type or functional 'var'iables.+--+-- > funny xx = False+-- > funny one = False+-- > funny idE = True+-- > funny (ff one) = True+funny :: Expr -> Bool+funny e = any (isFunTy . typ) $ e:vars e++-- | Returns 'True' when an 'Expr'ession has+-- no functional return type and no functional 'var'iables.+--+-- > serious xx = True+-- > serious one = True+-- > serious idE = False+-- > serious (ff one) = False+serious :: Expr -> Bool+serious = not . funny --- Misc Utilities ---
stack.yaml view
@@ -1,12 +1,8 @@-resolver: lts-13.30+resolver: lts-15.5 # or ghc-8.8.3 packages: - . extra-deps:-- leancheck-0.9.1-- express-0.1.1--flags: {}--extra-package-dbs: []+- leancheck-0.9.3+- express-0.1.3
test/model/algebraic-graphs-s4.out view
@@ -2,10 +2,10 @@ max #-tests = 1080 max #-vars = 2 (for inequational and conditional laws) -_ :: Bool (holes: Bool)-_ :: Int (holes: Int)-_ :: Nat3 (holes: Nat3)-_ :: Graph Nat3 (holes: Graph Nat3)+_ :: Bool+_ :: Int+_ :: Nat3+_ :: Graph Nat3 0 :: Nat3 0 :: Int True :: Bool@@ -16,36 +16,33 @@ overlay :: Graph Nat3 -> Graph Nat3 -> Graph Nat3 connect :: Graph Nat3 -> Graph Nat3 -> Graph Nat3 edge :: Nat3 -> Nat3 -> Graph Nat3-length :: Graph Nat3 -> Int size :: Graph Nat3 -> Int -length (vertex i) == length (vertex j)- size (vertex i) == length (vertex 0)-length (edge i j) == length (edge k i')-length (edge i j) == size (edge k i')- length (x * y) == length (x + y)- size (x * y) == size (x + y)- x + x == x- x + empty == x- x * empty == x- empty * x == x- x + y == y + x- overlay x y == x + y- connect x y == x * y+size (vertex x) == size empty+size (edge x y) == size (edge z x')+ size (g1 * g2) == size (g1 + g2)+ g1 + g1 == g1+ g1 + empty == g1+ g1 * empty == g1+ empty * g1 == g1+ g1 + g2 == g2 + g1+ overlay g1 g2 == g1 + g2+ connect g1 g2 == g1 * g2 - 0 <= length x- 0 <= size x- length x <= size x- size empty <= size x- length x <= length (x + y)- size x <= size (x + y)- length x <= size (y + x)-length (edge i i) <= size x- empty <= x- x <= x + y- x <= x * y- x <= y * x- vertex i <= edge i j- vertex i <= edge j i- x + y <= x * y+ 0 <= size g1+ size empty <= size g1+ size g1 <= size (g1 + g2)+size (edge x x) <= size (g1 + g2)+ empty <= g1+ g1 <= g1 + g2+ g1 <= g1 * g2+ g1 <= g2 * g1+ vertex 0 <= vertex x+ vertex x <= edge x y+ vertex x <= edge y x+ edge x x <= edge x y+ edge x x <= edge y x+ g1 + g2 <= g1 * g2+ edge 0 0 <= edge x y+ edge 0 x <= edge x 0
test/model/algebraic-graphs.out view
@@ -4,10 +4,10 @@ max #-tests = 1080 max #-vars = 2 (for inequational and conditional laws) -_ :: Bool (holes: Bool)-_ :: Int (holes: Int)-_ :: Nat3 (holes: Nat3)-_ :: Graph Nat3 (holes: Graph Nat3)+_ :: Bool+_ :: Int+_ :: Nat3+_ :: Graph Nat3 0 :: Nat3 0 :: Int True :: Bool@@ -18,41 +18,37 @@ overlay :: Graph Nat3 -> Graph Nat3 -> Graph Nat3 connect :: Graph Nat3 -> Graph Nat3 -> Graph Nat3 edge :: Nat3 -> Nat3 -> Graph Nat3-length :: Graph Nat3 -> Int size :: Graph Nat3 -> Int - length (vertex i) == length (vertex j)- size (vertex i) == length (vertex 0)- length (x * y) == length (x + y)- size (x * y) == size (x + y)-length (x + vertex i) == length (x + vertex j)- size (x + vertex i) == size (x + vertex j)- x + x == x- x + empty == x- x * empty == x- empty * x == x- x + y == y + x- overlay x y == x + y- connect x y == x * y- x + x * y == x * y- x + y * x == y * x- edge i j == vertex i * vertex j- (x + y) + z == x + (y + z)- (x * y) * z == x * (y * z)- x * (x * y) == x * (x + y)- (x + y) * x == y * (x * x)+ size (vertex x) == size empty+ size (g1 * g2) == size (g1 + g2)+size (g1 + vertex x) == size (g1 + vertex y)+ g1 + g1 == g1+ g1 + empty == g1+ g1 * empty == g1+ empty * g1 == g1+ g1 + g2 == g2 + g1+ overlay g1 g2 == g1 + g2+ connect g1 g2 == g1 * g2+ g1 + g1 * g2 == g1 * g2+ g1 + g2 * g1 == g2 * g1+ edge x y == vertex x * vertex y+ (g1 + g2) + g3 == g1 + (g2 + g3)+ (g1 * g2) * g3 == g1 * (g2 * g3)+ g1 * (g1 * g2) == g1 * (g1 + g2)+ (g1 + g2) * g1 == g2 * (g1 * g1) - 0 <= length x- 0 <= size x- length x <= size x-size empty <= size x- length x <= length (x + y)- size x <= size (x + y)- length x <= size (y + x)-size empty <= length (edge i i)- empty <= x- x <= x + y- x <= x * y- x <= y * x- x + y <= x * y+ 0 <= size g1+size empty <= size g1+ size g1 <= size (g1 + g2)+ empty <= g1+ g1 <= g1 + g2+ g1 <= g1 * g2+ g1 <= g2 * g1+ vertex 0 <= vertex x+ edge x x <= edge x y+ edge x x <= edge y x+ g1 + g2 <= g1 * g2+ edge 0 0 <= edge x y+ edge 0 x <= edge x 0
test/model/pretty-compact-s4.out view
@@ -4,10 +4,10 @@ max #-tests = 360 max #-vars = 2 (for inequational and conditional laws) -_ :: Char (holes: Char)-_ :: Int (holes: Int)-_ :: ODoc Any (holes: ODoc Any)-_ :: [Char] (holes: [Char])+_ :: Char+_ :: Int+_ :: ODoc Any+_ :: [Char] text :: [Char] -> ODoc Any char :: Char -> ODoc Any flush :: ODoc Any -> ODoc Any@@ -18,6 +18,10 @@ (</>) :: ODoc Any -> ODoc Any -> ODoc Any (<//>) :: ODoc Any -> ODoc Any -> ODoc Any (<$$>) :: ODoc Any -> ODoc Any -> ODoc Any++Warning: no Listable instance for Any, variables of this type will not be considered+Warning: no Eq instance for Any, equations of this type will not be considered+Warning: no Ord instance for Any, inequations of this type will not be considered d1 $$ d2 == flush d1 <> d2 d1 <$$> d2 == flush d1 <> d2
test/model/pretty-compact.out view
@@ -4,10 +4,10 @@ max #-tests = 360 max #-vars = 2 (for inequational and conditional laws) -_ :: Char (holes: Char)-_ :: Int (holes: Int)-_ :: ODoc Any (holes: ODoc Any)-_ :: [Char] (holes: [Char])+_ :: Char+_ :: Int+_ :: ODoc Any+_ :: [Char] text :: [Char] -> ODoc Any char :: Char -> ODoc Any flush :: ODoc Any -> ODoc Any@@ -18,6 +18,10 @@ (</>) :: ODoc Any -> ODoc Any -> ODoc Any (<//>) :: ODoc Any -> ODoc Any -> ODoc Any (<$$>) :: ODoc Any -> ODoc Any -> ODoc Any++Warning: no Listable instance for Any, variables of this type will not be considered+Warning: no Eq instance for Any, equations of this type will not be considered+Warning: no Ord instance for Any, inequations of this type will not be considered d1 $$ d2 == flush d1 <> d2 d1 <$$> d2 == flush d1 <> d2
test/order.hs view
@@ -1,7 +1,6 @@ {-# Language DeriveDataTypeable, StandaloneDeriving #-} -- Travis import Test import Test.Speculate.Utils-import qualified Test.LeanCheck.Utils as LC (comparison) import Test.Speculate.Expr import Test.Speculate.Reason (emptyThy)@@ -21,8 +20,8 @@ [ True -- see test-expr.hs for general Expr orders , holds n $ compare ==== (compareComplexity <> lexicompare)- , holds n $ LC.comparison lexicompare- , holds n $ LC.comparison compareComplexity+ , holds n $ isComparison lexicompare+ , holds n $ isComparison compareComplexity , holds n $ \(IntToIntE e1) (IntToIntE e2) (IntE e3) -> let cmp = lexicompare in e1 `cmp` e2 == (e1 :$ e3) `cmp` (e2 :$ e3)@@ -39,6 +38,10 @@ , value "xx" xx < value "emptyThyght" (Thyght emptyThy) , holds n $ simplificationOrder (|>|)+ , holds n $ seriousSimplificationOrder (|> )+ , holds n $ seriousSimplificationOrder (dwoBy (<))+ , fails 10080 $ compatible (|>) -- fails for funny exprs+ , fails n $ simplificationOrder ( >|) -- TODO: make this pass (holds) , fails n $ closedUnderSub ( >|) -- reason for the above, I believe this is an actual bug in >| -- > > checkFor 5040 $ closedUnderSub ( >|)@@ -50,26 +53,6 @@ -- The above bug did exist before the introduction of Express and probably -- since the creation of (>|). --- TODO: fix the following two tests--- > > checkFor 10080 $ simplificationOrder (dwoBy (<))--- > *** Failed! Falsifiable (after 6901 tests):--- > (f _ :: Int) (id _ :: Int) (_ :: Int)--- > > checkFor 10080 $ simplificationOrder (|> )--- > *** Failed! Falsifiable (after 6901 tests):--- > (f _ :: Int) (id _ :: Int) (_ :: Int)-- -- TODO: fix the following two tests with 10000 tests:- , holds 5040 $ simplificationOrder (|> )- , holds 5040 $ simplificationOrder (dwoBy (<))- , fails 10080 $ compatible (|>)--- TODO: fix the following two tests--- > > checkFor 10080 $ compatible (|>)--- > *** Failed! Falsifiable (after 6901 tests):--- > (f _ :: Int) (id _ :: Int) (_ :: Int)--- Like the one above--- Compatibility fails whenever there are function variables.-- , fails n $ \e1 e2 -> (e1 |>| e2) == (e1 |> e2) , fails n $ \e1 e2 -> (e1 |>| e2) == (e1 >| e2) , fails n $ \e1 e2 -> (e1 |> e2) == (e1 >| e2)@@ -111,6 +94,13 @@ e1 `lgt` e2 = e1 `lexicompare` e2 == GT e1 `cgt` e2 = e1 `compare` e2 == GT +-- weaker than simplificationOrder+seriousSimplificationOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool+seriousSimplificationOrder (>) = seriousp $ simplificationOrder (>)++seriousp :: (Expr -> Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool+seriousp prop = \e1 e2 e3 -> serious e1 && serious e2 && serious e3 ==> prop e1 e2 e3+ simplificationOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool simplificationOrder (>) = \e1 e2 e3 -> reductionOrder (>) e1 e2 e3 && subtermProperty (>) e1@@ -121,7 +111,7 @@ $ subexprs e -- isn't this subexprsV? I don't think so reductionOrder :: (Expr -> Expr -> Bool) -> Expr -> Expr -> Expr -> Bool-reductionOrder (>) = \e1 e2 e3 -> strictPartialOrder (>) e1 e2 e3+reductionOrder (>) = \e1 e2 e3 -> isStrictPartialOrder (>) e1 e2 e3 && compatible (>) e1 e2 e3 && closedUnderSub (>) e1 e2 e3
test/reason.hs view
@@ -93,34 +93,34 @@ --, holds n $ \(SameTypedPairsE eqs) -> theorize'' eqs == theorize eqs , holds n $ okThy . deduce- , holds n $ idempotent deduce+ , holds n $ isIdempotent deduce , holds n $ \thy -> ((>=) `on` length . equations) (deduce thy) thy , holds n $ \thy -> ((==) `on` rules) (deduce thy) thy , holds n $ okThy . simplify- , holds n $ idempotent simplify+ , holds n $ isIdempotent simplify , holds n $ \thy -> ((<=) `on` length . equations) (simplify thy) thy , holds n $ \thy -> ((==) `on` rules) (simplify thy) thy , holds n $ okThy . delete- , holds n $ idempotent delete+ , holds n $ isIdempotent delete , holds n $ \thy -> ((<=) `on` length . equations) (delete thy) thy , holds n $ \thy -> ((==) `on` rules) (delete thy) thy , holds n $ okThy . orient- , holds n $ idempotent orient+ , holds n $ isIdempotent orient , holds n $ \thy -> ((<=) `on` length . equations) (orient thy) thy , holds n $ \thy -> ((>=) `on` length . rules) (orient thy) thy , holds n $ \thy -> length (equations thy) - length (equations $ orient thy) >= length (rules $ orient thy) - length (rules thy) , holds n $ okThy . compose- , holds n $ idempotent compose+ , holds n $ isIdempotent compose , holds n $ \thy -> ((<=) `on` length . rules) (compose thy) thy , holds n $ \thy -> ((==) `on` equations) (compose thy) thy , holds n $ okThy . collapse- , holds n $ idempotent collapse+ , holds n $ isIdempotent collapse , holds n $ \thy -> ((<=) `on` length . rules) (collapse thy) thy , holds n $ \thy -> ((>=) `on` length . equations) (collapse thy) thy @@ -144,7 +144,7 @@ $ thy' { keepE = keepUpToLength (max (size e1) (size e2)) } in equivalent thy e1 e2 - , holds n $ idempotent finalize+ , holds n $ isIdempotent finalize , criticalPairs emptyThy { rules = [ ((xx -+- yy) -+- zz,xx -+- (yy -+- zz)) , (negate' xx -+- xx, zero) ] }@@ -154,22 +154,11 @@ , criticalPairs emptyThy { rules = [ (negate' (negate' xx), id' xx) ] } == [ (negate' (id' xx), id' (negate' xx)) ] - , criticalPairs emptyThy { canReduceTo = dwoBy (\e1 e2 -> e1 `lexicompare` e2 == GT)- , rules = [ (foo (goo (foo xx)), xx)- , (foo (goo xx), goo (foo xx)) ] }- == (let sortuple (x,y) | x < y = (y,x)- | otherwise = (x,y)- in nubSort . map sortuple- $ [ (goo xx, foo (goo (goo (foo xx))))- , (goo (foo xx), foo (goo xx))- , (goo (foo (foo xx)), xx)- , (goo (foo (foo (goo xx))), goo xx) ])- , criticalPairs emptyThy { rules = [ (foo (goo (foo xx)), xx) , (foo (goo xx), goo (foo xx)) ] }- == [ (goo (foo xx), foo (goo xx))+ == [ (goo xx, foo (goo (goo (foo xx))))+ , (goo (foo xx), foo (goo xx)) , (goo (foo (foo xx)), xx)- , (foo (goo (goo (foo xx))), goo xx) , (goo (foo (foo (goo xx))), goo xx) ] , theorize [ (xx -*- yy) -*- (yy -*- zz) ~~ yy ]
test/sdist view
@@ -1,33 +1,40 @@ #!/bin/bash #-# test-sdist: tests the package generated by "cabal sdist".+# test/sdist: tests the package generated by "cabal sdist". #-# Copyright (c) 2015-2018 Rudy Matela.+# Copyright (c) 2015-2020 Rudy Matela. # Distributed under the 3-Clause BSD licence.++set -xe+ export LC_ALL=C # consistent sort+ 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 &&-tar -tf $pkg.tar.gz | sort --ignore-case > ls-cabal-i &&-tar -tf $pkg.tar.gz | sort --ignore-case --unique > ls-cabal-iu &&-diff -rud ls-cabal-i ls-cabal-iu &&-rm -f ls-cabal ls-cabal-ignore-case &&-if [ -d ../.git ]+pkgbase=$pkgname-$pkgver++cabal sdist++# Try to find the package generated by cabal.+pkg=`find dist* -name $pkgbase.tar.gz`+[ -f "$pkg" ]+# If the script fails here, either:+# * no package was generated+# * there are packages in both dist and dist-newstyle folders.++tmp=`mktemp -d /tmp/test-sdist-XXXXXXXXXX`++# Test if our file is compatible with case-insensitive filesystems.+tar -tf $pkg | sort --ignore-case > $tmp/ls-cabal-i+tar -tf $pkg | sort --ignore-case --unique > $tmp/ls-cabal-iu+diff -rud $tmp/ls-cabal-i $tmp/ls-cabal-iu++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+ # Test if files included by cabal are the same as files tracked in git.+ git ls-files | sort > $tmp/ls-git+ tar -tf $pkg | grep -v "/$" | sed -e "s,$pkgbase/,," | sort > $tmp/ls-cabal+ diff -rud $tmp/ls-git $tmp/ls-cabal fi++rm -r $tmp
test/utils.hs view
@@ -8,7 +8,7 @@ import Data.List import Data.Function -import Test.LeanCheck.Utils (comparison)+import Test.LeanCheck.Utils main :: IO () main = mainTest tests 10000@@ -78,7 +78,7 @@ , compareIndex [3,2,1::Int] 1 3 == GT , compareIndex [3,2,1::Int] 4 1 == GT , compareIndex [3,2,1::Int] 1 0 == LT- , holds n $ \xs -> comparison (compareIndex (xs::[Int]))+ , holds n $ \xs -> isComparison (compareIndex (xs::[Int])) , partitionByMarkers '#' '*' "" == ("","") , partitionByMarkers '#' '*' "abc*def" == ("abc","def")