packages feed

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 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