chu2 2012.11.19 → 2012.11.20
raw patch · 10 files changed
+421/−259 lines, 10 filesPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
API changes (from Hackage documentation)
- Chu2.FFI: Env :: RequestMethod -> Field -> Field -> Field -> Field -> Field -> Headers -> Chu2UrlScheme -> Field -> Headers -> Env
- Chu2.FFI: Response :: Status -> Headers -> Field -> Response
- Chu2.FFI: data Chu2UrlScheme
- Chu2.FFI: data Env
- Chu2.FFI: data RequestMethod
- Chu2.FFI: data Response
- Chu2.FFI: data Status
- Chu2.FFI: instance Eq RequestMethod
- Chu2.FFI: instance Read RequestMethod
- Chu2.FFI: instance Show Chu2UrlScheme
- Chu2.FFI: instance Show RequestMethod
- Chu2.FFI: instance Show Response
- Chu2.FFI: instance Show Status
+ Chu2.FFI: EnvData :: RequestMethodData -> Field -> Field -> Field -> Field -> Field -> Headers -> Chu2UrlSchemeData -> Field -> Headers -> EnvData
+ Chu2.FFI: ResponseData :: StatusData -> Headers -> Field -> ResponseData
+ Chu2.FFI: data Chu2UrlSchemeData
+ Chu2.FFI: data EnvData
+ Chu2.FFI: data RequestMethodData
+ Chu2.FFI: data ResponseData
+ Chu2.FFI: data StatusData
+ Chu2.FFI: instance Eq RequestMethodData
+ Chu2.FFI: instance Read RequestMethodData
+ Chu2.FFI: instance Show Chu2UrlSchemeData
+ Chu2.FFI: instance Show RequestMethodData
+ Chu2.FFI: instance Show ResponseData
+ Chu2.FFI: instance Show StatusData
- Chu2.FFI: Accepted :: Status
+ Chu2.FFI: Accepted :: StatusData
- Chu2.FFI: BadRequest :: Status
+ Chu2.FFI: BadRequest :: StatusData
- Chu2.FFI: CONNECT :: RequestMethod
+ Chu2.FFI: CONNECT :: RequestMethodData
- Chu2.FFI: Conflict :: Status
+ Chu2.FFI: Conflict :: StatusData
- Chu2.FFI: Created :: Status
+ Chu2.FFI: Created :: StatusData
- Chu2.FFI: DELETE :: RequestMethod
+ Chu2.FFI: DELETE :: RequestMethodData
- Chu2.FFI: Forbidden :: Status
+ Chu2.FFI: Forbidden :: StatusData
- Chu2.FFI: GET :: RequestMethod
+ Chu2.FFI: GET :: RequestMethodData
- Chu2.FFI: Gone :: Status
+ Chu2.FFI: Gone :: StatusData
- Chu2.FFI: HEAD :: RequestMethod
+ Chu2.FFI: HEAD :: RequestMethodData
- Chu2.FFI: HTTP :: Chu2UrlScheme
+ Chu2.FFI: HTTP :: Chu2UrlSchemeData
- Chu2.FFI: HTTPS :: Chu2UrlScheme
+ Chu2.FFI: HTTPS :: Chu2UrlSchemeData
- Chu2.FFI: MethodNotAllowed :: Status
+ Chu2.FFI: MethodNotAllowed :: StatusData
- Chu2.FFI: MovedPermanently :: Status
+ Chu2.FFI: MovedPermanently :: StatusData
- Chu2.FFI: MovedTemporarily :: Status
+ Chu2.FFI: MovedTemporarily :: StatusData
- Chu2.FFI: MultipleChoices :: Status
+ Chu2.FFI: MultipleChoices :: StatusData
- Chu2.FFI: NoContent :: Status
+ Chu2.FFI: NoContent :: StatusData
- Chu2.FFI: NotAcceptable :: Status
+ Chu2.FFI: NotAcceptable :: StatusData
- Chu2.FFI: NotFound :: Status
+ Chu2.FFI: NotFound :: StatusData
- Chu2.FFI: NotImplemented :: Status
+ Chu2.FFI: NotImplemented :: StatusData
- Chu2.FFI: NotModified :: Status
+ Chu2.FFI: NotModified :: StatusData
- Chu2.FFI: OK :: Status
+ Chu2.FFI: OK :: StatusData
- Chu2.FFI: OPTIONS :: RequestMethod
+ Chu2.FFI: OPTIONS :: RequestMethodData
- Chu2.FFI: POST :: RequestMethod
+ Chu2.FFI: POST :: RequestMethodData
- Chu2.FFI: PUT :: RequestMethod
+ Chu2.FFI: PUT :: RequestMethodData
- Chu2.FFI: PreconditionFailed :: Status
+ Chu2.FFI: PreconditionFailed :: StatusData
- Chu2.FFI: RequestEntityTooLarge :: Status
+ Chu2.FFI: RequestEntityTooLarge :: StatusData
- Chu2.FFI: RequestURItooLong :: Status
+ Chu2.FFI: RequestURItooLong :: StatusData
- Chu2.FFI: SeeOther :: Status
+ Chu2.FFI: SeeOther :: StatusData
- Chu2.FFI: ServiceUnavailable :: Status
+ Chu2.FFI: ServiceUnavailable :: StatusData
- Chu2.FFI: TRACE :: RequestMethod
+ Chu2.FFI: TRACE :: RequestMethodData
- Chu2.FFI: Unauthorized :: Status
+ Chu2.FFI: Unauthorized :: StatusData
- Chu2.FFI: UnsupportedMediaType :: Status
+ Chu2.FFI: UnsupportedMediaType :: StatusData
- Chu2.FFI: body :: Response -> Field
+ Chu2.FFI: body :: ResponseData -> Field
- Chu2.FFI: chu2Headers :: Env -> Headers
+ Chu2.FFI: chu2Headers :: EnvData -> Headers
- Chu2.FFI: chu2Input :: Env -> Field
+ Chu2.FFI: chu2Input :: EnvData -> Field
- Chu2.FFI: chu2UrlScheme :: Env -> Chu2UrlScheme
+ Chu2.FFI: chu2UrlScheme :: EnvData -> Chu2UrlSchemeData
- Chu2.FFI: headers :: Response -> Headers
+ Chu2.FFI: headers :: ResponseData -> Headers
- Chu2.FFI: httpHeaders :: Env -> Headers
+ Chu2.FFI: httpHeaders :: EnvData -> Headers
- Chu2.FFI: pathInfo :: Env -> Field
+ Chu2.FFI: pathInfo :: EnvData -> Field
- Chu2.FFI: queryString :: Env -> Field
+ Chu2.FFI: queryString :: EnvData -> Field
- Chu2.FFI: requestMethod :: Env -> RequestMethod
+ Chu2.FFI: requestMethod :: EnvData -> RequestMethodData
- Chu2.FFI: scriptName :: Env -> Field
+ Chu2.FFI: scriptName :: EnvData -> Field
- Chu2.FFI: serverName :: Env -> Field
+ Chu2.FFI: serverName :: EnvData -> Field
- Chu2.FFI: serverPort :: Env -> Field
+ Chu2.FFI: serverPort :: EnvData -> Field
- Chu2.FFI: status :: Response -> Status
+ Chu2.FFI: status :: ResponseData -> StatusData
- Chu2.Interface.Hack2: chu2EnvToHack2Env :: Env -> Env
+ Chu2.Interface.Hack2: chu2EnvToHack2Env :: EnvData -> Env
- Chu2.Interface.Hack2: chu2RequestMethodToHack2RequestMethod :: RequestMethod -> RequestMethod
+ Chu2.Interface.Hack2: chu2RequestMethodToHack2RequestMethod :: RequestMethodData -> RequestMethod
- Chu2.Interface.Hack2: chu2ResponseToHack2Response :: Response -> Response
+ Chu2.Interface.Hack2: chu2ResponseToHack2Response :: ResponseData -> Response
- Chu2.Interface.Hack2: chu2UrlSchemeToHack2UrlScheme :: Chu2UrlScheme -> HackUrlScheme
+ Chu2.Interface.Hack2: chu2UrlSchemeToHack2UrlScheme :: Chu2UrlSchemeData -> HackUrlScheme
- Chu2.Interface.Hack2: hack2EnvToChu2Env :: Env -> Env
+ Chu2.Interface.Hack2: hack2EnvToChu2Env :: Env -> EnvData
- Chu2.Interface.Hack2: hack2RequestMethodToChu2RequestMethod :: RequestMethod -> RequestMethod
+ Chu2.Interface.Hack2: hack2RequestMethodToChu2RequestMethod :: RequestMethod -> RequestMethodData
- Chu2.Interface.Hack2: hack2ResponseToHack2Response :: Response -> Response
+ Chu2.Interface.Hack2: hack2ResponseToHack2Response :: Response -> ResponseData
- Chu2.Interface.Hack2: hack2UrlSchemeToChu2UrlScheme :: HackUrlScheme -> Chu2UrlScheme
+ Chu2.Interface.Hack2: hack2UrlSchemeToChu2UrlScheme :: HackUrlScheme -> Chu2UrlSchemeData
- Chu2.Interface.Hack2: readStatus :: Int -> Status
+ Chu2.Interface.Hack2: readStatus :: Int -> StatusData
- Chu2.Interface.Hack2: showStatus :: Status -> Int
+ Chu2.Interface.Hack2: showStatus :: StatusData -> Int
- Chu2.Interface.Hack2: type Application = Env -> IO Response
+ Chu2.Interface.Hack2: type Application = EnvData -> IO ResponseData
Files
- chu2.cabal +4/−3
- readme.md +13/−9
- src/Chu2.agda +11/−195
- src/Chu2/FFI.agda +339/−0
- src/Chu2/FFI.hs +8/−8
- src/Chu2/Handler/SnapServer.agda +3/−2
- src/Chu2/Interface/Hack2.hs +31/−31
- src/Chu2/Middleware/SimpleLogger.agda +3/−2
- src/Hello.agda +2/−2
- src/Hello2.agda +7/−7
chu2.cabal view
@@ -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
readme.md view
@@ -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
src/Chu2.agda view
@@ -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
+ src/Chu2/FFI.agda view
@@ -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
src/Chu2/FFI.hs view
@@ -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 }
src/Chu2/Handler/SnapServer.agda view
@@ -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)
src/Chu2/Interface/Hack2.hs view
@@ -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
src/Chu2/Middleware/SimpleLogger.agda view
@@ -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
src/Hello.agda view
@@ -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)
src/Hello2.agda view
@@ -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)