-- 
-- (C) Susumu Katayama
--
{-# LANGUAGE CPP #-}
module MagicHaskeller.Analytical.Synthesize where

import Data.List(transpose, genericLength, genericTake)
-- import Control.Monad.Search.RecompDL -- a version using DList, but did not actually improve the efficiency.
import Control.Monad -- hiding (guard)
import Control.Monad.State -- hiding (guard)
import qualified Data.IntMap as IntMap

import Language.Haskell.TH

import Control.Monad.Search.Combinatorial
import MagicHaskeller.CoreLang hiding (C)
import qualified MagicHaskeller.Types as Types
import MagicHaskeller.TyConLib
import MagicHaskeller.PriorSubsts hiding (unify)

import MagicHaskeller.Analytical.Syntax
import MagicHaskeller.Analytical.Parser
import MagicHaskeller.Analytical.UniT
import MagicHaskeller.Analytical.FMExpr

import Data.Int
import Data.Word

-- | function specification by examples.
data Fun a = BKF {Fun a -> Int
maxNumBVs :: Int, Fun a -> Int
arity :: Int, Fun a -> [IOPair a]
iopairs :: [IOPair a], Fun a -> FMExpr [IOPair a]
fmexpr :: FMExpr [IOPair a]} -- ^ the function is really a background knowledge (and thus there is no need for loop check)     
           | Rec {maxNumBVs :: Int, arity :: Int, iopairs :: [IOPair a], fmexpr :: FMExpr [IOPair a], Fun a -> TBS
toBeSought :: TBS} -- ^ it is actually a recursive call.
mkBKFun :: [IOPair a] -> Fun a
mkBKFun          iops :: [IOPair a]
iops@(IOPair a
iop:[IOPair a]
_) = BKF :: forall a. Int -> Int -> [IOPair a] -> FMExpr [IOPair a] -> Fun a
BKF {maxNumBVs :: Int
maxNumBVs = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (IOPair a -> Int) -> [IOPair a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> Int
forall a. IOPair a -> Int
numUniIDs [IOPair a]
iops, arity :: Int
arity = [Expr a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr a] -> Int) -> [Expr a] -> Int
forall a b. (a -> b) -> a -> b
$ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
iop, iopairs :: [IOPair a]
iopairs = [IOPair a]
iops, fmexpr :: FMExpr [IOPair a]
fmexpr = [IOPair a] -> FMExpr [IOPair a]
forall a. [IOPair a] -> FMExpr [IOPair a]
iopsToFME [IOPair a]
iops}
mkRecFun :: Int -> TBS -> [IOPair a] -> Fun a
mkRecFun Int
ari TBS
tbs iops :: [IOPair a]
iops@(IOPair a
iop:[IOPair a]
_) = Rec :: forall a.
Int -> Int -> [IOPair a] -> FMExpr [IOPair a] -> TBS -> Fun a
Rec {maxNumBVs :: Int
maxNumBVs = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ (IOPair a -> Int) -> [IOPair a] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> Int
forall a. IOPair a -> Int
numUniIDs [IOPair a]
iops, arity :: Int
arity = Int
ari, iopairs :: [IOPair a]
iopairs = [IOPair a]
iops, fmexpr :: FMExpr [IOPair a]
fmexpr = TBS -> [IOPair a] -> FMExpr [IOPair a]
forall a. TBS -> [IOPair a] -> FMExpr [IOPair a]
iopsToVisFME TBS
tbs [IOPair a]
iops, toBeSought :: TBS
toBeSought = TBS
tbs} -- arity = filter id tbs, but it is usually know beforehand
mkInitRecFun :: [IOPair a] -> Fun a
mkInitRecFun     iops :: [IOPair a]
iops@(IOPair a
iop:[IOPair a]
_) = let aritar :: Int
aritar = [Expr a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr a] -> Int) -> [Expr a] -> Int
forall a b. (a -> b) -> a -> b
$ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
iop in Int -> TBS -> [IOPair a] -> Fun a
forall a. Int -> TBS -> [IOPair a] -> Fun a
mkRecFun Int
aritar (Int -> Bool -> TBS
forall a. Int -> a -> [a]
replicate Int
aritar Bool
True) [IOPair a]
iops
setIOPairs :: [IOPair a] -> Fun a -> Fun a
setIOPairs [IOPair a]
iops recfun :: Fun a
recfun@Rec{toBeSought :: forall a. Fun a -> TBS
toBeSought=TBS
tbs} = Fun a
recfun{iopairs :: [IOPair a]
iopairs = [IOPair a]
iops, fmexpr :: FMExpr [IOPair a]
fmexpr = TBS -> [IOPair a] -> FMExpr [IOPair a]
forall a. TBS -> [IOPair a] -> FMExpr [IOPair a]
iopsToVisFME TBS
tbs [IOPair a]
iops}
type BK a = [Types.Typed (Fun a)]      -- ^ background knowledge.

applyFun :: [(Int, Expr a)] -> Fun a -> Fun a
applyFun [(Int, Expr a)]
s Fun a
fun = Fun a
fun{iopairs :: [IOPair a]
iopairs = [(Int, Expr a)] -> [IOPair a] -> [IOPair a]
forall a. [(Int, Expr a)] -> [IOPair a] -> [IOPair a]
applyIOPs [(Int, Expr a)]
s (Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
fun)}


analyticSynth :: Search m => TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
analyticSynth :: TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
analyticSynth TyConLib
tcl VarLib
vl [Dec]
target [Dec]
bkdec = (m CoreExpr, Type) -> m CoreExpr
forall a b. (a, b) -> a
fst ((m CoreExpr, Type) -> m CoreExpr)
-> (m CoreExpr, Type) -> m CoreExpr
forall a b. (a -> b) -> a -> b
$ TyConLib -> VarLib -> [Dec] -> [Dec] -> (m CoreExpr, Type)
forall (m :: * -> *).
Search m =>
TyConLib -> VarLib -> [Dec] -> [Dec] -> (m CoreExpr, Type)
analyticSynthAndInfType TyConLib
tcl VarLib
vl [Dec]
target [Dec]
bkdec
analyticSynthAndInfType :: Search m => TyConLib -> VarLib -> [Dec] -> [Dec] -> (m CoreExpr, Types.Type)
analyticSynthAndInfType :: TyConLib -> VarLib -> [Dec] -> [Dec] -> (m CoreExpr, Type)
analyticSynthAndInfType TyConLib
tcl VarLib
vl [Dec]
target [Dec]
bkdec
    = case PriorSubsts
  Maybe
  ([(Name, Typed [IOPair Type])], [(Name, Typed [IOPair Type])])
-> Subst
-> TyVar
-> Maybe
     (([(Name, Typed [IOPair Type])], [(Name, Typed [IOPair Type])]),
      Subst, TyVar)
forall (m :: * -> *) a.
PriorSubsts m a -> Subst -> TyVar -> m (a, Subst, TyVar)
unPS (([(Name, Typed [IOPair Type])]
 -> [(Name, Typed [IOPair Type])]
 -> ([(Name, Typed [IOPair Type])], [(Name, Typed [IOPair Type])]))
-> PriorSubsts Maybe [(Name, Typed [IOPair Type])]
-> PriorSubsts Maybe [(Name, Typed [IOPair Type])]
-> PriorSubsts
     Maybe
     ([(Name, Typed [IOPair Type])], [(Name, Typed [IOPair Type])])
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (,) (TyConLib
-> XVarLib
-> [Dec]
-> PriorSubsts Maybe [(Name, Typed [IOPair Type])]
forall (m :: * -> *).
(Functor m, MonadPlus m) =>
TyConLib
-> XVarLib -> [Dec] -> PriorSubsts m [(Name, Typed [IOPair Type])]
parseTypedIOPairss TyConLib
tcl XVarLib
xvl [Dec]
target) (TyConLib
-> XVarLib
-> [Dec]
-> PriorSubsts Maybe [(Name, Typed [IOPair Type])]
forall (m :: * -> *).
(Functor m, MonadPlus m) =>
TyConLib
-> XVarLib -> [Dec] -> PriorSubsts m [(Name, Typed [IOPair Type])]
parseTypedIOPairss TyConLib
tcl XVarLib
xvl [Dec]
bkdec)) Subst
forall a. [a]
Types.emptySubst TyVar
0 of
        Maybe
  (([(Name, Typed [IOPair Type])], [(Name, Typed [IOPair Type])]),
   Subst, TyVar)
Nothing -> [Char] -> (m CoreExpr, Type)
forall a. HasCallStack => [Char] -> a
error [Char]
"Type error occurred while reading the IO pairs."
        Just (([],[(Name, Typed [IOPair Type])]
_),Subst
_,TyVar
_) ->[Char] -> (m CoreExpr, Type)
forall a. HasCallStack => [Char] -> a
error [Char]
"MagicHaskeller.Synthesize.analyticSynth*: No I/O pairs are defined as the target."
        Just (([(Name
targetFunName, iops :: [IOPair Type]
iops@(IOPair Type
iop:[IOPair Type]
_) Types.:::Type
ty)],[(Name, Typed [IOPair Type])]
bktups),Subst
_,TyVar
mx) ->
               let ([Name]
bknames, [Typed [IOPair Type]]
bktiopss) = [(Name, Typed [IOPair Type])] -> ([Name], [Typed [IOPair Type]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(Name, Typed [IOPair Type])]
bktups
                   ([[IOPair Type]]
bkiopss, [Type]
bktypes)  = [Typed [IOPair Type]] -> ([[IOPair Type]], [Type])
forall a. [Typed a] -> ([a], [Type])
unzipTyped [Typed [IOPair Type]]
bktiopss
                   target :: Fun Type
target = Int -> TBS -> [IOPair Type] -> Fun Type
forall a. Int -> TBS -> [IOPair a] -> Fun a
mkRecFun Int
aritar TBS
tbs [IOPair Type]
iops
                   tbs :: TBS
tbs = Int -> Bool -> TBS
forall a. Int -> a -> [a]
replicate Int
aritar Bool
True                   
                   aritar :: Int
aritar = [Expr Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Expr Type] -> Int) -> [Expr Type] -> Int
forall a b. (a -> b) -> a -> b
$ IOPair Type -> [Expr Type]
forall a. IOPair a -> [Expr a]
inputs IOPair Type
iop
                   aritar8 :: TyVar
aritar8 = Int -> TyVar
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
aritar
                   bk :: [Typed (Fun Type)]
