chu2-2012.11.16: src/Chu2.agda

module Chu2 where

{-# IMPORT Chu2.FFI #-}

open import Data.List
open import Foreign.Haskell
open import Data.String
open import IO
open import Chu2.ByteString

import IO.Primitive as Prim



data Header : Set where
  _,_ : ByteString → ByteString → Header

{-# COMPILED_DATA Header Chu2.FFI.Header Chu2.FFI.Header #-}

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 Response : Set where
  response : 
      Status
    → Headers
    → Body
    → Response

{-# COMPILED_DATA Response Chu2.FFI.Response Chu2.FFI.Response #-}


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 Env : Set where
  env : 
      RequestMethod  
    → ScriptName     
    → PathInfo       
    → QueryString    
    → ServerName     
    → ServerPort     
    → HttpHeaders    
    → Chu2Version    
    → Chu2UrlScheme  
    → Chu2Input      
    → Chu2Errors     
    → Chu2Headers   
    → Env
  

{-# COMPILED_DATA Env Chu2.FFI.Env Chu2.FFI.Env #-}


Application = Env -> Prim.IO Response