packages feed

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