code-conjure 0.6.0 → 0.6.2

raw patch · 77 files changed

+599/−138 lines, 77 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• .gitignore +2/−0
• Makefile +2/−0
• TODO.md +90/−0
• bench/candidates.hs +8/−2
• bench/candidates.txt +192/−1
• bench/carry-on.txt +13/−9
• bench/erroneous.hs +1/−1
• bench/gps.txt +2/−2
• bench/gps2.txt +4/−4
• bench/p12.txt +1/−1
• bench/redundants.hs +1/−1
• bench/runtime/lapmatrud/bench/candidates.runtime +1/−1
• bench/runtime/lapmatrud/bench/carry-on.runtime +1/−1
• bench/runtime/lapmatrud/bench/gps.runtime +1/−1
• bench/runtime/lapmatrud/bench/gps2.runtime +1/−1
• bench/runtime/lapmatrud/bench/unique.runtime +1/−1
• bench/runtime/lapmatrud/eg/arith.runtime +1/−1
• bench/runtime/lapmatrud/eg/bits.runtime +1/−0
• bench/runtime/lapmatrud/eg/bools.runtime +1/−1
• bench/runtime/lapmatrud/eg/bst.runtime +1/−1
• bench/runtime/lapmatrud/eg/dupos.runtime +1/−1
• bench/runtime/lapmatrud/eg/fib01.runtime +1/−1
• bench/runtime/lapmatrud/eg/fibonacci.runtime +1/−1
• bench/runtime/lapmatrud/eg/ints.runtime +1/−1
• bench/runtime/lapmatrud/eg/pow.runtime +1/−1
• bench/runtime/lapmatrud/eg/tri.runtime +1/−0
• bench/runtime/zero/bench/candidates.runtime +1/−1
• bench/runtime/zero/bench/carry-on.runtime +1/−1
• bench/runtime/zero/bench/erroneous.runtime +1/−1
• bench/runtime/zero/bench/gps.runtime +1/−1
• bench/runtime/zero/bench/gps2.runtime +1/−1
• bench/runtime/zero/bench/p12.runtime +1/−1
• bench/runtime/zero/bench/redundants.runtime +1/−1
• bench/runtime/zero/bench/strategies.runtime +1/−1
• bench/runtime/zero/bench/terpret.runtime +1/−1
• bench/runtime/zero/bench/unique.runtime +1/−1
• bench/runtime/zero/bench/weird.runtime +1/−1
• bench/runtime/zero/eg/arith.runtime +1/−1
• bench/runtime/zero/eg/bits.runtime +1/−0
• bench/runtime/zero/eg/bools.runtime +1/−1
• bench/runtime/zero/eg/bst.runtime +1/−1
• bench/runtime/zero/eg/count.runtime +1/−1
• bench/runtime/zero/eg/dupos.runtime +1/−1
• bench/runtime/zero/eg/either.runtime +1/−1
• bench/runtime/zero/eg/factorial.runtime +1/−1
• bench/runtime/zero/eg/fib01.runtime +1/−1
• bench/runtime/zero/eg/fibonacci.runtime +1/−1
• bench/runtime/zero/eg/higher.runtime +1/−1
• bench/runtime/zero/eg/id.runtime +1/−1
• bench/runtime/zero/eg/ints.runtime +1/−1
• bench/runtime/zero/eg/list.runtime +1/−1
• bench/runtime/zero/eg/maybe.runtime +1/−1
• bench/runtime/zero/eg/oddeven.runtime +1/−1
• bench/runtime/zero/eg/pow.runtime +1/−1
• bench/runtime/zero/eg/replicate.runtime +1/−1
• bench/runtime/zero/eg/setelem.runtime +1/−1
• bench/runtime/zero/eg/take-drop.runtime +1/−1
• bench/runtime/zero/eg/tree.runtime +1/−1
• bench/runtime/zero/eg/tri.runtime +1/−0
• bench/strategies.txt +8/−8
• bench/unique.hs +1/−1
• bench/weird.hs +1/−1
• changelog.md +12/−0
• code-conjure.cabal +2/−2
• eg/bits.hs +40/−0
• eg/bits.txt +30/−0
• eg/count.hs +3/−7
• eg/fib01.hs +16/−14
• eg/fib01.txt +2/−11
• eg/fibonacci.txt +6/−6
• eg/pow.txt +4/−4
• eg/take-drop.txt +5/−5
• eg/tri.hs +18/−0
• eg/tri.txt +14/−0
• mk/depend.mk +34/−0
• src/Conjure/Defn.hs +4/−2
• src/Conjure/Engine.hs +35/−12

