code-conjure 0.3.6 → 0.4.0

raw patch · 82 files changed

+3776/−642 lines, 82 filesdep ~expressdep ~leancheckdep ~speculatePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: express, leancheck, speculate

API changes (from Hackage documentation)

Files

• .gitignore +10/−0
• Makefile +16/−0
• README.md +12/−12
• TODO.md +2/−3
• bench/avgs.hs +36/−0
• bench/bench +26/−0
• bench/candidates.hs +71/−0
• bench/candidates.out +1959/−0
• bench/ill-hit.hs +11/−11
• bench/ill-hit.out +3/−0
• bench/longshot.hs +43/−43
• bench/longshot.out +5/−0
• bench/p12.hs +74/−0
• bench/p12.out +12/−0
• bench/p30.hs +90/−0
• bench/p30.out +2/−0
• bench/runtime/zero/bench/candidates.runtime +1/−0
• bench/runtime/zero/bench/ill-hit.runtime +1/−1
• bench/runtime/zero/bench/longshot.runtime +1/−1
• bench/runtime/zero/bench/p12.runtime +1/−0
• bench/runtime/zero/bench/p30.runtime +1/−0
• bench/runtime/zero/bench/take-drop.runtime +1/−1
• bench/runtime/zero/eg/bools.runtime +1/−1
• bench/runtime/zero/eg/count.runtime +1/−1
• bench/runtime/zero/eg/factorial.runtime +1/−1
• bench/runtime/zero/eg/fibonacci.runtime +1/−1
• bench/runtime/zero/eg/ints.runtime +1/−1
• bench/runtime/zero/eg/list.runtime +1/−1
• bench/runtime/zero/eg/replicate.runtime +1/−0
• bench/runtime/zero/eg/setelem.runtime +1/−1
• bench/runtime/zero/eg/subset.runtime +1/−0
• bench/runtime/zero/eg/tapps.runtime +1/−1
• bench/runtime/zero/eg/tree.runtime +1/−1
• bench/runtime/zero/versions +2/−2
• bench/self.hs +6/−6
• bench/self.out +4/−0
• bench/take-drop.hs +15/−15
• bench/take-drop.out +2/−0
• changelog.md +13/−0
• code-conjure.cabal +15/−5
• eg/arith.hs +5/−5
• eg/arith.out +4/−0
• eg/bools.hs +11/−11
• eg/bools.out +5/−1
• eg/count.hs +16/−8
• eg/count.out +13/−2
• eg/factorial.hs +13/−12
• eg/factorial.out +7/−3
• eg/fibonacci.hs +11/−11
• eg/fibonacci.out +3/−1
• eg/gcd.hs +3/−3
• eg/gcd.out +1/−0
• eg/ints.hs +10/−10
• eg/ints.out +6/−0
• eg/list.hs +43/−43
• eg/list.out +9/−0
• eg/replicate.hs +62/−0
• eg/replicate.out +54/−0
• eg/setelem.hs +22/−22
• eg/setelem.out +8/−6
• eg/spec.hs +11/−11
• eg/spec.out +2/−0
• eg/subset.hs +60/−0
• eg/subset.out +27/−0
• eg/tapps.hs +18/−18
• eg/tapps.out +3/−0
• eg/tree.hs +58/−44
• eg/tree.out +11/−5
• mk/Toplibs.hs +1/−0
• mk/depend.mk +161/−37
• src/Conjure.hs +16/−10
• src/Conjure/Cases.hs +0/−122
• src/Conjure/Conjurable.hs +154/−46
• src/Conjure/Defn.hs +104/−0
• src/Conjure/Engine.hs +122/−32
• src/Conjure/Expr.hs +13/−40
• src/Conjure/Prim.hs +80/−0
• src/Conjure/Spec.hs +29/−28
• src/Conjure/Utils.hs +12/−0
• stack.yaml +2/−2
• test/conjurable.hs +68/−0
• test/defn.hs +72/−0

@@ -26,6 +26,8 @@ tags TAGS +**.runtimes+ # benches, prototypes and test programs eg/arith eg/bools@@ -37,13 +39,21 @@ eg/list eg/tapps eg/tree+eg/replicate eg/setelem+eg/subset eg/spec bench/self bench/longshot bench/ill-hit bench/take-drop+bench/lots+bench/p12+bench/p30+bench/candidates proto/u-conjure test/expr test/conjurable test/utils+test/cases+test/defn

@@ -14,18 +14,24 @@   eg/bools \   eg/gcd \   eg/list \+  eg/replicate \   eg/setelem \+  eg/subset \   eg/spec \   eg/tapps \   eg/tree \+  bench/candidates \   bench/ill-hit \   bench/longshot \   bench/self \   bench/take-drop \+  bench/p12 \+  bench/p30 \   proto/u-conjure  TESTS = \   test/expr \+  test/defn \   test/conjurable \   test/utils @@ -89,5 +95,15 @@ # actual Haskell source files mk/toplibs: mk/Toplibs.o 	touch mk/toplibs++p12: bench/p12+	./bench/bench $< | tee bench/runtime/$$HOSTNAME/p12.runtimes++p30: bench/p30+	./bench/bench $< | tee bench/runtime/$$HOSTNAME/p30.runtimes++avgs:+	runhaskell bench/avgs.hs <bench/runtime/$$HOSTNAME/p12.runtimes+	runhaskell bench/avgs.hs <bench/runtime/$$HOSTNAME/p30.runtimes  include mk/haskell.mk

@@ -46,11 +46,11 @@  and -	primitives :: [Expr]-	primitives  =  [ val (0::Int)-	               , val (1::Int)-	               , value "+" ((+) :: Int -> Int -> Int)-	               , value "*" ((*) :: Int -> Int -> Int)+	primitives :: [Prim]+	primitives  =  [ pr (0::Int)+	               , pr (1::Int)+	               , prim "+" ((+) :: Int -> Int -> Int)+	               , prim "*" ((*) :: Int -> Int -> Int) 	               ]  running@@ -86,13 +86,13 @@  and -	primitives :: [Expr]-	primitives  =  [ val (0::Int)-	               , val (1::Int)-	               , value "+" ((+) :: Int -> Int -> Int)-	               , value "*" ((*) :: Int -> Int -> Int)-	               , value "dec" (subtract 1 :: Int -> Int)-	               , value "==" ((==) :: Int -> Int -> Bool)+	primitives :: [Prim]+	primitives  =  [ pr (0::Int)+	               , pr (1::Int)+	               , prim "+" ((+) :: Int -> Int -> Int)+	               , prim "*" ((*) :: Int -> Int -> Int)+	               , prim "dec" (subtract 1 :: Int -> Int)+	               , prim "==" ((==) :: Int -> Int -> Bool) 	               ]  running

@@ -3,10 +3,9 @@  A non-exhaustive list of things TO DO for Conjure. -* generate functions with top-level case patterns:+* add switch for case candidates? -        len []  =  0-        len (x:xs)  =  1 + len xs+* improve pruning of generated case candidates   ### for later

@@ -0,0 +1,36 @@+-- Computes averages of several benchmarks+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Data.List+import Data.Function+import Text.Printf++groupOn f  =  groupBy ((==) `on` f)++parseLine :: String -> (String,Double)+parseLine s  =  (n,t)+  where+  n  =  unwords $ init ws+  t  =  read $ last ws+  ws  =  words s++showLine :: (String,Double) -> String+showLine (s,x)  =  printf "%-25s %.2f" s x++collapseAvg :: [(String,Double)] -> (String,Double)+collapseAvg sxs  =  (fst $ head sxs, avg $ map snd sxs)++avg :: [Double] -> Double+avg xs  =  sum xs / fromIntegral (length xs)++io :: String -> String+io  =  unlines+    .  map showLine+    .  map collapseAvg+    .  groupOn fst+    .  map parseLine+    .  lines++main :: IO ()+main  =  interact io

@@ -0,0 +1,26 @@+#!/bin/bash+#+# A more elaborate benchmark for p12 and p30+#+# Copyright (C) 2021 Rudy Matela+# Distributed under the 3-Clause BSD licence (see the file LICENSE).++run1() {+	echo -n "$@" ""+	/usr/bin/time -f%e "$@" 2>&1 >/dev/null+}++run6() {+	run1 "$@"+	run1 "$@"+	run1 "$@"+	run1 "$@"+	run1 "$@"+	run1 "$@"+}++for fun in factorial sum product length count+do+	run6 $1 "$fun"+	run6 $1 "$fun" t+done

@@ -0,0 +1,71 @@+-- print candidates+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure+import Conjure.Engine+import Conjure.Defn+import Data.Express.Fixtures++printCandidates :: Conjurable f => Int -> String -> f -> [Prim] -> IO ()+printCandidates n nm f ps  =  do+  putStrLn $ "Candidates for: " ++ nm ++ " :: " ++ show (typeOf f)+  putStrLn $ "  pruning with " ++ show nRules ++ "/" ++ show nREs ++ " rules"+  putStrLn $ "  " ++ show (map length cs1) ++ " direct candidates"+  putStrLn $ "  " ++ show (map length csC) ++ " pattern candidates"+  putStrLn ""+  printThy thy+  putStrLn $ "direct candidates:\n"+  putStrLn $ unlines $ map showDefn $ concat $ cs1+  putStrLn $ "pattern candidates:\n"+  putStrLn $ unlines $ map showDefn $ concat $ csC+  where+  cs1  =  take n cs1'+  csC  =  take n csC'+  (cs1', thy)  =  candidateDefns1 args nm f ps+  (csC', _)    =  candidateDefnsC args nm f ps+  nRules  =  length (rules thy)+  nREs  =  length (equations thy) + nRules++main :: IO ()+main  =  do+  printCandidates 6 "foo" (undefined :: Int -> Int)+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((+) :: Int -> Int -> Int)+    ]++  printCandidates 4 "?" (undefined :: Int -> Int -> Int)+    [ pr (0 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((+) :: Int -> Int -> Int)+    ]++  printCandidates 6 "goo" (undefined :: [Int] -> [Int])+    [ pr ([] :: [Int])+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])+    ]++  printCandidates 4 "??" (undefined :: [Int] -> [Int] -> [Int])+    [ pr ([] :: [Int])+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])+    ]++  printCandidates 6 "ton" (undefined :: Bool -> Bool)+    [ pr False+    , pr True+    , prim "&&" (&&)+    , prim "||" (||)+    , prim "not" not+    ]++  printCandidates 6 "&|" (undefined :: Bool -> Bool -> Bool)+    [ pr False+    , pr True+    , prim "&&" (&&)+    , prim "||" (||)+    , prim "not" not+    ]

