diff --git a/.gitignore b/.gitignore --- a/.gitignore +++ b/.gitignore @@ -32,6 +32,7 @@ eg/factorial eg/ints eg/list +bench/self proto/u-conjure test/expr test/conjurable diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -10,6 +10,7 @@ eg/factorial \ eg/ints \ eg/bools \ + bench/self \ proto/u-conjure TESTS = \ diff --git a/TODO.md b/TODO.md --- a/TODO.md +++ b/TODO.md @@ -7,9 +7,6 @@ We should only enumerate functions that were tested to be different. We can limit the tests to the ones that are defined in the given function. -* use FitSpec's notation of `"factorial n"` to name the variables - instead of just `"factorial"` - * use partially defined implementations? partial :: ((Int -> Int) -> Int -> Int) -> (Int -> Int) diff --git a/bench/runtime/zero/bench/self.runtime b/bench/runtime/zero/bench/self.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/self.runtime @@ -0,0 +1,1 @@ +0.01 diff --git a/bench/runtime/zero/eg/arith.runtime b/bench/runtime/zero/eg/arith.runtime --- a/bench/runtime/zero/eg/arith.runtime +++ b/bench/runtime/zero/eg/arith.runtime @@ -1,1 +1,1 @@ -3.72 +4.55 diff --git a/bench/runtime/zero/eg/bools.runtime b/bench/runtime/zero/eg/bools.runtime --- a/bench/runtime/zero/eg/bools.runtime +++ b/bench/runtime/zero/eg/bools.runtime @@ -1,1 +1,1 @@ -2.78 +3.29 diff --git a/bench/runtime/zero/eg/factorial.runtime b/bench/runtime/zero/eg/factorial.runtime --- a/bench/runtime/zero/eg/factorial.runtime +++ b/bench/runtime/zero/eg/factorial.runtime @@ -1,1 +1,1 @@ -2.18 +2.31 diff --git a/bench/runtime/zero/eg/ints.runtime b/bench/runtime/zero/eg/ints.runtime --- a/bench/runtime/zero/eg/ints.runtime +++ b/bench/runtime/zero/eg/ints.runtime @@ -1,1 +1,1 @@ -7.00 +1.95 diff --git a/bench/runtime/zero/versions b/bench/runtime/zero/versions --- a/bench/runtime/zero/versions +++ b/bench/runtime/zero/versions @@ -1,4 +1,4 @@ GHC 8.10.4 leancheck-0.9.4 -express-0.1.6 +express-0.1.8 speculate-0.4.6 diff --git a/bench/self.hs b/bench/self.hs new file mode 100644 --- /dev/null +++ b/bench/self.hs @@ -0,0 +1,24 @@ +-- self.hs: conjuring functions through themselves +-- +-- Copyright (C) 2021 Rudy Matela +-- Distributed under the 3-Clause BSD licence (see the file LICENSE). +import Conjure + +main :: IO () +main = do + cj "?" ((+) :: Int -> Int -> Int) background + cj "?" ((*) :: Int -> Int -> Int) background + cj "i" ((+1) :: Int -> Int) background + cj "d" ((subtract 1) :: Int -> Int) background + where + -- the monomorphism restriction strikes again + cj :: Conjurable f => String -> f -> [Expr] -> IO () + cj = conjureWith args{maxSize=3,maxEquationSize=0} + +background :: [Expr] +background = + [ val (0::Int) + , val (1::Int) + , value "+" ((+) :: Int -> Int -> Int) + , value "*" ((*) :: Int -> Int -> Int) + ] diff --git a/code-conjure.cabal b/code-conjure.cabal --- a/code-conjure.cabal +++ b/code-conjure.cabal @@ -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.1.0 +version: 0.1.2 synopsis: conjure Haskell functions out of partial definitions description: Conjure is a tool that produces Haskell functions out of partial definitions. @@ -27,8 +27,9 @@ extra-source-files: .gitignore , .github/workflows/build.yml , Makefile - , proto/*.hs + , bench/*.hs , eg/*.hs + , proto/*.hs , mk/All.hs , mk/Toplibs.hs , mk/depend.mk @@ -37,10 +38,12 @@ , mk/haskell.mk , mk/install-on , stack.yaml + , bench/runtime/zero/bench/*.runtime , bench/runtime/zero/eg/*.runtime , bench/runtime/zero/proto/*.runtime , bench/runtime/zero/versions , bench/versions + , test/model/bench/*.out , test/model/eg/*.out , test/model/proto/*.out , test/sdist @@ -53,7 +56,7 @@ source-repository this type: git location: https://github.com/rudymatela/conjure - tag: v0.1.0 + tag: v0.1.2 library exposed-modules: Conjure @@ -66,7 +69,7 @@ , leancheck >= 0.9.4 , template-haskell , speculate >= 0.4.6 - , express >= 0.1.6 + , express >= 0.1.8 hs-source-dirs: src default-language: Haskell2010 diff --git a/eg/bools.hs b/eg/bools.hs --- a/eg/bools.hs +++ b/eg/bools.hs @@ -4,16 +4,28 @@ -- Distributed under the 3-Clause BSD licence (see the file LICENSE). import Conjure +and' :: [Bool] -> Bool +and' [p] = p +and' [p,q] = p && q +and' [p,q,r] = p && q && r + +or' :: [Bool] -> Bool +or' [p] = p +or' [p,q] = p || q +or' [p,q,r] = p || q || r + main :: IO () main = do - conjure "and" (and :: [Bool] -> Bool) background - conjure "or" (or :: [Bool] -> Bool) background + conjure "and" (and' :: [Bool] -> Bool) background + conjure "or" (or' :: [Bool] -> Bool) background + -- conjure can use fold as well + conjureWithMaxSize 4 "and" (and' :: [Bool] -> Bool) backgroundWithFold + conjureWithMaxSize 4 "or" (or' :: [Bool] -> Bool) backgroundWithFold + background :: [Expr] background = - [ val False - , val True - , value "not" not + [ value "not" not , value "||" (||) , value "&&" (&&) , value "null" (null :: [Bool] -> Bool) @@ -21,6 +33,11 @@ , value "tail" (tail :: [Bool] -> [Bool]) ] +backgroundWithFold :: [Expr] +backgroundWithFold = + value "foldr" (foldr :: (Bool -> Bool -> Bool) -> Bool -> [Bool] -> Bool) + : background + -- target (for and): -- and ps = if null ps then True else head ps && and (tail ps) @@ -28,3 +45,12 @@ -- or -- and ps = null ps || head ps && and (tail ps) -- 1 2 3 4 5 6 7 8 9 symbols +-- +-- +-- for or, we only reach the solution at size 11: +-- +-- or' ps = not (null ps || not (head ps || or' (tail ps))) +-- +-- unfortunately this is an ill-case, +-- I think there are smaller expressions that rewrite to the above bigger +-- expression so it is only found at the bigger size. diff --git a/eg/factorial.hs b/eg/factorial.hs --- a/eg/factorial.hs +++ b/eg/factorial.hs @@ -14,7 +14,7 @@ main :: IO () -main = conjure "factorial" factorial background +main = conjure "factorial n" factorial background background :: [Expr] @@ -25,21 +25,19 @@ , value "*" ((*) :: Int -> Int -> Int) , value "dec" (subtract 1 :: Int -> Int) , value "isZero" ((==0) :: Int -> Bool) - , val False - , val True ] -- the actual factorial function: --- factorial x = if x == 0 then 1 else x * factorial (x - 1) +-- factorial n = if n == 0 then 1 else n * factorial (n - 1) -- 1 2 3 4 5 6 7 8 9 10 11 symbols -- -- OR -- --- factorial x = if x == 0 then 1 else x * factorial (dec x) +-- factorial n = if n == 0 then 1 else n * factorial (dec n) -- 1 2 3 4 5 6 7 8 9 10 symbols -- -- OR -- --- factorial x = if (isZero x) then 1 else (x * factorial (dec x)) +-- factorial n = if (isZero n) then 1 else (n * factorial (dec n)) -- 1 2 3 4 5 6 7 8 9 symbols diff --git a/eg/ints.hs b/eg/ints.hs --- a/eg/ints.hs +++ b/eg/ints.hs @@ -13,18 +13,29 @@ third [x,y,z] = z third [x,y,z,w] = z +sum' :: [Int] -> Int +sum' [x] = x +sum' [x,y] = x+y +sum' [x,y,z] = x+y+z + +product' :: [Int] -> Int +product' [x] = x +product' [x,y] = x*y +product' [x,y,z] = x*y*z + main :: IO () main = do - conjure "second" (second :: [Int] -> Int) background - conjure "third" (third :: [Int] -> Int) background - conjure "sum" (sum :: [Int] -> Int) background - conjure "product" (product :: [Int] -> Int) background + conjure "second" (second :: [Int] -> Int) background + conjure "third" (third :: [Int] -> Int) background + conjure "sum" (sum' :: [Int] -> Int) background + conjure "product" (product' :: [Int] -> Int) background + conjureWithMaxSize 4 "sum" (sum' :: [Int] -> Int) backgroundWithFold + conjureWithMaxSize 4 "product" (product' :: [Int] -> Int) backgroundWithFold + background :: [Expr] background = - [ val False - , val True - , val (0 :: Int) + [ val (0 :: Int) , val (1 :: Int) , value "+" ((+) :: Int -> Int -> Int) , value "*" ((*) :: Int -> Int -> Int) @@ -32,6 +43,11 @@ , value "head" (head :: [Int] -> Int) , value "tail" (tail :: [Int] -> [Int]) ] + +backgroundWithFold :: [Expr] +backgroundWithFold = + value "foldr" (foldr :: (Int -> Int -> Int) -> Int -> [Int] -> Int) + : background -- sum xs = if null xs then 0 else head xs + sum (tail xs) -- product xs = if null xs then 1 else head xs * product (tail xs) diff --git a/mk/depend.mk b/mk/depend.mk --- a/mk/depend.mk +++ b/mk/depend.mk @@ -1,3 +1,13 @@ +bench/self: \ + bench/self.hs \ + mk/toplibs +bench/self.o: \ + src/Conjure/Utils.hs \ + src/Conjure.hs \ + src/Conjure/Expr.hs \ + src/Conjure/Engine.hs \ + src/Conjure/Conjurable.hs \ + bench/self.hs eg/arith: \ eg/arith.hs \ mk/toplibs diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs --- a/src/Conjure/Conjurable.hs +++ b/src/Conjure/Conjurable.hs @@ -19,6 +19,7 @@ , reifyEquality , canonicalApplication , canonicalVarApplication + , conjureHoles , conjureIfs , conjureTiersFor , conjureMkEquation @@ -112,10 +113,13 @@ conjureReification1 x = (hole x, ifFor x, conjureEquality x, conjureTiers x) conjureReification :: Conjurable a => a -> [Reification1] -conjureReification x = conjureType x [conjureReification1 bool] +conjureReification x = nubOn (\(eh,_,_,_) -> eh) + $ conjureType x [conjureReification1 bool] where bool :: Bool bool = error "conjureReification: evaluated proxy boolean value (definitely a bug)" +-- The use of nubOn above is O(n^2). +-- So long as there is not a huge number of subtypes of a, so we're fine. -- | Reifies equality to be used in a conjurable type. -- @@ -146,6 +150,9 @@ 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 _) <- conjureReification f] @@ -287,17 +294,17 @@ resTy :: (a -> b) -> b resTy _ = undefined -canonicalArgumentVariables :: Conjurable f => f -> [Expr] -canonicalArgumentVariables = unfoldApp - . mostGeneralCanonicalVariation - . foldApp - . conjureArgumentHoles - canonicalApplication :: Conjurable f => String -> f -> Expr -canonicalApplication nm f = foldApp (value nm f : canonicalArgumentVariables f) +canonicalApplication = canonicalWhatApplication value canonicalVarApplication :: Conjurable f => String -> f -> Expr -canonicalVarApplication nm f = foldApp (var nm f : canonicalArgumentVariables f) +canonicalVarApplication = canonicalWhatApplication var + +canonicalWhatApplication :: Conjurable f => (String -> f -> Expr) -> String -> f -> Expr +canonicalWhatApplication what nm f = mostGeneralCanonicalVariation . foldApp + $ what nf f : zipWith varAsTypeOf nas (conjureArgumentHoles f) + where + (nf:nas) = words nm ++ repeat "" diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs --- a/src/Conjure/Engine.hs +++ b/src/Conjure/Engine.hs @@ -91,10 +91,11 @@ candidates = filter (\e -> typ e == typ ffxx) . concat . take maxSize - $ candidateExprs nm f maxEquationSize maxRecursiveCalls (===) [es ++ conjureIfs f] + $ candidateExprs nm f maxEquationSize maxRecursiveCalls (===) + [nub $ [val False, val True] ++ es ++ conjureIfs f] ffxx = canonicalApplication nm f vffxx = canonicalVarApplication nm f - rrff = var nm f + (rrff:_) = unfoldApp vffxx (===), (?=?) :: Expr -> Expr -> Bool e1 === e2 = isReallyTrue (e1 -==- e2) @@ -147,14 +148,17 @@ -- -- > conjureWithMaxSize 10 "function" function [...] conjureWithMaxSize :: Conjurable f => Int -> String -> f -> [Expr] -> IO () -conjureWithMaxSize sz = conjureWith args{maxSize = sz} +conjureWithMaxSize sz = conjureWith args + { maxSize = sz + , maxEquationSize = min sz (maxEquationSize args) + } -- | Like 'conjure' but allows setting options through 'Args'/'args'. -- -- > conjureWith args{maxSize = 11} "function" function [...] conjureWith :: Conjurable f => Args -> String -> f -> [Expr] -> IO () conjureWith args nm f es = do - print (var nm f) + print (var (head $ words nm) f) putStr $ "-- looking through " ++ show ncs ++ " candidates" hFlush stdout case rs of @@ -178,7 +182,7 @@ candidateExprs nm f sz mc (===) ess = expressionsT $ [ef:exs] \/ ess where (ef:exs) = unfoldApp $ canonicalVarApplication nm f - thy = theoryFromAtoms (===) sz $ [nub (b_:map holeAsTypeOf exs)] \/ ess + thy = theoryFromAtoms (===) sz $ [conjureHoles f] \/ ess expressionsT ds = filterT (\e -> count (== ef) (vars e) <= mc) $ filterT (isRootNormalE thy) $ ds \/ (delay $ productMaybeWith ($$) es es) diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs --- a/src/Conjure/Utils.hs +++ b/src/Conjure/Utils.hs @@ -17,6 +17,7 @@ , module Data.Typeable , count + , nubOn ) where @@ -29,3 +30,6 @@ count :: (a -> Bool) -> [a] -> Int count p = length . filter p + +nubOn :: Eq b => (a -> b) -> [a] -> [a] +nubOn f = nubBy ((==) `on` f) diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -11,4 +11,4 @@ extra-deps: - leancheck-0.9.4 - speculate-0.4.6 -- express-0.1.6 +- express-0.1.8 diff --git a/test/conjurable.hs b/test/conjurable.hs --- a/test/conjurable.hs +++ b/test/conjurable.hs @@ -21,6 +21,13 @@ tests n = [ True + , canonicalApplication "not" not == not' pp + , canonicalApplication "not q" not == not' qq + , canonicalApplication "negate" (negate :: Int -> Int) == negate' xx + , canonicalApplication "negate i" (negate :: Int -> Int) == negate' ii + , canonicalApplication "+" ((+) :: Int -> Int -> Int) == xx -+- yy + , canonicalApplication "+ i j" ((+) :: Int -> Int -> Int) == ii -+- jj + , holds n $ \x y -> (x <==> y) == (x == (y :: ())) , holds n $ \x y -> (x <==> y) == (x == (y :: Int)) , holds n $ \p q -> (p <==> q) == (p == (q :: Bool)) diff --git a/test/model/bench/self.out b/test/model/bench/self.out new file mode 100644 --- /dev/null +++ b/test/model/bench/self.out @@ -0,0 +1,16 @@ +(?) :: Int -> Int -> Int +-- looking through 52 candidates, 100% match, 60/60 assignments +x ? y = x + y + +(?) :: Int -> Int -> Int +-- looking through 52 candidates, 100% match, 60/60 assignments +x ? y = x * y + +i :: Int -> Int +-- looking through 24 candidates, 100% match, 60/60 assignments +i x = x + 1 + +d :: Int -> Int +-- looking through 24 candidates +cannot conjure + diff --git a/test/model/eg/bools.out b/test/model/eg/bools.out --- a/test/model/eg/bools.out +++ b/test/model/eg/bools.out @@ -1,8 +1,16 @@ and :: [Bool] -> Bool --- looking through 1207 candidates, 100% match, 60/60 assignments +-- looking through 1207 candidates, 100% match, 14/14 assignments and ps = null ps || head ps && and (tail ps) or :: [Bool] -> Bool --- looking through 1207 candidates, 90% match, 54/60 assignments +-- looking through 1207 candidates, 78% match, 11/14 assignments or ps = head ps || or (tail ps) + +and :: [Bool] -> Bool +-- looking through 19 candidates, 100% match, 14/14 assignments +and ps = foldr (&&) True ps + +or :: [Bool] -> Bool +-- looking through 19 candidates, 100% match, 14/14 assignments +or ps = foldr (||) False ps diff --git a/test/model/eg/factorial.out b/test/model/eg/factorial.out --- a/test/model/eg/factorial.out +++ b/test/model/eg/factorial.out @@ -1,4 +1,4 @@ factorial :: Int -> Int -- looking through 8576 candidates, 100% match, 6/6 assignments -factorial x = if isZero x then 1 else x * factorial (dec x) +factorial n = if isZero n then 1 else n * factorial (dec n) diff --git a/test/model/eg/ints.out b/test/model/eg/ints.out --- a/test/model/eg/ints.out +++ b/test/model/eg/ints.out @@ -1,16 +1,24 @@ second :: [Int] -> Int --- looking through 12955 candidates, 100% match, 47/47 assignments +-- looking through 636 candidates, 100% match, 47/47 assignments second xs = head (tail xs) third :: [Int] -> Int --- looking through 12955 candidates, 100% match, 34/34 assignments +-- looking through 636 candidates, 100% match, 34/34 assignments third xs = head (tail (tail xs)) sum :: [Int] -> Int --- looking through 12955 candidates, 8% match, 5/60 assignments +-- looking through 636 candidates, 13% match, 5/37 assignments sum xs = if null (tail xs) then head xs else sum xs product :: [Int] -> Int --- looking through 12955 candidates, 36% match, 22/60 assignments -product xs = 0 * head (tail (tail (tail xs))) +-- looking through 636 candidates, 13% match, 5/37 assignments +product xs = if null (tail xs) then head xs else product xs + +sum :: [Int] -> Int +-- looking through 15 candidates, 100% match, 37/37 assignments +sum xs = foldr (+) 0 xs + +product :: [Int] -> Int +-- looking through 15 candidates, 100% match, 37/37 assignments +product xs = foldr (*) 1 xs