chu2 2012.11.17 → 2012.11.17.1

raw patch · 8 files changed

+142/−139 lines, 8 filesdep +data-defaultPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: data-default

API changes (from Hackage documentation)

Files

• chu2.cabal +2/−1
• readme.md +4/−11
• src/Chu2.agda +119/−99
• src/Chu2/ByteString.agda +4/−0
• src/Chu2/FFI.hs +0/−6
• src/Chu2/Handler/SnapServerFFI.hs +5/−1
• src/Chu2/Interface/Hack2.hs +4/−10
• src/Hello.agda +4/−11

@@ -1,5 +1,5 @@ Name:                 chu2-Version:              2012.11.17+Version:              2012.11.17.1 Build-type:           Simple Synopsis:             FFI for Chu2 Agda Web Server Interface Description:@@ -28,6 +28,7 @@     , bytestring     , hack2     , hack2-handler-snap-server+    , data-default        hs-source-dirs: src/   exposed-modules:  

@@ -5,26 +5,19 @@  module Hello where -open import IO.Primitive    using (IO; return)-open import Foreign.Haskell using (Unit)+open import IO.Primitive    using (return) open import Data.List       using ([]) open import Chu2.ByteString using (pack) open import Function        using (_$_; const)--open import Chu2--postulate-  run : ApplicationData → IO Unit--{-# IMPORT Chu2.Handler.SnapServerFFI #-}-{-# COMPILED run Chu2.Handler.SnapServerFFI.run #-}+open import Chu2               hello-world-response = response OK [] (pack "Hello Agda!")  hello-world-app : Application hello-world-app = const $ return hello-world-response -main = run $ chu2 hello-world-app+open import Chu2.Handler.SnapServer+main = onPort 3000 run $ chu2 hello-world-app   ```

@@ -1,108 +1,30 @@ 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+open import Data.List using (List; [_])+open import Chu2.ByteString using (ByteString; pack; empty)+open import Foreign.Haskell using (Unit)+open import IO.Primitive using (IO)  data Tuple (A : Set)(B : Set) : Set where     _,_ : A → B → Tuple A B +{-# IMPORT Chu2.FFI #-} {-# 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+  OPTIONS   : RequestMethod+  GET       : RequestMethod+  HEAD      : RequestMethod+  POST      : RequestMethod+  PUT       : RequestMethod+  DELETE    : RequestMethod+  TRACE     : RequestMethod+  CONNECT   : RequestMethod+    {-# COMPILED_DATA RequestMethod Chu2.FFI.RequestMethod     Chu2.FFI.OPTIONS@@ -131,7 +53,7 @@ HttpHeaders   =  Headers Chu2Version   =  ByteString Chu2Input     =  ByteString-Chu2Errors    =  ByteString → Prim.IO Unit+Chu2Errors    =  ByteString → IO Unit Chu2Headers   =  Headers  data EnvData : Set where@@ -169,8 +91,8 @@     chu2Headers    : Chu2Headers             -EnvDataToEnv : EnvData → Env-EnvDataToEnv+envDataToEnv : EnvData → Env+envDataToEnv   ( envData       requestMethod         scriptName     @@ -201,11 +123,109 @@     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 -Application = Env → Prim.IO Response-ApplicationData = EnvData → Prim.IO ResponseData+{-# 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+#-} -open Prim using (_>>=_; return)+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+    +    +    +defaultResponse : Response+defaultResponse = +  record+    {+      status = OK+    ; headers = [(pack "Content-Type", pack "text/plain")]+    ; body = pack "Chu2!"+    }++ApplicationData = EnvData → IO ResponseData+MiddlewareData = ApplicationData → ApplicationData++Application = Env → IO Response+Middleware = Application → Application++Handler = ApplicationData → IO Unit++open IO.Primitive using (_>>=_; return)+ chu2 : Application → ApplicationData-chu2 app aEnvData = app (EnvDataToEnv aEnvData) >>= \aResponse → return (ResponseToResponseData aResponse)+chu2 app = λ aEnvData → app (envDataToEnv aEnvData) >>= λ aResponse → return (responseToResponseData aResponse)

@@ -11,7 +11,11 @@   ByteString  : Set   pack        : String -> ByteString   unpack      : ByteString -> String+  empty       : ByteString+  +    {-# COMPILED_TYPE ByteString Data.ByteString.Char8.ByteString #-} {-# COMPILED pack Data.ByteString.Char8.pack #-} {-# COMPILED unpack Data.ByteString.Char8.unpack #-}+{-# COMPILED empty Data.ByteString.Char8.empty #-}

@@ -3,11 +3,6 @@ import Data.ByteString (ByteString) import Data.ByteString.Char8 (pack) -{--data Header = Header ByteString ByteString-  deriving (Show)--}- type Header = (,) ByteString ByteString  data RequestMethod =@@ -83,5 +78,4 @@   deriving (Show)  -type Application = Env -> IO Response 

@@ -3,6 +3,10 @@ import Chu2.FFI import Chu2.Interface.Hack2 import qualified Hack2.Handler.SnapServer as Snap+import Data.Default  run :: Application -> IO ()-run app = Snap.run (chu2AppplicationToHack2Application app)+run app = Snap.run (chu2ApplicationToHack2Application app)++onPort_run :: Integer -> Application -> IO ()+onPort_run port app = Snap.runWithConfig def {Snap.port = fromIntegral port} (chu2ApplicationToHack2Application app)

@@ -24,14 +24,6 @@ chu2ErrorsFromHack2Errors :: Hack2.HackErrors -> Chu2Errors chu2ErrorsFromHack2Errors = Hack2.unHackErrors -{--headerToTuple :: Header -> (ByteString, ByteString)-headerToTuple (Header x y) = (x,y)--tupleToHeader :: (ByteString, ByteString) -> Header-tupleToHeader (x,y) = Header x y--}- chu2EnvFromHack2Env :: Hack2.Env -> Env chu2EnvFromHack2Env e =    Env@@ -86,8 +78,10 @@ showStatus ServiceUnavailable = 503  -chu2AppplicationToHack2Application :: Application -> Hack2.Application-chu2AppplicationToHack2Application app = \hack2Env -> do+type Application = Env -> IO Response++chu2ApplicationToHack2Application :: Application -> Hack2.Application+chu2ApplicationToHack2Application app = \hack2Env -> do   chu2Response <- app (chu2EnvFromHack2Env hack2Env)   return (chu2ResponseToHack2Response chu2Response)   

@@ -1,22 +1,15 @@ module Hello where -open import IO.Primitive    using (IO; return)-open import Foreign.Haskell using (Unit)+open import IO.Primitive    using (return) open import Data.List       using ([]) open import Chu2.ByteString using (pack) open import Function        using (_$_; const)--open import Chu2--postulate-  run : ApplicationData → IO Unit--{-# IMPORT Chu2.Handler.SnapServerFFI #-}-{-# COMPILED run Chu2.Handler.SnapServerFFI.run #-}+open import Chu2               hello-world-response = response OK [] (pack "Hello Agda!")  hello-world-app : Application hello-world-app = const $ return hello-world-response -main = run $ chu2 hello-world-app+open import Chu2.Handler.SnapServer+main = onPort 3000 run $ chu2 hello-world-app