-- 
-- (C) Susumu Katayama
--

module MagicHaskeller.RunAnalytical(
  -- | This module provides analytically-generate-and-test synthesis, i.e. synthesis by filtration of analytically generated (many) expressions.
  --   Actions whose name ends with F use random testing filter (like 'MagicHaskeller.filterThenF') in order to reduce the number of expressions.
  --
  --   ATTENTION: This module is supposed to be used under GHCi environment. Currently it is known not to work when executed as an a.out.
  --   Also, this module is tested only on Linux, and does not work with Windows. Another point is that currently functions in this module only
  --   work with known types appearing in 'MagicHaskeller.CoreLang.defaultPrimitives'.
  
  -- ** Re-exported modules
  module MagicHaskeller, module MagicHaskeller.ExecuteAPI610, module MagicHaskeller.Analytical, 
  {-
  -- ** Synthesizers which will be able to be used with any types but currently do not work with unknown types.
  -- *** All in one actions
  quickStartC, quickStartCF, 
  -- | 'filterGet1' and its friends can be used to synthesize one expression satisfying the given condition. For example,
  -- >>> session <- prepareAPI []
  -- >>> filterGet1_ session $(c [d| f [] = 0; f [a] = 1; f [a,b] = 2 |]) (\f -> f "foobar" == 6)
  -- > \a -> let fa (b@([])) = 0
  -- >           fa (b@(_ : d)) = succ (fa d)
  -- >       in fa a
  filterGet1_, filterGet1, filterGet1BK, 
  -- | Unlike 'filterGet1' and its friends, the following three functions do not print anything but only return results silently.
  getFilt, getFiltF, getAll,  
  -}
  
  {- -- ** Synthesizers which are easier to use that can be used only with types appearing in 'MagicHaskeller.CoreLang.defaultPrimitives' -}
  -- | All in one actions
  quickStart, quickStartF, 
  -- | 'filterGet1' and its friends can be used to synthesize one expression satisfying the given condition. For example,
  {- -- *** counterparts to 'filterGet1_', 'filterGet1', and 'filterGet1BK' -}
  filterGetOne_, filterGetOne, filterGetOneBK, 
  -- | Unlike 'filterGetOne' and its friends, the following three functions do not print anything but only return results silently.
  {- -- *** counterparts to 'getFilt', 'getFiltF', and 'getAll' -}
  synthFilt, synthFiltF, synthAll,
  {- -- *** counterpart to 'noBK' -}
  -- | 'noBKQ' can be used as the background knowledge for showing that no background knowledge functions are used.
  noBKQ
  ) where
import MagicHaskeller
import MagicHaskeller.ExecuteAPI610 -- use ExecuteAPI for GHC 6.8.* and below
import MagicHaskeller.Analytical
import Language.Haskell.TH
import HscTypes(HscEnv)
import MagicHaskeller.Classification(Filtrable)
import System.IO.Unsafe
import MagicHaskeller.GetTime
import System.IO


prepare :: IO HscEnv
prepare = [FilePath] -> [FilePath] -> IO HscEnv
prepareAPI [] [FilePath
"MagicHaskeller.RunAnalytical"]

quickStartC :: (Typeable a) =>
                     SplicedPrims -- ^ target I/O pairs
                     -> SplicedPrims -- ^ I/O pairs for background knowledge functions
                     -> (a -> Bool)  -- ^ test function
                     -> IO ()
quickStartC :: SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO ()
quickStartC SplicedPrims
tgt SplicedPrims
bk a -> Bool
pred = do HscEnv
session <- IO HscEnv
prepare 
                             Every a
tss     <- HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
forall a.
Typeable a =>
HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
getFilt HscEnv
session SplicedPrims
tgt SplicedPrims
bk a -> Bool
pred
                             Every a -> IO ()
forall a. Every a -> IO ()
pprs Every a
tss
quickStartCF :: (Filtrable a, Typeable a) =>
                     SplicedPrims -- ^ target I/O pairs
                     -> SplicedPrims -- ^ I/O pairs for background knowledge functions
                     -> (a -> Bool)  -- ^ test function
                     -> IO ()
