-- 
-- (C) Susumu Katayama
--
-- test with ghci -XTemplateHaskell -cpp -DCHTO MagicHaskeller/Analytical.hs
-- Was: monolithic MagicHaskeller.TypedIOPairs
{-# LANGUAGE TemplateHaskell, CPP #-}
module MagicHaskeller.Analytical(
  -- * Analytical synthesizer
  -- | This module provides with analytical synthesis, that only generates expressions without testing.
  --   (So this alone may not be very useful, and for this reason this is not very well-documented.)
  --   In order to generate-and-test over the result of this module, use "MagicHaskeller.RunAnalytical".
  
  -- ** Synthesizers which can be used with any types. 
     get1, getMany, getManyM, getManyTyped, noBK, c, SplicedPrims,
  -- ** Synthesizers which are easier to use that can be used only with types appearing 'MagicHaskeller.CoreLang.defaultPrimitives'
     getOne, synth, synthM, synthTyped
                                ) where

import Data.Char(ord,chr)
import Data.Array
import qualified Data.Map as Map
import Data.Generics
import Language.Haskell.TH

import Control.Monad.Search.Combinatorial
import Control.Monad.Search.Best
import MagicHaskeller.TyConLib
import MagicHaskeller.CoreLang hiding (C)
import MagicHaskeller.PriorSubsts
import MagicHaskeller.ReadTHType(typeToTHType)
import MagicHaskeller.MHTH(decsToExpDecs)

import MagicHaskeller(p1, tup)

import MagicHaskeller.Analytical.Synthesize
#ifdef DEBUG
import MagicHaskeller.Analytical.Debug
#endif


type Strategy = Matrix

type SplicedPrims = ([Dec],[Primitive])

-- | get1 can be used to synthesize one expression. For example,
--
-- >>> putStrLn $ pprint $ get1 $(c [d| f [] = 0; f [a] = 1; f [a,b] = 2 |]) noBK
-- > \a -> let fa (b@([])) = 0
-- >           fa (b@(_ : d)) = succ (fa d)
-- >       in fa a
get1 :: SplicedPrims    -- ^ target function definition by example
        -> SplicedPrims -- ^ background knowledge function definitions by example
        -> Exp
-- get1 target bk = head $ getBests $ getManyM target bk -- This uses Control.Monad.Search.Best. 
get1 :: SplicedPrims -> SplicedPrims -> Exp
get1 SplicedPrims
target SplicedPrims
bk = [Exp] -> Exp
forall a. [a] -> a
head ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ [[Exp]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Exp]] -> [Exp]) -> [[Exp]] -> [Exp]
forall a b. (a -> b) -> a -> b
$ SplicedPrims -> SplicedPrims -> [[Exp]]
getMany SplicedPrims
target SplicedPrims
bk
-- | getMany does what you expect from its name.
getMany :: SplicedPrims    -- ^ target function definition by example
        -> SplicedPrims -- ^ background knowledge function definitions by example
        -> [[Exp]]
getMany :: SplicedPrims -> SplicedPrims -> [[Exp]]
getMany SplicedPrims
tgt SplicedPrims
bk = Matrix Exp -> [[Exp]]
forall a. Matrix a -> Stream (Bag a)
unMx (Matrix Exp -> [[Exp]]) -> Matrix Exp -> [[Exp]]
forall a b. (a -> b) -> a -> b
$ Matrix Exp -> Matrix Exp
forall (m :: * -> *) a. Search m => m a -> Matrix a
toMx (SplicedPrims -> SplicedPrims -> Matrix Exp
forall (m :: * -> *).
Search m =>
SplicedPrims -> SplicedPrims -> m Exp
getManyM SplicedPrims
tgt SplicedPrims
bk :: Strategy Exp)
getManyM :: (Search m) =>
            SplicedPrims -- ^ target function definition by example
         -> SplicedPrims -- ^ background knowledge function definitions by example
         -> m Exp
