module Chu2 where {-# IMPORT Chu2.FFI #-} open import Data.List open import Foreign.Haskell open import Data.String open import Chu2.ByteString import IO.Primitive as Prim data Tuple (A : Set)(B : Set) : Set where _,_ : A → B → Tuple A B {-# COMPILED_DATA Tuple (,) (,) #-} Header = Tuple ByteString ByteString Headers = List Header data Status : Set where OK : Status Created : Status Accepted : Status NoContent : Status MultipleChoices : Status MovedPermanently : Status SeeOther : Status NotModified : Status MovedTemporarily : Status BadRequest : Status Unauthorized : Status Forbidden : Status NotFound : Status MethodNotAllowed : Status NotAcceptable : Status Conflict : Status Gone : Status PreconditionFailed : Status RequestEntityTooLarge : Status RequestURItooLong : Status UnsupportedMediaType : Status 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 = ByteString 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 status : Status headers : Headers body : Body ResponseToResponseData : Response → ResponseData ResponseToResponseData ( response status headers body ) = responseData status headers body data RequestMethod : Set where HEAD GET PUT DELETE POST TRACE CONNECT OPTIONS : 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 = ByteString PathInfo = ByteString QueryString = ByteString ServerName = ByteString ServerPort = ByteString HttpHeaders = Headers Chu2Version = ByteString Chu2Input = ByteString Chu2Errors = ByteString → Prim.IO Unit Chu2Headers = Headers data EnvData : Set where envData : RequestMethod → ScriptName → PathInfo → QueryString → ServerName → ServerPort → HttpHeaders → Chu2Version → Chu2UrlScheme → Chu2Input → Chu2Errors → Chu2Headers → EnvData {-# COMPILED_DATA EnvData Chu2.FFI.Env Chu2.FFI.Env #-} record Env : Set where constructor env field requestMethod : RequestMethod scriptName : ScriptName pathInfo : PathInfo queryString : QueryString serverName : ServerName serverPort : ServerPort httpHeaders : HttpHeaders chu2Version : Chu2Version chu2UrlScheme : Chu2UrlScheme chu2Input : Chu2Input chu2Errors : Chu2Errors chu2Headers : Chu2Headers EnvDataToEnv : EnvData → Env EnvDataToEnv ( envData requestMethod scriptName pathInfo queryString serverName serverPort httpHeaders chu2Version chu2UrlScheme chu2Input chu2Errors chu2Headers ) = env requestMethod scriptName pathInfo queryString serverName serverPort httpHeaders chu2Version chu2UrlScheme chu2Input chu2Errors chu2Headers Application = Env → Prim.IO Response ApplicationData = EnvData → Prim.IO ResponseData open Prim using (_>>=_; return) chu2 : Application → ApplicationData chu2 app aEnvData = app (EnvDataToEnv aEnvData) >>= \aResponse → return (ResponseToResponseData aResponse)