bk = [Typed (Fun Type)] -> [Typed (Fun Type)]
forall a. [a] -> [a]
reverse ([Typed (Fun Type)] -> [Typed (Fun Type)])
-> [Typed (Fun Type)] -> [Typed (Fun Type)]
forall a b. (a -> b) -> a -> b
$ (Fun Type -> Type -> Typed (Fun Type))
-> [Fun Type] -> [Type] -> [Typed (Fun Type)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Fun Type -> Type -> Typed (Fun Type)
forall a. a -> Type -> Typed a
(Types.:::) (([IOPair Type] -> Fun Type) -> [[IOPair Type]] -> [Fun Type]
forall a b. (a -> b) -> [a] -> [b]
map [IOPair Type] -> Fun Type
forall a. [IOPair a] -> Fun a
mkBKFun ([[IOPair Type]] -> [Fun Type]) -> [[IOPair Type]] -> [Fun Type]
forall a b. (a -> b) -> a -> b
$ [[IOPair Type]]
bkiopss) [Type]
bktypes
               in ((CoreExpr -> CoreExpr) -> m CoreExpr -> m CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\CoreExpr
e -> Int -> (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall i a. Integral i => i -> (a -> a) -> a -> a
napply ([(Name, Typed [IOPair Type])] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Name, Typed [IOPair Type])]
bktups) CoreExpr -> CoreExpr
FunLambda (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall a b. (a -> b) -> a -> b
$ Int -> (CoreExpr -> CoreExpr) -> CoreExpr -> CoreExpr
forall i a. Integral i => i -> (a -> a) -> a -> a
napply Int
aritar CoreExpr -> CoreExpr
Lambda (CoreExpr -> TyVar -> [TyVar] -> CoreExpr
Fix CoreExpr
e TyVar
aritar8 [TyVar
aritar8TyVar -> TyVar -> TyVar
forall a. Num a => a -> a -> a
-TyVar
1, TyVar
aritar8TyVar -> TyVar -> TyVar
forall a. Num a => a -> a -> a
-TyVar
2..TyVar
0])) (m CoreExpr -> m CoreExpr) -> m CoreExpr -> m CoreExpr
forall a b. (a -> b) -> a -> b
$   --  $ Fix e $ map X [arity-1, arity-2 .. 0]) $     -- 本当はこの結果のそれぞれに bknamesを適用したいのだが，bknamesなHValueがないので.... てゆーか，Expなら作れる．CoreExprも，BKが全部VarLibにはいっていれば作れる．
                   [Typed (Fun Type)] -> Typed (Fun Type) -> m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> m CoreExpr
fastAnalSynthNoUniT [Typed (Fun Type)]
bk (Fun Type
target Fun Type -> Type -> Typed (Fun Type)
forall a. a -> Type -> Typed a
Types.::: Type
ty)
                  ,(Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
(Types.:->) Type
ty [Type]
bktypes)
        Maybe
  (([(Name, Typed [IOPair Type])], [(Name, Typed [IOPair Type])]),
   Subst, TyVar)
_ -> [Char] -> (m CoreExpr, Type)
forall a. HasCallStack => [Char] -> a
error [Char]
"MagicHaskeller.Synthesize.analyticSynth*: More than one I/O pairs are defined as the target."
    where xvl :: XVarLib
xvl = VarLib -> XVarLib
mkXVarLib VarLib
vl


fastAnalSynthNoUniT :: BK a -> Typed (Fun a) -> m CoreExpr
fastAnalSynthNoUniT BK a
bk tfun :: Typed (Fun a)
tfun@(Fun a
fun Types.::: Type
_) | (Expr a -> Bool) -> [Expr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr a -> Bool
forall a. Expr a -> Bool
hasExistential ([Expr a] -> Bool) -> [Expr a] -> Bool
forall a b. (a -> b) -> a -> b
$ (IOPair a -> Expr a) -> [IOPair a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> Expr a
forall a. IOPair a -> Expr a
output ([IOPair a] -> [Expr a]) -> [IOPair a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
fun = BK a -> Typed (Fun a) -> m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> m CoreExpr
analSynthNoUniT BK a
bk Typed (Fun a)
tfun
                                              | Bool
otherwise                                  = BK a -> Typed (Fun a) -> m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> m CoreExpr
fastAnalSynthmNoUniT BK a
bk Typed (Fun a)
tfun

--fastAnalSynthNoUniT = fastAnalSynthmNoUniT
fastAnalSynthmNoUniT :: [Typed (Fun a)] -> Typed (Fun a) -> m CoreExpr
fastAnalSynthmNoUniT [Typed (Fun a)]
bk Typed (Fun a)
tfun
    = m CoreExpr
others m CoreExpr -> m CoreExpr -> m CoreExpr
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` m CoreExpr -> m CoreExpr
forall (m :: * -> *) a. Delay m => m a -> m a
delay m CoreExpr
bkRelated
  where newbk :: [Typed (Fun a)]
newbk = Typed (Fun a)
tfun Typed (Fun a) -> [Typed (Fun a)] -> [Typed (Fun a)]
forall a. a -> [a] -> [a]
: [Typed (Fun a)]
bk
        bkRelated :: m CoreExpr
bkRelated = ([Typed (Fun a)] -> Typed (Fun a) -> m CoreExpr)
-> ([Typed (Fun a)]
    -> Typed (Fun a)
    -> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar))
-> [Typed (Fun a)]
-> Typed (Fun a)
-> m CoreExpr
forall (m :: * -> *) (t :: * -> *) t a t b.
(Monad m, Traversable t) =>
(t -> Typed (Fun a) -> m CoreExpr)
-> (t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar))
-> t
-> t
-> m b
headSpine [Typed (Fun a)] -> Typed (Fun a) -> m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> m CoreExpr
analSynthNoUniT [Typed (Fun a)]
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar)
forall (m :: * -> *) a. Search m => Introducer a m
introBKm [Typed (Fun a)]
newbk Typed (Fun a)
tfun 
        others :: m CoreExpr
others    = ([Typed (Fun a)] -> Typed (Fun a) -> m CoreExpr)
-> ([Typed (Fun a)]
    -> Typed (Fun a)
    -> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar))
-> [Typed (Fun a)]
-> Typed (Fun a)
-> m CoreExpr
forall (m :: * -> *) (t :: * -> *) t a t b.
(Monad m, Traversable t) =>
(t -> Typed (Fun a) -> m CoreExpr)
-> (t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar))
-> t
-> t
-> m b
headSpine [Typed (Fun a)] -> Typed (Fun a) -> m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> m CoreExpr
fastAnalSynthNoUniT ([Typed (Fun a)]
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introConstr ([Typed (Fun a)]
 -> Typed (Fun a)
 -> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar))
-> ([Typed (Fun a)]
    -> Typed (Fun a)
    -> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar))
-> [Typed (Fun a)]
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar)
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ [Typed (Fun a)]
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introVarm ([Typed (Fun a)]
 -> Typed (Fun a)
 -> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar))
-> ([Typed (Fun a)]
    -> Typed (Fun a)
    -> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar))
-> [Typed (Fun a)]
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar)
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ Int
-> ([Typed (Fun a)]
    -> Typed (Fun a)
    -> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar))
-> [Typed (Fun a)]
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar)
forall (m :: * -> *) t t a.
Delay m =>
Int -> (t -> t -> m a) -> t -> t -> m a
ndelayIntro Int
2 [Typed (Fun a)]
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, [Typed (Fun a)], Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introCase) [Typed (Fun a)]
newbk Typed (Fun a)
tfun

analSynthNoUniT :: BK a -> Typed (Fun a) -> m CoreExpr
analSynthNoUniT BK a
bk Typed (Fun a)
tfun
  = (BK a -> Typed (Fun a) -> m CoreExpr)
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m CoreExpr
forall (m :: * -> *) (t :: * -> *) t a t b.
(Monad m, Traversable t) =>
(t -> Typed (Fun a) -> m CoreExpr)
-> (t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar))
-> t
-> t
-> m b
headSpine BK a -> Typed (Fun a) -> m CoreExpr
analSynthNoUniT (BK a
-> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introConstr (BK a
 -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ BK a
-> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introVarm' (BK a
 -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ Int
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) t t a.
Delay m =>
Int -> (t -> t -> m a) -> t -> t -> m a
ndelayIntro Int
2 BK a
-> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introCase (BK a
 -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ Int
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) t t a.
Delay m =>
Int -> (t -> t -> m a) -> t -> t -> m a
ndelayIntro Int
1 BK a
-> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. Search m => Introducer a m
introBKm) (Typed (Fun a)
tfunTyped (Fun a) -> BK a -> BK a
forall a. a -> [a] -> [a]
:BK a
bk) Typed (Fun a)
tfun

{-
The following definition of analSynth should work even if 
- existential variables are included in BK or in Fun, e.g. a function binding 
  f a = b
  is included
  or
- the same variable name appear multiple times in the LHS (input examples) of an I/O example in BK or in Fun, E.g. a function binding
  f a a = 1
  is included.
Those bindings are not valid Haskell, nor accepted by Template Haskell, so a library like haskell-src has to be used for parsing them.
-}
analSynth, analSynthm, fastAnalSynthNoUniT :: Search m => BK a -> Types.Typed (Fun a) -> m CoreExpr
analSynth :: BK a -> Typed (Fun a) -> m CoreExpr
analSynth BK a
bk tfun :: Typed (Fun a)
tfun@(Fun a
fun Types.::: Type
_) | (Expr a -> Bool) -> [Expr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Expr a -> Bool
forall a. Expr a -> Bool
hasExistential ([Expr a] -> Bool) -> [Expr a] -> Bool
forall a b. (a -> b) -> a -> b
$ (IOPair a -> Expr a) -> [IOPair a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> Expr a
forall a. IOPair a -> Expr a
output ([IOPair a] -> [Expr a]) -> [IOPair a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
fun = ((CoreExpr, St a) -> CoreExpr) -> m (CoreExpr, St a) -> m CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (CoreExpr, St a) -> CoreExpr
forall a b. (a, b) -> a
fst (m (CoreExpr, St a) -> m CoreExpr)
-> m (CoreExpr, St a) -> m CoreExpr
forall a b. (a -> b) -> a -> b
$ StateT (St a) m CoreExpr -> St a -> m (CoreExpr, St a)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (BK a -> Typed (Fun a) -> StateT (St a) m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> UniT a m CoreExpr
analSynthUTm BK a
bk Typed (Fun a)
tfun) St a
forall a. St a
emptySt
                                    | Bool
otherwise                                  = BK a -> Typed (Fun a) -> m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> m CoreExpr
analSynthm BK a
bk Typed (Fun a)
tfun
analSynthm :: BK a -> Typed (Fun a) -> m CoreExpr
analSynthm BK a
bk Typed (Fun a)
tfun
    = m CoreExpr
others m CoreExpr -> m CoreExpr -> m CoreExpr
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` m CoreExpr -> m CoreExpr
forall (m :: * -> *) a. Delay m => m a -> m a
delay m CoreExpr
bkRelated
  where newbk :: BK a
newbk = Typed (Fun a)
tfun Typed (Fun a) -> BK a -> BK a
forall a. a -> [a] -> [a]
: BK a
bk
        bkRelated :: m CoreExpr
bkRelated = (BK a -> Typed (Fun a) -> m CoreExpr)
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m CoreExpr
forall (m :: * -> *) (t :: * -> *) t a t b.
(Monad m, Traversable t) =>
(t -> Typed (Fun a) -> m CoreExpr)
-> (t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar))
-> t
-> t
-> m b
headSpine BK a -> Typed (Fun a) -> m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> m CoreExpr
analSynth BK a
-> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. Search m => Introducer a m
introBKm BK a
newbk Typed (Fun a)
tfun 
        others :: m CoreExpr
others    = (BK a -> Typed (Fun a) -> m CoreExpr)
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m CoreExpr
forall (m :: * -> *) (t :: * -> *) t a t b.
(Monad m, Traversable t) =>
(t -> Typed (Fun a) -> m CoreExpr)
-> (t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar))
-> t
-> t
-> m b
headSpine BK a -> Typed (Fun a) -> m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> m CoreExpr
analSynthm (BK a
-> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introConstr (BK a
 -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ BK a
-> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introVarm (BK a
 -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ Int
-> (BK a
    -> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) t t a.
Delay m =>
Int -> (t -> t -> m a) -> t -> t -> m a
ndelayIntro Int
2 BK a
-> Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introCase) BK a
newbk Typed (Fun a)
tfun
headSpine :: (t -> Typed (Fun a) -> m CoreExpr)
-> (t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar))
-> t
-> t
-> m b
headSpine t -> Typed (Fun a) -> m CoreExpr
rec t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar)
intro t
bk t
tfun 
  = do (t CoreExpr -> b
hd, t (Typed (Fun a))
subfuns, Maybe TyVar
mbpivot) <- t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar)
intro t
bk t
tfun
       t CoreExpr
