code-conjure 0.2.4 → 0.2.6

raw patch · 26 files changed

+909/−202 lines, 26 filesdep ~expressdep ~leancheckdep ~speculatePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: express, leancheck, speculate

API changes (from Hackage documentation)

Files

• .gitignore +1/−0
• Makefile +2/−1
• TODO.md +25/−7
• bench/runtime/zero/bench/ill-hit.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/−1
• bench/runtime/zero/eg/tapps.runtime +1/−1
• bench/runtime/zero/proto/u-conjure.runtime +1/−1
• bench/runtime/zero/versions +1/−1
• changelog.md +8/−0
• code-conjure.cabal +13/−5
• mk/depend.mk +35/−0
• proto/u-conjure.hs +85/−58
• src/Conjure/Engine.hs +116/−113
• src/Conjure/Expr.hs +87/−0
• src/Conjure/Spec.hs +6/−6
• src/Conjure/Utils.hs +16/−0
• test/Test.hs +6/−0
• test/Test/Candidates.hs +60/−0
• test/Test/ListableExpr.hs +285/−0
• test/expr.hs +125/−0
• test/model/proto/u-conjure.out +9/−3
• test/utils.hs +21/−0

@@ -39,3 +39,4 @@ proto/u-conjure test/expr test/conjurable+test/utils

@@ -19,7 +19,8 @@  TESTS = \   test/expr \-  test/conjurable+  test/conjurable \+  test/utils  all: mk/toplibs 

@@ -4,18 +4,36 @@ A non-exhaustive list of things TO DO for Conjure.  +* top-down generation of candidate expressions++* generate functions with top-level case patterns:++        len []  =  0+        len (x:xs)  =  1 + len xs++* only allow recursion on deconstructed arguments:++        foo (x:xs)  =  ... len xs ...++  this will require generation of functions with top-level case patterns.++ ### for later -* allow conjuring from tests instead of partial definitions?+* exclude magic numbers?  e.g.: `1+1`?  * allow conjuring from partially defined implementations? -    partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int)-    partial impl  =  f-      where-      f n  =  if n == 0-              then 1-              else impl f n+        partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int)+        partial impl  =  f+          where+          f n  =  if n == 0+                  then 1+                  else impl f n++* consider leveraging lazyness somehow?++* consider leveraging polymorphism somehow?   This file is part of Conjure,

@@ -1,1 +1,1 @@-2.26+1.89

@@ -1,1 +1,1 @@-7.78+7.20

@@ -1,1 +1,1 @@-6.99+7.18

@@ -1,1 +1,1 @@-1.83+1.84

@@ -1,1 +1,1 @@-10.71+10.23

@@ -1,1 +1,1 @@-1.63+1.47

@@ -1,1 +1,1 @@-0.96+0.87

@@ -1,1 +1,1 @@-0.10+0.32

@@ -1,4 +1,4 @@ GHC 8.10.4 leancheck-0.9.4-express-0.1.8+express-0.1.10 speculate-0.4.6

@@ -2,6 +2,14 @@ ============================  +v0.2.6+------++* require Express v0.1.10 due to `hasHole` being now exported there+* require Eq result on `conjure1`, `conjure2` and `conjure3`+* code cleanup and more tests++ v0.2.4 ------ 

@@ -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.4+version:             0.2.6 synopsis:            conjure Haskell functions out of partial definitions description:   Conjure is a tool that produces Haskell functions out of partial definitions.@@ -65,7 +65,7 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/conjure-  tag:             v0.2.4+  tag:             v0.2.6  library   exposed-modules: Conjure@@ -79,14 +79,14 @@                , leancheck >= 0.9.4                , template-haskell                , speculate >= 0.4.6-               , express >= 0.1.8+               , express >= 0.1.10   hs-source-dirs:      src   default-language:    Haskell2010  test-suite expr   type:                exitcode-stdio-1.0   main-is:             expr.hs-  other-modules:       Test+  other-modules:       Test, Test.ListableExpr, Test.Candidates   hs-source-dirs:      test   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure   default-language:    Haskell2010@@ -94,7 +94,15 @@ test-suite conjurable   type:                exitcode-stdio-1.0   main-is:             conjurable.hs-  other-modules:       Test+  other-modules:       Test, Test.ListableExpr, Test.Candidates+  hs-source-dirs:      test+  build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure+  default-language:    Haskell2010++test-suite utils+  type:                exitcode-stdio-1.0+  main-is:             utils.hs+  other-modules:       Test, Test.ListableExpr, Test.Candidates   hs-source-dirs:      test   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure   default-language:    Haskell2010

@@ -147,6 +147,8 @@   src/Conjure/Utils.hs test/conjurable.o: \   test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \   test/conjurable.hs \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \@@ -156,10 +158,14 @@   src/Conjure/Conjurable.hs test/conjurable: \   test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \   test/conjurable.hs \   mk/toplibs test/expr.o: \   test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \   test/expr.hs \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \@@ -169,10 +175,20 @@   src/Conjure/Conjurable.hs test/expr: \   test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \   test/expr.hs \   mk/toplibs+test/Test/Candidates.o: \+  test/Test/Candidates.hs \+  src/Conjure/Utils.hs \+  src/Conjure/Expr.hs+test/Test/ListableExpr.o: \+  test/Test/ListableExpr.hs test/Test.o: \   test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \   src/Conjure.hs \@@ -181,4 +197,23 @@   src/Conjure/Conjurable.hs test/Test: \   test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \+  mk/toplibs+test/utils.o: \+  test/utils.hs \+  test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \+  src/Conjure/Utils.hs \+  src/Conjure/Spec.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Conjurable.hs+test/utils: \+  test/utils.hs \+  test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \   mk/toplibs