@@ -0,0 +1,1959 @@+Candidates for: foo :: Int -> Int+  pruning with 6/10 rules+  [3,0,4,0,8,0] direct candidates+  [3,4,8,21,39,70] pattern candidates++rules:+x * y == x + y+x * y == y + x+x + 0 == x+0 + x == x+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+equations:+y + x == x + y+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)++direct candidates:++foo x  =  x++foo x  =  0++foo x  =  1++foo x  =  x + x++foo x  =  x + 1++foo x  =  1 + x++foo x  =  1 + 1++foo x  =  x + (x + x)++foo x  =  x + (x + 1)++foo x  =  x + (1 + x)++foo x  =  x + (1 + 1)++foo x  =  1 + (x + x)++foo x  =  1 + (x + 1)++foo x  =  1 + (1 + x)++foo x  =  1 + (1 + 1)+++pattern candidates:++foo x  =  x++foo x  =  0++foo x  =  1++foo 0  =  0+foo x  =  x++foo 0  =  0+foo x  =  1++foo 0  =  1+foo x  =  x++foo 0  =  1+foo x  =  0++foo x  =  x + x++foo x  =  x + 1++foo x  =  1 + x++foo x  =  1 + 1++foo 1  =  0+foo x  =  x++foo 1  =  0+foo x  =  1++foo 1  =  1+foo x  =  x++foo 1  =  1+foo x  =  0++foo 0  =  0+foo x  =  x + x++foo 0  =  0+foo x  =  x + 1++foo 0  =  0+foo x  =  1 + x++foo 0  =  0+foo x  =  1 + 1++foo 0  =  1+foo x  =  x + x++foo 0  =  1+foo x  =  x + 1++foo 0  =  1+foo x  =  1 + x++foo 0  =  1+foo x  =  1 + 1++foo 0  =  1 + 1+foo x  =  x++foo 0  =  1 + 1+foo x  =  0++foo 0  =  1 + 1+foo x  =  1++foo 0  =  0+foo 1  =  0+foo x  =  x++foo 0  =  0+foo 1  =  0+foo x  =  1++foo 0  =  0+foo 1  =  1+foo x  =  x++foo 0  =  0+foo 1  =  1+foo x  =  0++foo 0  =  0+foo 1  =  1+foo x  =  1++foo 0  =  1+foo 1  =  0+foo x  =  x++foo 0  =  1+foo 1  =  0+foo x  =  0++foo 0  =  1+foo 1  =  0+foo x  =  1++foo 0  =  1+foo 1  =  1+foo x  =  x++foo 0  =  1+foo 1  =  1+foo x  =  0++foo 0  =  0+foo x  =  foo (x + x)++foo 0  =  0+foo x  =  foo (x + 1)++foo 0  =  0+foo x  =  foo (x + 1)++foo 0  =  0+foo x  =  foo (1 + x)++foo 0  =  0+foo x  =  foo (1 + x)++foo 0  =  0+foo x  =  foo (x + x)++foo 0  =  0+foo x  =  foo (x + 1)++foo 0  =  0+foo x  =  foo (x + 1)++foo 0  =  0+foo x  =  foo (1 + x)++foo 0  =  0+foo x  =  foo (1 + x)++foo 0  =  1+foo x  =  foo (x + x)++foo 0  =  1+foo x  =  foo (x + 1)++foo 0  =  1+foo x  =  foo (x + 1)++foo 0  =  1+foo x  =  foo (1 + x)++foo 0  =  1+foo x  =  foo (1 + x)++foo 0  =  1+foo x  =  foo (x + x)++foo 0  =  1+foo x  =  foo (x + 1)++foo 0  =  1+foo x  =  foo (x + 1)++foo 0  =  1+foo x  =  foo (1 + x)++foo 0  =  1+foo x  =  foo (1 + x)++foo x  =  x + (x + x)++foo x  =  x + (x + 1)++foo x  =  x + (1 + x)++foo x  =  x + (1 + 1)++foo x  =  1 + (x + x)++foo x  =  1 + (x + 1)++foo x  =  1 + (1 + x)++foo x  =  1 + (1 + 1)++foo 1  =  0+foo x  =  x + x++foo 1  =  0+foo x  =  x + 1++foo 1  =  0+foo x  =  1 + x++foo 1  =  0+foo x  =  1 + 1++foo 1  =  1+foo x  =  x + x++foo 1  =  1+foo x  =  x + 1++foo 1  =  1+foo x  =  1 + x++foo 1  =  1+foo x  =  1 + 1++foo 1  =  1 + 1+foo x  =  x++foo 1  =  1 + 1+foo x  =  0++foo 1  =  1 + 1+foo x  =  1++foo 1  =  0+foo x  =  foo (x + x)++foo 1  =  0+foo x  =  foo (x + 1)++foo 1  =  0+foo x  =  foo (x + 1)++foo 1  =  0+foo x  =  foo (1 + x)++foo 1  =  0+foo x  =  foo (1 + x)++foo 1  =  0+foo x  =  foo (x + x)++foo 1  =  0+foo x  =  foo (x + 1)++foo 1  =  0+foo x  =  foo (x + 1)++foo 1  =  0+foo x  =  foo (1 + x)++foo 1  =  0+foo x  =  foo (1 + x)++foo 1  =  1+foo x  =  foo (x + x)++foo 1  =  1+foo x  =  foo (x + 1)++foo 1  =  1+foo x  =  foo (x + 1)++foo 1  =  1+foo x  =  foo (1 + x)++foo 1  =  1+foo x  =  foo (1 + x)++foo 1  =  1+foo x  =  foo (x + x)++foo 1  =  1+foo x  =  foo (x + 1)++foo 1  =  1+foo x  =  foo (x + 1)++foo 1  =  1+foo x  =  foo (1 + x)++foo 1  =  1+foo x  =  foo (1 + x)++foo 0  =  0+foo x  =  x + (x + x)++foo 0  =  0+foo x  =  x + (x + 1)++foo 0  =  0+foo x  =  x + (1 + x)++foo 0  =  0+foo x  =  x + (1 + 1)++foo 0  =  0+foo x  =  1 + (x + x)++foo 0  =  0+foo x  =  1 + (x + 1)++foo 0  =  0+foo x  =  1 + (1 + x)++foo 0  =  0+foo x  =  1 + (1 + 1)++foo 0  =  1+foo x  =  x + (x + x)++foo 0  =  1+foo x  =  x + (x + 1)++foo 0  =  1+foo x  =  x + (1 + x)++foo 0  =  1+foo x  =  x + (1 + 1)++foo 0  =  1+foo x  =  1 + (x + x)++foo 0  =  1+foo x  =  1 + (x + 1)++foo 0  =  1+foo x  =  1 + (1 + x)++foo 0  =  1+foo x  =  1 + (1 + 1)++foo 0  =  1 + 1+foo x  =  x + x++foo 0  =  1 + 1+foo x  =  x + 1++foo 0  =  1 + 1+foo x  =  1 + x++foo 0  =  1 + (1 + 1)+foo x  =  x++foo 0  =  1 + (1 + 1)+foo x  =  0++foo 0  =  1 + (1 + 1)+foo x  =  1++foo 0  =  0+foo 1  =  0+foo x  =  x + x++foo 0  =  0+foo 1  =  0+foo x  =  x + 1++foo 0  =  0+foo 1  =  0+foo x  =  1 + x++foo 0  =  0+foo 1  =  0+foo x  =  1 + 1++foo 0  =  0+foo 1  =  1+foo x  =  x + x++foo 0  =  0+foo 1  =  1+foo x  =  x + 1++foo 0  =  0+foo 1  =  1+foo x  =  1 + x++foo 0  =  0+foo 1  =  1+foo x  =  1 + 1++foo 0  =  0+foo 1  =  1 + 1+foo x  =  x++foo 0  =  0+foo 1  =  1 + 1+foo x  =  0++foo 0  =  0+foo 1  =  1 + 1+foo x  =  1++foo 0  =  1+foo 1  =  0+foo x  =  x + x++foo 0  =  1+foo 1  =  0+foo x  =  x + 1++foo 0  =  1+foo 1  =  0+foo x  =  1 + x++foo 0  =  1+foo 1  =  0+foo x  =  1 + 1++foo 0  =  1+foo 1  =  1+foo x  =  x + x++foo 0  =  1+foo 1  =  1+foo x  =  x + 1++foo 0  =  1+foo 1  =  1+foo x  =  1 + x++foo 0  =  1+foo 1  =  1+foo x  =  1 + 1++foo 0  =  1+foo 1  =  1 + 1+foo x  =  x++foo 0  =  1+foo 1  =  1 + 1+foo x  =  0++foo 0  =  1+foo 1  =  1 + 1+foo x  =  1++foo 0  =  1 + 1+foo 1  =  0+foo x  =  x++foo 0  =  1 + 1+foo 1  =  0+foo x  =  0++foo 0  =  1 + 1+foo 1  =  0+foo x  =  1++foo 0  =  1 + 1+foo 1  =  1+foo x  =  x++foo 0  =  1 + 1+foo 1  =  1+foo x  =  0++foo 0  =  1 + 1+foo 1  =  1+foo x  =  1+++Candidates for: ? :: Int -> Int -> Int+  pruning with 6/10 rules+  [3,0,4,0] direct candidates+  [3,8,15,84] pattern candidates++rules:+x * y == x + y+x * y == y + x+x + 0 == x+0 + x == x+(x + y) + z == x + (y + z)+(x + y) + z == y + (x + z)+equations:+y + x == x + y+y + (x + z) == x + (y + z)+z + (x + y) == x + (y + z)+z + (y + x) == x + (y + z)++direct candidates:++x ? y  =  x++x ? y  =  y++x ? y  =  0++x ? y  =  x + x++x ? y  =  x + y++x ? y  =  y + x++x ? y  =  y + y+++pattern candidates:++x ? y  =  x++x ? y  =  y++x ? y  =  0++x ? 0  =  x+x ? y  =  y++x ? 0  =  x+x ? y  =  0++x ? 0  =  0+x ? y  =  x++x ? 0  =  0+x ? y  =  y++0 ? x  =  x+x ? y  =  y++0 ? x  =  x+x ? y  =  0++0 ? x  =  0+x ? y  =  x++0 ? x  =  0+x ? y  =  y++x ? y  =  x + x++x ? y  =  x + y++x ? y  =  y + x++x ? y  =  y + y++0 ? 0  =  0+0 ? x  =  x+x ? 0  =  x+x ? y  =  x++0 ? 0  =  0+0 ? x  =  x+x ? 0  =  x+x ? y  =  y++0 ? 0  =  0+0 ? x  =  x+x ? 0  =  x+x ? y  =  0++0 ? 0  =  0+0 ? x  =  x+x ? 0  =  0+x ? y  =  x++0 ? 0  =  0+0 ? x  =  x+x ? 0  =  0+x ? y  =  y++0 ? 0  =  0+0 ? x  =  x+x ? 0  =  0+x ? y  =  0++0 ? 0  =  0+0 ? x  =  0+x ? 0  =  x+x ? y  =  x++0 ? 0  =  0+0 ? x  =  0+x ? 0  =  x+x ? y  =  y++0 ? 0  =  0+0 ? x  =  0+x ? 0  =  x+x ? y  =  0++0 ? 0  =  0+0 ? x  =  0+x ? 0  =  0+x ? y  =  x++0 ? 0  =  0+0 ? x  =  0+x ? 0  =  0+x ? y  =  y++x ? 0  =  x+x ? y  =  x ? x++x ? 0  =  x+x ? y  =  x ? 0++x ? 0  =  x+x ? y  =  x ? 0++x ? 0  =  x+x ? y  =  y ? x++x ? 0  =  x+x ? y  =  y ? y++x ? 0  =  x+x ? y  =  y ? 0++x ? 0  =  x+x ? y  =  y ? 0++x ? 0  =  x+x ? y  =  0 ? x++x ? 0  =  x+x ? y  =  0 ? y++x ? 0  =  x+x ? y  =  0 ? x++x ? 0  =  x+x ? y  =  0 ? y++x ? 0  =  x ? x+x ? y  =  x++x ? 0  =  0 ? x+x ? y  =  x++x ? 0  =  0 ? x+x ? y  =  x++x ? 0  =  x ? x+x ? y  =  y++x ? 0  =  0 ? x+x ? y  =  y++x ? 0  =  0 ? x+x ? y  =  y++x ? 0  =  x ? x+x ? y  =  0++x ? 0  =  0 ? x+x ? y  =  0++x ? 0  =  0 ? x+x ? y  =  0++x ? 0  =  0+x ? y  =  x ? x++x ? 0  =  0+x ? y  =  x ? 0++x ? 0  =  0+x ? y  =  x ? 0++x ? 0  =  0+x ? y  =  y ? x++x ? 0  =  0+x ? y  =  y ? y++x ? 0  =  0+x ? y  =  y ? 0++x ? 0  =  0+x ? y  =  y ? 0++x ? 0  =  0+x ? y  =  0 ? x++x ? 0  =  0+x ? y  =  0 ? y++x ? 0  =  0+x ? y  =  0 ? x++x ? 0  =  0+x ? y  =  0 ? y++0 ? x  =  x+x ? y  =  x ? x++0 ? x  =  x+x ? y  =  x ? 0++0 ? x  =  x+x ? y  =  x ? 0++0 ? x  =  x+x ? y  =  y ? x++0 ? x  =  x+x ? y  =  y ? y++0 ? x  =  x+x ? y  =  y ? 0++0 ? x  =  x+x ? y  =  y ? 0++0 ? x  =  x+x ? y  =  0 ? x++0 ? x  =  x+x ? y  =  0 ? y++0 ? x  =  x+x ? y  =  0 ? x++0 ? x  =  x+x ? y  =  0 ? y++0 ? x  =  x ? x+x ? y  =  x++0 ? x  =  x ? 0+x ? y  =  x++0 ? x  =  x ? 0+x ? y  =  x++0 ? x  =  x ? x+x ? y  =  y++0 ? x  =  x ? 0+x ? y  =  y++0 ? x  =  x ? 0+x ? y  =  y++0 ? x  =  x ? x+x ? y  =  0++0 ? x  =  x ? 0+x ? y  =  0++0 ? x  =  x ? 0+x ? y  =  0++0 ? x  =  0+x ? y  =  x ? x++0 ? x  =  0+x ? y  =  x ? 0++0 ? x  =  0+x ? y  =  x ? 0++0 ? x  =  0+x ? y  =  y ? x++0 ? x  =  0+x ? y  =  y ? y++0 ? x  =  0+x ? y  =  y ? 0++0 ? x  =  0+x ? y  =  y ? 0++0 ? x  =  0+x ? y  =  0 ? x++0 ? x  =  0+x ? y  =  0 ? y++0 ? x  =  0+x ? y  =  0 ? x++0 ? x  =  0+x ? y  =  0 ? y++x ? 0  =  x+x ? y  =  x + x++x ? 0  =  x+x ? y  =  x + y++x ? 0  =  x+x ? y  =  y + x++x ? 0  =  x+x ? y  =  y + y++x ? 0  =  0+x ? y  =  x + x++x ? 0  =  0+x ? y  =  x + y++x ? 0  =  0+x ? y  =  y + x++x ? 0  =  0+x ? y  =  y + y++x ? 0  =  x + x+x ? y  =  x++x ? 0  =  x + x+x ? y  =  y++x ? 0  =  x + x+x ? y  =  0++0 ? x  =  x+x ? y  =  x + x++0 ? x  =  x+x ? y  =  x + y++0 ? x  =  x+x ? y  =  y + x++0 ? x  =  x+x ? y  =  y + y++0 ? x  =  0+x ? y  =  x + x++0 ? x  =  0+x ? y  =  x + y++0 ? x  =  0+x ? y  =  y + x++0 ? x  =  0+x ? y  =  y + y++0 ? x  =  x + x+x ? y  =  x++0 ? x  =  x + x+x ? y  =  y++0 ? x  =  x + x+x ? y  =  0+++Candidates for: goo :: [Int] -> [Int]+  pruning with 4/4 rules+  [2,0,1,0,1,0] direct candidates+  [2,1,2,3,10,7] pattern candidates++rules:+xs ++ [] == xs+[] ++ xs == xs+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)+(x:xs) ++ ys == x:(xs ++ ys)++direct candidates:++goo xs  =  xs++goo xs  =  []++goo xs  =  xs ++ xs++goo xs  =  xs ++ (xs ++ xs)+++pattern candidates:++goo xs  =  xs++goo xs  =  []++goo []  =  []+goo (x:xs)  =  xs++goo []  =  []+goo (x:xs)  =  goo xs++goo xs  =  xs ++ xs++goo []  =  []+goo (x:xs)  =  x:xs++goo []  =  []+goo (x:xs)  =  [x]++goo []  =  []+goo (x:xs)  =  xs ++ xs++goo []  =  []+goo (x:xs)  =  goo [x]++goo []  =  []+goo (x:xs)  =  goo [x]++goo []  =  []+goo (x:xs)  =  goo [x]++goo []  =  []+goo (x:xs)  =  goo [x]++goo []  =  []+goo (x:xs)  =  goo (xs ++ xs)++goo []  =  []+goo (x:xs)  =  goo (xs ++ xs)++goo []  =  []+goo (x:xs)  =  x:goo xs++goo []  =  []+goo (x:xs)  =  xs ++ goo xs++goo []  =  []+goo (x:xs)  =  goo xs ++ xs++goo xs  =  xs ++ (xs ++ xs)++goo []  =  []+goo (x:xs)  =  goo xs ++ goo xs++goo []  =  []+goo (x:xs)  =  x:x:xs++goo []  =  []+goo (x:xs)  =  [x,x]++goo []  =  []+goo (x:xs)  =  x:(xs ++ xs)++goo []  =  []+goo (x:xs)  =  xs ++ (x:xs)++goo []  =  []+goo (x:xs)  =  xs ++ [x]++goo []  =  []+goo (x:xs)  =  xs ++ (xs ++ xs)+++Candidates for: ?? :: [Int] -> [Int] -> [Int]+  pruning with 4/4 rules+  [3,0,4,0] direct candidates+  [3,8,15,82] pattern candidates++rules:+xs ++ [] == xs+[] ++ xs == xs+(xs ++ ys) ++ zs == xs ++ (ys ++ zs)+(x:xs) ++ ys == x:(xs ++ ys)++direct candidates:++xs ?? ys  =  xs++xs ?? ys  =  ys++xs ?? ys  =  []++xs ?? ys  =  xs ++ xs++xs ?? ys  =  xs ++ ys++xs ?? ys  =  ys ++ xs++xs ?? ys  =  ys ++ ys+++pattern candidates:++xs ?? ys  =  xs++xs ?? ys  =  ys++xs ?? ys  =  []++xs ?? []  =  xs+xs ?? (x:ys)  =  ys++xs ?? []  =  xs+xs ?? (x:ys)  =  []++xs ?? []  =  []+xs ?? (x:ys)  =  xs++xs ?? []  =  []+xs ?? (x:ys)  =  ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  []++[] ?? xs  =  []+(x:xs) ?? ys  =  xs++[] ?? xs  =  []+(x:xs) ?? ys  =  ys++xs ?? ys  =  xs ++ xs++xs ?? ys  =  xs ++ ys++xs ?? ys  =  ys ++ xs++xs ?? ys  =  ys ++ ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  []++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  xs+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  []++[] ?? []  =  []+[] ?? (x:xs)  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  xs++[] ?? []  =  []+[] ?? (x:xs)  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  ys++[] ?? []  =  []+[] ?? (x:xs)  =  []+(x:xs) ?? []  =  xs+(x:xs) ?? (y:ys)  =  []++[] ?? []  =  []+[] ?? (x:xs)  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  xs++[] ?? []  =  []+[] ?? (x:xs)  =  []+(x:xs) ?? []  =  []+(x:xs) ?? (y:ys)  =  ys++xs ?? []  =  xs+xs ?? (x:ys)  =  xs ?? xs++xs ?? []  =  xs+xs ?? (x:ys)  =  xs ?? ys++xs ?? []  =  xs+xs ?? (x:ys)  =  xs ?? []++xs ?? []  =  xs+xs ?? (x:ys)  =  xs ?? []++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ?? xs++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ?? ys++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ?? []++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ?? []++xs ?? []  =  xs+xs ?? (x:ys)  =  [] ?? xs++xs ?? []  =  xs+xs ?? (x:ys)  =  [] ?? ys++xs ?? []  =  xs+xs ?? (x:ys)  =  [] ?? xs++xs ?? []  =  xs+xs ?? (x:ys)  =  [] ?? ys++xs ?? []  =  []+xs ?? (x:ys)  =  xs ?? xs++xs ?? []  =  []+xs ?? (x:ys)  =  xs ?? ys++xs ?? []  =  []+xs ?? (x:ys)  =  xs ?? []++xs ?? []  =  []+xs ?? (x:ys)  =  xs ?? []++xs ?? []  =  []+xs ?? (x:ys)  =  ys ?? xs++xs ?? []  =  []+xs ?? (x:ys)  =  ys ?? ys++xs ?? []  =  []+xs ?? (x:ys)  =  ys ?? []++xs ?? []  =  []+xs ?? (x:ys)  =  ys ?? []++xs ?? []  =  []+xs ?? (x:ys)  =  [] ?? xs++xs ?? []  =  []+xs ?? (x:ys)  =  [] ?? ys++xs ?? []  =  []+xs ?? (x:ys)  =  [] ?? xs++xs ?? []  =  []+xs ?? (x:ys)  =  [] ?? ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs ?? xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs ?? ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs ?? []++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs ?? []++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ?? xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ?? ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ?? []++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ?? []++[] ?? xs  =  xs+(x:xs) ?? ys  =  [] ?? xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  [] ?? ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  [] ?? xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  [] ?? ys++[] ?? xs  =  []+(x:xs) ?? ys  =  xs ?? xs++[] ?? xs  =  []+(x:xs) ?? ys  =  xs ?? ys++[] ?? xs  =  []+(x:xs) ?? ys  =  xs ?? []++[] ?? xs  =  []+(x:xs) ?? ys  =  xs ?? []++[] ?? xs  =  []+(x:xs) ?? ys  =  ys ?? xs++[] ?? xs  =  []+(x:xs) ?? ys  =  ys ?? ys++[] ?? xs  =  []+(x:xs) ?? ys  =  ys ?? []++[] ?? xs  =  []+(x:xs) ?? ys  =  ys ?? []++[] ?? xs  =  []+(x:xs) ?? ys  =  [] ?? xs++[] ?? xs  =  []+(x:xs) ?? ys  =  [] ?? ys++[] ?? xs  =  []+(x:xs) ?? ys  =  [] ?? xs++[] ?? xs  =  []+(x:xs) ?? ys  =  [] ?? ys++xs ?? []  =  xs+xs ?? (x:ys)  =  x:xs++xs ?? []  =  xs+xs ?? (x:ys)  =  x:ys++xs ?? []  =  xs+xs ?? (x:ys)  =  [x]++xs ?? []  =  xs+xs ?? (x:ys)  =  xs ++ xs++xs ?? []  =  xs+xs ?? (x:ys)  =  xs ++ ys++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ++ xs++xs ?? []  =  xs+xs ?? (x:ys)  =  ys ++ ys++xs ?? []  =  []+xs ?? (x:ys)  =  x:xs++xs ?? []  =  []+xs ?? (x:ys)  =  x:ys++xs ?? []  =  []+xs ?? (x:ys)  =  [x]++xs ?? []  =  []+xs ?? (x:ys)  =  xs ++ xs++xs ?? []  =  []+xs ?? (x:ys)  =  xs ++ ys++xs ?? []  =  []+xs ?? (x:ys)  =  ys ++ xs++xs ?? []  =  []+xs ?? (x:ys)  =  ys ++ ys++xs ?? []  =  xs ++ xs+xs ?? (x:ys)  =  xs++xs ?? []  =  xs ++ xs+xs ?? (x:ys)  =  ys++xs ?? []  =  xs ++ xs+xs ?? (x:ys)  =  []++[] ?? xs  =  xs+(x:xs) ?? ys  =  x:xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  x:ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  [x]++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs ++ xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  xs ++ ys++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ++ xs++[] ?? xs  =  xs+(x:xs) ?? ys  =  ys ++ ys++[] ?? xs  =  []+(x:xs) ?? ys  =  x:xs++[] ?? xs  =  []+(x:xs) ?? ys  =  x:ys++[] ?? xs  =  []+(x:xs) ?? ys  =  [x]++[] ?? xs  =  []+(x:xs) ?? ys  =  xs ++ xs++[] ?? xs  =  []+(x:xs) ?? ys  =  xs ++ ys++[] ?? xs  =  []+(x:xs) ?? ys  =  ys ++ xs++[] ?? xs  =  []+(x:xs) ?? ys  =  ys ++ ys++[] ?? xs  =  xs ++ xs+(x:xs) ?? ys  =  xs++[] ?? xs  =  xs ++ xs+(x:xs) ?? ys  =  ys++[] ?? xs  =  xs ++ xs+(x:xs) ?? ys  =  []+++Candidates for: ton :: Bool -> Bool+  pruning with 39/49 rules+  [3,1,0,0,2,4] direct candidates+  [3,3,0,0,0,0] pattern candidates++rules:+not False == True+not True == False+p && p == p+p || p == p+not (not p) == p+p && False == False+p && True == p+False && p == False+True && p == p+p || False == p+p || True == True+False || p == p+True || p == True+not (p && q) == not p || not q+not (p && q) == not q || not p+not (p || q) == not p && not q+not (p || q) == not q && not p+p && not p == False+not p && p == False+p || not p == True+not p || p == True+(p && q) && r == p && (q && r)+(p && q) && r == q && (p && r)+(p || q) || r == p || (q || r)+(p || q) || r == q || (p || r)+p && (p && q) == p && q+p && (q && p) == p && q+p && (q && p) == q && p+p || (p || q) == p || q+p || (q || p) == p || q+p || (q || p) == q || p+p && (p || q) == p+p && (q || p) == p+(p || q) && p == p+(p || q) && q == q+p || p && q == p+p || q && p == p+p && q || p == p+p && q || q == q+equations:+q && p == p && q+q || p == p || q+q && (p && r) == p && (q && r)+r && (p && q) == p && (q && r)+r && (q && p) == p && (q && r)+q || (p || r) == p || (q || r)+r || (p || q) == p || (q || r)+r || (q || p) == p || (q || r)+(r || q) && p == p && (q || r)+r && q || p == p || q && r++direct candidates:++ton p  =  p++ton p  =  False++ton p  =  True++ton p  =  not p++ton p  =  p && ton (not p)++ton p  =  p || ton (not p)++ton p  =  p && not (ton (not p))++ton p  =  not p && ton (not p)++ton p  =  p || not (ton (not p))++ton p  =  not p || ton (not p)+++pattern candidates:++ton p  =  p++ton p  =  False++ton p  =  True++ton p  =  not p++ton False  =  False+ton True  =  True++ton False  =  True+ton True  =  False+++Candidates for: &| :: Bool -> Bool -> Bool+  pruning with 39/49 rules+  [4,2,4,8,4,72] direct candidates+  [4,14,30,8,4,32] pattern candidates++rules:+not False == True+not True == False+p && p == p+p || p == p+not (not p) == p+p && False == False+p && True == p+False && p == False+True && p == p+p || False == p+p || True == True+False || p == p+True || p == True+not (p && q) == not p || not q+not (p && q) == not q || not p+not (p || q) == not p && not q+not (p || q) == not q && not p+p && not p == False+not p && p == False+p || not p == True+not p || p == True+(p && q) && r == p && (q && r)+(p && q) && r == q && (p && r)+(p || q) || r == p || (q || r)+(p || q) || r == q || (p || r)+p && (p && q) == p && q+p && (q && p) == p && q+p && (q && p) == q && p+p || (p || q) == p || q+p || (q || p) == p || q+p || (q || p) == q || p+p && (p || q) == p+p && (q || p) == p+(p || q) && p == p+(p || q) && q == q+p || p && q == p+p || q && p == p+p && q || p == p+p && q || q == q+equations:+q && p == p && q+q || p == p || q+q && (p && r) == p && (q && r)+r && (p && q) == p && (q && r)+r && (q && p) == p && (q && r)+q || (p || r) == p || (q || r)+r || (p || q) == p || (q || r)+r || (q || p) == p || (q || r)+(r || q) && p == p && (q || r)+r && q || p == p || q && r++direct candidates:++p &| q  =  p++p &| q  =  q++p &| q  =  False++p &| q  =  True++p &| q  =  not p++p &| q  =  not q++p &| q  =  p && q++p &| q  =  q && p++p &| q  =  p || q++p &| q  =  q || p++p &| q  =  not p && q++p &| q  =  not q && p++p &| q  =  not p || q++p &| q  =  not q || p++p &| q  =  p && not q++p &| q  =  q && not p++p &| q  =  p || not q++p &| q  =  q || not p++p &| q  =  not p && not q++p &| q  =  not q && not p++p &| q  =  not p || not q++p &| q  =  not q || not p++p &| q  =  p && (not p && q)++p &| q  =  p && (not p || q)++p &| q  =  p && (q && not p)++p &| q  =  p && (q || not p)++p &| q  =  q && (not q && p)++p &| q  =  q && (not q || p)++p &| q  =  q && (p && not q)++p &| q  =  q && (p || not q)++p &| q  =  p || not p && q++p &| q  =  p || (not p || q)++p &| q  =  p || q && not p++p &| q  =  p || (q || not p)++p &| q  =  q || not q && p++p &| q  =  q || (not q || p)++p &| q  =  q || p && not q++p &| q  =  q || (p || not q)++p &| q  =  not p && (p || q)++p &| q  =  not p && (q || p)++p &| q  =  not q && (p || q)++p &| q  =  not q && (q || p)++p &| q  =  not p || p && q++p &| q  =  not p || q && p++p &| q  =  not q || p && q++p &| q  =  not q || q && p++p &| q  =  (p || q) && not p++p &| q  =  (p || q) && not q++p &| q  =  (q || p) && not p++p &| q  =  (q || p) && not q++p &| q  =  p && q || not p++p &| q  =  p && q || not q++p &| q  =  q && p || not p++p &| q  =  q && p || not q++p &| q  =  p && p &| not q++p &| q  =  p && q &| not p++p &| q  =  p && q &| not q++p &| q  =  p && False &| not q++p &| q  =  p && True &| not q++p &| q  =  p && not p &| p++p &| q  =  p && not p &| q++p &| q  =  p && not p &| False++p &| q  =  p && not p &| True++p &| q  =  p && not q &| p++p &| q  =  q && p &| not q++p &| q  =  q && q &| not p++p &| q  =  q && q &| not q++p &| q  =  q && False &| not q++p &| q  =  q && True &| not q++p &| q  =  q && not p &| p++p &| q  =  q && not p &| q++p &| q  =  q && not p &| False++p &| q  =  q && not p &| True++p &| q  =  q && not q &| p++p &| q  =  p || p &| not q++p &| q  =  p || q &| not p++p &| q  =  p || q &| not q++p &| q  =  p || False &| not q++p &| q  =  p || True &| not q++p &| q  =  p || not p &| p++p &| q  =  p || not p &| q++p &| q  =  p || not p &| False++p &| q  =  p || not p &| True++p &| q  =  p || not q &| p++p &| q  =  q || p &| not q++p &| q  =  q || q &| not p++p &| q  =  q || q &| not q++p &| q  =  q || False &| not q++p &| q  =  q || True &| not q++p &| q  =  q || not p &| p++p &| q  =  q || not p &| q++p &| q  =  q || not p &| False++p &| q  =  q || not p &| True++p &| q  =  q || not q &| p+++pattern candidates:++p &| q  =  p++p &| q  =  q++p &| q  =  False++p &| q  =  True++p &| q  =  not p++p &| q  =  not q++p &| False  =  p+p &| True  =  False++p &| False  =  p+p &| True  =  True++p &| False  =  False+p &| True  =  p++p &| False  =  False+p &| True  =  True++p &| False  =  True+p &| True  =  p++p &| False  =  True+p &| True  =  False++False &| p  =  p+True &| p  =  False++False &| p  =  p+True &| p  =  True++False &| p  =  False+True &| p  =  p++False &| p  =  False+True &| p  =  True++False &| p  =  True+True &| p  =  p++False &| p  =  True+True &| p  =  False++p &| q  =  p && q++p &| q  =  q && p++p &| q  =  p || q++p &| q  =  q || p++p &| False  =  p+p &| True  =  not p++p &| False  =  False+p &| True  =  not p++p &| False  =  True+p &| True  =  not p++p &| False  =  not p+p &| True  =  p++p &| False  =  not p+p &| True  =  False++p &| False  =  not p+p &| True  =  True++False &| p  =  p+True &| p  =  not p++False &| p  =  False+True &| p  =  not p++False &| p  =  True+True &| p  =  not p++False &| p  =  not p+True &| p  =  p++False &| p  =  not p+True &| p  =  False++False &| p  =  not p+True &| p  =  True++False &| False  =  False+False &| True  =  False+True &| False  =  False+True &| True  =  True++False &| False  =  False+False &| True  =  False+True &| False  =  True+True &| True  =  False++False &| False  =  False+False &| True  =  False+True &| False  =  True+True &| True  =  True++False &| False  =  False+False &| True  =  True+True &| False  =  False+True &| True  =  False++False &| False  =  False+False &| True  =  True+True &| False  =  False+True &| True  =  True++False &| False  =  False+False &| True  =  True+True &| False  =  True+True &| True  =  False++False &| False  =  False+False &| True  =  True+True &| False  =  True+True &| True  =  True++False &| False  =  True+False &| True  =  False+True &| False  =  False+True &| True  =  False++False &| False  =  True+False &| True  =  False+True &| False  =  False+True &| True  =  True++False &| False  =  True+False &| True  =  False+True &| False  =  True+True &| True  =  False++False &| False  =  True+False &| True  =  False+True &| False  =  True+True &| True  =  True++False &| False  =  True+False &| True  =  True+True &| False  =  False+True &| True  =  False++False &| False  =  True+False &| True  =  True+True &| False  =  False+True &| True  =  True++False &| False  =  True+False &| True  =  True+True &| False  =  True+True &| True  =  False++p &| q  =  not p && q++p &| q  =  not q && p++p &| q  =  not p || q++p &| q  =  not q || p++p &| q  =  p && not q++p &| q  =  q && not p++p &| q  =  p || not q++p &| q  =  q || not p++p &| q  =  not p && not q++p &| q  =  not q && not p++p &| q  =  not p || not q++p &| q  =  not q || not p++p &| q  =  p && (not p && q)++p &| q  =  p && (not p || q)++p &| q  =  p && (q && not p)++p &| q  =  p && (q || not p)++p &| q  =  q && (not q && p)++p &| q  =  q && (not q || p)++p &| q  =  q && (p && not q)++p &| q  =  q && (p || not q)++p &| q  =  p || not p && q++p &| q  =  p || (not p || q)++p &| q  =  p || q && not p++p &| q  =  p || (q || not p)++p &| q  =  q || not q && p++p &| q  =  q || (not q || p)++p &| q  =  q || p && not q++p &| q  =  q || (p || not q)++p &| q  =  not p && (p || q)++p &| q  =  not p && (q || p)++p &| q  =  not q && (p || q)++p &| q  =  not q && (q || p)++p &| q  =  not p || p && q++p &| q  =  not p || q && p++p &| q  =  not q || p && q++p &| q  =  not q || q && p++p &| q  =  (p || q) && not p++p &| q  =  (p || q) && not q++p &| q  =  (q || p) && not p++p &| q  =  (q || p) && not q++p &| q  =  p && q || not p++p &| q  =  p && q || not q++p &| q  =  q && p || not p++p &| q  =  q && p || not q++

