diff --git a/.gitignore b/.gitignore --- a/.gitignore +++ b/.gitignore @@ -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 diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -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 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 diff --git a/TODO.md b/TODO.md --- a/TODO.md +++ b/TODO.md @@ -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 diff --git a/bench/avgs.hs b/bench/avgs.hs new file mode 100644 --- /dev/null +++ b/bench/avgs.hs @@ -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 diff --git a/bench/bench b/bench/bench new file mode 100644 --- /dev/null +++ b/bench/bench @@ -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 diff --git a/bench/candidates.hs b/bench/candidates.hs new file mode 100644 --- /dev/null +++ b/bench/candidates.hs @@ -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 + ] diff --git a/bench/candidates.out b/bench/candidates.out new file mode 100644 --- /dev/null +++ b/bench/candidates.out @@ -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 + + diff --git a/bench/ill-hit.hs b/bench/ill-hit.hs --- a/bench/ill-hit.hs +++ b/bench/ill-hit.hs @@ -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]) ] diff --git a/bench/ill-hit.out b/bench/ill-hit.out --- a/bench/ill-hit.out +++ b/bench/ill-hit.out @@ -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 diff --git a/bench/longshot.hs b/bench/longshot.hs --- a/bench/longshot.hs +++ b/bench/longshot.hs @@ -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) ] diff --git a/bench/longshot.out b/bench/longshot.out --- a/bench/longshot.out +++ b/bench/longshot.out @@ -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 diff --git a/bench/p12.hs b/bench/p12.hs new file mode 100644 --- /dev/null +++ b/bench/p12.hs @@ -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]) + ] diff --git a/bench/p12.out b/bench/p12.out new file mode 100644 --- /dev/null +++ b/bench/p12.out @@ -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] + diff --git a/bench/p30.hs b/bench/p30.hs new file mode 100644 --- /dev/null +++ b/bench/p30.hs @@ -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 [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) + ] diff --git a/bench/p30.out b/bench/p30.out new file mode 100644 --- /dev/null +++ b/bench/p30.out @@ -0,0 +1,2 @@ +running with 26 primitives +usage: p30 [t] diff --git a/bench/runtime/zero/bench/candidates.runtime b/bench/runtime/zero/bench/candidates.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/candidates.runtime @@ -0,0 +1,1 @@ +2.1 diff --git a/bench/runtime/zero/bench/ill-hit.runtime b/bench/runtime/zero/bench/ill-hit.runtime --- a/bench/runtime/zero/bench/ill-hit.runtime +++ b/bench/runtime/zero/bench/ill-hit.runtime @@ -1,1 +1,1 @@ -1.2 +1.4 diff --git a/bench/runtime/zero/bench/longshot.runtime b/bench/runtime/zero/bench/longshot.runtime --- a/bench/runtime/zero/bench/longshot.runtime +++ b/bench/runtime/zero/bench/longshot.runtime @@ -1,1 +1,1 @@ -4.7 +10.0 diff --git a/bench/runtime/zero/bench/p12.runtime b/bench/runtime/zero/bench/p12.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/p12.runtime @@ -0,0 +1,1 @@ +2.9 diff --git a/bench/runtime/zero/bench/p30.runtime b/bench/runtime/zero/bench/p30.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/bench/p30.runtime @@ -0,0 +1,1 @@ +0.0 diff --git a/bench/runtime/zero/bench/take-drop.runtime b/bench/runtime/zero/bench/take-drop.runtime --- a/bench/runtime/zero/bench/take-drop.runtime +++ b/bench/runtime/zero/bench/take-drop.runtime @@ -1,1 +1,1 @@ -7.2 +10.6 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 @@ -3.0 +3.9 diff --git a/bench/runtime/zero/eg/count.runtime b/bench/runtime/zero/eg/count.runtime --- a/bench/runtime/zero/eg/count.runtime +++ b/bench/runtime/zero/eg/count.runtime @@ -1,1 +1,1 @@ -3.2 +4.4 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 @@ -1.5 +2.8 diff --git a/bench/runtime/zero/eg/fibonacci.runtime b/bench/runtime/zero/eg/fibonacci.runtime --- a/bench/runtime/zero/eg/fibonacci.runtime +++ b/bench/runtime/zero/eg/fibonacci.runtime @@ -1,1 +1,1 @@ -22.2 +29.9 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 @@ -1.0 +1.3 diff --git a/bench/runtime/zero/eg/list.runtime b/bench/runtime/zero/eg/list.runtime --- a/bench/runtime/zero/eg/list.runtime +++ b/bench/runtime/zero/eg/list.runtime @@ -1,1 +1,1 @@ -0.5 +1.1 diff --git a/bench/runtime/zero/eg/replicate.runtime b/bench/runtime/zero/eg/replicate.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/replicate.runtime @@ -0,0 +1,1 @@ +7.0 diff --git a/bench/runtime/zero/eg/setelem.runtime b/bench/runtime/zero/eg/setelem.runtime --- a/bench/runtime/zero/eg/setelem.runtime +++ b/bench/runtime/zero/eg/setelem.runtime @@ -1,1 +1,1 @@ -22.5 +41.7 diff --git a/bench/runtime/zero/eg/subset.runtime b/bench/runtime/zero/eg/subset.runtime new file mode 100644 --- /dev/null +++ b/bench/runtime/zero/eg/subset.runtime @@ -0,0 +1,1 @@ +7.1 diff --git a/bench/runtime/zero/eg/tapps.runtime b/bench/runtime/zero/eg/tapps.runtime --- a/bench/runtime/zero/eg/tapps.runtime +++ b/bench/runtime/zero/eg/tapps.runtime @@ -1,1 +1,1 @@ -0.5 +0.7 diff --git a/bench/runtime/zero/eg/tree.runtime b/bench/runtime/zero/eg/tree.runtime --- a/bench/runtime/zero/eg/tree.runtime +++ b/bench/runtime/zero/eg/tree.runtime @@ -1,1 +1,1 @@ -5.6 +8.1 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.10 -express-0.1.14 -speculate-0.4.8 +express-1.0.2 +speculate-0.4.10 diff --git a/bench/self.hs b/bench/self.hs --- a/bench/self.hs +++ b/bench/self.hs @@ -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) ] diff --git a/bench/self.out b/bench/self.out --- a/bench/self.out +++ b/bench/self.out @@ -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 diff --git a/bench/take-drop.hs b/bench/take-drop.hs --- a/bench/take-drop.hs +++ b/bench/take-drop.hs @@ -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]) ] diff --git a/bench/take-drop.out b/bench/take-drop.out --- a/bench/take-drop.out +++ b/bench/take-drop.out @@ -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 diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -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 ------ 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.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 diff --git a/eg/arith.hs b/eg/arith.hs --- a/eg/arith.hs +++ b/eg/arith.hs @@ -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) ] diff --git a/eg/arith.out b/eg/arith.out --- a/eg/arith.out +++ b/eg/arith.out @@ -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 diff --git a/eg/bools.hs b/eg/bools.hs --- a/eg/bools.hs +++ b/eg/bools.hs @@ -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): diff --git a/eg/bools.out b/eg/bools.out --- a/eg/bools.out +++ b/eg/bools.out @@ -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 diff --git a/eg/count.hs b/eg/count.hs --- a/eg/count.hs +++ b/eg/count.hs @@ -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) ] diff --git a/eg/count.out b/eg/count.out --- a/eg/count.out +++ b/eg/count.out @@ -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) diff --git a/eg/factorial.hs b/eg/factorial.hs --- a/eg/factorial.hs +++ b/eg/factorial.hs @@ -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) ] diff --git a/eg/factorial.out b/eg/factorial.out --- a/eg/factorial.out +++ b/eg/factorial.out @@ -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 diff --git a/eg/fibonacci.hs b/eg/fibonacci.hs --- a/eg/fibonacci.hs +++ b/eg/fibonacci.hs @@ -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) diff --git a/eg/fibonacci.out b/eg/fibonacci.out --- a/eg/fibonacci.out +++ b/eg/fibonacci.out @@ -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 diff --git a/eg/gcd.hs b/eg/gcd.hs --- a/eg/gcd.hs +++ b/eg/gcd.hs @@ -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) diff --git a/eg/gcd.out b/eg/gcd.out --- a/eg/gcd.out +++ b/eg/gcd.out @@ -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 diff --git a/eg/ints.hs b/eg/ints.hs --- a/eg/ints.hs +++ b/eg/ints.hs @@ -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) diff --git a/eg/ints.out b/eg/ints.out --- a/eg/ints.out +++ b/eg/ints.out @@ -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 diff --git a/eg/list.hs b/eg/list.hs --- a/eg/list.hs +++ b/eg/list.hs @@ -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) ] diff --git a/eg/list.out b/eg/list.out --- a/eg/list.out +++ b/eg/list.out @@ -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 diff --git a/eg/replicate.hs b/eg/replicate.hs new file mode 100644 --- /dev/null +++ b/eg/replicate.hs @@ -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 diff --git a/eg/replicate.out b/eg/replicate.out new file mode 100644 --- /dev/null +++ b/eg/replicate.out @@ -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 + diff --git a/eg/setelem.hs b/eg/setelem.hs --- a/eg/setelem.hs +++ b/eg/setelem.hs @@ -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) ] diff --git a/eg/setelem.out b/eg/setelem.out --- a/eg/setelem.out +++ b/eg/setelem.out @@ -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) diff --git a/eg/spec.hs b/eg/spec.hs --- a/eg/spec.hs +++ b/eg/spec.hs @@ -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]) ] diff --git a/eg/spec.out b/eg/spec.out --- a/eg/spec.out +++ b/eg/spec.out @@ -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 diff --git a/eg/subset.hs b/eg/subset.hs new file mode 100644 --- /dev/null +++ b/eg/subset.hs @@ -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) + ] diff --git a/eg/subset.out b/eg/subset.out new file mode 100644 --- /dev/null +++ b/eg/subset.out @@ -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 + diff --git a/eg/tapps.hs b/eg/tapps.hs --- a/eg/tapps.hs +++ b/eg/tapps.hs @@ -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 diff --git a/eg/tapps.out b/eg/tapps.out --- a/eg/tapps.out +++ b/eg/tapps.out @@ -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 diff --git a/eg/tree.hs b/eg/tree.hs --- a/eg/tree.hs +++ b/eg/tree.hs @@ -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) ] diff --git a/eg/tree.out b/eg/tree.out --- a/eg/tree.out +++ b/eg/tree.out @@ -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 diff --git a/mk/Toplibs.hs b/mk/Toplibs.hs --- a/mk/Toplibs.hs +++ b/mk/Toplibs.hs @@ -2,3 +2,4 @@ module Toplibs () where import Conjure () +import Test () diff --git a/mk/depend.mk b/mk/depend.mk --- a/mk/depend.mk +++ b/mk/depend.mk @@ -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 \ diff --git a/src/Conjure.hs b/src/Conjure.hs --- a/src/Conjure.hs +++ b/src/Conjure.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 diff --git a/src/Conjure/Cases.hs b/src/Conjure/Cases.hs deleted file mode 100644 --- a/src/Conjure/Cases.hs +++ /dev/null @@ -1,122 +0,0 @@ --- | --- Module : Conjure.Cases --- Copyright : (c) 2021 Rudy Matela --- License : 3-Clause BSD (see the file LICENSE) --- Maintainer : Rudy Matela --- --- 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 diff --git a/src/Conjure/Conjurable.hs b/src/Conjure/Conjurable.hs --- a/src/Conjure/Conjurable.hs +++ b/src/Conjure/Conjurable.hs @@ -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 diff --git a/src/Conjure/Defn.hs b/src/Conjure/Defn.hs new file mode 100644 --- /dev/null +++ b/src/Conjure/Defn.hs @@ -0,0 +1,104 @@ +-- | +-- Module : Conjure.Defn +-- Copyright : (c) 2021 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 diff --git a/src/Conjure/Engine.hs b/src/Conjure/Engine.hs --- a/src/Conjure/Engine.hs +++ b/src/Conjure/Engine.hs @@ -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. diff --git a/src/Conjure/Expr.hs b/src/Conjure/Expr.hs --- a/src/Conjure/Expr.hs +++ b/src/Conjure/Expr.hs @@ -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 diff --git a/src/Conjure/Prim.hs b/src/Conjure/Prim.hs new file mode 100644 --- /dev/null +++ b/src/Conjure/Prim.hs @@ -0,0 +1,80 @@ +-- | +-- Module : Conjure.Prim +-- Copyright : (c) 2021 Rudy Matela +-- License : 3-Clause BSD (see the file LICENSE) +-- Maintainer : Rudy Matela +-- +-- 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 diff --git a/src/Conjure/Spec.hs b/src/Conjure/Spec.hs --- a/src/Conjure/Spec.hs +++ b/src/Conjure/Spec.hs @@ -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] diff --git a/src/Conjure/Utils.hs b/src/Conjure/Utils.hs --- a/src/Conjure/Utils.hs +++ b/src/Conjure/Utils.hs @@ -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 diff --git a/stack.yaml b/stack.yaml --- a/stack.yaml +++ b/stack.yaml @@ -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 diff --git a/test/conjurable.hs b/test/conjurable.hs --- a/test/conjurable.hs +++ b/test/conjurable.hs @@ -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 diff --git a/test/defn.hs b/test/defn.hs new file mode 100644 --- /dev/null +++ b/test/defn.hs @@ -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 =-