Add built-in support for Delay monad

lib/Haskell/Extra/Delay.agda

@@ -0,0 +1,9 @@
+{-# OPTIONS --sized-types #-}
+
+module Haskell.Extra.Delay where
+
+open import Haskell.Prim.Thunk
+
+data Delay (a : Set) (@0 i : Size) : Set where
+  now : a → Delay a i
+  later : Thunk (Delay a) i → Delay a i

src/Agda2Hs/Compile/Term.hs

@@ -63,6 +63,8 @@ isSpecialCon = prettyShow >>> \case
   "Haskell.Prim.Tuple._,_"         -> Just tupleTerm
   "Haskell.Prim.Tuple._×_×_._,_,_" -> Just tupleTerm
   "Haskell.Extra.Erase.Erased"     -> Just (\_ _ _ -> erasedTerm)
+  "Haskell.Extra.Delay.Delay.now"   -> Just $ \_ _ -> compileErasedApp
+  "Haskell.Extra.Delay.Delay.later" -> Just $ \_ _ -> compileErasedApp
   _ -> Nothing
 
 tupleTerm :: ConHead -> ConInfo -> Elims -> C (Hs.Exp ())

src/Agda2Hs/Compile/Type.hs

@@ -44,6 +44,7 @@ isSpecialType = prettyShow >>> \case
   "Haskell.Prim.Tuple._×_"   -> Just tupleType
   "Haskell.Prim.Tuple._×_×_" -> Just tupleType
   "Haskell.Extra.Erase.Erase" -> Just erasedType
+  "Haskell.Extra.Delay.Delay" -> Just delayType
   _ -> Nothing
 
 tupleType :: QName -> Elims -> C (Hs.Type ())
@@ -55,6 +56,12 @@ tupleType q es = do
 erasedType :: QName -> Elims -> C (Hs.Type ())
 erasedType _ _ = return $ Hs.TyTuple () Hs.Boxed []
 
+delayType :: QName -> Elims -> C (Hs.Type ())
+delayType _ (Apply a : _) = compileType (unArg a)
+delayType _ (_ : _) = __IMPOSSIBLE__
+delayType _ [] = genericDocError =<< text "Cannot compile unapplied Delay type"
+
+
 -- | Add a class constraint to a Haskell type.
 constrainType
   :: Hs.Asst () -- ^ The class assertion.

test/AllTests.agda

@@ -67,6 +67,7 @@ import Coerce
 import Inlining
 import EraseType
 import Issue257
+import Delay
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -133,4 +134,5 @@ import ModuleParametersImports
 import Coerce
 import Inlining
 import EraseType
+import Delay
 #-}

test/Delay.agda

@@ -0,0 +1,23 @@
+
+module Delay where
+
+open import Haskell.Prelude
+open import Haskell.Prim.Thunk
+open import Haskell.Extra.Delay
+
+open import Agda.Builtin.Size
+
+postulate
+  div : Int → Int → Int
+  mod : Int → Int → Int
+
+even : Int → Bool
+even x = mod x 2 == 0
+
+collatz : ∀ {@0 j} → Int → Delay Int j
+collatz x = 
+  if x == 0 then now 0
+  else if even x then later (λ where .force → collatz (div x 2))
+  else later λ where .force → collatz (3 * x + 1)
+
+{-# COMPILE AGDA2HS collatz #-}

test/golden/AllTests.hs

@@ -64,4 +64,5 @@ import ModuleParametersImports
 import Coerce
 import Inlining
 import EraseType
+import Delay
 

test/golden/Delay.hs

@@ -0,0 +1,7 @@
+module Delay where
+
+collatz :: Int -> Int
+collatz x
+  = if x == 0 then 0 else
+      if even x then collatz (div x 2) else collatz (3 * x + 1)
+