getManyM :: SplicedPrims -> SplicedPrims -> m Exp
getManyM ([Dec]
tgt,[Primitive]
pt) ([Dec]
bk,[Primitive]
pb) = let ps :: [Primitive]
ps  = [Primitive]
pt[Primitive] -> [Primitive] -> [Primitive]
forall a. [a] -> [a] -> [a]
++[Primitive]
pb
                                tcl :: TyConLib
tcl = [Primitive] -> TyConLib
primitivesToTCL [Primitive]
ps
                                vl :: VarLib
vl  = TyConLib -> [Primitive] -> VarLib
primitivesToVL  TyConLib
tcl [Primitive]
ps
                            in (CoreExpr -> Exp) -> m CoreExpr -> m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VarLib -> CoreExpr -> Exp
exprToTHExp VarLib
vl) (TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
forall (m :: * -> *).
Search m =>
TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
analyticSynth TyConLib
tcl VarLib
vl [Dec]
tgt [Dec]
bk)
-- | getManyTyped is a variant of 'getMany' that generates typed expressions.
--   This alone is not very useful, but the type info is required when compiling the expression and is used in "MagicHaskeller.RunAnalytical".
getManyTyped :: SplicedPrims    -- ^ target function definition by example
                -> SplicedPrims -- ^ background knowledge function definitions by example
                -> [[Exp]]
getManyTyped :: SplicedPrims -> SplicedPrims -> [[Exp]]
getManyTyped ([Dec]
tgt,[Primitive]
pt) ([Dec]
bk,[Primitive]
pb) 
  = let ps :: [Primitive]
ps  = [Primitive]
pt[Primitive] -> [Primitive] -> [Primitive]
forall a. [a] -> [a] -> [a]
++[Primitive]
pb
        tcl :: TyConLib
tcl = [Primitive] -> TyConLib
primitivesToTCL [Primitive]
ps
        vl :: VarLib
vl  = TyConLib -> [Primitive] -> VarLib
primitivesToVL  TyConLib
tcl [Primitive]
ps
        (Matrix CoreExpr
unit, Type
ty) = TyConLib -> VarLib -> [Dec] -> [Dec] -> (Matrix CoreExpr, Type)
forall (m :: * -> *).
Search m =>
TyConLib -> VarLib -> [Dec] -> [Dec] -> (m CoreExpr, Type)
analyticSynthAndInfType TyConLib
tcl VarLib
vl [Dec]
tgt [Dec]
bk
        addSignature :: Exp -> Exp
addSignature Exp
thexp = Exp -> Type -> Exp
SigE Exp
thexp (Type -> Exp) -> Type -> Exp
forall a b. (a -> b) -> a -> b
$ TyConLib -> Type -> Type
typeToTHType TyConLib
tcl Type
ty
    in ([CoreExpr] -> [Exp]) -> [[CoreExpr]] -> [[Exp]]
forall a b. (a -> b) -> [a] -> [b]
map ((CoreExpr -> Exp) -> [CoreExpr] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Exp -> Exp
addSignature (Exp -> Exp) -> (CoreExpr -> Exp) -> CoreExpr -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarLib -> CoreExpr -> Exp
exprToTHExpLite VarLib
vl)) ([[CoreExpr]] -> [[Exp]]) -> [[CoreExpr]] -> [[Exp]]
forall a b. (a -> b) -> a -> b
$ Matrix CoreExpr -> [[CoreExpr]]
forall a. Matrix a -> Stream (Bag a)
unMx (Matrix CoreExpr -> [[CoreExpr]])
-> Matrix CoreExpr -> [[CoreExpr]]
forall a b. (a -> b) -> a -> b
$ Matrix CoreExpr -> Matrix CoreExpr
forall (m :: * -> *) a. Search m => m a -> Matrix a
toMx (Matrix CoreExpr
unit :: Strategy CoreExpr)

noBK :: SplicedPrims
noBK :: SplicedPrims
noBK = ([],[])

