diff --git a/chu2.cabal b/chu2.cabal --- a/chu2.cabal +++ b/chu2.cabal @@ -1,5 +1,5 @@ Name: chu2 -Version: 2012.11.16.1 +Version: 2012.11.17 Build-type: Simple Synopsis: FFI for Chu2 Agda Web Server Interface Description: @@ -24,7 +24,7 @@ library build-depends: - base >= 4 && < 5 + base >= 4 && < 6 , bytestring , hack2 , hack2-handler-snap-server diff --git a/readme.md b/readme.md --- a/readme.md +++ b/readme.md @@ -5,25 +5,26 @@ module Hello where -import IO.Primitive as Prim -open import Chu2 -open import Foreign.Haskell -open import Data.List -open import Chu2.ByteString +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) -{-# IMPORT Chu2.Handler.SnapServerFFI #-} +open import Chu2 postulate - runChu2 : Application -> Prim.IO Unit + run : ApplicationData → IO Unit -{-# COMPILED runChu2 Chu2.Handler.SnapServerFFI.runChu2 #-} +{-# IMPORT Chu2.Handler.SnapServerFFI #-} +{-# COMPILED run Chu2.Handler.SnapServerFFI.run #-} -hello_world_response = response OK [] (pack "Hello Agda!") +hello-world-response = response OK [] (pack "Hello Agda!") -hello_world_app : Application -hello_world_app = \_ -> Prim.return hello_world_response +hello-world-app : Application +hello-world-app = const $ return hello-world-response -main = runChu2 hello_world_app +main = run $ chu2 hello-world-app ``` diff --git a/src/Chu2.agda b/src/Chu2.agda --- a/src/Chu2.agda +++ b/src/Chu2.agda @@ -5,17 +5,16 @@ open import Data.List open import Foreign.Haskell open import Data.String -open import IO open import Chu2.ByteString import IO.Primitive as Prim - +data Tuple (A : Set)(B : Set) : Set where + _,_ : A → B → Tuple A B -data Header : Set where - _,_ : ByteString → ByteString → Header +{-# COMPILED_DATA Tuple (,) (,) #-} -{-# COMPILED_DATA Header Chu2.FFI.Header Chu2.FFI.Header #-} +Header = Tuple ByteString ByteString Headers = List Header @@ -72,16 +71,36 @@ Body = ByteString -data Response : Set where - response : +data ResponseData : Set where + responseData : Status → Headers → Body - → Response + → ResponseData -{-# COMPILED_DATA Response Chu2.FFI.Response Chu2.FFI.Response #-} +{-# COMPILED_DATA ResponseData Chu2.FFI.Response Chu2.FFI.Response #-} +record Response : Set where + constructor response + field + status : Status + headers : Headers + body : Body + +ResponseToResponseData : Response → ResponseData +ResponseToResponseData + ( response + status + headers + body + ) = + + responseData + status + headers + body + data RequestMethod : Set where HEAD GET PUT DELETE POST TRACE CONNECT OPTIONS : RequestMethod @@ -112,11 +131,11 @@ HttpHeaders = Headers Chu2Version = ByteString Chu2Input = ByteString -Chu2Errors = ByteString -> Prim.IO Unit +Chu2Errors = ByteString → Prim.IO Unit Chu2Headers = Headers -data Env : Set where - env : +data EnvData : Set where + envData : RequestMethod → ScriptName → PathInfo @@ -129,11 +148,64 @@ → Chu2Input → Chu2Errors → Chu2Headers - → Env + → EnvData + +{-# COMPILED_DATA EnvData Chu2.FFI.Env Chu2.FFI.Env #-} + +record Env : Set where + constructor env + field + requestMethod : RequestMethod + scriptName : ScriptName + pathInfo : PathInfo + queryString : QueryString + serverName : ServerName + serverPort : ServerPort + httpHeaders : HttpHeaders + chu2Version : Chu2Version + chu2UrlScheme : Chu2UrlScheme + chu2Input : Chu2Input + chu2Errors : Chu2Errors + chu2Headers : Chu2Headers + + +EnvDataToEnv : EnvData → Env +EnvDataToEnv + ( envData + requestMethod + scriptName + pathInfo + queryString + serverName + serverPort + httpHeaders + chu2Version + chu2UrlScheme + chu2Input + chu2Errors + chu2Headers + ) = + env + requestMethod + scriptName + pathInfo + queryString + serverName + serverPort + httpHeaders + chu2Version + chu2UrlScheme + chu2Input + chu2Errors + chu2Headers -{-# COMPILED_DATA Env Chu2.FFI.Env Chu2.FFI.Env #-} -Application = Env -> Prim.IO Response +Application = Env → Prim.IO Response +ApplicationData = EnvData → Prim.IO ResponseData +open Prim using (_>>=_; return) + +chu2 : Application → ApplicationData +chu2 app aEnvData = app (EnvDataToEnv aEnvData) >>= \aResponse → return (ResponseToResponseData aResponse) diff --git a/src/Chu2/FFI.hs b/src/Chu2/FFI.hs --- a/src/Chu2/FFI.hs +++ b/src/Chu2/FFI.hs @@ -3,10 +3,13 @@ import Data.ByteString (ByteString) import Data.ByteString.Char8 (pack) - +{- data Header = Header ByteString ByteString deriving (Show) - +-} + +type Header = (,) ByteString ByteString + data RequestMethod = OPTIONS | GET diff --git a/src/Chu2/Handler/SnapServerFFI.hs b/src/Chu2/Handler/SnapServerFFI.hs --- a/src/Chu2/Handler/SnapServerFFI.hs +++ b/src/Chu2/Handler/SnapServerFFI.hs @@ -2,7 +2,7 @@ import Chu2.FFI import Chu2.Interface.Hack2 -import Hack2.Handler.SnapServer +import qualified Hack2.Handler.SnapServer as Snap -runChu2 :: Application -> IO () -runChu2 app = run (chu2AppplicationToHack2Application app) +run :: Application -> IO () +run app = Snap.run (chu2AppplicationToHack2Application app) diff --git a/src/Chu2/Interface/Hack2.hs b/src/Chu2/Interface/Hack2.hs --- a/src/Chu2/Interface/Hack2.hs +++ b/src/Chu2/Interface/Hack2.hs @@ -24,8 +24,13 @@ chu2ErrorsFromHack2Errors :: Hack2.HackErrors -> Chu2Errors chu2ErrorsFromHack2Errors = Hack2.unHackErrors +{- +headerToTuple :: Header -> (ByteString, ByteString) +headerToTuple (Header x y) = (x,y) + tupleToHeader :: (ByteString, ByteString) -> Header tupleToHeader (x,y) = Header x y +-} chu2EnvFromHack2Env :: Hack2.Env -> Env chu2EnvFromHack2Env e = @@ -37,23 +42,21 @@ , queryString = Hack2.queryString e , serverName = Hack2.serverName e , serverPort = pack $ show $ Hack2.serverPort e - , httpHeaders = map tupleToHeader (Hack2.httpHeaders e) + , httpHeaders = Hack2.httpHeaders e , chu2Version = pack $ show $ Hack2.hackVersion e , chu2UrlScheme = chu2UrlSchemeFromHack2UrlScheme $ Hack2.hackUrlScheme e , chu2Input = Hack2.hackInput e , chu2Errors = chu2ErrorsFromHack2Errors $ Hack2.hackErrors e - , chu2Headers = map tupleToHeader (Hack2.hackHeaders e) + , chu2Headers = Hack2.hackHeaders e } -headerToTuple :: Header -> (ByteString, ByteString) -headerToTuple (Header x y) = (x,y) chu2ResponseToHack2Response :: Response -> Hack2.Response chu2ResponseToHack2Response r = Hack2.Response { Hack2.status = showStatus $ status r - , Hack2.headers = map headerToTuple (headers r) + , Hack2.headers = headers r , Hack2.body = body r } diff --git a/src/Hello.agda b/src/Hello.agda --- a/src/Hello.agda +++ b/src/Hello.agda @@ -1,21 +1,22 @@ module Hello where -import IO.Primitive as Prim -open import Chu2 -open import Foreign.Haskell -open import Data.List -open import Chu2.ByteString +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) -{-# IMPORT Chu2.Handler.SnapServerFFI #-} +open import Chu2 postulate - runChu2 : Application -> Prim.IO Unit + run : ApplicationData → IO Unit -{-# COMPILED runChu2 Chu2.Handler.SnapServerFFI.runChu2 #-} +{-# IMPORT Chu2.Handler.SnapServerFFI #-} +{-# COMPILED run Chu2.Handler.SnapServerFFI.run #-} -hello_world_response = response OK [] (pack "Hello Agda!") +hello-world-response = response OK [] (pack "Hello Agda!") -hello_world_app : Application -hello_world_app = \_ -> Prim.return hello_world_response +hello-world-app : Application +hello-world-app = const $ return hello-world-response -main = runChu2 hello_world_app +main = run $ chu2 hello-world-app