{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.Termination.Inlining
( inlineWithClauses
, isWithFunction
, expandWithFunctionCall ) where
import Control.Monad.State
import qualified Data.List as List
import Data.Maybe
import Data.Traversable (traverse)
import Agda.Syntax.Common
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.List (downFrom)
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 (Maybe [Clause])
inlineWithClauses f cl = inTopContext $ do
let noInline = return Nothing
body <- fmap stripDontCare <$> instantiate (clauseBody cl)
case body of
Just (Def wf els) -> do
isWith <- isWithFunction wf
reportSDoc "term.with.inline" 20 $ sep
[ "inlineWithClauses: isWithFunction ="
, maybe "<none>" prettyTCM isWith
]
caseMaybe isWith noInline $ \ f' -> do
if f /= f' then noInline else do
let args = fromMaybe __IMPOSSIBLE__ . allApplyElims $ els
reportSDoc "term.with.inline" 70 $ sep
[ "Found with (raw):", nest 2 $ text $ show cl ]
reportSDoc "term.with.inline" 20 $ sep
[ "Found with:", nest 2 $ prettyTCM $ QNamed f cl ]
t <- defType <$> getConstInfo wf
cs1 <- withExprClauses cl t args
reportSDoc "term.with.inline" 70 $ vcat $
"withExprClauses (raw)" : map (nest 2 . text . show) cs1
reportSDoc "term.with.inline" 20 $ vcat $
"withExprClauses" : map (nest 2 . prettyTCM . QNamed f) cs1
cs2 <- inlinedClauses f cl t wf
reportSDoc "term.with.inline" 70 $ vcat $
"inlinedClauses (raw)" : map (nest 2 . text . show) cs2
reportSDoc "term.with.inline" 20 $ vcat $
"inlinedClauses" : map (nest 2 . prettyTCM . QNamed f) cs2
return $ Just $ cs1 ++ cs2
Just d -> do
reportSLn "term.with.inline" 20 $ "inlineWithClauses: clause body is not a Def"
reportSDoc "term.with.inline" 70 $ sep
[ "inlineWithClauses: clause body is not a Def but "
, (text . show) d
]
noInline
Nothing -> do
reportSLn "term.with.inline" 20 $ "inlineWithClauses: no clause body"
noInline
inlineWithClauses' :: QName -> Clause -> TCM [Clause]
inlineWithClauses' f cl = fromMaybe [cl] <$> inlineWithClauses f cl
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 = Just v
, 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 $ "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 $ addContext (clauseTel wcl) $ do
reportSDoc "term.with.inline" 70 $ "inlining (raw) =" <+> text (show wcl)
Just disp <- displayForm wf $ clauseElims wcl
reportSDoc "term.with.inline" 70 $ "display form (raw) =" <+> text (show disp)
reportSDoc "term.with.inline" 40 $ "display form =" <+> prettyTCM disp
(pats, perm) <- dispToPats disp
return wcl { namedClausePats = numberPatVars __IMPOSSIBLE__ perm pats }
where
numVars = size (clauseTel wcl)
dispToPats :: DisplayTerm -> TCM ([NamedArg Pattern], Permutation)
dispToPats (DWithApp (DDef _ es) ws zs) = do
let es' = es ++ map (Apply . defaultArg) ws ++ map (fmap DTerm) zs
(ps, (j, ren)) <- (`runStateT` (0, [])) $ mapM (traverse dtermToPat) es'
let perm = Perm j (map snd $ List.sort ren)
return (map ePatToPat 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)
ePatToPat :: Elim' Pattern -> NamedArg Pattern
ePatToPat (Apply p) = fmap unnamed p
ePatToPat (IApply x y p) = defaultNamedArg p
ePatToPat (Proj o d) = defaultNamedArg $ ProjP o d
dtermToPat :: DisplayTerm -> StateT (Int, [(Int, Int)]) TCM Pattern
dtermToPat v =
case v of
DWithApp{} -> __IMPOSSIBLE__
DCon c ci vs -> ConP c (toConPatternInfo ci) . map (fmap unnamed)
<$> mapM (traverse dtermToPat) vs
DDef d es -> do
ifM (return (null es) `and2M` do isJust <$> lift (isProjection d))
(return $ ProjP ProjPrefix d)
(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 ci vs) -> ConP c (toConPatternInfo ci) . map (fmap unnamed) <$>
mapM (traverse (dtermToPat . DTerm)) (fromMaybe __IMPOSSIBLE__ $ allApplyElims 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
as <- displayFormArities f
case as of
[a] | length es >= a -> do
Just disp <- displayForm f es
return $ dtermToTerm disp
[a] -> do
let pad = a - length es
es' = raise pad es ++ map (Apply . defaultArg . var) (downFrom pad)
Just disp <- displayForm f es'
let info = setOrigin Inserted defaultArgInfo
return $ foldr (\_ -> Lam info . Abs "") (dtermToTerm disp) (replicate pad ())
_ -> __IMPOSSIBLE__