chu2-2012.11.17: src/Chu2.agda

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)