@@ -2,7 +2,7 @@ -- -- Based on an example sent by Colin Runciman ----- Even though sum' is defined for 6 values,+-- Even though sum' is defined for 6 prims, -- Conjure only ever hits 4 of them. import Conjure @@ -25,10 +25,10 @@  main :: IO () main  =  do-  -- the following does not hit all 6 defined values, only 4+  -- the following does not hit all 6 defined prims, only 4   conjure "sum" (sum' :: [Int] -> Int) primitives -  -- the following forces 3 argument values, totaling 6+  -- the following forces 3 argument prims, totaling 6   conjureWith as "sum" (sum' :: [Int] -> Int) primitives    -- the following conjures from a spec@@ -43,13 +43,13 @@                   ]     } -primitives :: [Expr]+primitives :: [Prim] 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])+  [ pr (0 :: Int)+  , pr (1 :: Int)+  , prim "+" ((+) :: Int -> Int -> Int)+  , prim "*" ((*) :: Int -> Int -> Int)+  , prim "null" (null :: [Int] -> Bool)+  , prim "head" (head :: [Int] -> Int)+  , prim "tail" (tail :: [Int] -> [Int])   ]

@@ -1,5 +1,6 @@ sum :: [Int] -> Int -- testing 4 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -14,6 +15,7 @@  sum :: [Int] -> Int -- testing 6 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -28,6 +30,7 @@  sum :: [Int] -> Int -- testing 6 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3

@@ -51,15 +51,15 @@   -- not only this is out of reach performance wise,   -- but the needed recursive calls will not be enumerated   conjure "qsort" sort'-    [ val ([] :: [Int])-    , value ":" ((:) :: Int -> [Int] -> [Int])-    , value "head" (head :: [Int] -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)-    , value "++" ((++) :: [Int] -> [Int] -> [Int])-    , value "<" ((<) :: Int -> Int -> Bool)-    , value ">=" ((>=) :: Int -> Int -> Bool)-    , value "filter" (filter :: (Int -> Bool) -> [Int] -> [Int])+    [ pr ([] :: [Int])+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])+    , prim "<" ((<) :: Int -> Int -> Bool)+    , prim ">=" ((>=) :: Int -> Int -> Bool)+    , prim "filter" (filter :: (Int -> Bool) -> [Int] -> [Int])     ]    -- pow b e  =  if e == 0 then 1 else b * pow b (dec e)@@ -67,24 +67,24 @@   -- somehow this takes 30s to run, the two arguments   -- of the same type introduce the difficulty here.   conjureWithMaxSize 8 "pow" pow-    [ val (0::Int)-    , val (1::Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "*" ((*) :: Int -> Int -> Int)-    , value "dec" (subtract 1 :: Int -> Int)-    , value "==" ((==) :: Int -> Int -> Bool)+    [ pr (0::Int)+    , pr (1::Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)+    , prim "dec" (subtract 1 :: Int -> Int)+    , prim "==" ((==) :: Int -> Int -> Bool)     ]    -- pow b e  =  if e == 0 then 1 else pow b (halve e) * pow b (halve e) * if odd e then b else 1   --             1  2  3 4      5      6   7  8     9 10 11 12  13   14 15 16 17  18    19     20   -- out of reach performance wise   conjureWithMaxSize 8 "pow" pow-    [ val (0::Int)-    , val (1::Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "*" ((*) :: Int -> Int -> Int)-    , value "halve" ((`div` 2) :: Int -> Int)-    , value "==" ((==) :: Int -> Int -> Bool)+    [ pr (0::Int)+    , pr (1::Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)+    , prim "halve" ((`div` 2) :: Int -> Int)+    , prim "==" ((==) :: Int -> Int -> Bool)     ]    -- duplicates xs  =@@ -94,29 +94,29 @@   --        then head xs : duplicates (tail xs)                                     -- 24   --        else duplicates (tail xs)                                               -- 27   conjure "duplicates" duplicates-    [ val ([] :: [Int])-    , val True-    , val False-    , value "not" not-    , value "||" (||)-    , value "&&" (&&)-    , value ":" ((:) :: Int -> [Int] -> [Int])-    , value "head" (head :: [Int] -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)-    , value "elem" (elem :: Int -> [Int] -> Bool)+    [ pr ([] :: [Int])+    , pr True+    , pr False+    , prim "not" not+    , prim "||" (||)+    , prim "&&" (&&)+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)+    , prim "elem" (elem :: Int -> [Int] -> Bool)     ]    conjure "positionsFrom" positionsFrom-    [ val ([] :: [Int])-    , val True-    , val False-    , value "not" not-    , value "||" (||)-    , value "&&" (&&)-    , value ":" ((:) :: Int -> [Int] -> [Int])-    , value "head" (head :: [Int] -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)-    , value "==" ((==) :: Int -> Int -> Bool)+    [ pr ([] :: [Int])+    , pr True+    , pr False+    , prim "not" not+    , prim "||" (||)+    , prim "&&" (&&)+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)+    , prim "==" ((==) :: Int -> Int -> Bool)     ]

