{-# OPTIONS_GHC -XTemplateHaskell #-} module Igor2.RuleDevelopment.ListCata ( listCata )where import Data.Maybe (catMaybes, listToMaybe, fromJust, isJust, mapMaybe) import Data.List (partition, nub, findIndices, (\\), intersect) import qualified Data.Set as S (fromList) import Control.Monad import Control.Monad.Error import Data.Function (on) import Igor2.Data.IgorMonad import Igor2.Data.CallDependencies import Igor2.Data.Rules import Data.Util import Syntax import Igor2.Ppr import Igor2.Logging listCata :: CovrRule -> Int -> IM [(CovrRules,[Call])] listCata cr i = do evi <- breakupM cr catchError (checkUniPropAndMkIOs i evi >>= mkFoldCall i cr) (\e -> logNO (text $ "No fold: " ++ e) >> naiveMap i cr evi) -- maybe it is better to include naive Map as a 'normal' operator, but this --has to be checked with the heuristics mkFoldCall :: Int -> CovrRule -> (Rule,[Rule]) -> IM [(CovrRules,[Call])] mkFoldCall i cr (vr,fios) = (liftM (:[])) . fromJust . msum $ [ mbFilter i cr (vr,fios) , mbMap i cr (vr,fios) , Just $ mkFold i cr (vr,fios) ] noFoldCall :: Int -> IM [(CovrRules, [Call])] noFoldCall i = throwError . strMsg . show $ (text "ListCata not applicable!" <+> text "Universal Property for argument" <+> int i <+> text "not satisfied!") naiveMap :: Int -> CovrRule -> [CovrRule] -> IM [(CovrRules,[Call])] naiveMap i cr evi' = do let evi = map crul evi' let ios = nub . concat . (mapMaybe mbMapIO) $ evi if (not $ all (listAndSameLength i) evi) || (any hasFreeVars ios) || (null ios) then noFoldCall i -- check for naive map property, if there are ios, and if ios are a function else do logNO (text "Naive map detected!") afnm <- addIO . rules $ ios afcr <- coverAll afnm -- the argument function -- map :: (a -> b) -> [a] -> [b] -- map :: ^ afty ^ -> ^ atys ^ let afty = typeOf . crul $ afcr let atys = unArrowT . typeOf . crul $ cr -- f x0 = map fun1 x0 -- ^afExp^ -- ^ mExp ^ let afExp = foldTAppE ((tConE afnm) [afty])(init . lhs . crul $ cr) let mExp = foldTAppE (tConE 'map (afty:atys)) [afExp, ithArg i $ crul cr] let cr' = modifycrul cr (\r -> rule (lhs r) mExp) return [(covrRules [cr', afcr], [(name cr', afnm, LT)])] where mbMapIO r = liftM (map (\(inn, out) -> rule (butIthArg i r ++ [inn]) out)) $ liftM2 zip (mbListElems $ ithArg i r) (mbListElems . rhs $ r) mbFilter :: Int -> CovrRule -> (Rule,[Rule]) -> Maybe (IM (CovrRules,[Call])) mbFilter i cr (bc,evi) = do -- all IOs of fold's argument function can be partinioned into those where the -- 2nd input argument is identical to the output, and those where the second -- argument occurs unchanged in the output after a cons -- -- >fun1 (S x0) x1 = x1 -- >fun1 (Z) x0 = Z : x0 case partition lastArgIsOut evi of (f@(_:_), t@(_:_)) -> let fio = nub (mkFIO False f) tio = nub (mkFIO True t) in if not (filterApplicable t fio tio) then Nothing else Just $ do logNO (text "ListCata applicable for argument" <+> int i <+> text ", 'filter' detected!") afnm <- addIO . rules $ (fio ++ tio) afcr <- coverAll afnm -- prepare IO examples for the predicate/argument function (af) -- -- -- filter :: (a -> Bool) -> [a] -> [a] -- filter :: ^ pty ^ -> ^ atys ^ let afty = typeOf . crul $ afcr let atys = unArrowT . typeOf . crul $ cr -- f x0 = filter fun1 x0 -- ^pExp^ -- ^ fExp ^ let pExp = foldTAppE ((tConE afnm) [afty]) (init . lhs . crul $ cr) let fExp = foldTAppE (tConE 'filter (afty:atys)) [pExp, ithArg i $ crul cr] let cr' = modifycrul cr (\r -> rule (lhs r) fExp) -- build the 'filter expression' return (covrRules [cr', afcr], [(name cr', afnm, LT)]) otherwise -> Nothing where mkFIO = map . (\b r -> let n = if b then 'True else 'False in rule (init . lhs $ r)(tConE n [boolCon])) -- check wether a rule is just a projection on the second argument lastArgIsOut r = last (lhs r) == rhs r filterApplicable t fio tio = hasMapProperty (bc, t) && null (on intersect (map lhs) fio tio) -- check filter property, i.e. mapProperty on those examples which are not -- a projection on the last argument, and check if ios are a function. mbMap :: Int -> CovrRule -> (Rule,[Rule]) -> Maybe (IM (CovrRules,[Call])) mbMap i cr (bc,evi) = let ios = nub . (maybe [] id) . (mapM mkMapIO) $ evi in if not (mapApplicable ios) then Nothing else Just $ do logNO (text "ListCata applicable for argument" <+> int i <+> text ", 'map' detected!") afnm <- addIO . rules $ ios afcr <- coverAll afnm -- the argument function -- map :: (a -> b) -> [a] -> [b] -- map :: ^ afty ^ -> ^ atys ^ let afty = typeOf . crul $ afcr let atys = unArrowT . typeOf . crul $ cr -- f x0 = map fun1 x0 -- ^afExp^ -- ^ mExp ^ let afExp = foldTAppE ((tConE afnm) [afty])(init . lhs . crul $ cr) let mExp = foldTAppE (tConE 'map (afty:atys)) [afExp, ithArg i $ crul cr] let cr' = modifycrul cr (\r -> rule (lhs r) mExp) return (covrRules [cr', afcr], [(name cr', afnm, LT)]) where mapApplicable ios = hasMapProperty (bc, evi) && all (not . hasFreeVars) ios && not (null ios) -- map property satisfied?, none has free variables?, and ios are not empty mkMapIO r = liftM (rule (init . lhs $ r)) (listToMaybe . subterms . rhs $ r) mkFold :: Int -> CovrRule -> (Rule,[Rule]) -> IM (CovrRules,[Call]) mkFold i cr (vr,ios) = do {- When allowing sections as argument functions, it is possible that the default value contains a variable. Just taking the rhs of the base case would lead to an unbound variable: fun1 x0 x1 = foldr (fun2 x0) [a] x1 with I/O for the base case: fun1 a [] = [a] We could try to find a substitution to replace the variable 'a': 1) Bind the lhs of the example to the lhs of the generalised rule: fun1 x0 x1 fun1 a [] ~~> [x0/a, x1/[]] 2) Now take only those substitutions, which substitutes contain variables ( [x0/a] ) and replace them by the variable in the lhs of the example: fun1 a [] = [a] ~~> fun1 x0 [] = [x0] This leads to the following rule: fun1 x0 x1 = foldr (fun2 x0) [x0] x1 However, the base case for 'fun2' would be like like this: fun2 x0 x1 [x0] = Note the x0 occurs more than once, because this is exactly how we built 'fun2' before, namely that the base case of 'fun2' uses 'x0'. In fact, we use 'x0' for the base case _and_ additionally pass it as argument. Therefore, we remove those variables from the argument list of the argument function. -} subs <- lift . lift $ matchesLhs vr (crul cr) let v = foldl replaceInverseIn (rhs vr) (filter (hasVars . snd) (assocs subs)) let usedVarInd = findIndices (flip elem (nub $ getVars v)) (lhs . crul $ cr) let usedVarIndInIOs = [ case compare j i of { LT -> j; GT -> pred j } | j <- usedVarInd ] logNO (text "ListCata applicable for argument" <+> int i <+> text ", fallback to 'foldr'!") afnm <- addIO . rules $ map (rmArgsAt usedVarIndInIOs) ios afcr <- coverAll afnm -- foldr :: (a -> b -> b) -> b -> [a] -> b -- foldr :: ^ afty ^ -> ^ atys ^ let afty = typeOf . crul $ afcr let atys = [(typeOf . rhs $ vr), typeOf $ ithArg i $ crul cr ,(typeOf . rhs $ vr)] -- -- -- -- f x0 = foldr (fun1 ..) v x0 -- -- ^afExp ^ -- -- ^ fExp ^ let afExp = foldTAppE ((tConE afnm) [afty]) $ (butIthArgs (i:usedVarInd)) . crul $ cr let fExp = foldTAppE (tConE 'foldr (afty: atys)) [afExp, v, ithArg i $ crul cr] let cr' = modifycrul cr (\r -> rule (lhs r) fExp) -- make the fold expression rule return (covrRules [cr', afcr], [(name cr', afnm, GT)]) where replaceInverseIn t (n,s)= replaceTerm s (toVar s n) t rmArgsAt is r = rule (rmAll is (lhs r)) (rhs r) rmAll is l = l \\ (map (l!!) is) {- | Check if the given covered IO examples of a partial rule fulfill the universal property of fold for the specified argument with index 'i': - there is exactly one I/O defined on the empty list - all IOs are closed -} checkUniPropAndMkIOs :: Int -> [CovrRule] -> IM (Rule,[Rule]) checkUniPropAndMkIOs i evi = do (r,rs) <- definedOnNil i evi rs' <- mapM (abduceIO i evi) rs return (crul r,rs') {-| If the given IO examples are defined for the empty list, a tuple containig the base case and the other IOs is returned, Nothing otherwise -} definedOnNil :: (Error e, MonadError e m) => Int -> [CovrRule] -> m (CovrRule, [CovrRule]) definedOnNil i = exactly1Base . partition (isNilList . ithArg i . crul) where exactly1Base (l1, l2) = onlyOne l1 >>= return . flip (,) l2 onlyOne [a] = return a onlyOne _ = throwError . strMsg $ "Not only one" -- onlyOne l -- | all (\e -> ithArg i (crul e) == (rhs . crul) e) l = lift . fuse $ l -- | otherwise = fail "Not only one base case." -- check wether ith input argument type and out type is a list and both have same length listAndSameLength :: Int -> Rule -> Bool listAndSameLength i r = maybe False id $ liftM2 ((==) `on` length) (mbListElems $ ithArg i r)(mbListElems . rhs $ r) mbListElems :: TExp -> Maybe [TExp] mbListElems t@(TAppE _ _) = case unfoldTAppE t of [TConE n _, x, xs] -> if isCons n then fmap (x:) $ mbListElems xs else Nothing [TConE n _] -> if isNil n then Just [] else Nothing -- No List _owise -> Nothing -- No List mbListElems l = Nothing -- No List {- Map Property w.r.t the last argument: - identity on the empty list - for all non-empty lists, the last argument occurs unchanged in the output after a cons -} hasMapProperty :: (Rule,[Rule]) -> Bool hasMapProperty (bc,evi) = and [ isNilList . rhs $ bc , all lastArgConsed evi] where -- check wether the second argument of a rule occurs unchanged in the output -- after a cons lastArgConsed r = case rhs r of t@(TAppE _ _) -> case unfoldTAppE t of [TConE n _, _, xs] -> isCons n && ((last $ lhs r) == xs) _owise -> False _owise -> False abduceIO :: Int -> [CovrRule] -> CovrRule -> IM Rule abduceIO i evi cr = (do (x,xs) <- headTail carg xs' <- evalIO (name cr) (insertAt i xs args) >>= maybe (throwError . strMsg $ "Insufficient support in Examples") return let io = rule (args ++ [x,xs']) (rhs . crul $ cr) if not . hasFreeVars $ io then return io else throwError . strMsg $ "Open vars in abduced examples!") `catchError` \e -> throwError . strMsg $ "Insufficient suport in examples!" ++ show e where args = butIthArg i $ crul cr carg = ithArg i $ crul cr headTail :: (Monad m) => TExp -> m (TExp,TExp) -- headTail [TVarE x t@(AppT ListT et)] = Just (TVarE (mkName "x") et, TVarE (mkName "xs") t) headTail e = case unfoldTAppE e of [TConE n _, x, xs] -> if isCons n then return (x, xs) else fail "headTail: No list!" _ -> fail "headTail: No list!"