chu2 2012.11.18.2 → 2012.11.19
raw patch · 8 files changed
+55/−58 lines, 8 filesdep +utf8-string
Dependencies added: utf8-string
Files
- Nemesis +5/−0
- chu2.cabal +2/−1
- readme.md +7/−8
- src/Chu2.agda +35/−34
- src/Chu2/FFI.hs +0/−1
- src/Chu2/Interface/Hack2.hs +0/−8
- src/Hello.agda +4/−4
- src/Hello2.agda +2/−2
Nemesis view
@@ -28,3 +28,8 @@ desc "run hello2" task "hello2" - do sh "src/Hello2"+ + + desc "bench"+ task "bench" - do+ sh "ab -n 10000 -c 100 http://0.0.0.0:3001/"
chu2.cabal view
@@ -1,5 +1,5 @@ Name: chu2-Version: 2012.11.18.2+Version: 2012.11.19 Build-type: Simple Synopsis: FFI for Chu2 Agda Web Server Interface Description:@@ -32,6 +32,7 @@ , hack2 , hack2-handler-snap-server , data-default+ , utf8-string hs-source-dirs: src/ exposed-modules:
readme.md view
@@ -6,19 +6,18 @@ ```agda module Hello where -open import IO.Primitive using (return)+open import IO using (run; return) open import Data.List using ([])-open import Chu2.ByteString using (pack)-open import Function using (_$_; const)+open import Function using (const) open import Chu2 using (response; OK; Application) -hello-world-response = response OK [] (pack "Hello Agda!")+hello-world-response = response OK [] ("Hello Agda!") hello-world-app : Application-hello-world-app = const $ return hello-world-response+hello-world-app = const (return hello-world-response) open import Chu2.Handler.SnapServer using (on-port_run)-main = on-port 3000 run hello-world-app+main = run (on-port 3000 run hello-world-app) ``` ## Using Middleware@@ -29,7 +28,7 @@ -- simple-logger middleware open import Chu2.Middleware.SimpleLogger using (simple-logger) -open import IO.Primitive using (return)+open import IO using (run; return) open import Function using (const) open import Chu2 using (Application; defaultResponse; RawMiddleware) @@ -40,7 +39,7 @@ 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+main = run - on-port 3001 run - simple-logger hello-world-app ``` ## Note
src/Chu2.agda view
@@ -2,18 +2,20 @@ open import Data.List using (List; [_]) open import Foreign.Haskell using (Unit)-open import IO.Primitive using (IO)+open import IO using (IO; run; lift; _>>=_; return; _>>_)+open import Data.Unit using (⊤)+import IO.Primitive as Prim open import Data.String using (String)+open import Coinduction using (♯_) data Tuple (A : Set)(B : Set) : Set where _,_ : A → B → Tuple A B - {-# IMPORT Chu2.FFI #-} {-# COMPILED_DATA Tuple (,) (,) #-} -Header = Tuple String String-+Field = String+Header = Tuple Field Field Headers = List Header data RequestMethod : Set where@@ -46,14 +48,13 @@ Chu2.FFI.HTTPS #-} -ScriptName = String-PathInfo = String-QueryString = String-ServerName = String-ServerPort = String+ScriptName = Field+PathInfo = Field+QueryField = Field+ServerName = Field+ServerPort = Field HttpHeaders = Headers-Chu2Input = String-Chu2Errors = String → IO Unit+Chu2Input = Field Chu2Headers = Headers private@@ -62,13 +63,12 @@ RequestMethod → ScriptName → PathInfo - → QueryString + → QueryField → ServerName → ServerPort → HttpHeaders → Chu2UrlScheme → Chu2Input - → Chu2Errors → Chu2Headers → EnvData @@ -80,13 +80,12 @@ requestMethod : RequestMethod scriptName : ScriptName pathInfo : PathInfo - queryString : QueryString + queryField : QueryField serverName : ServerName serverPort : ServerPort httpHeaders : HttpHeaders chu2UrlScheme : Chu2UrlScheme chu2Input : Chu2Input - chu2Errors : Chu2Errors chu2Headers : Chu2Headers @@ -97,13 +96,12 @@ requestMethod scriptName pathInfo - queryString + queryField serverName serverPort httpHeaders chu2UrlScheme chu2Input - chu2Errors chu2Headers ) = @@ -111,43 +109,39 @@ requestMethod scriptName pathInfo - queryString + queryField serverName serverPort httpHeaders chu2UrlScheme chu2Input - chu2Errors chu2Headers -+ envToEnvData : Env → EnvData envToEnvData ( env requestMethod scriptName pathInfo - queryString + queryField serverName serverPort httpHeaders chu2UrlScheme chu2Input - chu2Errors chu2Headers ) =- envData requestMethod scriptName pathInfo - queryString + queryField serverName serverPort httpHeaders chu2UrlScheme chu2Input - chu2Errors chu2Headers data Status : Set where@@ -201,7 +195,7 @@ Chu2.FFI.ServiceUnavailable #-} -Body = String+Body = Field private data ResponseData : Set where@@ -254,7 +248,7 @@ record { status = OK- ; headers = [("Content-Type", "text/plain")]+ ; headers = [("Content-Type", "text/plain; charset=utf-8")] ; body = "Chu2!" } @@ -262,29 +256,36 @@ Middleware = Application → Application private- RawApplication = EnvData → IO ResponseData+ RawApplication = EnvData → Prim.IO ResponseData RawMiddleware = RawApplication → RawApplication private- open IO.Primitive using (_>>=_; return)+ open import Function using (_$_)+ applicationToRawApplication : Application → RawApplication applicationToRawApplication app = - λ aEnvData → app (envDataToEnv aEnvData) >>= λ aResponse → return (responseToResponseData aResponse)+ λ aEnvData → run $+ ♯ app (envDataToEnv aEnvData) >>= λ aResponse →+ ♯ return (responseToResponseData aResponse) rawApplicationToApplication : RawApplication → Application rawApplicationToApplication rawApp = - λ aEnv → rawApp (envToEnvData aEnv) >>= λ aRawResponse → return (responseDataToResponse aRawResponse)+ λ aEnv → ♯ lift (rawApp (envToEnvData aEnv)) >>= λ aRawResponse → + ♯ return (responseDataToResponse aRawResponse) -Handler = Application → IO Unit-RawHandler = RawApplication → IO Unit+Handler = Application → IO ⊤+RawHandler = RawApplication → Prim.IO Unit open import Function using (_∘_; _$_; id) rawHandlerToHandler : RawHandler → Handler-rawHandlerToHandler h = h ∘ applicationToRawApplication+rawHandlerToHandler rawHandler app = + ♯ lift (rawHandler (applicationToRawApplication app)) >> + ♯ return _+
src/Chu2/FFI.hs view
@@ -63,7 +63,6 @@ , httpHeaders :: Headers , chu2UrlScheme :: Chu2UrlScheme , chu2Input :: Field- , chu2Errors :: Chu2Errors , chu2Headers :: Headers }
src/Chu2/Interface/Hack2.hs view
@@ -37,13 +37,7 @@ chu2UrlSchemeToHack2UrlScheme HTTP = Hack2.HTTP chu2UrlSchemeToHack2UrlScheme HTTPS = Hack2.HTTPS -hack2ErrorsToChu2Errors :: Hack2.HackErrors -> Chu2Errors-hack2ErrorsToChu2Errors io x = Hack2.unHackErrors io (f2b_Utf8Encoding x) -chu2ErrorsToHack2Errors :: Chu2Errors -> Hack2.HackErrors-chu2ErrorsToHack2Errors io = Hack2.HackErrors (\x -> io (b2f_Utf8Encoding x))-- f2b :: Field -> ByteString f2b = pack @@ -65,7 +59,6 @@ { requestMethod = hack2RequestMethodToChu2RequestMethod $ Hack2.requestMethod e , chu2UrlScheme = hack2UrlSchemeToChu2UrlScheme $ Hack2.hackUrlScheme e- , chu2Errors = hack2ErrorsToChu2Errors $ Hack2.hackErrors e , serverPort = show $ Hack2.serverPort e , scriptName = b2f $ Hack2.scriptName e , pathInfo = b2f $ Hack2.pathInfo e@@ -82,7 +75,6 @@ { Hack2.requestMethod = chu2RequestMethodToHack2RequestMethod $ requestMethod e , Hack2.hackUrlScheme = chu2UrlSchemeToHack2UrlScheme $ chu2UrlScheme e- , Hack2.hackErrors = chu2ErrorsToHack2Errors $ chu2Errors e , Hack2.serverPort = read $ serverPort e , Hack2.scriptName = f2b $ scriptName e , Hack2.pathInfo = f2b $ pathInfo e
src/Hello.agda view
@@ -1,14 +1,14 @@ module Hello where -open import IO.Primitive using (return)+open import IO using (run; return) open import Data.List using ([])-open import Function using (_$_; const)+open import Function using (const) open import Chu2 using (response; OK; Application) hello-world-response = response OK [] ("Hello Agda!") hello-world-app : Application-hello-world-app = const $ return hello-world-response+hello-world-app = const (return hello-world-response) open import Chu2.Handler.SnapServer using (on-port_run)-main = on-port 3000 run hello-world-app+main = run (on-port 3000 run hello-world-app)
src/Hello2.agda view
@@ -3,7 +3,7 @@ -- simple-logger middleware open import Chu2.Middleware.SimpleLogger using (simple-logger) -open import IO.Primitive using (return)+open import IO using (run; return) open import Function using (const) open import Chu2 using (Application; defaultResponse; RawMiddleware) @@ -14,4 +14,4 @@ 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+main = run - on-port 3001 run - simple-logger hello-world-app