Example Chu2 Application in Agda

module Hello where

open import IO.Primitive    using (IO; return)
open import Foreign.Haskell using (Unit)
open import Data.List       using ([])
open import Chu2.ByteString using (pack)
open import Function        using (_$_; const)

open import Chu2

postulate
  run : ApplicationData → IO Unit

{-# IMPORT Chu2.Handler.SnapServerFFI #-}
{-# COMPILED run Chu2.Handler.SnapServerFFI.run #-}

hello-world-response = response OK [] (pack "Hello Agda!")

hello-world-app : Application
hello-world-app = const $ return hello-world-response

main = run $ chu2 hello-world-app

Note

• need the Agda standard library: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary
• need to read the Agda tutorial and be able to run Agda script from emacs: http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf