#if __GLASGOW_HASKELL__ >= 710
#endif
module Agda.Termination.Inlining
( inlineWithClauses
, isWithFunction
, expandWithFunctionCall ) where
import Control.Applicative
import Control.Monad.State
import Data.Traversable (traverse)
import Data.List as List
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 [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" 70 $ sep
[ text "Found with (raw):", nest 2 $ text $ show cl ]
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" 70 $ vcat $
text "withExprClauses (raw)" : map (nest 2 . text . show) cs1
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" 70 $ vcat $
text "inlinedClauses (raw)" : map (nest 2 . text . show) cs2
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
reportSDoc "term.with.inline" 70 $ text "inlining (raw) =" <+> text (show wcl)
let vs = clauseArgs wcl
Just disp <- displayForm wf vs
reportSDoc "term.with.inline" 70 $ text "display form (raw) =" <+> text (show disp)
reportSDoc "term.with.inline" 40 $ text "display form =" <+> prettyTCM disp
(pats, perm) <- dispToPats disp
let body = rebindBody (permRange perm) $
applySubst (renamingR perm) .
applySubst (renaming $ reverseP $ clausePerm wcl)
<$> clauseBody wcl
return wcl { namedClausePats = numberPatVars perm 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 _ es) ws zs) = do
let es' = es ++ map Apply (map 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 (Proj d) = defaultNamedArg $ ProjP d
dtermToPat :: DisplayTerm -> StateT (Int, [(Int, Int)]) TCM Pattern
dtermToPat v =
case v of
DWithApp{} -> __IMPOSSIBLE__
DCon c vs -> ConP c noConPatternInfo . map (fmap unnamed)
<$> mapM (traverse dtermToPat) vs
DDef d es -> do
ifM (return (null es) `and2M` do isJust <$> lift (isProjection d))
(return $ ProjP 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 vs) -> ConP c noConPatternInfo . 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
as <- displayFormArities f
case as of
[a] | length vs >= a -> do
Just disp <- displayForm f vs
return $ dtermToTerm disp `applyE` es'
[a] | null es' -> do
let pad = a length vs
vs' = raise pad vs ++ map (defaultArg . var) (downFrom pad)
Just disp <- displayForm f vs'
return $ foldr (\_ -> Lam defaultArgInfo . Abs "") (dtermToTerm disp) (replicate pad ())
_ -> __IMPOSSIBLE__
where
(vs, es') = splitApplyElims es