code-conjure 0.5.14 → 0.5.16
raw patch · 66 files changed
+423/−235 lines, 66 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- .github/workflows/build.yml +7/−7
- .gitignore +1/−0
- Makefile +8/−0
- bench/candidates.txt +1/−43
- bench/gps2.txt +2/−2
- bench/runtime/lapmatrud/bench/candidates.runtime +1/−1
- bench/runtime/lapmatrud/bench/gps.runtime +1/−1
- bench/runtime/lapmatrud/bench/gps2.runtime +1/−1
- bench/runtime/lapmatrud/bench/redundants.runtime +1/−1
- bench/runtime/lapmatrud/bench/strategies.runtime +1/−1
- bench/runtime/lapmatrud/bench/terpret.runtime +1/−1
- bench/runtime/lapmatrud/bench/unique.runtime +1/−1
- bench/runtime/lapmatrud/bench/weird.runtime +1/−1
- bench/runtime/lapmatrud/eg/factorial.runtime +1/−1
- bench/runtime/lapmatrud/eg/fib01.runtime +1/−1
- bench/runtime/lapmatrud/eg/fibonacci.runtime +1/−1
- bench/runtime/lapmatrud/eg/higher.runtime +1/−1
- bench/runtime/lapmatrud/eg/ints.runtime +1/−1
- bench/runtime/lapmatrud/eg/oddeven.runtime +1/−1
- bench/runtime/lapmatrud/eg/pow.runtime +1/−1
- bench/runtime/lapmatrud/eg/setelem.runtime +1/−1
- 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/bools.runtime +1/−1
- bench/runtime/zero/eg/bst.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/list.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/spec.runtime +1/−1
- changelog.md +9/−0
- code-conjure.cabal +6/−6
- eg/bst.hs +5/−5
- eg/bst.txt +12/−9
- eg/colin/IntFuns.hs +95/−0
- eg/colin/ListFuns.hs +147/−0
- eg/gcd.txt +2/−2
- src/Conjure/Conjurable.hs +3/−29
- src/Conjure/Conjurable/Derive.hs +1/−39
- src/Conjure/Defn.hs +23/−12
- src/Conjure/Engine.hs +2/−11
- src/Conjure/Expr.hs +3/−5
- src/Conjure/Prim.hs +1/−2
- src/Conjure/Red.hs +2/−2
- src/Conjure/Utils.hs +3/−2
- stack.yaml +1/−1
- test/Test.hs +0/−4
- test/defn.hs +40/−3
- test/derive.hs +9/−9
- test/mk +1/−0
- test/red.hs +0/−1
- test/utils.hs +0/−2
.github/workflows/build.yml view
@@ -68,15 +68,15 @@ strategy: max-parallel: 6 matrix:+ # starting with 9.10, docker/_/haskell requires -bullseye as suffix ghc:+ - '9.10-bullseye' - '9.8' - '9.6' - '9.4' - '9.2' - '9.0'- - '8.10'- - '8.6'- - '8.2'+ - '8.8' runs-on: ubuntu-latest needs: build-and-test container: haskell:${{ matrix.ghc }}@@ -158,15 +158,15 @@ ~/.ghcup /usr/local/.ghcup/bin /usr/local/.ghcup/db- /usr/local/.ghcup/ghc/9.0.2+ /usr/local/.ghcup/ghc/9.4.8 key: v1-${{ runner.os }}-ghcup-${{ hashFiles('stack.yaml') }} restore-keys: v1-${{ runner.os }}-ghcup- - name: Setup Haskell's GHC and Cabal as required by current Stackage LTS uses: haskell-actions/setup@v2- with: # lts-19.19- ghc-version: '9.0.2'- cabal-version: '3.4'+ with: # lts-21.25+ ghc-version: '9.4.8'+ cabal-version: '3.8' - run: du -hd2 ~/.stack ~/.ghcup /usr/local/.ghcup || true
.gitignore view
@@ -53,6 +53,7 @@ eg/sort eg/subset eg/spec+eg/colin/*Funs bench/carry-on bench/strategies bench/self
Makefile view
@@ -1,6 +1,12 @@+# Makefile for Conjure+#+# Copyright (C) 2021-2025 Rudy Matela+# Distributed under a 3-Clause BSD license, see the LICENSE file+ GHCIMPORTDIRS = src:test GHCFLAGS = -O2 -v0 \ $(shell grep -q "Arch Linux" /etc/lsb-release && echo -dynamic)+# -Wall -Werror -Wno-unused-matches -Wno-orphans -Wno-name-shadowing -Wno-incomplete-uni-patterns -Wno-unused-pattern-binds HADDOCKFLAGS = \ -i $(shell find ~/.cabal -name leancheck.haddock | tail -1) \ -i $(shell find ~/.cabal -name express.haddock | tail -1) \@@ -111,6 +117,8 @@ test-via-stack: stack test code-conjure:test:expr --ghc-options="$(GHCFLAGS) -O0" --system-ghc --no-install-ghc --no-terminal +test-on-ghc-9.10:+ make test GHC=ghc-9.10 GHCIMPORTDIRS=src:test:../leancheck/src:../express/src:../speculate/src fastest: $(LONG) make test -j$(NJOBS)
bench/candidates.txt view
@@ -3724,7 +3724,7 @@ Candidates for: gcd :: Int -> Int -> Int pruning with 0/0 rules [3,0,9,0,54,0,405,0,3402] direct candidates, 0 duplicates- [3,6,11,50,98,344,792,2956,6945] pattern candidates, 0 duplicates+ [3,6,11,50,98,330,774,2714,6660] pattern candidates, 0 duplicates no rules. @@ -4370,9 +4370,6 @@ gcd x y = gcd x (y `mod` y) gcd x 0 = x-gcd x y = gcd x (0 `mod` y)--gcd x 0 = x gcd x y = gcd y (x `mod` x) gcd x 0 = x@@ -4385,21 +4382,12 @@ gcd x y = gcd y (y `mod` y) gcd x 0 = x-gcd x y = gcd y (0 `mod` x)--gcd x 0 = x-gcd x y = gcd y (0 `mod` y)--gcd x 0 = x gcd x y = gcd 0 (x `mod` y) gcd x 0 = x gcd x y = gcd 0 (y `mod` y) gcd x 0 = x-gcd x y = gcd 0 (0 `mod` y)--gcd x 0 = x gcd x y = gcd (x `mod` x) x gcd x 0 = x@@ -4417,15 +4405,6 @@ gcd x 0 = x gcd x y = gcd (y `mod` y) x -gcd x 0 = x-gcd x y = gcd (0 `mod` x) x--gcd x 0 = x-gcd x y = gcd (0 `mod` x) y--gcd x 0 = x-gcd x y = gcd (0 `mod` y) x- gcd 0 x = x gcd x y = gcd x (x `mod` y) @@ -4433,9 +4412,6 @@ gcd x y = gcd x (y `mod` y) gcd 0 x = x-gcd x y = gcd x (0 `mod` y)--gcd 0 x = x gcd x y = gcd y (x `mod` x) gcd 0 x = x@@ -4448,12 +4424,6 @@ gcd x y = gcd y (y `mod` y) gcd 0 x = x-gcd x y = gcd y (0 `mod` x)--gcd 0 x = x-gcd x y = gcd y (0 `mod` y)--gcd 0 x = x gcd x y = gcd (x `mod` x) x gcd 0 x = x@@ -4476,18 +4446,6 @@ gcd 0 x = x gcd x y = gcd (y `mod` y) x--gcd 0 x = x-gcd x y = gcd (0 `mod` x) x--gcd 0 x = x-gcd x y = gcd (0 `mod` x) y--gcd 0 x = x-gcd x y = gcd (0 `mod` x) 0--gcd 0 x = x-gcd x y = gcd (0 `mod` y) x gcd x 0 = x gcd x y = (x `mod` x) `mod` x
bench/gps2.txt view
@@ -171,8 +171,8 @@ -- looking through 11 candidates of size 3 -- looking through 50 candidates of size 4 -- looking through 98 candidates of size 5--- looking through 344 candidates of size 6--- tested 173 candidates+-- looking through 330 candidates of size 6+-- tested 172 candidates gcd x 0 = x gcd x y = gcd y (x `mod` y)
bench/runtime/lapmatrud/bench/candidates.runtime view
@@ -1,1 +1,1 @@-9.1+9.9
bench/runtime/lapmatrud/bench/gps.runtime view
@@ -1,1 +1,1 @@-14.1+14.7
bench/runtime/lapmatrud/bench/gps2.runtime view
@@ -1,1 +1,1 @@-12.1+12.5
bench/runtime/lapmatrud/bench/redundants.runtime view
@@ -1,1 +1,1 @@-2.9+3.0
bench/runtime/lapmatrud/bench/strategies.runtime view
@@ -1,1 +1,1 @@-4.4+4.5
bench/runtime/lapmatrud/bench/terpret.runtime view
@@ -1,1 +1,1 @@-7.9+8.5
bench/runtime/lapmatrud/bench/unique.runtime view
@@ -1,1 +1,1 @@-2.2+2.3
bench/runtime/lapmatrud/bench/weird.runtime view
@@ -1,1 +1,1 @@-2.7+2.8
bench/runtime/lapmatrud/eg/factorial.runtime view
@@ -1,1 +1,1 @@-1.3+1.4
bench/runtime/lapmatrud/eg/fib01.runtime view
@@ -1,1 +1,1 @@-1.4+1.5
bench/runtime/lapmatrud/eg/fibonacci.runtime view
@@ -1,1 +1,1 @@-3.3+3.5
bench/runtime/lapmatrud/eg/higher.runtime view
@@ -1,1 +1,1 @@-0.6+0.7
bench/runtime/lapmatrud/eg/ints.runtime view
@@ -1,1 +1,1 @@-0.5+0.6
bench/runtime/lapmatrud/eg/oddeven.runtime view
@@ -1,1 +1,1 @@-1.5+1.6
bench/runtime/lapmatrud/eg/pow.runtime view
@@ -1,1 +1,1 @@-4.1+4.2
bench/runtime/lapmatrud/eg/setelem.runtime view
@@ -1,1 +1,1 @@-1.1+1.2
bench/runtime/zero/bench/candidates.runtime view
@@ -1,1 +1,1 @@-17.3+19.5
bench/runtime/zero/bench/carry-on.runtime view
@@ -1,1 +1,1 @@-4.9+4.5
bench/runtime/zero/bench/erroneous.runtime view
@@ -1,1 +1,1 @@-6.4+5.0
bench/runtime/zero/bench/gps.runtime view
@@ -1,1 +1,1 @@-28.9+29.6
bench/runtime/zero/bench/gps2.runtime view
@@ -1,1 +1,1 @@-24.4+22.6
bench/runtime/zero/bench/p12.runtime view
@@ -1,1 +1,1 @@-3.3+3.1
bench/runtime/zero/bench/redundants.runtime view
@@ -1,1 +1,1 @@-8.1+6.1
bench/runtime/zero/bench/strategies.runtime view
@@ -1,1 +1,1 @@-8.1+8.2
bench/runtime/zero/bench/terpret.runtime view
@@ -1,1 +1,1 @@-14.5+14.7
bench/runtime/zero/bench/unique.runtime view
@@ -1,1 +1,1 @@-4.5+4.4
bench/runtime/zero/bench/weird.runtime view
@@ -1,1 +1,1 @@-6.3+5.0
bench/runtime/zero/eg/arith.runtime view
@@ -1,1 +1,1 @@-1.8+1.9
bench/runtime/zero/eg/bools.runtime view
@@ -1,1 +1,1 @@-3.2+3.3
bench/runtime/zero/eg/bst.runtime view
@@ -1,1 +1,1 @@-14.0+14.5
bench/runtime/zero/eg/factorial.runtime view
@@ -1,1 +1,1 @@-2.4+2.5
bench/runtime/zero/eg/fib01.runtime view
@@ -1,1 +1,1 @@-2.6+2.7
bench/runtime/zero/eg/fibonacci.runtime view
@@ -1,1 +1,1 @@-8.1+6.3
bench/runtime/zero/eg/higher.runtime view
@@ -1,1 +1,1 @@-1.1+1.3
bench/runtime/zero/eg/list.runtime view
@@ -1,1 +1,1 @@-2.4+2.1
bench/runtime/zero/eg/oddeven.runtime view
@@ -1,1 +1,1 @@-2.7+2.9
bench/runtime/zero/eg/pow.runtime view
@@ -1,1 +1,1 @@-8.6+8.8
bench/runtime/zero/eg/replicate.runtime view
@@ -1,1 +1,1 @@-0.6+0.7
bench/runtime/zero/eg/spec.runtime view
@@ -1,1 +1,1 @@-1.3+1.1
changelog.md view
@@ -2,6 +2,15 @@ ============================ +v0.5.16 (January 2025)+----------------------++* slightly improve search space pruning+* slightly cleanup code+* fix build of tests on GHC >= 9.10+* improve tests and CI scripts++ v0.5.14 (February 2024) -----------------------
code-conjure.cabal view
@@ -3,7 +3,7 @@ -- Copyright (C) 2021-2024 Rudy Matela -- Distributed under the 3-Clause BSD licence (see the file LICENSE). name: code-conjure-version: 0.5.14+version: 0.5.16 synopsis: synthesize Haskell functions out of partial definitions description: Conjure is a tool that synthesizes Haskell functions out of partial definitions.@@ -29,6 +29,7 @@ , bench/*.txt , eg/*.hs , eg/*.txt+ , eg/colin/*.hs , proto/*.hs , proto/*.txt , mk/All.hs@@ -51,14 +52,13 @@ , bench/time , test/mk , test/sdist-tested-with: GHC==9.8+tested-with: GHC==9.10+ , GHC==9.8 , GHC==9.6 , GHC==9.4 , GHC==9.2 , GHC==9.0- , GHC==8.10- , GHC==8.6- , GHC==8.2+ , GHC==8.8 source-repository head type: git@@ -67,7 +67,7 @@ source-repository this type: git location: https://github.com/rudymatela/conjure- tag: v0.5.14+ tag: v0.5.16 library exposed-modules: Conjure
eg/bst.hs view
@@ -133,17 +133,17 @@ , primOrdCaseFor (undefined :: Bool) ] - -- simply out of reach performance-wise (reaching 16 but need size 26)+ -- simply out of reach performance-wise (reaching 16 but need size 22) conjureWithMaxSize 12 "insert" insert [ pr Leaf , prim "Node" Node , prim "unit" unit- , prim "==" ((==) :: Int -> Int -> Bool)- , prim "<" ((<) :: Int -> Int -> Bool)- , prif (undefined :: Tree)+ , prim "`compare`" (compare :: Int -> Int -> Ordering)+ , primOrdCaseFor (undefined :: Tree) ] -- out of reach performance-wise (reaching 16 but need 19)+ -- cf. the primOrdCaseFor version below conjureFromSpecWith args{maxSize = 12} "before" beforeSpec [ pr Leaf , prim "Node" Node@@ -170,7 +170,7 @@ , primOrdCaseFor (undefined :: Tree) ] - -- out of reach (reaching 11 but need 13)+ -- out of reach (reaching 12 but need 13) conjureWith args{maxSize = 9} "union" union [ pr Leaf , prim "Node" Node
eg/bst.txt view
@@ -34,24 +34,27 @@ -- looking through 384 candidates of size 12 -- tested 371 candidates mem x Leaf = False-mem x (Node t1 y t2) = case x `compare` y of LT -> mem x t1; EQ -> True; GT -> mem x t2+mem x (Node t1 y t2) = case x `compare` y of+ LT -> mem x t1+ EQ -> True+ GT -> mem x t2 insert :: Int -> Tree -> Tree -- testing 360 combinations of argument values--- pruning with 6/7 rules+-- pruning with 2/3 rules -- looking through 2 candidates of size 1 -- looking through 2 candidates of size 2 -- looking through 0 candidates of size 3 -- looking through 4 candidates of size 4 -- looking through 21 candidates of size 5 -- looking through 0 candidates of size 6--- looking through 86 candidates of size 7--- looking through 239 candidates of size 8--- looking through 104 candidates of size 9--- looking through 1558 candidates of size 10--- looking through 3555 candidates of size 11--- looking through 4028 candidates of size 12--- tested 9599 candidates+-- looking through 74 candidates of size 7+-- looking through 335 candidates of size 8+-- looking through 32 candidates of size 9+-- looking through 1504 candidates of size 10+-- looking through 6708 candidates of size 11+-- looking through 1760 candidates of size 12+-- tested 10442 candidates cannot conjure before :: Int -> Tree -> Tree
+ eg/colin/IntFuns.hs view
@@ -0,0 +1,95 @@+-- 2021 Colin Runciman+-- Updated in 2024 to use the new Conjure interface+import Conjure+import Prelude hiding (exp)++tri :: Int -> Int+tri 1 = 1+tri 2 = 3+tri 3 = 6+tri 5 = 15++-- hoping for something like+-- tri x = if x==1 then 1 else x + tri (dec x)++triPrimitives :: [Prim]+triPrimitives =+ [ prim "==" ((==) :: Int -> Int -> Bool)+ , pr (1::Int)+ , prim "+" ((+) :: Int -> Int -> Int)+ , prim "dec" ((\x -> x-1) :: Int -> Int)+ ]++-- looking through 3039 candidates, 25% match, 1/4 assignments+-- tri x = if x == 1 then 1 else tri x++fib :: Int -> Int+fib 0 = 1+fib 1 = 1+fib 2 = 2+fib 5 = 8+fib 6 = 13+fib 7 = 21++-- hoping for something like+-- fib x = if x <= 1 then 1 else fib (dec (dec x)) + fib (dec x)+-- 1 2 3 4 5 6 7 8 9 10 11 12 13+fibPrimitives :: [Prim]+fibPrimitives =+ [ prim "<=" ((<=) :: Int -> Int -> Bool)+ , pr (0::Int)+ , pr (1::Int)+ , prim "+" ((+) :: Int -> Int -> Int)+ , prim "dec" ((\x -> x-1) :: Int -> Int)+ ]++-- looking through 23418 candidates+-- cannot conjure++exp :: Int -> Int+exp 1 = 1+exp 2 = 4+exp 3 = 27+exp 5 = 3125++-- hoping for+-- exp x = product (replicate x x)+expPrimitives :: [Prim]+expPrimitives =+ [ prim "replicate" (replicate :: Int -> Int -> [Int])+ , prim "product" (product :: [Int] -> Int)+ ]++-- looking through 18 candidates+-- cannot conjure++pri :: Int -> Bool+pri 1 = False+pri 2 = True+pri 3 = True+pri 4 = False+pri 5 = True+pri 6 = False+pri 7 = True++-- hoping for something like+-- pri p = factors p == list2 1 p+priPrimitives :: [Prim]+priPrimitives =+ [ prim "==" ((==) :: [Int] -> [Int] -> Bool)+ , prim "factors" ((\n -> filter (\k -> n `mod` k == 0) [1..n]) :: Int -> [Int])+ , prim "list2" ((\i j -> [i,j]) :: Int -> Int -> [Int])+ , pr (1 :: Int)+ ]++-- looking through 38 candidates, 100% match, 7/7 assignments+-- pri x = factors x == list2 1 x+-- BINGO!++main :: IO ()+main = do+ conjureWithMaxSize 10 "tri" tri triPrimitives+ conjureWith args{maxSize=13} "fib" fib fibPrimitives+ conjure "exp" exp expPrimitives+ conjure "pri" pri priPrimitives+
+ eg/colin/ListFuns.hs view
@@ -0,0 +1,147 @@+-- 2021 Colin Runciman+-- updated in 2024 to use the recent interface of Conjure+import Conjure+import Prelude hiding (sum, take, drop)++sumSpec :: ([Int] -> Int) -> Bool+sumSpec sum = and [ sum [] == 0+ , sum [0,1] == 1+ , sum [1,0,1] == 2 ]++-- hoping for something like+-- sum xs = if null xs then 0 else head xs + sum (tail xs)++sumPrimitives :: [Prim]+sumPrimitives =+ [ prim "null" (null :: [Int] -> Bool)+ , pr (0::Int)+ , prim "+" ((+) :: Int -> Int -> Int)+ , prim "head" (head :: [Int] -> Int)+ , prim "tail" (tail :: [Int] -> [Int])+ ]++appSpec :: ([Int] -> [Int] -> [Int]) -> Bool+appSpec (++) = and [ [] ++ [0,1] == [0,1]+ , [0,1] ++ [] == [0,1]+ , [0,1] ++ [0,1] == [0,1,0,1] ]++-- hoping for something like+-- app xs ys = if null xs then ys else head xs : app (tail xs) ys++appPrimitives :: [Prim]+appPrimitives =+ [ prim "null" (null :: [Int] -> Bool)+ , prim ":" ((:) :: Int -> [Int] -> [Int])+ , prim "head" (head :: [Int] -> Int)+ , prim "tail" (tail :: [Int] -> [Int])+ ]++memSpec :: (Int -> [Int] -> Bool) -> Bool+memSpec mem = and [ 0 `mem` [] == False+ , 0 `mem` [0,1,1] == True+ , 0 `mem` [1,0,1] == True+ , 0 `mem` [1,1,0] == True+ , 0 `mem` [1,1,1] == False ]++-- hoping for something like+-- mem x xs = not (null xs) && (x == head xs || mem x (tail xs))++memPrimitives :: [Prim]+memPrimitives =+ [ pr False+ , pr True+ , pr ([] :: [Int])+ , prim ":" ((:) :: Int -> [Int] -> [Int])+ , prim "null" (null :: [Int] -> Bool)+ , prim "==" ((==) :: Int -> Int -> Bool)+ , prim "not" (not :: Bool -> Bool)+ , prim "&&" ((&&) :: Bool -> Bool -> Bool)+ , prim "||" ((||) :: Bool -> Bool -> Bool)+ , prim "head" (head :: [Int] -> Int)+ , prim "tail" (tail :: [Int] -> [Int])+ ]++setSpec :: ([Int] -> Bool) -> Bool+setSpec set = and [ set [] == True+ , set [0] == True+ , set [0,0] == False+ , set [0,1] == True+ , set [0,1,2] == True+ , set [0,0,1] == False+ , set [0,1,0] == False+ , set [0,1,1] == False ]++-- hoping for something like+-- set xs = null xs || not (elem (head xs) (tail xs)) && set (tail xs)++setPrimitives :: [Prim]+setPrimitives =+ [ prim "null" (null :: [Int] -> Bool)+ , pr False+ , pr True+ , pr ([] :: [Int])+ , prim ":" ((:) :: Int -> [Int] -> [Int])+ , prim "not" (not :: Bool -> Bool)+ , prim "&&" ((&&) :: Bool -> Bool -> Bool)+ , prim "||" ((||) :: Bool -> Bool -> Bool)+ , prim "head" (head :: [Int] -> Int)+ , prim "tail" (tail :: [Int] -> [Int])+ , prim "elem" (elem :: Int -> [Int] -> Bool)+ ]++takeSpec :: (Int -> [Int] -> [Int]) -> Bool+takeSpec take = and [ take 0 [] == []+ , take 1 [] == []+ , take 0 [0,1] == []+ , take 1 [0,1] == [0]+ , take 2 [0,1] == [0,1]+ , take 3 [0,1] == [0,1] ]++-- hoping for something like+-- take n xs = if n==0 || null xs then [] else head xs : take (dec n) (tail xs)++takePrimitives :: [Prim]+takePrimitives =+ [ pr (0 :: Int)+ , pr ([] :: [Int])+ , prim "null" (null :: [Int] -> Bool)+ , prim "==" ((==) :: Int -> Int -> Bool)+ , prim "||" ((||) :: Bool -> Bool -> Bool)+ , prim "dec" ((\n -> n-1) :: Int -> Int)+ , prim ":" ((:) :: Int -> [Int] -> [Int])+ , prim "head" (head :: [Int] -> Int)+ , prim "tail" (tail :: [Int] -> [Int])+ ]++dropSpec :: (Int -> [Int] -> [Int]) -> Bool+dropSpec drop = and [ drop 0 [] == []+ , drop 1 [] == []+ , drop 0 [0,1] == [0,1]+ , drop 1 [0,1] == [1]+ , drop 2 [0,1] == []+ , drop 3 [0,1] == [] ]++-- hoping for something like+-- drop n xs = if n==0 || null xs then xs else drop (dec n) (tail xs)++dropPrimitives :: [Prim]+dropPrimitives =+ [ pr (0 :: Int)+ , pr ([] :: [Int])+ , prim ":" ((:) :: Int -> [Int] -> [Int])+ , prim "null" (null :: [Int] -> Bool)+ , prim "==" ((==) :: Int -> Int -> Bool)+ , prim "||" ((||) :: Bool -> Bool -> Bool)+ , prim "dec" ((\n -> n-1) :: Int -> Int)+ , prim "tail" (tail :: [Int] -> [Int])+ ]++main :: IO ()+main = do+ conjureFromSpecWith args{maxSize=15} "sum" sumSpec sumPrimitives+ conjureFromSpecWith args{maxSize=15} "app" appSpec appPrimitives+ conjureFromSpecWith args{maxSize=15} "mem" memSpec memPrimitives+ conjureFromSpecWith args{maxSize=15} "set" setSpec setPrimitives+ conjureFromSpecWith args{maxSize=20} "take" takeSpec takePrimitives+ conjureFromSpecWith args{maxSize=15} "drop" dropSpec dropPrimitives+
eg/gcd.txt view
@@ -6,8 +6,8 @@ -- looking through 11 candidates of size 3 -- looking through 50 candidates of size 4 -- looking through 98 candidates of size 5--- looking through 344 candidates of size 6--- tested 173 candidates+-- looking through 330 candidates of size 6+-- tested 172 candidates gcd x 0 = x gcd x y = gcd y (x `mod` y)
src/Conjure/Conjurable.hs view
@@ -47,12 +47,11 @@ import Test.LeanCheck import Test.LeanCheck.Utils import Test.LeanCheck.Error (errorToFalse)-import Conjure.Expr hiding (application)+import Conjure.Expr import Conjure.Defn-import Data.Functor ((<$>))-import Control.Applicative ((<*>))+-- import Data.Functor ((<$>))+-- import Control.Applicative ((<*>)) import Data.Dynamic-import Data.Express import Data.Int -- for instances import Data.Word -- for instances@@ -78,25 +77,6 @@ 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.@@ -671,12 +651,6 @@ mk h [] = mapT (++ [h]) $ setsOf [[e] | e <- es, typ e == typ h] -- deal with types that have cases, such as lists, maybes, etc. mk h cs = [[[h]], [cs]]---prods :: [[a]] -> [[a]]-prods = foldr (productWith (:)) [[]]- where- productWith (?) xs ys = [x ? y | x <- xs, y <- ys] -- -- -- other Conjurable instances -- -- --
src/Conjure/Conjurable/Derive.hs view
@@ -15,17 +15,10 @@ import Test.LeanCheck import Test.LeanCheck.Derive-import Test.LeanCheck.Utils import Conjure.Expr hiding (mkName, Name, isInstanceOf) import Conjure.Conjurable hiding (Name)-import Data.Express.Utils (primeCycle) import Data.Express.Utils.TH -import Control.Monad-import Data.Char-import Data.List-import Language.Haskell.TH.Lib- #if __GLASGOW_HASKELL__ < 710 import Data.Functor ((<$>)) #endif@@ -120,12 +113,10 @@ , v <- vs] cs <- typeConstructorsArgNames t asName <- newName "x"- let withTheReturnTypeOfs = deriveWithTheReturnTypeOfs $ [length ns | (_,ns) <- cs] let inst = [d| instance Conjurable $(return nt) where conjureExpress = reifyExpress conjureEquality = reifyEquality conjureTiers = reifyTiers |]- -- withTheReturnTypeOfs |++| (cxt |=>| inst) cxt |=>| inst `addFun` deriveSize t `mergeI` deriveSubTypes t `mergeI` deriveCases t deriveCases :: Name -> DecsQ@@ -186,36 +177,6 @@ reallyDeriveConjurableCascading :: Name -> DecsQ reallyDeriveConjurableCascading = reallyDeriveCascading ''Conjurable reallyDeriveConjurable -deriveWithTheReturnTypeOfs :: [Int] -> DecsQ-deriveWithTheReturnTypeOfs =- fmap concat . mapM deriveWithTheReturnTypeOf . nubSort--deriveWithTheReturnTypeOf :: Int -> DecsQ-deriveWithTheReturnTypeOf n = do- mf <- lookupValueName name- case mf of- Nothing -> reallyDeriveWithTheReturnTypeOf n- Just _ -> return []- where- name = "-" ++ replicate n '>' ++ ":"--reallyDeriveWithTheReturnTypeOf :: Int -> DecsQ-reallyDeriveWithTheReturnTypeOf n = do- td <- sigD name theT- vd <- [d| $(varP name) = const |]- return $ td:vd- where- theT = bind [t| $(theFunT) -> $(last vars) -> $(theFunT) |]- theFunT = foldr1 funT vars- funT t1 t2 = [t| $(t1) -> $(t2) |]- vars = map (varT . mkName) . take (n+1) . primeCycle $ map (:"") ['a'..'z']- name = mkName $ "-" ++ replicate n '>' ++ ":"-#if __GLASGOW_HASKELL__ >= 800- bind = id -- unbound variables are automatically bound-#else- bind = toBoundedQ-#endif- addFun :: DecsQ -> DecsQ -> DecsQ qds1 `addFun` qds2 = do ds1 <- qds1 ds2 <- qds2@@ -226,3 +187,4 @@ #else [InstanceD o c ts ds1] `m` ds2 = [InstanceD o c ts (ds1 ++ ds2)] #endif+ _ `m` _ = error "Conjurable.Derive.addFun: unhandled case"
src/Conjure/Defn.hs view
@@ -38,12 +38,9 @@ import Conjure.Utils import Conjure.Expr-import Data.Express-import Data.Express.Express-import Data.Express.Fixtures+import Data.Express.Utils.Typeable (boolTy, orderingTy) import Data.Dynamic-import Control.Applicative ((<$>)) -- for older GHCs-import Test.LeanCheck.Utils ((-:>), classifyOn)+-- import Control.Applicative ((<$>)) -- for older GHCs -- | A function definition as a list of top-level case bindings ('Bndn'). --@@ -72,13 +69,24 @@ showDefn :: Defn -> String showDefn = unlines . map show1 where- show1 (lhs,Value "if" _ :$ c :$ t :$ e) = lhseqs ++ "if " ++ showExpr c- ++ "\n" ++ spaces ++ "then " ++ showExpr t- ++ "\n" ++ spaces ++ "else " ++ showExpr e- where- lhseqs = showExpr lhs ++ " = "- spaces = map (const ' ') lhseqs- show1 (lhs,rhs) = showExpr lhs ++ " = " ++ showExpr rhs+ show1 (lhs,rhs) =+ case rhs of+ (Value "if" _ :$ c :$ t :$ e) -> lhseqs ++ "if " ++ showExpr c+ ++ "\n" ++ spaces ++ "then " ++ showExpr t+ ++ "\n" ++ spaces ++ "else " ++ showExpr e+ (Value "case" _ :$ ep :$ ex :$ ey)+ | typ ep == boolTy -> lhseqs ++ "case " ++ showExpr ep ++ " of"+ ++ "\n" ++ spaces ++ "False -> " ++ showExpr ex+ ++ "\n" ++ spaces ++ "True -> " ++ showExpr ey+ (Value "case" _ :$ eo :$ ex :$ ey :$ ez)+ | typ eo == orderingTy -> lhseqs ++ "case " ++ showExpr eo ++ " of"+ ++ "\n" ++ spaces ++ "LT -> " ++ showExpr ex+ ++ "\n" ++ spaces ++ "EQ -> " ++ showExpr ey+ ++ "\n" ++ spaces ++ "GT -> " ++ showExpr ez+ _ -> lhseqs ++ showExpr rhs+ where+ lhseqs = showExpr lhs ++ " = "+ spaces = map (const ' ') lhseqs -- | Pretty-prints a 'Defn' to the screen. --@@ -203,8 +211,11 @@ -- In other words, this only works when the given 'Defn' is a singleton list -- whose first value of the only element is a simple application without -- constructors.+--+-- TODO: remove this from the interface? devalFast :: Typeable a => (Expr -> Expr) -> Int -> Defn -> a -> Expr -> a devalFast _ n [defn] x = reval defn n x+devalFast _ _ _ _ = error "devalFast: only works for singleton definitions" -- | Evaluates an 'Expr' expression into a regular Haskell value -- using a 'Defn' definition when it is found in the given expression.
src/Conjure/Engine.hs view
@@ -45,7 +45,6 @@ import Test.LeanCheck import Test.LeanCheck.Tiers import Test.LeanCheck.Error (errorToFalse)-import Test.LeanCheck.Utils (classifyOn) import Conjure.Expr import Conjure.Conjurable@@ -245,6 +244,7 @@ pr 1 0 rs where showEq eq = showExpr (fst eq) ++ " == " ++ showExpr (snd eq)+ pr :: Int -> Int -> [([Defn], [Defn])] -> IO () pr n t [] = do putStrLn $ "-- tested " ++ show t ++ " candidates" putStrLn $ "cannot conjure\n" pr n t ((is,cs):rs) = do@@ -314,7 +314,6 @@ (candidatesTT, thy) = candidateDefns args nm f es ffxx = conjureApplication nm f vffxx = conjureVarApplication nm f- (rrff:xxs) = unfoldApp vffxx requal dfn e1 e2 = isTrueWhenDefined dfn (e1 -==- e2) (-==-) = conjureMkEquation f@@ -420,7 +419,7 @@ eh = holeAsTypeOf efxs efxs = conjureVarApplication nm f- (ef:exs) = unfoldApp efxs+ (ef:_) = unfoldApp efxs keep | rewriting = isRootNormalC thy . fastMostGeneralVariation | otherwise = const True@@ -575,14 +574,6 @@ --- tiers utils -----productsThat :: (a -> [a] -> Bool) -> [ [[a]] ] -> [[ [a] ]]-productsThat p = foldr (productWithThat (:) p) [[[]]]--productWithThat :: (a->b->c) -> (a->b->Bool) -> [[a]] -> [[b]] -> [[c]]-productWithThat f p xss yss = mapT (uncurry f)- . filterT (uncurry p)- $ xss >< yss productsWith :: ([a] -> a) -> [ [[a]] ] -> [[a]] productsWith f = mapT f . products
src/Conjure/Expr.hs view
@@ -61,9 +61,9 @@ import Data.Express.Fixtures hiding ((-==-)) import Data.Dynamic-import Control.Applicative ((<$>)) -- for GHC <= 7.8+-- import Control.Applicative ((<$>)) -- for GHC <= 7.8 -import Test.LeanCheck (mapT, filterT, (\/), delay, productWith, productMaybeWith)+import Test.LeanCheck (mapT, filterT, (\/), delay, productWith) import Test.LeanCheck.Tiers (products) import Test.LeanCheck.Utils.Types (A, B, C, D, E, F) @@ -150,6 +150,7 @@ where e = re1 e' re1 e = case unfoldApp e of+ [] -> error "recursexpr: pattern is empty" [e] -> e (ef:exs) | ef == erf -> e' //- zip vs exs | otherwise -> foldApp (map re1 (ef:exs))@@ -536,9 +537,6 @@ | all isApp es = listConflicts [ef | ef :$ _ <- es] +++ listConflicts [ex | _ :$ ex <- es] | otherwise = [es | not (allEqual es)]- where- fun (ef :$ _) = ef- arg (_ :$ ex) = ex -- | Is the expression encoding a negative number. --
src/Conjure/Prim.hs view
@@ -10,7 +10,7 @@ -- -- You are probably better off importing "Conjure". module Conjure.Prim- ( Prim (..)+ ( Prim , prim , pr , prif@@ -24,7 +24,6 @@ import Conjure.Conjurable import Conjure.Expr-import Conjure.Utils import Test.LeanCheck.Error (errorToFalse) import Test.LeanCheck.Utils
src/Conjure/Red.hs view
@@ -17,7 +17,7 @@ import Conjure.Defn import Conjure.Conjurable-import Test.LeanCheck.Error (errorToFalse)+import Test.LeanCheck.Error (errorToFalse, errorToTrue) -- | Checks if an expression is a deconstruction. --@@ -37,7 +37,7 @@ x << 0 = True x << y = x < y is (sd,sx) = errorToFalse $ sd << sx- iz (sd,sx) = errorToFalse $ sd == 0 || sx == 0+ iz (sd,sx) = errorToTrue $ sd == 0 || sx == 0 -- We cannot simply conjureTiers for h here, because the deconstruction -- expression may contain variables, e.g.: @x `mod` _@. -- So conjureGrounds and the holeValue trick are required.
src/Conjure/Utils.hs view
@@ -134,6 +134,7 @@ -- | Applies a function to the head of a list. mapHead :: (a -> a) -> [a] -> [a] mapHead f (x:xs) = f x : xs+mapHead f [] = error "Conjure.Utils.mapHead: empty list" -- | Return sets of values based on the list. --@@ -211,8 +212,8 @@ EQ -> x:nubMergeBy cmp xs ys nubMergeBy _ xs ys = xs ++ ys -nubMergeOn :: Ord b => (a -> b) -> [a] -> [a] -> [a]-nubMergeOn f = nubMergeBy (compare `on` f)+-- nubMergeOn :: Ord b => (a -> b) -> [a] -> [a] -> [a]+-- nubMergeOn f = nubMergeBy (compare `on` f) nubMerge :: Ord a => [a] -> [a] -> [a] nubMerge = nubMergeBy compare
stack.yaml view
@@ -3,7 +3,7 @@ # Copyright (C) 2021-2024 Rudy Matela # Distributed under the 3-Clause BSD licence (see the file LICENSE). -resolver: lts-19.19 # or ghc-9.0.2+resolver: lts-21.25 # or ghc-9.4.8 packages: - .
test/Test.hs view
@@ -50,10 +50,7 @@ n <- getMaxTestsFromArgs n' reportTests pn (tests n) -printLines :: Show a => [a] -> IO ()-printLines = putStrLn . unlines . map show - -- checks if the functions conjureEquality, conjureExpress and conjureTiers -- were correctly generated. conjurableOK :: (Eq a, Show a, Express a, Listable a, Conjurable a) => a -> Bool@@ -66,6 +63,5 @@ ] where (-==-) = evl (fromJust $ conjureEquality x) -:> x- tiers' = mapT evl (fromJust $ conjureTiers x) -: [[x]] expr' = (conjureExpress x . val) -:> x cases' = conjureCases x
test/defn.hs view
@@ -184,12 +184,40 @@ , (xx -?- zero, xx) , (xx -?- yy, xx -+- yy) ] == True++ , showDefn factDefn+ == "fact 0 = 1\n"+ ++ "fact x = x * fact (x - 1)\n"++ , showDefn fact1Defn+ == "fact x = if x == 0\n"+ ++ " then 1\n"+ ++ " else x * fact (x - 1)\n"++ , showDefn factCDefn+ == "fact x = case x == 0 of\n"+ ++ " False -> x * fact (x - 1)\n"+ ++ " True -> 1\n"++ , showDefn sumDefn+ == "sum [] = 0\n"+ ++ "sum (x:xs) = x + sum xs\n"++ , showDefn appendDefn+ == "[] ++ xs = xs\n"+ ++ "(x:xs) ++ ys = x:(xs ++ ys)\n"++ , showDefn isZeroCDefn+ == "isZero x = case compare x 0 of\n"+ ++ " LT -> False\n"+ ++ " EQ -> True\n"+ ++ " GT -> False\n" ] dvl :: Typeable a => Defn -> Expr -> a dvl = devl exprExpr 11 -sumV, factV, nullV, isZeroV :: Expr+factV, sumV, andV, orV, isZeroV, isOneV, nullV, appendV :: Expr factV = var "fact" (undefined :: Int -> Int) sumV = var "sum" (undefined :: [Int] -> Int) andV = var "and" (undefined :: [Bool] -> Bool)@@ -211,13 +239,17 @@ factDefn :: Defn factDefn = [ fact' zero =- one- , fact' xx =- xx -*- (factV :$ (xx -+- minusOne))+ , fact' xx =- xx -*- (factV :$ (minus :$ xx :$ one)) ] where fact' e = factV :$ e fact1Defn :: Defn-fact1Defn = [ fact' xx =- if' (xx -==- zero) (one) (xx -*- (factV :$ (minus :$ xx :$ one)))+fact1Defn = [ fact' xx =- if' (xx -==- zero) one (xx -*- (factV :$ (minus :$ xx :$ one))) ] where fact' e = factV :$ e +factCDefn :: Defn+factCDefn = [ fact' xx =- caseBool (xx -==- zero) (xx -*- (factV :$ (minus :$ xx :$ one))) one+ ] where fact' e = factV :$ e+ nullDefn :: Defn nullDefn = [ null' nil =- true , null' (xx -:- xxs) =- false@@ -228,6 +260,10 @@ , isZero' xx =- false ] where isZero' e = isZeroV :$ e +isZeroCDefn :: Defn+isZeroCDefn = [ isZero' xx =- caseOrdering (xx `compare'` zero) false true false ]+ where isZero' e = isZeroV :$ e+ isOneDefn :: Defn isOneDefn = [ isOne' xx =- xx -==- one ] where isOne' e = isOneV :$ e@@ -340,5 +376,6 @@ , xx -?- yy =- yy ] +(=-) :: a -> b -> (a, b) (=-) = (,) infixr 0 =-
test/derive.hs view
@@ -11,13 +11,13 @@ data Choice = Ae | Bee | Cee deriving (Show, Eq, Typeable) data Peano = Zero | Succ Peano deriving (Show, Eq, Typeable)-data List a = a :- List a | Nil deriving (Show, Eq, Typeable)+data Lst a = a :- Lst a | Nil deriving (Show, Eq, Typeable) data Bush a = Bush a :-: Bush a | Leaf a deriving (Show, Eq, Typeable) data Tree a = Node (Tree a) a (Tree a) | Null deriving (Show, Eq, Typeable) deriveConjurable ''Choice deriveConjurable ''Peano-deriveConjurable ''List+deriveConjurable ''Lst deriveConjurable ''Bush deriveConjurable ''Tree @@ -73,7 +73,7 @@ , conjurableOK (undefined :: Choice) , conjurableOK (undefined :: Peano)- , conjurableOK (undefined :: List Int)+ , conjurableOK (undefined :: Lst Int) , conjurableOK (undefined :: Bush Int) , conjurableOK (undefined :: Tree Int) --, conjurableOK (undefined :: RN) -- TODO: FIX: infinite loop somewhere...@@ -84,8 +84,8 @@ , conjureSize Zero == 1 , conjureSize (Succ Zero) == 2 , conjureSize (Succ (Succ Zero)) == 3- , conjureSize (Nil :: List Int) == 1- , conjureSize (10 :- (20 :- Nil) :: List Int) == 33+ , conjureSize (Nil :: Lst Int) == 1+ , conjureSize (10 :- (20 :- Nil) :: Lst Int) == 33 , conjureCases choice == [ val Ae@@ -100,7 +100,7 @@ , conjureCases (lst int) == [ value ":-" ((:-) ->>: lst int) :$ hole int :$ hole (lst int)- , val (Nil :: List Int)+ , val (Nil :: Lst Int) ] , conjureCases (bush int)@@ -123,8 +123,8 @@ , conjureHoles (undefined :: Peano) == [ hole (undefined :: Peano) , hole (undefined :: Bool) ]- , conjureHoles (undefined :: List Int) == [ hole (undefined :: Int)- , hole (undefined :: List Int)+ , conjureHoles (undefined :: Lst Int) == [ hole (undefined :: Int)+ , hole (undefined :: Lst Int) , hole (undefined :: Bool) ] , conjureHoles (undefined :: Nested) == [ hole (undefined :: N0)@@ -159,7 +159,7 @@ peano :: Peano peano = undefined -lst :: a -> List a+lst :: a -> Lst a lst _ = undefined bush :: a -> Bush a
test/mk view
@@ -22,6 +22,7 @@ rmhs | # excludes extensions from the result of find rmtarget | # exclude Makefile target indicators grep -v '^bench/avgs$' | # not an actual benchmark+ grep -v '^eg/colin/*' | # not run by the makefile grep -v '^.*/[A-Z].*$' # test/benchmark/example scripts begin with lowercase }
test/red.hs view
@@ -3,7 +3,6 @@ import Test import Conjure.Red-import Data.Dynamic main :: IO () main = mainTest tests 5040
test/utils.hs view
@@ -21,5 +21,3 @@ , sets [1,2] == [[1,2], [1], [2], [] :: [Int]] , sets [1,2,3] == [[1,2,3],[1,2],[1,3],[1],[2,3],[2],[3],[] :: [Int]] ]- where- m = n `div` 60