[examples and batches added
martin.hofmann@uni-bamberg.de**20090826165021] addfile ./expl/AAIPExamples.hs
hunk ./expl/AAIPExamples.hs 1
+module AAIPExamples where
+
+data Peano = Z | S Peano deriving (Show)
+
+add :: Peano -> Peano -> Peano
+add Z Z = Z
+add (S Z) Z = (S Z)
+add Z (S Z) = (S Z)
+add (S Z) (S Z) = S (S Z)
+add Z (S (S Z)) = S (S Z)
+add (S (S Z)) Z = S (S Z)
+add (S Z) (S (S Z)) = S (S (S Z))
+add (S (S Z)) (S Z) = S (S (S Z))
+add (S (S (S Z))) Z = S (S (S Z))
+add Z (S (S (S Z))) = S (S (S Z))
+
+appenD  :: [a] -> [a] -> [a]
+appenD [][] = []
+appenD [a][] = [a]
+appenD [][c] = [c]
+appenD [a][c] = [a,c]
+appenD [a,b][] = [a,b]
+appenD [][c,d] = [c,d]
+appenD [a,b][c] = [a,b,c]
+appenD [a][c,d] = [a,c,d]
+appenD [a,b][c,d] = [a,b,c,d]
+
+droP :: Peano -> [a] -> [a]
+droP Z x = x
+--droP (S Z)         []      = []
+droP (S Z)         [a]     = []
+droP (S Z)         [a,b]   = [b]
+droP (S Z)         [a,b,c] = [b,c]
+--droP (S (S Z))     []      = []
+--droP (S (S Z))     [a]     = []
+droP (S (S Z))     [a,b]   = []
+droP (S (S Z))     [a,b,c] = [c]
+--droP (S (S (S Z))) []      = []
+--droP (S (S (S Z))) [a]     = []
+--droP (S (S (S Z))) [a,b]   = []
+droP (S (S (S Z))) [a,b,c] = []
+
+eveN :: Peano -> Bool
+eveN Z                     = True
+eveN (S Z)                 = False
+eveN (S (S Z))             = True
+eveN (S (S (S Z)))         = False
+eveN (S (S (S (S Z))))     = True
+eveN (S (S (S (S (S Z))))) = False
+
+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]
+
+eq :: Peano -> Peano -> Bool
+eq Z Z = True
+eq Z (S Z) = False
+eq Z (S (S Z)) = False
+eq (S Z) Z = False
+eq (S Z) (S Z) = True
+eq (S Z) (S (S Z)) = False
+eq (S (S Z)) Z = False
+eq (S (S Z)) (S Z) = False
+eq (S (S Z)) (S (S Z)) = True
+
+iniT :: [a] -> [a]
+iniT [a] = []
+iniT [a,b] = [a]
+iniT [a,b,c] = [a,b]
+iniT [a,b,c,d] = [a,b,c]
+
+-- BK for sort only, does not work alone
+insert :: Peano -> [Peano] -> [Peano]
+--insert Z [] = [Z]
+--insert (S Z) [] = [S Z]
+--insert (S(S Z)) = [S(S Z)]
+insert x [] = [x]	
+insert Z [S Z] = [Z,S Z]
+insert Z [S(S Z)] = [Z,S(S Z)]
+--insert Z [S Z, S(S Z)] = [Z, S(S Z)]
+--insert Z (x:xs) = (Z:x:xs)
+insert (S Z) [Z] = [Z,(S Z)]
+insert (S Z) [S(S Z)] = [S Z, S(S Z)]
+insert (S(S Z)) [Z] = [Z, S(S Z)]
+insert (S(S Z)) [S Z] = [S Z, S(S Z)]	
+insert Z [S Z, S(S Z)] = [Z, S Z, S(S Z)]
+insert (S Z) [Z,S(S Z)] = [Z, S Z, S(S Z)]
+insert (S(S Z)) [Z, S Z] = [Z, S Z, S(S Z)]
+
+lasT :: [a] -> a
+lasT [a] = a 
+lasT [a,b] = b
+lasT [a,b,c] = c
+lasT [a,b,c,d] = 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]
+
+lengtH :: [a] -> Peano
+lengtH [] = Z
+lengtH [a] = S Z
+lengtH [a,b] = S(S Z)
+lengtH [a,b,c] = S(S(S Z))
+
+odD :: Peano -> Bool
+odD Z                     = False
+odD (S Z)                 = True
+odD (S (S Z))             = False
+odD (S (S (S Z)))         = True
+odD (S (S (S (S Z))))     = False
+odD (S (S (S (S (S Z))))) = True
+
+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]
+oddpos [a,b,c,d,e,f] = [a,c,e]
+
+repeatfirst :: [a] -> [a]
+repeatfirst [a] = [a]
+repeatfirst [a,b] = [a,a]
+repeatfirst [a,b,c] = [a,a,a]
+repeatfirst [a,b,c,d] = [a,a,a,a]
+
+repeatlast :: [a] -> [a]
+repeatlast [] = []
+repeatlast [a] = [a]
+repeatlast [a,b] = [b,b]
+repeatlast [a,b,c] = [c,c,c]
+repeatlast [a,b,c,d] = [d,d,d,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]
+
+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]
+
+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]
+
+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]
+
+sort :: [Peano] -> [Peano]
+sort [] = []
+sort [Z]        = [Z]
+sort [S Z]      = [S Z]
+--sort [S(S Z)]   = [S(S Z)]	
+sort [Z,S Z]        = [Z,S Z]
+--sort [Z,S(S Z)]     = [Z,S(S Z)]
+sort [S Z, Z]       = [Z,S Z]
+--sort [S Z,S(S Z)]   = [S Z,S(S Z)]
+--sort [S(S Z), Z]    = [Z,S(S Z)]
+--sort [S(S Z),S Z]   = [S Z,S(S Z)]	
+--sort [Z,S Z,S(S Z)] = [Z,S Z,S(S Z)]
+--sort [Z,S(S Z),S Z] = [Z,S Z,S(S Z)]
+--sort [S Z,Z,S(S Z)] = [Z,S Z,S(S Z)]
+--sort [S Z,S(S Z),Z] = [Z,S Z,S(S Z)]
+--sort [S(S Z),Z,S Z] = [Z,S Z,S(S Z)]
+sort [S(S Z),S Z,Z] = [Z,S Z,S(S Z)]
+
+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]
+
+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]
+
+taiL :: [a] -> [a]
+taiL [a] = []
+taiL [a,b] = [b]
+taiL [a,b,c] = [b,c]
+taiL [a,b,c,d] = [b,c,d]
+
+takE :: Peano -> [a] -> [a]
+takE Z             []      = []
+takE Z             [a]     = []
+takE Z             [a,b]   = []
+--takE Z             [a,b,c] = []
+takE (S Z)         []      = []
+takE (S Z)         [a]     = [a]
+takE (S Z)         [a,b]   = [a]
+--takE (S Z)         [a,b,c] = [a]
+takE (S (S Z))     []      = []
+takE (S (S Z))     [a]     = [a]
+takE (S (S Z))     [a,b]   = [a,b]
+--takE (S (S Z))     [a,b,c] = [a,b]
+--takE (S (S (S Z))) []      = []
+--takE (S (S (S Z))) [a]     = [a]
+--takE (S (S (S Z))) [a,b]   = [a,b]
+--takE (S (S (S Z))) [a,b,c] = [a,b,c]
+
+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]
+
addfile ./expl/AAIPbatch.txt
hunk ./expl/AAIPbatch.txt 1
+:yell "...Load example file" 
+:load ./expl/AAIPExamples.hs
+:y "...set simplification to TRUE"
+:s +simplify
+
+--:y "...generalise and test 'add'"
+--:g add; :test add on "add (S(S(S(S(S Z))))) (S(S(S(S(S Z)))))"
+
+:y "...generalise and test 'appenD'"
+:g appenD; :test appenD on "appenD [1,1,1,1,1][2,2,2,2,2]"
+
+:y "...generalise and test 'droP'"
+:g droP; :test droP on "droP (S(S(S(S(S Z))))) [1,1,1,1,1,0,0,0]"
+
+--:y "...generalise and test 'eveN'"
+--:g eveN; :test eveN on "map eveN [Z,S Z, S (S Z), S(S(S Z)), S(S(S(S Z))), S(S(S(S(S Z)))), S(S(S(S(S(S Z))))), S(S(S(S(S(S(S Z))))))]"
+
+:y "...generalise and test 'evenpos'"
+:g evenpos; :test evenpos on "evenpos [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'eq'"
+--:g eq; :test eq on "map (uncurry eq) [ (S(S(S(S(S(S Z))))),S(S(S(S(S(S Z)))))), (S(S(S(S(S Z)))),S(S(S(S(S(S(S Z))))))), (S(S(S(S(S(S(S Z)))))),S(S(S(S(S Z)))))]"
+
+:y "...generalise and test 'iniT'"
+:g iniT; :test iniT on "iniT [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'lasT'"
+:g lasT; :test lasT on "lasT [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'lasts'"
+:g lasts; :test lasts on "lasts [[1,2,3],[9,8,7,6,5,4,3],[3,3,3,3,3,3],[1,4,5,6,7,8,3]]"
+
+:y "...generalise and test 'lengtH'"
+:g lengtH; :test lengtH on "lengtH [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'odD'"
+--:g odD; :test odD on "map odD [Z,S Z, S (S Z), S(S(S Z)), S(S(S(S Z))), S(S(S(S(S Z)))), S(S(S(S(S(S Z))))), S(S(S(S(S(S(S Z))))))]"
+
+:y "...generalise and test 'odD, eveN'"
+:g odD, eveN; :test odD, eveN on "map (\a -> (odd a, eveN a)) [Z,S Z, S (S Z), S(S(S Z)), S(S(S(S Z))), S(S(S(S(S Z)))), S(S(S(S(S(S Z))))), S(S(S(S(S(S(S Z))))))]"
+
+:y "...generalise and test 'oddpos'"
+:g oddpos; :test oddpos on "oddpos [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'repeatfirst'"
+:g repeatfirst; :test repeatfirst on "repeatfirst [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'repeatlast'"
+:g repeatlast; :test repeatlast on "repeatlast [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'reversE'"
+:g reversE; :test reversE on "reversE [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'reversE, snoc'"
+:g reversE, snoc; :test reversE, snoc on "reversE [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'reversE with snoc'"
+--:g reversE with snoc; :test reversE with snoc on "reversE [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'shiftl'"
+:g shiftl; :test shiftl on "shiftl [1,2,3,4,5,6,7,8]"
+
+:y "...generalise 'sort' with 'insert'"
+:g sort with insert; -- :test sort with insert on "sort [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'shiftr'"
+:g shiftr; :test shiftr on "shiftr [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'snoc'"
+--:g snoc; :test snoc on "snoc 9 [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'swap'"
+:g swap; :test swap on "swap [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'switch'"
+:g switch; :test switch on "switch [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'taiL'"
+--:g taiL; :test taiL on "taiL [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'takE'"
+:g takE; :test takE on "takE (S(S(S(S(S Z))))) [1,1,1,1,1,0,0,0]"
+
+:y "...generalise and test 'weave'"
+:g weave; :test weave on "weave [1,1,1,1,1,0,0,0][2,2,2,2,2]"
+
+:y "That's all! Finished!"
+:q
+
addfile ./expl/Miyazaki.bat
hunk ./expl/Miyazaki.bat 1
+:yell "...Load example file" 
+:load ./expl/Examples.hs
+:y "...set simplification to TRUE"
+:s +simplify
+
+:y "...generalise and test 'reverse'"
+:y " - - - Automatically induce and use subprograms - - - "
+:g reversE; :test reversE on "reversE [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'sum'"
+:y " - - - Complex case distinctions - - - "
+:g suM; :test suM on "suM [Z,S Z, S (S Z), S(S Z)]"
+
+:y "...generalise and test 'lasts'"
+:g lasts; :test lasts on "lasts [[1,2,3],[9,8,7,6,5,4,3],[3,3,3,3,3,3],[1,4,5,6,7,8,3]]"
+
+:y "...generalise and test '<='"
+:y " - - - Recursion over multiple arguments - - - "
+:g leq; :test leq on "map (uncurry leq) [ (S(S(S(S(S(S Z))))),S(S(S(S(S(S Z)))))), (S(S(S(S(S Z)))),S(S(S(S(S(S(S Z))))))), (S(S(S(S(S(S(S Z)))))),S(S(S(S(S Z)))))]"
+
+:y "...generalise and test 'weave'"
+:g weave; :test weave on "weave [1,1,1,1,1,0,0,0][2,2,2,2,2]"
+
+:y "...generalise and test 'odD, eveN'"
+:y " - - - Mutual recursive functions - - - "
+:g odD, eveN; :test odD, eveN on "map (\a -> (odd a, eveN a)) [Z,S Z, S (S Z), S(S(S Z)), S(S(S(S Z))), S(S(S(S(S Z)))), S(S(S(S(S(S Z))))), S(S(S(S(S(S(S Z))))))]"
+
+
+:y "...generalise and test 'add'"
+:g add; :test add on "add (S(S(S(S(S Z))))) (S(S(S(S(S Z)))))"
+
+:y "...generalise and test 'appenD'"
+:g appenD; :test appenD on "appenD [1,1,1,1,1][2,2,2,2,2]"
+
+:y "...generalise and test 'droP'"
+:g droP; :test droP on "droP (S(S(S(S(S Z))))) [1,1,1,1,1,0,0,0]"
+
+--:y "...generalise and test 'eveN'"
+--:g eveN; :test eveN on "map eveN [Z,S Z, S (S Z), S(S(S Z)), S(S(S(S Z))), S(S(S(S(S Z)))), S(S(S(S(S(S Z))))), S(S(S(S(S(S(S Z))))))]"
+
+:y "...generalise and test 'evenpos'"
+:g evenpos; :test evenpos on "evenpos [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'eq'"
+--:g eq; :test eq on "map (uncurry eq) [ (S(S(S(S(S(S Z))))),S(S(S(S(S(S Z)))))), (S(S(S(S(S Z)))),S(S(S(S(S(S(S Z))))))), (S(S(S(S(S(S(S Z)))))),S(S(S(S(S Z)))))]"
+
+:y "...generalise and test 'iniT'"
+:g iniT; :test iniT on "iniT [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'lasT'"
+:g lasT; :test lasT on "lasT [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'lengtH'"
+:g lengtH; :test lengtH on "lengtH [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'odD'"
+--:g odD; :test odD on "map odD [Z,S Z, S (S Z), S(S(S Z)), S(S(S(S Z))), S(S(S(S(S Z)))), S(S(S(S(S(S Z))))), S(S(S(S(S(S(S Z))))))]"
+
+:y "...generalise and test 'oddpos'"
+:g oddpos; :test oddpos on "oddpos [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'repeatfirst'"
+:g repeatfirst; :test repeatfirst on "repeatfirst [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'repeatlast'"
+:g repeatlast; :test repeatlast on "repeatlast [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'reversE with snoc'"
+--:g reversE with snoc; :test reversE with snoc on "reversE [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'shiftl'"
+:g shiftl; :test shiftl on "shiftl [1,2,3,4,5,6,7,8]"
+
+:y "...generalise 'sort' with 'insert'"
+:g sort with insert; -- :test sort with insert on "sort [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'shiftr'"
+:g shiftr; :test shiftr on "shiftr [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'snoc'"
+--:g snoc; :test snoc on "snoc 9 [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'swap'"
+:g swap; :test swap on "swap [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'switch'"
+:g switch; :test switch on "switch [1,2,3,4,5,6,7,8]"
+
+--:y "...generalise and test 'taiL'"
+--:g taiL; :test taiL on "taiL [1,2,3,4,5,6,7,8]"
+
+:y "...generalise and test 'takE'"
+:g takE; :test takE on "takE (S(S(S(S(S Z))))) [1,1,1,1,1,0,0,0]"
+
+
+:y "That's all! Finished!"
+:q
+
addfile ./expl/TestExpl.hs
hunk ./expl/TestExpl.hs 1
+
+module TestExpl where
+
+
+data Peano = Z | S Peano deriving (Show,Eq,Ord)
+
+foo :: a -> a
+foo a = a
+
+-- BK for sort only, does not work alone
+insert :: Peano -> [Peano] -> [Peano]
+--insert Z [] = [Z]
+--insert (S Z) [] = [S Z]
+--insert (S(S Z)) = [S(S Z)]
+insert x [] = [x]   
+insert Z [S Z] = [Z,S Z]
+insert Z [S(S Z)] = [Z,S(S Z)]
+--insert Z [S Z, S(S Z)] = [Z, S(S Z)]
+--insert Z (x:xs) = (Z:x:xs)
+insert (S Z) [Z] = [Z,(S Z)]
+insert (S Z) [S(S Z)] = [S Z, S(S Z)]
+insert (S(S Z)) [Z] = [Z, S(S Z)]
+insert (S(S Z)) [S Z] = [S Z, S(S Z)]   
+insert Z [S Z, S(S Z)] = [Z, S Z, S(S Z)]
+insert (S Z) [Z,S(S Z)] = [Z, S Z, S(S Z)]
+insert (S(S Z)) [Z, S Z] = [Z, S Z, S(S Z)]
+
+mem :: Int -> [Int] -> Bool
+mem x [] = False
+mem 1 [1] = True
+mem 1 [2] = False
+mem 2 [1] = False
+mem 2 [2] = True
+mem 1 [2,1] = True
+mem 1 [2,2] = False
+mem 2 [1,2] = True
+mem 2 [1,1] = False
+
+evens :: [Peano] -> [Peano]
+evens []  = []
+evens [Z] = [Z]
+evens [Z,Z] = [Z,Z]
+evens [Z,S Z] = [Z]
+evens [Z,S (S Z)] = [Z,S (S Z)]
+evens [Z,S (S (S Z))] = [Z]
+evens [S Z, Z] = [Z]
+evens [S Z, S Z] = []
+evens [S Z, S (S Z)] = [S (S Z)]
+evens [S Z, S( S (S Z))] = []
+evens [S (S Z), Z] = [S (S Z),Z]
+evens [S (S Z), S Z] = [S (S Z)]
+evens [S (S Z), S (S Z)] = [S (S Z),S (S Z)]
+evens [S (S Z), S( S (S Z))] = [S (S Z)]
+evens [S( S (S Z)), Z] = [Z]
+evens [S( S (S Z)), S Z] = []
+evens [S( S (S Z)), S (S Z)] = [S (S Z)]
+evens [S( S (S Z)), S( S (S Z))] = []
+
+zeros :: [Peano] -> [Peano]
+zeros [] = []
+zeros [Z] = [Z]
+zeros [S x] = []
+zeros [Z,S x] = [Z]
+zeros [S x,Z] = [Z]
+zeros [S x,S y] = []
+zeros [Z,Z] = [Z,Z]
+zeros [Z,S x,S y] = [Z]
+zeros [S x,Z,S y] = [Z]
+zeros [S y,S x,Z] = [Z]
+zeros [Z,Z,S x] = [Z,Z]
+zeros [Z,S x,Z] = [Z,Z]
+zeros [S x,Z,Z] = [Z,Z]
+zeros [Z,Z,Z] = [Z,Z,Z]
+