{-# LANGUAGE CPP #-}
module Agda.TypeChecking.Functions
( etaExpandClause
, getDef
) where
import Control.Arrow ( first )
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Monad.Base
import Agda.TypeChecking.Monad.Context
import Agda.TypeChecking.Monad.Debug
import Agda.TypeChecking.Monad.Options
import Agda.TypeChecking.Level
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.Utils.Impossible
import Agda.Utils.Functor ( ($>) )
import Agda.Utils.Pretty ( prettyShow )
import Agda.Utils.Monad
import Agda.Utils.Size
#include "undefined.h"
etaExpandClause :: MonadTCM tcm => Clause -> tcm Clause
etaExpandClause clause = liftTCM $ do
case clause of
Clause _ _ ctel ps _ Nothing _ _ -> return clause
Clause _ _ ctel ps Nothing (Just t) _ _ -> return clause
Clause rl rf ctel ps (Just body) (Just t) catchall unreachable -> do
TelV tel0 t' <- telView $ unArg t
let xs = peekLambdas body
let ltel = useNames xs $ telToList tel0
let tel = telFromList ltel
let n = size tel
unless (n == size tel0) __IMPOSSIBLE__
let ctel' = telFromList $ telToList ctel ++ ltel
ps' = raise n ps ++ teleNamedArgs tel
body' = raise n body `apply` teleArgs tel
reportSDoc "term.clause.expand" 30 $ inTopContext $ vcat
[ text "etaExpandClause"
, text " body = " <+> (addContext ctel' $ prettyTCM body)
, text " xs = " <+> text (prettyShow xs)
, text " new tel = " <+> prettyTCM ctel'
]
return $ Clause rl rf ctel' ps' (Just body') (Just (t $> t')) catchall unreachable
where
peekLambdas :: Term -> [Arg ArgName]
peekLambdas v =
case v of
Lam info b -> Arg info (absName b) : peekLambdas (unAbs b)
_ -> []
useNames :: [Arg ArgName] -> ListTel -> ListTel
useNames [] tel = map (setOrigin Inserted) tel
useNames (_:_) [] = []
useNames (x:xs) (dom:tel)
| sameHiding x dom =
fmap (first $ const $ unArg x) dom : useNames xs tel
| otherwise =
setOrigin Inserted dom : useNames (x:xs) tel
getDef :: Term -> TCM (Maybe QName)
getDef t = reduce t >>= \case
Def d _ -> return $ Just d
Lam _ v -> underAbstraction_ v getDef
Level v -> getDef =<< reallyUnLevelView v
DontCare v -> getDef v
_ -> return Nothing