summaryrefslogtreecommitdiff
path: root/src/full/Agda/Compiler/Treeless/DelayCoinduction.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Compiler/Treeless/DelayCoinduction.hs')
-rw-r--r--src/full/Agda/Compiler/Treeless/DelayCoinduction.hs69
1 files changed, 69 insertions, 0 deletions
diff --git a/src/full/Agda/Compiler/Treeless/DelayCoinduction.hs b/src/full/Agda/Compiler/Treeless/DelayCoinduction.hs
new file mode 100644
index 0000000..6ed21e4
--- /dev/null
+++ b/src/full/Agda/Compiler/Treeless/DelayCoinduction.hs
@@ -0,0 +1,69 @@
+{-# LANGUAGE CPP #-}
+-- | Inserts an additional lambda into all coinductive auxiliary definitions (== target type Inf XX). E.g.:
+--
+-- f : A -> B -> C -> Inf A
+-- f = \a b c -> body
+-- is converted to
+-- f = \a b c _ -> body
+--
+-- Assumes that flat/sharp are implemented as follows:
+--
+-- flat = \x -> x
+-- sharp = \x -> x ()
+
+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
+ -- insert additional lambda
+ 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 (n-1) b
+ _ -> __IMPOSSIBLE__