chu2-2012.11.20: src/Chu2.agda

module Chu2 where

open import Data.List using (List; [_])
open import Data.String using (String)
open import Data.Product using (Σ; _,_)


-- HTTP

Field = String
KV = Σ Field (\_ → Field)
Header = KV
Headers = List Header

data RequestMethod : Set where
  OPTIONS   : RequestMethod
  GET       : RequestMethod
  HEAD      : RequestMethod
  POST      : RequestMethod
  PUT       : RequestMethod
  DELETE    : RequestMethod
  TRACE     : RequestMethod
  CONNECT   : RequestMethod
  


data Chu2UrlScheme : Set where
  HTTP HTTPS : Chu2UrlScheme
  

ScriptName    =  Field
PathInfo      =  Field
QueryField    =  Field
ServerName    =  Field
ServerPort    =  Field
HttpHeaders   =  Headers
Chu2Input     =  Field
Chu2Headers   =  Headers


record Env : Set where
  constructor env
  field
    requestMethod  : RequestMethod  
    scriptName     : ScriptName     
    pathInfo       : PathInfo       
    queryField     : QueryField    
    serverName     : ServerName     
    serverPort     : ServerPort     
    httpHeaders    : HttpHeaders    
    chu2UrlScheme  : Chu2UrlScheme  
    chu2Input      : Chu2Input      
    chu2Headers    : 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


Body = Field

record Response : Set where
  constructor response
  field
    status  : Status
    headers : Headers
    body    : Body

    
default-response : Response
default-response = 
  record
    {
      status = OK
    ; headers = [("Content-Type", "text/plain; charset=utf-8")]
    ; body = "Chu2!"
    }


-- Interface

open import IO using (IO)
open import Data.Unit using (⊤)

Application = Env → IO Response
Middleware = Application → Application
Handler = Application → IO ⊤