quickStartCF :: SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO ()
quickStartCF SplicedPrims
tgt SplicedPrims
bk a -> Bool
pred = do HscEnv
session <- IO HscEnv
prepare 
                              Every a
tss <- HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
forall a.
(Filtrable a, Typeable a) =>
HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
getFiltF HscEnv
session SplicedPrims
tgt SplicedPrims
bk a -> Bool
pred
                              Every a -> IO ()
forall a. Every a -> IO ()
pprs Every a
tss
filterGet1_ :: (Typeable a) => 
               HscEnv               -- ^ session in which synthesized expressions are run 
               -> SplicedPrims      -- ^ target I/O pairs
               -> (a -> Bool)       -- ^ test function
               -> IO ()
filterGet1_ :: HscEnv -> SplicedPrims -> (a -> Bool) -> IO ()
filterGet1_ HscEnv
s SplicedPrims
t a -> Bool
p = HscEnv -> SplicedPrims -> (a -> Bool) -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> SplicedPrims -> (a -> Bool) -> IO (Every a)
filterGet1 HscEnv
s SplicedPrims
t a -> Bool
p IO (Every a) -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
filterGet1  :: (Typeable a) => 
               HscEnv               -- ^ session in which synthesized expressions are run 
               -> SplicedPrims      -- ^ target I/O pairs
               -> (a -> Bool)       -- ^ test function
               -> IO (Every a)
filterGet1 :: HscEnv -> SplicedPrims -> (a -> Bool) -> IO (Every a)
filterGet1 HscEnv
session SplicedPrims
tgt = HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
forall a.
Typeable a =>
HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
filterGet1BK HscEnv
session SplicedPrims
tgt SplicedPrims
noBK
filterGet1BK :: (Typeable a) => 
                HscEnv               -- ^ session in which synthesized expressions are run 
                -> SplicedPrims      -- ^ target I/O pairs
                -> SplicedPrims      -- ^ I/O pairs for background knowledge functions
                -> (a -> Bool)       -- ^ test function
                -> IO (Every a)
filterGet1BK :: HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
filterGet1BK HscEnv
session SplicedPrims
tgt SplicedPrims
bk a -> Bool
predicate = do Every a
tss <- HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
forall a.
Typeable a =>
HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
getFilt HscEnv
session SplicedPrims
tgt SplicedPrims
bk a -> Bool
predicate
                                           FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Exp -> FilePath
