module Agda.Termination.Inlining
( inlineWithClauses
, isWithFunction
, expandWithFunctionCall ) where
import Control.Applicative
import Control.Monad.State
import Data.Maybe (fromMaybe)
import Data.Monoid
import Data.Foldable (foldMap)
import Data.Traversable (traverse)
import Data.List as List
import Agda.Syntax.Common hiding (NamedArg)
import Agda.Syntax.Internal
import Agda.Syntax.Internal.Pattern
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.DisplayForm
import Agda.TypeChecking.Telescope
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Permutation
import Agda.Utils.Size
import Agda.Utils.Impossible
#include "undefined.h"
inlineWithClauses :: QName -> Clause -> TCM [Clause]
inlineWithClauses f cl = inTopContext $ do
let noInline = return [cl]
body <- traverse instantiate $ getBodyUnraised cl
case body of
Just (Def wf els) ->
caseMaybeM (isWithFunction wf) noInline $ \ f' ->
if f /= f' then noInline else do
let args = fromMaybe __IMPOSSIBLE__ . allApplyElims $ els
reportSDoc "term.with.inline" 20 $ sep
[ text "Found with:", nest 2 $ prettyTCM $ QNamed f cl ]
t <- defType <$> getConstInfo wf
cs1 <- withExprClauses cl t args
reportSDoc "term.with.inline" 20 $ vcat $
text "withExprClauses" : map (nest 2 . prettyTCM . QNamed f) cs1
cs2 <- inlinedClauses f cl t wf
reportSDoc "term.with.inline" 20 $ vcat $
text "inlinedClauses" : map (nest 2 . prettyTCM . QNamed f) cs2
return $ cs1 ++ cs2
_ -> noInline
withExprClauses :: Clause -> Type -> Args -> TCM [Clause]
withExprClauses cl t args = loop t args where
loop t [] = return []
loop t (a:as) =
case unArg a of
Var i [] -> rest
v ->
(cl { clauseBody = v <$ clauseBody cl
, clauseType = Just $ defaultArg dom
} :) <$> rest
where
rest = loop (piApply t [a]) as
dom = case unEl t of
Pi a _ -> unDom a
_ -> __IMPOSSIBLE__
inlinedClauses :: QName -> Clause -> Type -> QName -> TCM [Clause]
inlinedClauses f cl t wf = do
wcs <- concat <$> (mapM (inlineWithClauses wf) =<< defClauses <$> getConstInfo wf)
reportSDoc "term.with.inline" 30 $ vcat $ text "With-clauses to inline" :
map (nest 2 . prettyTCM . QNamed wf) wcs
mapM (inline f cl t wf) wcs
inline :: QName -> Clause -> Type -> QName -> Clause -> TCM Clause
inline f pcl t wf wcl = inTopContext $ addCtxTel (clauseTel wcl) $ do
let vs = clauseArgs wcl
Just disp <- displayForm wf vs
(pats, perm) <- dispToPats disp
let body = rebindBody (permRange perm) $
applySubst (renamingR perm) .
applySubst (renaming $ reverseP $ clausePerm wcl)
<$> clauseBody wcl
return wcl { clausePerm = perm
, namedClausePats = pats
, clauseBody = body
, clauseType = Nothing
}
where
numVars = size (clauseTel wcl)
rebindBody n b = bind n $ maybe NoBody Body $ getBodyUnraised b
where
bind 0 = id
bind n = Bind . Abs (stringToArgName $ "h" ++ show n') . bind n'
where n' = n 1
dispToPats :: DisplayTerm -> TCM ([NamedArg Pattern], Permutation)
dispToPats (DWithApp (DDef _ vs) ws zs) = do
let us = vs ++ map defaultArg ws ++ map (fmap DTerm) zs
(ps, (j, ren)) <- (`runStateT` (0, [])) $
map (fmap unnamed) <$> mapM (traverse dtermToPat) us
let perm = Perm j (map snd $ List.sort ren)
return (ps, perm)
dispToPats t = __IMPOSSIBLE__
bindVar i = do
(j, is) <- get
let i' = numVars i 1
case lookup i' is of
Nothing -> True <$ put (j + 1, (i', j) : is)
Just{} -> False <$ put (j + 1, is)
skip = modify $ \(j, is) -> (j + 1, is)
dtermToPat v =
case v of
DWithApp{} -> __IMPOSSIBLE__
DCon c vs -> ConP c Nothing . map (fmap unnamed)
<$> mapM (traverse dtermToPat) vs
DDef{} -> DotP (dtermToTerm v) <$ skip
DDot v -> DotP v <$ skip
DTerm (Var i []) ->
ifM (bindVar i) (VarP . nameToPatVarName <$> lift (nameOfBV i))
(pure $ DotP (Var i []))
DTerm (Con c vs) -> ConP c Nothing . map (fmap unnamed) <$> mapM (traverse (dtermToPat . DTerm)) vs
DTerm v -> DotP v <$ skip
isWithFunction :: MonadTCM tcm => QName -> tcm (Maybe QName)
isWithFunction x = liftTCM $ do
def <- getConstInfo x
return $ case theDef def of
Function{ funWith = w } -> w
_ -> Nothing
expandWithFunctionCall :: QName -> Elims -> TCM Term
expandWithFunctionCall f es = do
Just disp <- displayForm f vs
return $ dtermToTerm disp `applyE` es'
where
(vs, es') = splitApplyElims es
dtermToTerm :: DisplayTerm -> Term
dtermToTerm (DWithApp d ds vs) = dtermToTerm d `apply` (map (defaultArg . dtermToTerm) ds ++ vs)
dtermToTerm (DCon c args) = Con c $ map (fmap dtermToTerm) args
dtermToTerm (DDef f args) = Def f $ map (Apply . fmap dtermToTerm) args
dtermToTerm (DDot v) = v
dtermToTerm (DTerm v) = v