@@ -20,8 +20,10 @@ import Data.List import Data.Maybe import Data.Express+import Data.Typeable import Test.LeanCheck.Error + square :: Int -> Int square 0  =  0 square 1  =  1@@ -35,37 +37,64 @@ add 1 0  =  1 add 1 1  =  2 -fact :: Int -> Int-fact 0  =  1-fact 1  =  1-fact 2  =  2-fact 3  =  6-fact 4  =  24+factorial :: Int -> Int+factorial 0  =  1+factorial 1  =  1+factorial 2  =  2+factorial 3  =  6+factorial 4  =  24  second :: [Int] -> Int second [x,y]  =  y second [x,y,z]  =  y second [x,y,z,w]  =  y +-- reverse+reverse' :: [Int] -> [Int]+reverse' [x,y]  =  [y,x]+reverse' [x,y,z]  =  [z,y,x]++-- +++(+++) :: [Int] -> [Int] -> [Int]+[x] +++ [y]  =  [x,y]+[x,y] +++ [z,w]  =  [x,y,z,w]++ main :: IO () main  =  do-  value "square" (square :: Int -> Int) `conjureFrom` intBackground-  value "add" (add :: Int -> Int -> Int) `conjureFrom` intBackground-  value "fact" (fact :: Int -> Int) `conjureFrom` intBackground+  conjure "square"    square    primitives+  conjure "add"       add       primitives+  conjure "factorial" factorial primitives -  value "==>" (==>) `conjureFrom`-    [ val False-    , val True-    , value "not" not-    , value "&&" (&&)-    , value "||" (||)+  conjure "factorial"   factorial+    [ val (0 :: Int)+    , val (1 :: Int)+    , value "+" ((+) :: Int -> Int -> Int)+    , value "*" ((*) :: Int -> Int -> Int)+    , value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)+    , value "enumFromTo" (enumFromTo :: Int -> Int -> [Int])     ] -  value "second" (second :: [Int] -> Int) `conjureFrom` listBackground-  value "reverse" (reverse :: [Int] -> [Int]) `conjureFrom` listBackground+  conjure "second"  second   listPrimitives+  conjure "++"      (+++)    listPrimitives+  conjure "reverse" reverse' listPrimitives++  -- even by using fold and some cheating,+  -- this function is out of reach+  --  reverse xs  =  foldr (\x xs -> xs ++ [x]) [] xs+  --  reverse xs  =  foldr (flip (++) . unit) [] xs+  conjure "reverse" reverse' $ listPrimitives +++    [ value "unit" ((:[]) :: Int -> [Int])+    , value "++" ((++) :: [Int] -> [Int] -> [Int])+    -- these last two are cheats:+    , value "flip" (flip :: ([Int]->[Int]->[Int]) -> [Int] -> [Int] -> [Int])+    , value "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int])+    ]+   where-  intBackground :: [Expr]-  intBackground  =++  primitives :: [Expr]+  primitives =     [ val (0 :: Int)     , val (1 :: Int)     , val (2 :: Int)@@ -74,67 +103,65 @@     , value "*" ((*) :: Int -> Int -> Int)     , value "-" ((-) :: Int -> Int -> Int)     ]-  listBackground :: [Expr]-  listBackground  =++  listPrimitives :: [Expr]+  listPrimitives =     [ val (0 :: Int)     , val (1 :: Int)     , val ([] :: [Int])     , value "head" (head :: [Int] -> Int)     , value "tail" (tail :: [Int] -> [Int])     , value ":" ((:) :: Int -> [Int] -> [Int])-    , value "++" ((++) :: [Int] -> [Int] -> [Int])+    , value "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])     ]  -conjureFrom :: Expr -> [Expr] -> IO ()-ff `conjureFrom` es  =  do-  print ff  -- prints the type signature-  case rs of+conjure :: Typeable f => String -> f -> [Expr] -> IO ()+conjure nm f primitives  =  do+  print (value nm f) -- prints the type signature+  case conjureImplementations nm f primitives of     []    -> putStrLn $ "cannot conjure" --  es    -> putStrLn $ unlines $ map showEq es  -- uncomment to show all found variations     (e:_) -> putStrLn $ showEq e   putStrLn ""   where-  nm (Value s _)  =  s-  rrff  =  ('_':nm ff) `varAsTypeOf` ff-  rs  =  [ ffxx -==- e-         | e <- candidateExprsFrom $ [rrff] ++ xxs ++ filter isGround es-         , isWellTyped (ffxx -==- e)-         , isTrue (ffxx -==- e)-         , isDefined e-         ]-  ffxx  =  mostGeneralCanonicalVariation-        .  fromJust-        $  application ff es-  (_:xxs)  =  unfoldApp ffxx   showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)  -application :: Expr -> [Expr] -> Maybe Expr-application ff es  =  appn ff+conjureImplementations :: Typeable f => String -> f -> [Expr] -> [Expr]+conjureImplementations nm f primitives  =+  [ appn -==- e+  | e <- candidateExprsFrom $ exs ++ primitives+  , isTrue (appn -==- e)+  ]   where-  appn ff-    | isFun ff   =  case [e | Just (_ :$ e) <- (map (ff $$)) es] of-                    [] -> Nothing  -- could not find type representative in es-                    (e:_) -> appn (ff :$ holeAsTypeOf e)-    | otherwise  =  Just ff+  appn  =  application nm f primitives+  (ef:exs)  =  unfoldApp appn+  isTrue e  =  all (errorToFalse . eval False) . map (e //-) $ definedBinds appn  -candidateExprsFrom :: [Expr] -> [Expr]-candidateExprsFrom  =  concat . take 6 . expressionsT+definedBinds :: Expr -> [[(Expr,Expr)]]+definedBinds ffxx  =  [bs | bs <- bss, errorToFalse . eval False $ e //- bs]   where-  expressionsT ds  =  [ds] \/ (delay $ productMaybeWith ($$) es es)-    where-    es = expressionsT ds+  e  =  ffxx -==- ffxx+  bss  =  take 360 $ groundBinds ffxx  -isTrue :: Expr -> Bool-isTrue  =  all (errorToTrue . eval False) . take 60 . grounds+application :: Typeable f => String -> f -> [Expr] -> Expr+application nm f es  =  mostGeneralCanonicalVariation $ appn (value nm f)+  where+  appn ff | isFun ff   =  case [e | Just (_ :$ e) <- (map (ff $$)) es] of+                          [] -> error "application: could not find type representative"+                          (e:_) -> appn (ff :$ holeAsTypeOf e)+          | otherwise  =  ff  --- checks if a function is defined for at least one combination of argument values-isDefined :: Expr -> Bool-isDefined e  =  any (isJust . errorToNothing . eval False) . take 60 . grounds $ (e -==- e)+candidateExprsFrom :: [Expr] -> [Expr]+candidateExprsFrom  =  concat . take 7 . expressionsT+  where+  expressionsT ds  =  [ds] \/ (delay $ productMaybeWith ($$) es es)+    where+    es = expressionsT ds   (-==-) :: Expr -> Expr -> Expr@@ -148,14 +175,14 @@   headOr x []     =  x   headOr _ (x:_)  =  x + lhs, rhs :: Expr -> Expr lhs (((Value "==" _) :$ e) :$ _)  =  e rhs (((Value "==" _) :$ _) :$ e)  =  e  -grounds :: Expr -> [Expr]-grounds e  =  map (e //-)  .  concat-           $  products [mapT ((,) v) (tiersFor v) | v <- nubVars e]+groundBinds :: Expr -> [[(Expr,Expr)]]+groundBinds e  =  concat $ products [mapT ((,) v) (tiersFor v) | v <- nubVars e]   tiersFor :: Expr -> [[Expr]]

