-- 
-- (c) Susumu Katayama
--
-- This file is supposed to be used with Version 0.8.5 of MagicHaskeller.
-- For previous versions, try:
-- darcs get http://nautilus.cs.miyazaki-u.ac.jp/~skata/ somedirectoryname
-- and retrieve an older version via some darcs command.
{-# OPTIONS -XTemplateHaskell -XNoMonomorphismRestriction -fglasgow-exts #-}
module MagicHaskeller.LibTH(module MagicHaskeller.LibTH, module MagicHaskeller) where

import MagicHaskeller
import System.Random(mkStdGen)
import Control.Monad(liftM2)

initialize, init075, inittv1 :: IO ()
initialize = do setPrimitives (list ++ nat ++ natural ++ mb ++ bool ++ $(p [| (hd :: (->) [a] (Maybe a), (+) :: Int -> Int -> Int, (+) :: Integer -> Integer -> Integer) |]))
                setDepth 10
-- MagicHaskeller version 0.8 ignores the setDepth value and always memoizes.

init075 = do setPG $ mkMemo075 (list ++ nat ++ natural ++ mb ++ bool ++ $(p [| ((+) :: Int -> Int -> Int, (+) :: Integer -> Integer -> Integer) |] ))
             setDepth 10

-- The @tv1@ option prevents type variable @a@ in @forall a. E1(a) -> E2(a) -> ... -> En(a) -> a@ from matching n-ary functions where n>=2.
-- This can safely be used if @(,)@ and @uncurry@ are in the primitive set,
-- because @forall a b c. E1(a->b->c) -> E2(a->b->c) -> ... -> En(a->b->c) -> a -> b -> c@ and @forall a b c. E1((a,b)->c) -> E2((a,b)->c) -> ... -> En((a,b)->c) -> (a,b) -> c@ are isomorphic, and thus the latter can always be used instead of the former.

inittv1 = do setPG $ mkPGOpt (options{primopt = Nothing, tv1 = True})
                             (list ++ nat ++ natural ++ mb ++ bool ++ tuple ++ $(p [| (hd :: (->) [a] (Maybe a), (+) :: Int -> Int -> Int, (+) :: Integer -> Integer -> Integer) |] ))
             setDepth 10

tuple = $(p [| ((,) :: a -> b -> (a,b), uncurry :: (a->b->c) -> (->) (a,b) c) |])

-- Specialized memoization tables. Choose one for quicker results.
mall, mlist, mlist', mnat, mlistnat, mnat_nc  :: ProgramGenerator pg => pg
mall  = mkPG (list ++ nat ++ natural ++ mb ++ bool ++ $(p [| (hd :: (->) [a] (Maybe a), (+) :: Int -> Int -> Int, (+) :: Integer -> Integer -> Integer) |]))
mlist = mkPG list
mlist' = mkPG list'
mnat  = mkPG (nat ++ $(p [| (+) :: Int -> Int -> Int |]))
mnatural  = mkPG (natural ++ $(p [| (+) :: Integer -> Integer -> Integer |]))
mlistnat = mkPG (list ++ nat ++ $(p [| (+) :: Int -> Int -> Int |]))
mlistnatural = mkPG (list ++ natural ++ $(p [| (+) :: Integer -> Integer -> Integer |]))

mnat_nc = mkMemo (nat ++ $(p [| (+) :: Int -> Int -> Int |]))

hd :: [a] -> Maybe a
hd []    = Nothing
hd (x:_) = Just x

-- Prefixed (->) means that the parameter can be matched as an assumption when 'constrL' option is True. Also, this info is used when 'guess' option is True. For example of maybe :: a -> (b->a) -> (->) (Maybe b) a, 
--   Gamma |- A   Gamma,B |- A
--  ---------------------------maybe
--   Gamma, Maybe B |- A
-- rather than
--   Gamma |- A   Gamma,B |- A   Gamma |- Maybe B
--  -----------------------------------------------maybe
--   Gamma |- A
-- This is just for the efficiency reason, and one can use the infixed form, i.e., maybe :: a -> (b->a) -> Maybe b -> a, if efficiency does not matter. In fact, this info is ignored if both 'guess' and 'constrL' options are False.

mb, nat, natural, list', list, bool, boolean, eq, intinst, list1, list2, list3, nats, tuple, rich, rich', debug :: [Primitive]
mb = $(p [| ( Nothing :: Maybe a, Just :: a -> Maybe a, maybe :: a -> (b->a) -> (->) (Maybe b) a ) |] )

nat = $(p [| (0 :: Int, succ :: Int->Int, nat_para :: (->) Int (a -> (Int -> a -> a) -> a)) |] )
natural = $(p [| (0 :: Integer, succ :: Integer->Integer, nat_para :: (->) Integer (a -> (Integer -> a -> a) -> a)) |] )

-- Nat paramorphism
nat_para :: Integral i => i -> a -> (i -> a -> a) -> a
nat_para i x f = np (abs i) -- Version 0.8 does not deal with partial functions very well.
    where np 0 = x
          np i = let i' = i-1
                 in f i' (np i')

