chu2-2012.11.18: src/Chu2.agda

module Chu2 where

open import Data.List using (List; [_])
open import Chu2.ByteString using (ByteString; pack; empty)
open import Foreign.Haskell using (Unit)
open import IO.Primitive using (IO)

data Tuple (A : Set)(B : Set) : Set where
    _,_ : A → B → Tuple A B


{-# IMPORT Chu2.FFI #-}
{-# COMPILED_DATA Tuple (,) (,) #-}

Header = Tuple ByteString ByteString

Headers = List Header

data RequestMethod : Set where
  OPTIONS   : RequestMethod
  GET       : RequestMethod
  HEAD      : RequestMethod
  POST      : RequestMethod
  PUT       : RequestMethod
  DELETE    : RequestMethod
  TRACE     : RequestMethod
  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    =  ByteString
PathInfo      =  ByteString
QueryString   =  ByteString
ServerName    =  ByteString
ServerPort    =  ByteString
HttpHeaders   =  Headers
Chu2Input     =  ByteString
Chu2Errors    =  ByteString → IO Unit
Chu2Headers   =  Headers

private
  data EnvData : Set where
    envData : 
        RequestMethod  
      → ScriptName     
      → PathInfo       
      → QueryString    
      → ServerName     
      → ServerPort     
      → HttpHeaders    
      → 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    
    chu2UrlScheme  : Chu2UrlScheme  
    chu2Input      : Chu2Input      
    chu2Errors     : Chu2Errors     
    chu2Headers    : Chu2Headers   
    

private
  envDataToEnv : EnvData → Env
  envDataToEnv
    ( envData
        requestMethod  
        scriptName     
        pathInfo       
        queryString    
        serverName     
        serverPort     
        httpHeaders    
        chu2UrlScheme  
        chu2Input      
        chu2Errors     
        chu2Headers    
    ) =
  
    env
      requestMethod  
      scriptName     
      pathInfo       
      queryString    
      serverName     
      serverPort     
      httpHeaders    
      chu2UrlScheme  
      chu2Input      
      chu2Errors     
      chu2Headers    


  envToEnvData : Env → EnvData
  envToEnvData
    ( env
        requestMethod  
        scriptName     
        pathInfo       
        queryString    
        serverName     
        serverPort     
        httpHeaders    
        chu2UrlScheme  
        chu2Input      
        chu2Errors     
        chu2Headers    
    ) =
  
    envData
      requestMethod  
      scriptName     
      pathInfo       
      queryString    
      serverName     
      serverPort     
      httpHeaders    
      chu2UrlScheme  
      chu2Input      
      chu2Errors     
      chu2Headers  

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

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
    status  : Status
    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 = 
  record
    {
      status = OK
    ; headers = [(pack "Content-Type", pack "text/plain")]
    ; body = pack "Chu2!"
    }

Application = Env → IO Response
Middleware = Application → Application

private
  RawApplication = EnvData → IO ResponseData

RawMiddleware = RawApplication → RawApplication

private
  open IO.Primitive using (_>>=_; return)
  applicationToRawApplication : Application → RawApplication
  applicationToRawApplication app = 
    λ aEnvData → app (envDataToEnv aEnvData) >>= λ aResponse → return (responseToResponseData aResponse)

  rawApplicationToApplication : RawApplication → Application
  rawApplicationToApplication rawApp = 
    λ aEnv → rawApp (envToEnvData aEnv) >>= λ aRawResponse → return (responseDataToResponse aRawResponse)


Handler = Application → IO Unit
RawHandler = RawApplication → IO Unit

open import Function using (_∘_; _$_; id)


rawHandlerToHandler : RawHandler → Handler
rawHandlerToHandler h = h ∘ applicationToRawApplication



rawMiddlewareToMiddleware : RawMiddleware → Middleware
rawMiddlewareToMiddleware r app = rawApplicationToApplication $ r $ applicationToRawApplication app