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