diff --git a/chu2.cabal b/chu2.cabal --- a/chu2.cabal +++ b/chu2.cabal @@ -1,5 +1,5 @@ Name: chu2 -Version: 2012.11.19 +Version: 2012.11.20 Build-type: Simple Synopsis: FFI for Chu2 Agda Web Server Interface Description: @@ -18,11 +18,12 @@ Nemesis Guardfile src/Chu2.agda + src/Chu2/FFI.agda src/Chu2/Handler/SnapServer.agda - src/Hello.agda - src/Hello2.agda src/Chu2/Middleware/SimpleLogger.agda src/Chu2/Middleware/SimpleLoggerFFI.hs + src/Hello.agda + src/Hello2.agda library diff --git a/readme.md b/readme.md --- a/readme.md +++ b/readme.md @@ -6,7 +6,7 @@ ```agda module Hello where -open import IO using (run; return) +open import IO using (return) renaming (run to io) open import Data.List using ([]) open import Function using (const) open import Chu2 using (response; OK; Application) @@ -17,7 +17,7 @@ hello-world-app = const (return hello-world-response) open import Chu2.Handler.SnapServer using (on-port_run) -main = run (on-port 3000 run hello-world-app) +main = io (on-port 3000 run hello-world-app) ``` ## Using Middleware @@ -28,19 +28,23 @@ -- simple-logger middleware open import Chu2.Middleware.SimpleLogger using (simple-logger) -open import IO using (run; return) +open import IO using (return) renaming (run to io) open import Function using (const) -open import Chu2 using (Application; defaultResponse; RawMiddleware) +open import Chu2 using (Application; default-response) --- https://github.com/nfjinjing/gumi -open import Gumi.Light using (_-_) +default-app : Application +default-app = const (return default-response) -hello-world-app : Application -hello-world-app = const - return defaultResponse +app : Application +app = simple-logger default-app open import Chu2.Handler.SnapServer using (on-port_run) -main = run - on-port 3001 run - simple-logger hello-world-app +main = io (on-port 3001 run app) ``` + +## Full spec + +[`Chu2.agda`](https://github.com/nfjinjing/chu2/blob/master/src/Chu2.agda) ## Note diff --git a/src/Chu2.agda b/src/Chu2.agda --- a/src/Chu2.agda +++ b/src/Chu2.agda @@ -1,21 +1,15 @@ module Chu2 where open import Data.List using (List; [_]) -open import Foreign.Haskell using (Unit) -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 (♯_) +open import Data.Product using (Σ; _,_) -data Tuple (A : Set)(B : Set) : Set where - _,_ : A → B → Tuple A B -{-# IMPORT Chu2.FFI #-} -{-# COMPILED_DATA Tuple (,) (,) #-} +-- HTTP Field = String -Header = Tuple Field Field +KV = Σ Field (\_ → Field) +Header = KV Headers = List Header data RequestMethod : Set where @@ -29,24 +23,10 @@ CONNECT : RequestMethod -{-# COMPILED_DATA RequestMethod Chu2.FFI.RequestMethod - Chu2.FFI.OPTIONS - Chu2.FFI.GET - Chu2.FFI.HEAD - Chu2.FFI.POST - Chu2.FFI.PUT - Chu2.FFI.DELETE - Chu2.FFI.TRACE - Chu2.FFI.CONNECT -#-} data Chu2UrlScheme : Set where HTTP HTTPS : Chu2UrlScheme -{-# COMPILED_DATA Chu2UrlScheme Chu2.FFI.Chu2UrlScheme - Chu2.FFI.HTTP - Chu2.FFI.HTTPS -#-} ScriptName = Field PathInfo = Field @@ -57,23 +37,7 @@ Chu2Input = Field Chu2Headers = Headers -private - data EnvData : Set where - envData : - RequestMethod - → ScriptName - → PathInfo - → QueryField - → ServerName - → ServerPort - → HttpHeaders - → Chu2UrlScheme - → Chu2Input - → Chu2Headers - → EnvData - {-# COMPILED_DATA EnvData Chu2.FFI.Env Chu2.FFI.Env #-} - record Env : Set where constructor env field @@ -89,61 +53,6 @@ chu2Headers : Chu2Headers -private - envDataToEnv : EnvData → Env - envDataToEnv - ( envData - requestMethod - scriptName - pathInfo - queryField - serverName - serverPort - httpHeaders - chu2UrlScheme - chu2Input - chu2Headers - ) = - - env - requestMethod - scriptName - pathInfo - queryField - serverName - serverPort - httpHeaders - chu2UrlScheme - chu2Input - chu2Headers - - - envToEnvData : Env → EnvData - envToEnvData - ( env - requestMethod - scriptName - pathInfo - queryField - serverName - serverPort - httpHeaders - chu2UrlScheme - chu2Input - chu2Headers - ) = - envData - requestMethod - scriptName - pathInfo - queryField - serverName - serverPort - httpHeaders - chu2UrlScheme - chu2Input - chu2Headers - data Status : Set where OK : Status Created : Status @@ -169,45 +78,9 @@ NotImplemented : Status ServiceUnavailable : Status -{-# COMPILED_DATA Status Chu2.FFI.Status - Chu2.FFI.OK - Chu2.FFI.Created - Chu2.FFI.Accepted - Chu2.FFI.NoContent - Chu2.FFI.MultipleChoices - Chu2.FFI.MovedPermanently - Chu2.FFI.SeeOther - Chu2.FFI.NotModified - Chu2.FFI.MovedTemporarily - Chu2.FFI.BadRequest - Chu2.FFI.Unauthorized - Chu2.FFI.Forbidden - Chu2.FFI.NotFound - Chu2.FFI.MethodNotAllowed - Chu2.FFI.NotAcceptable - Chu2.FFI.Conflict - Chu2.FFI.Gone - Chu2.FFI.PreconditionFailed - Chu2.FFI.RequestEntityTooLarge - Chu2.FFI.RequestURItooLong - Chu2.FFI.UnsupportedMediaType - Chu2.FFI.NotImplemented - Chu2.FFI.ServiceUnavailable -#-} Body = Field -private - data ResponseData : Set where - responseData : - Status - → Headers - → Body - → ResponseData - - {-# COMPILED_DATA ResponseData Chu2.FFI.Response Chu2.FFI.Response #-} - - record Response : Set where constructor response field @@ -215,36 +88,9 @@ headers : Headers body : Body -private - responseToResponseData : Response → ResponseData - responseToResponseData - ( response - status - headers - body - ) = - - responseData - status - headers - body - - responseDataToResponse : ResponseData → Response - responseDataToResponse - ( responseData - status - headers - body - ) = - - response - status - headers - body - -defaultResponse : Response -defaultResponse = +default-response : Response +default-response = record { status = OK @@ -252,42 +98,12 @@ ; body = "Chu2!" } -Application = Env → IO Response -Middleware = Application → Application -private - RawApplication = EnvData → Prim.IO ResponseData - -RawMiddleware = RawApplication → RawApplication - -private - open import Function using (_$_) - - applicationToRawApplication : Application → RawApplication - applicationToRawApplication app = - λ aEnvData → run $ - ♯ app (envDataToEnv aEnvData) >>= λ aResponse → - ♯ return (responseToResponseData aResponse) - - rawApplicationToApplication : RawApplication → Application - rawApplicationToApplication rawApp = - λ aEnv → ♯ lift (rawApp (envToEnvData aEnv)) >>= λ aRawResponse → - ♯ return (responseDataToResponse aRawResponse) +-- Interface +open import IO using (IO) +open import Data.Unit using (⊤) +Application = Env → IO Response +Middleware = Application → Application Handler = Application → IO ⊤ -RawHandler = RawApplication → Prim.IO Unit - -open import Function using (_∘_; _$_; id) - - -rawHandlerToHandler : RawHandler → Handler -rawHandlerToHandler rawHandler app = - ♯ lift (rawHandler (applicationToRawApplication app)) >> - ♯ return _ - - - - -rawMiddlewareToMiddleware : RawMiddleware → Middleware -rawMiddlewareToMiddleware r app = rawApplicationToApplication $ r $ applicationToRawApplication app diff --git a/src/Chu2/FFI.agda b/src/Chu2/FFI.agda new file mode 100644 --- /dev/null +++ b/src/Chu2/FFI.agda @@ -0,0 +1,339 @@ +module Chu2.FFI where + +open import Foreign.Haskell using (Unit) +open import IO using (IO; run; lift; _>>=_; return; _>>_) +open import Data.String using (String) +open import Coinduction using (♯_) +open import Function using (_$_) +open import Data.Product using (_,_) +open import Data.List using (map; List) + +import IO.Primitive as Prim + +open import Chu2 + + +data Tuple (A : Set)(B : Set) : Set where + _,_ : A → B → Tuple A B + +{-# IMPORT Chu2.FFI #-} +{-# COMPILED_DATA Tuple (,) (,) #-} + +HeaderData = Tuple String String +HeadersData = List HeaderData + +HeaderData→Header : HeaderData → Header +HeaderData→Header (a , b) = (a , b) + +Header→HeaderData : Header → HeaderData +Header→HeaderData (a , b) = (a , b) + +Headers→HeadersData : Headers → HeadersData +Headers→HeadersData = map Header→HeaderData + +HeadersData→Headers : HeadersData → Headers +HeadersData→Headers = map HeaderData→Header + +data RequestMethodData : Set where + OPTIONS : RequestMethodData + GET : RequestMethodData + HEAD : RequestMethodData + POST : RequestMethodData + PUT : RequestMethodData + DELETE : RequestMethodData + TRACE : RequestMethodData + CONNECT : RequestMethodData + +{-# COMPILED_DATA RequestMethodData Chu2.FFI.RequestMethodData + Chu2.FFI.OPTIONS + Chu2.FFI.GET + Chu2.FFI.HEAD + Chu2.FFI.POST + Chu2.FFI.PUT + Chu2.FFI.DELETE + Chu2.FFI.TRACE + Chu2.FFI.CONNECT +#-} + +RequestMethodData→RequestMethod : RequestMethodData → RequestMethod +RequestMethodData→RequestMethod OPTIONS = OPTIONS +RequestMethodData→RequestMethod GET = GET +RequestMethodData→RequestMethod HEAD = HEAD +RequestMethodData→RequestMethod POST = POST +RequestMethodData→RequestMethod PUT = PUT +RequestMethodData→RequestMethod DELETE = DELETE +RequestMethodData→RequestMethod TRACE = TRACE +RequestMethodData→RequestMethod CONNECT = CONNECT + +RequestMethod→RequestMethodData : RequestMethod → RequestMethodData +RequestMethod→RequestMethodData OPTIONS = OPTIONS +RequestMethod→RequestMethodData GET = GET +RequestMethod→RequestMethodData HEAD = HEAD +RequestMethod→RequestMethodData POST = POST +RequestMethod→RequestMethodData PUT = PUT +RequestMethod→RequestMethodData DELETE = DELETE +RequestMethod→RequestMethodData TRACE = TRACE +RequestMethod→RequestMethodData CONNECT = CONNECT + + + + +data Chu2UrlSchemeData : Set where + HTTP HTTPS : Chu2UrlSchemeData + +{-# COMPILED_DATA Chu2UrlSchemeData Chu2.FFI.Chu2UrlSchemeData + Chu2.FFI.HTTP + Chu2.FFI.HTTPS +#-} + +Chu2UrlSchemeData→Chu2UrlScheme : Chu2UrlSchemeData → Chu2UrlScheme +Chu2UrlSchemeData→Chu2UrlScheme HTTP = HTTP +Chu2UrlSchemeData→Chu2UrlScheme HTTPS = HTTPS + +Chu2UrlScheme→Chu2UrlSchemeData : Chu2UrlScheme → Chu2UrlSchemeData +Chu2UrlScheme→Chu2UrlSchemeData HTTP = HTTP +Chu2UrlScheme→Chu2UrlSchemeData HTTPS = HTTPS + +Chu2HeadersData = HeadersData +HttpHeadersData = HeadersData + +data EnvData : Set where + envData : + RequestMethodData + → ScriptName + → PathInfo + → QueryField + → ServerName + → ServerPort + → HttpHeadersData + → Chu2UrlSchemeData + → Chu2Input + → Chu2HeadersData + → EnvData + +{-# COMPILED_DATA EnvData Chu2.FFI.EnvData Chu2.FFI.EnvData #-} + +Env→EnvData : Env → EnvData +Env→EnvData + ( env + requestMethod + scriptName + pathInfo + queryField + serverName + serverPort + httpHeaders + chu2UrlScheme + chu2Input + chu2Headers + ) = + envData + (RequestMethod→RequestMethodData requestMethod) + scriptName + pathInfo + queryField + serverName + serverPort + (Headers→HeadersData httpHeaders) + (Chu2UrlScheme→Chu2UrlSchemeData chu2UrlScheme) + chu2Input + (Headers→HeadersData chu2Headers) + +EnvData→Env : EnvData → Chu2.Env +EnvData→Env + ( envData + requestMethodData + scriptName + pathInfo + queryField + serverName + serverPort + httpHeaders + chu2UrlSchemeData + chu2Input + chu2Headers + ) = + + env + (RequestMethodData→RequestMethod requestMethodData) + scriptName + pathInfo + queryField + serverName + serverPort + (HeadersData→Headers httpHeaders) + (Chu2UrlSchemeData→Chu2UrlScheme chu2UrlSchemeData) + chu2Input + (HeadersData→Headers chu2Headers) + + + +data StatusData : Set where + OK : StatusData + Created : StatusData + Accepted : StatusData + NoContent : StatusData + MultipleChoices : StatusData + MovedPermanently : StatusData + SeeOther : StatusData + NotModified : StatusData + MovedTemporarily : StatusData + BadRequest : StatusData + Unauthorized : StatusData + Forbidden : StatusData + NotFound : StatusData + MethodNotAllowed : StatusData + NotAcceptable : StatusData + Conflict : StatusData + Gone : StatusData + PreconditionFailed : StatusData + RequestEntityTooLarge : StatusData + RequestURItooLong : StatusData + UnsupportedMediaType : StatusData + NotImplemented : StatusData + ServiceUnavailable : StatusData + +{-# COMPILED_DATA StatusData Chu2.FFI.StatusData + Chu2.FFI.OK + Chu2.FFI.Created + Chu2.FFI.Accepted + Chu2.FFI.NoContent + Chu2.FFI.MultipleChoices + Chu2.FFI.MovedPermanently + Chu2.FFI.SeeOther + Chu2.FFI.NotModified + Chu2.FFI.MovedTemporarily + Chu2.FFI.BadRequest + Chu2.FFI.Unauthorized + Chu2.FFI.Forbidden + Chu2.FFI.NotFound + Chu2.FFI.MethodNotAllowed + Chu2.FFI.NotAcceptable + Chu2.FFI.Conflict + Chu2.FFI.Gone + Chu2.FFI.PreconditionFailed + Chu2.FFI.RequestEntityTooLarge + Chu2.FFI.RequestURItooLong + Chu2.FFI.UnsupportedMediaType + Chu2.FFI.NotImplemented + Chu2.FFI.ServiceUnavailable +#-} + +StatusData→Status : StatusData → Status +StatusData→Status OK = OK +StatusData→Status Created = Created +StatusData→Status Accepted = Accepted +StatusData→Status NoContent = NoContent +StatusData→Status MultipleChoices = MultipleChoices +StatusData→Status MovedPermanently = MovedPermanently +StatusData→Status SeeOther = SeeOther +StatusData→Status NotModified = NotModified +StatusData→Status MovedTemporarily = MovedTemporarily +StatusData→Status BadRequest = BadRequest +StatusData→Status Unauthorized = Unauthorized +StatusData→Status Forbidden = Forbidden +StatusData→Status NotFound = NotFound +StatusData→Status MethodNotAllowed = MethodNotAllowed +StatusData→Status NotAcceptable = NotAcceptable +StatusData→Status Conflict = Conflict +StatusData→Status Gone = Gone +StatusData→Status PreconditionFailed = PreconditionFailed +StatusData→Status RequestEntityTooLarge = RequestEntityTooLarge +StatusData→Status RequestURItooLong = RequestURItooLong +StatusData→Status UnsupportedMediaType = UnsupportedMediaType +StatusData→Status NotImplemented = NotImplemented +StatusData→Status ServiceUnavailable = ServiceUnavailable + +Status→StatusData : Status → StatusData +Status→StatusData OK = OK +Status→StatusData Created = Created +Status→StatusData Accepted = Accepted +Status→StatusData NoContent = NoContent +Status→StatusData MultipleChoices = MultipleChoices +Status→StatusData MovedPermanently = MovedPermanently +Status→StatusData SeeOther = SeeOther +Status→StatusData NotModified = NotModified +Status→StatusData MovedTemporarily = MovedTemporarily +Status→StatusData BadRequest = BadRequest +Status→StatusData Unauthorized = Unauthorized +Status→StatusData Forbidden = Forbidden +Status→StatusData NotFound = NotFound +Status→StatusData MethodNotAllowed = MethodNotAllowed +Status→StatusData NotAcceptable = NotAcceptable +Status→StatusData Conflict = Conflict +Status→StatusData Gone = Gone +Status→StatusData PreconditionFailed = PreconditionFailed +Status→StatusData RequestEntityTooLarge = RequestEntityTooLarge +Status→StatusData RequestURItooLong = RequestURItooLong +Status→StatusData UnsupportedMediaType = UnsupportedMediaType +Status→StatusData NotImplemented = NotImplemented +Status→StatusData ServiceUnavailable = ServiceUnavailable + + +data ResponseData : Set where + responseData : + StatusData + → HeadersData + → Body + → ResponseData + +{-# COMPILED_DATA ResponseData Chu2.FFI.ResponseData Chu2.FFI.ResponseData #-} + +Response→ResponseData : Response → ResponseData +Response→ResponseData + ( response + status + headers + body + ) = + + responseData + (Status→StatusData status) + (Headers→HeadersData headers) + body + +ResponseData→Response : ResponseData → Response +ResponseData→Response + ( responseData + statusData + headers + body + ) = + + response + (StatusData→Status statusData) + (HeadersData→Headers headers) + body + + + +RawApplication = EnvData → Prim.IO ResponseData + +Application→RawApplication : Application → RawApplication +Application→RawApplication anApp = + λ anEnvData → run $ + ♯ anApp (EnvData→Env anEnvData) >>= λ aResponse → + ♯ return (Response→ResponseData aResponse) + +RawApplication→Application : RawApplication → Application +RawApplication→Application aRawApp = + λ anEnv → ♯ lift (aRawApp (Env→EnvData anEnv)) >>= λ aRawResponse → + ♯ return (ResponseData→Response aRawResponse) + + +RawHandler = RawApplication → Prim.IO Unit + +RawHandler→Handler : RawHandler → Handler +RawHandler→Handler aRawHandler anApp = + ♯ lift (aRawHandler (Application→RawApplication anApp)) >> + ♯ return _ + + +RawMiddleware = RawApplication → RawApplication + +RawMiddleware→Middleware : RawMiddleware → Middleware +RawMiddleware→Middleware aRawMiddleware anApp = + let rawApp = aRawMiddleware (Application→RawApplication anApp) + in + + RawApplication→Application rawApp diff --git a/src/Chu2/FFI.hs b/src/Chu2/FFI.hs --- a/src/Chu2/FFI.hs +++ b/src/Chu2/FFI.hs @@ -2,7 +2,7 @@ import Data.ByteString (ByteString) -data RequestMethod = +data RequestMethodData = OPTIONS | GET | HEAD @@ -15,7 +15,7 @@ -data Status = +data StatusData = OK | Created | Accepted @@ -49,27 +49,27 @@ type Chu2Errors = Field -> IO () -data Chu2UrlScheme = HTTP | HTTPS +data Chu2UrlSchemeData = HTTP | HTTPS deriving (Show) -data Env = Env - { requestMethod :: RequestMethod +data EnvData = EnvData + { requestMethod :: RequestMethodData , scriptName :: Field , pathInfo :: Field , queryString :: Field , serverName :: Field , serverPort :: Field , httpHeaders :: Headers - , chu2UrlScheme :: Chu2UrlScheme + , chu2UrlScheme :: Chu2UrlSchemeData , chu2Input :: Field , chu2Headers :: Headers } -data Response = Response - { status :: Status +data ResponseData = ResponseData + { status :: StatusData , headers :: Headers , body :: Field } 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,6 +1,7 @@ module Chu2.Handler.SnapServer where -open import Chu2 using (Handler; RawHandler; rawHandlerToHandler; RawMiddleware) +open import Chu2 using (Handler) +open import Chu2.FFI using (RawHandler; RawHandler→Handler; RawMiddleware) private postulate @@ -24,4 +25,4 @@ on-port_run port = let port-i = primNatToInteger port in - rawHandlerToHandler (onPort_run port-i) + RawHandler→Handler (onPort_run port-i) 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 @@ -9,7 +9,7 @@ -hack2RequestMethodToChu2RequestMethod :: Hack2.RequestMethod -> RequestMethod +hack2RequestMethodToChu2RequestMethod :: Hack2.RequestMethod -> RequestMethodData hack2RequestMethodToChu2RequestMethod Hack2.OPTIONS = OPTIONS hack2RequestMethodToChu2RequestMethod Hack2.GET = GET hack2RequestMethodToChu2RequestMethod Hack2.HEAD = HEAD @@ -19,7 +19,7 @@ hack2RequestMethodToChu2RequestMethod Hack2.TRACE = TRACE hack2RequestMethodToChu2RequestMethod Hack2.CONNECT = CONNECT -chu2RequestMethodToHack2RequestMethod :: RequestMethod -> Hack2.RequestMethod +chu2RequestMethodToHack2RequestMethod :: RequestMethodData -> Hack2.RequestMethod chu2RequestMethodToHack2RequestMethod OPTIONS = Hack2.OPTIONS chu2RequestMethodToHack2RequestMethod GET = Hack2.GET chu2RequestMethodToHack2RequestMethod HEAD = Hack2.HEAD @@ -29,11 +29,11 @@ chu2RequestMethodToHack2RequestMethod TRACE = Hack2.TRACE chu2RequestMethodToHack2RequestMethod CONNECT = Hack2.CONNECT -hack2UrlSchemeToChu2UrlScheme :: Hack2.HackUrlScheme -> Chu2UrlScheme +hack2UrlSchemeToChu2UrlScheme :: Hack2.HackUrlScheme -> Chu2UrlSchemeData hack2UrlSchemeToChu2UrlScheme Hack2.HTTP = HTTP hack2UrlSchemeToChu2UrlScheme Hack2.HTTPS = HTTPS -chu2UrlSchemeToHack2UrlScheme :: Chu2UrlScheme -> Hack2.HackUrlScheme +chu2UrlSchemeToHack2UrlScheme :: Chu2UrlSchemeData -> Hack2.HackUrlScheme chu2UrlSchemeToHack2UrlScheme HTTP = Hack2.HTTP chu2UrlSchemeToHack2UrlScheme HTTPS = Hack2.HTTPS @@ -53,41 +53,41 @@ mapTuple :: (a -> b) -> [(a,a)] -> [(b,b)] mapTuple f = map (\(x,y) -> (f x, f y)) -hack2EnvToChu2Env :: Hack2.Env -> Env +hack2EnvToChu2Env :: Hack2.Env -> EnvData hack2EnvToChu2Env e = - Env + EnvData { - requestMethod = hack2RequestMethodToChu2RequestMethod $ Hack2.requestMethod e - , chu2UrlScheme = hack2UrlSchemeToChu2UrlScheme $ Hack2.hackUrlScheme e - , serverPort = show $ Hack2.serverPort e - , scriptName = b2f $ Hack2.scriptName e - , pathInfo = b2f $ Hack2.pathInfo e - , queryString = b2f $ Hack2.queryString e - , serverName = b2f $ Hack2.serverName e - , httpHeaders = mapTuple b2f $ Hack2.httpHeaders e - , chu2Input = b2f_Utf8Encoding $ Hack2.hackInput e - , chu2Headers = mapTuple b2f $ Hack2.hackHeaders e + requestMethod = hack2RequestMethodToChu2RequestMethod $ Hack2.requestMethod e + , chu2UrlScheme = hack2UrlSchemeToChu2UrlScheme $ Hack2.hackUrlScheme e + , serverPort = show $ Hack2.serverPort e + , scriptName = b2f $ Hack2.scriptName e + , pathInfo = b2f $ Hack2.pathInfo e + , queryString = b2f $ Hack2.queryString e + , serverName = b2f $ Hack2.serverName e + , httpHeaders = mapTuple b2f $ Hack2.httpHeaders e + , chu2Input = b2f_Utf8Encoding $ Hack2.hackInput e + , chu2Headers = mapTuple b2f $ Hack2.hackHeaders e } -chu2EnvToHack2Env :: Env -> Hack2.Env +chu2EnvToHack2Env :: EnvData -> Hack2.Env chu2EnvToHack2Env e = def { Hack2.requestMethod = chu2RequestMethodToHack2RequestMethod $ requestMethod e , Hack2.hackUrlScheme = chu2UrlSchemeToHack2UrlScheme $ chu2UrlScheme e - , Hack2.serverPort = read $ serverPort e - , Hack2.scriptName = f2b $ scriptName e - , Hack2.pathInfo = f2b $ pathInfo e - , Hack2.queryString = f2b $ queryString e - , Hack2.serverName = f2b $ serverName e - , Hack2.httpHeaders = mapTuple f2b $ httpHeaders e - , Hack2.hackInput = f2b_Utf8Encoding $ chu2Input e - , Hack2.hackHeaders = mapTuple f2b $ chu2Headers e + , Hack2.serverPort = read $ serverPort e + , Hack2.scriptName = f2b $ scriptName e + , Hack2.pathInfo = f2b $ pathInfo e + , Hack2.queryString = f2b $ queryString e + , Hack2.serverName = f2b $ serverName e + , Hack2.httpHeaders = mapTuple f2b $ httpHeaders e + , Hack2.hackInput = f2b_Utf8Encoding $ chu2Input e + , Hack2.hackHeaders = mapTuple f2b $ chu2Headers e } -showStatus :: Status -> Int +showStatus :: StatusData -> Int showStatus OK = 200 showStatus Created = 201 showStatus Accepted = 202 @@ -113,7 +113,7 @@ showStatus ServiceUnavailable = 503 -readStatus :: Int -> Status +readStatus :: Int -> StatusData readStatus 200 = OK readStatus 201 = Created readStatus 202 = Accepted @@ -140,7 +140,7 @@ readStatus _ = ServiceUnavailable -chu2ResponseToHack2Response :: Response -> Hack2.Response +chu2ResponseToHack2Response :: ResponseData -> Hack2.Response chu2ResponseToHack2Response r = Hack2.Response { @@ -149,9 +149,9 @@ , Hack2.body = f2b_Utf8Encoding $ body r } -hack2ResponseToHack2Response :: Hack2.Response -> Response +hack2ResponseToHack2Response :: Hack2.Response -> ResponseData hack2ResponseToHack2Response r = - Response + ResponseData { status = readStatus $ Hack2.status r , headers = mapTuple b2f $ Hack2.headers r @@ -162,7 +162,7 @@ -type Application = Env -> IO Response +type Application = EnvData -> IO ResponseData type Middleware = Application -> Application chu2ApplicationToHack2Application :: Application -> Hack2.Application diff --git a/src/Chu2/Middleware/SimpleLogger.agda b/src/Chu2/Middleware/SimpleLogger.agda --- a/src/Chu2/Middleware/SimpleLogger.agda +++ b/src/Chu2/Middleware/SimpleLogger.agda @@ -1,6 +1,7 @@ module Chu2.Middleware.SimpleLogger where -open import Chu2 using (rawMiddlewareToMiddleware; RawMiddleware; Middleware) +open import Chu2 using (Middleware) +open import Chu2.FFI using (RawMiddleware→Middleware; RawMiddleware) private postulate @@ -10,4 +11,4 @@ {-# COMPILED raw-simple-logger Chu2.Middleware.SimpleLoggerFFI.simple_logger #-} simple-logger : Middleware -simple-logger = rawMiddlewareToMiddleware raw-simple-logger +simple-logger = RawMiddleware→Middleware raw-simple-logger diff --git a/src/Hello.agda b/src/Hello.agda --- a/src/Hello.agda +++ b/src/Hello.agda @@ -1,6 +1,6 @@ module Hello where -open import IO using (run; return) +open import IO using (return) renaming (run to io) open import Data.List using ([]) open import Function using (const) open import Chu2 using (response; OK; Application) @@ -11,4 +11,4 @@ hello-world-app = const (return hello-world-response) open import Chu2.Handler.SnapServer using (on-port_run) -main = run (on-port 3000 run hello-world-app) +main = io (on-port 3000 run hello-world-app) diff --git a/src/Hello2.agda b/src/Hello2.agda --- a/src/Hello2.agda +++ b/src/Hello2.agda @@ -3,15 +3,15 @@ -- simple-logger middleware open import Chu2.Middleware.SimpleLogger using (simple-logger) -open import IO using (run; return) +open import IO using (return) renaming (run to io) open import Function using (const) -open import Chu2 using (Application; defaultResponse; RawMiddleware) +open import Chu2 using (Application; default-response) --- https://github.com/nfjinjing/gumi -open import Gumi.Light using (_-_) +default-app : Application +default-app = const (return default-response) -hello-world-app : Application -hello-world-app = const - return defaultResponse +app : Application +app = simple-logger default-app open import Chu2.Handler.SnapServer using (on-port_run) -main = run - on-port 3001 run - simple-logger hello-world-app +main = io (on-port 3001 run app)