list' = $(p [| ([], (:), foldr :: (b -> a -> a) -> a -> (->) [b] a, tail :: [a] -> [a]) |] ) -- foldr's argument order makes the synthesis slower:)
list  = $(p [| ([], (:), list_para :: (->) [b] (a -> (b -> [b] -> a -> a) -> a)) |] )

-- List paramorphism
list_para :: [b] -> a -> (b -> [b] -> a -> a) -> a
list_para []     x f = x
list_para (y:ys) x f = f y ys (list_para ys x f)

bool = $(p [| (True, False, iF :: (->) Bool (a -> a -> a)) |] )

iF :: Bool -> a -> a -> a
iF True  t f = t
iF False t f = f

-- | 'postprocess' replaces uncommon functions like paramorphisms with well-known functions. In future it can do some refactoring.
postprocess :: Exp -> ExpQ
{- This type of patterns is not available yet.
postprocess (AppE (AppE (AppE (VarE 'iF)        p)  t) f) = [| if $(postprocess p) then $(postprocess t) else $(postprocess f) |]
postprocess (AppE (AppE (AppE (VarE 'nat_para)  i)  x) f) = [| let {np 0  = $(postprocess x); np (n+1)  = $(postprocess f) n (np n)}     in np (abs $(postprocess i)) |]
postprocess (AppE (AppE (AppE (VarE 'list_para) xs) x) f) = [| let {lp [] = $(postprocess x); lp (y:ys) = $(postprocess f) y ys (lp ys)} in lp $(postprocess xs) |]
-}
postprocess (AppE (AppE (AppE (VarE name)        p)  t) f)
    = case nameBase name of
        "iF"        -> [| if $(postprocess p) then $(postprocess t) else $(postprocess f) |]
        "nat_para"  -> [| let {np 0  = $(postprocess t); np n  = let i=n-1 in $(postprocess f) i (np i)}     in np (abs $(postprocess p)) |]
        "list_para" -> [| let {lp [] = $(postprocess t); lp (y:ys) = $(postprocess f) y ys (lp ys)} in lp $(postprocess p) |]
postprocess (AppE f x) = [| $(postprocess f) $(postprocess x) |]
-- postprocess (VarE 'iF) = [| \p t f -> if p then t else f |] -- This pattern is actually unnecessary because only eta-long normal expressions will be generated.
-- ...
postprocess (InfixE me1 op me2) = let fmapM f Nothing  = return Nothing
                                      fmapM f (Just x) = fmap Just (f x)
                                  in liftM2 (\e1 e2 -> InfixE e1 op e2) (fmapM postprocess me1) (fmapM postprocess me2)
postprocess (LamE pats e) = fmap (LamE pats) (postprocess e)
postprocess (TupE es) = fmap TupE (mapM postprocess es)
postprocess (ListE es) = fmap ListE (mapM postprocess es)
postprocess (SigE e ty) = fmap (`SigE` ty) (postprocess e)
postprocess e = return e

{-
postprocess :: Exp -> Exp
postprocess (AppE (AppE (AppE (VarE 'iF) p) t) f) = CondE (postprocess p) (postprocess t) (postprocess f)
postprocess (VarE 'iF) = LamE [ VarP n | n <- names ] (CondE p t f)
    where names@[p,t,f] = [ mkName [n] | n <- "ptf" ]
postprocess 
-}

exploit :: (Typeable a, Filtrable a) => (a -> Bool) -> IO ()
exploit pred = filterThenF pred (everything (reallyall::ProgGenSF)) >>= pprs

boolean = $(p [| ((&&) :: Bool -> Bool -> Bool,
                  (||) :: Bool -> Bool -> Bool,
                  not  :: Bool -> Bool) |] )
-- Type classes are not supported yet....
eq = $(p [| ((==) :: Int->Int->Bool,   (/=) :: Int->Int->Bool,
             (==) :: Char->Char->Bool, (/=) :: Char->Char->Bool,
             (==) :: Bool->Bool->Bool, (/=) :: Bool->Bool->Bool,
             (==) :: [Int] ->[Int] ->Bool, (/=) :: [Int] ->[Int]->Bool,
             (==) :: [Char]->[Char]->Bool, (/=) :: [Char]->[Char]->Bool,
             (==) :: [Bool]->[Bool]->Bool, (/=) :: [Bool]->[Bool]->Bool) |] )
-- ...bothered.
intinst = $(p [| ( (<=) :: Int->Int->Bool,
                   (<)  :: Int->Int->Bool,
                   (>=) :: Int->Int->Bool,
                   (>)  :: Int->Int->Bool,
                   max  :: Int->Int->Int,
                   min  :: Int->Int->Int,
                   (-)  :: Int->Int->Int,
                   (*)  :: Int->Int->Int,
                   div  :: Int->Int->Int,
                   mod  :: Int->Int->Int,
                   gcd  :: Int->Int->Int,
                   lcm  :: Int->Int->Int,
                   (^)  :: Int->Int->Int) |])

list1 = $(p [| (map       :: (a -> b) -> (->) [a] [b],
                (++)      :: [a] -> [a] -> [a],
                filter    :: (a -> Bool) -> [a] -> [a],
                concat    :: [[a]] -> [a],
                concatMap :: (a -> [b]) -> (->) [a] [b],
                length    :: (->) [a] Int,
                replicate :: Int -> a -> [a],
                take      :: Int -> [a] -> [a],
                drop      :: Int -> [a] -> [a],
                takeWhile :: (a -> Bool) -> [a] -> [a],
                dropWhile :: (a -> Bool) -> [a] -> [a]) |] )
list2 = $(p [| (
                lines            :: [Char] -> [[Char]],
                words            :: [Char] -> [[Char]],
                unlines            :: [[Char]] -> [Char],
                unwords            :: [[Char]] -> [Char] ) |] )

list3 = $(p [| (reverse :: [a] -> [a],
                and         :: [Bool] -> Bool,
                or          :: [Bool] -> Bool,
                any         :: (a -> Bool) -> (->) [a] Bool,
                all         :: (a -> Bool) -> (->) [a] Bool,
                zipWith          :: (a->b->c) -> (->) [a] ((->) [b] [c]) ) |] )

nats = $(p [| (1 ::Int, 2 :: Int, 3 :: Int) |])

reallyall :: ProgramGenerator pg => pg
reallyall = mkPG rich

nrnds = repeat 5


-- comment out (mkStdGen 123456) when using 0.8.3*


-- Currently only the pg==ConstrLSF case makes sense.
mix, poormix :: ProgramGenerator pg => pg
mix = mkPGSF (mkStdGen 123456)
              nrnds
              (list++bool)
              rich

rich =        (list' ++
                    nat ++
                        mb ++ bool ++ $(p [| (hd :: [a] -> Maybe a, (+) :: Int -> Int -> Int) |]) ++
                    boolean ++ eq ++ intinst ++
                    list1 ++ list2 ++ list3)


poormix = mkPGSF (mkStdGen 123456)
              nrnds
              $(p [| ([] :: [a], True) |] )
              rich

-- just for debugging
ra :: ProgramGenerator pg => pg
ra = mkPG rich'
rich' =      (list'++bool++boolean++
                    list1 ++ list3)

mx :: ProgramGenerator pg => pg
mx = mkPGSF (mkStdGen 123456)
             nrnds
             (list++bool)
             rich'

debug = $(p [| (list_para :: (->) [b] (a -> (b -> [b] -> a -> a) -> a), concatMap :: (a -> [b]) -> (->) [a] [b]) |] )