diff --git a/Nemesis b/Nemesis --- a/Nemesis +++ b/Nemesis @@ -15,11 +15,16 @@ , "log" ] - - - desc "prepare cabal dist" - task "dist" $ do + task "dist" - do sh "cabal clean" sh "cabal configure" sh "cabal sdist" + + desc "run hello" + task "hello" - do + sh "src/Hello" + + desc "run hello2" + task "hello2" - do + sh "src/Hello2" diff --git a/chu2.cabal b/chu2.cabal --- a/chu2.cabal +++ b/chu2.cabal @@ -1,5 +1,5 @@ Name: chu2 -Version: 2012.11.17.2 +Version: 2012.11.18 Build-type: Simple Synopsis: FFI for Chu2 Agda Web Server Interface Description: @@ -18,9 +18,12 @@ Nemesis Guardfile src/Chu2.agda - src/Hello.agda src/Chu2/ByteString.agda src/Chu2/Handler/SnapServer.agda + src/Hello.agda + src/Hello2.agda + src/Chu2/Middleware/SimpleLogger.agda + src/Chu2/Middleware/SimpleLoggerFFI.hs library diff --git a/readme.md b/readme.md --- a/readme.md +++ b/readme.md @@ -1,29 +1,49 @@ -Example Chu2 Application in Agda -================================== +Chu2 Agda Web Server Interface +=============================== -```agda +## hello world example +```agda module Hello where open import IO.Primitive using (return) open import Data.List using ([]) open import Chu2.ByteString using (pack) open import Function using (_$_; const) -open import Chu2 +open import Chu2 using (response; OK; Application) hello-world-response = response OK [] (pack "Hello Agda!") hello-world-app : Application hello-world-app = const $ return hello-world-response -open import Chu2.Handler.SnapServer -main = onPort 3000 run $ chu2 hello-world-app +open import Chu2.Handler.SnapServer using (on-port_run) +main = on-port 3000 run hello-world-app +``` +## Using Middleware +```agda +module Hello2 where + +-- simple-logger middleware +open import Chu2.Middleware.SimpleLogger using (simple-logger) + +open import IO.Primitive using (return) +open import Function using (const) +open import Chu2 using (Application; defaultResponse; RawMiddleware) + +-- https://github.com/nfjinjing/gumi +open import Gumi.Light using (_-_) + +hello-world-app : Application +hello-world-app = const - return defaultResponse + +open import Chu2.Handler.SnapServer using (on-port_run) +main = on-port 3001 run - simple-logger hello-world-app ``` -Note -==== +## Note * need the Agda standard library: * need to read the Agda tutorial and be able to run Agda script from emacs: diff --git a/src/Chu2.agda b/src/Chu2.agda --- a/src/Chu2.agda +++ b/src/Chu2.agda @@ -8,6 +8,7 @@ data Tuple (A : Set)(B : Set) : Set where _,_ : A → B → Tuple A B + {-# IMPORT Chu2.FFI #-} {-# COMPILED_DATA Tuple (,) (,) #-} @@ -51,28 +52,27 @@ ServerName = ByteString ServerPort = ByteString HttpHeaders = Headers -Chu2Version = ByteString Chu2Input = ByteString Chu2Errors = ByteString → IO Unit Chu2Headers = Headers -data EnvData : Set where - envData : - RequestMethod - → ScriptName - → PathInfo - → QueryString - → ServerName - → ServerPort - → HttpHeaders - → Chu2Version - → Chu2UrlScheme - → Chu2Input - → Chu2Errors - → Chu2Headers - → EnvData +private + data EnvData : Set where + envData : + RequestMethod + → ScriptName + → PathInfo + → QueryString + → ServerName + → ServerPort + → HttpHeaders + → Chu2UrlScheme + → Chu2Input + → Chu2Errors + → Chu2Headers + → EnvData -{-# COMPILED_DATA EnvData Chu2.FFI.Env Chu2.FFI.Env #-} + {-# COMPILED_DATA EnvData Chu2.FFI.Env Chu2.FFI.Env #-} record Env : Set where constructor env @@ -84,16 +84,30 @@ serverName : ServerName serverPort : ServerPort httpHeaders : HttpHeaders - chu2Version : Chu2Version chu2UrlScheme : Chu2UrlScheme chu2Input : Chu2Input chu2Errors : Chu2Errors chu2Headers : Chu2Headers - -envDataToEnv : EnvData → Env -envDataToEnv - ( envData + +private + envDataToEnv : EnvData → Env + envDataToEnv + ( envData + requestMethod + scriptName + pathInfo + queryString + serverName + serverPort + httpHeaders + chu2UrlScheme + chu2Input + chu2Errors + chu2Headers + ) = + + env requestMethod scriptName pathInfo @@ -101,28 +115,41 @@ serverName serverPort httpHeaders - chu2Version chu2UrlScheme chu2Input chu2Errors chu2Headers - ) = - - env - requestMethod - scriptName - pathInfo - queryString - serverName - serverPort - httpHeaders - chu2Version - chu2UrlScheme - chu2Input - chu2Errors - chu2Headers + envToEnvData : Env → EnvData + envToEnvData + ( env + requestMethod + scriptName + pathInfo + queryString + serverName + serverPort + httpHeaders + chu2UrlScheme + chu2Input + chu2Errors + chu2Headers + ) = + + envData + requestMethod + scriptName + pathInfo + queryString + serverName + serverPort + httpHeaders + chu2UrlScheme + chu2Input + chu2Errors + chu2Headers + data Status : Set where OK : Status Created : Status @@ -176,14 +203,15 @@ Body = ByteString -data ResponseData : Set where - responseData : - Status - → Headers - → Body - → ResponseData +private + data ResponseData : Set where + responseData : + Status + → Headers + → Body + → ResponseData -{-# COMPILED_DATA ResponseData Chu2.FFI.Response Chu2.FFI.Response #-} + {-# COMPILED_DATA ResponseData Chu2.FFI.Response Chu2.FFI.Response #-} record Response : Set where @@ -193,20 +221,33 @@ headers : Headers body : Body -responseToResponseData : Response → ResponseData -responseToResponseData - ( response +private + responseToResponseData : Response → ResponseData + responseToResponseData + ( response + status + headers + body + ) = + + responseData status headers body - ) = - - responseData - status - headers - body - + + responseDataToResponse : ResponseData → Response + responseDataToResponse + ( responseData + status + headers + body + ) = + + response + status + headers + body defaultResponse : Response defaultResponse = @@ -217,15 +258,35 @@ ; body = pack "Chu2!" } -ApplicationData = EnvData → IO ResponseData -MiddlewareData = ApplicationData → ApplicationData - Application = Env → IO Response Middleware = Application → Application -Handler = ApplicationData → IO Unit +private + RawApplication = EnvData → IO ResponseData -open IO.Primitive using (_>>=_; return) +RawMiddleware = RawApplication → RawApplication -chu2 : Application → ApplicationData -chu2 app = λ aEnvData → app (envDataToEnv aEnvData) >>= λ aResponse → return (responseToResponseData aResponse) +private + open IO.Primitive using (_>>=_; return) + applicationToRawApplication : Application → RawApplication + applicationToRawApplication app = + λ aEnvData → app (envDataToEnv aEnvData) >>= λ aResponse → return (responseToResponseData aResponse) + + rawApplicationToApplication : RawApplication → Application + rawApplicationToApplication rawApp = + λ aEnv → rawApp (envToEnvData aEnv) >>= λ aRawResponse → return (responseDataToResponse aRawResponse) + + +Handler = Application → IO Unit +RawHandler = RawApplication → IO Unit + +open import Function using (_∘_; _$_; id) + + +rawHandlerToHandler : RawHandler → Handler +rawHandlerToHandler h = h ∘ applicationToRawApplication + + + +rawMiddlewareToMiddleware : RawMiddleware → Middleware +rawMiddlewareToMiddleware r app = rawApplicationToApplication $ r $ applicationToRawApplication app diff --git a/src/Chu2/FFI.hs b/src/Chu2/FFI.hs --- a/src/Chu2/FFI.hs +++ b/src/Chu2/FFI.hs @@ -61,7 +61,6 @@ , serverName :: ByteString , serverPort :: ByteString , httpHeaders :: Headers - , chu2Version :: ByteString , chu2UrlScheme :: Chu2UrlScheme , chu2Input :: ByteString , chu2Errors :: Chu2Errors diff --git a/src/Chu2/Handler/SnapServer.agda b/src/Chu2/Handler/SnapServer.agda --- a/src/Chu2/Handler/SnapServer.agda +++ b/src/Chu2/Handler/SnapServer.agda @@ -1,24 +1,27 @@ module Chu2.Handler.SnapServer where -open import Chu2 using (Handler) +open import Chu2 using (Handler; RawHandler; rawHandlerToHandler; RawMiddleware) private postulate Integer : Set - onPort_run' : Integer → Handler + onPort_run : Integer → RawHandler {-# BUILTIN INTEGER Integer #-} {-# COMPILED_TYPE Integer Integer #-} {-# IMPORT Chu2.Handler.SnapServerFFI #-} -{-# COMPILED onPort_run' Chu2.Handler.SnapServerFFI.onPort_run #-} +{-# COMPILED onPort_run Chu2.Handler.SnapServerFFI.onPort_run #-} open import Data.Nat using (ℕ) primitive primNatToInteger : ℕ -> Integer -onPort_run : ℕ → Handler -onPort_run port = onPort_run' (primNatToInteger port) - +open import Function using (_$_; id) +on-port_run : ℕ → Handler +on-port_run port = + let port-i = primNatToInteger port + in + rawHandlerToHandler (onPort_run port-i) 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 @@ -4,9 +4,11 @@ import Chu2.Interface.Hack2 import qualified Hack2.Handler.SnapServer as Snap import Data.Default +import qualified Hack2 as Hack2 -run :: Application -> IO () -run app = Snap.run (chu2ApplicationToHack2Application app) onPort_run :: Integer -> Application -> IO () -onPort_run port app = Snap.runWithConfig def {Snap.port = fromIntegral port} (chu2ApplicationToHack2Application app) +onPort_run port app = + Snap.runWithConfig + def {Snap.port = fromIntegral port} + (chu2ApplicationToHack2Application 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 @@ -2,87 +2,173 @@ import Data.ByteString (ByteString) import qualified Hack2 as Hack2 -import Data.ByteString.Char8 (pack) - +import Data.ByteString.Char8 (pack, unpack) +import Data.Default import Chu2.FFI -chu2RequestMethodFromHack2RequestMethod :: Hack2.RequestMethod -> RequestMethod -chu2RequestMethodFromHack2RequestMethod Hack2.OPTIONS = OPTIONS -chu2RequestMethodFromHack2RequestMethod Hack2.GET = GET -chu2RequestMethodFromHack2RequestMethod Hack2.HEAD = HEAD -chu2RequestMethodFromHack2RequestMethod Hack2.POST = POST -chu2RequestMethodFromHack2RequestMethod Hack2.PUT = PUT -chu2RequestMethodFromHack2RequestMethod Hack2.DELETE = DELETE -chu2RequestMethodFromHack2RequestMethod Hack2.TRACE = TRACE -chu2RequestMethodFromHack2RequestMethod Hack2.CONNECT = CONNECT +hack2RequestMethodToChu2RequestMethod :: Hack2.RequestMethod -> RequestMethod +hack2RequestMethodToChu2RequestMethod Hack2.OPTIONS = OPTIONS +hack2RequestMethodToChu2RequestMethod Hack2.GET = GET +hack2RequestMethodToChu2RequestMethod Hack2.HEAD = HEAD +hack2RequestMethodToChu2RequestMethod Hack2.POST = POST +hack2RequestMethodToChu2RequestMethod Hack2.PUT = PUT +hack2RequestMethodToChu2RequestMethod Hack2.DELETE = DELETE +hack2RequestMethodToChu2RequestMethod Hack2.TRACE = TRACE +hack2RequestMethodToChu2RequestMethod Hack2.CONNECT = CONNECT +chu2RequestMethodToHack2RequestMethod :: RequestMethod -> Hack2.RequestMethod +chu2RequestMethodToHack2RequestMethod OPTIONS = Hack2.OPTIONS +chu2RequestMethodToHack2RequestMethod GET = Hack2.GET +chu2RequestMethodToHack2RequestMethod HEAD = Hack2.HEAD +chu2RequestMethodToHack2RequestMethod POST = Hack2.POST +chu2RequestMethodToHack2RequestMethod PUT = Hack2.PUT +chu2RequestMethodToHack2RequestMethod DELETE = Hack2.DELETE +chu2RequestMethodToHack2RequestMethod TRACE = Hack2.TRACE +chu2RequestMethodToHack2RequestMethod CONNECT = Hack2.CONNECT -chu2UrlSchemeFromHack2UrlScheme :: Hack2.HackUrlScheme -> Chu2UrlScheme -chu2UrlSchemeFromHack2UrlScheme Hack2.HTTP = HTTP -chu2UrlSchemeFromHack2UrlScheme Hack2.HTTPS = HTTPS +hack2UrlSchemeToChu2UrlScheme :: Hack2.HackUrlScheme -> Chu2UrlScheme +hack2UrlSchemeToChu2UrlScheme Hack2.HTTP = HTTP +hack2UrlSchemeToChu2UrlScheme Hack2.HTTPS = HTTPS -chu2ErrorsFromHack2Errors :: Hack2.HackErrors -> Chu2Errors -chu2ErrorsFromHack2Errors = Hack2.unHackErrors +chu2UrlSchemeToHack2UrlScheme :: Chu2UrlScheme -> Hack2.HackUrlScheme +chu2UrlSchemeToHack2UrlScheme HTTP = Hack2.HTTP +chu2UrlSchemeToHack2UrlScheme HTTPS = Hack2.HTTPS -chu2EnvFromHack2Env :: Hack2.Env -> Env -chu2EnvFromHack2Env e = +hack2ErrorsToChu2Errors :: Hack2.HackErrors -> Chu2Errors +hack2ErrorsToChu2Errors = Hack2.unHackErrors + +chu2ErrorsToHack2Errors :: Chu2Errors -> Hack2.HackErrors +chu2ErrorsToHack2Errors = Hack2.HackErrors + +hack2EnvToChu2Env :: Hack2.Env -> Env +hack2EnvToChu2Env e = Env { - requestMethod = chu2RequestMethodFromHack2RequestMethod $ Hack2.requestMethod e - , scriptName = Hack2.scriptName e - , pathInfo = Hack2.pathInfo e - , queryString = Hack2.queryString e - , serverName = Hack2.serverName e - , serverPort = pack $ show $ Hack2.serverPort 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 = Hack2.hackHeaders e + requestMethod = hack2RequestMethodToChu2RequestMethod $ Hack2.requestMethod e + , scriptName = Hack2.scriptName e + , pathInfo = Hack2.pathInfo e + , queryString = Hack2.queryString e + , serverName = Hack2.serverName e + , serverPort = pack $ show $ Hack2.serverPort e + , httpHeaders = Hack2.httpHeaders e + , chu2UrlScheme = hack2UrlSchemeToChu2UrlScheme $ Hack2.hackUrlScheme e + , chu2Input = Hack2.hackInput e + , chu2Errors = hack2ErrorsToChu2Errors $ Hack2.hackErrors e + , chu2Headers = Hack2.hackHeaders e } - +chu2EnvToHack2Env :: Env -> Hack2.Env +chu2EnvToHack2Env e = + def + { + Hack2.requestMethod = chu2RequestMethodToHack2RequestMethod $ requestMethod e + , Hack2.scriptName = scriptName e + , Hack2.pathInfo = pathInfo e + , Hack2.queryString = queryString e + , Hack2.serverName = serverName e + , Hack2.serverPort = read $ unpack $ serverPort e + , Hack2.httpHeaders = httpHeaders e + , Hack2.hackUrlScheme = chu2UrlSchemeToHack2UrlScheme $ chu2UrlScheme e + , Hack2.hackInput = chu2Input e + , Hack2.hackErrors = chu2ErrorsToHack2Errors $ chu2Errors e + , Hack2.hackHeaders = chu2Headers e + } + + + +showStatus :: Status -> Int +showStatus OK = 200 +showStatus Created = 201 +showStatus Accepted = 202 +showStatus NoContent = 204 +showStatus MultipleChoices = 300 +showStatus MovedPermanently = 301 +showStatus SeeOther = 303 +showStatus NotModified = 304 +showStatus MovedTemporarily = 307 +showStatus BadRequest = 400 +showStatus Unauthorized = 401 +showStatus Forbidden = 403 +showStatus NotFound = 404 +showStatus MethodNotAllowed = 405 +showStatus NotAcceptable = 406 +showStatus Conflict = 409 +showStatus Gone = 410 +showStatus PreconditionFailed = 412 +showStatus RequestEntityTooLarge = 413 +showStatus RequestURItooLong = 414 +showStatus UnsupportedMediaType = 415 +showStatus NotImplemented = 501 +showStatus ServiceUnavailable = 503 + + +readStatus :: Int -> Status +readStatus 200 = OK +readStatus 201 = Created +readStatus 202 = Accepted +readStatus 204 = NoContent +readStatus 300 = MultipleChoices +readStatus 301 = MovedPermanently +readStatus 303 = SeeOther +readStatus 304 = NotModified +readStatus 307 = MovedTemporarily +readStatus 400 = BadRequest +readStatus 401 = Unauthorized +readStatus 403 = Forbidden +readStatus 404 = NotFound +readStatus 405 = MethodNotAllowed +readStatus 406 = NotAcceptable +readStatus 409 = Conflict +readStatus 410 = Gone +readStatus 412 = PreconditionFailed +readStatus 413 = RequestEntityTooLarge +readStatus 414 = RequestURItooLong +readStatus 415 = UnsupportedMediaType +readStatus 501 = NotImplemented +readStatus 503 = ServiceUnavailable +readStatus _ = ServiceUnavailable + + chu2ResponseToHack2Response :: Response -> Hack2.Response chu2ResponseToHack2Response r = Hack2.Response { Hack2.status = showStatus $ status r - , Hack2.headers = headers r - , Hack2.body = body r + , Hack2.headers = headers r + , Hack2.body = body r } -showStatus :: Status -> Int -showStatus OK = 200 -showStatus Created = 201 -showStatus Accepted = 202 -showStatus NoContent = 204 -showStatus MultipleChoices = 300 -showStatus MovedPermanently = 301 -showStatus SeeOther = 303 -showStatus NotModified = 304 -showStatus MovedTemporarily = 307 -showStatus BadRequest = 400 -showStatus Unauthorized = 401 -showStatus Forbidden = 403 -showStatus NotFound = 404 -showStatus MethodNotAllowed = 405 -showStatus NotAcceptable = 406 -showStatus Conflict = 409 -showStatus Gone = 410 -showStatus PreconditionFailed = 412 -showStatus RequestEntityTooLarge = 413 -showStatus RequestURItooLong = 414 -showStatus UnsupportedMediaType = 415 -showStatus NotImplemented = 501 -showStatus ServiceUnavailable = 503 +hack2ResponseToHack2Response :: Hack2.Response -> Response +hack2ResponseToHack2Response r = + Response + { + status = readStatus $ Hack2.status r + , headers = Hack2.headers r + , body = Hack2.body r + } + + + type Application = Env -> IO Response +type Middleware = Application -> Application chu2ApplicationToHack2Application :: Application -> Hack2.Application chu2ApplicationToHack2Application app = \hack2Env -> do - chu2Response <- app (chu2EnvFromHack2Env hack2Env) + chu2Response <- app (hack2EnvToChu2Env hack2Env) return (chu2ResponseToHack2Response chu2Response) +hack2ApplicationToChu2Application :: Hack2.Application -> Application +hack2ApplicationToChu2Application hack2App = \env -> do + hack2Response <- hack2App (chu2EnvToHack2Env env) + return (hack2ResponseToHack2Response hack2Response) +hack2MiddlewareToChu2Middleware :: Hack2.Middleware -> Middleware +hack2MiddlewareToChu2Middleware h2m app = + let hackApp = h2m $ chu2ApplicationToHack2Application app + in + + hack2ApplicationToChu2Application hackApp + + diff --git a/src/Chu2/Middleware/SimpleLogger.agda b/src/Chu2/Middleware/SimpleLogger.agda new file mode 100644 --- /dev/null +++ b/src/Chu2/Middleware/SimpleLogger.agda @@ -0,0 +1,13 @@ +module Chu2.Middleware.SimpleLogger where + +open import Chu2 using (rawMiddlewareToMiddleware; RawMiddleware; Middleware) + +private + postulate + raw-simple-logger : RawMiddleware + +{-# IMPORT Chu2.Middleware.SimpleLoggerFFI #-} +{-# COMPILED raw-simple-logger Chu2.Middleware.SimpleLoggerFFI.simple_logger #-} + +simple-logger : Middleware +simple-logger = rawMiddlewareToMiddleware raw-simple-logger diff --git a/src/Chu2/Middleware/SimpleLoggerFFI.hs b/src/Chu2/Middleware/SimpleLoggerFFI.hs new file mode 100644 --- /dev/null +++ b/src/Chu2/Middleware/SimpleLoggerFFI.hs @@ -0,0 +1,18 @@ + +-- require: cabal install hack2-contrib + +module Chu2.Middleware.SimpleLoggerFFI where + +import Hack2.Contrib.Middleware.SimpleAccessLogger +import Hack2.Contrib.Middleware.XForwardedForToRemoteHost +import Hack2.Contrib.Middleware.ContentLength +import Hack2.Contrib.Utils + +import Chu2.Interface.Hack2 + +simple_logger = hack2MiddlewareToChu2Middleware $ use + [ + x_forwarded_for_to_remote_host + , simple_access_logger Nothing + , content_length + ] diff --git a/src/Hello.agda b/src/Hello.agda --- a/src/Hello.agda +++ b/src/Hello.agda @@ -4,12 +4,12 @@ open import Data.List using ([]) open import Chu2.ByteString using (pack) open import Function using (_$_; const) -open import Chu2 +open import Chu2 using (response; OK; Application) hello-world-response = response OK [] (pack "Hello Agda!") hello-world-app : Application hello-world-app = const $ return hello-world-response -open import Chu2.Handler.SnapServer -main = onPort 3000 run $ chu2 hello-world-app +open import Chu2.Handler.SnapServer using (on-port_run) +main = on-port 3000 run hello-world-app diff --git a/src/Hello2.agda b/src/Hello2.agda new file mode 100644 --- /dev/null +++ b/src/Hello2.agda @@ -0,0 +1,17 @@ +module Hello2 where + +-- simple-logger middleware +open import Chu2.Middleware.SimpleLogger using (simple-logger) + +open import IO.Primitive using (return) +open import Function using (const) +open import Chu2 using (Application; defaultResponse; RawMiddleware) + +-- https://github.com/nfjinjing/gumi +open import Gumi.Light using (_-_) + +hello-world-app : Application +hello-world-app = const - return defaultResponse + +open import Chu2.Handler.SnapServer using (on-port_run) +main = on-port 3001 run - simple-logger hello-world-app