@@ -10,35 +10,82 @@ -- (a.k.a.: functional inductive programming) {-# LANGUAGE CPP, RecordWildCards, TupleSections #-} module Conjure.Engine-  ( module Data.Express-  , module Data.Express.Fixtures-  , module Test.Speculate.Engine-  , module Test.Speculate.Reason+  ( conjure+  , conjureWithMaxSize   , Args(..)   , args-  , conjure   , conjureWith-  , conjureWithMaxSize   , conjpure   , conjpureWith   , candidateExprs+  , module Data.Express+  , module Data.Express.Fixtures+  , module Test.Speculate.Engine+  , module Test.Speculate.Reason   ) where  import Data.Express import Data.Express.Fixtures hiding ((-==-))-import qualified Data.Ratio-import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing)++import Test.LeanCheck import Test.LeanCheck.Tiers-import Test.Speculate hiding ((===), Args(..), args)-import Test.Speculate.Reason-import Test.Speculate.Engine-import Test.Speculate.Expr-import System.IO+import Test.LeanCheck.Error (errorToTrue, errorToFalse, errorToNothing) +import Test.Speculate.Reason (isRootNormalE)+import Test.Speculate.Engine (theoryFromAtoms, groundBinds)+ import Conjure.Expr import Conjure.Conjurable ++-- | Conjures an implementation of a partially defined function.+--+-- Takes a 'String' with the name of a function,+-- a partially-defined function from a conjurable type,+-- and a list of building blocks encoded as 'Expr's.+--+-- For example, given:+--+-- > square :: Int -> Int+-- > square 0  =  0+-- > square 1  =  1+-- > square 2  =  4+-- >+-- > primitives :: [Expr]+-- > primitives =+-- >   [ val (0::Int)+-- >   , val (1::Int)+-- >   , value "+" ((+) :: Int -> Int -> Int)+-- >   , value "*" ((*) :: Int -> Int -> Int)+-- > ]+--+-- The conjure function does the following:+--+-- > > conjure "square" square primitives+-- > 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+-- > square x  =  x * x+--+-- The primitives list is defined with 'val' and 'value'.+conjure :: Conjurable f => String -> f -> [Expr] -> IO ()+conjure  =  conjureWith args+++-- | Like 'conjure' but allows setting the maximum size of considered expressions+--   instead of the default value of 12.+--+-- > conjureWithMaxSize 10 "function" function [...]+conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()+conjureWithMaxSize sz  =  conjureWith args+                       {  maxSize = sz+                       ,  maxEquationSize = min sz (maxEquationSize args)+                       }++ -- | Arguments to be passed to 'conjureWith' or 'conjpureWith'. --   See 'args' for the defaults. data Args = Args@@ -51,6 +98,7 @@   , forceTests :: [[Expr]]  -- ^ force tests   } + -- | Default arguments to conjure. -- -- * 60 tests@@ -70,6 +118,29 @@   , forceTests         =  []   } ++-- | Like 'conjure' but allows setting options through 'Args'/'args'.+--+-- > conjureWith args{maxSize = 11} "function" function [...]+conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()+conjureWith args nm f es  =  do+  print (var (head $ words nm) f)+  putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"+  pr 1 rs+  where+  pr n []  =  putStrLn $ "cannot conjure"+  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  =  zip3 iss css ess+  (iss, css, ess, ts)  =  conjpureWith args nm f es++ -- | Like 'conjure' but in the pure world. -- -- Returns a triple with:@@ -81,6 +152,7 @@ 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]], [Expr]) conjpureWith Args{..} nm f es  =  (implementationsT, candidatesT, allCandidatesT, tests)@@ -111,75 +183,7 @@     where     e  =  ffxx -==- ffxx --- | Conjures an implementation of a partially defined function.------ Takes a 'String' with the name of a function,--- a partially-defined function from a conjurable type,--- and a list of building blocks encoded as 'Expr's.------ For example, given:------ > square :: Int -> Int--- > square 0  =  0--- > square 1  =  1--- > square 2  =  4--- >--- > primitives :: [Expr]--- > primitives =--- >   [ val (0::Int)--- >   , val (1::Int)--- >   , value "+" ((+) :: Int -> Int -> Int)--- >   , value "*" ((*) :: Int -> Int -> Int)--- > ]------ The conjure function does the following:------ > > conjure "square" square primitives--- > 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--- > square x  =  x * x------ The primitives list is defined with 'val' and 'value'.-conjure :: Conjurable f => String -> f -> [Expr] -> IO ()-conjure  =  conjureWith args --- | Like 'conjure' but allows setting the maximum size of considered expressions---   instead of the default value of 9.------ > conjureWithMaxSize 10 "function" function [...]-conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()-conjureWithMaxSize sz  =  conjureWith args-                       {  maxSize = sz-                       ,  maxEquationSize = min sz (maxEquationSize args)-                       }------ | Like 'conjure' but allows setting options through 'Args'/'args'.------ > conjureWith args{maxSize = 11} "function" function [...]-conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()-conjureWith args nm f es  =  do-  print (var (head $ words nm) f)-  putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"-  pr 1 rs-  where-  pr n []  =  putStrLn $ "cannot conjure"-  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  =  zip3 iss css ess-  (iss, css, ess, ts)  =  conjpureWith args nm f es-  showEq eq  =  showExpr (lhs eq) ++ "  =  " ++ showExpr (rhs eq)- candidateExprs :: Conjurable f                => String -> f                -> Int@@ -190,6 +194,7 @@ candidateExprs nm f sz mc (===) es  =   candidateExprsT nm f sz mc (===) [nub $ es ++ conjureIfs f] + candidateExprsT :: Conjurable f                 => String -> f                 -> Int@@ -197,44 +202,42 @@                 -> (Expr -> Expr -> Bool)                 -> [[Expr]]                 -> [[Expr]]-candidateExprsT nm f sz mc (===) ess  =  expressionsT $ [ef:exs] \/ ess+candidateExprsT nm f sz mc (===) ess  =+  candidateExprsTT keep $ [ef:exs] \/ ess   where   (ef:exs)  =  unfoldApp $ conjureVarApplication nm f+  keep e  =  isRootNormalE thy e && count (== ef) (vars e) <= mc+  thy  =  theoryFromAtoms (===) sz $ [conjureHoles f ++ falseAndTrue]+                                  \/ filterT (`notElem` falseAndTrue) ess   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-    es = expressionsT ds -lhs, rhs :: Expr -> Expr-lhs (((Value "==" _) :$ e) :$ _)  =  e-rhs (((Value "==" _) :$ _) :$ e)  =  e -compareResult :: (Int,Expr) -> (Int,Expr) -> Ordering-compareResult (n1,e1) (n2,e2)  =  n2 `compare` n1-                               <> e1 `compareSimplicity` e2+candidateExprsTT :: (Expr -> Bool) -> [[Expr]] -> [[Expr]]+candidateExprsTT keep  =  exprT+  where+  exprT ess  =  filterT keep+             $  ess \/ (delay $ productMaybeWith ($$) rss rss)+    where+    rss = exprT ess -(%) :: 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+candidatesTD :: (Expr -> Bool) -> Expr -> [Expr] -> [[Expr]]+candidatesTD keep h primitives  =  filterT (not . hasHole)+                                $  town [[h]]   where-  t1  =  ktyp e1-  t2  =  ktyp e2+  most = mostGeneralCanonicalVariation -ktyp :: Expr -> TypeRep-ktyp (e1 :$ e2)  =  resultTy (ktyp e1)-ktyp e  =  typ e+  town :: [[Expr]] -> [[Expr]]+  town ((e:es):ess) | keep (most e)  =  [[e]] \/ town (expand e \/ (es:ess))+                    | otherwise      =  town (es:ess)+  town ([]:ess)  =  []:town ess+  town []  =  []++  expand :: Expr -> [[Expr]]+  expand e  =  case holesBFS e of+    [] -> []+    (h:_) -> mapT (fillBFS e) (replacementsFor h)++  replacementsFor :: Expr -> [[Expr]]+  replacementsFor h  =  filterT (\e -> typ e == typ h)+                     $  primitiveApplications primitives

@@ -11,6 +11,7 @@   ( module Data.Express   , module Data.Express.Fixtures +  , (>$$<)   , funToVar   , recursexpr   , apparentlyTerminates@@ -18,6 +19,16 @@   , applicationOld   , compareSimplicity   , ifFor+  , primitiveHoles+  , primitiveApplications+  , valuesBFS+  , holesBFS+  , fillBFS+  , showEq+  , lhs+  , rhs+  , ($$**)+  , ($$|<)    , module Conjure.Utils   )@@ -26,6 +37,7 @@ import Conjure.Utils  import Data.Express+import Data.Express.Utils.Typeable import Data.Express.Fixtures hiding ((-==-))  -- | /O(n)/.@@ -172,3 +184,78 @@ -- if you want recursive functions to be considered and produced. ifFor :: Typeable a => a -> Expr ifFor a  =  value "if" (\p x y -> if p then x else y `asTypeOf` a)++-- | Application cross-product between lists of Exprs+(>$$<) :: [Expr] -> [Expr] -> [Expr]+exs >$$< eys  =  catMaybes [ex $$ ey | ex <- exs, ey <- eys]+-- TODO: move >$$< into Data.Express?++primitiveHoles :: [Expr] -> [Expr]+primitiveHoles prims  =  sort $ ph hs+  where+  hs  =  nub $ map holeAsTypeOf prims+  ph  =  iterateUntil (==) ps+  ps es  =  nub $ es ++ sq es+  sq es  =  nub $ map holeAsTypeOf $ es >$$< es+-- FIXME: the function above is quite inefficient.+--        Should run fast for a small number of types,+--        but if this number increases runtime may start+--        to become significant.++primitiveApplications :: [Expr] -> [[Expr]]+primitiveApplications prims  =  takeWhile (not . null)+                             $  iterate (>$$< primitiveHoles prims) prims++-- lists terminal values in BFS order+valuesBFS :: Expr -> [Expr]+valuesBFS  =  concat . bfs+  where+  bfs :: Expr -> [[Expr]]+  bfs (ef :$ ex)  =  [] : mzip (bfs ef) (bfs ex)+  bfs e  =  [[e]]++-- lists holes in BFS order+holesBFS :: Expr -> [Expr]+holesBFS  =  filter isHole . valuesBFS++fillBFS :: Expr -> Expr -> Expr+fillBFS e e'  =  fst (f e)+  where+  f :: Expr -> (Expr,Maybe Int)+  f (ef :$ ex)  =  case (mf, mx) of+    (Nothing, Nothing)             -> (ef :$ ex, Nothing)+    (Just lf, Nothing)             -> (ef' :$ ex, Just $ lf+1)+    (Nothing, Just lx)             -> (ef :$ ex', Just $ lx+1)+    (Just lf, Just lx) | lf <= lx  -> (ef' :$ ex, Just $ lf+1)+                       | otherwise -> (ef :$ ex', Just $ lx+1)+    where+    (ef', mf)  =  f ef+    (ex', mx)  =  f ex+  f e | isHole e && typ e == typ e'  =  (e', Just 0)+      | otherwise                    =  (e, Nothing)+-- TODO: move BFS functions into Express?++showEq :: Expr -> String+showEq (((Value "==" _) :$ lhs) :$ rhs)  =  showExpr lhs ++ "  =  " ++ showExpr rhs+showEq e  =  "not an Eq: " ++ show e++lhs, rhs :: Expr -> Expr+lhs (((Value "==" _) :$ e) :$ _)  =  e+rhs (((Value "==" _) :$ _) :$ e)  =  e++-- 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

@@ -97,7 +97,7 @@ -- > 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)+conjure1 :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b)          => String -> Spec1 a b -> [Expr] -> IO () conjure1  =  conjure1With args @@ -133,7 +133,7 @@ -- (cf. 'Spec2', 'conjure2With') conjure2 :: ( Conjurable a, Eq a, Show a             , Conjurable b, Eq b, Show b-            , Conjurable c+            , Conjurable c, Eq c             ) => String -> Spec2 a b c -> [Expr] -> IO () conjure2  =  conjure2With args @@ -144,13 +144,13 @@ conjure3 :: ( Conjurable a, Eq a, Show a             , Conjurable b, Eq b, Show b             , Conjurable c, Eq c, Show c-            , Conjurable d+            , Conjurable d, Eq 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)+conjure1With :: (Eq a, Eq b, 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@@ -160,7 +160,7 @@ -- | Like 'conjure2' but allows setting options through 'Args'/'args'. conjure2With :: ( Conjurable a, Eq a, Show a                 , Conjurable b, Eq b, Show b-                , Conjurable c+                , Conjurable c, Eq c                 ) => Args -> String -> Spec2 a b c -> [Expr] -> IO () conjure2With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun2 bs)   where@@ -171,7 +171,7 @@ conjure3With :: ( Conjurable a, Eq a, Show a                 , Conjurable b, Eq b, Show b                 , Conjurable c, Eq c, Show c-                , Conjurable d+                , Conjurable d, Eq d                 ) => Args -> String -> Spec3 a b c d -> [Expr] -> IO () conjure3With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun3 bs)   where