@@ -55,6 +55,8 @@ eg/subset eg/spec eg/colin/*Funs+eg/tri+eg/bits bench/carry-on bench/strategies bench/self

@@ -45,6 +45,8 @@   eg/tapps \   eg/tree \   eg/bst \+  eg/tri \+  eg/bits \   bench/candidates \   bench/redundants \   bench/erroneous \

@@ -3,9 +3,99 @@  A non-exhaustive list of things TO DO for Conjure. +* forbid recursion into negatives+ * consider the size of patterns to thin-out each size partition  * consider non top-level cases+++## Forbid recursion into negatives++Instead of reporting:++	tri 1  =  1+	tri x  =  x + tri (x - 1)++Report:++	tri 1          =  1+	tri x | x > 1  =  x + tri (x - 1)++This is not trivial to implement.+Tentative steps:++1. create a `descents` function, similar to `descends`,+   that is able to list the groups of variable that have recursive descents.+   This will somehow need a dummy `isDecOf` function.+   This may require changing the format definitions themselves...+2. use this on `showDefn` somehow+3. use this on `toDynamicWithDefn` somehow+++## Thin-out size partitions++Consider the following two candidates:++	fib01 x y z  =  dec x++	fib01 x y 0  =  x+	fib01 x y z  =  y++They both currently have size 2.+Perhaps the second should be bigger than the first?+"Simple" solution:+consider the number of (extra) patterns as part of the size.++See the following two candidates of size 3:++	fib01 x y z  =  x + x++	fib01 x y 0  =  x+	fib01 x y z  =  dec x++The same thing can be said.++Now a little bit more complex...+The following two candidates appear at size 3 for fib01:++	fib01 x 0 y  =  x+	fib01 x y 0  =  y+	fib01 x y z  =  0++	fib01 x 0 0  =  x+	fib01 x 0 y  =  y+	fib01 x y z  =  0++Shouldn't these two have different size?+The second feels bigger than the first.+Maybe the size of non-variable patterns should be taken into account.++This relates to the eg/fib01 example.++Also:+see the allowed patterns on the Int functions of two arguments+in bench/candidates.txt.  Search for "allowed patterns".++There are two levels here:++1. considering the number of patterns as part of the size+2. considering the number of non-variable LHS arguments as part of the size++Level 2. is not addressed at all.  But it turns out that level 1. is already+handled at the conjurePatterns function.  The patterns reported with showPatterns+and on bench/candidates already seem to be divided considering the number of+lines...++Something to keep in mind: tiers enumerations have size "0".+If one wants to increase size, one needs to push things to size "1".+So the size is actually being considered.  One would need a delayedProducts to+complete "1.".  Maybe it is better to start investigating from "2."++The enumeration currently works like so:+the size of patterns is defined by the number of patterns that are allowed to+have _another_ option other than a simple variable.+Perhaps these should be thinned-out in post processing to achieve "2."?   ## Non top-level cases

@@ -19,6 +19,12 @@   putStrLn $ unlines $ map showDefn $ concat $ take n $ css1   putStrLn $ "pattern candidates:\n"   putStrLn $ unlines $ map showDefn $ concat $ take n $ cssC+  putStrLn ""+  putStrLn $ "allowed patterns:\n"+  putStrLn $ unlines $ map unlines $ map (map showDefn) $ pss+  putStrLn ""+  putStrLn $ "allowed deconstructions:\n"+  putStrLn $ unlines $ map show ds   where   nd1  =  length cs1 - length (nubSort cs1)   ndC  =  length csC - length (nubSort csC)@@ -26,8 +32,8 @@   csC  =  concat cssC   css1  =  take m css1'   cssC  =  take m cssC'-  (css1', thy, _)  =  candidateDefns1 args nm f ps-  (cssC', _, _)    =  candidateDefnsC args nm f ps+  (css1', thy, _, _)  =  candidateDefns1 args nm f ps+  (cssC', _, pss, ds)  =  candidateDefnsC args nm f ps   nRules  =  length (rules thy)   nREs  =  length (equations thy) + nRules 

@@ -1,7 +1,7 @@ Candidates for: foo :: Int -> Int   pruning with 27/65 rules   [3,0,8,0,30,0,177,0,1203] direct candidates, 0 duplicates-  [3,3,9,10,32,39,185,217,1169] pattern candidates, 0 duplicates+  [3,3,9,10,32,39,185,233,1169] pattern candidates, 0 duplicates  rules: x - x == 0@@ -428,6 +428,31 @@ foo x  =  0 - x  ++allowed patterns:++foo x  =  _+++foo 0  =  _+foo x  =  _+++foo 1  =  _+foo x  =  _+++foo 0  =  _+foo 1  =  _+foo x  =  _+++++allowed deconstructions:++_ - 1 :: Int+ Candidates for: ? :: Int -> Int -> Int   pruning with 13/34 rules   [3,3,9,18,60,162,489,1475,4619] direct candidates, 0 duplicates@@ -1586,6 +1611,42 @@ x ? y  =  dec x  ++allowed patterns:++x ? y  =  _+++x ? 0  =  _+x ? y  =  _++0 ? x  =  _+x ? y  =  _+++0 ? x  =  _+x ? 0  =  _+x ? y  =  _++0 ? 0  =  _+0 ? x  =  _+x ? y  =  _+++0 ? 0  =  _+0 ? x  =  _+x ? 0  =  _+x ? y  =  _+++++allowed deconstructions:++dec _ :: Int+dec (dec _) :: Int+dec (dec (dec _)) :: Int+ Candidates for: goo :: [Int] -> [Int]   pruning with 4/4 rules   [2,0,1,0,1,0,1,0,1] direct candidates, 0 duplicates@@ -1661,6 +1722,21 @@ goo (x:xs)  =  xs ++ (xs ++ xs)  ++allowed patterns:++goo xs  =  _+++goo []  =  _+goo (x:xs)  =  _+++++allowed deconstructions:++ Candidates for: ?? :: [Int] -> [Int] -> [Int]   pruning with 4/4 rules   [3,0,4,0,8,0,16,0,32] direct candidates, 0 duplicates@@ -3307,6 +3383,39 @@ (x:xs) ?? (y:ys)  =  []  ++allowed patterns:++xs ?? ys  =  _+++xs ?? []  =  _+xs ?? (x:ys)  =  _++[] ?? xs  =  _+(x:xs) ?? ys  =  _+++[] ?? xs  =  _+(x:xs) ?? []  =  _+(x:xs) ?? (y:ys)  =  _++[] ?? []  =  _+[] ?? (x:xs)  =  _+(x:xs) ?? ys  =  _+++[] ?? []  =  _+[] ?? (x:xs)  =  _+(x:xs) ?? []  =  _+(x:xs) ?? (y:ys)  =  _+++++allowed deconstructions:++ Candidates for: ton :: Bool -> Bool   pruning with 39/49 rules   [3,1,0,0,0,0,0,0,0] direct candidates, 0 duplicates@@ -3392,6 +3501,21 @@ ton True  =  False  ++allowed patterns:++ton p  =  _+++ton False  =  _+ton True  =  _+++++allowed deconstructions:++ Candidates for: &| :: Bool -> Bool -> Bool   pruning with 39/49 rules   [4,2,2,4,2,16,17,56,110] direct candidates, 0 duplicates@@ -3721,6 +3845,39 @@ p &| q  =  not q || (p || q)  ++allowed patterns:++p &| q  =  _+++p &| False  =  _+p &| True  =  _++False &| p  =  _+True &| p  =  _+++False &| p  =  _+True &| False  =  _+True &| True  =  _++False &| False  =  _+False &| True  =  _+True &| p  =  _+++False &| False  =  _+False &| True  =  _+True &| False  =  _+True &| True  =  _+++++allowed deconstructions:++ Candidates for: gcd :: Int -> Int -> Int   pruning with 0/0 rules   [3,0,9,0,54,0,405,0,3402] direct candidates, 0 duplicates@@ -5353,4 +5510,38 @@ gcd 0 x  =  0 `mod` (0 `mod` x) gcd x y  =  0 +++allowed patterns:++gcd x y  =  _+++gcd x 0  =  _+gcd x y  =  _++gcd 0 x  =  _+gcd x y  =  _+++gcd 0 x  =  _+gcd x 0  =  _+gcd x y  =  _++gcd 0 0  =  _+gcd 0 x  =  _+gcd x y  =  _+++gcd 0 0  =  _+gcd 0 x  =  _+gcd x 0  =  _+gcd x y  =  _+++++allowed deconstructions:++x `mod` _ :: Int 

@@ -12,32 +12,36 @@ factorial 0  =  1 factorial x  =  x * factorial (x - 1) --- looking through 195 candidates of size 8+-- looking through 203 candidates of size 8+-- tested 254 candidates+factorial 1  =  1+factorial x  =  x * factorial (x - 1)+ -- looking through 1048 candidates of size 9--- tested 539 candidates+-- tested 547 candidates factorial 0  =  0 factorial 1  =  1 factorial x  =  x * factorial (x - 1) --- tested 547 candidates+-- tested 555 candidates factorial 0  =  1 factorial 1  =  1 factorial x  =  x * factorial (x - 1) --- looking through 1256 candidates of size 10--- looking through 7198 candidates of size 11--- tested 3160 candidates+-- looking through 1301 candidates of size 10+-- looking through 7201 candidates of size 11+-- tested 3216 candidates factorial 0  =  1 factorial x  =  x + x * (factorial (x - 1) - 1) --- tested 3340 candidates+-- tested 3396 candidates factorial 0  =  1 factorial x  =  x - x * (1 - factorial (x - 1)) --- tested 3463 candidates+-- tested 3519 candidates factorial 0  =  1 factorial x  =  (0 - x) * (0 - factorial (x - 1)) --- tested 9948 candidates+-- tested 10004 candidates cannot conjure 

@@ -40,7 +40,7 @@   css            =  take n                  .  discardT isRedundantByIntroduction -- additional pruning rule                  $  css'-  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates+  (css', thy, _, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates   nRules         =  length (rules thy)   nREs           =  length (equations thy) + nRules   maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark

@@ -305,9 +305,9 @@ -- looking through 28 candidates of size 5 -- looking through 35 candidates of size 6 -- looking through 167 candidates of size 7--- looking through 195 candidates of size 8+-- looking through 203 candidates of size 8 -- looking through 1048 candidates of size 9--- tested 458 candidates+-- tested 466 candidates gps17 0  =  0 gps17 x  =  gps17 (x - 1) + x * x 

@@ -320,13 +320,13 @@ -- looking through 3 candidates of size 4 -- looking through 11 candidates of size 5 -- looking through 13 candidates of size 6--- looking through 85 candidates of size 7+-- looking through 91 candidates of size 7 -- looking through 104 candidates of size 8--- looking through 811 candidates of size 9+-- looking through 850 candidates of size 9 -- looking through 923 candidates of size 10--- looking through 8602 candidates of size 11+-- looking through 8902 candidates of size 11 -- looking through 9662 candidates of size 12--- tested 20217 candidates+-- tested 20562 candidates cannot conjure  gps22 :: Int -> [Char]

@@ -7,7 +7,7 @@ -- looking through 6 candidates of size 3 -- looking through 13 candidates of size 4 -- looking through 40 candidates of size 5--- looking through 137 candidates of size 6+-- looking through 138 candidates of size 6 -- tested 69 candidates factorial 0  =  1 factorial x  =  x * factorial (dec x)

@@ -40,7 +40,7 @@   css            =  take n                  .  discardT isRedundantByIntroduction -- additional pruning rule                  $  css'-  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates+  (css', thy, _, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates   nRules         =  length (rules thy)   nREs           =  length (equations thy) + nRules   maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark

@@ -1,1 +1,1 @@-9.5+9.2

@@ -1,1 +1,1 @@-1.8+2.4

@@ -1,1 +1,1 @@-13.7+14.3

@@ -1,1 +1,1 @@-11.6+11.9

@@ -1,1 +1,1 @@-2.1+2.2

@@ -1,1 +1,1 @@-0.9+1.0

@@ -0,0 +1,1 @@+2.8

@@ -1,1 +1,1 @@-1.3+1.4

@@ -1,1 +1,1 @@-7.6+7.5

@@ -1,1 +1,1 @@-3.2+3.4

@@ -1,1 +1,1 @@-1.4+0.8

@@ -1,1 +1,1 @@-2.8+3.3

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

@@ -1,1 +1,1 @@-3.5+4.1

@@ -0,0 +1,1 @@+0.2

@@ -1,1 +1,1 @@-16.7+16.1

@@ -1,1 +1,1 @@-3.5+4.3

@@ -1,1 +1,1 @@-5.1+4.8

@@ -1,1 +1,1 @@-25.3+25.6

@@ -1,1 +1,1 @@-21.1+22.9

@@ -1,1 +1,1 @@-3.0+2.9

@@ -1,1 +1,1 @@-5.7+5.6

@@ -1,1 +1,1 @@-8.2+8.0

@@ -1,1 +1,1 @@-14.1+13.6

@@ -1,1 +1,1 @@-4.3+4.0

@@ -1,1 +1,1 @@-4.9+4.6

@@ -1,1 +1,1 @@-1.9+1.7

@@ -0,0 +1,1 @@+5.6

@@ -1,1 +1,1 @@-3.4+2.6

@@ -1,1 +1,1 @@-14.4+13.8

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

@@ -1,1 +1,1 @@-6.6+6.2

@@ -1,1 +1,1 @@-0.3+0.2

@@ -1,1 +1,1 @@-2.4+2.2

@@ -1,1 +1,1 @@-2.8+1.4

@@ -1,1 +1,1 @@-5.4+5.9

@@ -1,1 +1,1 @@-1.2+1.1

@@ -1,1 +1,1 @@-0.0+0.1

@@ -1,1 +1,1 @@-1.0+0.9

@@ -1,1 +1,1 @@-3.8+1.0

@@ -1,1 +1,1 @@-0.6+0.5

@@ -1,1 +1,1 @@-3.0+2.7

@@ -1,1 +1,1 @@-6.8+7.3

@@ -1,1 +1,1 @@-0.6+0.3

@@ -1,1 +1,1 @@-2.1+1.4

@@ -1,1 +1,1 @@-0.6+0.5

@@ -1,1 +1,1 @@-2.6+2.5

@@ -0,0 +1,1 @@+0.4

@@ -67,9 +67,9 @@ -- looking through 12 candidates of size 3 -- looking through 24 candidates of size 4 -- looking through 37 candidates of size 5--- looking through 70 candidates of size 6+-- looking through 72 candidates of size 6 -- looking through 196 candidates of size 7--- tested 163 candidates+-- tested 165 candidates factorial 0  =  1 factorial x  =  x * factorial (x - 1) @@ -82,9 +82,9 @@ -- looking through 12 candidates of size 3 -- looking through 24 candidates of size 4 -- looking through 47 candidates of size 5--- looking through 70 candidates of size 6+-- looking through 82 candidates of size 6 -- looking through 342 candidates of size 7--- tested 272 candidates+-- tested 284 candidates factorial 0  =  1 factorial x  =  x * factorial (x - 1) @@ -97,9 +97,9 @@ -- looking through 21 candidates of size 3 -- looking through 42 candidates of size 4 -- looking through 302 candidates of size 5--- looking through 600 candidates of size 6+-- looking through 602 candidates of size 6 -- looking through 6115 candidates of size 7--- tested 999 candidates+-- tested 1001 candidates factorial 0  =  1 factorial x  =  x * factorial (x - 1) @@ -127,9 +127,9 @@ -- looking through 21 candidates of size 3 -- looking through 42 candidates of size 4 -- looking through 330 candidates of size 5--- looking through 600 candidates of size 6+-- looking through 630 candidates of size 6 -- looking through 7215 candidates of size 7--- tested 1915 candidates+-- tested 1945 candidates factorial 0  =  1 factorial x  =  x * factorial (x - 1) 

@@ -46,7 +46,7 @@   css            =  take n                  $  discardT isRedundantByIntroduction -- additional pruning rule                  $  css'-  (css', thy, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates+  (css', thy, _, _) =  candidateDefnsC args nm f ps  -- Conjure uses this for listing candidates   nRules         =  length (rules thy)   nREs           =  length (equations thy) + nRules   maxTests       =  60 -- a hardcoded value probably will not hurt in this simple benchmark

@@ -24,7 +24,7 @@   conjure "^^^" (^^^) primitives   conjureWith args{usePatterns = False} "^^^" (^^^) primitives -  -- This example is quite degenerate,+  -- This example is quite the degenerate case,   -- it takes a while to conjure even with just 2 primitives.   -- I am leaving it commented-out for now...   -- conjure "thirty" thirty [pr (0::Int), prim "+" ((+) :: Int -> Int -> Int)]

@@ -2,6 +2,18 @@ ============================  +v0.6.2 (February 2025)+----------------------++* don't require 0 as a base case by default+  (defalt to `requireZero=False`)+* add switch to limit the size of constant sub-expressions+  (`Args.maxConstantSize`)+* add switch to enable showing of allowed patterns+  (`Args.showPatterns`)+* update examples++ v0.6.0 (February 2025) ---------------------- 

@@ -3,7 +3,7 @@ -- Copyright (C) 2021-2025 Rudy Matela -- Distributed under the 3-Clause BSD licence (see the file LICENSE). name:                code-conjure-version:             0.6.0+version:             0.6.2 synopsis:            synthesize Haskell functions out of partial definitions description:   Conjure is a tool that synthesizes Haskell functions out of partial definitions.@@ -68,7 +68,7 @@ source-repository this   type:            git   location:        https://github.com/rudymatela/conjure-  tag:             v0.6.0+  tag:             v0.6.2  library   exposed-modules: Conjure

@@ -0,0 +1,40 @@+-- bits.hs: functions over bits+--+-- Copyright (C) 2025 Rudy Matela+-- Distributed under the 3-Clause BSD licence (see the file LICENSE).+import Conjure++-- binary digit sum+-- binaryDigitSum+bitsum :: Int -> Int+bitsum 0  =  0  --   0+bitsum 1  =  1  --   1+bitsum 2  =  1  --  10+bitsum 3  =  2  --  11+bitsum 4  =  1  -- 100+bitsum 5  =  2  -- 101+bitsum 6  =  2  -- 110+bitsum 7  =  3  -- 111++main :: IO ()+main  =  do+  conjure "bitsum" bitsum+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , prim "halve" ((`div` 2) :: Int -> Int)+    , prim "parity" ((`mod` 2) :: Int -> Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    ]+  -- bitsum 0  =  0+  -- bitsum n  =  parity n + bitsum (halve n)++  conjure "bitsum" bitsum+    [ pr (0 :: Int)+    , pr (1 :: Int)+    , pr (2 :: Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "`div`" (div :: Int -> Int -> Int)+    , prim "`mod`" (mod :: Int -> Int -> Int)+    ]+  -- bitsum 0  =  0+  -- bitsum n  =  n `mod` 2 + bitsum (n `div` 2)

@@ -0,0 +1,30 @@+bitsum :: Int -> Int+-- testing 8 combinations of argument values+-- pruning with 21/25 rules+-- looking through 3 candidates of size 1+-- looking through 3 candidates of size 2+-- looking through 5 candidates of size 3+-- looking through 10 candidates of size 4+-- looking through 26 candidates of size 5+-- looking through 68 candidates of size 6+-- looking through 182 candidates of size 7+-- tested 145 candidates+bitsum 0  =  0+bitsum x  =  bitsum (halve x) + parity x++bitsum :: Int -> Int+-- testing 8 combinations of argument values+-- pruning with 27/32 rules+-- looking through 4 candidates of size 1+-- looking through 2 candidates of size 2+-- looking through 17 candidates of size 3+-- looking through 16 candidates of size 4+-- looking through 246 candidates of size 5+-- looking through 239 candidates of size 6+-- looking through 4504 candidates of size 7+-- looking through 4542 candidates of size 8+-- looking through 89215 candidates of size 9+-- tested 10191 candidates+bitsum 0  =  0+bitsum x  =  bitsum (x `div` 2) + x `mod` 2+

@@ -1,19 +1,13 @@ -- count.hs: elem and set functions import Conjure +-- an idiomatic count without using filter count :: Eq a => a -> [a] -> Int count x  =  c   where   c []  =  0   c (y:ys)  =  (if x == y then 1 else 0) + c ys --- this is the expected function-countIf :: A -> [A] -> Int-countIf x xs  =  if null xs                                                 -- 3-                 then 0                                                     -- 4-                 else (if x == head xs then 1 else 0) + countIf x (tail xs) -- 16-                 --    5  6 7   8   9      10     11 12   13   14   15  16- count' :: A -> [A] -> Int count' 0 [0]  =  1 count' 0 [1]  =  0@@ -39,6 +33,8 @@     , prim "==" ((==) :: A -> A -> Bool)     ] +  -- count x []  =  0+  -- count x (y:xs)  =  count x xs + (if x == y then 1 else 0)   conjure "count" count'     [ pr (0 :: Int)     , pr (1 :: Int)

@@ -23,27 +23,29 @@  main :: IO () main  =  do-  conjureWithMaxSize 5 "fib01" fib01+  -- These two examples show that currently+  -- functions with "many" argument (>=3)+  -- are particularly hard for conjure to synthesize.+  -- I've added an item in TODO.md to address this in 2025-02.++  -- It takes about 33 seconds to run with maxSize=8+  -- running with maxSize = 5 for faster runtime+  conjureWith args{maxSize=5, maxConstantSize=1} "fib01" fib01     [ pr (0::Int)     , prim "dec" (subtract 1 :: Int -> Int)     , prim "+" ((+) :: Int -> Int -> Int)     ] -  -- takes about 22 seconds to run with maxSize=12-  conjureWith args{usePatterns = False, maxSize = 10} "fib01" fib01+  -- It takes about 27 seconds to run with maxSize=12+  -- running with maxSize = 9 for faster runtime+  conjureWith args{usePatterns = False, maxSize = 1, maxConstantSize=1} "fib01" fib01     [ pr (0::Int)     , prim "+" ((+) :: Int -> Int -> Int)     , prim "dec" (subtract 1 :: Int -> Int)     , prim "<=" ((<=) :: Int -> Int -> Bool)+    , prif (undefined :: Int)     ]--- expected function:--- fib01 x y z  =  if z <= 0 then y else fib01 y (x + y) (dec z)---                 1  2 3  4      5      6     7  8 9 10  11 12--  -- out of reach as well:-  -- conjure "fib01" fib01-  --   [ pr (0::Int)-  --   , pr (1::Int)-  --   , prim "+" ((+) :: Int -> Int -> Int)-  --   , prim "-" ((-) :: Int -> Int -> Int)-  --   ]+  -- expected function:+  -- fib01 x y z  =  if z <= 0                     -- 4+  --                 then y                        -- 5+  --                 else fib01 y (x + y) (dec z)  -- 12

@@ -11,17 +11,8 @@  fib01 :: Int -> Int -> Int -> Int -- testing 8 combinations of argument values--- pruning with 18/38 rules+-- pruning with 21/41 rules -- looking through 4 candidates of size 1--- looking through 4 candidates of size 2--- looking through 10 candidates of size 3--- looking through 16 candidates of size 4--- looking through 44 candidates of size 5--- looking through 92 candidates of size 6--- looking through 210 candidates of size 7--- looking through 520 candidates of size 8--- looking through 1197 candidates of size 9--- looking through 10436 candidates of size 10--- tested 12533 candidates+-- tested 4 candidates cannot conjure 

@@ -8,12 +8,12 @@ -- looking through 26 candidates of size 5 -- looking through 27 candidates of size 6 -- looking through 116 candidates of size 7--- looking through 102 candidates of size 8--- looking through 532 candidates of size 9--- looking through 474 candidates of size 10--- looking through 2571 candidates of size 11--- looking through 2287 candidates of size 12--- tested 3951 candidates+-- looking through 120 candidates of size 8+-- looking through 552 candidates of size 9+-- looking through 540 candidates of size 10+-- looking through 2663 candidates of size 11+-- looking through 2675 candidates of size 12+-- tested 4147 candidates fibonacci 0  =  1 fibonacci 1  =  1 fibonacci x  =  fibonacci (x - 1) + fibonacci (x - 2)

@@ -7,9 +7,9 @@ -- looking through 159 candidates of size 4 -- looking through 433 candidates of size 5 -- looking through 1382 candidates of size 6--- looking through 4118 candidates of size 7+-- looking through 4136 candidates of size 7 -- looking through 13292 candidates of size 8--- tested 6365 candidates+-- tested 6383 candidates pow x 0  =  1 pow x y  =  x * pow x (y - 1) @@ -21,7 +21,7 @@ -- looking through 58 candidates of size 3 -- looking through 174 candidates of size 4 -- looking through 485 candidates of size 5--- looking through 1369 candidates of size 6--- tested 2108 candidates+-- looking through 1387 candidates of size 6+-- tested 2126 candidates cannot conjure 

@@ -7,7 +7,7 @@ -- looking through 6 candidates of size 4 -- looking through 8 candidates of size 5 -- looking through 13 candidates of size 6--- looking through 22 candidates of size 7+-- looking through 24 candidates of size 7 -- tested 39 candidates drop 0 xs  =  xs drop x []  =  []@@ -22,10 +22,10 @@ -- looking through 6 candidates of size 4 -- looking through 8 candidates of size 5 -- looking through 13 candidates of size 6--- looking through 22 candidates of size 7--- looking through 26 candidates of size 8--- looking through 58 candidates of size 9--- tested 104 candidates+-- looking through 24 candidates of size 7+-- looking through 31 candidates of size 8+-- looking through 59 candidates of size 9+-- tested 111 candidates take 0 xs  =  [] take x []  =  [] take x (y:xs)  =  y:take (x - 1) xs

@@ -0,0 +1,18 @@+-- tri.hs: conjuring a tri function+--+-- 2025 Colin Runciman and Rudy Matela+import Conjure++tri :: Int -> Int+tri 1  =  1+tri 2  =  3+tri 3  =  6+tri 5  =  15++main :: IO ()+main  =  do+  conjure "tri" tri+    [ pr (1::Int)+    , prim "+" ((+) :: Int -> Int -> Int)+    , prim "-" ((-) :: Int -> Int -> Int)+    ]

@@ -0,0 +1,14 @@+tri :: Int -> Int+-- testing 4 combinations of argument values+-- pruning with 11/33 rules+-- looking through 2 candidates of size 1+-- looking through 0 candidates of size 2+-- looking through 5 candidates of size 3+-- looking through 5 candidates of size 4+-- looking through 10 candidates of size 5+-- looking through 8 candidates of size 6+-- looking through 41 candidates of size 7+-- tested 31 candidates+tri 1  =  1+tri x  =  x + tri (x - 1)+

@@ -292,6 +292,23 @@   src/Conjure/Conjurable.hs \   src/Conjure/Conjurable/Derive.hs \   eg/arith.hs+eg/bits: \+  eg/bits.hs \+  mk/toplibs+eg/bits.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Red.hs \+  src/Conjure/Reason.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn/Test.hs \+  src/Conjure/Defn/Redundancy.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  src/Conjure/Conjurable/Derive.hs \+  eg/bits.hs eg/bools: \   eg/bools.hs \   mk/toplibs@@ -734,6 +751,23 @@   src/Conjure/Conjurable.hs \   src/Conjure/Conjurable/Derive.hs \   eg/tree.hs+eg/tri: \+  eg/tri.hs \+  mk/toplibs+eg/tri.o: \+  src/Conjure/Utils.hs \+  src/Conjure/Red.hs \+  src/Conjure/Reason.hs \+  src/Conjure/Prim.hs \+  src/Conjure.hs \+  src/Conjure/Expr.hs \+  src/Conjure/Engine.hs \+  src/Conjure/Defn/Test.hs \+  src/Conjure/Defn/Redundancy.hs \+  src/Conjure/Defn.hs \+  src/Conjure/Conjurable.hs \+  src/Conjure/Conjurable/Derive.hs \+  eg/tri.hs mk/All.o: \   src/Conjure/Utils.hs \   src/Conjure/Red.hs \

@@ -169,8 +169,10 @@   -- ef' :$ exprExpr ex :$ exprExpr ey :$ ...   red :: Int -> Memo -> Expr -> Maybe (Int, Memo, Dynamic)   red n m e  |  size e > n  =  err "argument-size limit reached"-  -- prevent recursion into negatives:-  -- red n m e  |  any isNegative (unfoldApp e)  =  err "recursion into negatives"+  -- prevent recursion into negatives, we fail earlier in these cases+  -- we match a non-empty memo table to know that we already have a call stack+  -- red n (_:_) e | any isNegative (unfoldApp e)  =  err "recursion into negatives"+  -- the above is not correct, we need to detect which arguments are descending somehow...   red n m e  =  case lookup e m of     Just Nothing -> err $ "loop detected " ++ show e     Just (Just d) -> Just (n,m,d)

@@ -191,6 +191,7 @@   , maxEquationSize       :: Int  -- ^ maximum size of equation operands   , maxSearchTests        :: Int  -- ^ maximum number of tests to search for defined values   , maxDeconstructionSize :: Int  -- ^ maximum size of deconstructions (e.g.: @_ - 1@)+  , maxConstantSize       :: Int  -- ^ maximum size of constants (0 for no limit)    -- advanced & debug options --   , carryOn               :: Bool -- ^ whether to carry on after finding a suitable candidate@@ -198,7 +199,8 @@   , usePatterns           :: Bool -- ^ use pattern matching to create (recursive) candidates   , showCandidates        :: Bool -- ^ (debug) show candidates -- warning: wall of text   , showTests             :: Bool -- ^ (debug) show tests-  , showDeconstructions   :: Bool -- ^ (debug) show conjecture-and-allowed deconstructions+  , showPatterns          :: Bool -- ^ (debug) show possible LHS patterns+  , showDeconstructions   :: Bool -- ^ (debug) show conjectured-and-allowed deconstructions    -- pruning options --   , rewriting             :: Bool -- ^ unique-modulo-rewriting candidates@@ -231,6 +233,7 @@   , maxEquationSize        =   5   , maxSearchTests         =  100000   , maxDeconstructionSize  =   4+  , maxConstantSize        =   0 -- unlimited    -- advanced & debug options --   , carryOn                =  False@@ -239,6 +242,7 @@   , showCandidates         =  False   , showTests              =  False   , showDeconstructions    =  False+  , showPatterns           =  False    -- pruning options --   , rewriting              =  True@@ -246,11 +250,13 @@   , adHocRedundancy        =  True   , copyBindings           =  True   , atomicNumbers          =  True-  , requireZero            =  True+  , requireZero            =  False   , uniqueCandidates       =  False   } +-- TODO: remove the requireZero option from args? + -- | Like 'conjure' but allows setting options through 'Args'/'args'. -- -- > conjureWith args{maxSize = 18} "function" function [...]@@ -287,6 +293,8 @@       putStrLn $ "invalid:"       putStr   $ unlines $ map showEq $ invalid thy       putStrLn $ "-}"+  when (showPatterns args) $ do+    putStr   $ unlines $ zipWith (\i -> (("-- allowed patterns of size " ++ show i ++ "\n{-\n") ++) . (++ "-}") . unlines) [1..] $ mapT showDefn $ patternss results   when (showDeconstructions args) $ do     putStrLn $ "{- List of allowed deconstructions:"     putStr   $ unlines $ map show $ deconstructions results@@ -331,6 +339,7 @@   , candidatess :: [[Defn]]      -- ^ tiers of candidates   , bindings :: [Expr]           -- ^ test bindings used to verify candidates   , theory :: Thy                -- ^ the underlying theory+  , patternss :: [[Defn]]        -- ^ tiers of allowed patterns   , deconstructions :: [Expr]    -- ^ the list of allowed deconstructions   } @@ -370,6 +379,7 @@   , candidatess  =  candidatesT   , bindings  =  tests   , theory  =  thy+  , patternss  =  patternss   , deconstructions  =  deconstructions   }   where@@ -380,7 +390,7 @@                  && errorToFalse (p (cevl maxEvalRecursions fx))   candidatesT  =  (if uniqueCandidates then nubCandidates args nm f else id)                $  take maxSize candidatesTT-  (candidatesTT, thy, deconstructions)  =  candidateDefns args nm f es+  (candidatesTT, thy, patternss, deconstructions)  =  candidateDefns args nm f es   ffxx   =  conjureApplication nm f   vffxx  =  conjureVarApplication nm f @@ -420,7 +430,7 @@ -- 1. tiers of candidate definitions -- 2. an equational theory -- 3. a list of allowed deconstructions-candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])+candidateDefns :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [[Defn]], [Expr]) candidateDefns args  =  candidateDefns' args   where   candidateDefns'  =  if usePatterns args@@ -430,17 +440,22 @@  -- | Return apparently unique candidate definitions --   where there is a single body.-candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])-candidateDefns1 args nm f ps  =  first3 (mapT toDefn) $ candidateExprs args nm f ps+candidateDefns1 :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [[Defn]], [Expr])+candidateDefns1 args nm f ps  =  first4 (mapT toDefn) $ candidateExprs args nm f ps   where   efxs  =  conjureVarApplication nm f   toDefn e  =  [(efxs, e)]-  first3 f (x,y,z)  =  (f x, y, z)+  first4 f (x,y,z,w)  =  (f x, y, z, w)   -- | Return apparently unique candidate bodies.-candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy, [Expr])-candidateExprs Args{..} nm f ps  =  (as \/ concatMapT (`enumerateFillings` recs) ts, thy, deconstructions)+candidateExprs :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Expr]], Thy, [[Defn]], [Expr])+candidateExprs Args{..} nm f ps  =+  ( as \/ concatMapT (`enumerateFillings` recs) ts+  , thy+  , [[ [(efxs, eh)] ]]+  , deconstructions+  )   where   es  =  map fst ps   ts | typ efxs == boolTy  =  foldAppProducts andE [cs, rs]@@ -488,8 +503,13 @@  -- | Return apparently unique candidate definitions --   using pattern matching.-candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [Expr])-candidateDefnsC Args{..} nm f ps  =  (discardT hasRedundant $ concatMapT fillingsFor fss,thy,deconstructions)+candidateDefnsC :: Conjurable f => Args -> String -> f -> [Prim] -> ([[Defn]], Thy, [[Defn]], [Expr])+candidateDefnsC Args{..} nm f ps  =+  ( discardT hasRedundant $ concatMapT fillingsFor fss+  , thy+  , mapT (map (,eh)) pats+  , deconstructions+  )   where   pats  =  conjurePats es nm f   fss  =  concatMapT ps2fss pats@@ -506,9 +526,12 @@   appsWith eh vs  =  enumerateAppsFor eh k $ vs ++ es     where     k | atomicNumbers && isNumeric eh  =  \e -> keepNumeric e && keep e+      | maxConstantSize > 0            =  \e -> keepConstant e && keep e       | otherwise                      =  keep     -- discards non-atomic numeric ground expressions such as 1 + 1     keepNumeric e  =  isFun e || isConst e || not (isGround e)+    -- discards big non-atomic ground expressions such as 1 + 1 or reverse [1,2]+    keepConstant e  =  isFun e || isConst e || not (isGround e) || size e <= maxConstantSize    isRedundant | adHocRedundancy  =  \e -> isRedundantDefn e || isRedundantModuloRewriting (normalize thy) e               | otherwise        =  const False@@ -530,7 +553,7 @@     p2eess pat | copyBindings && isGroundPat f pat  =  [[(pat, toValPat f pat)]]     p2eess pat  =  mapT (pat,)                 .  appsWith pat-                .  tail+                .  drop 1 -- this excludes the function name itself                 $  vars pat ++ [eh | any (uncurry should) (zip aess aes)]       where       -- computes whether we should include a recurse for this given argument