--
-- (C) Susumu Katayama
--
-- (Typed)IOPairs¾å¤Ç¥Ç¡¼¥¿¤ò¤È¤ë¡¥ghci¾å¤Ç :cmd ¤ò»È¤¤¤Þ¤¯¤ë´¶¤¸¡¥
{-# LANGUAGE RankNTypes, CPP #-}
module ExperimIOP(module ExperimIOP, module MagicHaskeller.RunAnalytical) where
import MagicHaskeller.Analytical
#ifdef DEBUG
hiding (rev)
#endif
import MagicHaskeller.Classification(Filtrable)
import MagicHaskeller.RunAnalytical
#ifdef DEBUG
hiding (main)
#endif
import MagicHaskeller.GetTime(batchWrite)
main = do iop <- runQ andL
let e = getOne iop []
putStrLn $ pprint e
-- Eg. :cmd prepare
prepare :: IO String
prepare = run [":set +s",":m +Language.Haskell.TH","session <- prepareAPI [\"MagicHaskeller\"]"]
run :: [String] -> IO String
run = return . unlines . echoOn
-- set of lightweight experiments
batchWriteFile filename = do
session <- prepareAPI ["MagicHaskeller"]
let f :: forall a. (Filtrable a, Typeable a) => Q [Dec] -> (a -> Bool) -> IO ()
f = filterGetOne_ session
batchWrite filename [ f addN longAddNPred
, f andL andLPred
, f heaD headPred
, f incr incrPred
, f append appendPred
-- , f allOdd'21 (\\allodd -> allodd [3,3] && not (allodd [2,3]) && allodd [1,3,5] && not (allodd [1,2,4]))
-- , f concat12 (\\concat -> concat [\"abc\",\"\",\"de\",\"fghi\"] == \"abcdefghi\")
, f drop'9 dropPred
, f eq9 eqPred
, f evenpos7 evenposPred
-- , f evens21 (\\evens -> evens [4,6,9,2,3,8,8] == [4,6,2,8,8])
-- , f fib6 (\\fib -> fib 1 == 1 && fib 2 == 1 && fib 4 == 3 && fib 6 == 8 && fib 8 == 21)
, f iniT initPred
, f oddpos6 oddposPred
, f lasT lastPred
, f lasts lastsPred
, f lens lengthsPred
, f multFst multFstPred
, f multLst multLstPred
, f negateall negateAllPred
, f reversE revPred
, f shiftl shiftlPred
, f shiftr shiftrPred
, f snoc snocPred
-- , f suM (\\sum -> sum [7,3,8,5] == 23)
, f swap swapPred
, f switch switchPred
, f takE takePred
, f weave weavePred
]
-- :cmd batch
batch :: IO String
batch = run $ filtGetOne "addN" "longAddNPred" ++
filtGetOne "andL" "andLPred"
++ filtGetOne "heaD" "headPred"
++ filtGetOne "incr" "incrPred"
++ filtGetOne "append" "appendPred"
-- ++ filtGetOne "allOdd'21" "(\\allodd -> allodd [3,3] && not (allodd [2,3]) && allodd [1,3,5] && not (allodd [1,2,4]))"
-- ++ filtGetOne "concat12" "(\\concat -> concat [\"abc\",\"\",\"de\",\"fghi\"] == \"abcdefghi\")"
++ filtGetOne "drop'9" "dropPred"
++ filtGetOne "eq9" "eqPred"
++ filtGetOne "evenpos7" "evenposPred"
-- ++ filtGetOne "evens21" "(\\evens -> evens [4,6,9,2,3,8,8] == [4,6,2,8,8])"
-- ++ filtGetOne "fib6" "(\\fib -> fib 1 == 1 && fib 2 == 1 && fib 4 == 3 && fib 6 == 8 && fib 8 == 21)"
++ filtGetOne "iniT" "initPred"
++ filtGetOne "oddpos6" "oddposPred"
++ filtGetOne "lasT" "lastPred"
++ filtGetOne "lasts" "lastsPred"
++ filtGetOne "lens" "lengthsPred"
++ filtGetOne "multFst" "multFstPred"
++ filtGetOne "multLst" "multLstPred"
++ filtGetOne "negateall" "negateAllPred"
++ filtGetOne "reversE" "revPred"
++ filtGetOne "shiftl" "shiftlPred"
++ filtGetOne "shiftr" "shiftrPred"
++ filtGetOne "snoc" "snocPred"
-- ++ filtGetOne "suM" "(\\sum -> sum [7,3,8,5] == 23)"
++ filtGetOne "swap" "swapPred"
++ filtGetOne "switch" "switchPred"
++ filtGetOne "takE" "takePred"
++ filtGetOne "weave" "weavePred"
untype :: Functor m => m [a] -> m [a]
untype = fmap tail
-- E.g. :cmd run $ tryGetOne "add6"
tryGetOne :: String -> [String]
tryGetOne str = ["iop <- runQ $ "++str, "let e = getOne iop []", "putStrLn $ pprint e"]
-- E.g. :cmd run $ tryGetOneBK "add6" []
-- :cmd run $ tryGetOneBK "fib6" ["add6"]
tryGetOneBK :: String -> String -> [String]
tryGetOneBK str bk = ["iop <- runQ $ "++str, "bk <- runQ $ "++bk, "let e = getOne iop bk", "putStrLn $ pprint e"]
-- E.g. :cmd run $ testGetOne "add6" addArgss
testGetOne :: String -> [String] -> [String]
testGetOne str argss = tryGetOne str ++ map ("$(return e) "++) argss
-- E.g. :cmd run $ filtGetOne "reversE" "(\\f -> f \"abcdef\" == \"fedcba\")"
filtGetOne :: String -> String -> [String]
filtGetOne str predicate = ["filterGetOne session ("++str++") ("++predicate++")"]
filtGetOneBK :: String -> String -> String -> [String]
filtGetOneBK str bk predicate = ["filterGetOneBK session ("++str++") ("++bk++") ("++predicate++")"]
emptyBK = [d| {} |]
-- :cmd run $ filtGetOne "add''" "(\\(+) -> 3+5==8)"
add6 = [d| f :: Int->Int->Int; f 0 0 = 0; f 0 1 = 1; f 1 0 = 1; f 2 0 = 2; f 1 1 = 2; f 0 2 = 2 |]
add'7 = [d| f :: Int->Int->Int; f 0 x = x; f x 0 = x; f 1 1 = 2; f 1 2 = 3; f 2 1 = 3; f 2 2 = 4; f 2 3 = 5 |] -- dame. ¤Ç¤â¡¤Igor¤Ç¤ÏOK.
add'6 = [d| f :: Int->Int->Int; f 0 x = x; f x 0 = x; f 1 1 = 2; f 1 2 = 3; f 2 1 = 3; f 2 2 = 4 |] -- dame
add'5 = [d| f :: Int->Int->Int; f 0 x = x; f x 0 = x; f 1 1 = 2; f 1 2 = 3; f 2 1 = 3 |] -- dame
add'3 = [d| f :: Int->Int->Int; f 0 x = x; f x 0 = x; f 1 1 = 2 |] -- dame
add'2 = [d| f :: Int->Int->Int; f 0 x = x; f x 0 = x |] -- dame ¤É¤¦¤âoverlap¤·¤Æ¤¤¤ë¤Î¤¬¤Þ¤º¤¤¤Î¤Ç¤Ï? ¼«Æ°Åª¤Ëcaseʬ¤±¤¹¤ë¤è¤¦¤Ë¤¹¤ì¤Ð¤è¤¤¡¥
add'1 = [d| f :: Int->Int->Int; f 0 x = x |]
add'' = [d| f :: Int->Int->Int; f 0 x = x; f 1 0 = 1; f 2 0 = 2; f 1 1 = 2; f 1 2 = 3; f 2 1 = 3; f 2 2 = 4; f 2 3 = 5 |]
addArgss = ["3 5"]
-- :cmd run $ filtGetOne "addN" "longAddNPred"
addN = [d|
addN :: Int -> [Int] -> [Int]
addN 0 [] = []
addN 1 [] = []
addN 2 [] = []
addN 0 [0] = [0]
addN 0 [1] = [1]
addN 0 [2] = [2]
addN 0 [0,1] = [0,1]
addN 0 [1,0] = [1,0]
addN 1 [0,1] = [1,2]
addN 1 [1,0] = [2,1]
addN 1 [0] = [1]
addN 1 [1] = [2]
addN 1 [2] = [3]
addN 2 [0] = [2]
addN 2 [1] = [3]
addN 2 [2] = [4]
addN 2 [0,1] = [2,3]
addN 2 [2,0] = [4,2]
|]
--batchAddN = do session <- prepareAPI ["MagicHaskeller"]
-- batchWrite "addN.dat" $ map (\n -> filterGetOne session (tunedAddN n) addNPred) [5..22] -- ¤³¤¦½ñ¤¤¤Æ¤Ï¸«¤¿¤â¤Î¤Î¡¤¥¿¥¤¥à¥¢¥¦¥È¤Ï¡©
testAddN = [d|
addN :: Int -> [Int] -> [Int]
addN 0 [] = []
addN 1 [] = []
addN 2 [] = []
|]
takeFunD n (FunD name clauses : xs) = FunD name (take n clauses) : takeFunD n xs
takeFunD n (x:xs) = x : takeFunD n xs
takeFunD _ [] = []
-- 22¤Þ¤Ç¡¥¼ÂºÝ¤Ë¤Ï¡¤[3,6..21]¤Ç¼Â¹Ô¤¹¤ë¤À¤±¤ÇÌÌÇò¤¤´¶¤¸¡¥(3¤È21°Ê³°¤Ï¤¦¤Þ¤¯¤¤¤¯¡¥)
tunedAddN n = fmap (takeFunD n) [d|
addN :: Int -> [Int] -> [Int]
addN 0 [] = []
addN 1 [] = []
addN 2 [] = []
addN 0 [0] = [0]
addN 0 [1] = [1]
addN 0 [2] = [2]
addN 0 [0,0] = [0,0]
addN 0 [0,1] = [0,1]
addN 0 [1,0] = [1,0]
addN 1 [0] = [1]
addN 1 [1] = [2]
addN 1 [2] = [3]
addN 1 [0,0] = [1,1]
addN 1 [0,1] = [1,2]
addN 1 [1,0] = [2,1]
addN 2 [0] = [2]
addN 2 [1] = [3]
addN 2 [2] = [4]
addN 2 [0,0] = [2,2]
addN 2 [0,1] = [2,3]
addN 2 [1,0] = [3,2]
addN 2 [2,0] = [4,2]
|]
addNPred, longAddNPred :: (Int -> [Int] -> [Int]) -> Bool
addNPred addN = addN 3 [5,7] == [8,10]
longAddNPred addN = addN 3 [5,7,2] == [8,10,5]
-- :cmd run $ filtGetOne "andL" "(\\and -> not (and [True,False]) && and [True,True] && and [True,True,True] && not (and [False,True,True]))"
andL = tunedAndL 15
-- [1,3,7,15,31]
tunedAndL n = fmap (takeFunD n) [d|
andL :: [Bool] -> Bool
andL [] = True
andL [True] = True
andL [False] = False
andL [True,True] = True
andL [True,False] = False
andL [False,True] = False
andL [False,False] = False
andL [True,True,True] = True
andL [False,True,True] = False
andL [True,False,True] = False
andL [True,True,False] = False
andL [True,False,False] = False
andL [False,True,False] = False
andL [False,False,True] = False
andL [False,False,False] = False
andL [True,True,True,True] = True
andL [True,False,True,True] = False
andL [True,True,False,True] = False
andL [True,True,True,False] = False
andL [True,True,False,False] = False
andL [True,False,True,False] = False
andL [True,False,False,True] = False
andL [True,False,False,False] = False
andL [False,True,True,True] = True
andL [False,False,True,True] = False
andL [False,True,False,True] = False
andL [False,True,True,False] = False
andL [False,True,False,False] = False
andL [False,False,True,False] = False
andL [False,False,False,True] = False
andL [False,False,False,False] = False
|]
andLPred and = not (and [True,False]) && and [True,True] && and [True,True,True] && not (and [False,True,True])
allOdd4 = [d| f :: [Int]->Bool; f [] = True; f [x] = odd x; f [x,y] = odd x && odd y; f [x,y,z] = odd x && (odd y && odd z) |]
-- :cmd run $ filtGetOne "allOdd'21" "longAlloddPred"
allOdd'21 = [d| f :: [Int]->Bool; f [] = True; f [0] = False; f [1] = True; f [2] = False; f [3] = True;
f [0,0] = False; f [0,1] = False; f [0,2] = False; f [0,3] = False;
f [1,0] = False; f [1,1] = True; f [1,2] = False; f [1,3] = True;
f [2,0] = False; f [2,1] = False; f [2,2] = False; f [2,3] = False;
f [3,0] = False; f [3,1] = True; f [3,2] = False; f [3,3] = True |]
-- [1,3,6,10,15] ¤¢¤È¡¤allOdd'21¤Ï¤³¤ì¤é¤òÊñ´Þ¤¹¤ë¡¥
tunedAllOdd n = fmap (takeFunD n)
[d| f :: [Int]->Bool; f [] = True; f [0] = False; f [0,0] = False;
f [1] = True; f [0,1] = False; f [1,0] = False;
f [2] = False; f [0,2] = False; f [1,1] = True; f [2,0] = False;
f [3] = True; f [0,3] = False; f [1,2] = False; f [2,1] = False; f [3,0] = False |] -- dame
-- Igor¤Ç¤âcatamorphism extension¤Ê¤·¤Ç¤Ï¤Ç¤¤Ê¤¤¤Î¤Ç¤¤¤¤¤ä¡¥
alloddPred allodd = allodd [3,3] && not (allodd [2,3]) && allodd [1,3,5] && not (allodd [1,2,4])
longAlloddPred allodd = allodd [3,3] && not (allodd [2,3]) && allodd [1,3,5] && not (allodd [3,7,5,1,2])
-- Example.hs¤½¤Î¤Þ¤Þ
-- :cmd run $ filtGetOne "append" "appendPred"
append = [d|
appenD :: [a] -> [a] -> [a]
appenD [] x = x
--appenD [][] = []
appenD [a][] = [a]
--appenD [][c] = [c]
--appenD [][c,d] = [c,d]
appenD [a][c] = [a,c]
appenD [a,b][] = [a,b]
--appenD [] [a,b,c] = [a,b,c]
appenD [a][c,d] = [a,c,d]
appenD [a,b][d] = [a,b,d]
appenD [a,c,d][] = [a,c,d]
--appenD [][a,b,c,d] = [a,b,c,d]
appenD [a,b][c,d] = [a,b,c,d]
appenD [a,b,c][d] = [a,b,c,d]
appenD [a,b,c,d][] = [a,b,c,d]
|] -- ¤¤¤±¤ë
-- [2,4,7,11,16]
tunedAppend n = fmap (takeFunD n) [d|
appenD :: [a] -> [a] -> [a]
appenD [] x = x
--appenD [][] = []
appenD [a][] = [a]
--appenD [][c] = [c]
--appenD [][c,d] = [c,d]
appenD [a][c] = [a,c]
appenD [a,b][] = [a,b]
--appenD [] [a,b,c] = [a,b,c]
appenD [a][c,d] = [a,c,d]
appenD [a,b][d] = [a,b,d]
appenD [a,c,d][] = [a,c,d]
appenD [a][b,c,d] = [a,b,c,d]
appenD [a,b][c,d] = [a,b,c,d]
appenD [a,b,c][d] = [a,b,c,d]
appenD [a,b,c,d][] = [a,b,c,d]
appenD [a][b,c,d,e] = [a,b,c,d,e]
appenD [a,b][c,d,e] = [a,b,c,d,e]
appenD [a,b,c][d,e] = [a,b,c,d,e]
appenD [a,b,c,d][e] = [a,b,c,d,e]
appenD [a,b,c,d,e][] = [a,b,c,d,e]
|] -- ¤¤¤±¤ë
appendPred (++) = "foo" ++ "bar" == "foobar"
-- :cmd run $ filtGetOne "concat12" "(\\concat -> concat [\"abc\",\"\",\"de\",\"fghi\"] == \"abcdefghi\")"
concat12 = [d|
concaT :: [[a]] -> [a]
concaT [] = []
concaT [[]] = []
concaT [[a]] = [a]
concaT [[],[a]] = [a]
concaT [[a],[]] = [a]
concaT [[a],[b]] = [a,b]
concaT [[c,d]]= [c,d]
concaT [[a,b,c]] = [a,b,c]
concaT [[a,b],[c]] = [a,b,c]
concaT [[a],[c,d]] = [a,c,d]
concaT [[a],[b],[c]] = [a,b,c]
concaT [[a,b],[c,d]] = [a,b,c,d]
|] -- dame. igor¤Ç¤â¥À¥á¡¥MH¤À¤È°ì½Ö¡¥
-- ¤Æ¤æ¡¼¤«¡¤Í×ÁÇ¿ô3¤Ä¤Î¾ì¹ç¤Ë¶õ¥ê¥¹¥È¤¬¤Ê¤«¤Ã¤¿¤ê¤¹¤ëÌõ¤Ç¡¤¤½¤ÎÊÕ·ÏÅýŪ¤ÊÎã¤È¤Ï¤¤¤¨¤Ê¤¤¤Î¤Ç¡¤²¿¤È¤â¸À¤¨¤Ê¤¤¡¥
tunedConcat n = fmap (takeFunD n) [d|
concaT :: [[a]] -> [a]
concaT [] = []
concaT [[]] = []
concaT [[a]] = [a]
concaT [[],[]] = []
concaT [[],[a]] = [a]
concaT [[a],[]] = [a]
concaT [[a],[b]] = [a,b]
concaT [[c,d]]= [c,d]
concaT [[a,b,c]] = [a,b,c]
concaT [[],[a,b,c]] = [a,b,c]
concaT [[a,b,c],[]] = [a,b,c]
concaT [[a,b],[c]] = [a,b,c]
concaT [[a],[c,d]] = [a,c,d]
-- concaT [[a,b],[c,d]] = [a,b,c,d]
-- concaT [[a],[b],[c]] = [a,b,c]
|]
concatPred concat = concat ["abc","","de","fghi"] == "abcdefghi"
allOddArgss = ["[3,1,5]", "[1,3,2]"]
-- ¤³¤Ã¤Á¤¬tuned
drop12 = [d| droP :: Int -> [a] -> [a]
droP 0 [] = []
droP 0 [a] = [a]
droP 0 [a,b] = [a,b]
droP 0 [a,b,c] = [a,b,c]
droP 1 [] = []
droP 1 [a] = []
droP 1 [a,b] = [b]
droP 1 [a,b,c] = [b,c]
droP 2 [] = []
droP 2 [a] = []
droP 2 [a,b] = []
droP 2 [a,b,c] = [c]
--droP (S (S 1)) [] = []
--droP (S (S 1)) [a] = []
--droP (S (S 1)) [a,b] = []
--droP (S (S 1)) [a,b,c] = []
|] -- ¤¤¤±¤ë¡¥
-- :cmd run $ filtGetOne "drop'9" "dropPred"
drop'9 = [d| droP :: Int -> [a] -> [a]
droP 0 x = x
--droP 0 [] = []
--droP 0 [a] = [a]
--droP x [] = []
droP 1 [] = []
droP 2 [] = []
--droP 0 [a,b] = [a,b]
--droP 0 [a,b,c] = [a,b,c]
droP 1 [a] = []
droP 1 [a,b] = [b]
droP 1 [a,b,c] = [b,c]
droP 2 [a] = []
droP 2 [a,b] = []
droP 2 [a,b,c] = [c]
--droP (S (S 1)) [] = []
--droP (S (S 1)) [a] = []
--droP (S (S 1)) [a,b] = []
--droP (S (S 1)) [a,b,c] = []
|] -- ¤¤¤±¤ë¡¥¤Á¤Ê¤ß¤Ë¡¤drop12¤Î¾ì¹ç¤È¤Ï¤Ù¤Ä¤Î²ò¤¬ÀèƬ¤ËÍè¤ë¤¬¡¤¤É¤Á¤é¤âÀµ²ò¡¥¤Ê¤ª¡¤drop'9¤¬Example.hs¤ÈƱ¤¸¤â¤Î¡¥
dropPred :: (Int -> String -> String) -> Bool
dropPred drop = drop 3 "abcde" == "de"
dropArgss = ["3 [4,5,6,7,8]"]
even6 = [d| f :: Int -> Bool; f 0 = True; f 1 = False; f 2 = True; f 3 = False; f 4 = True; f 5 = False |]
evenArgss = ["8", "9"]
-- :cmd run $ filtGetOne "evenpos7" "evenposPred"
evenpos7 = [d| evenpos :: [a] -> [a]
evenpos [] = []
evenpos [a] = []
evenpos [a,b] = [b]
evenpos [a,b,c] = [b]
evenpos [a,b,c,d] = [b,d]
evenpos [a,b,c,d,e] = [b,d]
evenpos [a,b,c,d,e,f] = [b,d,f]
|] -- Examples.hs¤ÈƱ¤¸¤â¤Î¡¥
evenposPred evenpos = evenpos "abcdefg" == "bdf"
-- :cmd run $ filtGetOne "evens21" "evensPred"
evens21 = [d|
evens :: [Int] -> [Int]
evens [] = []
evens [0] = [0]
evens [1] = []
evens [2] = [2]
evens [3] = []
evens [0,0] = [0,0]
evens [0,1] = [0]
evens [0,2] = [0,2]
evens [0,3] = [0]
evens [1, 0] = [0]
evens [1, 1] = []
evens [1, 2] = [2]
evens [1, 3] = []
evens [2, 0] = [2,0]
evens [2, 1] = [2]
evens [2, 2] = [2,2]
evens [2, 3] = [2]
evens [3, 0] = [0]
evens [3, 1] = []
evens [3, 2] = [2]
evens [3, 3] = []
|]
evens13 = [d|
evens :: [Int] -> [Int]
evens [] = []
evens [0] = [0]
evens [1] = []
evens [2] = [2]
evens [0,0] = [0,0]
evens [0,1] = [0]
evens [0,2] = [0,2]
evens [1, 0] = [0]
evens [1, 1] = []
evens [1, 2] = [2]
evens [2, 0] = [2,0]
evens [2, 1] = [2]
evens [2, 2] = [2,2]
|]
evensArgss = ["[1,2,3,4,5]"]
evensPred evens = evens [4,6,9,2,3,8,8] == [4,6,2,8,8]
-- :cmd run $ filtGetOne "eq9" "eqPred"
eq9 = [d| f :: Int->Int->Bool; f 0 0 = True; f 0 1 = False; f 0 2 = False; f 1 0 = False; f 1 1 = True; f 1 2 = False; f 2 0 = False; f 2 1 = False; f 2 2 = True |] -- Examples.hs¤ÈƱ¤¸¤â¤Î
eq16 = [d| f :: Int->Int->Bool; f 0 0 = True; f 0 1 = False; f 0 2 = False; f 0 3 = False; f 1 0 = False; f 1 1 = True; f 1 2 = False; f 1 3 = False; f 2 0 = False; f 2 1 = False; f 2 2 = True; f 2 3 = False; f 3 0 = False; f 3 1 = False; f 3 2 = False; f 3 3 = True |] -- dame ... too slow....
eqArgss = ["4 4", "5 7"]
eqPred :: (Int->Int->Bool) -> Bool
eqPred (==) = 3==3 && not (4==6) && 0==0 && not (2==0) && not (0==2) && not (3==5)
tryFib :: [String]
tryFib = ["iop <- runQ $ fib6", "let e = getOne iop []", "putStrLn $ pprint e"]
-- note that this starts with 0 rather than 1. Also, more examples should be given.
-- :cmd run $ filtGetOne "fib6" "(\\fib -> fib 1 == 1 && fib 2 == 1 && fib 4 == 3 && fib 6 == 8 && fib 8 == 21)"
fib6 = [d| fib :: Int->Int
fib 0 = 0
fib 1 = 1
fib 2 = 1
fib 3 = 2
fib 4 = 3
fib 5 = 5
|] -- Examples.hs¤È¤ª¤Ê¤¸¤â¤Î
-- :cmd run $ filtGetOne "fib8" "(\\fib -> fib 1 == 1 && fib 2 == 1 && fib 4 == 3 && fib 6 == 8 && fib 8 == 21)"
fib8 = [d| fib :: Int->Int
fib 0 = 0
fib 1 = 1
fib 2 = 1
fib 3 = 2
fib 4 = 3
fib 5 = 5
fib 6 = 8
fib 7 = 13
|]
fib9 = [d| fib :: Int->Int
fib 0 = 0
fib 1 = 1
fib 2 = 1
fib 3 = 2
fib 4 = 3
fib 5 = 5
fib 6 = 8
fib 7 = 13
fib 8 = 21
|]
fib10 = [d| fib :: Int->Int
fib 0 = 0
fib 1 = 1
fib 2 = 1
fib 3 = 2
fib 4 = 3
fib 5 = 5
fib 6 = 8
fib 7 = 13
fib 8 = 21
fib 9 = 34
|]
fibPred fib = fib 1 == 1 && fib 2 == 1 && fib 4 == 3 && fib 6 == 8 && fib 8 == 21
-- :cmd run $ filtGetOne "heaD" "headPred"
heaD = [d|
heaD :: [a] -> a
heaD [a] = a
heaD [a,b] = a
heaD [a,b,c] = a
heaD [a,b,c,d] = a
|]
headPred head = head "abcde" == 'a'
-- :cmd run $ filtGetOne "incr" "incrPred"
incr = [d|
incr :: [Int] -> [Int]
incr [] = []
incr [0] = [1]
incr [1] = [2]
--incr [2] = [3]
incr [0,1] = [1,2]
--incr [0,2] = [1,3]
incr [1,0] = [2,1]
|] -- Examples.hs¤ÈƱ¤¸¤â¤Î¡¥Ä¹¤µ¤¬Â¤ê¤º¡¤filter¤¬Í¸ú¤ÊÎã¡¥`mplus`¤Ç¤â(+/)¤Ç¤â¡¥¤Ç¤â¡¤Igor¤À¤È¤¦¤Þ¤¯¤¤¤¯¡¥
incrPred :: ([Int] -> [Int]) -> Bool
incrPred f = f [0,1,1,2] == [1,2,2,3]
incr' = [d|
incr :: [Int] -> [Int]
incr [] = []
incr [0] = [1]
incr [1] = [2]
--incr [2] = [3]
incr [0,1] = [1,2]
--incr [0,2] = [1,3]
incr [1,0] = [2,1]
-- incr [0,0,0] = [1,1,1]
incr [1,0,0] = [2,1,1]
incr [0,1,0] = [1,2,1]
incr [0,0,1] = [1,1,2]
incr [1,0,0,0] = [2,1,1,1]
incr [0,1,0,0] = [1,2,1,1]
incr [0,0,1,0] = [1,1,2,1]
incr [0,0,0,1] = [1,1,1,2]
|] -- ¤³¤¦¤ä¤Ã¤Æ¤â¥À¥á¡¥
-- :cmd run $ filtGetOne "iniT" "initPred"
iniT = [d|
iniT:: [a] -> [a]
iniT [a] = []
iniT [a,b] = [a]
iniT [a,b,c] = [a,b]
iniT [a,b,c,d] = [a,b,c]
|] -- ¤ª¤Ê¤¸¤ä¤Ä
initPred init = init "foobar" == "fooba"
-- taken from Examples.hs in igor2-0.7.1.3, but equivalence over Ints has to be defined in order to work with igor2, because equivalence over Ints are not defined.
-- These (with eq9 as the BK) should not work when anti-unification is forced. ¤Ê¤¼¤Ê¤é¡¤succ¤¬Æ³Æþ¤µ¤ì¤ÆintroBK¤¬Á˳²¤µ¤ì¤ë¤«¤é¡¥1¤«¤é¤Ç¤Ê¤¯0¤«¤é»Ï¤á¤ë¤Ù¤¡¥
mem15 = [d|
mem :: Int -> [Int] -> Bool
mem 1 [] = False
mem 2 [] = False
mem 3 [] = False
mem 1 [1] = True
mem 2 [1] = False
mem 3 [1] = False
mem 1 [2] = False
mem 2 [2] = True
mem 3 [2] = False
mem 1 [3] = False
mem 2 [3] = False
mem 3 [3] = True
mem 1 [2,1] = True
mem 2 [2,1] = True
--member 1 [3,1,2] = [1,2]
--member 1 [1,2,3] = [1,2,3]
mem 1 [3,2,1] = True
|]
mem8 = [d|
mem :: Int -> [Int] -> Bool
mem 1 [] = False
mem 2 [] = False
mem 1 [1] = True
mem 2 [1] = False
mem 1 [2] = False
mem 2 [2] = True
mem 1 [2,1] = True
mem 2 [2,1] = True
|]
mem6 = [d|
mem :: Int -> [Int] -> Bool
mem 1 [] = False
mem 2 [] = False
mem 1 [1] = True
mem 2 [1] = False
mem 1 [2] = False
mem 2 [2] = True
|]
mem'15 = [d|
mem :: Int -> [Int] -> Bool
mem 0 [] = False
mem 1 [] = False
mem 2 [] = False
mem 0 [0] = True
mem 1 [0] = False
mem 2 [0] = False
mem 0 [1] = False
mem 1 [1] = True
mem 2 [1] = False
mem 0 [2] = False
mem 1 [2] = False
mem 2 [2] = True
mem 0 [1,0] = True
mem 1 [1,0] = True
--member 0 [2,0,1] = [0,1]
--member 0 [0,1,2] = [0,1,2]
mem 0 [2,1,0] = True
|]
mem'6 = [d|
mem :: Int -> [Int] -> Bool
mem 0 [] = False
mem 1 [] = False
mem 0 [0] = True
mem 1 [0] = False
mem 0 [1] = False
mem 1 [1] = True
|]
mem'8 = [d|
mem :: Int -> [Int] -> Bool
mem 0 [] = False
mem 1 [] = False
mem 0 [0] = True
mem 1 [0] = False
mem 0 [1] = False
mem 1 [1] = True
mem 0 [0,1] = True
mem 1 [0,1] = True
|]
-- rev n = fmap (take (n+1)) [d| f :: [a]->[a]; f [] = []; f [a] = [a]; f [a,b] = [b,a]; f [a,b,c] = [c,b,a]; f [a,b,c,d] = [d,c,b,a] |]
-- :cmd run $ filtGetOne "oddpos6" "oddposPred"
oddpos6 = [d|
oddpos :: [a] -> [a]
oddpos [] = []
oddpos [a] = [a]
oddpos [a,b] = [a]
oddpos [a,b,c] = [a,c]
oddpos [a,b,c,d] = [a,c]
oddpos [a,b,c,d,e] = [a,c,e]
|]
oddposPred oddpos = oddpos "abcdef" == "ace" && oddpos "abc" == "ac"
-- :cmd run $ filtGetOne "lasT" "lastPred"
lasT = [d|
lasT :: [a] -> a
lasT [a] = a
lasT [a,b] = b
lasT [a,b,c] = c
lasT [a,b,c,d] = d
|]
lastPred last = last "abcde" == 'e'
lastM = [d|
lastM :: [a] -> Maybe a
lastM [] = Nothing
lastM [a] = Just a
lastM [a,b] = Just b
lastM [a,b,c] = Just c
lastM [a,b,c,d] = Just d
|] -- Maybe¤ä¤Ã¤Æ¤Ê¤«¤Ã¤¿¡¥
-- :cmd run $ filtGetOne "lasts" "lastsPred"
lasts = [d|
lasts :: [[a]] -> [a]
lasts [] = []
lasts [[a]] = [a]
lasts [[a,b]] = [b]
lasts [[a,b,c]] = [c]
lasts [[b],[a]] = [b,a]
lasts [[c],[a,b]] = [c,b]
lasts [[a,b],[c,d]] = [b,d]
lasts [[c,d],[b]] = [d,b]
lasts [[c],[d,e],[f]] = [c,e,f]
lasts [[c,d],[e,f],[g]] = [d,f,g]
|]
lasts' = [d|
lasts :: [[a]] -> [a]
lasts [] = []
lasts [[a]] = [a]
lasts [[a,b]] = [b]
-- lasts [[a,b,c]] = [c]
lasts [[b],[a]] = [b,a]
lasts [[c],[a,b]] = [c,b]
lasts [[a,b],[c,d]] = [b,d]
lasts [[c,d],[b]] = [d,b]
-- lasts [[c],[e],[f]] = [c,e,f]
-- lasts [[c],[d,e],[f]] = [c,e,f]
-- lasts [[c,d],[e,f],[g]] = [d,f,g]
-- lasts [[c,d],[e,f],[h,g]] = [d,f,g]
|]
lastsPred lasts = lasts ["abcdef", "abc", "abcde"] == "fce"
-- :cmd run $ filtGetOne "lens" "lengthsPred"
lens = [d|
lengths :: [[a]] -> [Int]
lengths [] = []
lengths [[]] = [0]
lengths [[a]] = [1]
lengths [[b,a]] = [2]
--lengths [[c,b,a]] = [S(S(1)]
lengths [[],[]] = [0, 0]
lengths [[],[a]] = [0,1]
lengths [[],[b,a]] = [0,2]
|]
lengthsPred :: ([String] -> [Int]) -> Bool
lengthsPred lengths = lengths ["abcdef", "abc", "abcde"] == [6,3,5]
-- :cmd run $ filtGetOne "multFst" "multFstPred"
multFst = [d|
multfst :: [a] -> [a]
multfst [] = []
multfst [a] = [a]
multfst [a,b] = [a,a]
multfst [a,b,c] = [a,a,a]
multfst [a,b,c,d] = [a,a,a,a]
--multfst [a,b,c,d,e] = [a,a,a,a,a]
--multfst [a,b,c,d,e,f] = [a,a,a,a,a,a]
|]
multFstPred multfst = multfst "abcdef" == "aaaaaa"
-- :cmd run $ filtGetOne "multLst" "multLstPred"
multLst = [d|
multlst :: [a] -> [a]
multlst [] = []
multlst [a] = [a]
multlst [a,b] = [b,b]
multlst [a,b,c] = [c,c,c]
multlst [a,b,c,d] = [d,d,d,d]
--multlst [a,b,c,d,e] = [e,e,e,e,e]
--multlst [a,b,c,d,e,f] = [f,f,f,f,f,f]
|]
multLstPred multlst = multlst "abcdef" == "ffffff"
-- :cmd run $ filtGetOne "negateall" "negateAllPred"
negateall = [d|
negateAll :: [Bool] -> [Bool]
negateAll [] = []
negateAll [True] = [False]
negateAll [False] = [True]
negateAll [False,False] = [True,True]
negateAll [False,True] = [True,False]
negateAll [True,False] = [False,True]
negateAll [True,True] = [False,False]
|]
negateAllPred f = f [True,False,False,True] == [False,True,True,False] && f [False,True,False] == [True,False,True]
-- :cmd run $ filtGetOne "powset" "(\\powset -> powset \"abcd\" == [\"abcd\",\"abc\",\"abd\",\"ab\",\"acd\",\"ac\",\"ad\",\"a\",\"bcd\",\"bc\",\"bd\",\"b\",\"cd\",\"c\",\"d\",\"\"])"
powset = [d|
powset :: [a] -> [[a]]
powset [] = [[]]
powset [a] = [[a],[]]
powset [a,b] = [[a,b],[a],[b],[]]
powset [a,b,c] = [[a,b,c],[a,b],[a,c],[a],[b,c],[b],[c],[]]
--powset [a,b,c,d] = [[a,b,c,d],[a,b,c],[a,b,d],[a,b],[a,c,d],[a,c],[a,d],[a],[b,c,d],[b,c],[b,d],[b],[c,d],[c],[d],[]]
|]
odD = [d|
odD :: Int -> Bool
odD 0 = False
odD 1 = True
odD 2 = False
odD 3 = True
odD 4 = False
odD 5 = True
|]
-- :cmd run $ filtGetOne "reversE" "(\\rev -> rev \"abcde\" == \"edcba\")"
reversE = [d|
reversE :: [a] -> [a]
reversE [] = []
reversE [a] =[a]
reversE [a,b] = [b,a]
reversE [a,b,c] = [c,b,a]
reversE [a,b,c,d] = [d,c,b,a]
--reversE [a,b,c,d,e] = [e,d,c,b,a]
--reversE [a,b,c,d,e,f] = [f,e,d,c,b,a]
|]
revPred rev = rev "abcdef" == "fedcba"
-- :cmd run $ filtGetOne "shiftl" "shiftlPred"
shiftl = [d|
shiftl :: [a] -> [a]
shiftl [] = []
shiftl [a] = [a]
shiftl [a,b] = [b,a]
shiftl [a,b,c] = [b,c,a]
shiftl [a,b,c,d] = [b,c,d,a]
--shiftl [a,b,c,d,e] = [b,c,d,e,a]
--shiftl [a,b,c,d,e,f] = [b,c,d,e,f,a]
--shiftl [a,b,c,d,e,f,g] = [b,c,d,e,f,g,a]
--shiftl [a,b,c,d,e,f,g,h] = [b,c,d,e,f,g,h,a]
|]
shiftlPred shiftl = shiftl "abcde" == "bcdea"
-- :cmd run $ filtGetOne "shiftr" "shiftrPred"
shiftr = [d|
shiftr :: [a] -> [a]
shiftr [] = []
shiftr [a] = [a]
shiftr [a,b] = [b,a]
shiftr [a,b,c] = [c,a,b]
shiftr [a,b,c,d] = [d,a,b,c]
-- shiftr [a,b,c,d,e] = [e,a,b,c,d]
|]
shiftrPred shiftr = shiftr "abcde" == "eabcd"
-- :cmd run $ filtGetOne "snoc" "snocPred"
snoc = [d|
snoc :: a -> [a] -> [a]
snoc a [] = [a]
snoc b [a] = [a,b]
snoc c [a,b] = [a,b,c]
snoc d [a,b,c] = [a,b,c,d]
--snoc e [a,b,c,d] = [a,b,c,d,e]
--snoc f [a,b,c,d,e] = [a,b,c,d,e,f]
|]
snocPred snoc = snoc 'f' "abcde" == "abcdef"
-- :cmd run $ filtGetOne "suM" "(\\sum -> sum [7,3,8,5] == 23)"
suM = [d|
suM :: [Int] -> Int
suM [] = 0
suM [0] = 0
suM [1] = 1
suM [2] = 2
suM [0,0] = 0
suM [0,1] = 1
suM [0,2] = 2
suM [1,0] = 1
suM [1,1] = 2
suM [1,2] = 3
suM [2,0] = 2
suM [2,1] = 3
suM [2,2] = 4
suM [2,1, 2] = 5
|]
tunedSum n = fmap (takeFunD n) suM
sumPred sum = sum [7,3,8,5] == 23
-- :cmd run $ filtGetOne "swap" "swapPred"
swap = [d|
swap:: [a] -> [a]
swap [] = []
swap [a] = [a]
swap [a,b] = [b,a]
swap [a,b,c] = [b,a,c]
swap [a,b,c,d] = [b,a,d,c]
swap [a,b,c,d,e] = [b,a,d,c,e]
swap [a,b,c,d,e,f] = [b,a,d,c,f,e]
|]
swapPred swap = swap "abcde" == "badce"
-- :cmd run $ filtGetOne "switch" "switchPred"
switch = [d|
switch :: [a] -> [a]
switch [] = []
switch [a] = [a]
switch [a,b] = [b,a]
switch [a,b,c] = [c,b,a]
switch [a,b,c,d] = [d,b,c,a]
--switch [a,b,c,d,e] = [e,b,c,d,a]
--switch [a,b,c,d,e,f] = [f,b,c,d,e,a]
|]
switchPred switch = switch "abcde" == "ebcda"
-- :cmd run $ filtGetOne "takE" "takePred"
takE = [d|
takE :: Int -> [a] -> [a]
takE 0 [] = []
takE 0 [a] = []
takE 0 [a,b] = []
--takE 0 [a,b,c] = []
takE 1 [] = []
takE 1 [a] = [a]
takE 1 [a,b] = [a]
--takE 1 [a,b,c] = [a]
takE 2 [] = []
takE 2 [a] = [a]
takE 2 [a,b] = [a,b]
--takE 2 [a,b,c] = [a,b]
takE 3 [] = []
takE 3 [a] = [a]
takE 3 [a,b] = [a,b]
--takE 3 [a,b,c] = [a,b,c]
|]
takePred :: (Int->String->String) -> Bool
takePred take = take 3 "abcde" == "abc"
-- :cmd run $ filtGetOne "weave" "weavePred"
weave = [d|
weave :: [a] -> [a] -> [a]
weave [] [] = []
weave [a][] = [a]
weave [][c] = [c]
weave [a][c] = [a,c]
weave [a,b][] = [a,b]
weave [][c,d] = [c,d]
weave [a,b][c] = [a,c,b]
weave [a][c,d] = [a,c,d]
weave [a,b][c,d] = [a,c,b,d]
|]
weavePred weave = weave "abc" "def" == "adbecf"
{-
zeros = [d|
zeros :: [Int] -> [Int]
zeros [] = []
zeros [0] = [0]
zeros [S x] = []
zeros [0,S x] = [0]
zeros [S x,0] = [0]
zeros [S x,S y] = []
zeros [0,0] = [0,0]
--zeros [0,S x,S y] = [0]
--zeros [S x,0,S y] = [0]
--zeros [S y,S x,0] = [0]
--zeros [0,0,S x] = [0,0]
--zeros [0,S x,0] = [0,0]
--zeros [S x,0,0] = [0,0]
--zeros [0,0,0] = [0,0,0]
|]
-}
zeros'7 = [d|
zeros :: [Int] -> [Int]
zeros [] = []
zeros [0] = [0]
zeros [1] = []
zeros [0,1] = [0]
zeros [1,0] = [0]
zeros [1,1] = []
zeros [0,0] = [0,0]
|] -- dame
zeros'14 = [d|
zeros :: [Int] -> [Int]
zeros [] = []
zeros [0] = [0]
zeros [1] = []
zeros [0,1] = [0]
zeros [1,0] = [0]
zeros [1,1] = []
zeros [0,0] = [0,0]
zeros [1,1,1] = []
zeros [0,1,1] = [0]
zeros [1,0,1] = [0]
zeros [1,1,0] = [0]
zeros [0,0,1] = [0,0]
zeros [0,1,0] = [0,0]
zeros [1,0,0] = [0,0]
zeros [0,0,0] = [0,0,0]
|] -- dame
zeros'31 = [d|
zeros :: [Int] -> [Int]
zeros [] = []
zeros [0] = [0]
zeros [1] = []
zeros [0,1] = [0]
zeros [1,0] = [0]
zeros [1,1] = []
zeros [0,0] = [0,0]
zeros [1,1,1] = []
zeros [0,1,1] = [0]
zeros [1,0,1] = [0]
zeros [1,1,0] = [0]
zeros [0,0,1] = [0,0]
zeros [0,1,0] = [0,0]
zeros [1,0,0] = [0,0]
zeros [0,0,0] = [0,0,0]
zeros [1,1,1,1] = []
zeros [0,1,1,1] = [0]
zeros [1,0,1,1] = [0]
zeros [1,1,0,1] = [0]
zeros [0,0,1,1] = [0,0]
zeros [0,1,0,1] = [0,0]
zeros [1,0,0,1] = [0,0]
zeros [0,0,0,1] = [0,0,0]
zeros [1,1,1,0] = []
zeros [0,1,1,0] = [0,0]
zeros [1,0,1,0] = [0,0]
zeros [1,1,0,0] = [0,0]
zeros [0,0,1,0] = [0,0,0]
zeros [0,1,0,0] = [0,0,0]
zeros [1,0,0,0] = [0,0,0]
zeros [0,0,0,0] = [0,0,0,0]
|] -- dame
echoOn :: [String] -> [String]
echoOn [] = []
echoOn (x:xs) = ("putStrLn "++ show x) : x : echoOn xs
withEcho :: String -> String
withEcho str = show str ++ '\n' : str ++ "\n"
ins21 = [d|
ins 0 [] = [0]
ins 1 [] = [1]
ins 2 [] = [2]
ins 0 [0] = [0,0]
ins 1 [0] = [0,1]
ins 2 [0] = [0,2]
ins 0 [1] = [0,1]
ins 1 [1] = [1,1]
ins 2 [1] = [1,2]
ins 0 [2] = [0,2]
ins 1 [2] = [1,2]
ins 0 [0,0] = [0,0,0]
ins 1 [0,0] = [0,0,1]
ins 2 [0,0] = [0,0,2]
ins 0 [0,1] = [0,0,1]
ins 1 [0,1] = [0,1,1]
ins 2 [0,1] = [0,1,2]
ins 0 [0,2] = [0,0,2]
ins 1 [0,2] = [0,1,2]
ins 0 [1,1] = [0,1,1]
ins 1 [1,1] = [1,1,1]
|]
ins30 = [d|
ins 0 [] = [0]
ins 1 [] = [1]
ins 2 [] = [2]
ins 0 [0] = [0,0]
ins 1 [0] = [0,1]
ins 2 [0] = [0,2]
ins 0 [1] = [0,1]
ins 1 [1] = [1,1]
ins 2 [1] = [1,2]
ins 0 [2] = [0,2]
ins 1 [2] = [1,2]
ins 2 [2] = [2,2]
ins 0 [0,0] = [0,0,0]
ins 1 [0,0] = [0,0,1]
ins 2 [0,0] = [0,0,2]
ins 0 [0,1] = [0,0,1]
ins 1 [0,1] = [0,1,1]
ins 2 [0,1] = [0,1,2]
ins 0 [0,2] = [0,0,2]
ins 1 [0,2] = [0,1,2]
ins 2 [0,2] = [0,2,2]
ins 0 [1,1] = [0,1,1]
ins 1 [1,1] = [1,1,1]
ins 2 [1,1] = [1,1,2]
ins 0 [1,2] = [0,1,2]
ins 1 [1,2] = [1,1,2]
ins 2 [1,2] = [1,2,2]
ins 0 [2,2] = [0,2,2]
ins 1 [2,2] = [1,2,2]
ins 2 [2,2] = [2,2,2]
|]
bmin = [d|
mi 0 x = 0
mi 1 0 = 0
mi 1 1 = 1
mi 1 2 = 1
mi 2 0 = 0
mi 2 1 = 1
mi 2 2 = 2
|]
bmax = [d|
ma 0 0 = 0
ma 0 1 = 1
ma 0 2 = 2
ma 1 0 = 1
ma 1 1 = 1
ma 1 2 = 2
ma 2 0 = 2
ma 2 1 = 2
ma 2 2 = 2
|]