chu2 2012.11.17.2 → 2012.11.18

raw patch · 12 files changed

+374/−147 lines, 12 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Nemesis +9/−4
• chu2.cabal +5/−2
• readme.md +28/−8
• src/Chu2.agda +123/−62
• src/Chu2/FFI.hs +0/−1
• src/Chu2/Handler/SnapServer.agda +9/−6
• src/Chu2/Handler/SnapServerFFI.hs +5/−3
• src/Chu2/Interface/Hack2.hs +144/−58
• src/Chu2/Middleware/SimpleLogger.agda +13/−0
• src/Chu2/Middleware/SimpleLoggerFFI.hs +18/−0
• src/Hello.agda +3/−3
• src/Hello2.agda +17/−0

@@ -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"

@@ -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

@@ -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: <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>

@@ -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

@@ -61,7 +61,6 @@   ,  serverName     :: ByteString   ,  serverPort     :: ByteString   ,  httpHeaders    :: Headers-  ,  chu2Version    :: ByteString   ,  chu2UrlScheme  :: Chu2UrlScheme   ,  chu2Input      :: ByteString   ,  chu2Errors     :: Chu2Errors

@@ -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)

@@ -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)

@@ -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+  +  

@@ -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

@@ -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+  ]

@@ -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

@@ -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