c :: Q [Dec] -> ExpQ
-- ^ Also, @ $(c [d| ... |]) :: SplicedPrims @
--   'c' is a helper function for extracting some info from the quoted declarations.
c :: Q [Dec] -> ExpQ
c Q [Dec]
decq = do [Dec]
decs <- Q [Dec]
decq
            Exp
expdecs  <- [Dec] -> ExpQ
decsToExpDecs [Dec]
decs
            Exp
expPrims <- ([Exp] -> Exp) -> Q [Exp] -> ExpQ
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Exp] -> Exp
ListE (Q [Exp] -> ExpQ) -> Q [Exp] -> ExpQ
forall a b. (a -> b) -> a -> b
$ (Exp -> ExpQ) -> [Exp] -> Q [Exp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Exp -> ExpQ
p1 ([Exp] -> Q [Exp]) -> [Exp] -> Q [Exp]
forall a b. (a -> b) -> a -> b
$ [Dec] -> [Exp]
forall a. (Data a, Typeable a) => a -> [Exp]
cons [Dec]
decs
            Exp -> ExpQ
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> ExpQ) -> Exp -> ExpQ
forall a b. (a -> b) -> a -> b
$ [Exp] -> Exp
tup [Exp
expdecs, Exp
expPrims]

cons, conEs, conPs :: (Data a, Typeable a) => a -> [Exp]
cons :: a -> [Exp]
cons a
a = a -> [Exp]
forall a. (Data a, Typeable a) => a -> [Exp]
conEs a
a [Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
++ a -> [Exp]
forall a. (Data a, Typeable a) => a -> [Exp]
conPs a
a
conEs :: a -> [Exp]
conEs = ([Exp] -> [Exp] -> [Exp]) -> GenericQ [Exp] -> GenericQ [Exp]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
(++) ([Exp] -> (Exp -> [Exp]) -> a -> [Exp]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [] (\Exp
x -> [ Exp
e | e :: Exp
e@(ConE Name
_)   <- [Exp
x]]))
conPs :: a -> [Exp]
conPs = ([Exp] -> [Exp] -> [Exp]) -> GenericQ [Exp] -> GenericQ [Exp]
forall r. (r -> r -> r) -> GenericQ r -> GenericQ r
everything [Exp] -> [Exp] -> [Exp]
forall a. [a] -> [a] -> [a]
(++) ([Exp] -> (Pat -> [Exp]) -> a -> [Exp]
forall a b r. (Typeable a, Typeable b) => r -> (b -> r) -> a -> r
mkQ [] (\Pat
x -> [ Name -> Exp
ConE Name
name | (ConP Name
name [Pat]
_) <- [Pat
x]]))


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

getOne :: [Dec] -> [Dec] -> Exp
-- ^ Example:
--
-- >>> runQ [d| f [] = 0; f [a] = 1; f [a,b] = 2 |] >>= \iops -> putStrLn $ pprint $ getOne iops []
-- > \a -> let fa (b@([])) = 0
-- >           fa (b@(_ : d)) = succ (fa d)
-- >       in fa a
getOne :: [Dec] -> [Dec] -> Exp
getOne [Dec]
iops [Dec]
bk = [Exp] -> Exp
forall a. [a] -> a
head ([Exp] -> Exp) -> [Exp] -> Exp
forall a b. (a -> b) -> a -> b
$ [[Exp]] -> [Exp]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Exp]] -> [Exp]) -> [[Exp]] -> [Exp]
forall a b. (a -> b) -> a -> b
$ [Dec] -> [Dec] -> [[Exp]]
synth [Dec]
iops [Dec]
bk
-- getOne iops bk = head $ getBests $ synthM iops bk -- This uses Control.Monad.Search.Best. 
synth :: [Dec] -> [Dec] -> [[Exp]]
synth :: [Dec] -> [Dec] -> [[Exp]]
synth  [Dec]
iops [Dec]
bk = Matrix Exp -> [[Exp]]
forall a. Matrix a -> Stream (Bag a)
unMx (Matrix Exp -> [[Exp]]) -> Matrix Exp -> [[Exp]]
forall a b. (a -> b) -> a -> b
$ Matrix Exp -> Matrix Exp
forall (m :: * -> *) a. Search m => m a -> Matrix a
toMx ([Dec] -> [Dec] -> Matrix Exp
forall (m :: * -> *). Search m => [Dec] -> [Dec] -> m Exp
synthM [Dec]
iops [Dec]
bk :: Strategy Exp)
synthM :: Search m => [Dec] -> [Dec] -> m Exp
synthM :: [Dec] -> [Dec] -> m Exp
synthM [Dec]
iops [Dec]
bk = (CoreExpr -> Exp) -> m CoreExpr -> m Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VarLib -> CoreExpr -> Exp
exprToTHExp VarLib
defaultVarLib) (TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
forall (m :: * -> *).
Search m =>
TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
analyticSynth TyConLib
defaultTCL VarLib
defaultVarLib [Dec]
iops [Dec]
bk)

