module Agda.Compiler.Treeless.DelayCoinduction where
import Control.Applicative
import Agda.Syntax.Internal (Type)
import Agda.Syntax.Abstract.Name (QName)
import Agda.Syntax.Treeless
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Reduce ( instantiateFull, normalise )
import Agda.TypeChecking.Substitute hiding (underLambdas)
import Agda.TypeChecking.Telescope
import Agda.Compiler.Treeless.Subst
import Agda.Utils.Impossible
#include "undefined.h"
delayCoinduction :: TTerm -> Type -> TCM TTerm
delayCoinduction t ty = do
kit <- coinductionKit
case kit of
Just kit -> transform kit t ty
Nothing -> return t
transform :: CoinductionKit -> TTerm -> Type -> TCM TTerm
transform kit t ty = do
isInf <- outputIsInf (Just kit) ty
if isInf then do
ty <- normalise ty
TelV tel _ <- telView ty
return $ underLambdas (length $ telToList tel) (TLam . raise 1) t
else
return t
outputIsInf :: Maybe CoinductionKit -> Type -> TCM Bool
outputIsInf kit ty = do
ty <- normalise ty
tn <- getOutputTypeName ty
case tn of
OutputTypeName tn -> return $ Just tn == (nameOfInf <$> kit)
_ -> return False
underLambdas :: Int -> (TTerm -> TTerm) -> TTerm -> TTerm
underLambdas n cont v = loop n v where
loop 0 v = cont v
loop n v = case v of
TLam b -> TLam $ loop (n1) b
_ -> __IMPOSSIBLE__