chu2-2012.11.20: src/Chu2/FFI.agda

module Chu2.FFI where

open import Foreign.Haskell using (Unit)
open import IO using (IO; run; lift; _>>=_; return; _>>_)
open import Data.String using (String)
open import Coinduction using (♯_)
open import Function using (_$_)
open import Data.Product using (_,_)
open import Data.List using (map; List)

import IO.Primitive as Prim

open import Chu2


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

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

HeaderData = Tuple String String
HeadersData = List HeaderData

HeaderData→Header : HeaderData → Header
HeaderData→Header (a , b) = (a , b)

Header→HeaderData : Header → HeaderData
Header→HeaderData (a , b) = (a , b)

Headers→HeadersData : Headers → HeadersData
Headers→HeadersData = map Header→HeaderData

HeadersData→Headers : HeadersData → Headers
HeadersData→Headers = map HeaderData→Header

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

{-# COMPILED_DATA RequestMethodData Chu2.FFI.RequestMethodData
    Chu2.FFI.OPTIONS
    Chu2.FFI.GET
    Chu2.FFI.HEAD
    Chu2.FFI.POST
    Chu2.FFI.PUT
    Chu2.FFI.DELETE
    Chu2.FFI.TRACE
    Chu2.FFI.CONNECT
#-}

RequestMethodData→RequestMethod : RequestMethodData → RequestMethod
RequestMethodData→RequestMethod OPTIONS = OPTIONS 
RequestMethodData→RequestMethod GET     = GET     
RequestMethodData→RequestMethod HEAD    = HEAD    
RequestMethodData→RequestMethod POST    = POST    
RequestMethodData→RequestMethod PUT     = PUT     
RequestMethodData→RequestMethod DELETE  = DELETE  
RequestMethodData→RequestMethod TRACE   = TRACE   
RequestMethodData→RequestMethod CONNECT = CONNECT 

RequestMethod→RequestMethodData : RequestMethod → RequestMethodData
RequestMethod→RequestMethodData OPTIONS = OPTIONS 
RequestMethod→RequestMethodData GET     = GET     
RequestMethod→RequestMethodData HEAD    = HEAD    
RequestMethod→RequestMethodData POST    = POST    
RequestMethod→RequestMethodData PUT     = PUT     
RequestMethod→RequestMethodData DELETE  = DELETE  
RequestMethod→RequestMethodData TRACE   = TRACE   
RequestMethod→RequestMethodData CONNECT = CONNECT 




data Chu2UrlSchemeData : Set where
  HTTP HTTPS : Chu2UrlSchemeData
  
{-# COMPILED_DATA Chu2UrlSchemeData Chu2.FFI.Chu2UrlSchemeData
    Chu2.FFI.HTTP
    Chu2.FFI.HTTPS
#-}

Chu2UrlSchemeData→Chu2UrlScheme : Chu2UrlSchemeData → Chu2UrlScheme
Chu2UrlSchemeData→Chu2UrlScheme HTTP = HTTP
Chu2UrlSchemeData→Chu2UrlScheme HTTPS = HTTPS

Chu2UrlScheme→Chu2UrlSchemeData : Chu2UrlScheme → Chu2UrlSchemeData
Chu2UrlScheme→Chu2UrlSchemeData HTTP = HTTP
Chu2UrlScheme→Chu2UrlSchemeData HTTPS = HTTPS

Chu2HeadersData = HeadersData
HttpHeadersData = HeadersData

data EnvData : Set where
  envData : 
      RequestMethodData  
    → ScriptName     
    → PathInfo       
    → QueryField    
    → ServerName     
    → ServerPort     
    → HttpHeadersData   
    → Chu2UrlSchemeData  
    → Chu2Input      
    → Chu2HeadersData   
    → EnvData

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

Env→EnvData : Env → EnvData
Env→EnvData
  ( env
      requestMethod  
      scriptName     
      pathInfo       
      queryField    
      serverName     
      serverPort     
      httpHeaders    
      chu2UrlScheme 
      chu2Input      
      chu2Headers    
  ) =
  envData
    (RequestMethod→RequestMethodData requestMethod)
    scriptName     
    pathInfo       
    queryField    
    serverName     
    serverPort     
    (Headers→HeadersData httpHeaders)
    (Chu2UrlScheme→Chu2UrlSchemeData chu2UrlScheme)
    chu2Input      
    (Headers→HeadersData chu2Headers)

EnvData→Env : EnvData → Chu2.Env
EnvData→Env
  ( envData
      requestMethodData  
      scriptName     
      pathInfo       
      queryField    
      serverName     
      serverPort     
      httpHeaders    
      chu2UrlSchemeData  
      chu2Input      
      chu2Headers    
  ) =

  env
    (RequestMethodData→RequestMethod requestMethodData)
    scriptName     
    pathInfo       
    queryField    
    serverName     
    serverPort     
    (HeadersData→Headers httpHeaders)
    (Chu2UrlSchemeData→Chu2UrlScheme chu2UrlSchemeData)
    chu2Input      
    (HeadersData→Headers chu2Headers)



data StatusData : Set where
  OK                        : StatusData
  Created                   : StatusData
  Accepted                  : StatusData
  NoContent                 : StatusData
  MultipleChoices           : StatusData
  MovedPermanently          : StatusData
  SeeOther                  : StatusData
  NotModified               : StatusData
  MovedTemporarily          : StatusData
  BadRequest                : StatusData
  Unauthorized              : StatusData
  Forbidden                 : StatusData
  NotFound                  : StatusData
  MethodNotAllowed          : StatusData
  NotAcceptable             : StatusData
  Conflict                  : StatusData
  Gone                      : StatusData
  PreconditionFailed        : StatusData
  RequestEntityTooLarge     : StatusData
  RequestURItooLong         : StatusData
  UnsupportedMediaType      : StatusData
  NotImplemented            : StatusData
  ServiceUnavailable        : StatusData

{-# COMPILED_DATA StatusData Chu2.FFI.StatusData
  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
#-}

StatusData→Status : StatusData → Status
StatusData→Status OK                       = OK                       
StatusData→Status Created                  = Created                  
StatusData→Status Accepted                 = Accepted                 
StatusData→Status NoContent                = NoContent                
StatusData→Status MultipleChoices          = MultipleChoices          
StatusData→Status MovedPermanently         = MovedPermanently         
StatusData→Status SeeOther                 = SeeOther                 
StatusData→Status NotModified              = NotModified              
StatusData→Status MovedTemporarily         = MovedTemporarily         
StatusData→Status BadRequest               = BadRequest               
StatusData→Status Unauthorized             = Unauthorized             
StatusData→Status Forbidden                = Forbidden                
StatusData→Status NotFound                 = NotFound                 
StatusData→Status MethodNotAllowed         = MethodNotAllowed         
StatusData→Status NotAcceptable            = NotAcceptable            
StatusData→Status Conflict                 = Conflict                 
StatusData→Status Gone                     = Gone                     
StatusData→Status PreconditionFailed       = PreconditionFailed       
StatusData→Status RequestEntityTooLarge    = RequestEntityTooLarge    
StatusData→Status RequestURItooLong        = RequestURItooLong        
StatusData→Status UnsupportedMediaType     = UnsupportedMediaType     
StatusData→Status NotImplemented           = NotImplemented           
StatusData→Status ServiceUnavailable       = ServiceUnavailable       

Status→StatusData : Status → StatusData
Status→StatusData OK                       = OK                       
Status→StatusData Created                  = Created                  
Status→StatusData Accepted                 = Accepted                 
Status→StatusData NoContent                = NoContent                
Status→StatusData MultipleChoices          = MultipleChoices          
Status→StatusData MovedPermanently         = MovedPermanently         
Status→StatusData SeeOther                 = SeeOther                 
Status→StatusData NotModified              = NotModified              
Status→StatusData MovedTemporarily         = MovedTemporarily         
Status→StatusData BadRequest               = BadRequest               
Status→StatusData Unauthorized             = Unauthorized             
Status→StatusData Forbidden                = Forbidden                
Status→StatusData NotFound                 = NotFound                 
Status→StatusData MethodNotAllowed         = MethodNotAllowed         
Status→StatusData NotAcceptable            = NotAcceptable            
Status→StatusData Conflict                 = Conflict                 
Status→StatusData Gone                     = Gone                     
Status→StatusData PreconditionFailed       = PreconditionFailed       
Status→StatusData RequestEntityTooLarge    = RequestEntityTooLarge    
Status→StatusData RequestURItooLong        = RequestURItooLong        
Status→StatusData UnsupportedMediaType     = UnsupportedMediaType     
Status→StatusData NotImplemented           = NotImplemented           
Status→StatusData ServiceUnavailable       = ServiceUnavailable


data ResponseData : Set where
  responseData : 
      StatusData
    → HeadersData
    → Body
    → ResponseData

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

Response→ResponseData : Response → ResponseData
Response→ResponseData 
  ( response
      status
      headers
      body
  ) =

  responseData
    (Status→StatusData status)
    (Headers→HeadersData headers)
    body

ResponseData→Response : ResponseData → Response
ResponseData→Response 
  ( responseData
      statusData
      headers
      body
  ) =

  response
    (StatusData→Status statusData)
    (HeadersData→Headers headers)
    body



RawApplication = EnvData → Prim.IO ResponseData

Application→RawApplication : Application → RawApplication
Application→RawApplication anApp = 
  λ anEnvData → run $
    ♯ anApp (EnvData→Env anEnvData) >>= λ aResponse →
    ♯ return (Response→ResponseData aResponse)

RawApplication→Application : RawApplication → Application
RawApplication→Application aRawApp = 
  λ anEnv → ♯ lift (aRawApp (Env→EnvData anEnv)) >>= λ aRawResponse → 
            ♯ return (ResponseData→Response aRawResponse)
           

RawHandler = RawApplication → Prim.IO Unit

RawHandler→Handler : RawHandler → Handler
RawHandler→Handler aRawHandler anApp = 
 ♯ lift (aRawHandler (Application→RawApplication anApp)) >> 
 ♯ return _


RawMiddleware = RawApplication → RawApplication

RawMiddleware→Middleware : RawMiddleware → Middleware
RawMiddleware→Middleware aRawMiddleware anApp = 
  let rawApp = aRawMiddleware (Application→RawApplication anApp)
  in

  RawApplication→Application rawApp