subexps <- (Typed (Fun a) -> m CoreExpr)
-> t (Typed (Fun a)) -> m (t CoreExpr)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Typed (Fun a)
subfun -> let arisub :: TyVar
arisub = Int -> TyVar
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> TyVar) -> Int -> TyVar
forall a b. (a -> b) -> a -> b
$ Fun a -> Int
forall a. Fun a -> Int
arity (Fun a -> Int) -> Fun a -> Int
forall a b. (a -> b) -> a -> b
$ Typed (Fun a) -> Fun a
forall a. Typed a -> a
Types.typee Typed (Fun a)
subfun :: Int8 in (CoreExpr -> CoreExpr) -> m CoreExpr -> m CoreExpr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\CoreExpr
e -> CoreExpr -> TyVar -> [TyVar] -> CoreExpr
Fix CoreExpr
e TyVar
arisub (Maybe TyVar -> TyVar -> [TyVar]
forall a. Integral a => Maybe a -> a -> [a]
mkArgs Maybe TyVar
mbpivot TyVar
arisub)) (m CoreExpr -> m CoreExpr) -> m CoreExpr -> m CoreExpr
forall a b. (a -> b) -> a -> b
$ t -> Typed (Fun a) -> m CoreExpr
rec t
bk Typed (Fun a)
subfun)  t (Typed (Fun a))
subfuns
       b -> m b
forall (m :: * -> *) a. Monad m => a -> m a
return (t CoreExpr -> b
hd t CoreExpr
subexps)
#ifdef DEBUG
headSpine_debug rec trs intro bk tfun 
  = do (hd, subfuns, mbpivot) <- intro bk tfun
       subexps <- zipWithM (\tr subfun -> let arisub = fromIntegral $ arity $ Types.typee subfun in fmap (\e -> Fix e arisub (mkArgs mbpivot arisub)) $ rec tr bk subfun) trs subfuns
       return (hd subexps)
#endif

analSynthUTm :: Search m => BK a -> Types.Typed (Fun a) -> UniT a m CoreExpr
-- analSynthm ([], _, _) = mzero -- If there is no example, nothing can be done. (But is this line necessary?)
analSynthUTm :: BK a -> Typed (Fun a) -> UniT a m CoreExpr
analSynthUTm BK a
bk (Fun a
fun Types.::: Type
ty)
    = do 
         Subst a
s <- (St a -> Subst a) -> StateT (St a) m (Subst a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St a -> Subst a
forall a. St a -> Subst a
subst
         let aptfun :: Typed (Fun a)
aptfun = Subst a -> Fun a -> Fun a
forall a. [(Int, Expr a)] -> Fun a -> Fun a
applyFun Subst a
s Fun a
fun Fun a -> Type -> Typed (Fun a)
forall a. a -> Type -> Typed a
Types.::: Type
ty
             newbk :: BK a
newbk  = Typed (Fun a)
aptfun Typed (Fun a) -> BK a -> BK a
forall a. a -> [a] -> [a]
: BK a
bk
         (BK a -> Typed (Fun a) -> UniT a m CoreExpr)
-> (BK a
    -> Typed (Fun a)
    -> StateT (St a) m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> BK a
-> Typed (Fun a)
-> UniT a m CoreExpr
forall (m :: * -> *) (t :: * -> *) t a t b.
(Monad m, Traversable t) =>
(t -> Typed (Fun a) -> m CoreExpr)
-> (t -> t -> m (t CoreExpr -> b, t (Typed (Fun a)), Maybe TyVar))
-> t
-> t
-> m b
headSpine BK a -> Typed (Fun a) -> UniT a m CoreExpr
forall (m :: * -> *) a.
Search m =>
BK a -> Typed (Fun a) -> UniT a m CoreExpr
analSynthUTm BK a
-> Typed (Fun a)
-> StateT (St a) m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. Search m => IntroUniT a m
introAny BK a
newbk Typed (Fun a)
aptfun

mkArgs :: Maybe a -> a -> [a]
mkArgs Maybe a
Nothing a
arisub = [a
arisuba -> a -> a
forall a. Num a => a -> a -> a
-a
1,a
arisuba -> a -> a
forall a. Num a => a -> a -> a
-a
2..a
0]
mkArgs (Just a
pivot) a
arisub = a -> [a] -> [a]
forall i a. Integral i => i -> [a] -> [a]
genericTake a
pivot [a
arisub,a
arisuba -> a -> a
forall a. Num a => a -> a -> a
-a
1..] [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a
arisuba -> a -> a
forall a. Num a => a -> a -> a
-a
pivota -> a -> a
forall a. Num a => a -> a -> a
-a
1,a
arisuba -> a -> a
forall a. Num a => a -> a -> a
-a
pivota -> a -> a
forall a. Num a => a -> a -> a
-a
2..a
0]

#ifdef DEBUG
analyticSynthNoUniT_debug :: Search m => Tree (Introducer a m) ->  TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
analyticSynthNoUniT_debug tree tcl vl target bkdec
    = case unPS (liftM2 (,) (parseTypedIOPairss tcl xvl target) (parseTypedIOPairss tcl xvl bkdec)) Types.emptySubst 0 of
        Nothing -> error "Type error occurred while reading the IO pairs."
        Just (([],_),_,_) ->error "TypedIOPairs.analyticSynth*: No I/O pairs are defined as the target."
        Just (([(targetFunName, iops@(iop:_) Types.:::ty)],bktups),_,mx) ->
               let (bknames, bktiopss) = unzip bktups
                   (bkiopss, bktypes)  = unzipTyped bktiopss
                   target = mkRecFun aritar tbs iops
                   tbs = replicate aritar True                   
                   aritar = length $ inputs iop
                   bk = reverse $ zipWith (Types.:::) (map mkBKFun $ bkiopss) bktypes
               in (fmap (\e -> napply (length bktups) FunLambda $ napply aritar Lambda (Fix e aritar [aritar-1, aritar-2..0])) $   --  $ Fix e $ map X [arity-1, arity-2 .. 0]) $     -- 本当はこの結果のそれぞれに bknamesを適用したいのだが，bknamesなHValueがないので.... てゆーか，Expなら作れる．CoreExprも，BKが全部VarLibにはいっていれば作れる．
                   analSynthNoUniT_debug tree bk (target Types.:::ty)
                  )
        _ -> error "TypedIOPairs.analyticSynth*: More than one I/O pairs are defined as the target."
    where xvl = mkXVarLib vl
analSynthNoUniT_debug (Br intro trs) bk tfun
  = headSpine_debug analSynthNoUniT_debug trs intro (tfun:bk) tfun


data Tree x = Br x [Tree x] deriving Show
tryall, tryVar :: Search m => Tree (IntroUniT a m)
tryall = Br introAny (repeat tryall)
tryVar = Br introVarUTm []
tryVarm :: (Functor m, MonadPlus m) => Tree (Introducer a m)
tryVarm = Br introVarm []

analyticSynth_debug :: Search m => Tree (IntroUniT a m) -> TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
analyticSynth_debug tree tcl vl target bkdec
    = do ((tgt,bktups),_,mx) <-
             unPS (liftM2 (,) (parseTypedIOPairss tcl xvl target) (parseTypedIOPairss tcl xvl bkdec)) Types.emptySubst 0
         case tgt of
           [] -> error "analyticSynth: No I/O pairs are defined as the target."
           [(targetFunName, iops@(iop:_) Types.:::ty)] ->
               let (bknames, bktiopss) = unzip bktups
                   (bkiopss, bktypes)  = unzipTyped bktiopss
                   target = mkRecFun aritar tbs iops
                   tbs = replicate aritar True
                   aritar = length $ inputs iop
                   bk = reverse $ zipWith (Types.:::) (map mkBKFun $ bkiopss) bktypes
               in fmap (\(e,_st) -> napply (length bktups) FunLambda $ napply aritar Lambda (Fix e aritar [aritar-1, aritar-2..0])) $   --  $ Fix e $ map X [arity-1, arity-2 .. 0]) $     -- 本当はこの結果のそれぞれに bknamesを適用したいのだが，bknamesなHValueがないので.... てゆーか，Expなら作れる．CoreExprも，BKが全部VarLibにはいっていれば作れる．
                        runStateT (analSynthUT_debug tree bk (target Types.::: ty)) emptySt -- ONLY DIFFER HERE.
           _ -> error "analyticSynth: More than one I/O pairs are defined as the target."
    where xvl = mkXVarLib vl

-- | 'analSynthUT_debug' can be used to try only the given introducer at each selection point. @analSynthUT = analSynthUT_debug tryall@
analSynthUT_debug :: Search m => Tree (IntroUniT a m) -> BK a -> Types.Typed (Fun a) -> UniT a m CoreExpr
analSynthUT_debug (Br intro iss) bk (fun Types.::: ty)
    = do
         s <- gets subst
         let aptfun = applyFun s fun Types.::: ty
             newbk   = aptfun : bk
         (hd, subfuns, mbpivot) <- intro newbk aptfun
         subexps <- zipWithM (\is subfun -> let arisub = arity $ Types.typee subfun in fmap (\e -> Fix e arisub (mkArgs mbpivot arisub)) $ analSynthUT_debug is newbk subfun) iss subfuns
         return (hd subexps)
#endif

type Introducer a m = BK a -> Types.Typed (Fun a) -> m ([CoreExpr] -> CoreExpr, [Types.Typed (Fun a)], Maybe Int8)
type IntroUniT  a m = Introducer a (UniT a m)
-- NB: We should not use @StateT Env@ where @Env=(BK a,TBS)@ because the Env affects only subexpressions.

