MagicHaskeller-0.8.6: MagicHaskeller/Analytical/Synthesize.hs
--
-- (C) Susumu Katayama
--
{-# LANGUAGE CPP #-}
module MagicHaskeller.Analytical.Synthesize where
import Data.List(transpose)
-- 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
-- | function specification by examples.
data Fun = BKF {maxNumBVs :: Int, arity :: Int, iopairs :: [IOPair], fmexpr :: FMExpr [IOPair]} -- ^ the function is really a background knowledge (and thus there is no need for loop check)
| Rec {maxNumBVs :: Int, arity :: Int, iopairs :: [IOPair], fmexpr :: FMExpr [IOPair], toBeSought :: TBS} -- ^ it is actually a recursive call.
mkBKFun iops@(iop:_) = BKF {maxNumBVs = maximum $ map numUniIDs iops, arity = length $ inputs iop, iopairs = iops, fmexpr = iopsToFME iops}
mkRecFun ari tbs iops@(iop:_) = Rec {maxNumBVs = maximum $ map numUniIDs iops, arity = ari, iopairs = iops, fmexpr = iopsToVisFME tbs iops, toBeSought = tbs} -- arity = filter id tbs, but it is usually know beforehand
setIOPairs iops recfun@Rec{toBeSought=tbs} = recfun{iopairs = iops, fmexpr = iopsToVisFME tbs iops}
type BK = [Types.Typed Fun] -- ^ background knowledge.
applyFun s fun = fun{iopairs = applyIOPs s (iopairs fun)}
analyticSynth :: Search m => TyConLib -> VarLib -> [Dec] -> [Dec] -> m CoreExpr
analyticSynth tcl vl target bkdec = fst $ analyticSynthAndInfType tcl vl target bkdec
analyticSynthAndInfType :: Search m => TyConLib -> VarLib -> [Dec] -> [Dec] -> (m CoreExpr, Types.Type)
analyticSynthAndInfType 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¤Ë¤Ï¤¤¤Ã¤Æ¤¤¤ì¤Ðºî¤ì¤ë¡¥
analSynthm {- analSynthNoUniT ¤³¤Ã¤Á¤À¤È¤Á¤ç¤Ã¤È¤¤¤¤²Ã¸º¤Ç¤Á¤ç¤Ã¤È®¤¤ -} bk (target Types.:::ty)
,ty)
_ -> error "TypedIOPairs.analyticSynth*: More than one I/O pairs are defined as the target."
where xvl = mkXVarLib vl
analSynth, analSynthm :: Search m => BK -> Types.Typed Fun -> m CoreExpr
analSynth bk tfun@(fun Types.::: _) | any hasExistential $ map output $ iopairs fun = fmap fst $ runStateT (analSynthUTm bk tfun) emptySt
| otherwise = analSynthm bk tfun
analSynthm bk tfun
= others `mplus` delay bkRelated
where newbk = tfun : bk
bkRelated = headSpine analSynth introBKm newbk tfun
others = headSpine analSynthm (introConstr +++ introVarm +++ ndelayIntro 2 introCase) newbk tfun
headSpine rec intro bk tfun
= do (hd, subfuns, mbpivot) <- intro bk tfun
subexps <- mapM (\subfun -> let arisub = arity $ Types.typee subfun in fmap (\e -> Fix e arisub (mkArgs mbpivot arisub)) $ rec bk subfun) subfuns
return (hd subexps)
#ifdef DEBUG
headSpine_debug rec trs intro bk tfun
= do (hd, subfuns, mbpivot) <- intro bk tfun
subexps <- zipWithM (\tr subfun -> let arisub = 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 -> Types.Typed Fun -> UniT m CoreExpr
-- analSynthm ([], _, _) = mzero -- If there is no example, nothing can be done. (But is this line necessary?)
analSynthUTm bk (fun Types.::: ty)
= do
s <- gets subst
let aptfun = applyFun s fun Types.::: ty
newbk = aptfun : bk
headSpine analSynthUTm introAny newbk aptfun
mkArgs Nothing arisub = [arisub-1,arisub-2..0]
mkArgs (Just pivot) arisub = take pivot [arisub,arisub-1..] ++ [arisub-pivot-1,arisub-pivot-2..0]
#ifdef DEBUG
analyticSynthNoUniT_debug :: Search m => Tree (Introducer 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 is inaccurate, but should work in most cases. This can be used in place of analSynthm
analSynthNoUniT bk tfun
= headSpine analSynthNoUniT (introConstr +++ introVarm +++ ndelayIntro 2 introCase +++ ndelayIntro 1 introBKm) (tfun:bk) tfun
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 m)
tryall = Br introAny (repeat tryall)
tryVar = Br introVarUTm []
tryVarm :: (Functor m, MonadPlus m) => Tree (Introducer m)
tryVarm = Br introVarm []
analyticSynth_debug :: Search m => Tree (IntroUniT 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 m) -> BK -> Types.Typed Fun -> UniT 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 m = BK -> Types.Typed Fun -> m ([CoreExpr] -> CoreExpr, [Types.Typed Fun], Maybe Int)
type IntroUniT m = Introducer (UniT m)
-- NB: We should not use @StateT Env@ where @Env=(BK,TBS)@ because the Env affects only subexpressions.
il +++ ir = \bk iops -> il bk iops `mplus` ir bk iops
ndelayIntro n intro = \e a -> ndelay n $ intro e a
introAny :: Search m => IntroUniT m
introAny = introConstr +++ {- +/ -} (
introVarUTm +++
ndelayIntro 1 introBKUTm +++
ndelayIntro 2 introCase )
(+/) :: MonadPlus m => IntroUniT [] -> IntroUniT m -> IntroUniT m
m +/ n = \bk iops ->
do st <- get
case runStateT (m bk iops) st of [] -> n bk iops
ts -> StateT $ \_ -> msum $ map return ts
liftList :: MonadPlus m => StateT s [] a -> StateT s m a
liftList = mapStateT (msum . map return)
introVarm, introConstr, introCase :: (Functor m, MonadPlus m) => Introducer m -- introConstr¤Ç¤Ï¡¤¼ÂºÝ¤Ë¤ÏCoreExpr¤ÏConstr¤Ç¤è¤¤¡¥
introBKm :: (Search m) => Introducer m -- introConstr¤Ç¤Ï¡¤¼ÂºÝ¤Ë¤ÏCoreExpr¤ÏConstr¤Ç¤è¤¤¡¥
introVarUTm, introBKUTm :: MonadPlus m => IntroUniT 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 b f = liftList $ introVar (zipWithM_ appUnifyUT) b f
-- introVarm b f = introVar (zipWithM_ unify) b f *************************************** ¤³¤ì¤Ï¥Ç¥Ð¥Ã¥°»þ¤ËÍÍѤʤ³¤È¤â¡¥
introVarm = introVar (\a b -> guard $ a==b)
introVar :: MonadPlus m => ([Expr] -> [Expr] -> m ()) -> Introducer m
introVar cmp _ (fun Types.::: ty)
= do let (argtys, retty) = Types.splitArgs ty
iops = iopairs fun
arifun = arity fun
let trins = transpose $ map inputs iops
-- (ix,inps Types.::: argty) <- msum $ map return $ zip [0..] trins
(ix,argty,inps) <- msum [ return t | t@(_,aty,_) <- zip3 [0..] argtys $ visibles (toBeSought fun) trins, aty == retty ]
-- The following four lines should be equivalent to
cmp (map output iops) 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
-}
return (const (X ix), [], Nothing)
introConstr bk (fun Types.::: ty)
= let argtys = Types.getArgs ty
iops = iopairs fun
in
case [ output iop | iop <- iops ] of
outs@(C _ (cid Types.::: cty) flds : rest)
| all (`sConstrIs` cid) rest -> return (foldl (:$) (Primitive cid),
zipWith (\iops retty -> setIOPairs iops fun Types.::: Types.popArgs argtys retty)
(transpose [ divideIOP iop | iop <- iops ])
(case Types.revSplitArgs cty of (_,fieldtys,_) -> fieldtys),
Nothing)
_ -> mzero
divideIOP (IOP bvs ins out) = map (IOP bvs ins) $ fields out -- The actual number of buondVars may reduce, but not updating the field would not hurt.
shareConstr (C _ (cid Types.::: _) _ : iops) = all (`sConstrIs` cid) iops
shareConstr _ = False
-- type¤¬°ã¤¦¤ÈƱ¤¸cid¤ò°Û¤Ê¤ëconstructor¤Ç»È¤¤ÆÀ¤ë¾ì¹ç¡¤type¤´¤ÈÈæ³Ó¤¹¤ëɬÍפ¬¤¢¤ë¤¬¡¤¸½ºß¤Ï¤½¤¦¤Ç¤Ï¤Ê¤¤¤Î¤Ç¡¥
C _ (c Types.::: _) _ `sConstrIs` cid = cid==c
_ `sConstrIs` cid = False
select [] [] = []
select (b:bs) (p:ps) | b = (p, False:bs) : rest
| otherwise = rest
where rest = [ (result, b:newbs) | (result,newbs) <- select bs ps ]
introCase bk (fun Types.::: ty) = msum $ reverse $ zipWith introCase' [0..] $ select (toBeSought fun) trins
where trins = transpose $ map inputs iops
(argtys,retty) = Types.splitArgs ty
iops = iopairs fun
arifun = arity fun
introCase' :: MonadPlus m =>
Int -- ^ the pivot position
-> ([Expr],TBS) -- ^ (the pivot expression for each I/O pair, the next TBS)
-> m ([CoreExpr] -> CoreExpr, [Types.Typed Fun], Maybe Int)
introCase' pos (pivots, tbs) -- includes variable cases. Overlapping patterns are not supported yet.
= case mapM maybeCtor pivots of
Nothing -> mzero
Just ctors
-> let
pipairs = zip pivots iops :: [(Expr,IOPair)]
ts = IntMap.toList $ IntMap.fromListWith (\(t,xs) (_,ys) -> (t,xs++ys)) $
zipWith (\(c Types.::: ct) x -> (c,(ct,[x]))) ctors pipairs
:: [(Constr, (Types.Type, [(Expr,IOPair)]))]
-- Array.accum can also be used instead of IntMap because we can tell the range from that of VarLib.
hd ces = Case (X pos)
(zipWith (\(constr, (_, (pivot,_):_)) ce -> (constr, length (fields pivot), ce))
ts
ces)
iopss = [ Rec { maxNumBVs = maxNumBVs fun,
arity = arifun-1+lenflds,
iopairs = iops,
fmexpr = iopsToVisFME newtbs iops,
toBeSought = newtbs
}
Types.::: Types.popArgs (dropNth pos argtys) (Types.popArgs (Types.getArgs cty) retty)
| (_c, (cty, nextpipairs@((C _ _ flds', _):_))) <- ts,
let lenflds = length flds'
iops = [ IOP bvs (reverse flds ++ is) o | (C _ _c flds, IOP bvs is o) <- nextpipairs ]
newtbs = replicate lenflds True ++ tbs
]
in return (hd, iopss, Just (arifun-pos-1))
dropNth pos bs = case splitAt pos bs of (tk,_:dr) -> tk ++ dr
introBKm bk tfun = fromMx $ toMx $ introBK subtractIOPairsFromIOPairsBKm subtractIOPairsFromIOPairsm bk tfun
introBKUTm bk tfun = liftList $ introBK (const subtractIOPairsFromIOPairsBKUTm) (const subtractIOPairsFromIOPairsUTm) bk tfun
introBK subBK sub bk (fun Types.:::ty) = do
let (argtys, retty) = Types.splitArgs ty
(ix, bkfun Types.::: bkty) <- msum $ map return $ tail $ zip [0..] 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 (bkargtys, bkretty) = Types.splitArgs bkty
substy <- Types.match bkretty retty
iopss <- case bkfun of BKF{maxNumBVs=addendum} -> subBK (-addendum) (iopairs fun) bkfun
Rec{maxNumBVs=addendum} -> sub (-addendum) initTS (iopairs fun) bkfun
return (foldl (:$) (FunX ix),
[ setIOPairs iops fun Types.::: tys
| iops Types.::: tys <- reverse $
zipWith (\x retty -> x Types.::: Types.popArgs argtys retty)
(transpose iopss)
(map (Types.apply substy) bkargtys) ],
Nothing)
subtractIOPairsFromIOPairsBKUTm :: MonadPlus m => [IOPair] -> Fun -> UniT m [[IOPair]]
{-
subtractIOPairsFromIOPairsBK funs bks = foldr (liftM2 (:)) (return []) $ map (flip subtractIOPairs bks) funs
-}
subtractIOPairsFromIOPairsBKUTm [] bkf = return []
subtractIOPairsFromIOPairsBKUTm (fun:funs) bkf = do
iops <- subtractIOPairsBKUTm fun bkf
iopss <- subtractIOPairsFromIOPairsBKUTm funs bkf -- iops¤Ï¡¤subfunction¤¬Ê£¿ô¤¢¤Ã¤Æ¡¤¤½¤ì¤ésubfunctions¤Î¤½¤ì¤¾¤ì¤Ë´Ø¤·¤ÆIOPair1¸Ä¤º¤Ä¤Ë²á¤®¤Ê¤¤¡¥
return (iops: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 -> Fun -> UniT m [IOPair] -- Æ⦥ꥹ¥È¤Î´ð¿ô¤Ïfun¤Îarity, ³°Â¦¤Ïbk¤ÎIO pair¤Î¤¦¤Ámatch¤¹¤ë¤Î¤Ï¤¤¤¯¤Ä¤¢¤ë¤«
-- ¤Æ¤æ¡¼¤«¡¤Æ⦤Ïbk¤Îarity¤Ç¤Ï¡©
subtractIOPairsBKUTm tgt bkf = do
s <- gets subst
let aptgt = applyIOP s tgt
apbkf = applyIOPs s $ iopairs bkf
bkiop <- msum $ map return apbkf
subtractIOPairUTm aptgt bkiop
subtractIOPairsFromIOPairsUTm :: MonadPlus m => TermStat -> [IOPair] -> Fun -> UniT m [[IOPair]]
{-
subtractIOPairsFromIOPairs funs bks = foldr (\fun rest -> do iops <- subtractIOPairs fun bks
iopss <- rest
return (iops:iopss)) (return []) funs
-}
subtractIOPairsFromIOPairsUTm ts [] bkf = return []
subtractIOPairsFromIOPairsUTm ts (fun:funs) bkf = do
(iops,newts) <- subtractIOPairsUTm ts fun bkf
iopss <- subtractIOPairsFromIOPairsUTm newts funs bkf -- iops¤Ï¡¤subfunction¤¬Ê£¿ô¤¢¤Ã¤Æ¡¤¤½¤ì¤ésubfunctions¤Î¤½¤ì¤¾¤ì¤Ë´Ø¤·¤ÆIOPair1¸Ä¤º¤Ä¤Ë²á¤®¤Ê¤¤¡¥
return (iops:iopss)
subtractIOPairsUTm :: MonadPlus m => TermStat -> IOPair -> Fun -> UniT m ([IOPair], TermStat) -- Æ⦥ꥹ¥È¤Î´ð¿ô¤Ïfun¤Îarity, ³°Â¦¤Ïbk¤ÎIO pair¤Î¤¦¤Ámatch¤¹¤ë¤Î¤Ï¤¤¤¯¤Ä¤¢¤ë¤«
-- ¤Æ¤æ¡¼¤«¡¤Æ⦤Ïbk¤Îarity¤Ç¤Ï¡©
subtractIOPairsUTm ts tgt bkf = do
s <- gets subst
let aptgt = applyIOP s tgt
bktbs = toBeSought bkf
-- apbkf = applyIOPs s bkf
apvistgt = reverse $ visibles (reverse bktbs) $ reverse $ inputs aptgt
bkiop <- msum $ map return $ iopairs bkf
let visbki = visibles bktbs $ inputs bkiop
guard $ evalTS $ updateTS visbki apvistgt ts -- apply¤¹¤ë¤Þ¤¨¤Îbkf¤ÇÅ굡Ū¤Ëfilter¤·¤Æ¤ß¤¿¤±¤É¡¤¤¤¤Þ¤¤¤Á¡¥
let apvisbki = map (apply s) visbki
iops <- subtractIOPairUTm aptgt bkiop{inputs=apvisbki, output=apply s $ output bkiop}
let newts = updateTS apvisbki apvistgt ts -- This makes sure that the generated program does not go into a loop.
guard $ evalTS newts
-- guard $ lessExprss (reverse bkis) (reverse apis)
return (iops, 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 -> IOPair -> UniT m [IOPair]
subtractIOPairUTm fun bkiop
= do frbkiop <- freshIOP bkiop
unifyUT (output frbkiop) (output fun)
s <- gets subst
return [ fun{output=apply s o} | o <- inputs frbkiop ] -- This @apply@ is necessary here because introBKm will soon forget the substitution.
subtractIOPairsFromIOPairsm :: Int -- maxNumBVs¤Ç¥²¥Ã¥È¤Ç¤¤ëÃÍ¡¥
-> TermStat -> [IOPair] -> Fun -> [] [[IOPair]]
subtractIOPairsFromIOPairsm addendum ts tgt bkf = subtractIOPairsFromIOPairsmFME addendum ts tgt bkf addendum
subtractIOPairsFromIOPairsmFME :: Int -> TermStat -> [IOPair] -> Fun -> Int -> [] [[IOPair]]
{-
subtractIOPairsFromIOPairsBK funs bks = foldr (liftM2 (:)) (return []) $ map (flip subtractIOPairs bks) funs
-}
subtractIOPairsFromIOPairsmFME addendum ts [] bkf offset = return []
subtractIOPairsFromIOPairsmFME addendum ts (fun:funs) bkf offset = do
(iops,newts) <- subtractIOPairsmFME ts fun bkf offset
iopss <- subtractIOPairsFromIOPairsmFME addendum newts funs bkf (offset+addendum) -- iops¤Ï¡¤subfunction¤¬Ê£¿ô¤¢¤Ã¤Æ¡¤¤½¤ì¤ésubfunctions¤Î¤½¤ì¤¾¤ì¤Ë´Ø¤·¤ÆIOPair1¸Ä¤º¤Ä¤Ë²á¤®¤Ê¤¤¡¥
return (iops: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 -> IOPair -> Fun -> Int -> [([IOPair], TermStat)] -- ÊÖ¤êÃͤÎ[IOPair]¤Ï³Æ°ú¿ô¤ËÂбþ
subtractIOPairsmFME ts tgtiop bkf offset = do
let vistgt = reverse $ visibles (reverse $ toBeSought bkf) $ reverse $ inputs tgtiop
visbkis <- unifyingIOPairs (output tgtiop) (fmexpr bkf) offset
let iops = [ tgtiop{output=o} | o <- visbkis ]
let newts = updateTS visbkis vistgt ts -- This makes sure that the generated program does not go into a loop.
guard $ evalTS newts
-- guard $ lessExprss (reverse bkis) (reverse apis)
return (iops, newts)
subtractIOPairsFromIOPairsBKm :: Int -- maxNumBVs¤Ç¥²¥Ã¥È¤Ç¤¤ëÃÍ¡¥
-> [IOPair] -> Fun -> [] [[IOPair]]
subtractIOPairsFromIOPairsBKm addendum tgt bkf = subtractIOPairsFromIOPairsBKmFME addendum tgt (iopsToFME $ iopairs bkf) addendum
subtractIOPairsFromIOPairsBKmFME :: Int -> [IOPair] -> FMExpr [IOPair] -> Int -> [] [[IOPair]]
{-
subtractIOPairsFromIOPairsBK funs bks = foldr (liftM2 (:)) (return []) $ map (flip subtractIOPairs bks) funs
-}
subtractIOPairsFromIOPairsBKmFME addendum [] bkf offset = return []
subtractIOPairsFromIOPairsBKmFME addendum (fun:funs) bkf offset = do
iops <- subtractIOPairsBKmFME fun bkf offset
iopss <- subtractIOPairsFromIOPairsBKmFME addendum funs bkf (offset+addendum) -- iops¤Ï¡¤subfunction¤¬Ê£¿ô¤¢¤Ã¤Æ¡¤¤½¤ì¤ésubfunctions¤Î¤½¤ì¤¾¤ì¤Ë´Ø¤·¤ÆIOPair1¸Ä¤º¤Ä¤Ë²á¤®¤Ê¤¤¡¥
return (iops: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 -> FMExpr [IOPair] -> Int -> [] [IOPair] -- ÊÖ¤êÃͤÎ[IOPair]¤Ï³Æ°ú¿ô¤ËÂбþ
subtractIOPairsBKmFME tgtiop bkfme offset = do
visbkis <- unifyingIOPairs (output tgtiop) bkfme offset
return [ tgtiop{output=o} | o <- visbkis ]
unifyingIOPairs :: Expr -> FMExpr [IOPair] -> Int -> [] [Expr]
unifyingIOPairs e fme 0 = [ inputs iop | (iops, _) <- unifyFME e fme, iop <- iops ]
unifyingIOPairs e fme offset = [ map (mapE (offset+) . apfresh s) $ inputs iop | (iops, s) <- unifyFME e fme, iop <- iops ]