@@ -1,5 +1,6 @@ qsort :: [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 13/14 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 3 candidates of size 3@@ -16,6 +17,7 @@  pow :: Int -> Int -> Int -- testing 5 combinations of argument values+-- pruning with 40/73 rules -- looking through 4 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 13 candidates of size 3@@ -28,6 +30,7 @@  pow :: Int -> Int -> Int -- testing 5 combinations of argument values+-- pruning with 31/55 rules -- looking through 4 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 15 candidates of size 3@@ -40,6 +43,7 @@  duplicates :: [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 44/55 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 2 candidates of size 3@@ -56,6 +60,7 @@  positionsFrom :: Int -> Int -> [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 42/55 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 6 candidates of size 3

@@ -0,0 +1,74 @@+-- 12 background primitives+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure+import System.Environment++conjureT :: Conjurable f => String -> f -> [Prim] -> IO ()+conjureT  =  conjureWith args{maxSize=1}++factorial :: Int -> Int+factorial 0  =  1+factorial 1  =  1+factorial 2  =  2+factorial 3  =  6+factorial 4  =  24+factorial 5  =  120++count' :: Int -> [Int] -> Int+count' 0 [0]  =  1+count' 0 [1]  =  0+count' 1 [0]  =  0+count' 1 [1]  =  1+count' 0 [0,0]  =  2+count' 0 [0,1]  =  1+count' 0 [1,2]  =  0+count' 1 [0,0]  =  0+count' 1 [0,1]  =  1+count' 1 [1,2]  =  1+count' 0 [0,0,0]  =  3+count' 0 [0,0,1]  =  2+count' 0 [1,0,0]  =  2++main :: IO ()+main  =  do+  putStrLn $ "running with " ++ show (length primitives) ++ " primitives"+  as <- getArgs+  case as of+    ["factorial"]     -> conjure  "factorial n" factorial primitives+    ["factorial","t"] -> conjureT "factorial n" factorial primitives+    ["sum"]           -> conjure  "sum"     (sum     :: [Int] -> Int) primitives+    ["sum","t"]       -> conjureT "sum"     (sum     :: [Int] -> Int) primitives+    ["product"]       -> conjure  "product" (product :: [Int] -> Int) primitives+    ["product","t"]   -> conjureT "product" (product :: [Int] -> Int) primitives+    ["length"]        -> conjure  "length"  (length  :: [Int] -> Int) primitives+    ["length","t"]    -> conjureT "length"  (length  :: [Int] -> Int) primitives+    ["count"]         -> conjure  "count"   count' $ primitives ++ primsCount+    ["count","t"]     -> conjureT "count"   count' $ primitives ++ primsCount+    _                 -> conjure  "factorial n" factorial primitives++primitives :: [Prim]+primitives  =+  [ pr (0::Int)+  , pr (1::Int)+  , prim "+" ((+) :: Int -> Int -> Int)+  , prim "*" ((*) :: Int -> Int -> Int)+  , prim "dec" (subtract 1 :: Int -> Int)++  , prim "==" ((==) :: Int -> Int -> Bool)++  , pr ([] :: [Int])+  , prim ":" ((:) :: Int -> [Int] -> [Int])+  , prim "head" (head :: [Int] -> Int)+  , prim "tail" (tail :: [Int] -> [Int])+  , prim "null" (null :: [Int] -> Bool)+  , prim "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)+  , prim ".." (enumFromTo :: Int -> Int -> [Int])+  ]++primsCount :: [Prim]+primsCount  =+  [ prim "length" (length :: [Int] -> Int)+  , prim "filter" (filter :: (Int -> Bool) -> [Int] -> [Int])+  ]

@@ -0,0 +1,12 @@+running with 13 primitives+factorial :: Int -> Int+-- testing 6 combinations of argument values+-- pruning with 67/100 rules+-- looking through 3 candidates of size 1+-- looking through 3 candidates of size 2+-- looking through 6 candidates of size 3+-- looking through 16 candidates of size 4+-- looking through 55 candidates of size 5+-- looking through 175 candidates of size 6+factorial n  =  foldr (*) 1 [1..n]+

@@ -0,0 +1,90 @@+-- 30 background primitives, does Conjure scale?+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure+import System.Environment++conjureT :: Conjurable f => String -> f -> [Prim] -> IO ()+conjureT  =  conjureWith args{maxSize=1}++factorial :: Int -> Int+factorial 0  =  1+factorial 1  =  1+factorial 2  =  2+factorial 3  =  6+factorial 4  =  24+factorial 5  =  120++count' :: Int -> [Int] -> Int+count' 0 [0]  =  1+count' 0 [1]  =  0+count' 1 [0]  =  0+count' 1 [1]  =  1+count' 0 [0,0]  =  2+count' 0 [0,1]  =  1+count' 0 [1,2]  =  0+count' 1 [0,0]  =  0+count' 1 [0,1]  =  1+count' 1 [1,2]  =  1+count' 0 [0,0,0]  =  3+count' 0 [0,0,1]  =  2+count' 0 [1,0,0]  =  2++main :: IO ()+main  =  do+  putStrLn $ "running with " ++ show (length primitives) ++ " primitives"+  as <- getArgs+  case as of+    ["factorial"]     -> conjure  "factorial n" factorial primitives+    ["factorial","t"] -> conjureT "factorial n" factorial primitives+    ["sum"]           -> conjure  "sum"     (sum     :: [Int] -> Int) primitives+    ["sum","t"]       -> conjureT "sum"     (sum     :: [Int] -> Int) primitives+    ["product"]       -> conjure  "product" (product :: [Int] -> Int) primitives+    ["product","t"]   -> conjureT "product" (product :: [Int] -> Int) primitives+    ["length"]        -> conjure  "length"  (length  :: [Int] -> Int) primitives+    ["length","t"]    -> conjureT "length"  (length  :: [Int] -> Int) primitives+    ["count"]         -> conjure  "count"   count' $ primitives ++ primsLength+    ["count","t"]     -> conjureT "count"   count' $ primitives ++ primsLength+    _                 -> putStrLn "usage: p30 <factorial|sum|product|length|count> [t]"++primitives :: [Prim]+primitives  =+  [ pr False+  , pr True+  , prim "&&" (&&)+  , prim "||" (||)+  , prim "not" not++  , pr (0::Int)+  , pr (1::Int)+  , prim "+" ((+) :: Int -> Int -> Int)+  , prim "*" ((*) :: Int -> Int -> Int)+  , prim "dec" (subtract 1 :: Int -> Int)+  , prim "-" ((-) :: Int -> Int -> Int)++  , prim "==" ((==) :: Int -> Int -> Bool)+  , prim "<=" ((<=) :: Int -> Int -> Bool)+  , prim "<"  ((<) :: Int -> Int -> Bool)++  , prim "const" (const :: Int -> Int -> Int)++  , pr ([] :: [Int])+  , prim ":" ((:) :: Int -> [Int] -> [Int])+  , prim "head" (head :: [Int] -> Int)+  , prim "tail" (tail :: [Int] -> [Int])+  , prim "null" (null :: [Int] -> Bool)+  , prim "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)++  , prim "map" (map :: (Int -> Int) -> [Int] -> [Int])+  , prim "filter" (filter :: (Int -> Bool) -> [Int] -> [Int])+  , prim ".." (enumFromTo :: Int -> Int -> [Int])++  , prim "++" ((++) :: [Int] -> [Int] -> [Int])+  , prim "elem" (elem :: Int -> [Int] -> Bool)+  ]++primsLength :: [Prim]+primsLength =+  [ prim "length" (length :: [Int] -> Int)+  ]

@@ -0,0 +1,2 @@+running with 26 primitives+usage: p30 <factorial|sum|product|length|count> [t]

@@ -0,0 +1,1 @@+2.1

@@ -1,1 +1,1 @@-1.2+1.4

@@ -1,1 +1,1 @@-4.7+10.0

@@ -0,0 +1,1 @@+2.9

@@ -0,0 +1,1 @@+0.0

@@ -1,1 +1,1 @@-7.2+10.6

@@ -1,1 +1,1 @@-3.0+3.9

@@ -1,1 +1,1 @@-3.2+4.4

@@ -1,1 +1,1 @@-1.5+2.8

@@ -1,1 +1,1 @@-22.2+29.9

@@ -1,1 +1,1 @@-1.0+1.3

@@ -1,1 +1,1 @@-0.5+1.1

@@ -0,0 +1,1 @@+7.0

@@ -1,1 +1,1 @@-22.5+41.7

@@ -0,0 +1,1 @@+7.1

@@ -1,1 +1,1 @@-0.5+0.7

@@ -1,1 +1,1 @@-5.6+8.1

@@ -1,4 +1,4 @@ GHC 8.10.4 leancheck-0.9.10-express-0.1.14-speculate-0.4.8+express-1.0.2+speculate-0.4.10

@@ -12,13 +12,13 @@   cj "d" ((subtract 1) :: Int -> Int) primitives   where   -- the monomorphism restriction strikes again-  cj :: Conjurable f => String -> f -> [Expr] -> IO ()+  cj :: Conjurable f => String -> f -> [Prim] -> IO ()   cj  =  conjureWith args{maxSize=3,maxEquationSize=0} -primitives :: [Expr]+primitives :: [Prim] primitives =-  [ val (0::Int)-  , val (1::Int)-  , value "+" ((+) :: Int -> Int -> Int)-  , value "*" ((*) :: Int -> Int -> Int)+  [ pr (0::Int)+  , pr (1::Int)+  , prim "+" ((+) :: Int -> Int -> Int)+  , prim "*" ((*) :: Int -> Int -> Int)   ]

@@ -1,5 +1,6 @@ (?) :: Int -> Int -> Int -- testing 60 combinations of argument values+-- pruning with 0/0 rules -- looking through 4 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 32 candidates of size 3@@ -7,6 +8,7 @@  (?) :: Int -> Int -> Int -- testing 60 combinations of argument values+-- pruning with 0/0 rules -- looking through 4 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 32 candidates of size 3@@ -14,6 +16,7 @@  i :: Int -> Int -- testing 60 combinations of argument values+-- pruning with 0/0 rules -- looking through 3 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 18 candidates of size 3@@ -21,6 +24,7 @@  d :: Int -> Int -- testing 60 combinations of argument values+-- pruning with 0/0 rules -- looking through 3 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 18 candidates of size 3

@@ -22,24 +22,24 @@   -- drop n xs = if n==0 || null xs then xs else drop (dec n) (tail xs)   -- needs size 13   conjureWithMaxSize 13 "drop" (drop' :: Int -> [A] -> [A])-    [ val (0 :: Int)-    , value "null" (null :: [A] -> Bool)-    , value "==" ((==) :: Int -> Int -> Bool)-    , value "||" (||)-    , value "dec" (subtract 1 :: Int -> Int)-    , value "tail" (tail :: [A] -> [A])+    [ pr (0 :: Int)+    , prim "null" (null :: [A] -> Bool)+    , prim "==" ((==) :: Int -> Int -> Bool)+    , prim "||" (||)+    , prim "dec" (subtract 1 :: Int -> Int)+    , prim "tail" (tail :: [A] -> [A])     ]    -- take n xs = if n==0 || null xs then [] else head xs : take (dec n) (tail xs)   -- needs size 16   conjureWithMaxSize 16 "take" (take' :: Int -> [A] -> [A])-    [ val (0 :: Int)-    , val ([] :: [A])-    , value "null" (null :: [A] -> Bool)-    , value "==" ((==) :: Int -> Int -> Bool)-    , value "||" ((||) :: Bool -> Bool -> Bool)-    , value "dec" ((\n -> n-1) :: Int -> Int)-    , value ":" ((:) :: A -> [A] -> [A])-    , value "head" (head :: [A] -> A)-    , value "tail" (tail :: [A] -> [A])+    [ pr (0 :: Int)+    , pr ([] :: [A])+    , prim "null" (null :: [A] -> Bool)+    , prim "==" ((==) :: Int -> Int -> Bool)+    , prim "||" ((||) :: Bool -> Bool -> Bool)+    , prim "dec" ((\n -> n-1) :: Int -> Int)+    , prim ":" ((:) :: A -> [A] -> [A])+    , prim "head" (head :: [A] -> A)+    , prim "tail" (tail :: [A] -> [A])     ]

@@ -1,5 +1,6 @@ drop :: Int -> [A] -> [A] -- testing 60 combinations of argument values+-- pruning with 16/22 rules -- looking through 1 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 1 candidates of size 3@@ -17,6 +18,7 @@  take :: Int -> [A] -> [A] -- testing 60 combinations of argument values+-- pruning with 20/26 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 2 candidates of size 3

@@ -2,6 +2,19 @@ ============================  +v0.4.0+------++* background primitives are now provided with `pr` and `prim`.+* report number of rules used in pruning+* require Express v1.0.4 and Speculate v0.4.12+* allow `..` notation+* add benchmarks, replicate, subset, p12, p30 and candidates+* add and use the `Defn` type and `conjureDefns`+* minor changes in benchmarks+* cleanup unused code++ v0.3.6 ------ 

@@ -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.3.6+version:             0.4.0 synopsis:            conjure Haskell functions out of partial definitions description:   Conjure is a tool that produces Haskell functions out of partial definitions.@@ -28,6 +28,7 @@ extra-source-files: .gitignore                   , .github/workflows/build.yml                   , Makefile+                  , bench/bench                   , bench/*.hs                   , bench/*.out                   , eg/*.hs@@ -65,28 +66,37 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/conjure-  tag:             v0.3.6+  tag:             v0.4.0  library   exposed-modules: Conjure                  , Conjure.Conjurable                  , Conjure.Engine                  , Conjure.Expr+                 , Conjure.Prim                  , Conjure.Spec                  , Conjure.Utils-                 , Conjure.Cases+                 , Conjure.Defn   other-extensions: TemplateHaskell, CPP   build-depends: base >= 4 && < 5                , leancheck >= 0.9.10                , template-haskell-               , speculate >= 0.4.8-               , express >= 0.1.14+               , speculate >= 0.4.12+               , express >= 1.0.4   hs-source-dirs:      src   default-language:    Haskell2010  test-suite expr   type:                exitcode-stdio-1.0   main-is:             expr.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++test-suite defn+  type:                exitcode-stdio-1.0+  main-is:             defn.hs   other-modules:       Test, Test.ListableExpr, Test.Candidates   hs-source-dirs:      test   build-depends:       base >= 4 && < 5, leancheck, express, speculate, code-conjure

@@ -33,10 +33,10 @@   conjure "square" square primitives   conjure "tnpo"   tnpo   primitives -primitives :: [Expr]+primitives :: [Prim] primitives =-  [ val (0::Int)-  , val (1::Int)-  , value "+" ((+) :: Int -> Int -> Int)-  , value "*" ((*) :: Int -> Int -> Int)+  [ pr (0::Int)+  , pr (1::Int)+  , prim "+" ((+) :: Int -> Int -> Int)+  , prim "*" ((*) :: Int -> Int -> Int)   ]

@@ -1,5 +1,6 @@ double :: Int -> Int -- testing 4 combinations of argument values+-- pruning with 14/25 rules -- looking through 3 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 5 candidates of size 3@@ -7,6 +8,7 @@  add :: Int -> Int -> Int -- testing 4 combinations of argument values+-- pruning with 14/25 rules -- looking through 4 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 13 candidates of size 3@@ -14,6 +16,7 @@  square :: Int -> Int -- testing 3 combinations of argument values+-- pruning with 14/25 rules -- looking through 3 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 5 candidates of size 3@@ -21,6 +24,7 @@  tnpo :: Int -> Int -- testing 3 combinations of argument values+-- pruning with 14/25 rules -- looking through 3 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 5 candidates of size 3

@@ -23,21 +23,21 @@   conjure "and" (and' :: [Bool] -> Bool) primitivesWithFold   conjure "or"  (or'  :: [Bool] -> Bool) primitivesWithFold -primitives :: [Expr]+primitives :: [Prim] primitives =-  [ val False-  , val True-  , value "not" not-  , value "||" (||)-  , value "&&" (&&)-  , value "null" (null :: [Bool] -> Bool)-  , value "head" (head :: [Bool] -> Bool)-  , value "tail" (tail :: [Bool] -> [Bool])+  [ pr False+  , pr True+  , prim "not" not+  , prim "||" (||)+  , prim "&&" (&&)+  , prim "null" (null :: [Bool] -> Bool)+  , prim "head" (head :: [Bool] -> Bool)+  , prim "tail" (tail :: [Bool] -> [Bool])   ] -primitivesWithFold :: [Expr]+primitivesWithFold :: [Prim] primitivesWithFold  =-    value "foldr" (foldr :: (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool)+    prim "foldr" (foldr :: (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool)   : primitives  -- target (for and):

@@ -1,5 +1,6 @@ and :: [Bool] -> Bool -- testing 14 combinations of argument values+-- pruning with 37/47 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 4 candidates of size 3@@ -13,6 +14,7 @@  or :: [Bool] -> Bool -- testing 14 combinations of argument values+-- pruning with 37/47 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 4 candidates of size 3@@ -22,11 +24,12 @@ -- looking through 45 candidates of size 7 -- looking through 80 candidates of size 8 -- looking through 172 candidates of size 9--- looking through 454 candidates of size 10+-- looking through 462 candidates of size 10 or ps  =  not (null ps) && (head ps || or (tail ps))  and :: [Bool] -> Bool -- testing 14 combinations of argument values+-- pruning with 40/50 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 4 candidates of size 3@@ -35,6 +38,7 @@  or :: [Bool] -> Bool -- testing 14 combinations of argument values+-- pruning with 40/50 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 4 candidates of size 3

@@ -31,13 +31,21 @@  main :: IO () main = do+  -- count x xs  =  length (filter (== x) xs)+  --                1       2       3  4  5+  conjure "count" count'+    [ prim "length" (length :: [A] -> Int)+    , prim "filter" (filter :: (A -> Bool) -> [A] -> [A])+    , prim "==" ((==) :: A -> A -> Bool)+    ]+   conjureWithMaxSize 16 "count" count'-    [ val (0 :: Int)-    , val (1 :: Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "head" (head :: [A] -> A)-    , value "tail" (tail :: [A] -> [A])-    , value "null" (null :: [A] -> Bool)-    , value "==" ((==) :: A -> A -> Bool)-    , value "if" (\p x y -> if p then x else y :: Int)+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "head" (head :: [A] -> A)+    , prim "tail" (tail :: [A] -> [A])+    , prim "null" (null :: [A] -> Bool)+    , prim "==" ((==) :: A -> A -> Bool)+    , prim "if" (\p x y -> if p then x else y :: Int)     ]

@@ -1,5 +1,16 @@ count :: A -> [A] -> Int -- testing 13 combinations of argument values+-- pruning with 1/2 rules+-- looking through 0 candidates of size 1+-- looking through 1 candidates of size 2+-- looking through 0 candidates of size 3+-- looking through 0 candidates of size 4+-- looking through 1 candidates of size 5+count x xs  =  length (filter (x ==) xs)++count :: A -> [A] -> Int+-- testing 13 combinations of argument values+-- pruning with 8/13 rules -- looking through 2 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 1 candidates of size 3@@ -14,7 +25,7 @@ -- looking through 448 candidates of size 12 -- looking through 1145 candidates of size 13 -- looking through 2144 candidates of size 14--- looking through 5212 candidates of size 15--- looking through 10296 candidates of size 16+-- looking through 5216 candidates of size 15+-- looking through 10320 candidates of size 16 count x xs  =  if null xs then 0 else (if head xs == x then 1 else 0) + count x (tail xs) 

@@ -17,19 +17,20 @@ main  =  do   -- using enumFromTo   conjure "factorial n" factorial-    [ val (1::Int)-    , value "enumFromTo" (enumFromTo :: Int -> Int -> [Int])-    , value "product" (product :: [Int] -> Int)+    [ pr (1::Int)+    , prim ".." (enumFromTo :: Int -> Int -> [Int])+    , prim "*" ((*) :: Int -> Int -> Int)+    , prim "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)     ]    -- explicit recursion   conjure "factorial n" factorial-    [ val (0::Int)-    , val (1::Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "*" ((*) :: Int -> Int -> Int)-    , value "dec" (subtract 1 :: Int -> Int)-    , value "==" ((==) :: Int -> Int -> Bool)+    [ pr (0::Int)+    , pr (1::Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)+    , prim "dec" (subtract 1 :: Int -> Int)+    , prim "==" ((==) :: Int -> Int -> Bool)     ]  -- the actual factorial function:@@ -60,9 +61,9 @@    -- using a paramorphism   conjure "factorial n" factorial-    [ val (1::Int)-    , value "para" (para :: (Int->Int->Int) -> Int -> Int -> Int)-    , value "*" ((*) :: Int -> Int -> Int)+    [ pr (1::Int)+    , prim "para" (para :: (Int->Int->Int) -> Int -> Int -> Int)+    , prim "*" ((*) :: Int -> Int -> Int)     ]  

@@ -1,13 +1,17 @@ factorial :: Int -> Int -- testing 6 combinations of argument values+-- pruning with 4/8 rules -- looking through 2 candidates of size 1 -- looking through 0 candidates of size 2--- looking through 0 candidates of size 3--- looking through 2 candidates of size 4-factorial n  =  product (enumFromTo 1 n)+-- looking through 1 candidates of size 3+-- looking through 0 candidates of size 4+-- looking through 1 candidates of size 5+-- looking through 8 candidates of size 6+factorial n  =  foldr (*) 1 [1..n]  factorial :: Int -> Int -- testing 6 combinations of argument values+-- pruning with 40/73 rules -- looking through 3 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 5 candidates of size 3

@@ -22,25 +22,25 @@ fib01 0 1 7  =  21  as :: Args-as  =  args{maxSize=13,maxBodyRecursions=2}+as  =  args{maxSize=13}  main :: IO () main  =  do-  conjureWith as "fibonacci n" fibonacci-    [ val (1::Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "dec" (subtract 1 :: Int -> Int)-    , value "<=" ((<=) :: Int -> Int -> Bool)+  conjureWithMaxSize 13 "fibonacci n" fibonacci+    [ pr (1::Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "dec" (subtract 1 :: Int -> Int)+    , prim "<=" ((<=) :: Int -> Int -> Bool)     ] -- expected function: -- fibonacci n  =  if n <= 1 then 1 else fibonacci (dec n) + fibonacci (dec (dec n)) --                 1  2 3  4      5      6          7   8  9        10  11   12  13 -  conjureWithMaxSize 12 "fib01" fib01-    [ val (0::Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "dec" (subtract 1 :: Int -> Int)-    , value "<=" ((<=) :: Int -> Int -> Bool)+  conjure "fib01" fib01+    [ pr (0::Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "dec" (subtract 1 :: Int -> Int)+    , prim "<=" ((<=) :: Int -> Int -> Bool)     ] -- expected function: -- fib01 x y z  =  if z <= 0 then y else fib01 y (x + y) (dec z)

@@ -1,5 +1,6 @@ fibonacci :: Int -> Int -- testing 8 combinations of argument values+-- pruning with 20/38 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 6 candidates of size 3@@ -12,11 +13,12 @@ -- looking through 172 candidates of size 10 -- looking through 519 candidates of size 11 -- looking through 1281 candidates of size 12--- looking through 3281 candidates of size 13+-- looking through 3289 candidates of size 13 fibonacci n  =  if n <= 1 then 1 else fibonacci (dec n) + fibonacci (dec (dec n))  fib01 :: Int -> Int -> Int -> Int -- testing 8 combinations of argument values+-- pruning with 18/37 rules -- looking through 4 candidates of size 1 -- looking through 4 candidates of size 2 -- looking through 9 candidates of size 3

@@ -19,9 +19,9 @@  main :: IO () main = conjureWith args{requireDescent=False} "gcd a b" gcd'-  [ val (0::Int)-  , value "`mod`" (mod :: Int -> Int -> Int)-  , value "==" ((==) :: Int -> Int -> Bool)+  [ pr (0::Int)+  , prim "`mod`" (mod :: Int -> Int -> Int)+  , prim "==" ((==) :: Int -> Int -> Bool)   ]   -- desired function:   -- gcd a b  =  if b == 0 then a else gcd b (a `mod` b)

@@ -1,5 +1,6 @@ gcd :: Int -> Int -> Int -- testing 11 combinations of argument values+-- pruning with 1/2 rules -- looking through 3 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 9 candidates of size 3

@@ -33,20 +33,20 @@   conjure "sum"     (sum'     :: [Int] -> Int) primitivesWithFold   conjure "product" (product' :: [Int] -> Int) primitivesWithFold -primitives :: [Expr]+primitives :: [Prim] 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])+  [ pr (0 :: Int)+  , pr (1 :: Int)+  , prim "+" ((+) :: Int -> Int -> Int)+  , prim "*" ((*) :: Int -> Int -> Int)+  , prim "null" (null :: [Int] -> Bool)+  , prim "head" (head :: [Int] -> Int)+  , prim "tail" (tail :: [Int] -> [Int])   ] -primitivesWithFold :: [Expr]+primitivesWithFold :: [Prim] primitivesWithFold  =-    value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)+    prim "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)   : primitives  -- sum xs      =  if null xs then 0 else head xs + sum (tail xs)

@@ -1,5 +1,6 @@ second :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -7,6 +8,7 @@  third :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -15,6 +17,7 @@  sum :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -29,6 +32,7 @@  product :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -43,6 +47,7 @@  sum :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 15/26 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -51,6 +56,7 @@  product :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 15/26 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3

@@ -42,90 +42,90 @@   -- length xs  =  if null xs then 0 else 1 + length (tail xs)   --               1  2    3       4      5 6 7       8    9   conjure "length" length'-    [ val (0 :: Int)-    , val (1 :: Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)     ]    -- reverse xs  =  if null xs then [] else reverse (tail xs) ++ [head xs]   --                1  2    3       4       5        6    7   8  9 10 11 12   -- needs size 11 with unit   conjure "reverse" reverse'-    [ val ([] :: [Int])-    , value "unit" ((:[]) :: Int -> [Int])-    , value "++" ((++) :: [Int] -> [Int] -> [Int])-    , value "head" (head :: [Int] -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)+    [ pr ([] :: [Int])+    , prim "unit" ((:[]) :: Int -> [Int])+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)     ]    -- sort xs  =  if null xs then [] else insert (head xs) (sort (tail xs))   --             1  2    3       4       5       6    7    8     9    10   conjure "sort" sort'-    [ val ([] :: [Int])-    , value "insert" (insert :: Int -> [Int] -> [Int])-    , value "head" (head :: [Int] -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)+    [ pr ([] :: [Int])+    , prim "insert" (insert :: Int -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)     ]    -- 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)+    [ pr ([] :: [Int])+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)     ]    -- now through fold   -- length xs  =  foldr (const (1 +)) 0 xs   conjure "length" length'-    [ val (0 :: Int)-    , val (1 :: Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)-    , value "const" (const :: (Int -> Int) -> Int -> (Int -> Int)) -- cheating?+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)+    , prim "const" (const :: (Int -> Int) -> Int -> (Int -> Int)) -- cheating?     ]    -- now through fold and some cheating   --  reverse xs  =  foldr (\x xs -> xs ++ [x]) [] xs   --  reverse xs  =  foldr (flip (++) . unit) [] xs   conjure "reverse" reverse'-    [ val ([] :: [Int])-    , value "unit" ((:[]) :: Int -> [Int])-    , value "++" ((++) :: [Int] -> [Int] -> [Int])-    , value "foldr" (foldr :: (Int->[Int]->[Int]) -> [Int] -> [Int] -> [Int])+    [ pr ([] :: [Int])+    , prim "unit" ((:[]) :: Int -> [Int])+    , prim "++" ((++) :: [Int] -> [Int] -> [Int])+    , prim "foldr" (foldr :: (Int->[Int]->[Int]) -> [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])+    , prim "flip" (flip :: ([Int]->[Int]->[Int]) -> [Int] -> [Int] -> [Int])+    , prim "." ((.) :: ([Int]->[Int]->[Int]) -> (Int->[Int]) -> Int -> [Int] -> [Int])     ]    -- 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])+    [ pr ([] :: [Int])+    , prim "insert" (insert :: Int -> [Int] -> [Int])+    , prim "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])+    [ pr ([] :: [Int])+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "foldr" (foldr :: (Int -> [Int] -> [Int]) -> [Int] -> [Int] -> [Int])     ]    -- intercalate   -- xs \/ ys  =  if null xs then ys else head xs : (ys \/ tail xs)   conjure "\\/" (\/)-    [ val ([] :: [Int])-    , value ":" ((:) :: Int -> [Int] -> [Int])-    , value "head" (head :: [Int] -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)+    [ pr ([] :: [Int])+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)     ]

@@ -1,5 +1,6 @@ length :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 4/8 rules -- looking through 2 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 1 candidates of size 3@@ -13,6 +14,7 @@  reverse :: [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 12/13 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 5 candidates of size 3@@ -28,6 +30,7 @@  sort :: [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 6/7 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 2 candidates of size 3@@ -42,6 +45,7 @@  (++) :: [Int] -> [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 4/4 rules -- looking through 3 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 3 candidates of size 3@@ -57,6 +61,7 @@  length :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 6/10 rules -- looking through 2 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 1 candidates of size 3@@ -67,6 +72,7 @@  reverse :: [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 6/6 rules -- looking through 2 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 1 candidates of size 3@@ -78,6 +84,7 @@  sort :: [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 1/2 rules -- looking through 2 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 0 candidates of size 3@@ -86,6 +93,7 @@  (++) :: [Int] -> [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 2/2 rules -- looking through 3 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 0 candidates of size 3@@ -94,6 +102,7 @@  (\/) :: [Int] -> [Int] -> [Int] -- testing 60 combinations of argument values+-- pruning with 4/4 rules -- looking through 3 candidates of size 1 -- looking through 3 candidates of size 2 -- looking through 3 candidates of size 3

@@ -0,0 +1,62 @@+-- replicate.hs: replicate and other functions+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure+import Data.List (transpose)++replicate' :: Int -> Char -> String+replicate' 0 c  =  []+replicate' 1 c  =  [c]+replicate' 2 c  =  [c,c]+replicate' 3 c  =  [c,c,c]+replicate' 4 c  =  [c,c,c,c]++-- this function is one of the examples of MagicHaskeller+replicates' :: String -> Int -> String+replicates' [a]     1  =  [a]+replicates' [a,b]   1  =  [a,b]+replicates' [a]     2  =  [a,a]+replicates' [a,b]   2  =  [a,a,b,b]+replicates' [a,b,c] 2  =  [a,a,b,b,c,c]+replicates' [a]     3  =  [a,a,a]+replicates' [a,b]   3  =  [a,a,a,b,b,b]+replicates' [a,b,c] 3  =  [a,a,a,b,b,b,c,c,c]++main :: IO ()+main = do+  conjure "replicate" replicate'+    [ pr (0 :: Int)+    , prim "dec" (subtract 1 :: Int -> Int)+    , prim "==" ((==) :: Int -> Int -> Bool)+    , pr ""+    , prim ":" ((:) :: Char -> String -> String)+    ]++  -- emulates how MagicHaskeller generates "replicates"+  conjureWith args{maxTests=360} "replicates" replicates'+    [ prim "replicate" (replicate :: Int -> String -> [String])+    , prim "transpose" (transpose :: [[Char]] -> [[Char]])+    , prim "concat"    (concat :: [String] -> String)+    ]++  -- emulates an alternative generation that works on MagicHaskeller+  conjureWith args{maxTests=360} "replicates" replicates'+    [ prim "replicate" (replicate :: Int -> Char -> String)+    , prim "map"       (map :: (Char -> String) -> String -> [String])+    , prim "concat"    (concat :: [String] -> String)+    ]++  -- alternative generation using recursion+  conjureWith args{maxTests=360, maxSize=13} "replicates" replicates'+    [ pr ""+    , prim "null" (null :: String -> Bool)+    , prim "head" (head :: String -> Char)+    , prim "tail" (tail :: String -> String)+    , prim ":" ((:) :: Char -> String -> String)+    , prim "++" ((++) :: String -> String -> String)+    , prim "replicate" (replicate :: Int -> Char -> String)+    ]++replicates n []  =  []+replicates n (x:xs)  =  replicate n x ++ replicates n xs

@@ -0,0 +1,54 @@+replicate :: Int -> Char -> [Char]+-- testing 60 combinations of argument values+-- pruning with 6/7 rules+-- looking through 1 candidates of size 1+-- looking through 0 candidates of size 2+-- looking through 1 candidates of size 3+-- looking through 0 candidates of size 4+-- looking through 1 candidates of size 5+-- looking through 0 candidates of size 6+-- looking through 1 candidates of size 7+-- looking through 0 candidates of size 8+-- looking through 3 candidates of size 9+-- looking through 4 candidates of size 10+-- looking through 11 candidates of size 11+replicate x c  =  if x == 0 then "" else c:replicate (dec x) c++replicates :: [Char] -> Int -> [Char]+-- testing 360 combinations of argument values+-- pruning with 2/2 rules+-- looking through 1 candidates of size 1+-- looking through 0 candidates of size 2+-- looking through 0 candidates of size 3+-- looking through 1 candidates of size 4+-- looking through 1 candidates of size 5+replicates cs x  =  concat (transpose (replicate x cs))++replicates :: [Char] -> Int -> [Char]+-- testing 360 combinations of argument values+-- pruning with 0/0 rules+-- looking through 1 candidates of size 1+-- looking through 0 candidates of size 2+-- looking through 0 candidates of size 3+-- looking through 0 candidates of size 4+-- looking through 1 candidates of size 5+replicates cs x  =  concat (map (replicate x) cs)++replicates :: [Char] -> Int -> [Char]+-- testing 360 combinations of argument values+-- pruning with 9/14 rules+-- looking through 2 candidates of size 1+-- looking through 2 candidates of size 2+-- looking through 3 candidates of size 3+-- looking through 13 candidates of size 4+-- looking through 28 candidates of size 5+-- looking through 67 candidates of size 6+-- looking through 197 candidates of size 7+-- looking through 523 candidates of size 8+-- looking through 1430 candidates of size 9+-- looking through 4072 candidates of size 10+-- looking through 11488 candidates of size 11+-- looking through 32782 candidates of size 12+-- looking through 94734 candidates of size 13+replicates cs x  =  if null cs then cs else replicate x (head cs) ++ replicates (tail cs) x+

@@ -17,31 +17,31 @@   -- elem x xs  =  not (null xs) && (elem x (tail xs) || x == head xs)   --               1    2    3    4  5    6   7   8   9  10 11 12  13   conjureWithMaxSize 13 "elem" (elem')-    [ val ([] :: [Int])-    , val True-    , val False-    , value "||" (||)-    , value "&&" (&&)-    , value "not" not-    , value ":" ((:) :: Int -> [Int] -> [Int])-    , value "head" (head :: [Int] -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)-    , value "==" ((==) :: Int -> Int -> Bool)+    [ pr ([] :: [Int])+    , pr True+    , pr False+    , prim "||" (||)+    , prim "&&" (&&)+    , prim "not" not+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)+    , prim "==" ((==) :: Int -> Int -> Bool)     ]    -- set xs  =  null xs || set (tail xs) && not (elem (head xs) (tail xs))   --            1    2  3  4    5    6    7  8    9    10   11   12   13   conjureWithMaxSize 13 "set" (set')-    [ val ([] :: [Int])-    , val True-    , val False-    , value "&&" (&&)-    , value "||" (||)-    , value "not" not-    , value ":" ((:) :: Int -> [Int] -> [Int])-    , value "head" (head :: [Int] -> Int)-    , value "tail" (tail :: [Int] -> [Int])-    , value "null" (null :: [Int] -> Bool)-    , value "elem" (elem :: Int -> [Int] -> Bool)+    [ pr ([] :: [Int])+    , pr True+    , pr False+    , prim "&&" (&&)+    , prim "||" (||)+    , prim "not" not+    , prim ":" ((:) :: Int -> [Int] -> [Int])+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)+    , prim "elem" (elem :: Int -> [Int] -> Bool)     ]

@@ -1,5 +1,6 @@ elem :: Int -> [Int] -> Bool -- testing 60 combinations of argument values+-- pruning with 44/57 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 3 candidates of size 3@@ -11,12 +12,13 @@ -- looking through 332 candidates of size 9 -- looking through 747 candidates of size 10 -- looking through 1826 candidates of size 11--- looking through 4407 candidates of size 12--- looking through 10888 candidates of size 13+-- looking through 4411 candidates of size 12+-- looking through 10932 candidates of size 13 elem x xs  =  not (null xs) && (head xs == x || elem x (tail xs))  set :: [Int] -> Bool -- testing 60 combinations of argument values+-- pruning with 46/57 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 3 candidates of size 3@@ -26,9 +28,9 @@ -- looking through 64 candidates of size 7 -- looking through 145 candidates of size 8 -- looking through 310 candidates of size 9--- looking through 717 candidates of size 10--- looking through 1734 candidates of size 11--- looking through 4135 candidates of size 12--- looking through 9734 candidates of size 13+-- looking through 721 candidates of size 10+-- looking through 1762 candidates of size 11+-- looking through 4235 candidates of size 12+-- looking through 10038 candidates of size 13 set xs  =  null xs || not (elem (head xs) (tail xs)) && set (tail xs) 

@@ -15,13 +15,13 @@ -- hoping for something like -- sum xs  =  if null xs then 0 else head xs + sum (tail xs) -sumPrimitives :: [Expr]+sumPrimitives :: [Prim] sumPrimitives  =-  [ value "null" (null :: [Int] -> Bool)-  , val (0::Int)-  , value "+"    ((+) :: Int -> Int -> Int)-  , value "head" (head :: [Int] -> Int)-  , value "tail" (tail :: [Int] -> [Int])+  [ prim "null" (null :: [Int] -> Bool)+  , pr (0::Int)+  , prim "+"    ((+) :: Int -> Int -> Int)+  , prim "head" (head :: [Int] -> Int)+  , prim "tail" (tail :: [Int] -> [Int])   ]  @@ -35,12 +35,12 @@ -- hoping for something like -- app xs ys = if null xs then ys else head xs : app (tail xs) ys -appPrimitives :: [Expr]+appPrimitives :: [Prim] appPrimitives =-  [ value "null" (null :: [Int] -> Bool)-  , value ":"    ((:) :: Int -> [Int] -> [Int])-  , value "head" (head :: [Int] -> Int)-  , value "tail" (tail :: [Int] -> [Int])+  [ prim "null" (null :: [Int] -> Bool)+  , prim ":"    ((:) :: Int -> [Int] -> [Int])+  , prim "head" (head :: [Int] -> Int)+  , prim "tail" (tail :: [Int] -> [Int])   ]  

@@ -1,5 +1,6 @@ sum :: [Int] -> Int -- testing 3 combinations of argument values+-- pruning with 4/8 rules -- looking through 1 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 1 candidates of size 3@@ -14,6 +15,7 @@  (++) :: [Int] -> [Int] -> [Int] -- testing 3 combinations of argument values+-- pruning with 3/3 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 2 candidates of size 3

@@ -0,0 +1,60 @@+-- subset.hs: conjuring the subset function+--+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+{-# LANGUAGE CPP #-}+import Conjure+import Data.List (sort)++#if __GLASGOW_HASKELL__ >= 710+import Data.List (isSubsequenceOf)+#else+isSubsequenceOf :: Eq a => [a] -> [a] -> Bool+isSubsequenceOf []    _  = True+isSubsequenceOf (_:_) [] = False+isSubsequenceOf (x:xs) (y:ys)+  | x == y    =    xs  `isSubsequenceOf` ys+  | otherwise = (x:xs) `isSubsequenceOf` ys+#endif++subset' :: [Int] -> [Int] -> Bool+subset' [] [x]  =  True+subset' [x] []  =  False+subset' [0] [0]  =  True+subset' [1] [1]  =  True+subset' [0] [1]  =  False+subset' [1] [0]  =  False+subset' [0] [0,1]  =  True+subset' [1] [0,1]  =  True+subset' [0] [1,0]  =  True+subset' [1] [1,0]  =  True+subset' [2] [0,1]  =  False+subset' [2] [1,0]  =  False+subset' [0,1] [0]  =  False+subset' [0,1] [1]  =  False+subset' [0,1] [0,1]  =  True+subset' [0,1] [1,0]  =  True+subset' [1,0] [0,1]  =  True+subset' [1,0] [1,0]  =  True+subset' [0,1,2] [0,1,2]  =  True+subset' [0,1,2,3] [0,1,2,3]  =  True++main :: IO ()+main = do+  -- subset xs ys  =  null xs || elem (head xs) ys && subset (tail xs) ys+  --                  1    2  3  4     5    6   7  8  9       10   11  12+  conjure "subset" (subset')+    [ pr ([] :: [Int])+    , prim "&&" (&&)+    , prim "||" (||)+    , prim "head" (head :: [Int] -> Int)+    , prim "tail" (tail :: [Int] -> [Int])+    , prim "null" (null :: [Int] -> Bool)+    , prim "elem" (elem :: Int -> [Int] -> Bool)+    ]++  -- subset xs ys  =  sort xs `isSubsequenceOf` sort ys+  conjureWith args{maxTests=360} "subset" (subset')+    [ prim "sort" (sort :: [Int] -> [Int])+    , prim "`isSubsequenceOf`" (isSubsequenceOf :: [Int] -> [Int] -> Bool)+    ]

@@ -0,0 +1,27 @@+subset :: [Int] -> [Int] -> Bool+-- testing 44 combinations of argument values+-- pruning with 30/40 rules+-- looking through 0 candidates of size 1+-- looking through 2 candidates of size 2+-- looking through 3 candidates of size 3+-- looking through 9 candidates of size 4+-- looking through 22 candidates of size 5+-- looking through 47 candidates of size 6+-- looking through 132 candidates of size 7+-- looking through 323 candidates of size 8+-- looking through 854 candidates of size 9+-- looking through 2421 candidates of size 10+-- looking through 6452 candidates of size 11+-- looking through 17815 candidates of size 12+subset xs ys  =  null xs || elem (head xs) ys && subset (tail xs) ys++subset :: [Int] -> [Int] -> Bool+-- testing 44 combinations of argument values+-- pruning with 3/3 rules+-- looking through 0 candidates of size 1+-- looking through 0 candidates of size 2+-- looking through 2 candidates of size 3+-- looking through 6 candidates of size 4+-- looking through 2 candidates of size 5+subset xs ys  =  sort xs `isSubsequenceOf` sort ys+

@@ -25,41 +25,41 @@   conjure "product" product' primitives   conjure "product" product' primitivesWithFold -primitives :: [Expr]+primitives :: [Prim] primitives =-  [ val (0 :: Int)-  , val (1 :: Int)+  [ pr (0 :: Int)+  , pr (1 :: Int) #if __GLASGOW_HASKELL__ < 800-  , value "+" ((+) :: Int -> Int -> Int)-  , value "*" ((*) :: Int -> Int -> Int)-  , value "null" (null :: [Int] -> Bool)-  , value "head" (head :: [Int] -> Int)-  , value "tail" (tail :: [Int] -> [Int])+  , prim "+" ((+) :: Int -> Int -> Int)+  , prim "*" ((*) :: Int -> Int -> Int)+  , prim "null" (null :: [Int] -> Bool)+  , prim "head" (head :: [Int] -> Int)+  , prim "tail" (tail :: [Int] -> [Int]) #else-  , value "+" ((+) @Int)-  , value "*" ((*) @Int)+  , prim "+" ((+) @Int)+  , prim "*" ((*) @Int) -- the following #if was added just for dramatic effect (see notes below) #if __GLASGOW_HASKELL__ < 710-  , value "null" (null @Int)+  , prim "null" (null @Int) #else-  , value "null" (null @[] @Int)+  , prim "null" (null @[] @Int) #endif-  , value "head" (head @Int)-  , value "tail" (tail @Int)+  , prim "head" (head @Int)+  , prim "tail" (tail @Int) #endif   ] -primitivesWithFold :: [Expr]+primitivesWithFold :: [Prim] #if __GLASGOW_HASKELL__ < 800 primitivesWithFold  =-    value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)+    prim "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int)   : primitives #else -- the following #if was added just for dramatic effect (see notes below) #if __GLASGOW_HASKELL__ < 710-primitivesWithFold  =  value "foldr" (foldr @Int @Int) : primitives+primitivesWithFold  =  prim "foldr" (foldr @Int @Int) : primitives #else-primitivesWithFold  =  value "foldr" (foldr @[] @Int @Int) : primitives+primitivesWithFold  =  prim "foldr" (foldr @[] @Int @Int) : primitives #endif #endif 

@@ -1,5 +1,6 @@ third :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -8,6 +9,7 @@  product :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 14/25 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -22,6 +24,7 @@  product :: [Int] -> Int -- testing 60 combinations of argument values+-- pruning with 15/26 rules -- looking through 2 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3

@@ -2,7 +2,7 @@ -- -- Copyright (C) 2021 Rudy Matela -- Distributed under the 3-Clause BSD licence (see the file LICENSE).-{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP, TemplateHaskell #-} #if __GLASGOW_HASKELL__ == 708 {-# LANGUAGE DeriveDataTypeable, StandaloneDeriving #-} import Data.Typeable (Typeable)@@ -10,7 +10,13 @@  import Conjure import Test.LeanCheck+import Data.Express hiding (height,size) +-- TODO: remove the following import+-- and fix build on GHC 7.10 and 7.8+-- the generation fo -: and ->>>: somehow fails.+import Test.LeanCheck.Utils+ data Tree  =  Leaf            |  Node Tree Int Tree   deriving (Eq, Ord, Show, Read)@@ -19,6 +25,8 @@ deriving instance Typeable Tree #endif +deriveExpress ''Tree+ unit :: Int -> Tree unit x  =  Node Leaf x Leaf @@ -70,70 +78,76 @@         \/  cons3 Node  instance Conjurable Tree where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers   conjureSubTypes x  =  conjureType (undefined :: Int)+  conjureCases t  =  [ val (Leaf -: t)+                     , value "Node" (Node ->>>: t) :$ hole l :$ hole x :$ hole r+                     ]+    where+    Node l x r  =  Node undefined undefined undefined -: t   main :: IO () main = do   conjure "leftmost" leftmost-    [ value "valu" valu-    , value "nil" nil-    , value "left" left-    , value "right" right+    [ prim "valu" valu+    , prim "nil" nil+    , prim "left" left+    , prim "right" right     ]    conjure "rightmost" rightmost-    [ value "valu" valu-    , value "nil" nil-    , value "left" left-    , value "right" right+    [ prim "valu" valu+    , prim "nil" nil+    , prim "left" left+    , prim "right" right     ] -  conjureWith args{maxBodyRecursions=2, maxSize=13} "size" size-    [ val (0 :: Int)-    , val (1 :: Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "nil" nil-    , value "left" left-    , value "right" right+  conjureWithMaxSize 13 "size" size+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "nil" nil+    , prim "left" left+    , prim "right" right     ] -  conjureWith args{maxBodyRecursions=2, maxSize=13} "height" height-    [ val (0 :: Int)-    , val (1 :: Int)-    , val (-1 :: Int)-    , value "+" ((+) :: Int -> Int -> Int)-    , value "max" (max :: Int -> Int -> Int)-    , value "nil" nil-    , value "left" left-    , value "right" right+  conjureWithMaxSize 13 "height" height+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , pr (-1 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "max" (max :: Int -> Int -> Int)+    , prim "nil" nil+    , prim "left" left+    , prim "right" right     ]    -- out of reach performance-wise-  conjureWith args{maxBodyRecursions=2, maxSize=12} "mem" mem-    [ val False-    , value "||" (||)-    , value "==" ((==) :: Int -> Int -> Bool)-    , value "nil" nil-    , value "left" left-    , value "right" right-    , value "valu" valu+  conjure "mem" mem+    [ pr False+    , prim "||" (||)+    , prim "==" ((==) :: Int -> Int -> Bool)+    , prim "nil" nil+    , prim "left" left+    , prim "right" right+    , prim "valu" valu     ]    -- simply out of reach performance-wise (size 34)-  conjureWith args{maxBodyRecursions=2, maxSize=9} "insert" mem-    [ val Leaf-    , value "Node" Node-    , value "left" left-    , value "right" right-    , value "valu" valu-    , value "nil" nil-    , value "unit" unit-    , value "==" ((==) :: Int -> Int -> Bool)-    , value "<" ((<) :: Int -> Int -> Bool)-    , value ">" ((>) :: Int -> Int -> Bool)+  conjureWithMaxSize 9 "insert" mem+    [ pr Leaf+    , prim "Node" Node+    , prim "left" left+    , prim "right" right+    , prim "valu" valu+    , prim "nil" nil+    , prim "unit" unit+    , prim "==" ((==) :: Int -> Int -> Bool)+    , prim "<" ((<) :: Int -> Int -> Bool)+    , prim ">" ((>) :: Int -> Int -> Bool)     ]  

@@ -1,5 +1,6 @@ leftmost :: Tree -> Int -- testing 60 combinations of argument values+-- pruning with 0/0 rules -- looking through 0 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -13,6 +14,7 @@  rightmost :: Tree -> Int -- testing 60 combinations of argument values+-- pruning with 0/0 rules -- looking through 0 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -26,6 +28,7 @@  size :: Tree -> Int -- testing 60 combinations of argument values+-- pruning with 4/8 rules -- looking through 2 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 1 candidates of size 3@@ -43,6 +46,7 @@  height :: Tree -> Int -- testing 60 combinations of argument values+-- pruning with 49/65 rules -- looking through 3 candidates of size 1 -- looking through 0 candidates of size 2 -- looking through 2 candidates of size 3@@ -53,13 +57,14 @@ -- looking through 48 candidates of size 8 -- looking through 299 candidates of size 9 -- looking through 896 candidates of size 10--- looking through 3113 candidates of size 11--- looking through 8528 candidates of size 12--- looking through 24896 candidates of size 13-cannot conjure+-- looking through 3137 candidates of size 11+-- looking through 8672 candidates of size 12+-- looking through 26088 candidates of size 13+height x  =  if nil x then -1 else 1 + max (height (left x)) (height (right x))  mem :: Int -> Tree -> Bool -- testing 60 combinations of argument values+-- pruning with 11/17 rules -- looking through 1 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 2 candidates of size 3@@ -71,11 +76,12 @@ -- looking through 376 candidates of size 9 -- looking through 930 candidates of size 10 -- looking through 2302 candidates of size 11--- looking through 5752 candidates of size 12+-- looking through 5760 candidates of size 12 cannot conjure  insert :: Int -> Tree -> Bool -- testing 60 combinations of argument values+-- pruning with 9/10 rules -- looking through 0 candidates of size 1 -- looking through 1 candidates of size 2 -- looking through 4 candidates of size 3

@@ -2,3 +2,4 @@ module Toplibs () where  import Conjure ()+import Test ()

@@ -1,14 +1,33 @@+bench/avgs: \+  bench/avgs.hs \+  mk/toplibs+bench/avgs.o: \+  bench/avgs.hs+bench/candidates: \+  bench/candidates.hs \+  mk/toplibs+bench/candidates.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  bench/candidates.hs bench/ill-hit: \   bench/ill-hit.hs \   mk/toplibs bench/ill-hit.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   bench/ill-hit.hs bench/longshot: \   bench/longshot.hs \@@ -16,23 +35,51 @@ bench/longshot.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   bench/longshot.hs+bench/p12: \+  bench/p12.hs \+  mk/toplibs+bench/p12.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  bench/p12.hs+bench/p30: \+  bench/p30.hs \+  mk/toplibs+bench/p30.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  bench/p30.hs bench/self: \   bench/self.hs \   mk/toplibs bench/self.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   bench/self.hs bench/take-drop: \   bench/take-drop.hs \@@ -40,11 +87,12 @@ bench/take-drop.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   bench/take-drop.hs eg/arith: \   eg/arith.hs \@@ -52,11 +100,12 @@ eg/arith.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/arith.hs eg/bools: \   eg/bools.hs \@@ -64,11 +113,12 @@ eg/bools.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/bools.hs eg/count: \   eg/count.hs \@@ -76,11 +126,12 @@ eg/count.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/count.hs eg/factorial: \   eg/factorial.hs \@@ -88,11 +139,12 @@ eg/factorial.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/factorial.hs eg/fibonacci: \   eg/fibonacci.hs \@@ -100,11 +152,12 @@ eg/fibonacci.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/fibonacci.hs eg/gcd: \   eg/gcd.hs \@@ -112,11 +165,12 @@ eg/gcd.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/gcd.hs eg/ints: \   eg/ints.hs \@@ -124,11 +178,12 @@ eg/ints.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/ints.hs eg/list: \   eg/list.hs \@@ -136,23 +191,38 @@ eg/list.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/list.hs+eg/replicate: \+  eg/replicate.hs \+  mk/toplibs+eg/replicate.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  eg/replicate.hs eg/setelem: \   eg/setelem.hs \   mk/toplibs eg/setelem.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/setelem.hs eg/spec: \   eg/spec.hs \@@ -160,23 +230,38 @@ eg/spec.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/spec.hs+eg/subset: \+  eg/subset.hs \+  mk/toplibs+eg/subset.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  eg/subset.hs eg/tapps: \   eg/tapps.hs \   mk/toplibs eg/tapps.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/tapps.hs eg/tree: \   eg/tree.hs \@@ -184,67 +269,83 @@ eg/tree.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   eg/tree.hs mk/All.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   mk/All.hs mk/Toplibs.o: \+  test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \   src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs \   mk/Toplibs.hs proto/u-conjure.o: \   proto/u-conjure.hs proto/u-conjure: \   proto/u-conjure.hs \   mk/toplibs-src/Conjure/Cases.o: \-  src/Conjure/Utils.hs \-  src/Conjure/Cases.hs src/Conjure/Conjurable.o: \   src/Conjure/Utils.hs \   src/Conjure/Expr.hs \-  src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs+src/Conjure/Defn.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Defn.hs src/Conjure/Engine.o: \   src/Conjure/Utils.hs \+  src/Conjure/Prim.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \-  src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs src/Conjure/Expr.o: \   src/Conjure/Utils.hs \   src/Conjure/Expr.hs src/Conjure.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \-  src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs+src/Conjure/Prim.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Prim.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs src/Conjure/Spec.o: \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \-  src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs src/Conjure/Utils.o: \   src/Conjure/Utils.hs test/conjurable.o: \@@ -254,17 +355,37 @@   test/conjurable.hs \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \-  src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs test/conjurable: \   test/Test.hs \   test/Test/ListableExpr.hs \   test/Test/Candidates.hs \   test/conjurable.hs \   mk/toplibs+test/defn.o: \+  test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \+  test/defn.hs \+  src/Conjure/Utils.hs \+  src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs+test/defn: \+  test/Test.hs \+  test/Test/ListableExpr.hs \+  test/Test/Candidates.hs \+  test/defn.hs \+  mk/toplibs test/expr.o: \   test/Test.hs \   test/Test/ListableExpr.hs \@@ -272,11 +393,12 @@   test/expr.hs \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \-  src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs test/expr: \   test/Test.hs \   test/Test/ListableExpr.hs \@@ -295,11 +417,12 @@   test/Test/Candidates.hs \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \-  src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs test/Test: \   test/Test.hs \   test/Test/ListableExpr.hs \@@ -312,11 +435,12 @@   test/Test/Candidates.hs \   src/Conjure/Utils.hs \   src/Conjure/Spec.hs \+  src/Conjure/Prim.hs \   src/Conjure.hs \   src/Conjure/Expr.hs \   src/Conjure/Engine.hs \-  src/Conjure/Conjurable.hs \-  src/Conjure/Cases.hs+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs test/utils: \   test/utils.hs \   test/Test.hs \

@@ -21,12 +21,12 @@ -- -- Step 2: declare a list with the potential building blocks: ----- > primitives :: [Expr]+-- > primitives :: [Prim] -- > primitives =--- >   [ val (0::Int)--- >   , val (1::Int)--- >   , value "+" ((+) :: Int -> Int -> Int)--- >   , value "*" ((*) :: Int -> Int -> Int)+-- >   [ pr (0::Int)+-- >   , pr (1::Int)+-- >   , prim "+" ((+) :: Int -> Int -> Int)+-- >   , prim "*" ((*) :: Int -> Int -> Int) -- > ] -- -- Step 3: call conjure and see your generated function:@@ -43,15 +43,18 @@   ( -- * Basic use     conjure-  , val-  , value-  , Expr+  , Prim+  , pr+  , prim  -- * Advanced use   , conjureWithMaxSize   , conjureWith   , Args(..)   , args+  , Expr+  , val+  , value  -- * Conjuring from a specification   , Spec1@@ -66,8 +69,10 @@   , conjure3With  -- * When using custom types-  , Conjurable (conjureEquality, conjureTiers, conjureSubTypes)-  , reifyEquality, reifyTiers+  , Conjurable (conjureExpress, conjureEquality, conjureTiers, conjureCases, conjureSubTypes)+  , reifyExpress+  , reifyEquality+  , reifyTiers   , conjureType  -- * Pure interfaces@@ -82,3 +87,4 @@ import Conjure.Engine import Conjure.Spec import Conjure.Conjurable+import Conjure.Prim

@@ -1,122 +0,0 @@--- |--- Module      : Conjure.Cases--- Copyright   : (c) 2021 Rudy Matela--- License     : 3-Clause BSD  (see the file LICENSE)--- Maintainer  : Rudy Matela <rudy@matela.com.br>------ This module is part of 'Conjure'.------ This module defines the 'Cases' typeclass--- that allows listing cases of a type--- encoded as 'Expr's------ You are probably better off importing "Conjure".-{-# Language DeriveDataTypeable, StandaloneDeriving #-} -- for GHC < 7.10-module Conjure.Cases-  ( Cases (..)-  , Fxpr-  , sumFxpr-  , factFxpr-  , nullFxpr-  , isZeroFxpr-  )-where--import Conjure.Utils-import Data.Express-import Data.Express.Express-import Data.Express.Fixtures-import Data.Dynamic-import Data.Typeable (Typeable)--type Fxpr  =  (Expr, Cxpr)-type Cxpr  =  [([Expr],Expr)]--sumFxpr :: Fxpr-sumFxpr  =  var "sum" (undefined :: [Int] -> Int) =--  [ [nil]           =-  zero-  , [(xx -:- xxs)]  =-  xx -+- (var "recurse" (undefined :: [Int] -> Int) :$ xxs)-  ]-  where-  (=-) = (,)-  infixr 0 =---factFxpr :: Fxpr-factFxpr  =  error "TODO: write me"--nullFxpr :: Fxpr-nullFxpr  =  error "TODO" =--  [ [nil]          =- false-  , [(xx -:- xxs)] =- false-  ]-  where-  (=-) = (,)-  infixr 0 =---isZeroFxpr :: Fxpr-isZeroFxpr  =  error "TODO" =--  [ [zero]  =- true-  , [inc xx] =- false-  ]-  where-  inc = undefined -- TODO: define me-  (=-) = (,)-  infixr 0 =------ | Evaluates an 'Expr' using the given 'Fxpr' as definition---   when a recursive call is found.-fxprToDynamic :: Int -> Fxpr -> Expr -> Maybe Dynamic-fxprToDynamic  =  undefined---class Express a => Cases a where-  cases :: a -> [Expr]--instance Cases () where-  cases _  =  [val ()]--instance Cases Bool where-  cases _  =  [val False, val True]--instance Cases Int where-  cases x  =  [val (0 -: x), hole x]--instance Cases Integer where-  cases x  =  [val (0 -: x), hole x]--instance Cases Char where-  cases _  =  []--instance Express a => Cases [a] where-  cases xs  =  [ val ([] -: xs)-               , value ":" ((:) ->>: xs) :$ hole x :$ hole xs-               ]-    where-    x  =  head xs--instance (Express a, Express b) => Cases (a,b) where-  cases xy  =  [value "," ((,) ->>: xy) :$ hole x :$ hole y]-    where-    (x,y) = (undefined,undefined) -: xy--instance (Express a, Express b, Express c) => Cases (a,b,c) where-  cases xyz  =  [value ",," ((,,) ->>>: xyz) :$ hole x :$ hole y :$ hole z]-    where-    (x,y,z) = (undefined,undefined,undefined) -: xyz--instance Express a => Cases (Maybe a) where-  cases mx  =  [ value "Nothing" (Nothing -: mx)-               , value "Just" (Just ->: mx) :$ hole x-               ]-    where-    x  =  Just undefined -: mx---instance (Express a, Express b) => Cases (Either a b) where-  cases exy  =  [ value "Left" (Left ->: exy) :$ hole x-                , value "Right" (Right ->: exy) :$ hole y-                ]-    where-    x  =  Left undefined -: exy-    y  =  Right undefined -: exy

@@ -17,15 +17,19 @@   , conjureType   , reifyTiers   , reifyEquality+  , reifyExpress   , conjureApplication   , conjureVarApplication+  , conjurePats   , conjureHoles-  , conjureIfs   , conjureTiersFor   , conjureAreEqual   , conjureMkEquation   , A, B, C, D, E, F   , conjureIsDeconstructor+  , conjureIsUnbreakable+  , conjureReification+  , conjureReification1   ) where @@ -33,7 +37,7 @@ import Test.LeanCheck.Utils import Test.LeanCheck.Error (errorToFalse) import Conjure.Expr hiding (application)-import Conjure.Cases+import Conjure.Defn import Test.Speculate.Expr import Data.Functor ((<$>)) import Control.Applicative ((<*>))@@ -46,8 +50,8 @@  -- | Single reification of some functions over a type as 'Expr's. ----- A hole, an if function, an equality function and tiers.-type Reification1  =  (Expr, Expr, Maybe Expr, Maybe [[Expr]])+-- A hole, an equality function and tiers.+type Reification1  =  (Expr, Maybe Expr, Maybe [[Expr]], Bool)  -- | A reification over a collection of types. --@@ -55,6 +59,25 @@ type Reification  =  [Reification1] -> [Reification1]  +-- | A primtive expression (paired with instance reification).+type Prim  =  (Expr, Reification)+++-- | Provides a primitive value to Conjure.+--   To be used on 'Show' instances.+--   (cf. 'prim')+pr :: (Conjurable a, Show a) => a -> Prim+pr x  =  (val x, conjureType x)+++-- | Provides a primitive value to Conjure.+--   To be used on values that are not 'Show' instances+--   such as functions.+--   (cf. 'pr')+prim :: Conjurable a => String -> a -> Prim+prim s x  =  (value s x, conjureType x)++ -- | Class of 'Conjurable' types. -- Functions are 'Conjurable' -- if all their arguments are 'Conjurable', 'Listable' and 'Show'able.@@ -110,7 +133,15 @@   conjureIf :: a -> Expr   conjureIf   =  ifFor +  conjureCases :: a -> [Expr]+  conjureCases _  =  [] +  conjureArgumentCases :: a -> [[Expr]]+  conjureArgumentCases _  =  []++  conjureExpress :: a -> Expr -> Expr++ conjureType :: Conjurable a => a -> Reification conjureType x ms  =   if hole x `elem` [h | (h,_,_,_) <- ms]@@ -124,7 +155,7 @@ -- 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)+conjureReification1 x  =  (hole x, conjureEquality x, conjureTiers x, null $ conjureCases x)  conjureReification :: Conjurable a => a -> [Reification1] conjureReification x  =  nubConjureType x [conjureReification1 bool]@@ -158,19 +189,19 @@ reifyTiers :: (Listable a, Show a, Typeable a) => a -> Maybe [[Expr]] reifyTiers  =  Just . mkExprTiers +reifyExpress :: (Express a, Show a) => a -> Expr -> Expr+reifyExpress a e  =  case value "expr" (expr -:> a) $$ e of+  Nothing -> e         -- TODO: consider throwing an error+  Just e' -> eval e e' -- TODO: consider throwing an error+ mkExprTiers :: (Listable a, Show a, Typeable a) => a -> [[Expr]] mkExprTiers a  =  mapT val (tiers -: [[a]])  conjureHoles :: Conjurable f => f -> [Expr]-conjureHoles f  =  [eh | (eh,_,_,Just _) <- conjureReification f]--conjureIfs :: Conjurable f => f -> [Expr]-conjureIfs f  =  [eef | (_,eef,_,Just _) <- nubConjureType f []]--- this does not include if for bools automatically--- differently from conjureHoles, conjureMkEquation and conjureTiersFor+conjureHoles f  =  [eh | (eh,_,Just _,_) <- conjureReification f]  conjureMkEquation :: Conjurable f => f -> Expr -> Expr -> Expr-conjureMkEquation f  =  mkEquation [eq | (_,_,Just eq,_) <- conjureReification f]+conjureMkEquation f  =  mkEquation [eq | (_,Just eq,_,_) <- conjureReification f]  conjureAreEqual :: Conjurable f => f -> Int -> Expr -> Expr -> Bool conjureAreEqual f maxTests  =  (===)@@ -184,7 +215,7 @@ conjureTiersFor f e  =  tf allTiers   where   allTiers :: [ [[Expr]] ]-  allTiers  =  [etiers | (_,_,_,Just etiers) <- conjureReification f]+  allTiers  =  [etiers | (_,_,Just etiers,_) <- conjureReification f]   tf []  =  [[e]] -- no tiers found, keep variable   tf (etiers:etc)  =  case etiers of                       ((e':_):_) | typ e' == typ e -> etiers@@ -195,23 +226,34 @@                                    .  take maxTests                                    .  grounds (conjureTiersFor f) +conjureIsUnbreakable :: Conjurable f => f -> Expr -> Bool+conjureIsUnbreakable f e  =  head+  [is | (h,_,_,is) <- conjureReification f, typ h == typ e]+ instance Conjurable () where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers+  conjureCases _   =  [val ()]  instance Conjurable Bool where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers+  conjureCases _   =  [val False, val True]  instance Conjurable Int where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Integer where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Char where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers @@ -219,9 +261,13 @@ (==:) :: (a -> a -> Bool) -> a -> (a -> a -> Bool) (==:)  =  const -instance (Conjurable a, Listable a, Show a) => Conjurable [a] where+instance (Conjurable a, Listable a, Express a, Show a) => Conjurable [a] where+  conjureExpress   =  reifyExpress   conjureSubTypes xs  =  conjureType (head xs)   conjureTiers     =  reifyTiers+  conjureCases xs  =  [ val ([] -: xs)+                      , value ":" ((:) ->>: xs) :$ hole x :$ hole xs+                      ]  where  x  =  head xs   conjureEquality xs  =  from <$> conjureEquality x     where     x  =  head xs@@ -233,12 +279,16 @@       []     == (y:ys) = False       (x:xs) == (y:ys) = x .==. y && xs == ys -instance ( Conjurable a, Listable a, Show a-         , Conjurable b, Listable b, Show b+instance ( Conjurable a, Listable a, Show a, Express a+         , Conjurable b, Listable b, Show b, Express b          ) => Conjurable (a,b) where+  conjureExpress   =  reifyExpress   conjureTiers     =  reifyTiers   conjureSubTypes xy  =  conjureType (fst xy)                       .  conjureType (snd xy)+  conjureCases xy  =  [value "," ((,) ->>: xy) :$ hole x :$ hole y]+    where+    (x,y) = (undefined,undefined) -: xy   conjureEquality xy  =  from <$> conjureEquality x <*> conjureEquality y     where     (x,y)  =  xy@@ -249,15 +299,19 @@       (x1,y1) == (x2,y2)  =  x1 ==. x2 && y1 .== y2  -instance ( Conjurable a, Listable a, Show a-         , Conjurable b, Listable b, Show b-         , Conjurable c, Listable c, Show c+instance ( Conjurable a, Listable a, Show a, Express a+         , Conjurable b, Listable b, Show b, Express b+         , Conjurable c, Listable c, Show c, Express c          ) => Conjurable (a,b,c) where+  conjureExpress   =  reifyExpress   conjureTiers     =  reifyTiers   conjureSubTypes xyz =  conjureType x                       .  conjureType y                       .  conjureType z                       where (x,y,z) = xyz+  conjureCases xyz  =  [value ",," ((,,) ->>>: xyz) :$ hole x :$ hole y :$ hole z]+    where+    (x,y,z) = (undefined,undefined,undefined) -: xyz   conjureEquality xyz  =  from                       <$> conjureEquality x                       <*> conjureEquality y@@ -273,9 +327,15 @@                                 && y1 .==. y2                                 && z1 ..== z2 -instance (Conjurable a, Listable a, Show a) => Conjurable (Maybe a) where+instance (Conjurable a, Listable a, Show a, Express a) => Conjurable (Maybe a) where+  conjureExpress   =  reifyExpress   conjureTiers     =  reifyTiers   conjureSubTypes mx  =  conjureType (fromJust mx)+  conjureCases mx  =  [ value "Nothing" (Nothing -: mx)+                      , value "Just" (Just ->: mx) :$ hole x+                      ]+    where+    x  =  Just undefined -: mx   conjureEquality mx  =  from <$> conjureEquality x     where     x  =  fromJust mx@@ -288,14 +348,21 @@       (Just x) == (Just y)  =  x .==. y  -instance ( Conjurable a, Listable a, Show a-         , Conjurable b, Listable b, Show b+instance ( Conjurable a, Listable a, Show a, Express a+         , Conjurable b, Listable b, Show b, Express b          ) => Conjurable (Either a b) where+  conjureExpress   =  reifyExpress   conjureTiers     =  reifyTiers   conjureSubTypes elr  =  conjureType l . conjureType r     where     Left l   =  elr     Right r  =  elr+  conjureCases exy  =  [ value "Left" (Left ->: exy) :$ hole x+                       , value "Right" (Right ->: exy) :$ hole y+                       ]+    where+    x  =  Left undefined -: exy+    y  =  Right undefined -: exy   conjureEquality elr  =  from <$> conjureEquality l <*> conjureEquality r     where     Left l   =  elr@@ -313,6 +380,10 @@   conjureArgumentHoles f  =  hole (argTy f) : conjureArgumentHoles (f undefined)   conjureSubTypes f  =  conjureType (argTy f) . conjureType (resTy f)   conjureIf f  =  conjureIf (f undefined)+  conjureArgumentCases f  =  conjureCases (argTy f) : conjureArgumentCases (f undefined)+  conjureExpress f e+    | typ e == typeOf (argTy f)  =  conjureExpress (argTy f) e+    | otherwise                  =  conjureExpress (f undefined) e  argTy :: (a -> b) -> a argTy _  =  undefined@@ -332,64 +403,91 @@   where   (nf:nas)  =  words nm ++ repeat "" +conjurePats :: Conjurable f => [Expr] -> String -> f -> [[[Expr]]]+conjurePats es nm f  =  mapT (map (foldApp . (ef:) . unfold . mostGeneralCanonicalVariation . fold) . prods) $ cs+  where+  ef  =  var (head $ words nm) f  -- TODO: take the tail into account+  cs  =  products $ zipWith mk (conjureArgumentHoles f) (conjureArgumentCases f)+  mk h []  =  mapT (++ [h]) $ setsOf [[e] | e <- es, typ e == typ h]+  mk h cs  =  [[[h]], [cs]]+  tiersFor  =  conjureTiersFor f +prods :: [[a]] -> [[a]]+prods  =  foldr (productWith (:)) [[]]+  where+  productWith (?) xs ys  =  [x ? y | x <- xs, y <- ys] + -- -- -- other Conjurable instances -- -- --  instance Conjurable Ordering where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Float where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Double where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Int8 where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Int16 where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Int32 where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Int64 where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Word where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Word8 where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Word16 where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Word32 where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable Word64 where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers -instance (Integral a, Conjurable a, Listable a, Show a, Eq a) => Conjurable (Ratio a) where+instance (Integral a, Conjurable a, Listable a, Show a, Eq a, Express a) => Conjurable (Ratio a) where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers   conjureSubTypes q  =  conjureType (numerator q) -instance (RealFloat a, Conjurable a, Listable a, Show a, Eq a) => Conjurable (Complex a) where+instance (RealFloat a, Conjurable a, Listable a, Show a, Eq a, Express a) => Conjurable (Complex a) where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers   conjureSubTypes x  =  conjureType (realPart x)@@ -397,37 +495,44 @@  -- Conjurable helper types -- instance Conjurable A where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable B where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable C where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable D where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable E where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers  instance Conjurable F where+  conjureExpress   =  reifyExpress   conjureEquality  =  reifyEquality   conjureTiers     =  reifyTiers   -- Conjurable tuples -- -instance ( Conjurable a, Listable a, Show a-         , Conjurable b, Listable b, Show b-         , Conjurable c, Listable c, Show c-         , Conjurable d, Listable d, Show d+instance ( Conjurable a, Listable a, Show a, Express a+         , Conjurable b, Listable b, Show b, Express b+         , Conjurable c, Listable c, Show c, Express c+         , Conjurable d, Listable d, Show d, Express d          ) => Conjurable (a,b,c,d) where+  conjureExpress   =  reifyExpress   conjureTiers     =  reifyTiers   conjureSubTypes xyzw =  conjureType x                        .  conjureType y@@ -452,12 +557,13 @@                                       && z1 ..==. z2                                       && w1 ...== w2 -instance ( Conjurable a, Listable a, Show a-         , Conjurable b, Listable b, Show b-         , Conjurable c, Listable c, Show c-         , Conjurable d, Listable d, Show d-         , Conjurable e, Listable e, Show e+instance ( Conjurable a, Listable a, Show a, Express a+         , Conjurable b, Listable b, Show b, Express b+         , Conjurable c, Listable c, Show c, Express c+         , Conjurable d, Listable d, Show d, Express d+         , Conjurable e, Listable e, Show e, Express e          ) => Conjurable (a,b,c,d,e) where+  conjureExpress   =  reifyExpress   conjureTiers     =  reifyTiers   conjureSubTypes xyzwv =  conjureType x                         .  conjureType y@@ -486,13 +592,14 @@                                             && w1 ...==. w2                                             && v1 ....== v2 -instance ( Conjurable a, Listable a, Show a-         , Conjurable b, Listable b, Show b-         , Conjurable c, Listable c, Show c-         , Conjurable d, Listable d, Show d-         , Conjurable e, Listable e, Show e-         , Conjurable f, Listable f, Show f+instance ( Conjurable a, Listable a, Show a, Express a+         , Conjurable b, Listable b, Show b, Express b+         , Conjurable c, Listable c, Show c, Express c+         , Conjurable d, Listable d, Show d, Express d+         , Conjurable e, Listable e, Show e, Express e+         , Conjurable f, Listable f, Show f, Express f          ) => Conjurable (a,b,c,d,e,f) where+  conjureExpress   =  reifyExpress   conjureTiers     =  reifyTiers   conjureSubTypes xyzwvu =  conjureType x                          .  conjureType y@@ -525,14 +632,15 @@                                                   && v1 ....==. v2                                                   && u1 .....== u2 -instance ( Conjurable a, Listable a, Show a-         , Conjurable b, Listable b, Show b-         , Conjurable c, Listable c, Show c-         , Conjurable d, Listable d, Show d-         , Conjurable e, Listable e, Show e-         , Conjurable f, Listable f, Show f-         , Conjurable g, Listable g, Show g+instance ( Conjurable a, Listable a, Show a, Express a+         , Conjurable b, Listable b, Show b, Express b+         , Conjurable c, Listable c, Show c, Express c+         , Conjurable d, Listable d, Show d, Express d+         , Conjurable e, Listable e, Show e, Express e+         , Conjurable f, Listable f, Show f, Express f+         , Conjurable g, Listable g, Show g, Express g          ) => Conjurable (a,b,c,d,e,f,g) where+  conjureExpress   =  reifyExpress   conjureTiers     =  reifyTiers   conjureSubTypes xyzwvut =  conjureType x                           .  conjureType y

@@ -0,0 +1,104 @@+-- |+-- Module      : Conjure.Defn+-- Copyright   : (c) 2021 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of 'Conjure'.+--+-- This module exports the 'Defn' type synonym and utilities involving it.+--+-- You are probably better off importing "Conjure".+{-# LANGUAGE TupleSections #-}+module Conjure.Defn+  ( Defn+  , Bndn+  , toDynamicWithDefn+  , devaluate+  , deval+  , devl+  , devalFast+  , showDefn+  , defnApparentlyTerminates+  , module Conjure.Expr+  )+where++import Conjure.Utils+import Conjure.Expr+import Data.Express+import Data.Express.Express+import Data.Express.Fixtures+import Data.Dynamic+import Control.Applicative ((<$>)) -- for older GHCs+import Test.LeanCheck.Utils ((-:>)) -- for toDynamicWithDefn++type Defn  =  [Bndn]+type Bndn  =  (Expr,Expr)++showDefn :: Defn -> String+showDefn  =  unlines . map show1+  where+  show1 (lhs,rhs)  =  showExpr lhs ++ "  =  " ++ showExpr rhs+++-- | Evaluates an 'Expr' using the given 'Defn' as definition+--   when a recursive call is found.+toDynamicWithDefn :: (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe Dynamic+toDynamicWithDefn exprExpr n cx  =  fmap (\(_,_,d) -> d) . re (n * sum (map (size . snd) cx)) n+  where+  (ef':_)  =  unfoldApp . fst $ head cx++  rev :: Typeable a => Int -> Int -> Expr -> Maybe (Int, Int, a)+  rev m n e  =  case re m n e of+                Nothing    -> Nothing+                Just (m,n,d) -> case fromDynamic d of+                                Nothing -> Nothing+                                Just x  -> Just (m, n, x)++  re :: Int -> Int -> Expr -> Maybe (Int, Int, Dynamic)+  re m n _  | n <= 0  =  error "toDynamicWithDefn: recursion limit reached"+  re m n _  | m <= 0  =  error "toDynamicWithDefn: evaluation limit reached"+  re m n (Value "if" _ :$ ec :$ ex :$ ey)  =  case rev m n ec of+    Nothing    -> Nothing+    Just (m,n,True)  -> re m n ex+    Just (m,n,False) -> re m n ey+  re m n (Value "||" _ :$ ep :$ eq)  =  case rev m n ep of+    Nothing        -> Nothing+    Just (m,n,True)  -> (m,n,) <$> toDynamic (val True)+    Just (m,n,False) -> re m n eq+  re m n (Value "&&" _ :$ ep :$ eq)  =  case rev m n ep of+    Nothing    -> Nothing+    Just (m,n,True)  -> re m n eq+    Just (m,n,False) -> (m,n,) <$> toDynamic (val False)+  re m n e  =  case unfoldApp e of+    [] -> error "toDynamicWithDefn: empty application unfold"  -- should never happen+    [e] -> (m-1,n,) <$> toDynamic e+    (ef:exs) | ef == ef' -> headOr (error $ "toDynamicWithDefn: unhandled pattern " ++ show e)+                          [ re m (n-1) $ e' //- bs+                          | let e  =  foldApp (ef:map exprExpr exs)+                          , (a',e') <- cx+                          , Just bs <- [e `match` a']+                          ]+             | otherwise -> foldl ($$) (re m n ef) exs++  Just (m,n,d1) $$ e2  =  case re m n e2 of+                          Nothing -> Nothing+                          Just (m', n', d2) -> (m',n',) <$> dynApply d1 d2+  _ $$ _               =  Nothing++devaluate :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> Maybe a+devaluate ee n fxpr e  =  toDynamicWithDefn ee n fxpr e >>= fromDynamic++deval :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a+deval ee n fxpr x  =  fromMaybe x . devaluate ee n fxpr++devalFast :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a+devalFast _ n [defn] x  =  reval defn n x++devl :: Typeable a => (Expr -> Expr) -> Int -> Defn -> Expr -> a+devl ee n fxpr  =  deval ee n fxpr (error "devl: incorrect type?")++defnApparentlyTerminates :: Defn -> Bool+defnApparentlyTerminates [(efxs, e)]  =  apparentlyTerminates efxs e+defnApparentlyTerminates _  =  True

@@ -18,6 +18,11 @@   , conjpure   , conjpureWith   , candidateExprs+  , candidateDefns+  , candidateDefns1+  , candidateDefnsC+  , conjureTheory+  , conjureTheoryWith   , module Data.Express   , module Data.Express.Fixtures   , module Test.Speculate.Engine@@ -40,6 +45,8 @@  import Conjure.Expr import Conjure.Conjurable+import Conjure.Prim+import Conjure.Defn   -- | Conjures an implementation of a partially defined function.@@ -55,12 +62,12 @@ -- > square 1  =  1 -- > square 2  =  4 -- >--- > primitives :: [Expr]+-- > primitives :: [Prim] -- > primitives =--- >   [ val (0::Int)--- >   , val (1::Int)--- >   , value "+" ((+) :: Int -> Int -> Int)--- >   , value "*" ((*) :: Int -> Int -> Int)+-- >   [ pr (0::Int)+-- >   , pr (1::Int)+-- >   , prim "+" ((+) :: Int -> Int -> Int)+-- >   , prim "*" ((*) :: Int -> Int -> Int) -- > ] -- -- The conjure function does the following:@@ -73,8 +80,8 @@ -- > -- 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 ()+-- The primitives list is defined with 'pr' and 'prim'.+conjure :: Conjurable f => String -> f -> [Prim] -> IO () conjure  =  conjureWith args  @@ -82,7 +89,7 @@ --   instead of the default value of 12. -- -- > conjureWithMaxSize 10 "function" function [...]-conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO ()+conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Prim] -> IO () conjureWithMaxSize sz  =  conjureWith args                        {  maxSize = sz                        ,  maxEquationSize = min sz (maxEquationSize args)@@ -94,7 +101,6 @@ data Args = Args   { maxTests          :: Int  -- ^ maximum number of tests to each candidate   , maxSize           :: Int  -- ^ maximum size of candidate bodies-  , maxBodyRecursions :: Int  -- ^ maximum number of recursive calls in candidate bodies   , maxEvalRecursions :: Int  -- ^ maximum number of recursive evaluations when testing candidates   , maxEquationSize   :: Int  -- ^ maximum size of equation operands   , maxSearchTests    :: Int  -- ^ maximum number of tests to search for defined values@@ -116,7 +122,6 @@ args = Args   { maxTests           =  60   , maxSize            =  12-  , maxBodyRecursions  =   1   , maxEvalRecursions  =  60   , maxEquationSize    =   5   , maxSearchTests     =  100000@@ -128,10 +133,11 @@ -- | Like 'conjure' but allows setting options through 'Args'/'args'. -- -- > conjureWith args{maxSize = 11} "function" function [...]-conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO ()+conjureWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO () conjureWith args nm f es  =  do   print (var (head $ words nm) f)   putStrLn $ "-- testing " ++ show (length ts) ++ " combinations of argument values"+  putStrLn $ "-- pruning with " ++ show nRules ++ "/" ++ show nREs ++ " rules"   pr 1 rs   where   pr n []  =  putStrLn $ "cannot conjure\n"@@ -139,13 +145,14 @@     putStrLn $ "-- looking through "             ++ show (length cs)             ++ " candidates of size " ++ show n-    -- when (n<=12) $ putStrLn $ unlines $ map show cs+    -- when (n<=12) $ putStrLn $ unlines $ map showDefn cs     case is of       []     ->  pr (n+1) rs-      (i:_)  ->  do putStrLn $ showEq i-                    putStrLn ""+      (i:_)  ->  putStrLn $ showDefn i   rs  =  zip iss css-  (iss, css, ts)  =  conjpureWith args nm f es+  (iss, css, ts, thy)  =  conjpureWith args nm f es+  nRules  =  length (rules thy)+  nREs  =  length (equations thy) + nRules   -- | Like 'conjure' but in the pure world.@@ -156,20 +163,20 @@ -- 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])+conjpure :: Conjurable f => String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy) 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@(Args{..}) nm f es  =  (implementationsT, candidatesT, tests)+conjpureWith :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], [[Defn]], [Expr], Thy)+conjpureWith args@(Args{..}) nm f es  =  (implementationsT, candidatesT, tests, thy)   where   tests  =  [ffxx //- bs | bs <- dbss]-  implementationsT  =  mapT (vffxx -==-) $ filterT implements candidatesT-  implements e  =  apparentlyTerminates rrff e-                && requal (vffxx,e) ffxx vffxx-  candidatesT  =  take maxSize-               $  candidateExprs args nm f es+  implementationsT  =  filterT implements candidatesT+  implements fx  =  defnApparentlyTerminates fx+                 && requal fx ffxx vffxx+  candidatesT  =  take maxSize candidatesTT+  (candidatesTT, thy)  =  candidateDefns args nm f es   ffxx   =  conjureApplication nm f   vffxx  =  conjureVarApplication nm f   (rrff:xxs)  =  unfoldApp vffxx@@ -177,7 +184,8 @@   requal dfn e1 e2  =  isTrueWhenDefined dfn (e1 -==- e2)   (-==-)  =  conjureMkEquation f -  isTrueWhenDefined dfn e  =  all (errorToFalse . reval dfn maxEvalRecursions False) $ map (e //-) dbss+  isTrueWhenDefined dfn e  =  all (errorToFalse . deval (conjureExpress f) maxEvalRecursions dfn False)+                           $  map (e //-) dbss    bss, dbss :: [[(Expr,Expr)]]   bss  =  take maxSearchTests $ groundBinds (conjureTiersFor f) ffxx@@ -189,9 +197,39 @@     e  =  ffxx -==- ffxx  -candidateExprs :: Conjurable f => Args -> String -> f -> [Expr] -> [[Expr]]-candidateExprs Args{..} nm f es  =  as \/ concatMapT (`enumerateFillings` recs) ts+conjureTheory :: Conjurable f => String -> f -> [Prim] -> IO ()+conjureTheory  =  conjureTheoryWith args+++conjureTheoryWith :: Conjurable f => Args -> String -> f -> [Prim] -> IO ()+conjureTheoryWith args nm f es  =  do+  putStrLn $ "theory with " ++ (show . length $ rules thy) ++ " rules and "+                            ++ (show . length $ equations thy) ++ " equations"+  printThy thy   where+  (_, _, _, thy)  =  conjpureWith args nm f es+++-- | Return apparently unique candidate definitions.+candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)+candidateDefns  =  candidateDefns1+++-- | Return apparently unique candidate definitions+--   where there is a single body.+candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)+candidateDefns1 args nm f ps  =  mapFst (mapT toDefn) $ candidateExprs args nm f ps+  where+  mapFst f (x,y)  =  (f x, y)+  efxs  =  conjureVarApplication nm f+  toDefn e  =  [(efxs, e)]+++-- | Return apparently unique candidate bodies.+candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy)+candidateExprs Args{..} nm f ps  =  (as \/ concatMapT (`enumerateFillings` recs) ts, thy)+  where+  es  =  map fst ps   ts | typ efxs == boolTy  =  foldAppProducts andE [cs, rs]                            \/ foldAppProducts orE  [cs, rs]      | otherwise           =  filterT keepIf@@ -201,22 +239,74 @@       $  forN (hole (undefined :: Bool))   as  =  forN efxs   rs  =  forR efxs-  forN h  =  enumerateAppsFor h keep [exs ++ es]+  forN h  =  enumerateAppsFor h keep $ exs ++ es   forR h  =  filterT (\e -> (eh `elem`) (holes e))-          $  enumerateAppsFor h keep $ [exs ++ es ++ [eh]]+          $  enumerateAppsFor h keep $ exs ++ es ++ [eh]   eh  =  holeAsTypeOf efxs   efxs  =  conjureVarApplication nm f   (ef:exs)  =  unfoldApp efxs-  keep e  =  isRootNormalE thy e-          && count (== ef) (vars e) <= maxBodyRecursions+  keep  =  isRootNormalE thy . fastMostGeneralVariation   ds  =  map snd $ deconstructors f maxTests es   keepR | requireDescent  =  descends (`elem` ds) efxs         | otherwise       =  const True   recs  =  filterT keepR         $  foldAppProducts ef [forN h | h <- conjureArgumentHoles f]   thy  =  theoryFromAtoms (===) maxEquationSize . (:[]) . nub-       $  conjureHoles f ++ [val False, val True] ++ es-  (===)  =  conjureAreEqual f maxTests+       $  cjHoles (prim nm f:ps) ++ [val False, val True] ++ es+  (===)  =  cjAreEqual (prim nm f:ps) maxTests++-- | Return apparently unique candidate definitions+--   using pattern matching.+candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy)+candidateDefnsC Args{..} nm f ps  =  (concatMapT fillingsFor fss,thy)+  where+  fss  =  concatMapT ps2fss (conjurePats es nm f)+  es  =  map fst ps++  eh  =  holeAsTypeOf efxs+  efxs  =  conjureVarApplication nm f+  (ef:exs)  =  unfoldApp efxs++  keep  =  isRootNormalE thy . fastMostGeneralVariation++  appsWith :: Expr -> [Expr] -> [[Expr]]+  appsWith eh vs  =  enumerateAppsFor eh keep $ vs ++ es+++  ps2fss :: [Expr] -> [[Defn]]+  ps2fss pats  =  discardT (allEqual . map snd) . products $ map p2eess pats+    where+    p2eess :: Expr -> [[Bndn]]+    p2eess pat  =  mapT (pat,)+                .  appsWith pat+                .  tail+                $  vars pat ++ [eh | length pats > 1, any should aes]+      where+      should ae  =  hasVar ae && (isApp ae || isUnbreakable ae)+      (_:aes)  =  unfoldApp pat++  fillingsFor1 :: Bndn -> [[Bndn]]+  fillingsFor1 (ep,er)  =  mapT (\es -> (ep,fill er es))+                        .  products+                        .  replicate (length $ holes er)+                        $  recs ep es++  fillingsFor :: Defn -> [[Defn]]+  fillingsFor  =  products . map fillingsFor1++  recs ep es  =  discardT (\e -> e == ep)+              $  filterT (\e -> any (`elem` vs) (vars e))+              $  foldAppProducts ef [appsWith h (vs ++ es) | h <- conjureArgumentHoles f]+    where -- TODO: proper descent check above+    vs  =  tail (vars ep)++  thy  =  theoryFromAtoms (===) maxEquationSize . (:[]) . nub+       $  cjHoles (prim nm f:ps) ++ [val False, val True] ++ es+  (===)  =  cjAreEqual (prim nm f:ps) maxTests+  isUnbreakable  =  conjureIsUnbreakable f+-- this seems to work, see:+-- > blindCandidateDefns args "fact" (undefined :: [Int] -> Int) [pr (0::Int), pr (1::Int), prim "+" ((+)::Int->Int->Int)]+  -- | Returns whether the given recursive call --   deconstructs one of its arguments.

@@ -34,7 +34,6 @@   , revaluate   , reval -  , enumerateApps   , enumerateAppsFor   , enumerateFillings @@ -53,6 +52,7 @@  import Test.LeanCheck (mapT, filterT, (\/), delay, productWith, productMaybeWith) import Test.LeanCheck.Tiers (products)+import Test.LeanCheck.Utils.Types (A, B, C, D, E, F)  -- | /O(n)/. -- Compares the simplicity of two 'Expr's.@@ -285,47 +285,13 @@  -- -- Expression enumeration -- -- -enumerateAppsFor :: Expr -> (Expr -> Bool) -> [[Expr]] -> [[Expr]]-enumerateAppsFor  =  enumerateApps3For--enumerateApps :: (Expr -> Bool) -> [Expr] -> [[Expr]]-enumerateApps  =  enumerateApps1--enumerateApps1For :: Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]-enumerateApps1For h keep  =  filterT (\e -> typ e == typ h) . enumerateApps1 keep--enumerateApps1 :: (Expr -> Bool) -> [Expr] -> [[Expr]]-enumerateApps1 keep  =  exprT . (:[])-  where-  exprT ess  =  filterT keep-             $  ess \/ (delay $ productMaybeWith ($$) rss rss)-    where-    rss = exprT ess--enumerateApps2For :: Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]-enumerateApps2For h keep  =  map concat-                          .  filterT (\(e:_) -> typ e == typ h)-                          .  exprT-                          .  map (groupOn typ . sortOn typ)-                          .  (:[])-  where-  exprT :: [[[Expr]]] -> [[[Expr]]]-  exprT ess  =  ess \/ (delay $ productMaybeWith ($$**) rss rss)-    where-    rss = exprT ess-    efs $$** exs-      | isNothing (head efs $$ head exs)  =  Nothing-      | otherwise  =  case [ef :$ ex | ef <- efs, ex <- exs, keep (ef :$ ex)] of-                      [] -> Nothing-                      es -> Just es--enumerateApps3For :: Expr -> (Expr -> Bool) -> [[Expr]] -> [[Expr]]-enumerateApps3For h keep ess  =  for h+enumerateAppsFor :: Expr -> (Expr -> Bool) -> [Expr] -> [[Expr]]+enumerateAppsFor h keep es  =  for h   where   hs :: [Expr]-  hs  =  possibleHoles . concat $ take 1 ess+  hs  =  possibleHoles es   for :: Expr -> [[Expr]]-  for h  =  filterT (\e -> typ h == typ e) ess \/ delay apps+  for h  =  filter (\e -> typ h == typ e) es : apps     where     apps  =  foldr (\/) []           [  filterT keep $ fliproductWith (:$) (for hf) (for hx)@@ -389,7 +355,7 @@ revaluate dfn n e  =  recursiveToDynamic dfn n e >>= fromDynamic  reval :: Typeable a => (Expr,Expr) -> Int -> a -> Expr -> a-reval dfn n x e = fromMaybe x (revaluate dfn n e)+reval dfn n x  =  fromMaybe x . revaluate dfn n  -- | like 'productWith' but prefers enumerating from the second tiers first fliproductWith :: (a->b->c) -> [[a]] -> [[b]] -> [[c]]@@ -399,3 +365,10 @@                                \/ delay (productWith f xss yss)   where   xs ** ys  =  [x `f` y | x <- xs, y <- ys]++instance Express A where  expr  =  val+instance Express B where  expr  =  val+instance Express C where  expr  =  val+instance Express D where  expr  =  val+instance Express E where  expr  =  val+instance Express F where  expr  =  val

@@ -0,0 +1,80 @@+-- |+-- Module      : Conjure.Prim+-- Copyright   : (c) 2021 Rudy Matela+-- License     : 3-Clause BSD  (see the file LICENSE)+-- Maintainer  : Rudy Matela <rudy@matela.com.br>+--+-- This module is part of 'Conjure'.+--+-- The 'Prim' type and utilities involving it.+--+-- You are probably better off importing "Conjure".+module Conjure.Prim+  ( Prim (..)+  , prim+  , pr+  , cjHoles+  , cjTiersFor+  , cjAreEqual+  , cjMkEquation+  )+where++import Conjure.Conjurable+import Conjure.Expr+import Conjure.Utils+import Test.LeanCheck.Error (errorToFalse)+import Test.LeanCheck.Utils+import Test.Speculate.Expr+++-- | A primtive expression (paired with instance reification).+type Prim  =  (Expr, Reification)+++-- | Provides a primitive value to Conjure.+--   To be used on 'Show' instances.+--   (cf. 'prim')+pr :: (Conjurable a, Show a) => a -> Prim+pr x  =  (val x, conjureType x)+++-- | Provides a primitive value to Conjure.+--   To be used on values that are not 'Show' instances+--   such as functions.+--   (cf. 'pr')+prim :: Conjurable a => String -> a -> Prim+prim s x  =  (value s x, conjureType x)+++-- the following functions mirror their "conjure" counterparts from+-- Conjure.Conjurable but need a list of Prims instead of a Conjurable+-- representative.++cjReification :: [Prim] -> [Reification1]+cjReification ps  =  nubOn (\(eh,_,_,_) -> eh)+                  $  foldr (.) id (map snd ps) [conjureReification1 bool]++cjHoles :: [Prim] -> [Expr]+cjHoles ps  =  [eh | (eh,_,Just _,_) <- cjReification ps]++cjMkEquation :: [Prim] -> Expr -> Expr -> Expr+cjMkEquation ps  =  mkEquation [eq | (_,Just eq,_,_) <- cjReification ps]++cjAreEqual :: [Prim] -> Int -> Expr -> Expr -> Bool+cjAreEqual ps maxTests  =  (===)+  where+  (-==-)  =  cjMkEquation ps+  e1 === e2  =  isTrue $ e1 -==- e2+  isTrue  =  all (errorToFalse . eval False) . gs+  gs  =  take maxTests . grounds (cjTiersFor ps)++cjTiersFor :: [Prim] -> Expr -> [[Expr]]+cjTiersFor ps e  =  tf allTiers+  where+  allTiers :: [ [[Expr]] ]+  allTiers  =  [etiers | (_,_,Just etiers,_) <- cjReification ps]+  tf []  =  [[e]] -- no tiers found, keep variable+  tf (etiers:etc)  =  case etiers of+                      ((e':_):_) | typ e' == typ e -> etiers+                      _                            -> tf etc

@@ -25,6 +25,7 @@ import Conjure.Engine import Conjure.Conjurable import Conjure.Utils+import Conjure.Prim   -- | A partial specification of a function with one argument:@@ -78,13 +79,13 @@ -- >   , [3,4,5] -= 12 -- >   ] ----- > sumPrimitives :: [Expr]+-- > sumPrimitives :: [Prim] -- > sumPrimitives  =--- >   [ value "null" (null :: [Int] -> Bool)--- >   , val (0::Int)--- >   , value "+"    ((+) :: Int -> Int -> Int)--- >   , value "head" (head :: [Int] -> Int)--- >   , value "tail" (tail :: [Int] -> [Int])+-- >   [ prim "null" (null :: [Int] -> Bool)+-- >   , pr (0::Int)+-- >   , prim "+"    ((+) :: Int -> Int -> Int)+-- >   , prim "head" (head :: [Int] -> Int)+-- >   , prim "tail" (tail :: [Int] -> [Int]) -- >   ] -- -- Then:@@ -97,8 +98,8 @@ -- > xs ++ ys  =  if null xs then ys else head xs:(tail xs ++ ys) -- -- (cf. 'Spec1', 'conjure1With')-conjure1 :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b)-         => String -> Spec1 a b -> [Expr] -> IO ()+conjure1 :: (Eq a, Eq b, Show a, Express a, Conjurable a, Conjurable b)+         => String -> Spec1 a b -> [Prim] -> IO () conjure1  =  conjure1With args  @@ -115,10 +116,10 @@ -- -- > appPrimitives :: [Expr] -- > appPrimitives =--- >   [ value "null" (null :: [Int] -> Bool)--- >   , value ":"    ((:) :: Int -> [Int] -> [Int])--- >   , value "head" (head :: [Int] -> Int)--- >   , value "tail" (tail :: [Int] -> [Int])+-- >   [ prim "null" (null :: [Int] -> Bool)+-- >   , prim ":"    ((:) :: Int -> [Int] -> [Int])+-- >   , prim "head" (head :: [Int] -> Int)+-- >   , prim "tail" (tail :: [Int] -> [Int]) -- >   ] -- -- Then:@@ -131,48 +132,48 @@ -- > 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+conjure2 :: ( Conjurable a, Eq a, Show a, Express a+            , Conjurable b, Eq b, Show b, Express b             , Conjurable c, Eq c-            ) => String -> Spec2 a b c -> [Expr] -> IO ()+            ) => String -> Spec2 a b c -> [Prim] -> 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+conjure3 :: ( Conjurable a, Eq a, Show a, Express a+            , Conjurable b, Eq b, Show b, Express b+            , Conjurable c, Eq c, Show c, Express c             , Conjurable d, Eq d-            ) => String -> Spec3 a b c d -> [Expr] -> IO ()+            ) => String -> Spec3 a b c d -> [Prim] -> IO () conjure3  =  conjure3With args   -- | Like 'conjure1' but allows setting options through 'Args'/'args'.-conjure1With :: (Eq a, Eq b, Show a, Conjurable a, Conjurable b)-             => Args -> String -> Spec1 a b -> [Expr] -> IO ()+conjure1With :: (Eq a, Eq b, Show a, Express a, Conjurable a, Conjurable b)+             => Args -> String -> Spec1 a b -> [Prim] -> 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+conjure2With :: ( Conjurable a, Eq a, Show a, Express a+                , Conjurable b, Eq b, Show b, Express b                 , Conjurable c, Eq c-                ) => Args -> String -> Spec2 a b c -> [Expr] -> IO ()+                ) => Args -> String -> Spec2 a b c -> [Prim] -> 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+conjure3With :: ( Conjurable a, Eq a, Show a, Express a+                , Conjurable b, Eq b, Show b, Express b+                , Conjurable c, Eq c, Show c, Express c                 , Conjurable d, Eq d-                ) => Args -> String -> Spec3 a b c d -> [Expr] -> IO ()+                ) => Args -> String -> Spec3 a b c d -> [Prim] -> IO () conjure3With args nm bs  =  conjureWith args{forceTests=ts} nm (mkFun3 bs)   where   ts = [[val x, val y, val z] | ((x,y,z),_) <- bs]

@@ -32,6 +32,8 @@   , idIO   , mapHead   , sets+  , headOr+  , allEqual   ) where @@ -44,6 +46,12 @@  import System.IO.Unsafe +allEqual :: Eq a => [a] -> Bool+allEqual []  =  False+allEqual [x]  =  False+allEqual [x,y]  =  x == y+allEqual (x:y:xs)  =  x == y && allEqual (y:xs)+ count :: (a -> Bool) -> [a] -> Int count p  =  length . filter p @@ -118,3 +126,7 @@ sets (x:xs)  =  map (x:) ss ++ ss   where   ss  =  sets xs++headOr :: a -> [a] -> a+headOr x []  =  x+headOr _ (x:xs)  =  x

@@ -10,5 +10,5 @@  extra-deps: - leancheck-0.9.10-- speculate-0.4.8-- express-0.1.14+- speculate-0.4.12+- express-1.0.4

@@ -12,8 +12,11 @@  instance Listable Unit where list = [Unit] instance Conjurable Unit where+  conjureExpress = reifyExpress   conjureTiers = reifyTiers +instance Express Unit where  expr  =  val+ main :: IO () main  =  mainTest tests 5040 @@ -108,7 +111,72 @@   , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Unit,Bool,Bool))   , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Bool,Unit,Bool))   , isNothing $ conjureEquality (undefined :: (Bool,Bool,Bool,Bool,Bool,Bool,Unit))++  , length (conjureCases (undefined :: ()))      == 1+  , length (conjureCases (undefined :: Bool))    == 2+  , length (conjureCases (undefined :: Int))     == 0+  , length (conjureCases (undefined :: Integer)) == 0+  , length (conjureCases (undefined :: [Int]))   == 2+  , length (conjureCases (undefined :: [Bool]))  == 2++  , conjurePats [zero, one] "f" (undefined :: Int -> Int)+    == [ [ [ ff xx+           ]+         ]+       , [ [ ff zero+           , ff xx+           ]+         ]+       , [ [ ff one+           , ff xx+           ]+         ]+       , [ [ ff zero+           , ff one+           , ff xx+           ]+         ]+       ]++  , conjurePats [] "f" (undefined :: [Int] -> Int)+    == [ [ [ ffs xxs+           ]+         ]+       , [ [ ffs nilInt+           , ffs (xx -:- xxs)+           ]+         ]+       ]++  , conjurePats [] "foo" (undefined :: [Int] -> [Char] -> Int)+    == [ [ [ ffoo xxs ccs+           ]+         ]+       , [ [ ffoo xxs emptyString+           , ffoo xxs (cc -:- ccs)+           ]+         , [ ffoo nilInt       ccs+           , ffoo (xx -:- xxs) ccs+           ]+         ]+       , [ [ ffoo nilInt emptyString+           , ffoo nilInt (cc -:- ccs)+           , ffoo (xx -:- xxs) emptyString+           , ffoo (xx -:- xxs) (cc -:- ccs)+           ]+         ]+       ]   ]++ffs :: Expr -> Expr+ffs e  =  ffE :$ e+  where+  ffE  =  var "f" (undefined :: [Int] -> Int)++ffoo :: Expr -> Expr -> Expr+ffoo e1 e2  =  fooE :$ e1 :$ e2+  where+  fooE  =  var "foo" (undefined :: [Int] -> [Char] -> Int)  -- Equality but obtained through conjurable (<==>) :: Conjurable a => a -> a -> Bool

@@ -0,0 +1,72 @@+-- Copyright (C) 2021 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).++import Test+import Conjure.Defn+import Test.LeanCheck.Error (errorToLeft)++main :: IO ()+main  =  mainTest tests 5040++tests :: Int -> [Bool]+tests n  =+  [ True++  , dvl sumDefn (sumV :$ val [1,2,3,11::Int]) == (17 :: Int)+  , dvl sumDefn (sumV :$ val [1,2,3::Int])    == ( 6 :: Int)+  , dvl sumDefn (sumV :$ val [1,2,3,4::Int])  == (10 :: Int)++  , dvl factDefn (factV :$ val (0 :: Int)) == (1 :: Int)+  , dvl factDefn (factV :$ val (1 :: Int)) == (1 :: Int)+  , dvl factDefn (factV :$ val (2 :: Int)) == (2 :: Int)+  , dvl factDefn (factV :$ val (3 :: Int)) == (6 :: Int)+  , dvl factDefn (factV :$ val (4 :: Int)) == (24 :: Int)+  , dvl factDefn (factV :$ val (9 :: Int)) == (362880 :: Int)+  , errorToLeft (dvl factDefn (factV :$ val (10 :: Int)))+    == Right (3628800 :: Int)+  , errorToLeft (dvl factDefn (factV :$ val (11 :: Int)) == (39916800 :: Int))+    == Left "toDynamicWithDefn: recursion limit reached"++  , dvl isZeroDefn (isZeroV :$ val (0 :: Int)) == True+  , dvl isZeroDefn (isZeroV :$ val (1 :: Int)) == False++  , dvl nullDefn (nullV :$ val [0,1,2,3::Int]) == False+  , dvl nullDefn (nullV :$ val ([] :: [Int])) == False+  ]++dvl :: Typeable a => Defn -> Expr -> a+dvl  =  devl exprExpr 12++sumV, factV, nullV, isZeroV :: Expr+factV    =  var "fact"   (undefined :: Int -> Int)+sumV     =  var "sum"    (undefined :: [Int] -> Int)+isZeroV  =  var "isZero" (undefined :: Int -> Bool)+nullV    =  var "null"   (undefined :: [Int] -> Bool)++-- NOTE: a hack for testing needs all types that are Express as arguments of+--       undefined.+exprExpr :: Expr -> Expr+exprExpr  =  conjureExpress (undefined :: Int -> [Int] -> ())++sumDefn :: Defn+sumDefn  =  [ sum' nil           =-  zero+            , sum' (xx -:- xxs)  =-  xx -+- (sumV :$ xxs)+            ]  where  sum' e  =  sumV :$ e++factDefn :: Defn+factDefn  =  [ fact' zero  =-  one+             , fact' xx    =-  xx -*- (factV :$ (xx -+- minusOne))+             ]  where  fact' e  =  factV :$ e++nullDefn :: Defn+nullDefn  =  [ null' nil           =-  false+             , null' (xx -:- xxs)  =-  false+             ]  where  null' e  =  nullV :$ e++isZeroDefn :: Defn+isZeroDefn  =  [ isZero' zero  =-  true+               , isZero' xx    =-  false+               ]  where  isZero' e  =  isZeroV :$ e++(=-) = (,)+infixr 0 =-