@@ -18,6 +18,8 @@    , count   , nubOn+  , iterateUntil+  , mzip   ) where @@ -33,3 +35,17 @@  nubOn :: Eq b => (a -> b) -> [a] -> [a] nubOn f  =  nubBy ((==) `on` f)++iterateUntil :: (a -> a -> Bool) -> (a -> a) -> a -> a+iterateUntil (?) f  =  iu+  where+  iu x | x ? fx     =  x+       | otherwise  =  iu fx+    where+    fx  =  f x++mzip :: Monoid a => [a] -> [a] -> [a]+mzip [] []  =  []+mzip [] ys  =  ys+mzip xs []  =  xs+mzip (x:xs) (y:ys)  =  x <> y : mzip xs ys

@@ -11,6 +11,9 @@   , module Conjure.Expr   , module Conjure.Conjurable   , module Test.LeanCheck+  , module Test.LeanCheck.Utils+  , module Test.ListableExpr+  , module Test.Candidates    , mainTest   )@@ -20,6 +23,9 @@ import System.Environment (getArgs)  import Test.LeanCheck+import Test.LeanCheck.Utils+import Test.ListableExpr+import Test.Candidates  import Conjure import Conjure.Expr hiding (delete, insert)

@@ -0,0 +1,60 @@+-- |+-- Module      : TEst.Candidates+-- Copyright   : (c) 2021 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- Reference implementations of candidate generation.+--+-- Bottom-up and top-down+module Test.Candidates+  ( boupCandidates+  , townCandidates+  , dropTrail+  )+where++import Conjure.Expr+import Test.LeanCheck++boupCandidates :: Expr -> [Expr] -> [[Expr]]+boupCandidates appn primitives  =  dropTrail $ filterT (\e -> typ e == typ appn) boup+  where+  boup :: [[Expr]]+  boup = expressionsT [primitives]++  expressionsT ds  =  ds \/ (delay $ productMaybeWith ($$) es es)+    where+    es = expressionsT ds++townCandidates :: Expr -> [Expr] -> [[Expr]]+townCandidates appn primitives  =  normalizeT+                                $  filterT (not . hasHole)+                                $  town [[holeAsTypeOf appn]]+  where+  town :: [[Expr]] -> [[Expr]]+  town ((e:es):ess)  =  [[e]] \/ town (expand e \/ (es:ess))+  town ([]:ess)  =  []:town ess+  town []  =  []++  expand :: Expr -> [[Expr]]+  expand e  =  case holesBFS e of+    [] -> []+    (h:_) -> mapT (fillBFS e) (replacementsFor h)++  replacementsFor :: Expr -> [[Expr]]+  replacementsFor h  =  filterT (\e -> typ e == typ h)+                     $  primitiveApplications primitives++-- like normalizeT, but considers 6 empty tiers as an infinite trail of tiers+-- this should only be used on testing+dropTrail :: [[a]] -> [[a]]+dropTrail []  =  []+dropTrail [[]]  =  []+dropTrail [[],[]]  =  []+dropTrail [[],[],[]]  =  []+dropTrail [[],[],[],[]]  =  []+dropTrail [[],[],[],[],[]]  =  []+dropTrail [[],[],[],[],[],[]]  =  []+dropTrail ([]:[]:[]:[]:[]:[]:_)  =   []+dropTrail (xs:xss)  =  xs:dropTrail xss