-- | 'synthTyped' is like synth, but adds the infered type signature to each expression. This is useful for executing the expression at runtime using GHC API.
synthTyped :: [Dec] -> [Dec] -> [[Exp]]
synthTyped :: [Dec] -> [Dec] -> [[Exp]]
synthTyped [Dec]
iops [Dec]
bk
    = let (Matrix CoreExpr
unit, Type
ty) = TyConLib -> VarLib -> [Dec] -> [Dec] -> (Matrix CoreExpr, Type)
forall (m :: * -> *).
Search m =>
TyConLib -> VarLib -> [Dec] -> [Dec] -> (m CoreExpr, Type)
analyticSynthAndInfType TyConLib
defaultTCL VarLib
defaultVarLib [Dec]
iops [Dec]
bk
          addSignature :: Exp -> Exp
addSignature Exp
thexp = Exp -> Type -> Exp
SigE Exp
thexp (Type -> Exp) -> Type -> Exp
forall a b. (a -> b) -> a -> b
$ TyConLib -> Type -> Type
typeToTHType TyConLib
defaultTCL Type
ty
      in ([CoreExpr] -> [Exp]) -> [[CoreExpr]] -> [[Exp]]
forall a b. (a -> b) -> [a] -> [b]
map ((CoreExpr -> Exp) -> [CoreExpr] -> [Exp]
forall a b. (a -> b) -> [a] -> [b]
map (Exp -> Exp
addSignature (Exp -> Exp) -> (CoreExpr -> Exp) -> CoreExpr -> Exp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarLib -> CoreExpr -> Exp
exprToTHExpLite VarLib
defaultVarLib)) ([[CoreExpr]] -> [[Exp]]) -> [[CoreExpr]] -> [[Exp]]
forall a b. (a -> b) -> a -> b
$ Matrix CoreExpr -> [[CoreExpr]]
forall a. Matrix a -> Stream (Bag a)
unMx (Matrix CoreExpr -> [[CoreExpr]])
-> Matrix CoreExpr -> [[CoreExpr]]
forall a b. (a -> b) -> a -> b
$ Matrix CoreExpr -> Matrix CoreExpr
forall (m :: * -> *) a. Search m => m a -> Matrix a
toMx (Matrix CoreExpr
unit :: Strategy CoreExpr)
synthesize :: [Dec] -> [Dec] -> [[String]]
synthesize :: [Dec] -> [Dec] -> [[String]]
synthesize [Dec]
iops [Dec]
bk
    = ([Exp] -> [String]) -> [[Exp]] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map ((Exp -> String) -> [Exp] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Exp -> String
forall a. Ppr a => a -> String
pprint) ([[Exp]] -> [[String]]) -> [[Exp]] -> [[String]]
forall a b. (a -> b) -> a -> b
$ [Dec] -> [Dec] -> [[Exp]]
synth [Dec]
iops [Dec]
bk