t -> t -> m a
il +++ :: (t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ t -> t -> m a
ir = \t
bk t
iops -> t -> t -> m a
il t
bk t
iops m a -> m a -> m a
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` t -> t -> m a
ir t
bk t
iops
ndelayIntro :: Int -> (t -> t -> m a) -> t -> t -> m a
ndelayIntro Int
n t -> t -> m a
intro = \t
e t
a -> Int -> m a -> m a
forall (m :: * -> *) a. Delay m => Int -> m a -> m a
ndelay Int
n (m a -> m a) -> m a -> m a
forall a b. (a -> b) -> a -> b
$ t -> t -> m a
intro t
e t
a

introAny :: Search m => IntroUniT a m
introAny :: IntroUniT a m
introAny     =          IntroUniT a m
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introConstr IntroUniT a m -> IntroUniT a m -> IntroUniT a m
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++ {- +/ -} (
                        IntroUniT a m
forall (m :: * -> *) a. MonadPlus m => IntroUniT a m
introVarUTm IntroUniT a m -> IntroUniT a m -> IntroUniT a m
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++
                        Int -> IntroUniT a m -> IntroUniT a m
forall (m :: * -> *) t t a.
Delay m =>
Int -> (t -> t -> m a) -> t -> t -> m a
ndelayIntro Int
1 IntroUniT a m
forall (m :: * -> *) a. MonadPlus m => IntroUniT a m
introBKUTm IntroUniT a m -> IntroUniT a m -> IntroUniT a m
forall (m :: * -> *) t t a.
MonadPlus m =>
(t -> t -> m a) -> (t -> t -> m a) -> t -> t -> m a
+++
                        Int -> IntroUniT a m -> IntroUniT a m
forall (m :: * -> *) t t a.
Delay m =>
Int -> (t -> t -> m a) -> t -> t -> m a
ndelayIntro Int
2 IntroUniT a m
forall (m :: * -> *) a. (Functor m, MonadPlus m) => Introducer a m
introCase )

(+/) :: MonadPlus m => IntroUniT a [] -> IntroUniT a m -> IntroUniT a m
IntroUniT a []
m +/ :: IntroUniT a [] -> IntroUniT a m -> IntroUniT a m
+/ IntroUniT a m
n = \BK a
bk Typed (Fun a)
iops ->
         do St a
st <- StateT (St a) m (St a)
forall s (m :: * -> *). MonadState s m => m s
get
       	    case StateT (St a) [] ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> St a -> [(([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)]
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (IntroUniT a []
m BK a
bk Typed (Fun a)
iops) St a
st of [] -> IntroUniT a m
n BK a
bk Typed (Fun a)
iops
                                             [(([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)]
ts -> (St a -> m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a))
-> UniT a m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT ((St a -> m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a))
 -> UniT a m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> (St a -> m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a))
-> UniT a m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ \St a
_ -> [m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)]
-> m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)]
 -> m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a))
-> [m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)]
-> m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)
forall a b. (a -> b) -> a -> b
$ ((([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)
 -> m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a))
-> [(([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)]
-> [m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)]
forall a b. (a -> b) -> [a] -> [b]
map (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)
-> m (([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)
forall (m :: * -> *) a. Monad m => a -> m a
return [(([CoreExpr] -> CoreExpr, BK a, Maybe TyVar), St a)]
ts
liftList :: MonadPlus m => StateT s [] a -> StateT s m a
liftList :: StateT s [] a -> StateT s m a
liftList = ([(a, s)] -> m (a, s)) -> StateT s [] a -> StateT s m a
forall (m :: * -> *) a s (n :: * -> *) b.
(m (a, s) -> n (b, s)) -> StateT s m a -> StateT s n b
mapStateT ([m (a, s)] -> m (a, s)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m (a, s)] -> m (a, s))
-> ([(a, s)] -> [m (a, s)]) -> [(a, s)] -> m (a, s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, s) -> m (a, s)) -> [(a, s)] -> [m (a, s)]
forall a b. (a -> b) -> [a] -> [b]
map (a, s) -> m (a, s)
forall (m :: * -> *) a. Monad m => a -> m a
return)

introVarm, introVarm', introConstr, introCase :: (Functor m, MonadPlus m) => Introducer a m -- introConstrでは，実際にはCoreExprはConstrでよい．
introBKm :: (Search m) => Introducer a m -- introConstrでは，実際にはCoreExprはConstrでよい．
introVarUTm, introBKUTm :: MonadPlus m => IntroUniT a m
-- introVarUTmは一連のIgor関係の論文にはないものの，introBKが有効に働くには必要．これがないと，fを作るのにBKとしてfを使っても，introBKだけで終わってくれず，生成されない．
{- introBKのあとのintroVarUTmをintroBKに含めようとして，やっぱ止めた．
introVarUTm (iops,_,_,True) = mzero
introVarUTm (iops,_,_,False)  = msum $ map (\(ix,_) -> return (const (X ix), [])) $ filter (\(_,inp) -> inp == map output iops) $ zip [0..] $ transpose $ map inputs iops
-}
-- introVarUTm (iops,_,_,_)  = msum $ map (\(ix,_) -> return (const (X ix), [])) $ filter (\(_,inp) -> inp == map output iops) $ zip [0..] $ transpose $ map inputs iops
introVarUTm :: IntroUniT a m
introVarUTm BK a
b Typed (Fun a)
f = StateT (St a) [] ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> StateT (St a) m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) s a.
MonadPlus m =>
StateT s [] a -> StateT s m a
liftList (StateT (St a) [] ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
 -> StateT (St a) m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> StateT (St a) [] ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> StateT (St a) m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ ([Expr a] -> [Expr a] -> StateT (St a) [] ())
-> Introducer a (StateT (St a) [])
forall (m :: * -> *) a.
MonadPlus m =>
([Expr a] -> [Expr a] -> m ()) -> Introducer a m
introVar ((Expr a -> Expr a -> StateT (St a) [] ())
-> [Expr a] -> [Expr a] -> StateT (St a) [] ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Expr a -> Expr a -> StateT (St a) [] ()
forall (m :: * -> *) a.
MonadPlus m =>
Expr a -> Expr a -> StateT (St a) m ()
appUnifyUT) BK a
b Typed (Fun a)
f
-- introVarm b f  = introVar (zipWithM_ unify) b f  *************************************** これはデバッグ時に有用なことも．
introVarm :: Introducer a m
introVarm   = ([Expr a] -> [Expr a] -> m ()) -> Introducer a m
forall (m :: * -> *) a.
MonadPlus m =>
([Expr a] -> [Expr a] -> m ()) -> Introducer a m
introVar (\[Expr a]
a [Expr a]
b -> Bool -> m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> m ()) -> Bool -> m ()
forall a b. (a -> b) -> a -> b
$ [Expr a]
a[Expr a] -> [Expr a] -> Bool
forall a. Eq a => a -> a -> Bool
==[Expr a]
b)

introVarm' :: Introducer a m
introVarm' = ([Expr a] -> [Expr a] -> m ()) -> Introducer a m
forall (m :: * -> *) a.
MonadPlus m =>
([Expr a] -> [Expr a] -> m ()) -> Introducer a m
introVar ((Expr a -> Expr a -> m [(Int, Expr a)])
-> [Expr a] -> [Expr a] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ Expr a -> Expr a -> m [(Int, Expr a)]
forall (m :: * -> *) a.
MonadPlus m =>
Expr a -> Expr a -> m [(Int, Expr a)]
unify)

introVar :: MonadPlus m => ([Expr a] -> [Expr a] -> m ()) -> Introducer a m
introVar :: ([Expr a] -> [Expr a] -> m ()) -> Introducer a m
introVar [Expr a] -> [Expr a] -> m ()
cmp BK a
_ (Fun a
fun Types.::: Type
ty)
               = do let ([Type]
argtys, Type
retty) = Type -> ([Type], Type)
Types.splitArgs Type
ty
                        iops :: [IOPair a]
iops = Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
fun
                        arifun :: Int
arifun = Fun a -> Int
forall a. Fun a -> Int
arity Fun a
fun
                    let trins :: [[Expr a]]
trins = [[Expr a]] -> [[Expr a]]
forall a. [[a]] -> [[a]]
transpose ([[Expr a]] -> [[Expr a]]) -> [[Expr a]] -> [[Expr a]]
forall a b. (a -> b) -> a -> b
$ (IOPair a -> [Expr a]) -> [IOPair a] -> [[Expr a]]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs [IOPair a]
iops
--                    (ix,inps Types.::: argty) <- msum $ map return $ zip [0..] trins
                    (TyVar
ix,Type
argty,[Expr a]
inps) <- [m (TyVar, Type, [Expr a])] -> m (TyVar, Type, [Expr a])
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [ (TyVar, Type, [Expr a]) -> m (TyVar, Type, [Expr a])
forall (m :: * -> *) a. Monad m => a -> m a
return (TyVar, Type, [Expr a])
t | t :: (TyVar, Type, [Expr a])
t@(TyVar
_,Type
aty,[Expr a]
_) <- [TyVar] -> [Type] -> [[Expr a]] -> [(TyVar, Type, [Expr a])]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [TyVar
0..] [Type]
argtys ([[Expr a]] -> [(TyVar, Type, [Expr a])])
-> [[Expr a]] -> [(TyVar, Type, [Expr a])]
forall a b. (a -> b) -> a -> b
$ TBS -> [[Expr a]] -> [[Expr a]]
forall a. TBS -> [a] -> [a]
visibles (Fun a -> TBS
forall a. Fun a -> TBS
toBeSought Fun a
fun) [[Expr a]]
trins, Type -> Type -> Maybe Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
Types.mgu Type
aty Type
retty Maybe Subst -> Maybe Subst -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Subst
forall a. Maybe a
Nothing]

-- The following four lines should be equivalent to
                    [Expr a] -> [Expr a] -> m ()
cmp ((IOPair a -> Expr a) -> [IOPair a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> Expr a
forall a. IOPair a -> Expr a
output [IOPair a]
iops) [Expr a]
inps
-- but use of Maybe and simpler substitutions should be good for efficiency.
{-
                    st0 <- get
                    case runStateT (zipWithM_ appUnifyUT (map output iops) inps) st0{subst=[]} of
                              Just ((),st) -> put (st{subst= subst st `plusSubst` subst st0})
	  	     	      Nothing      -> mzero
-}
                    ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return (CoreExpr -> [CoreExpr] -> CoreExpr
forall a b. a -> b -> a
const (TyVar -> CoreExpr
X TyVar
ix), [], Maybe TyVar
forall a. Maybe a
Nothing)

introConstr :: Introducer a m
introConstr BK a
bk (Fun a
fun Types.::: Type
ty)
    = let argtys :: [Type]
argtys = Type -> [Type]
Types.getArgs Type
ty 
          iops :: [IOPair a]
iops   = Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
fun
      in
      case [ IOPair a -> Expr a
forall a. IOPair a -> Expr a
output IOPair a
iop | IOPair a
iop <- [IOPair a]
iops ] of
        outs :: [Expr a]
outs@(C a
_ Int
_ (Constr
cid Types.::: Type
cty) [Expr a]
flds : [Expr a]
rest)
            | (Expr a -> Bool) -> [Expr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Expr a -> Constr -> Bool
forall a. Expr a -> Constr -> Bool
`sConstrIs` Constr
cid) [Expr a]
rest -> ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. Monad m => a -> m a
return ((CoreExpr -> CoreExpr -> CoreExpr)
-> CoreExpr -> [CoreExpr] -> CoreExpr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoreExpr -> CoreExpr -> CoreExpr
(:$) (Constr -> CoreExpr
PrimCon Constr
cid),
                                                    ([IOPair a] -> Type -> Typed (Fun a))
-> [[IOPair a]] -> [Type] -> BK a
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\[IOPair a]
iops Type
retty -> [IOPair a] -> Fun a -> Fun a
forall a a. [IOPair a] -> Fun a -> Fun a
setIOPairs [IOPair a]
iops Fun a
fun Fun a -> Type -> Typed (Fun a)
forall a. a -> Type -> Typed a
Types.::: [Type] -> Type -> Type
Types.popArgs [Type]
argtys Type
retty)
                                                            ([[IOPair a]] -> [[IOPair a]]
forall a. [[a]] -> [[a]]
transpose [ IOPair a -> [IOPair a]
forall a. IOPair a -> [IOPair a]
divideIOP IOPair a
iop | IOPair a
iop <- [IOPair a]
iops ])
                                                            (case Type -> (Integer, [Type], Type)
forall i. Integral i => Type -> (i, [Type], Type)
Types.revSplitArgs Type
cty of (Integer
_,[Type]
fieldtys,Type
_) -> [Type]
fieldtys),
                                                    Maybe TyVar
forall a. Maybe a
Nothing)
        [Expr a]
_                        -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
divideIOP :: IOPair a -> [IOPair a]
divideIOP (IOP Int
bvs [Expr a]
ins Expr a
out) = (Expr a -> IOPair a) -> [Expr a] -> [IOPair a]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> [Expr a] -> Expr a -> IOPair a
forall a. Int -> [Expr a] -> Expr a -> IOPair a
IOP Int
bvs [Expr a]
ins) ([Expr a] -> [IOPair a]) -> [Expr a] -> [IOPair a]
forall a b. (a -> b) -> a -> b
$ Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
fields Expr a
out -- The actual number of buondVars may reduce, but not updating the field would not hurt.

shareConstr :: [Expr a] -> Bool
shareConstr (C a
_ Int
_ (Constr
cid Types.::: Type
_) [Expr a]
_ : [Expr a]
iops) = (Expr a -> Bool) -> [Expr a] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Expr a -> Constr -> Bool
forall a. Expr a -> Constr -> Bool
`sConstrIs` Constr
cid) [Expr a]
iops 
shareConstr [Expr a]
_                = Bool
False
-- typeが違うと同じcidを異なるconstructorで使い得る場合，typeごと比較する必要があるが，現在はそうではないので．
C a
_ Int
_ (Constr
c Types.::: Type
_) [Expr a]
_ sConstrIs :: Expr a -> Constr -> Bool
`sConstrIs` Constr
cid = Constr
cidConstr -> Constr -> Bool
forall a. Eq a => a -> a -> Bool
==Constr
c
Expr a
_                       `sConstrIs` Constr
cid = Bool
False


select :: TBS -> [a] -> [(a, TBS)]
select []     []      = []
select (Bool
b:TBS
bs) (a
p:[a]
ps) | Bool
b         = (a
p, Bool
FalseBool -> TBS -> TBS
forall a. a -> [a] -> [a]
:TBS
bs) (a, TBS) -> [(a, TBS)] -> [(a, TBS)]
forall a. a -> [a] -> [a]
: [(a, TBS)]
rest
                     | Bool
otherwise = [(a, TBS)]
rest
            where rest :: [(a, TBS)]
rest = [ (a
result, Bool
bBool -> TBS -> TBS
forall a. a -> [a] -> [a]
:TBS
newbs) | (a
result,TBS
newbs) <- TBS -> [a] -> [(a, TBS)]
select TBS
bs [a]
ps ]

introCase :: Introducer a m
introCase BK a
bk (Fun a
fun Types.::: Type
ty) = [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
 -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
-> [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
forall a. [a] -> [a]
reverse ([m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
 -> [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)])
-> [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
-> [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
forall a b. (a -> b) -> a -> b
$ (Int
 -> ([Expr a], TBS)
 -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> [Int]
-> [([Expr a], TBS)]
-> [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int
-> ([Expr a], TBS) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a.
(MonadPlus m, Num a) =>
Int -> ([Expr a], TBS) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe a)
introCase' [Int
0..] ([([Expr a], TBS)]
 -> [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)])
-> [([Expr a], TBS)]
-> [m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
forall a b. (a -> b) -> a -> b
$ TBS -> [[Expr a]] -> [([Expr a], TBS)]
forall a. TBS -> [a] -> [(a, TBS)]
select (Fun a -> TBS
forall a. Fun a -> TBS
toBeSought Fun a
fun) [[Expr a]]
trins
    where trins :: [[Expr a]]
trins = [[Expr a]] -> [[Expr a]]
forall a. [[a]] -> [[a]]
transpose ([[Expr a]] -> [[Expr a]]) -> [[Expr a]] -> [[Expr a]]
forall a b. (a -> b) -> a -> b
$ (IOPair a -> [Expr a]) -> [IOPair a] -> [[Expr a]]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs [IOPair a]
iops
          ([Type]
argtys,Type
retty) = Type -> ([Type], Type)
Types.splitArgs Type
ty
          iops :: [IOPair a]
iops   = Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
fun
          arifun :: Int
arifun = Fun a -> Int
forall a. Fun a -> Int
arity Fun a
fun
          {-
          introCase' :: MonadPlus m =>
                         Int              -- ^ the pivot position
                         -> ([Expr a],TBS)  -- ^ (the pivot expression for each I/O pair, the next TBS)
                         -> m ([CoreExpr] -> CoreExpr, [Types.Typed (Fun a)], Maybe Int)
          -}          
          introCase' :: Int -> ([Expr a], TBS) -> m ([CoreExpr] -> CoreExpr, BK a, Maybe a)
introCase' Int
pos ([Expr a]
pivots, TBS
tbs) -- includes variable cases. Overlapping patterns are not supported yet.
              = case (Expr a -> Maybe (Typed Constr))
-> [Expr a] -> Maybe [Typed Constr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Expr a -> Maybe (Typed Constr)
forall a. Expr a -> Maybe (Typed Constr)
maybeCtor [Expr a]
pivots of 
                  Maybe [Typed Constr]
Nothing -> m ([CoreExpr] -> CoreExpr, BK a, Maybe a)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                  Just [Typed Constr]
ctors
                      -> let
                             pipairs :: [(Expr a, IOPair a)]
pipairs = [Expr a] -> [IOPair a] -> [(Expr a, IOPair a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Expr a]
pivots [IOPair a]
iops -- :: [(Expr a, IOPair a)]
                             ts :: [(Int, (Type, [(Expr a, IOPair a)]))]
ts      = IntMap (Type, [(Expr a, IOPair a)])
-> [(Int, (Type, [(Expr a, IOPair a)]))]
forall a. IntMap a -> [(Int, a)]
IntMap.toList (IntMap (Type, [(Expr a, IOPair a)])
 -> [(Int, (Type, [(Expr a, IOPair a)]))])
-> IntMap (Type, [(Expr a, IOPair a)])
-> [(Int, (Type, [(Expr a, IOPair a)]))]
forall a b. (a -> b) -> a -> b
$ ((Type, [(Expr a, IOPair a)])
 -> (Type, [(Expr a, IOPair a)]) -> (Type, [(Expr a, IOPair a)]))
-> [(Int, (Type, [(Expr a, IOPair a)]))]
-> IntMap (Type, [(Expr a, IOPair a)])
forall a. (a -> a -> a) -> [(Int, a)] -> IntMap a
IntMap.fromListWith (\(Type
t,[(Expr a, IOPair a)]
xs) (Type
_,[(Expr a, IOPair a)]
ys) -> (Type
t,[(Expr a, IOPair a)]
xs[(Expr a, IOPair a)]
-> [(Expr a, IOPair a)] -> [(Expr a, IOPair a)]
forall a. [a] -> [a] -> [a]
++[(Expr a, IOPair a)]
ys)) ([(Int, (Type, [(Expr a, IOPair a)]))]
 -> IntMap (Type, [(Expr a, IOPair a)]))
-> [(Int, (Type, [(Expr a, IOPair a)]))]
-> IntMap (Type, [(Expr a, IOPair a)])
forall a b. (a -> b) -> a -> b
$
                                           (Typed Constr
 -> (Expr a, IOPair a) -> (Int, (Type, [(Expr a, IOPair a)])))
-> [Typed Constr]
-> [(Expr a, IOPair a)]
-> [(Int, (Type, [(Expr a, IOPair a)]))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Constr
c Types.::: Type
ct) (Expr a, IOPair a)
x -> (Constr -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Constr
c,(Type
ct,[(Expr a, IOPair a)
x]))) [Typed Constr]
ctors [(Expr a, IOPair a)]
pipairs
                                              -- :: [(Constr, (Types.Type, [(Expr a,IOPair a)]))]
                  -- Array.accum can also be used instead of IntMap because we can tell the range from that of VarLib.
                             hd :: [CoreExpr] -> CoreExpr
hd [CoreExpr]
ces = CoreExpr -> [(Constr, TyVar, CoreExpr)] -> CoreExpr
Case (TyVar -> CoreExpr
X (TyVar -> CoreExpr) -> TyVar -> CoreExpr
forall a b. (a -> b) -> a -> b
$ Int -> TyVar
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
pos)
                                            (((Int, (Type, [(Expr a, IOPair a)]))
 -> CoreExpr -> (Constr, TyVar, CoreExpr))
-> [(Int, (Type, [(Expr a, IOPair a)]))]
-> [CoreExpr]
-> [(Constr, TyVar, CoreExpr)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\(Int
constr, (Type
_, (Expr a
pivot,IOPair a
_):[(Expr a, IOPair a)]
_)) CoreExpr
ce -> (Int -> Constr
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
constr, [Expr a] -> TyVar
forall i a. Num i => [a] -> i
genericLength (Expr a -> [Expr a]
forall a. Expr a -> [Expr a]
fields Expr a
pivot), CoreExpr
ce))
                                                     [(Int, (Type, [(Expr a, IOPair a)]))]
ts
                                                     [CoreExpr]
ces)
                             iopss :: BK a
iopss  = [ Rec :: forall a.
Int -> Int -> [IOPair a] -> FMExpr [IOPair a] -> TBS -> Fun a
Rec { maxNumBVs :: Int
maxNumBVs  = Fun a -> Int
forall a. Fun a -> Int
maxNumBVs Fun a
fun, 
                                              arity :: Int
arity      = Int
arifunInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
lenflds,
                                              iopairs :: [IOPair a]
iopairs    = [IOPair a]
iops,
                                              fmexpr :: FMExpr [IOPair a]
fmexpr     = TBS -> [IOPair a] -> FMExpr [IOPair a]
forall a. TBS -> [IOPair a] -> FMExpr [IOPair a]
iopsToVisFME TBS
newtbs [IOPair a]
iops,
                                              toBeSought :: TBS
toBeSought = TBS
newtbs
                                            }
                                          Fun a -> Type -> Typed (Fun a)
forall a. a -> Type -> Typed a
Types.::: [Type] -> Type -> Type
Types.popArgs (Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
dropNth Int
pos [Type]
argtys) ([Type] -> Type -> Type
Types.popArgs (Type -> [Type]
Types.getArgs Type
cty) Type
retty)
                                      | (Int
_c, (Type
cty, nextpipairs :: [(Expr a, IOPair a)]
nextpipairs@((C a
_ Int
_ Typed Constr
_ [Expr a]
flds', IOPair a
_):[(Expr a, IOPair a)]
_))) <- [(Int, (Type, [(Expr a, IOPair a)]))]
ts,
                                        let lenflds :: Int
lenflds = [Expr a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Expr a]
flds'
                                            iops :: [IOPair a]
iops    = [ Int -> [Expr a] -> Expr a -> IOPair a
forall a. Int -> [Expr a] -> Expr a -> IOPair a
IOP Int
bvs ([Expr a] -> [Expr a]
forall a. [a] -> [a]
reverse [Expr a]
flds [Expr a] -> [Expr a] -> [Expr a]
forall a. [a] -> [a] -> [a]
++ [Expr a]
is) Expr a
o | (C a
_ Int
_ Typed Constr
_c [Expr a]
flds, IOP Int
bvs [Expr a]
is Expr a
o) <- [(Expr a, IOPair a)]
nextpipairs ]
                                            newtbs :: TBS
newtbs  = Int -> Bool -> TBS
forall a. Int -> a -> [a]
replicate Int
lenflds Bool
True TBS -> TBS -> TBS
forall a. [a] -> [a] -> [a]
++ TBS
tbs
                                      ]
                         in ([CoreExpr] -> CoreExpr, BK a, Maybe a)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([CoreExpr] -> CoreExpr
hd, BK a
iopss, a -> Maybe a
forall a. a -> Maybe a
Just (Int -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> a) -> Int -> a
forall a b. (a -> b) -> a -> b
$ Int
arifun Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
posInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1))

dropNth :: Int -> [a] -> [a]
dropNth Int
pos [a]
bs = case Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
pos [a]
bs of ([a]
tk,a
_:[a]
dr) -> [a]
tk [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
dr



introBKm :: Introducer a m
introBKm   BK a
bk Typed (Fun a)
tfun = Matrix ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. Search m => Matrix a -> m a
fromMx (Matrix ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
 -> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> Matrix ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ [([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
-> Matrix ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) a. Search m => m a -> Matrix a
toMx ([([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
 -> Matrix ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> [([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
-> Matrix ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ (Int -> [IOPair a] -> Fun a -> [[[IOPair a]]])
-> (Int -> TermStat -> Fun a -> Fun a -> [[[IOPair a]]])
-> BK a
-> Typed (Fun a)
-> [([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)]
forall (m :: * -> *) (t :: * -> *) a a a a.
(MonadPlus m, Foldable t) =>
(Int -> [IOPair a] -> Fun a -> m [[IOPair a]])
-> (Int -> TermStat -> Fun a -> Fun a -> m [[IOPair a]])
-> [Typed (Fun a)]
-> Typed (Fun a)
-> m (t CoreExpr -> CoreExpr, [Typed (Fun a)], Maybe a)
introBK Int -> [IOPair a] -> Fun a -> [[[IOPair a]]]
forall a. Int -> [IOPair a] -> Fun a -> [[[IOPair a]]]
subtractIOPairsFromIOPairsBKm Int -> TermStat -> Fun a -> Fun a -> [[[IOPair a]]]
forall a. Int -> TermStat -> Fun a -> Fun a -> [[[IOPair a]]]
subtractIOPairsFromIOPairsm BK a
bk Typed (Fun a)
tfun
introBKUTm :: IntroUniT a m
introBKUTm BK a
bk Typed (Fun a)
tfun = StateT (St a) [] ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> StateT (St a) m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) s a.
MonadPlus m =>
StateT s [] a -> StateT s m a
liftList (StateT (St a) [] ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
 -> StateT (St a) m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar))
-> StateT (St a) [] ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
-> StateT (St a) m ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall a b. (a -> b) -> a -> b
$ (Int -> [IOPair a] -> Fun a -> StateT (St a) [] [[IOPair a]])
-> (Int
    -> TermStat -> Fun a -> Fun a -> StateT (St a) [] [[IOPair a]])
-> BK a
-> Typed (Fun a)
-> StateT (St a) [] ([CoreExpr] -> CoreExpr, BK a, Maybe TyVar)
forall (m :: * -> *) (t :: * -> *) a a a a.
(MonadPlus m, Foldable t) =>
(Int -> [IOPair a] -> Fun a -> m [[IOPair a]])
-> (Int -> TermStat -> Fun a -> Fun a -> m [[IOPair a]])
-> [Typed (Fun a)]
-> Typed (Fun a)
-> m (t CoreExpr -> CoreExpr, [Typed (Fun a)], Maybe a)
introBK (([IOPair a] -> Fun a -> StateT (St a) [] [[IOPair a]])
-> Int -> [IOPair a] -> Fun a -> StateT (St a) [] [[IOPair a]]
forall a b. a -> b -> a
const [IOPair a] -> Fun a -> StateT (St a) [] [[IOPair a]]
forall (m :: * -> *) a.
MonadPlus m =>
[IOPair a] -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsBKUTm) ((TermStat -> Fun a -> Fun a -> StateT (St a) [] [[IOPair a]])
-> Int
-> TermStat
-> Fun a
-> Fun a
-> StateT (St a) [] [[IOPair a]]
forall a b. a -> b -> a
const TermStat -> Fun a -> Fun a -> StateT (St a) [] [[IOPair a]]
forall (m :: * -> *) a.
MonadPlus m =>
TermStat -> Fun a -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsUTm) BK a
bk Typed (Fun a)
tfun
introBK :: (Int -> [IOPair a] -> Fun a -> m [[IOPair a]])
-> (Int -> TermStat -> Fun a -> Fun a -> m [[IOPair a]])
-> [Typed (Fun a)]
-> Typed (Fun a)
-> m (t CoreExpr -> CoreExpr, [Typed (Fun a)], Maybe a)
introBK Int -> [IOPair a] -> Fun a -> m [[IOPair a]]
subBK Int -> TermStat -> Fun a -> Fun a -> m [[IOPair a]]
sub [Typed (Fun a)]
bk (Fun a
fun Types.:::Type
ty) = do          
                              let ([Type]
argtys, Type
retty) = Type -> ([Type], Type)
Types.splitArgs Type
ty
                              (TyVar
ix, Fun a
bkfun Types.::: Type
bkty) <- [m (TyVar, Typed (Fun a))] -> m (TyVar, Typed (Fun a))
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([m (TyVar, Typed (Fun a))] -> m (TyVar, Typed (Fun a)))
-> [m (TyVar, Typed (Fun a))] -> m (TyVar, Typed (Fun a))
forall a b. (a -> b) -> a -> b
$ ((TyVar, Typed (Fun a)) -> m (TyVar, Typed (Fun a)))
-> [(TyVar, Typed (Fun a))] -> [m (TyVar, Typed (Fun a))]
forall a b. (a -> b) -> [a] -> [b]
map (TyVar, Typed (Fun a)) -> m (TyVar, Typed (Fun a))
forall (m :: * -> *) a. Monad m => a -> m a
return ([(TyVar, Typed (Fun a))] -> [m (TyVar, Typed (Fun a))])
-> [(TyVar, Typed (Fun a))] -> [m (TyVar, Typed (Fun a))]
forall a b. (a -> b) -> a -> b
$ [(TyVar, Typed (Fun a))] -> [(TyVar, Typed (Fun a))]
forall a. [a] -> [a]
tail ([(TyVar, Typed (Fun a))] -> [(TyVar, Typed (Fun a))])
-> [(TyVar, Typed (Fun a))] -> [(TyVar, Typed (Fun a))]
forall a b. (a -> b) -> a -> b
$ [TyVar] -> [Typed (Fun a)] -> [(TyVar, Typed (Fun a))]
forall a b. [a] -> [b] -> [(a, b)]
zip [TyVar
0..] [Typed (Fun a)]
bk
                                              -- The tail function here is used to avoid generating expressions like
                                              -- fix (\fa x1 ... xn -> fa ...).
                                              -- Such expressions would be excluded by the loop checker even without the tail function, 
                                              -- but we exclude them beforehand for efficiency reasons.
                              let ([Type]
bkargtys, Type
bkretty) = Type -> ([Type], Type)
Types.splitArgs Type
bkty
                              Subst
substy <- Type -> Type -> m Subst
forall (m :: * -> *). MonadPlus m => Type -> Type -> m Subst
Types.match Type
bkretty Type
retty
                              [[IOPair a]]
iopss <- case Fun a
bkfun of BKF{maxNumBVs :: forall a. Fun a -> Int
maxNumBVs=Int
addendum} -> Int -> [IOPair a] -> Fun a -> m [[IOPair a]]
subBK (-Int
addendum) (Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
fun) Fun a
bkfun
                                                     Rec{maxNumBVs :: forall a. Fun a -> Int
maxNumBVs=Int
addendum} -> Int -> TermStat -> Fun a -> Fun a -> m [[IOPair a]]
sub (-Int
addendum) TermStat
initTS Fun a
fun Fun a
bkfun
                              (t CoreExpr -> CoreExpr, [Typed (Fun a)], Maybe a)
-> m (t CoreExpr -> CoreExpr, [Typed (Fun a)], Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return ((CoreExpr -> CoreExpr -> CoreExpr)
-> CoreExpr -> t CoreExpr -> CoreExpr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CoreExpr -> CoreExpr -> CoreExpr
(:$) (TyVar -> CoreExpr
FunX TyVar
ix),
                                      [ [IOPair a] -> Fun a -> Fun a
forall a a. [IOPair a] -> Fun a -> Fun a
setIOPairs [IOPair a]
iops Fun a
fun Fun a -> Type -> Typed (Fun a)
forall a. a -> Type -> Typed a
Types.::: Type
tys 
                                      | [IOPair a]
iops Types.::: Type
tys <- [Typed [IOPair a]] -> [Typed [IOPair a]]
forall a. [a] -> [a]
reverse ([Typed [IOPair a]] -> [Typed [IOPair a]])
-> [Typed [IOPair a]] -> [Typed [IOPair a]]
forall a b. (a -> b) -> a -> b
$ 
                                                              ([IOPair a] -> Type -> Typed [IOPair a])
-> [[IOPair a]] -> [Type] -> [Typed [IOPair a]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\[IOPair a]
x Type
retty -> [IOPair a]
x [IOPair a] -> Type -> Typed [IOPair a]
forall a. a -> Type -> Typed a
Types.::: [Type] -> Type -> Type
Types.popArgs [Type]
argtys Type
retty)
                                                                      ([[IOPair a]] -> [[IOPair a]]
forall a. [[a]] -> [[a]]
transpose [[IOPair a]]
iopss)
                                                                      ((Type -> Type) -> [Type] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Subst -> Type -> Type
Types.apply Subst
substy) [Type]
bkargtys) ],
                                      Maybe a
forall a. Maybe a
Nothing)



subtractIOPairsFromIOPairsBKUTm :: MonadPlus m => [IOPair a] -> (Fun a) -> UniT a m [[IOPair a]]
{-
subtractIOPairsFromIOPairsBK funs bks = foldr (liftM2 (:)) (return []) $ map (flip subtractIOPairs bks) funs
-}
subtractIOPairsFromIOPairsBKUTm :: [IOPair a] -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsBKUTm []         Fun a
bkf = [[IOPair a]] -> UniT a m [[IOPair a]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
subtractIOPairsFromIOPairsBKUTm (IOPair a
fun:[IOPair a]
funs) Fun a
bkf = do 
                                                 [IOPair a]
iops <- IOPair a -> Fun a -> UniT a m [IOPair a]
forall (m :: * -> *) a.
MonadPlus m =>
IOPair a -> Fun a -> UniT a m [IOPair a]
subtractIOPairsBKUTm IOPair a
fun Fun a
bkf
                                                 [[IOPair a]]
iopss <- [IOPair a] -> Fun a -> UniT a m [[IOPair a]]
forall (m :: * -> *) a.
MonadPlus m =>
[IOPair a] -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsBKUTm [IOPair a]
funs Fun a
bkf -- iopsは，subfunctionが複数あって，それらsubfunctionsのそれぞれに関してIOPair1個ずつに過ぎない．
                                                 [[IOPair a]] -> UniT a m [[IOPair a]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([IOPair a]
iops[IOPair a] -> [[IOPair a]] -> [[IOPair a]]
forall a. a -> [a] -> [a]
:[[IOPair a]]
iopss)
-- Applying substitutions to funs is not currently necessary (because funs does not include existential variables), but that will be useful in future versions which fill gaps of input examples.

{-
subtractIOPairs :: IOPair -> [IOPair] -> [[IOPair]] -- 内側リストの基数はfunのarity, 外側はbkのIO pairのうちmatchするのはいくつあるか
                                                    -- てゆーか，内側はbkのarityでは？
subtractIOPairs fun bkpairs = [ iops | bk <- bkpairs, iops <- subtractIOPair fun bk ]
-}
subtractIOPairsBKUTm :: MonadPlus m => IOPair a -> (Fun a) -> UniT a m [IOPair a] -- 内側リストの基数はfunのarity, 外側はbkのIO pairのうちmatchするのはいくつあるか
                                                    -- てゆーか，内側はbkのarityでは？
subtractIOPairsBKUTm :: IOPair a -> Fun a -> UniT a m [IOPair a]
subtractIOPairsBKUTm IOPair a
tgt Fun a
bkf = do 
                               Subst a
s <- (St a -> Subst a) -> StateT (St a) m (Subst a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St a -> Subst a
forall a. St a -> Subst a
subst
                               let aptgt :: IOPair a
aptgt = Subst a -> IOPair a -> IOPair a
forall a. [(Int, Expr a)] -> IOPair a -> IOPair a
applyIOP  Subst a
s IOPair a
tgt
                                   apbkf :: [IOPair a]
apbkf = Subst a -> [IOPair a] -> [IOPair a]
forall a. [(Int, Expr a)] -> [IOPair a] -> [IOPair a]
applyIOPs Subst a
s ([IOPair a] -> [IOPair a]) -> [IOPair a] -> [IOPair a]
forall a b. (a -> b) -> a -> b
$ Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
bkf
                               IOPair a
bkiop <- [StateT (St a) m (IOPair a)] -> StateT (St a) m (IOPair a)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([StateT (St a) m (IOPair a)] -> StateT (St a) m (IOPair a))
-> [StateT (St a) m (IOPair a)] -> StateT (St a) m (IOPair a)
forall a b. (a -> b) -> a -> b
$ (IOPair a -> StateT (St a) m (IOPair a))
-> [IOPair a] -> [StateT (St a) m (IOPair a)]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> StateT (St a) m (IOPair a)
forall (m :: * -> *) a. Monad m => a -> m a
return [IOPair a]
apbkf
                               IOPair a -> IOPair a -> UniT a m [IOPair a]
forall (m :: * -> *) a.
MonadPlus m =>
IOPair a -> IOPair a -> UniT a m [IOPair a]
subtractIOPairUTm IOPair a
aptgt IOPair a
bkiop
subtractIOPairsFromIOPairsUTm :: MonadPlus m => TermStat -> Fun a -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsUTm :: TermStat -> Fun a -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsUTm TermStat
ts Fun a
tgt Fun a
bkf = TermStat -> [IOPair a] -> Fun a -> UniT a m [[IOPair a]]
forall (m :: * -> *) a.
MonadPlus m =>
TermStat -> [IOPair a] -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsUTm' TermStat
ts (Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
tgt) Fun a
bkf
subtractIOPairsFromIOPairsUTm' :: MonadPlus m => TermStat -> [IOPair a] -> Fun a -> UniT a m [[IOPair a]]
{-
subtractIOPairsFromIOPairs funs bks = foldr (\fun rest -> do iops <- subtractIOPairs fun bks
                                                             iopss <- rest
                                                             return (iops:iopss)) (return []) funs
-}
subtractIOPairsFromIOPairsUTm' :: TermStat -> [IOPair a] -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsUTm' TermStat
ts []         Fun a
bkf = [[IOPair a]] -> UniT a m [[IOPair a]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
subtractIOPairsFromIOPairsUTm' TermStat
ts (IOPair a
fun:[IOPair a]
funs) Fun a
bkf = do
                                ([IOPair a]
iops,TermStat
newts) <- TermStat -> IOPair a -> Fun a -> UniT a m ([IOPair a], TermStat)
forall (m :: * -> *) a.
MonadPlus m =>
TermStat -> IOPair a -> Fun a -> UniT a m ([IOPair a], TermStat)
subtractIOPairsUTm TermStat
ts IOPair a
fun Fun a
bkf
                                [[IOPair a]]
iopss        <- TermStat -> [IOPair a] -> Fun a -> UniT a m [[IOPair a]]
forall (m :: * -> *) a.
MonadPlus m =>
TermStat -> [IOPair a] -> Fun a -> UniT a m [[IOPair a]]
subtractIOPairsFromIOPairsUTm' TermStat
newts [IOPair a]
funs Fun a
bkf -- iopsは，subfunctionが複数あって，それらsubfunctionsのそれぞれに関してIOPair1個ずつに過ぎない．
                                [[IOPair a]] -> UniT a m [[IOPair a]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([IOPair a]
iops[IOPair a] -> [[IOPair a]] -> [[IOPair a]]
forall a. a -> [a] -> [a]
:[[IOPair a]]
iopss)
subtractIOPairsUTm :: MonadPlus m => TermStat -> IOPair a -> (Fun a) -> UniT a m ([IOPair a], TermStat) -- 内側リストの基数はfunのarity, 外側はbkのIO pairのうちmatchするのはいくつあるか
                                                    -- てゆーか，内側はbkのarityでは？
subtractIOPairsUTm :: TermStat -> IOPair a -> Fun a -> UniT a m ([IOPair a], TermStat)
subtractIOPairsUTm TermStat
ts IOPair a
tgt Fun a
bkf = do
                                Subst a
s <- (St a -> Subst a) -> StateT (St a) m (Subst a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St a -> Subst a
forall a. St a -> Subst a
subst
                                let aptgt :: IOPair a
aptgt = Subst a -> IOPair a -> IOPair a
forall a. [(Int, Expr a)] -> IOPair a -> IOPair a
applyIOP Subst a
s IOPair a
tgt
                                    bktbs :: TBS
bktbs = Fun a -> TBS
forall a. Fun a -> TBS
toBeSought Fun a
bkf
                                    -- apbkf = applyIOPs s bkf
                                    apvistgt :: [Expr a]
apvistgt = [Expr a] -> [Expr a]
forall a. [a] -> [a]
reverse ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ TBS -> [Expr a] -> [Expr a]
forall a. TBS -> [a] -> [a]
visibles (TBS -> TBS
forall a. [a] -> [a]
reverse TBS
bktbs) ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ [Expr a] -> [Expr a]
forall a. [a] -> [a]
reverse ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
aptgt
                                IOPair a
bkiop <- [StateT (St a) m (IOPair a)] -> StateT (St a) m (IOPair a)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([StateT (St a) m (IOPair a)] -> StateT (St a) m (IOPair a))
-> [StateT (St a) m (IOPair a)] -> StateT (St a) m (IOPair a)
forall a b. (a -> b) -> a -> b
$ (IOPair a -> StateT (St a) m (IOPair a))
-> [IOPair a] -> [StateT (St a) m (IOPair a)]
forall a b. (a -> b) -> [a] -> [b]
map IOPair a -> StateT (St a) m (IOPair a)
forall (m :: * -> *) a. Monad m => a -> m a
return ([IOPair a] -> [StateT (St a) m (IOPair a)])
-> [IOPair a] -> [StateT (St a) m (IOPair a)]
forall a b. (a -> b) -> a -> b
$ Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
bkf
                                let visbki :: [Expr a]
visbki = TBS -> [Expr a] -> [Expr a]
forall a. TBS -> [a] -> [a]
visibles TBS
bktbs ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
bkiop
                                Bool -> StateT (St a) m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT (St a) m ()) -> Bool -> StateT (St a) m ()
forall a b. (a -> b) -> a -> b
$ TermStat -> Bool
evalTS (TermStat -> Bool) -> TermStat -> Bool
forall a b. (a -> b) -> a -> b
$ [Expr a] -> [Expr a] -> TermStat -> TermStat
forall a. [Expr a] -> [Expr a] -> TermStat -> TermStat
updateTS [Expr a]
visbki [Expr a]
apvistgt TermStat
ts  -- applyするまえのbkfで投機的にfilterしてみたけど，いまいち．
                                let apvisbki :: [Expr a]
apvisbki = (Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map (Subst a -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply Subst a
s) [Expr a]
visbki
                                [IOPair a]
iops <- IOPair a -> IOPair a -> UniT a m [IOPair a]
forall (m :: * -> *) a.
MonadPlus m =>
IOPair a -> IOPair a -> UniT a m [IOPair a]
subtractIOPairUTm IOPair a
aptgt IOPair a
bkiop{inputs :: [Expr a]
inputs=[Expr a]
apvisbki, output :: Expr a
output=Subst a -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply Subst a
s (Expr a -> Expr a) -> Expr a -> Expr a
forall a b. (a -> b) -> a -> b
$ IOPair a -> Expr a
forall a. IOPair a -> Expr a
output IOPair a
bkiop}
                                let newts :: TermStat
newts = [Expr a] -> [Expr a] -> TermStat -> TermStat
forall a. [Expr a] -> [Expr a] -> TermStat -> TermStat
updateTS [Expr a]
apvisbki [Expr a]
apvistgt TermStat
ts -- This makes sure that the generated program does not go into a loop.
                                Bool -> StateT (St a) m ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> StateT (St a) m ()) -> Bool -> StateT (St a) m ()
forall a b. (a -> b) -> a -> b
$ TermStat -> Bool
evalTS TermStat
newts
--                                guard $ lessExprss (reverse bkis) (reverse apis)
                                ([IOPair a], TermStat) -> UniT a m ([IOPair a], TermStat)
forall (m :: * -> *) a. Monad m => a -> m a
return ([IOPair a]
iops, TermStat
newts)

-- 例えば，join [x,y] [z,w] = [x,y,z,w]からbk [a,b] [c,d] = [a,c,b,d]を引くことを考える．
-- join [x,y] [z,w] = bk (f [x,y] [z,w]) (g [x,y] [z,w])においてf [x,y] [z,w] = [x,z], g [x,y] [z,w] = [y,w]なので，
-- subtractIOPair IOP{inputs=[[x,y],[z,w]],output=[x,y,z,w]} IOP{inputs=[[a,b],[c,d]],output=[a,c,b,d]} = [IOP{inputs=[[x,y],[z,w]],output=[x,z]}, IOP{inputs=[[x,y],[z,w]],output=[y,w]}]
-- ということになる．
subtractIOPairUTm :: MonadPlus m => IOPair a -> IOPair a -> UniT a m [IOPair a]
subtractIOPairUTm :: IOPair a -> IOPair a -> UniT a m [IOPair a]
subtractIOPairUTm IOPair a
fun IOPair a
bkiop
                      = do IOPair a
frbkiop <- IOPair a -> StateT (St a) m (IOPair a)
forall (m :: * -> *) a1 a2.
MonadState (St a1) m =>
IOPair a2 -> m (IOPair a2)
freshIOP IOPair a
bkiop
                           Expr a -> Expr a -> UniT a m ()
forall (m :: * -> *) a.
MonadPlus m =>
Expr a -> Expr a -> StateT (St a) m ()
unifyUT (IOPair a -> Expr a
forall a. IOPair a -> Expr a
output IOPair a
frbkiop) (IOPair a -> Expr a
forall a. IOPair a -> Expr a
output IOPair a
fun)
                           Subst a
s <- (St a -> Subst a) -> StateT (St a) m (Subst a)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets St a -> Subst a
forall a. St a -> Subst a
subst
                           [IOPair a] -> UniT a m [IOPair a]
forall (m :: * -> *) a. Monad m => a -> m a
return [ IOPair a
fun{output :: Expr a
output=Subst a -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apply Subst a
s Expr a
o} | Expr a
o <- IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
frbkiop ] -- This @apply@ is necessary here because introBKm will soon forget the substitution.

subtractIOPairsFromIOPairsm :: Int -- maxNumBVsでゲットできる値．
                               -> TermStat -> Fun a -> Fun a -> [] [[IOPair a]]
subtractIOPairsFromIOPairsm :: Int -> TermStat -> Fun a -> Fun a -> [[[IOPair a]]]
subtractIOPairsFromIOPairsm Int
addendum TermStat
ts Fun a
tgt Fun a
bkf
    = Int
-> TermStat -> Int -> [IOPair a] -> Fun a -> Int -> [[[IOPair a]]]
forall a.
Int
-> TermStat -> Int -> [IOPair a] -> Fun a -> Int -> [[[IOPair a]]]
subtractIOPairsFromIOPairsmFME Int
addendum TermStat
ts (TBS -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (TBS -> Int) -> TBS -> Int
forall a b. (a -> b) -> a -> b
$ (Bool -> Bool) -> TBS -> TBS
forall a. (a -> Bool) -> [a] -> [a]
filter Bool -> Bool
forall a. a -> a
id (TBS -> TBS) -> TBS -> TBS
forall a b. (a -> b) -> a -> b
$ Fun a -> TBS
forall a. Fun a -> TBS
toBeSought Fun a
tgt) -- the actual arity
        (Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
tgt) Fun a
bkf Int
addendum
subtractIOPairsFromIOPairsmFME :: Int -> TermStat -> Int -> [IOPair a] -> Fun a -> Int -> [] [[IOPair a]]
{-
subtractIOPairsFromIOPairsBK funs bks = foldr (liftM2 (:)) (return []) $ map (flip subtractIOPairs bks) funs
-}
subtractIOPairsFromIOPairsmFME :: Int
-> TermStat -> Int -> [IOPair a] -> Fun a -> Int -> [[[IOPair a]]]
subtractIOPairsFromIOPairsmFME Int
addendum TermStat
ts Int
ary []         Fun a
bkf Int
offset = [[IOPair a]] -> [[[IOPair a]]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
subtractIOPairsFromIOPairsmFME Int
addendum TermStat
ts Int
ary (IOPair a
fun:[IOPair a]
funs) Fun a
bkf Int
offset = do 
                                                 ([IOPair a]
iops,TermStat
newts) <- TermStat
-> Int -> IOPair a -> Fun a -> Int -> [([IOPair a], TermStat)]
forall a.
TermStat
-> Int -> IOPair a -> Fun a -> Int -> [([IOPair a], TermStat)]
subtractIOPairsmFME TermStat
ts Int
ary IOPair a
fun Fun a
bkf Int
offset
                                                 [[IOPair a]]
iopss <- Int
-> TermStat -> Int -> [IOPair a] -> Fun a -> Int -> [[[IOPair a]]]
forall a.
Int
-> TermStat -> Int -> [IOPair a] -> Fun a -> Int -> [[[IOPair a]]]
subtractIOPairsFromIOPairsmFME Int
addendum TermStat
newts Int
ary [IOPair a]
funs Fun a
bkf (Int
offsetInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
addendum) -- iopsは，subfunctionが複数あって，それらsubfunctionsのそれぞれに関してIOPair1個ずつに過ぎない．
                                                 [[IOPair a]] -> [[[IOPair a]]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([IOPair a]
iops[IOPair a] -> [[IOPair a]] -> [[IOPair a]]
forall a. a -> [a] -> [a]
:[[IOPair a]]
iopss)
-- Applying substitutions to funs is not currently necessary (because funs does not include existential variables), but that will be useful in future versions which fill gaps of input examples.

subtractIOPairsmFME :: TermStat -> Int -> IOPair a -> Fun a -> Int -> [([IOPair a], TermStat)] -- 返り値の[IOPair]は各引数に対応
subtractIOPairsmFME :: TermStat
-> Int -> IOPair a -> Fun a -> Int -> [([IOPair a], TermStat)]
subtractIOPairsmFME TermStat
ts Int
ary IOPair a
tgtiop Fun a
bkf Int
offset 
  = case IOPair a -> Expr a
forall a. IOPair a -> Expr a
output IOPair a
tgtiop of E{}  -> [(Int -> IOPair a -> [IOPair a]
forall a. Int -> a -> [a]
replicate (Fun a -> Int
forall a. Fun a -> Int
arity Fun a
bkf) IOPair a
tgtiop, TermStat
ts)] -- targetの返り値が単にexistential variableの場合，使われないのでなんでもよい．が，arityを揃える必要がある．
                          Expr a
tgto -> do 
                                let vistgt :: [Expr a]
vistgt = [Expr a] -> [Expr a]
forall a. [a] -> [a]
reverse ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ TBS -> [Expr a] -> [Expr a]
forall a. TBS -> [a] -> [a]
visibles (TBS -> TBS
forall a. [a] -> [a]
reverse (TBS -> TBS) -> TBS -> TBS
forall a b. (a -> b) -> a -> b
$ Fun a -> TBS
forall a. Fun a -> TBS
toBeSought Fun a
bkf) ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ [Expr a] -> [Expr a]
forall a. [a] -> [a]
reverse ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
tgtiop
                                [Expr a]
visbkis <- Expr a -> FMExpr [IOPair a] -> Int -> [[Expr a]]
forall a. Expr a -> FMExpr [IOPair a] -> Int -> [[Expr a]]
unifyingIOPairs Expr a
tgto (Fun a -> FMExpr [IOPair a]
forall a. Fun a -> FMExpr [IOPair a]
fmexpr Fun a
bkf) Int
offset
                                let iops :: [IOPair a]
iops = [ IOPair a
tgtiop{output :: Expr a
output=Expr a
o} | Expr a
o <- [Expr a]
visbkis ]
                                let newts :: TermStat
newts = [Expr a] -> [Expr a] -> TermStat -> TermStat
forall a. [Expr a] -> [Expr a] -> TermStat -> TermStat
updateTS [Expr a]
visbkis [Expr a]
vistgt TermStat
ts -- This makes sure that the generated program does not go into a loop.
                                Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ TermStat -> Bool
evalTS TermStat
newts
--                                guard $ lessExprss (reverse bkis) (reverse apis)
                                ([IOPair a], TermStat) -> [([IOPair a], TermStat)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([IOPair a]
iops, TermStat
newts)
                                
                                
subtractIOPairsFromIOPairsBKm :: Int -- maxNumBVsでゲットできる値．
                                 -> [IOPair a] -> (Fun a) -> [] [[IOPair a]]
subtractIOPairsFromIOPairsBKm :: Int -> [IOPair a] -> Fun a -> [[[IOPair a]]]
subtractIOPairsFromIOPairsBKm Int
addendum [IOPair a]
tgt Fun a
bkf = Int -> [IOPair a] -> FMExpr [IOPair a] -> Int -> [[[IOPair a]]]
forall a.
Int -> [IOPair a] -> FMExpr [IOPair a] -> Int -> [[[IOPair a]]]
subtractIOPairsFromIOPairsBKmFME Int
addendum [IOPair a]
tgt ([IOPair a] -> FMExpr [IOPair a]
forall a. [IOPair a] -> FMExpr [IOPair a]
iopsToFME ([IOPair a] -> FMExpr [IOPair a])
-> [IOPair a] -> FMExpr [IOPair a]
forall a b. (a -> b) -> a -> b
$ Fun a -> [IOPair a]
forall a. Fun a -> [IOPair a]
iopairs Fun a
bkf) Int
addendum
subtractIOPairsFromIOPairsBKmFME :: Int -> [IOPair a] -> FMExpr [IOPair a] -> Int -> [] [[IOPair a]]
{-
subtractIOPairsFromIOPairsBK funs bks = foldr (liftM2 (:)) (return []) $ map (flip subtractIOPairs bks) funs
-}
subtractIOPairsFromIOPairsBKmFME :: Int -> [IOPair a] -> FMExpr [IOPair a] -> Int -> [[[IOPair a]]]
subtractIOPairsFromIOPairsBKmFME Int
addendum []         FMExpr [IOPair a]
bkf Int
offset = [[IOPair a]] -> [[[IOPair a]]]
forall (m :: * -> *) a. Monad m => a -> m a
return []
subtractIOPairsFromIOPairsBKmFME Int
addendum (IOPair a
fun:[IOPair a]
funs) FMExpr [IOPair a]
bkf Int
offset = do 
                                                 [IOPair a]
iops <- IOPair a -> FMExpr [IOPair a] -> Int -> [[IOPair a]]
forall a. IOPair a -> FMExpr [IOPair a] -> Int -> [[IOPair a]]
subtractIOPairsBKmFME IOPair a
fun FMExpr [IOPair a]
bkf Int
offset
                                                 [[IOPair a]]
iopss <- Int -> [IOPair a] -> FMExpr [IOPair a] -> Int -> [[[IOPair a]]]
forall a.
Int -> [IOPair a] -> FMExpr [IOPair a] -> Int -> [[[IOPair a]]]
subtractIOPairsFromIOPairsBKmFME Int
addendum [IOPair a]
funs FMExpr [IOPair a]
bkf (Int
offsetInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
addendum) -- iopsは，subfunctionが複数あって，それらsubfunctionsのそれぞれに関してIOPair1個ずつに過ぎない．
                                                 [[IOPair a]] -> [[[IOPair a]]]
forall (m :: * -> *) a. Monad m => a -> m a
return ([IOPair a]
iops[IOPair a] -> [[IOPair a]] -> [[IOPair a]]
forall a. a -> [a] -> [a]
:[[IOPair a]]
iopss)
-- Applying substitutions to funs is not currently necessary (because funs does not include existential variables), but that will be useful in future versions which fill gaps of input examples.
                              
                                
                                
subtractIOPairsBKmFME :: IOPair a -> FMExpr [IOPair a] -> Int -> [] [IOPair a] -- 返り値の[IOPair a]は各引数に対応
subtractIOPairsBKmFME :: IOPair a -> FMExpr [IOPair a] -> Int -> [[IOPair a]]
subtractIOPairsBKmFME IOPair a
tgtiop FMExpr [IOPair a]
bkfme Int
offset = do 
                                [Expr a]
visbkis <- Expr a -> FMExpr [IOPair a] -> Int -> [[Expr a]]
forall a. Expr a -> FMExpr [IOPair a] -> Int -> [[Expr a]]
unifyingIOPairs (IOPair a -> Expr a
forall a. IOPair a -> Expr a
output IOPair a
tgtiop) FMExpr [IOPair a]
bkfme Int
offset
                                [IOPair a] -> [[IOPair a]]
forall (m :: * -> *) a. Monad m => a -> m a
return [ IOPair a
tgtiop{output :: Expr a
output=Expr a
o} | Expr a
o <- [Expr a]
visbkis ]


unifyingIOPairs :: Expr a -> FMExpr [IOPair a] -> Int -> [] [Expr a]
unifyingIOPairs :: Expr a -> FMExpr [IOPair a] -> Int -> [[Expr a]]
unifyingIOPairs Expr a
e FMExpr [IOPair a]
fme Int
0      = [ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
iop | ([IOPair a]
iops, Subst a
_) <- Expr a -> FMExpr [IOPair a] -> [([IOPair a], Subst a)]
forall b a. Expr b -> FMExpr a -> [(a, Subst b)]
unifyFME Expr a
e FMExpr [IOPair a]
fme, IOPair a
iop <- [IOPair a]
iops ]
unifyingIOPairs Expr a
e FMExpr [IOPair a]
fme Int
offset = [ (Expr a -> Expr a) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> [a] -> [b]
map ((Int -> Int) -> Expr a -> Expr a
forall a. (Int -> Int) -> Expr a -> Expr a
mapE (Int
offsetInt -> Int -> Int
forall a. Num a => a -> a -> a
+) (Expr a -> Expr a) -> (Expr a -> Expr a) -> Expr a -> Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Subst a -> Expr a -> Expr a
forall a. [(Int, Expr a)] -> Expr a -> Expr a
apfresh Subst a
s) ([Expr a] -> [Expr a]) -> [Expr a] -> [Expr a]
forall a b. (a -> b) -> a -> b
$ IOPair a -> [Expr a]
forall a. IOPair a -> [Expr a]
inputs IOPair a
iop | ([IOPair a]
iops, Subst a
s) <- Expr a -> FMExpr [IOPair a] -> [([IOPair a], Subst a)]
forall b a. Expr b -> FMExpr a -> [(a, Subst b)]
unifyFME Expr a
e FMExpr [IOPair a]
fme, IOPair a
iop <- [IOPair a]
iops ]