@@ -0,0 +1,285 @@+-- |+-- Module      : Test.ListableExpr+-- Copyright   : (c) 2019-2021 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module exports a 'Listable' 'Expr' instance.+-- This instance does not, by any means, list all possible expressions.+-- It lists expressions based on a subset of the symbols exported by+-- "Data.Express.Fixtures".+--+-- This is only intended to be used for testing,+-- so this will not be exported on @ express.cabal @.+module Test.ListableExpr+  (+  -- * The Expr type+    Expr++  -- * Expressions of a type+  , IntE (..)+  , BoolE (..)+  , IntsE (..)+  , CharE (..)++  , IntE0 (..)+  , IntEV (..)+  , BoolE0 (..)+  , BoolEV (..)+  , IntsE0 (..)+  , IntsEV (..)+  , CharE0 (..)+  , CharEV (..)++  -- ** Functional values+  , IntToIntE (..)+  , IntToIntToIntE (..)+  , BoolToBoolE (..)+  , BoolToBoolToBoolE (..)++  , SameTypeE (..)+  , unSameTypeE+  , SameTypedPairsE (..)++  -- * Terminal expressions+  , E0 (..)+  , EV (..)++  -- * Ill typed expressions+  , Ill (..)+  )+where++-- TODO: StringE++import Test.LeanCheck+import Test.LeanCheck.Function.ShowFunction+import Data.Express.Fixtures+import Data.Function (on)++-- | Terminal constants.+newtype E0  =  E0 { unE0 :: Expr }++-- | Variables.+newtype EV  =  EV { unEV :: Expr }++-- | Expression of 'Int' type.+newtype IntE  =  IntE { unIntE :: Expr }++-- | Constant terminal value of 'Int' type.+newtype IntE0  =  IntE0 { unIntE0 :: Expr }++-- | Variable of 'Int' type.+newtype IntEV  =  IntEV { unIntEV :: Expr }++-- | Functions from Int to Int+newtype IntToIntE  =  IntToIntE { unIntToIntE :: Expr }+newtype IntToIntToIntE  =  IntToIntToIntE { unIntToIntToIntE :: Expr }++-- | Expression of 'Bool' type.+newtype BoolE  =  BoolE { unBoolE :: Expr }++-- | Constant terminal value of 'Bool' type.+newtype BoolE0  =  BoolE0 { unBoolE0 :: Expr }++-- | Varialbe of 'Bool' type.+newtype BoolEV  =  BoolEV { unBoolEV :: Expr }++-- | Functions from Bool to Bool+newtype BoolToBoolE  =  BoolToBoolE { unBoolToBoolE :: Expr }+newtype BoolToBoolToBoolE  =  BoolToBoolToBoolE { unBoolToBoolToBoolE :: Expr }++newtype CharE  =  CharE { unCharE :: Expr }++newtype CharE0  =  CharE0 { unCharE0 :: Expr }++newtype CharEV  =  CharEV { unCharEV :: Expr }++data SameTypeE  =  SameTypeE Expr Expr++unSameTypeE :: SameTypeE -> (Expr,Expr)+unSameTypeE (SameTypeE e1 e2)  =  (e1,e2)++data SameTypedPairsE  =  SameTypedPairsE { unSameTypedPairsE :: [(Expr,Expr)] }++-- | Ill typed expressions.+newtype Ill  =  Ill { unIll :: Expr }+++instance Show E0  where  show (E0 e) = show e+instance Show EV  where  show (EV e) = show e++instance Show IntE  where  show (IntE e) = show e++instance Show IntE0  where  show (IntE0 e) = show e+instance Show IntEV  where  show (IntEV e) = show e++instance Show IntToIntE  where  show (IntToIntE e) = show e+instance Show IntToIntToIntE  where  show (IntToIntToIntE e) = show e++instance Show BoolE  where  show (BoolE e) = show e++instance Show BoolE0  where  show (BoolE0 e) = show e+instance Show BoolEV  where  show (BoolEV e) = show e++instance Show BoolToBoolE  where  show (BoolToBoolE e) = show e+instance Show BoolToBoolToBoolE  where  show (BoolToBoolToBoolE e) = show e++instance Show IntsE  where  show (IntsE e) = show e++instance Show IntsE0  where  show (IntsE0 e) = show e+instance Show IntsEV  where  show (IntsEV e) = show e++instance Show CharE  where  show (CharE e) = show e++instance Show CharE0  where  show (CharE0 e) = show e+instance Show CharEV  where  show (CharEV e) = show e++instance Show SameTypeE  where  show (SameTypeE e1 e2) = show (e1,e2)++instance Show SameTypedPairsE  where  show (SameTypedPairsE ees)  =  show ees++-- | Expression of 'Ints' type.+newtype IntsE  =  IntsE { unIntsE :: Expr }++-- | Constant terminal value of 'Ints' type.+newtype IntsE0  =  IntsE0 { unIntsE0 :: Expr }++-- | Varialbe of 'Ints' type.+newtype IntsEV  =  IntsEV { unIntsEV :: Expr }++instance Show Ill where  show (Ill e) = show e++instance Listable IntE  where+  tiers  =  mapT IntE+         $  cons0 i_+         \/ cons1 unIntEV+         \/ cons1 unIntE0+         \/ cons2 (\(IntToIntE f) (IntE xx) -> f :$ xx)+         \/ cons1 (head' . unIntsE) `ofWeight` 2+         \/ cons1 (ord' . unCharE) `ofWeight` 2++instance Listable IntE0 where+  tiers  =  (IntE0 . val) `mapT` (tiers :: [[Int]])++instance Listable IntEV where+  list  =  map IntEV $ listVars "x" (undefined :: Int)++instance Listable IntToIntE where+  tiers  =  mapT IntToIntE+         $  cons0 idE+         \/ cons0 negateE `addWeight` 1+         \/ cons0 absE    `addWeight` 1+         \/ cons2 (\(IntToIntToIntE ef) (IntE ex) -> ef :$ ex)+         \/ toTiers (listVars "f" (undefined :: Int -> Int)) `addWeight` 2++instance Listable IntToIntToIntE where+  list  =  map IntToIntToIntE [plus, times]++instance Listable IntsE  where+  tiers  =  mapT IntsE+         $  cons0 is_+         \/ cons1 unIntsEV+         \/ cons1 unIntsE0+         \/ cons2 (\(IntE ex) (IntsE exs) -> ex -:- exs)+         \/ cons1 (tail' . unIntsE) `ofWeight` 2+         \/ cons2 (\(IntsE exs) (IntsE eys) -> exs -++- eys) `ofWeight` 2+         \/ cons1 (\(IntsE exs) -> sort' exs) `ofWeight` 3+         \/ cons2 (\(IntE ex) (IntsE exs) -> insert' ex exs) `ofWeight` 3++instance Listable IntsE0 where+  tiers  =  (IntsE0 . val) `mapT` (tiers :: [[ [Int] ]])++instance Listable IntsEV where+  list  =  map IntsEV $ listVars "xs" (undefined :: [Int])++instance Listable BoolE  where+  tiers  =  mapT BoolE+         $  cons0 b_+         \/ cons1 unBoolEV+         \/ cons1 unBoolE0+         \/ cons2 (\(BoolToBoolE ef) (BoolE ep) -> ef :$ ep)+         \/ cons2 ((-==-) `on` unIntE)  `addWeight` 2+         \/ cons2 ((-==-) `on` unBoolE) `addWeight` 2+         \/ cons2 ((-<=-) `on` unIntE)  `addWeight` 3+         \/ cons2 ((-<=-) `on` unBoolE) `addWeight` 3+         \/ cons2 ((-<-)  `on` unIntE)  `addWeight` 4+         \/ cons2 ((-<-)  `on` unBoolE) `addWeight` 4+         \/ cons2 ((-/=-) `on` unIntE)  `addWeight` 5+         \/ cons2 ((-/=-) `on` unBoolE) `addWeight` 5+         \/ cons1 (odd'  . unIntE) `addWeight` 2+         \/ cons1 (even' . unIntE) `addWeight` 2+         \/ cons2 (\(IntE ex) (IntsE exs) -> elem' ex exs) `addWeight` 2++instance Listable BoolE0 where+  tiers  =  (BoolE0 . val) `mapT` (tiers :: [[Bool]])++instance Listable BoolEV where+  list  =  map BoolEV $ listVars "p" (undefined :: Bool)++instance Listable BoolToBoolE where+  tiers  =  mapT BoolToBoolE+         $  cons0 notE+         \/ cons2 (\(BoolToBoolToBoolE ef) (BoolE ex) -> ef :$ ex)++instance Listable BoolToBoolToBoolE where+  list  =  map BoolToBoolToBoolE [orE, andE, implies]++instance Listable CharE where+  tiers  =  mapT CharE $ cons0 c_+                      \/ cons1 unCharEV+                      \/ cons1 unCharE0++instance Listable CharEV where+  list  =  map CharEV $ listVars "c" (undefined :: Char)++instance Listable CharE0 where+  tiers  =  (CharE0 . val) `mapT` (tiers :: [[Char]])++instance Listable SameTypeE where+  tiers = cons1 (\(IntE  e1, IntE  e2) -> SameTypeE e1 e2) `ofWeight` 0+       \/ cons1 (\(BoolE e1, BoolE e2) -> SameTypeE e1 e2) `ofWeight` 1+       \/ cons1 (\(IntsE e1, IntsE e2) -> SameTypeE e1 e2) `ofWeight` 1+       \/ cons1 (\(CharE e1, CharE e2) -> SameTypeE e1 e2) `ofWeight` 2+       \/ cons1 (\(IntToIntE e1, IntToIntE e2)     -> SameTypeE e1 e2) `ofWeight` 2+       \/ cons1 (\(BoolToBoolE e1, BoolToBoolE e2) -> SameTypeE e1 e2) `ofWeight` 2+       \/ cons1 (\(BoolToBoolToBoolE e1, BoolToBoolToBoolE e2) -> SameTypeE e1 e2) `ofWeight` 2+       \/ cons1 (\(IntToIntToIntE e1, IntToIntToIntE e2)       -> SameTypeE e1 e2) `ofWeight` 2++instance Listable SameTypedPairsE where+  tiers = cons1 (SameTypedPairsE . map unSameTypeE) `ofWeight` 0++instance Listable E0 where+  tiers  =  mapT E0+         $  cons1 unIntE0  `ofWeight` 0+         \/ cons1 unBoolE0 `ofWeight` 1+         \/ cons1 unIntsE0 `ofWeight` 1++instance Listable EV where+  tiers  =  mapT EV+         $  cons1 unIntEV  `ofWeight` 0+         \/ cons1 unBoolEV `ofWeight` 1+         \/ cons1 unIntsEV `ofWeight` 1+++instance Listable Expr where+  tiers  =  reset (cons1 unIntE)+         \/ cons1 unBoolE+         \/ cons1 unCharE+         \/ cons1 unIntsE+         \/ cons1 unIntToIntE         `addWeight` 1+         \/ cons1 unIntToIntToIntE    `addWeight` 1+         \/ cons1 unBoolToBoolE       `addWeight` 2+         \/ cons1 unBoolToBoolToBoolE `addWeight` 2+++-- | This listable instance only produces Ill typed expressions+instance Listable Ill where+  tiers  =  mapT Ill+         $  cons2 (\(IntE ef) (IntE ex) -> ef :$ ex) `ofWeight` 0+         \/ cons2 (\(IntToIntE ef) (IntToIntE ex) -> ef :$ ex)+         \/ cons2 (\(Ill ef) ex -> ef :$ ex)+         \/ cons2 (\ef (Ill ex)-> ef :$ ex)+++instance ShowFunction Expr where bindtiers  =  bindtiersShow

