code-conjure 0.2.2 → 0.2.4
raw patch · 33 files changed
+783/−243 lines, 33 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Conjure.Conjurable: canonicalApplication :: Conjurable f => String -> f -> Expr
- Conjure.Conjurable: canonicalVarApplication :: Conjurable f => String -> f -> Expr
- Conjure.Conjurable: instance (Test.LeanCheck.Core.Listable a, GHC.Show.Show a, Conjure.Conjurable.Conjurable a, Conjure.Conjurable.Conjurable b) => Conjure.Conjurable.Conjurable (a -> b)
+ Conjure: (-=) :: a -> b -> (a, b)
+ Conjure: [forceTests] :: Args -> [[Expr]]
+ Conjure: conjure1 :: (Eq a, Show a, Conjurable a, Conjurable b) => String -> Spec1 a b -> [Expr] -> IO ()
+ Conjure: conjure1With :: (Eq a, Show a, Conjurable a, Conjurable b) => Args -> String -> Spec1 a b -> [Expr] -> IO ()
+ Conjure: conjure2 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c) => String -> Spec2 a b c -> [Expr] -> IO ()
+ Conjure: conjure2With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c) => Args -> String -> Spec2 a b c -> [Expr] -> IO ()
+ Conjure: conjure3 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d) => String -> Spec3 a b c d -> [Expr] -> IO ()
+ Conjure: conjure3With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d) => Args -> String -> Spec3 a b c d -> [Expr] -> IO ()
+ Conjure: type Spec1 a b = [(a, b)]
+ Conjure: type Spec2 a b c = [((a, b), c)]
+ Conjure: type Spec3 a b c d = [((a, b, c), d)]
+ Conjure.Conjurable: conjureApplication :: Conjurable f => String -> f -> Expr
+ Conjure.Conjurable: conjureAreEqual :: Conjurable f => f -> Int -> Expr -> Expr -> Bool
+ Conjure.Conjurable: conjureVarApplication :: Conjurable f => String -> f -> Expr
+ Conjure.Conjurable: instance (Conjure.Conjurable.Conjurable a, Conjure.Conjurable.Conjurable b) => Conjure.Conjurable.Conjurable (a -> b)
+ Conjure.Engine: [forceTests] :: Args -> [[Expr]]
+ Conjure.Spec: (-=) :: a -> b -> (a, b)
+ Conjure.Spec: conjure1 :: (Eq a, Show a, Conjurable a, Conjurable b) => String -> Spec1 a b -> [Expr] -> IO ()
+ Conjure.Spec: conjure1With :: (Eq a, Show a, Conjurable a, Conjurable b) => Args -> String -> Spec1 a b -> [Expr] -> IO ()
+ Conjure.Spec: conjure2 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c) => String -> Spec2 a b c -> [Expr] -> IO ()
+ Conjure.Spec: conjure2With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c) => Args -> String -> Spec2 a b c -> [Expr] -> IO ()
+ Conjure.Spec: conjure3 :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d) => String -> Spec3 a b c d -> [Expr] -> IO ()
+ Conjure.Spec: conjure3With :: (Conjurable a, Eq a, Show a, Conjurable b, Eq b, Show b, Conjurable c, Eq c, Show c, Conjurable d) => Args -> String -> Spec3 a b c d -> [Expr] -> IO ()
+ Conjure.Spec: type Spec1 a b = [(a, b)]
+ Conjure.Spec: type Spec2 a b c = [((a, b), c)]
+ Conjure.Spec: type Spec3 a b c d = [((a, b, c), d)]
- Conjure: Args :: Int -> Int -> Int -> Int -> Int -> Int -> Args
+ Conjure: Args :: Int -> Int -> Int -> Int -> Int -> Int -> [[Expr]] -> Args
- Conjure: conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
+ Conjure: conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
- Conjure: conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
+ Conjure: conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
- Conjure.Engine: Args :: Int -> Int -> Int -> Int -> Int -> Int -> Args
+ Conjure.Engine: Args :: Int -> Int -> Int -> Int -> Int -> Int -> [[Expr]] -> Args
- Conjure.Engine: conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
+ Conjure.Engine: conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
- Conjure.Engine: conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])
+ Conjure.Engine: conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])
Files
- .gitignore +2/−0
- Makefile +2/−0
- TODO.md +0/−12
- bench/ill-hit.hs +55/−0
- bench/runtime/zero/bench/ill-hit.runtime +1/−0
- bench/runtime/zero/eg/arith.runtime +1/−1
- bench/runtime/zero/eg/bools.runtime +1/−1
- bench/runtime/zero/eg/factorial.runtime +1/−1
- bench/runtime/zero/eg/ints.runtime +1/−1
- bench/runtime/zero/eg/list.runtime +1/−1
- bench/runtime/zero/eg/spec.runtime +1/−0
- bench/runtime/zero/eg/tapps.runtime +1/−1
- bench/runtime/zero/proto/u-conjure.runtime +1/−1
- changelog.md +34/−0
- code-conjure.cabal +4/−2
- eg/bools.hs +3/−1
- eg/list.hs +26/−3
- eg/spec.hs +50/−0
- mk/depend.mk +41/−0
- src/Conjure.hs +13/−0
- src/Conjure/Conjurable.hs +31/−16
- src/Conjure/Engine.hs +53/−26
- src/Conjure/Spec.hs +190/−0
- test/conjurable.hs +6/−6
- test/model/bench/ill-hit.out +42/−0
- test/model/bench/self.out +12/−12
- test/model/eg/arith.out +16/−16
- test/model/eg/bools.out +28/−28
- test/model/eg/factorial.out +14/−14
- test/model/eg/ints.out +35/−35
- test/model/eg/list.out +70/−47
- test/model/eg/spec.out +29/−0
- test/model/eg/tapps.out +18/−18
.gitignore view
@@ -33,7 +33,9 @@ eg/ints eg/list eg/tapps+eg/spec bench/self+bench/ill-hit proto/u-conjure test/expr test/conjurable
Makefile view
@@ -11,7 +11,9 @@ eg/ints \ eg/bools \ eg/list \+ eg/spec \ eg/tapps \+ bench/ill-hit \ bench/self \ proto/u-conjure
TODO.md view
@@ -3,18 +3,6 @@ A non-exhaustive list of things TO DO for Conjure. -* report number of "hit" assignments, add ill example as a bench--* refactor `candidateExprs` and `conjpureWith`.- Move down conjuring of `(===)` from `conjpureWith` into `candidateExprs`.--* refactor `conjureTiersFor` to use `conjureMaybeTiersFor`--* implement `conjureHasTiers` and use it on `conjureMkEquation`;- this will make it easy to backport unique candidateExprs from the erased- commit back into the tool: just `discardLaterT (===)`.- Will this impact performance a bit? I don't think so.- ### for later
+ bench/ill-hit.hs view
@@ -0,0 +1,55 @@+-- ill-hit.hs: failing to hit a function completely+--+-- Based on an example sent by Colin Runciman+--+-- Even though sum' is defined for 6 values,+-- Conjure only ever hits 4 of them.+import Conjure++sum' :: [Int] -> Int+sum' [] = 0+sum' [1] = 1+sum' [1,2] = 3+sum' [1,2,3] = 6+sum' [3,4,5] = 12+sum' [1,2,3,4] = 10++sumSpec :: [([Int],Int)]+sumSpec = [ [] -= 0+ , [1] -= 1+ , [1,2] -= 3+ , [1,2,3] -= 6+ , [3,4,5] -= 12+ , [1,2,3,4] -= 10+ ]++main :: IO ()+main = do+ -- the following does not hit all 6 defined values, only 4+ conjure "sum" (sum' :: [Int] -> Int) primitives++ -- the following forces 3 argument values, totaling 6+ conjureWith as "sum" (sum' :: [Int] -> Int) primitives++ -- the following conjures from a spec+ conjure1 "sum" sumSpec primitives++as :: Args+as = args+ { forceTests = map (map val)+ [ [[1,2]]+ , [[3,4,5::Int]]+ , [[1,2,3,4]]+ ]+ }++primitives :: [Expr]+primitives =+ [ val (0 :: Int)+ , val (1 :: Int)+ , value "+" ((+) :: Int -> Int -> Int)+ , value "*" ((*) :: Int -> Int -> Int)+ , value "null" (null :: [Int] -> Bool)+ , value "head" (head :: [Int] -> Int)+ , value "tail" (tail :: [Int] -> [Int])+ ]
+ bench/runtime/zero/bench/ill-hit.runtime view
@@ -0,0 +1,1 @@+2.26
bench/runtime/zero/eg/arith.runtime view
@@ -1,1 +1,1 @@-1.16+0.95
bench/runtime/zero/eg/bools.runtime view
@@ -1,1 +1,1 @@-7.68+7.78
bench/runtime/zero/eg/factorial.runtime view
@@ -1,1 +1,1 @@-7.75+6.99
bench/runtime/zero/eg/ints.runtime view
@@ -1,1 +1,1 @@-2.39+1.83
bench/runtime/zero/eg/list.runtime view
@@ -1,1 +1,1 @@-8.56+10.71
+ bench/runtime/zero/eg/spec.runtime view
@@ -0,0 +1,1 @@+1.63
bench/runtime/zero/eg/tapps.runtime view
@@ -1,1 +1,1 @@-1.20+0.96
bench/runtime/zero/proto/u-conjure.runtime view
@@ -1,1 +1,1 @@-0.11+0.10
+ changelog.md view
@@ -0,0 +1,34 @@+Changelog for (Code) Conjure+============================+++v0.2.4+------++* allow conjuring from specifications in addition to partial definitions+ (`conjure1`, `conjure2`, `conjure3` and related functions)+* improve examples+* improve criteria for automatic primitive inclusion:+ - only include `if :: ... -> Bool` if there are `Bool` primitives+ - include `False` and `True` automatically only on Speculate's background+* add code-optional candidate nubbing and debug functions+++v0.2.2+------++* by default, search for 60 argument combinations+ among 100000 enumerated combinations+++v0.2.0+------++* search until 100% match is found and exit+* other misc changes+++v0.1.2+------++For the changelog of earlier versions, check the git commit history.
code-conjure.cabal view
@@ -3,7 +3,7 @@ -- Copyright (C) 2021 Rudy Matela -- Distributed under the 3-Clause BSD licence (see the file LICENSE). name: code-conjure-version: 0.2.2+version: 0.2.4 synopsis: conjure Haskell functions out of partial definitions description: Conjure is a tool that produces Haskell functions out of partial definitions.@@ -23,6 +23,7 @@ extra-doc-files: README.md , TODO.md+ , changelog.md , doc/conjure.svg extra-source-files: .gitignore , .github/workflows/build.yml@@ -64,13 +65,14 @@ source-repository this type: git location: https://github.com/rudymatela/conjure- tag: v0.2.2+ tag: v0.2.4 library exposed-modules: Conjure , Conjure.Conjurable , Conjure.Engine , Conjure.Expr+ , Conjure.Spec , Conjure.Utils other-extensions: TemplateHaskell, CPP build-depends: base >= 4 && < 5
eg/bools.hs view
@@ -25,7 +25,9 @@ primitives :: [Expr] primitives =- [ value "not" not+ [ val False+ , val True+ , value "not" not , value "||" (||) , value "&&" (&&) , value "null" (null :: [Bool] -> Bool)
eg/list.hs view
@@ -27,6 +27,11 @@ | x <= y && y <= z = [x,y,z] | z <= y && y <= x = [z,y,x] +(+++) :: [Int] -> [Int] -> [Int]+[x] +++ [y] = [x,y]+[x,y] +++ [z,w] = [x,y,z,w]+[x,y,z] +++ [w,v,u] = [x,y,z,w,v,u]+ main :: IO () main = do -- length xs = if null xs then 0 else 1 + length (tail xs)@@ -61,7 +66,17 @@ , value "null" (null :: [Int] -> Bool) ] - -- now through folds+ -- xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)+ -- 1 2 3 4 5 6 7 8 9 10 11+ conjure "++" (+++)+ [ val ([] :: [Int])+ , value ":" ((:) :: Int -> [Int] -> [Int])+ , value "head" (head :: [Int] -> Int)+ , value "tail" (tail :: [Int] -> [Int])+ , value "null" (null :: [Int] -> Bool)+ ]++ -- now through fold -- length xs = foldr (const (1 +)) 0 xs conjure "length" length' [ val (0 :: Int)@@ -71,7 +86,7 @@ , value "const" (const :: (Int -> Int) -> Int -> (Int -> Int)) -- cheating? ] - -- now through folds and some cheating+ -- now through fold and some cheating -- reverse xs = foldr (\x xs -> xs ++ [x]) [] xs -- reverse xs = foldr (flip (++) . unit) [] xs conjure "reverse" reverse'@@ -84,10 +99,18 @@ , value "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int]) ] - -- now through folds+ -- now through fold -- sort xs = foldr insert [] xs conjure "sort" sort' [ val ([] :: [Int]) , value "insert" (insert :: Int -> [Int] -> [Int])+ , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])+ ]++ -- now through fold+ -- xs ++ ys = foldr (:) ys xs+ conjure "++" (+++)+ [ val ([] :: [Int])+ , value ":" ((:) :: Int -> [Int] -> [Int]) , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int]) ]
+ eg/spec.hs view
@@ -0,0 +1,50 @@+-- spec.hs: conjuring a function from a specification+--+-- Adapted from Colin Runciman's example "ListFuns"+import Conjure+import Prelude hiding (sum)+++sumSpec :: Spec1 [Int] Int+sumSpec =+ [ [] -= 0+ , [1,2] -= 3+ , [3,4,5] -= 12+ ]++-- hoping for something like+-- sum xs = if null xs then 0 else head xs + sum (tail xs)++sumPrimitives :: [Expr]+sumPrimitives =+ [ value "null" (null :: [Int] -> Bool)+ , val (0::Int)+ , value "+" ((+) :: Int -> Int -> Int)+ , value "head" (head :: [Int] -> Int)+ , value "tail" (tail :: [Int] -> [Int])+ ]+++appSpec :: Spec2 [Int] [Int] [Int]+appSpec =+ [ (,) [] [0,1] -= [0,1]+ , (,) [2,3] [] -= [2,3]+ , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]+ ]++-- hoping for something like+-- app xs ys = if null xs then ys else head xs : app (tail xs) ys++appPrimitives :: [Expr]+appPrimitives =+ [ value "null" (null :: [Int] -> Bool)+ , value ":" ((:) :: Int -> [Int] -> [Int])+ , value "head" (head :: [Int] -> Int)+ , value "tail" (tail :: [Int] -> [Int])+ ]+++main :: IO ()+main = do+ conjure1 "sum" sumSpec sumPrimitives+ conjure2 "++" appSpec appPrimitives
mk/depend.mk view
@@ -1,8 +1,20 @@+bench/ill-hit: \+ bench/ill-hit.hs \+ mk/toplibs+bench/ill-hit.o: \+ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs \+ bench/ill-hit.hs bench/self: \ bench/self.hs \ mk/toplibs bench/self.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -13,6 +25,7 @@ mk/toplibs eg/arith.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -23,6 +36,7 @@ mk/toplibs eg/bools.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -33,6 +47,7 @@ mk/toplibs eg/factorial.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -43,6 +58,7 @@ mk/toplibs eg/ints.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -53,16 +69,29 @@ mk/toplibs eg/list.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \ src/Conjure/Conjurable.hs \ eg/list.hs+eg/spec: \+ eg/spec.hs \+ mk/toplibs+eg/spec.o: \+ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \+ src/Conjure.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs \+ eg/spec.hs eg/tapps: \ eg/tapps.hs \ mk/toplibs eg/tapps.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -70,6 +99,7 @@ eg/tapps.hs mk/All.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -77,6 +107,7 @@ mk/All.hs mk/Toplibs.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -101,16 +132,24 @@ src/Conjure/Expr.hs src/Conjure.o: \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \ src/Conjure/Conjurable.hs+src/Conjure/Spec.o: \+ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \+ src/Conjure/Expr.hs \+ src/Conjure/Engine.hs \+ src/Conjure/Conjurable.hs src/Conjure/Utils.o: \ src/Conjure/Utils.hs test/conjurable.o: \ test/Test.hs \ test/conjurable.hs \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -123,6 +162,7 @@ test/Test.hs \ test/expr.hs \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \@@ -134,6 +174,7 @@ test/Test.o: \ test/Test.hs \ src/Conjure/Utils.hs \+ src/Conjure/Spec.hs \ src/Conjure.hs \ src/Conjure/Expr.hs \ src/Conjure/Engine.hs \
src/Conjure.hs view
@@ -53,6 +53,18 @@ , Args(..) , args +-- * Conjuring from a specification+ , Spec1+ , Spec2+ , Spec3+ , (-=)+ , conjure1+ , conjure2+ , conjure3+ , conjure1With+ , conjure2With+ , conjure3With+ -- * When using custom types , Conjurable (conjureEquality, conjureTiers) , reifyEquality, reifyTiers@@ -64,4 +76,5 @@ where import Conjure.Engine+import Conjure.Spec import Conjure.Conjurable
src/Conjure/Conjurable.hs view
@@ -17,17 +17,19 @@ , conjureType , reifyTiers , reifyEquality- , canonicalApplication- , canonicalVarApplication+ , conjureApplication+ , conjureVarApplication , conjureHoles , conjureIfs , conjureTiersFor+ , conjureAreEqual , conjureMkEquation ) where import Test.LeanCheck import Test.LeanCheck.Utils+import Test.LeanCheck.Error (errorToFalse) import Conjure.Expr hiding (application) import Test.Speculate.Expr import Data.Functor ((<$>))@@ -109,17 +111,20 @@ then ms else conjureSubTypes x $ conjureReification1 x : ms +-- | like 'conjureType' but without type repetitions+nubConjureType :: Conjurable a => a -> Reification+nubConjureType x = nubOn (\(eh,_,_,_) -> eh) . conjureType x+-- The use of nubOn above is O(n^2).+-- So long as there is not a huge number of subtypes of a, so we're fine.+ conjureReification1 :: Conjurable a => a -> Reification1 conjureReification1 x = (hole x, ifFor x, conjureEquality x, conjureTiers x) conjureReification :: Conjurable a => a -> [Reification1]-conjureReification x = nubOn (\(eh,_,_,_) -> eh)- $ conjureType x [conjureReification1 bool]+conjureReification x = nubConjureType x [conjureReification1 bool] where bool :: Bool bool = error "conjureReification: evaluated proxy boolean value (definitely a bug)"--- The use of nubOn above is O(n^2).--- So long as there is not a huge number of subtypes of a, so we're fine. -- | Reifies equality to be used in a conjurable type. --@@ -154,11 +159,21 @@ conjureHoles f = [eh | (eh,_,_,Just _) <- conjureReification f] conjureIfs :: Conjurable f => f -> [Expr]-conjureIfs f = [eef | (_,eef,_,Just _) <- conjureReification f]+conjureIfs f = [eef | (_,eef,_,Just _) <- nubConjureType f []]+-- this does not include if for bools automatically+-- differently from conjureHoles, conjureMkEquation and conjureTiersFor conjureMkEquation :: Conjurable f => f -> Expr -> Expr -> Expr conjureMkEquation f = mkEquation [eq | (_,_,Just eq,_) <- conjureReification f] +conjureAreEqual :: Conjurable f => f -> Int -> Expr -> Expr -> Bool+conjureAreEqual f maxTests = (===)+ where+ (-==-) = conjureMkEquation f+ e1 === e2 = isTrue $ e1 -==- e2+ isTrue = all (errorToFalse . eval False) . gs+ gs = take maxTests . grounds (conjureTiersFor f)+ conjureTiersFor :: Conjurable f => f -> Expr -> [[Expr]] conjureTiersFor f e = tf allTiers where@@ -284,9 +299,9 @@ (Right _) == (Left _) = False (Right x) == (Right y) = x .== y -instance (Listable a, Show a, Conjurable a, Conjurable b) => Conjurable (a -> b) where+instance (Conjurable a, Conjurable b) => Conjurable (a -> b) where conjureArgumentHoles f = hole (argTy f) : conjureArgumentHoles (f undefined)- conjureSubTypes f = conjureType (argTy f) . conjureType (resTy f)+ conjureSubTypes f = conjureType (argTy f) . conjureType (resTy f) argTy :: (a -> b) -> a argTy _ = undefined@@ -294,15 +309,15 @@ resTy :: (a -> b) -> b resTy _ = undefined -canonicalApplication :: Conjurable f => String -> f -> Expr-canonicalApplication = canonicalWhatApplication value+conjureApplication :: Conjurable f => String -> f -> Expr+conjureApplication = conjureWhatApplication value -canonicalVarApplication :: Conjurable f => String -> f -> Expr-canonicalVarApplication = canonicalWhatApplication var+conjureVarApplication :: Conjurable f => String -> f -> Expr+conjureVarApplication = conjureWhatApplication var -canonicalWhatApplication :: Conjurable f => (String -> f -> Expr) -> String -> f -> Expr-canonicalWhatApplication what nm f = mostGeneralCanonicalVariation . foldApp- $ what nf f : zipWith varAsTypeOf nas (conjureArgumentHoles f)+conjureWhatApplication :: Conjurable f => (String -> f -> Expr) -> String -> f -> Expr+conjureWhatApplication what nm f = mostGeneralCanonicalVariation . foldApp+ $ what nf f : zipWith varAsTypeOf nas (conjureArgumentHoles f) where (nf:nas) = words nm ++ repeat ""
src/Conjure/Engine.hs view
@@ -29,6 +29,7 @@ import Data.Express.Fixtures hiding ((-==-)) import qualified Data.Ratio import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)+import Test.LeanCheck.Tiers import Test.Speculate hiding ((===), Args(..), args) import Test.Speculate.Reason import Test.Speculate.Engine@@ -47,6 +48,7 @@ , maxEquationSize :: Int -- ^ maximum size of equation operands , maxRecursionSize :: Int -- ^ maximum size of a recursive expression expansion , maxSearchTests :: Int -- ^ maximum number of tests to search for defined values+ , forceTests :: [[Expr]] -- ^ force tests } -- | Default arguments to conjure.@@ -65,6 +67,7 @@ , maxEquationSize = 5 , maxRecursionSize = 60 , maxSearchTests = 100000+ , forceTests = [] } -- | Like 'conjure' but in the pure world.@@ -72,39 +75,39 @@ -- Returns a triple with: -- -- 1. tiers of implementations--- 2. tiers of candidate bodies--- 3. a list of tests-conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])+-- 2. tiers of candidate bodies (right type)+-- 3. tiers of candidate expressions (any type)+-- 4. a list of tests+conjpure :: Conjurable f => String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr]) conjpure = conjpureWith args -- | Like 'conjpure' but allows setting options through 'Args' and 'args'.-conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [Expr])-conjpureWith Args{..} nm f es = (implementationsT, candidatesT, tests)+conjpureWith :: Conjurable f => Args -> String -> f -> [Expr] -> ([[Expr]], [[Expr]], [[Expr]], [Expr])+conjpureWith Args{..} nm f es = (implementationsT, candidatesT, allCandidatesT, tests) where tests = [ffxx //- bs | bs <- dbss] implementationsT = mapT (vffxx -==-) $ filterT implements candidatesT implements e = apparentlyTerminates rrff e && ffxx ?=? recursexpr maxRecursionSize vffxx e- candidatesT = filterT (\e -> typ e == typ ffxx)- . take maxSize- $ candidateExprs nm f maxEquationSize maxRecursiveCalls (===) es- ffxx = canonicalApplication nm f- vffxx = canonicalVarApplication nm f- (rrff:_) = unfoldApp vffxx+ candidatesT = filterT (\e -> typ e == typ ffxx) allCandidatesT+ allCandidatesT = take maxSize+ $ candidateExprs nm f maxEquationSize maxRecursiveCalls (===) es+ ffxx = conjureApplication nm f+ vffxx = conjureVarApplication nm f+ (rrff:xxs) = unfoldApp vffxx - e1 === e2 = isReallyTrue (e1 -==- e2)+ (===) = conjureAreEqual f maxTests e1 ?=? e2 = isTrueWhenDefined (e1 -==- e2) (-==-) = conjureMkEquation f isTrueWhenDefined e = all (errorToFalse . eval False) $ map (e //-) dbss- isReallyTrue = all (errorToFalse . eval False) . gs - gs :: Expr -> [Expr]- gs = take maxTests . grounds (conjureTiersFor f)- bss, dbss :: [[(Expr,Expr)]] bss = take maxSearchTests $ groundBinds (conjureTiersFor f) ffxx- dbss = take maxTests [bs | bs <- bss, errorToFalse . eval False $ e //- bs]+ fbss = [zip xxs vs | vs <- forceTests, isWellTyped $ foldApp (rrff:vs)]+ dbss = take maxTests+ $ ([bs | bs <- bss, errorToFalse . eval False $ e //- bs] \\ fbss)+ ++ fbss where e = ffxx -==- ffxx @@ -153,6 +156,8 @@ , maxEquationSize = min sz (maxEquationSize args) } ++ -- | Like 'conjure' but allows setting options through 'Args'/'args'. -- -- > conjureWith args{maxSize = 11} "function" function [...]@@ -163,14 +168,16 @@ pr 1 rs where pr n [] = putStrLn $ "cannot conjure"- pr n ((is,es):rs) = do- putStrLn $ "-- looking through " ++ show (length es) ++ " candidates of size " ++ show n+ pr n ((is,cs,es):rs) = do+ putStrLn $ "-- looking through "+ ++ show (length cs) ++ "/" ++ show (length es)+ ++ " candidates of size " ++ show n case is of [] -> pr (n+1) rs (i:_) -> do putStrLn $ showEq i putStrLn ""- rs = zip iss css- (iss, css, ts) = conjpureWith args nm f es+ rs = zip3 iss css ess+ (iss, css, ess, ts) = conjpureWith args nm f es showEq eq = showExpr (lhs eq) ++ " = " ++ showExpr (rhs eq) candidateExprs :: Conjurable f@@ -181,8 +188,7 @@ -> [Expr] -> [[Expr]] candidateExprs nm f sz mc (===) es =- candidateExprsT nm f sz mc (===)- [nub $ [val False, val True] ++ es ++ conjureIfs f]+ candidateExprsT nm f sz mc (===) [nub $ es ++ conjureIfs f] candidateExprsT :: Conjurable f => String -> f@@ -193,9 +199,13 @@ -> [[Expr]] candidateExprsT nm f sz mc (===) ess = expressionsT $ [ef:exs] \/ ess where- (ef:exs) = unfoldApp $ canonicalVarApplication nm f- thy = theoryFromAtoms (===) sz $ [conjureHoles f] \/ ess- expressionsT ds = filterT (\e -> count (== ef) (vars e) <= mc)+ (ef:exs) = unfoldApp $ conjureVarApplication nm f+ falseAndTrue = [val False, val True]+ thy = theoryFromAtoms (===) sz $ [conjureHoles f ++ falseAndTrue] \/ filterT (`notElem` falseAndTrue) ess+ nubET = id -- no nub, good enough results+ -- nubET = discardLaterT (===) -- huge computational cost+ expressionsT ds = nubET+ $ filterT (\e -> count (== ef) (vars e) <= mc) $ filterT (isRootNormalE thy) $ ds \/ (delay $ productMaybeWith ($$) es es) where@@ -211,3 +221,20 @@ (%) :: Int -> Int -> Int x % y = x * 100 `div` y++-- Debug: application that always works+(*$$*) :: Expr -> Expr -> Maybe Expr+e1 *$$* e2 = Just $ e1 :$ e2++-- Debug: application that works for the correct kinds+(>$$<) :: Expr -> Expr -> Maybe Expr+e1 >$$< e2 = if isFunTy t1 && tyArity (argumentTy t1) == tyArity t2+ then Just $ e1 :$ e2+ else Nothing+ where+ t1 = ktyp e1+ t2 = ktyp e2++ktyp :: Expr -> TypeRep+ktyp (e1 :$ e2) = resultTy (ktyp e1)+ktyp e = typ e
+ src/Conjure/Spec.hs view
@@ -0,0 +1,190 @@+-- |+-- Module : Conjure.Spec+-- Copyright : (c) 2021 Rudy Matela+-- License : 3-Clause BSD (see the file LICENSE)+-- Maintainer : Rudy Matela <rudy@matela.com.br>+--+-- An internal module of 'Conjure',+-- a library for Conjuring function implementations+-- from tests or partial definitions.+-- (a.k.a.: functional inductive programming)+module Conjure.Spec+ ( Spec1+ , Spec2+ , Spec3+ , (-=)+ , conjure1+ , conjure2+ , conjure3+ , conjure1With+ , conjure2With+ , conjure3With+ )+where++import Conjure.Engine+import Conjure.Conjurable+import Conjure.Utils+++-- | A partial specification of a function with one argument:+--+-- > sumSpec :: Spec1 [Int] Int+-- > sumSpec =+-- > [ [] -= 0+-- > , [1,2] -= 3+-- > , [3,4,5] -= 12+-- > ]+--+-- To be passed as one of the arguments to 'conjure1'.+type Spec1 a b = [(a,b)]+++-- | A partial specification of a function with two arguments:+--+-- > appSpec :: Spec2 [Int] [Int] [Int]+-- > appSpec =+-- > [ (,) [] [0,1] -= [0,1]+-- > , (,) [2,3] [] -= [2,3]+-- > , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]+-- > ]+--+-- To be passed as one of the arguments to 'conjure2'.+type Spec2 a b c = [((a,b),c)]+++-- | A partial specification of a function with three arguments.+--+-- To be passed as one of the arguments to 'conjure3'+type Spec3 a b c d = [((a,b,c),d)]+++-- | To be used when constructing specifications:+-- 'Spec1',+-- 'Spec2' and+-- 'Spec3'.+(-=) :: a -> b -> (a,b)+(-=) = (,)+++-- | Conjures a one argument function from a specification.+--+-- Given:+--+-- > sumSpec :: Spec1 [Int] Int+-- > sumSpec =+-- > [ [] -= 0+-- > , [1,2] -= 3+-- > , [3,4,5] -= 12+-- > ]+--+-- > sumPrimitives :: [Expr]+-- > sumPrimitives =+-- > [ value "null" (null :: [Int] -> Bool)+-- > , val (0::Int)+-- > , value "+" ((+) :: Int -> Int -> Int)+-- > , value "head" (head :: [Int] -> Int)+-- > , value "tail" (tail :: [Int] -> [Int])+-- > ]+--+-- Then:+--+-- > > conjure1 "sum" sumSpec sumPrimitives+-- > sum :: [Int] -> Int+-- > -- testing 3 combinations of argument values+-- > -- ...+-- > -- looking through 189/465 candidates of size 10+-- > xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)+--+-- (cf. 'Spec1', 'conjure1With')+conjure1 :: (Eq a, Show a, Conjurable a, Conjurable b)+ => String -> Spec1 a b -> [Expr] -> IO ()+conjure1 = conjure1With args+++-- | Conjures a two argument function from a specification.+--+-- Given:+--+-- > appSpec :: Spec2 [Int] [Int] [Int]+-- > appSpec =+-- > [ (,) [] [0,1] -= [0,1]+-- > , (,) [2,3] [] -= [2,3]+-- > , (,) [4,5,6] [7,8,9] -= [4,5,6,7,8,9]+-- > ]+--+-- > appPrimitives :: [Expr]+-- > appPrimitives =+-- > [ value "null" (null :: [Int] -> Bool)+-- > , value ":" ((:) :: Int -> [Int] -> [Int])+-- > , value "head" (head :: [Int] -> Int)+-- > , value "tail" (tail :: [Int] -> [Int])+-- > ]+--+-- Then:+--+-- > > conjure2 "++" appSpec appPrimitives+-- > (++) :: [Int] -> [Int] -> [Int]+-- > -- testing 3 combinations of argument values+-- > -- ...+-- > -- looking through 26166/57090 candidates of size 11+-- > xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)+--+-- (cf. 'Spec2', 'conjure2With')+conjure2 :: ( Conjurable a, Eq a, Show a+ , Conjurable b, Eq b, Show b+ , Conjurable c+ ) => String -> Spec2 a b c -> [Expr] -> IO ()+conjure2 = conjure2With args+++-- | Conjures a three argument function from a specification.+--+-- (cf. 'Spec3', 'conjure3With')+conjure3 :: ( Conjurable a, Eq a, Show a+ , Conjurable b, Eq b, Show b+ , Conjurable c, Eq c, Show c+ , Conjurable d+ ) => String -> Spec3 a b c d -> [Expr] -> IO ()+conjure3 = conjure3With args+++-- | Like 'conjure1' but allows setting options through 'Args'/'args'.+conjure1With :: (Eq a, Show a, Conjurable a, Conjurable b)+ => Args -> String -> Spec1 a b -> [Expr] -> IO ()+conjure1With args nm bs = conjureWith args{forceTests=ts} nm (mkFun1 bs)+ where+ ts = [[val x] | (x,_) <- bs]+++-- | Like 'conjure2' but allows setting options through 'Args'/'args'.+conjure2With :: ( Conjurable a, Eq a, Show a+ , Conjurable b, Eq b, Show b+ , Conjurable c+ ) => Args -> String -> Spec2 a b c -> [Expr] -> IO ()+conjure2With args nm bs = conjureWith args{forceTests=ts} nm (mkFun2 bs)+ where+ ts = [[val x, val y] | ((x,y),_) <- bs]+++-- | Like 'conjure3' but allows setting options through 'Args'/'args'.+conjure3With :: ( Conjurable a, Eq a, Show a+ , Conjurable b, Eq b, Show b+ , Conjurable c, Eq c, Show c+ , Conjurable d+ ) => Args -> String -> Spec3 a b c d -> [Expr] -> IO ()+conjure3With args nm bs = conjureWith args{forceTests=ts} nm (mkFun3 bs)+ where+ ts = [[val x, val y, val z] | ((x,y,z),_) <- bs]+++mkFun1 :: Eq a => [(a,b)] -> a -> b+mkFun1 bs = \x -> fromMaybe undefined $ lookup x bs+++mkFun2 :: (Eq a, Eq b) => [((a,b),c)] -> a -> b -> c+mkFun2 bs = \x y -> fromMaybe undefined $ lookup (x,y) bs+++mkFun3 :: (Eq a, Eq b, Eq c) => [((a,b,c),d)] -> a -> b -> c -> d+mkFun3 bs = \x y z -> fromMaybe undefined $ lookup (x,y,z) bs
test/conjurable.hs view
@@ -21,12 +21,12 @@ tests n = [ True - , canonicalApplication "not" not == not' pp- , canonicalApplication "not q" not == not' qq- , canonicalApplication "negate" (negate :: Int -> Int) == negate' xx- , canonicalApplication "negate i" (negate :: Int -> Int) == negate' ii- , canonicalApplication "+" ((+) :: Int -> Int -> Int) == xx -+- yy- , canonicalApplication "+ i j" ((+) :: Int -> Int -> Int) == ii -+- jj+ , conjureApplication "not" not == not' pp+ , conjureApplication "not q" not == not' qq+ , conjureApplication "negate" (negate :: Int -> Int) == negate' xx+ , conjureApplication "negate i" (negate :: Int -> Int) == negate' ii+ , conjureApplication "+" ((+) :: Int -> Int -> Int) == xx -+- yy+ , conjureApplication "+ i j" ((+) :: Int -> Int -> Int) == ii -+- jj , holds n $ \x y -> (x <==> y) == (x == (y :: ())) , holds n $ \x y -> (x <==> y) == (x == (y :: Int))
+ test/model/bench/ill-hit.out view
@@ -0,0 +1,42 @@+sum :: [Int] -> Int+-- testing 4 combinations of argument values+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3+-- looking through 5/18 candidates of size 4+-- looking through 13/33 candidates of size 5+-- looking through 26/68 candidates of size 6+-- looking through 63/143 candidates of size 7+-- looking through 152/336 candidates of size 8+-- looking through 358/783 candidates of size 9+-- looking through 860/1835 candidates of size 10+sum xs = if null xs then 0 else head xs + sum (tail xs)++sum :: [Int] -> Int+-- testing 6 combinations of argument values+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3+-- looking through 5/18 candidates of size 4+-- looking through 13/33 candidates of size 5+-- looking through 26/68 candidates of size 6+-- looking through 63/143 candidates of size 7+-- looking through 152/336 candidates of size 8+-- looking through 358/783 candidates of size 9+-- looking through 860/1835 candidates of size 10+sum xs = if null xs then 0 else head xs + sum (tail xs)++sum :: [Int] -> Int+-- testing 6 combinations of argument values+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3+-- looking through 5/18 candidates of size 4+-- looking through 13/33 candidates of size 5+-- looking through 26/68 candidates of size 6+-- looking through 63/143 candidates of size 7+-- looking through 152/336 candidates of size 8+-- looking through 358/783 candidates of size 9+-- looking through 860/1835 candidates of size 10+sum xs = if null xs then 0 else head xs + sum (tail xs)+
test/model/bench/self.out view
@@ -1,27 +1,27 @@ (?) :: Int -> Int -> Int -- testing 60 combinations of argument values--- looking through 4 candidates of size 1--- looking through 0 candidates of size 2--- looking through 48 candidates of size 3+-- looking through 4/8 candidates of size 1+-- looking through 0/12 candidates of size 2+-- looking through 48/48 candidates of size 3 x ? y = x + y (?) :: Int -> Int -> Int -- testing 60 combinations of argument values--- looking through 4 candidates of size 1--- looking through 0 candidates of size 2--- looking through 48 candidates of size 3+-- looking through 4/8 candidates of size 1+-- looking through 0/12 candidates of size 2+-- looking through 48/48 candidates of size 3 x ? y = x * y i :: Int -> Int -- testing 60 combinations of argument values--- looking through 3 candidates of size 1--- looking through 3 candidates of size 2--- looking through 18 candidates of size 3+-- looking through 3/7 candidates of size 1+-- looking through 3/9 candidates of size 2+-- looking through 18/24 candidates of size 3 i x = x + 1 d :: Int -> Int -- testing 60 combinations of argument values--- looking through 3 candidates of size 1--- looking through 3 candidates of size 2--- looking through 18 candidates of size 3+-- looking through 3/7 candidates of size 1+-- looking through 3/9 candidates of size 2+-- looking through 18/24 candidates of size 3 cannot conjure
test/model/eg/arith.out view
@@ -1,32 +1,32 @@ double :: Int -> Int -- testing 4 combinations of argument values--- looking through 3 candidates of size 1--- looking through 3 candidates of size 2--- looking through 5 candidates of size 3+-- looking through 3/7 candidates of size 1+-- looking through 3/9 candidates of size 2+-- looking through 5/11 candidates of size 3 double x = x + x add :: Int -> Int -> Int -- testing 4 combinations of argument values--- looking through 4 candidates of size 1--- looking through 0 candidates of size 2--- looking through 29 candidates of size 3+-- looking through 4/8 candidates of size 1+-- looking through 0/12 candidates of size 2+-- looking through 29/29 candidates of size 3 add x y = x + y square :: Int -> Int -- testing 3 combinations of argument values--- looking through 3 candidates of size 1--- looking through 3 candidates of size 2--- looking through 5 candidates of size 3+-- looking through 3/7 candidates of size 1+-- looking through 3/9 candidates of size 2+-- looking through 5/11 candidates of size 3 square x = x * x tnpo :: Int -> Int -- testing 3 combinations of argument values--- looking through 3 candidates of size 1--- looking through 3 candidates of size 2--- looking through 5 candidates of size 3--- looking through 20 candidates of size 4--- looking through 13 candidates of size 5--- looking through 97 candidates of size 6--- looking through 42 candidates of size 7+-- looking through 3/7 candidates of size 1+-- looking through 3/9 candidates of size 2+-- looking through 5/11 candidates of size 3+-- looking through 20/30 candidates of size 4+-- looking through 13/53 candidates of size 5+-- looking through 97/123 candidates of size 6+-- looking through 42/236 candidates of size 7 tnpo x = x + (x + (x + 1))
test/model/eg/bools.out view
@@ -1,44 +1,44 @@ and :: [Bool] -> Bool -- testing 14 combinations of argument values--- looking through 2 candidates of size 1--- looking through 3 candidates of size 2--- looking through 6 candidates of size 3--- looking through 6 candidates of size 4--- looking through 16 candidates of size 5--- looking through 41 candidates of size 6--- looking through 103 candidates of size 7--- looking through 278 candidates of size 8--- looking through 752 candidates of size 9+-- looking through 2/12 candidates of size 1+-- looking through 3/12 candidates of size 2+-- looking through 6/25 candidates of size 3+-- looking through 6/48 candidates of size 4+-- looking through 16/84 candidates of size 5+-- looking through 41/185 candidates of size 6+-- looking through 103/447 candidates of size 7+-- looking through 278/1123 candidates of size 8+-- looking through 752/2982 candidates of size 9 and ps = null ps || head ps && and (tail ps) or :: [Bool] -> Bool -- testing 14 combinations of argument values--- looking through 2 candidates of size 1--- looking through 3 candidates of size 2--- looking through 6 candidates of size 3--- looking through 6 candidates of size 4--- looking through 16 candidates of size 5--- looking through 41 candidates of size 6--- looking through 103 candidates of size 7--- looking through 278 candidates of size 8--- looking through 752 candidates of size 9--- looking through 1963 candidates of size 10--- looking through 5427 candidates of size 11+-- looking through 2/12 candidates of size 1+-- looking through 3/12 candidates of size 2+-- looking through 6/25 candidates of size 3+-- looking through 6/48 candidates of size 4+-- looking through 16/84 candidates of size 5+-- looking through 41/185 candidates of size 6+-- looking through 103/447 candidates of size 7+-- looking through 278/1123 candidates of size 8+-- looking through 752/2982 candidates of size 9+-- looking through 1963/7993 candidates of size 10+-- looking through 5427/21497 candidates of size 11 or ps = not (null ps || not (head ps || or (tail ps))) and :: [Bool] -> Bool -- testing 14 combinations of argument values--- looking through 2 candidates of size 1--- looking through 3 candidates of size 2--- looking through 6 candidates of size 3--- looking through 8 candidates of size 4+-- looking through 2/13 candidates of size 1+-- looking through 3/14 candidates of size 2+-- looking through 6/31 candidates of size 3+-- looking through 8/63 candidates of size 4 and ps = foldr (&&) True ps or :: [Bool] -> Bool -- testing 14 combinations of argument values--- looking through 2 candidates of size 1--- looking through 3 candidates of size 2--- looking through 6 candidates of size 3--- looking through 8 candidates of size 4+-- looking through 2/13 candidates of size 1+-- looking through 3/14 candidates of size 2+-- looking through 6/31 candidates of size 3+-- looking through 8/63 candidates of size 4 or ps = foldr (||) False ps
test/model/eg/factorial.out view
@@ -1,22 +1,22 @@ factorial :: Int -> Int -- testing 6 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 0 candidates of size 3--- looking through 2 candidates of size 4+-- looking through 2/6 candidates of size 1+-- looking through 2/4 candidates of size 2+-- looking through 0/6 candidates of size 3+-- looking through 2/10 candidates of size 4 factorial n = product (enumFromTo 1 n) factorial :: Int -> Int -- testing 6 combinations of argument values--- looking through 3 candidates of size 1--- looking through 5 candidates of size 2--- looking through 8 candidates of size 3--- looking through 26 candidates of size 4--- looking through 59 candidates of size 5--- looking through 167 candidates of size 6--- looking through 581 candidates of size 7--- looking through 1654 candidates of size 8--- looking through 5754 candidates of size 9--- looking through 17797 candidates of size 10+-- looking through 3/9 candidates of size 1+-- looking through 5/14 candidates of size 2+-- looking through 8/26 candidates of size 3+-- looking through 26/66 candidates of size 4+-- looking through 59/180 candidates of size 5+-- looking through 167/505 candidates of size 6+-- looking through 581/1521 candidates of size 7+-- looking through 1654/4809 candidates of size 8+-- looking through 5736/15120 candidates of size 9+-- looking through 17617/48943 candidates of size 10 factorial n = if n == 0 then 1 else n * factorial (dec n)
test/model/eg/ints.out view
@@ -1,59 +1,59 @@ second :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3 second xs = head (tail xs) third :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3--- looking through 5 candidates of size 4+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3+-- looking through 5/18 candidates of size 4 third xs = head (tail (tail xs)) sum :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3--- looking through 5 candidates of size 4--- looking through 13 candidates of size 5--- looking through 26 candidates of size 6--- looking through 63 candidates of size 7--- looking through 154 candidates of size 8--- looking through 368 candidates of size 9--- looking through 902 candidates of size 10+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3+-- looking through 5/18 candidates of size 4+-- looking through 13/33 candidates of size 5+-- looking through 26/68 candidates of size 6+-- looking through 63/143 candidates of size 7+-- looking through 152/336 candidates of size 8+-- looking through 358/783 candidates of size 9+-- looking through 860/1835 candidates of size 10 sum xs = if null xs then 0 else head xs + sum (tail xs) product :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3--- looking through 5 candidates of size 4--- looking through 13 candidates of size 5--- looking through 26 candidates of size 6--- looking through 63 candidates of size 7--- looking through 154 candidates of size 8--- looking through 368 candidates of size 9--- looking through 902 candidates of size 10+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3+-- looking through 5/18 candidates of size 4+-- looking through 13/33 candidates of size 5+-- looking through 26/68 candidates of size 6+-- looking through 63/143 candidates of size 7+-- looking through 152/336 candidates of size 8+-- looking through 358/783 candidates of size 9+-- looking through 860/1835 candidates of size 10 product xs = if null xs then 1 else head xs * product (tail xs) sum :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3--- looking through 8 candidates of size 4+-- looking through 2/12 candidates of size 1+-- looking through 2/10 candidates of size 2+-- looking through 3/15 candidates of size 3+-- looking through 8/26 candidates of size 4 sum xs = foldr (+) 0 xs product :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3--- looking through 8 candidates of size 4+-- looking through 2/12 candidates of size 1+-- looking through 2/10 candidates of size 2+-- looking through 3/15 candidates of size 3+-- looking through 8/26 candidates of size 4 product xs = foldr (*) 1 xs
test/model/eg/list.out view
@@ -1,71 +1,94 @@ length :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 1 candidates of size 2--- looking through 2 candidates of size 3--- looking through 3 candidates of size 4--- looking through 5 candidates of size 5--- looking through 11 candidates of size 6--- looking through 22 candidates of size 7--- looking through 53 candidates of size 8--- looking through 101 candidates of size 9+-- looking through 2/9 candidates of size 1+-- looking through 1/5 candidates of size 2+-- looking through 2/7 candidates of size 3+-- looking through 3/12 candidates of size 4+-- looking through 5/17 candidates of size 5+-- looking through 11/30 candidates of size 6+-- looking through 22/57 candidates of size 7+-- looking through 51/119 candidates of size 8+-- looking through 95/240 candidates of size 9 length xs = if null xs then 0 else 1 + length (tail xs) reverse :: [Int] -> [Int] -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 4 candidates of size 2--- looking through 9 candidates of size 3--- looking through 24 candidates of size 4--- looking through 65 candidates of size 5--- looking through 215 candidates of size 6--- looking through 673 candidates of size 7--- looking through 2178 candidates of size 8--- looking through 7154 candidates of size 9--- looking through 23801 candidates of size 10--- looking through 80160 candidates of size 11+-- looking through 2/10 candidates of size 1+-- looking through 4/9 candidates of size 2+-- looking through 9/23 candidates of size 3+-- looking through 24/56 candidates of size 4+-- looking through 65/153 candidates of size 5+-- looking through 215/466 candidates of size 6+-- looking through 673/1462 candidates of size 7+-- looking through 2176/4680 candidates of size 8+-- looking through 7126/15229 candidates of size 9+-- looking through 23619/50202 candidates of size 10+-- looking through 79162/167174 candidates of size 11 reverse xs = if null xs then xs else reverse (tail xs) ++ unit (head xs) sort :: [Int] -> [Int] -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 4 candidates of size 2--- looking through 6 candidates of size 3--- looking through 12 candidates of size 4--- looking through 31 candidates of size 5--- looking through 98 candidates of size 6--- looking through 287 candidates of size 7--- looking through 792 candidates of size 8--- looking through 2220 candidates of size 9--- looking through 6516 candidates of size 10+-- looking through 2/9 candidates of size 1+-- looking through 4/7 candidates of size 2+-- looking through 6/18 candidates of size 3+-- looking through 12/38 candidates of size 4+-- looking through 31/81 candidates of size 5+-- looking through 98/207 candidates of size 6+-- looking through 287/576 candidates of size 7+-- looking through 790/1661 candidates of size 8+-- looking through 2192/4759 candidates of size 9+-- looking through 6352/13661 candidates of size 10 sort xs = if null xs then xs else insert (head xs) (sort (tail xs)) +(++) :: [Int] -> [Int] -> [Int]+-- testing 60 combinations of argument values+-- looking through 3/10 candidates of size 1+-- looking through 3/11 candidates of size 2+-- looking through 12/28 candidates of size 3+-- looking through 39/81 candidates of size 4+-- looking through 83/212 candidates of size 5+-- looking through 290/623 candidates of size 6+-- looking through 1013/2039 candidates of size 7+-- looking through 3482/6732 candidates of size 8+-- looking through 11207/22507 candidates of size 9+-- looking through 36383/74650 candidates of size 10+-- looking through 124785/250463 candidates of size 11+xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)+ length :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 1 candidates of size 2--- looking through 1 candidates of size 3--- looking through 4 candidates of size 4--- looking through 4 candidates of size 5--- looking through 27 candidates of size 6+-- looking through 2/9 candidates of size 1+-- looking through 1/4 candidates of size 2+-- looking through 1/6 candidates of size 3+-- looking through 4/13 candidates of size 4+-- looking through 2/21 candidates of size 5+-- looking through 10/45 candidates of size 6 length xs = foldr (const (1 +)) 0 xs reverse :: [Int] -> [Int] -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 1 candidates of size 3--- looking through 5 candidates of size 4--- looking through 1 candidates of size 5--- looking through 25 candidates of size 6--- looking through 77 candidates of size 7+-- looking through 2/10 candidates of size 1+-- looking through 2/6 candidates of size 2+-- looking through 1/8 candidates of size 3+-- looking through 5/14 candidates of size 4+-- looking through 1/19 candidates of size 5+-- looking through 17/43 candidates of size 6+-- looking through 37/89 candidates of size 7 reverse xs = foldr (flip (++) . unit) [] xs sort :: [Int] -> [Int] -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 0 candidates of size 3--- looking through 2 candidates of size 4+-- looking through 2/7 candidates of size 1+-- looking through 2/3 candidates of size 2+-- looking through 0/2 candidates of size 3+-- looking through 2/4 candidates of size 4 sort xs = foldr insert [] xs++(++) :: [Int] -> [Int] -> [Int]+-- testing 60 combinations of argument values+-- looking through 3/8 candidates of size 1+-- looking through 0/4 candidates of size 2+-- looking through 9/12 candidates of size 3+-- looking through 4/4 candidates of size 4+xs ++ ys = foldr (:) ys xs
+ test/model/eg/spec.out view
@@ -0,0 +1,29 @@+sum :: [Int] -> Int+-- testing 3 combinations of argument values+-- looking through 1/9 candidates of size 1+-- looking through 2/5 candidates of size 2+-- looking through 2/8 candidates of size 3+-- looking through 2/10 candidates of size 4+-- looking through 5/16 candidates of size 5+-- looking through 10/29 candidates of size 6+-- looking through 23/56 candidates of size 7+-- looking through 46/114 candidates of size 8+-- looking through 92/228 candidates of size 9+-- looking through 189/465 candidates of size 10+sum xs = if null xs then 0 else head xs + sum (tail xs)++(++) :: [Int] -> [Int] -> [Int]+-- testing 3 combinations of argument values+-- looking through 2/9 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 6/18 candidates of size 3+-- looking through 18/42 candidates of size 4+-- looking through 38/102 candidates of size 5+-- looking through 110/262 candidates of size 6+-- looking through 334/746 candidates of size 7+-- looking through 1018/2170 candidates of size 8+-- looking through 2966/6442 candidates of size 9+-- looking through 8662/19142 candidates of size 10+-- looking through 26166/57090 candidates of size 11+xs ++ ys = if null xs then ys else head xs:(tail xs ++ ys)+
test/model/eg/tapps.out view
@@ -1,30 +1,30 @@ third :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3--- looking through 5 candidates of size 4+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3+-- looking through 5/18 candidates of size 4 third xs = head (tail (tail xs)) product :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3--- looking through 5 candidates of size 4--- looking through 13 candidates of size 5--- looking through 26 candidates of size 6--- looking through 63 candidates of size 7--- looking through 154 candidates of size 8--- looking through 368 candidates of size 9--- looking through 902 candidates of size 10+-- looking through 2/11 candidates of size 1+-- looking through 2/8 candidates of size 2+-- looking through 3/11 candidates of size 3+-- looking through 5/18 candidates of size 4+-- looking through 13/33 candidates of size 5+-- looking through 26/68 candidates of size 6+-- looking through 63/143 candidates of size 7+-- looking through 152/336 candidates of size 8+-- looking through 358/783 candidates of size 9+-- looking through 860/1835 candidates of size 10 product xs = if null xs then 1 else head xs * product (tail xs) product :: [Int] -> Int -- testing 60 combinations of argument values--- looking through 2 candidates of size 1--- looking through 2 candidates of size 2--- looking through 3 candidates of size 3--- looking through 8 candidates of size 4+-- looking through 2/12 candidates of size 1+-- looking through 2/10 candidates of size 2+-- looking through 3/15 candidates of size 3+-- looking through 8/26 candidates of size 4 product xs = foldr (*) 1 xs