forall a. Ppr a => a -> FilePath
pprint (Exp -> FilePath) -> Exp -> FilePath
forall a b. (a -> b) -> a -> b
$ (Exp, a) -> Exp
forall a b. (a, b) -> a
fst ((Exp, a) -> Exp) -> (Exp, a) -> Exp
forall a b. (a -> b) -> a -> b
$ [(Exp, a)] -> (Exp, a)
forall a. [a] -> a
head ([(Exp, a)] -> (Exp, a)) -> [(Exp, a)] -> (Exp, a)
forall a b. (a -> b) -> a -> b
$ Every a -> [(Exp, a)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat Every a
tss
                                           Every a -> IO (Every a)
forall (m :: * -> *) a. Monad m => a -> m a
return Every a
tss

getFilt  :: (Typeable a) =>
                     HscEnv          -- ^ session in which synthesized expressions are run 
                     -> SplicedPrims -- ^ target I/O pairs
                     -> SplicedPrims -- ^ I/O pairs for background knowledge functions
                     -> (a -> Bool)  -- ^ test function
                     -> IO (Every a)
getFilt :: HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
getFilt  HscEnv
session SplicedPrims
tgt SplicedPrims
bk a -> Bool
pred = (a -> Bool) -> Every a -> IO (Every a)
forall a. Typeable a => (a -> Bool) -> Every a -> IO (Every a)
filterThen  a -> Bool
pred (Every a -> IO (Every a)) -> IO (Every a) -> IO (Every a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HscEnv -> SplicedPrims -> SplicedPrims -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> SplicedPrims -> SplicedPrims -> IO (Every a)
getAll HscEnv
session SplicedPrims
tgt SplicedPrims
bk
getFiltF :: (Filtrable a, Typeable a) =>
                     HscEnv          -- ^ session in which synthesized expressions are run 
                     -> SplicedPrims -- ^ target I/O pairs
                     -> SplicedPrims -- ^ I/O pairs for background knowledge functions
                     -> (a -> Bool)  -- ^ test function
                     -> IO (Every a)
getFiltF :: HscEnv
-> SplicedPrims -> SplicedPrims -> (a -> Bool) -> IO (Every a)
getFiltF HscEnv
session SplicedPrims
tgt SplicedPrims
bk a -> Bool
pred = (a -> Bool) -> Every a -> IO (Every a)
forall a.
(Typeable a, Filtrable a) =>
(a -> Bool) -> Every a -> IO (Every a)
filterThenF a -> Bool
pred (Every a -> IO (Every a)) -> IO (Every a) -> IO (Every a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HscEnv -> SplicedPrims -> SplicedPrims -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> SplicedPrims -> SplicedPrims -> IO (Every a)
getAll HscEnv
session SplicedPrims
tgt SplicedPrims
bk
getAll :: (Typeable a) => 
          HscEnv           -- ^ session in which synthesized expressions are run 
          -> SplicedPrims  -- ^ target I/O pairs
          -> SplicedPrims  -- ^ I/O pairs for background knowledge functions
          -> IO (Every a)
getAll :: HscEnv -> SplicedPrims -> SplicedPrims -> IO (Every a)
getAll  HscEnv
session SplicedPrims
tgt SplicedPrims
bk = HscEnv -> [[Exp]] -> IO (Every a)
forall a. HscEnv -> [[Exp]] -> IO (Every a)
thExpssToEvery HscEnv
session (SplicedPrims -> SplicedPrims -> [[Exp]]
getManyTyped SplicedPrims
tgt SplicedPrims
bk)


-- Functions appearing from here are easier to use, but they work only for limited types, included in 'defaultPrimitives'.

noBKQ :: Q [Dec]
noBKQ :: Q [Dec]
noBKQ = [Dec] -> Q [Dec]
forall (m :: * -> *) a. Monad m => a -> m a
return []

-- main = quickStart (return [rev]) noBKQ (\f -> f "abcdef" == "fedcba")
{-
main = quickStart [d| f :: Int->Int; f 0 = 0; f 1 = 3; f 2 = 6 |] noBKQ (\f -> f (10::Int) == (30::Int))
-}
{-
main = quickStart [d| f::[a] -> Int; f [] = 0; f [a] = 3; f [a,b] = 6 |] noBKQ (\f -> f "hogehoge" == (24::Int))
-}
{-
main = quickStart [d| f::[a] -> a; f [a] = a; f [a,b] = b; f [a,b,c] = c |] noBKQ (\f -> f "hogehoge" == 'e')
-}
-- | Example of 'quickStart'
--
-- >>> quickStart [d| f [] = 0; f [a] = 1 |] noBKQ (\f -> f "12345" == 5)
-- > \a -> let fa (b@([])) = 0
-- >           fa (b@(c : d)) = succ (fa d)
-- >       in fa a :: forall t2 . [t2] -> Int
-- > ^CInterrupted.
quickStart :: (Typeable a) => 
              Q [Dec]        -- ^ target I/O pairs
              -> Q [Dec]     -- ^ I/O pairs for background knowledge functions
              -> (a -> Bool) -- ^ test function
              -> IO ()
quickStart :: Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO ()
quickStart Q [Dec]
iops Q [Dec]
bk a -> Bool
pred = do HscEnv
session <- IO HscEnv
prepare
                             Every a
tss <- HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
synthFilt HscEnv
session Q [Dec]
iops Q [Dec]
bk a -> Bool
pred
                             Every a -> IO ()
forall a. Every a -> IO ()
pprs Every a
tss
quickStartF :: (Filtrable a, Typeable a) => 
               Q [Dec]         -- ^ target I/O pairs
               -> Q [Dec]      -- ^ I/O pairs for background knowledge functions
               -> (a -> Bool)  -- ^ test function
               -> IO ()
quickStartF :: Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO ()
quickStartF Q [Dec]
iops Q [Dec]
bk a -> Bool
pred = do HscEnv
session <- IO HscEnv
prepare
                              Every a
tss <- HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
forall a.
(Filtrable a, Typeable a) =>
HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
synthFiltF HscEnv
session Q [Dec]
iops Q [Dec]
bk a -> Bool
pred
                              Every a -> IO ()
forall a. Every a -> IO ()
pprs Every a
tss

batchExample :: IO ()
batchExample = do HscEnv
session <- IO HscEnv
prepare
                  let f :: Q [Dec] -> ((FilePath -> FilePath) -> Bool) -> IO ()
f = HscEnv -> Q [Dec] -> ((FilePath -> FilePath) -> Bool) -> IO ()
forall a. Typeable a => HscEnv -> Q [Dec] -> (a -> Bool) -> IO ()
filterGetOne_ HscEnv
session
                  FilePath -> [IO ()] -> IO ()
forall a. FilePath -> [IO a] -> IO ()
batchWrite FilePath
"example.dat" [ Q [Dec] -> ((FilePath -> FilePath) -> Bool) -> IO ()
f [d| reverse [] = []; reverse [a] = [a]; reverse [a,b] = [b,a]; reverse [a,b,c] = [c,b,a] |] (\FilePath -> FilePath
r -> FilePath -> FilePath
r FilePath
"abcd" FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
"dcba")
                                           , Q [Dec] -> ((FilePath -> FilePath) -> Bool) -> IO ()
f [d| 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]; |] (\FilePath -> FilePath
s -> FilePath -> FilePath
s FilePath
"abcde" FilePath -> FilePath -> Bool
forall a. Eq a => a -> a -> Bool
== FilePath
"ebcda")
                                           ]
filterGetOne_ :: HscEnv -> Q [Dec] -> (a -> Bool) -> IO ()
filterGetOne_ HscEnv
s Q [Dec]
t a -> Bool
p = HscEnv -> Q [Dec] -> (a -> Bool) -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> Q [Dec] -> (a -> Bool) -> IO (Every a)
filterGetOne HscEnv
s Q [Dec]
t a -> Bool
p IO (Every a) -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
filterGetOne  :: (Typeable a) => 
                 HscEnv            -- ^ session in which synthesized expressions are run
                 -> Q [Dec]        -- ^ target I/O pairs
                 -> (a -> Bool)    -- ^ test function
                 -> IO (Every a)
filterGetOne :: HscEnv -> Q [Dec] -> (a -> Bool) -> IO (Every a)
filterGetOne HscEnv
session Q [Dec]
tgt = HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
filterGetOneBK HscEnv
session Q [Dec]
tgt [d| {} |]
filterGetOneBK :: (Typeable a) => 
                  HscEnv           -- ^ session in which synthesized expressions are run
                  -> Q [Dec]       -- ^ target I/O pairs
                  -> Q [Dec]       -- ^ I/O pairs for background knowledge functions
                  -> (a -> Bool)   -- ^ test function
                  -> IO (Every a)
filterGetOneBK :: HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
filterGetOneBK HscEnv
session Q [Dec]
tgt Q [Dec]
bk a -> Bool
predicate = do Every a
tss <- HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
synthFilt HscEnv
session Q [Dec]
tgt Q [Dec]
bk a -> Bool
predicate
                                             FilePath -> IO ()
putStrLn (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ Exp -> FilePath
forall a. Ppr a => a -> FilePath
pprint (Exp -> FilePath) -> Exp -> FilePath
forall a b. (a -> b) -> a -> b
$ (Exp, a) -> Exp
forall a b. (a, b) -> a
fst ((Exp, a) -> Exp) -> (Exp, a) -> Exp
forall a b. (a -> b) -> a -> b
$ [(Exp, a)] -> (Exp, a)
forall a. [a] -> a
head ([(Exp, a)] -> (Exp, a)) -> [(Exp, a)] -> (Exp, a)
forall a b. (a -> b) -> a -> b
$ Every a -> [(Exp, a)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat Every a
tss
                                             Every a -> IO (Every a)
forall (m :: * -> *) a. Monad m => a -> m a
return Every a
tss

synthFilt  :: (Typeable a) => 
              HscEnv            -- ^ session in which synthesized expressions are run
              -> Q [Dec]        -- ^ target I/O pairs
              -> Q [Dec]        -- ^ I/O pairs for background knowledge functions
              -> (a -> Bool)    -- ^ test function
              -> IO (Every a)
synthFilt :: HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
synthFilt  HscEnv
session Q [Dec]
tgt Q [Dec]
bk a -> Bool
pred = (a -> Bool) -> Every a -> IO (Every a)
forall a. Typeable a => (a -> Bool) -> Every a -> IO (Every a)
filterThen  a -> Bool
pred (Every a -> IO (Every a)) -> IO (Every a) -> IO (Every a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HscEnv -> Q [Dec] -> Q [Dec] -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> Q [Dec] -> Q [Dec] -> IO (Every a)
synthAll HscEnv
session Q [Dec]
tgt Q [Dec]
bk
synthFiltF :: (Filtrable a, Typeable a) => 
              HscEnv             -- ^ session in which synthesized expressions are run
              -> Q [Dec]         -- ^ target I/O pairs
              -> Q [Dec]         -- ^ I/O pairs for background knowledge functions
              -> (a -> Bool)     -- ^ test function
              -> IO (Every a)
synthFiltF :: HscEnv -> Q [Dec] -> Q [Dec] -> (a -> Bool) -> IO (Every a)
synthFiltF HscEnv
session Q [Dec]
tgt Q [Dec]
bk a -> Bool
pred = (a -> Bool) -> Every a -> IO (Every a)
forall a.
(Typeable a, Filtrable a) =>
(a -> Bool) -> Every a -> IO (Every a)
filterThenF a -> Bool
pred (Every a -> IO (Every a)) -> IO (Every a) -> IO (Every a)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HscEnv -> Q [Dec] -> Q [Dec] -> IO (Every a)
forall a.
Typeable a =>
HscEnv -> Q [Dec] -> Q [Dec] -> IO (Every a)
synthAll HscEnv
session Q [Dec]
tgt Q [Dec]
bk
synthAll :: (Typeable a) => 
            HscEnv              -- ^ session in which synthesized expressions are run
            -> Q [Dec]          -- ^ target I/O pairs
            -> Q [Dec]          -- ^ I/O pairs for background knowledge functions
            -> IO (Every a)
synthAll :: HscEnv -> Q [Dec] -> Q [Dec] -> IO (Every a)
synthAll  HscEnv
session Q [Dec]
tgt Q [Dec]
bk = do [Dec]
tgtdecs <- Q [Dec] -> IO [Dec]
forall (m :: * -> *) a. Quasi m => Q a -> m a
runQ Q [Dec]
tgt
                              [Dec]
bkdecs  <- Q [Dec] -> IO [Dec]
forall (m :: * -> *) a. Quasi m => Q a -> m a
runQ Q [Dec]
bk
                              HscEnv -> [[Exp]] -> IO (Every a)
forall a. HscEnv -> [[Exp]] -> IO (Every a)
thExpssToEvery HscEnv
session ([Dec] -> [Dec] -> [[Exp]]
synthTyped [Dec]
tgtdecs [Dec]
bkdecs)
thExpssToEvery :: HscEnv -> [[Exp]] -> IO (Every a)
thExpssToEvery :: HscEnv -> [[Exp]] -> IO (Every a)
thExpssToEvery HscEnv
session [[Exp]]
ess = Every a -> IO (Every a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Every a -> IO (Every a)) -> Every a -> IO (Every a)
forall a b. (a -> b) -> a -> b
$ ([Exp] -> [(Exp, a)]) -> [[Exp]] -> Every a
forall a b. (a -> b) -> [a] -> [b]
map ((Exp -> (Exp, a)) -> [Exp] -> [(Exp, a)]
forall a b. (a -> b) -> [a] -> [b]
map (\Exp
e -> (Exp
e, IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ HscEnv -> Exp -> IO a
forall a. HscEnv -> Exp -> IO a
executeTHExp HscEnv
session Exp
e))) [[Exp]]
ess
-- thExpssToEvery session ess = mapM (mapM (\e -> fmap ((,) e) $ executeTHExp session e)) ess -- これだとダメ. unsafeInterleaveIOをうまく使う手もあるのかも．