Example Chu2 Application in Agda

module Hello where

import IO.Primitive as Prim
open import Chu2
open import Foreign.Haskell
open import Data.List
open import Chu2.ByteString

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

postulate
  runChu2 : Application -> Prim.IO Unit

{-# COMPILED runChu2 Chu2.Handler.SnapServerFFI.runChu2 #-}

hello_world_response = response OK [] (pack "Hello Agda!")

hello_world_app : Application
hello_world_app = \_ -> Prim.return hello_world_response

main = runChu2 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