@@ -34,4 +34,129 @@   , apparentlyTerminates ffE (if' pp zero (ff xx)) == True   , apparentlyTerminates ffE (if' pp (ff xx) zero) == False   , apparentlyTerminates ffE (if' (odd' (ff xx)) zero zero) == False++  , [false, true, zero, one] >$$< [notE, andE, orE, plus, times] == []+  , [notE, andE, orE, plus, times] >$$< [false, true, zero, one]+    == [ not' false+       , not' true+       , andE :$ false+       , andE :$ true+       , orE :$ false+       , orE :$ true+       , plus :$ zero+       , plus :$ one+       , times :$ zero+       , times :$ one+       ]+  , [notE, andE, orE, plus, times] >$$< [false, true, zero, one] >$$< [false, true, zero, one]+    == [ false -&&- false+       , false -&&- true+       , true -&&- false+       , true -&&- true+       , false -||- false+       , false -||- true+       , true -||- false+       , true -||- true+       , zero -+- zero+       , zero -+- one+       , one -+- zero+       , one -+- one+       , zero -*- zero+       , zero -*- one+       , one -*- zero+       , one -*- one+       ]++  , primitiveHoles [false, true]  ==  [b_]+  , primitiveHoles [zero, one]  ==  [i_]+  , primitiveHoles [false, zero]  ==  [b_, i_]++  , primitiveHoles [false, true, notE]  ==+      [ hole (undefined :: Bool)+      , hole (undefined :: Bool -> Bool)+      ]++  , primitiveHoles [false, true, notE, andE, orE]  ==+      [ hole (undefined :: Bool)+      , hole (undefined :: Bool -> Bool)+      , hole (undefined :: Bool -> Bool -> Bool)+      ]++  , primitiveHoles [false, true, andE, orE]  ==+      [ hole (undefined :: Bool)+      , hole (undefined :: Bool -> Bool)+      , hole (undefined :: Bool -> Bool -> Bool)+      ]++  , primitiveHoles [zero, one, plus, times]  ==+      [ hole (undefined :: Int)+      , hole (undefined :: Int -> Int)+      , hole (undefined :: Int -> Int -> Int)+      ]++  , primitiveHoles [false, true, andE, orE, zero, one, plus, times]+    == [ hole (undefined :: Bool)+       , hole (undefined :: Int)+       , hole (undefined :: Bool -> Bool)+       , hole (undefined :: Int -> Int)+       , hole (undefined :: Bool -> Bool -> Bool)+       , hole (undefined :: Int -> Int -> Int)+       ]++  , holds n $ \es -> all (`elem` primitiveHoles es) (map holeAsTypeOf es)+  , fails n $ \es -> primitiveHoles es == map holeAsTypeOf es++  , map (map show) (primitiveApplications [false, true, andE, orE, zero, one, plus, times])+    == [ [ "False :: Bool"+         , "True :: Bool"+         , "(&&) :: Bool -> Bool -> Bool"+         , "(||) :: Bool -> Bool -> Bool"+         , "0 :: Int"+         , "1 :: Int"+         , "(+) :: Int -> Int -> Int"+         , "(*) :: Int -> Int -> Int"+         ]+       , [ "(_ &&) :: Bool -> Bool"+         , "(_ ||) :: Bool -> Bool"+         , "(_ +) :: Int -> Int"+         , "(_ *) :: Int -> Int"+         ]+       , [ "_ && _ :: Bool"+         , "_ || _ :: Bool"+         , "_ + _ :: Int"+         , "_ * _ :: Int"+         ]+       ]++  , holds n $ \e -> sort (valuesBFS e) == sort (values e)+  , holds n $ \e -> holesBFS e == filter isHole (valuesBFS e)+  , valuesBFS false == [false]+  , valuesBFS true  == [true]+  , valuesBFS zero  == [zero]+  , valuesBFS one   == [one]+  , valuesBFS (not' false) == [notE, false]+  , valuesBFS (not' true)  == [notE, true]+  , valuesBFS (not' $ not' true) == [notE, notE, true]+  , valuesBFS (false -&&- true) == [true, andE, false]+  , valuesBFS (true -||- false) == [false, orE, true]+  , valuesBFS (one -*- two -+- three -*- xx)+    == [plus, xx, two, times, three, times, one]+    -- (((+) (((*) 1) 2)) (((*) 3) x))++  , fillBFS (b_ -&&- b_) false == (b_ -&&- false)+  , fillBFS (b_ -&&- b_) (b_ -&&- b_) == (b_ -&&- (b_ -&&- b_))+  , fillBFS (b_ -&&- (b_ -&&- b_)) false == (false -&&- (b_ -&&- b_))+  , fillBFS (b_ -&&- (b_ -&&- b_)) (b_ -&&- b_) == ((b_ -&&- b_) -&&- (b_ -&&- b_))+  , fillBFS ((b_ -&&- b_) -&&- (b_ -&&- b_)) false == ((b_ -&&- b_) -&&- (b_ -&&- false))+  , fillBFS true false == true++  , holds n $ \(SameTypeE e1 e2) -> let e3 = fillBFS e1 e2+                                    in e3 == e1+                                    || length (holes e3) == length (holes e1) - 1 + length (holes e2)++  , boupCandidates i_ [zero, one, plus] =$ map sort . take 12 $=+    townCandidates i_ [zero, one, plus]++  , holds n $ \e es -> not (any hasHole es)+                   ==> boupCandidates e es =$ map sort . take 12 $= townCandidates e es   ]

@@ -4,15 +4,21 @@ add :: Int -> Int -> Int add x y  =  x + y -fact :: Int -> Int+factorial :: Int -> Int cannot conjure -(==>) :: Bool -> Bool -> Bool-p ==> q  =  q || not p+factorial :: Int -> Int+factorial x  =  foldr (*) 1 (enumFromTo 1 x)  second :: [Int] -> Int second xs  =  head (tail xs) +(++) :: [Int] -> [Int] -> [Int]+xs ++ ys  =  foldr (:) ys xs+ reverse :: [Int] -> [Int] cannot conjure++reverse :: [Int] -> [Int]+reverse xs  =  foldr (foldr (:) . unit) [] xs 

@@ -0,0 +1,21 @@+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).++import Test++main :: IO ()+main  =  mainTest tests 5040++tests :: Int -> [Bool]+tests n  =+  [ True++  , holds n $ \x -> iterateUntil (==) (`quot` (2 :: Int)) x == 0+  , holds n $ \xs -> iterateUntil (==) (drop 1) xs == ([]::[Bool])++  , holds n $ \xs ys -> length xs == length ys+                    ==> zipWith (<>) xs ys == mzip xs (ys :: [[Int]])++  , holds n $ \xs ys -> length xs >= length ys+                    ==> zipWith (<>) xs (ys <> repeat mempty) == mzip xs (ys :: [[Int]])+  ]