chu2 (empty) → 2012.11.16
raw patch · 12 files changed
+518/−0 lines, 12 filesdep +basedep +bytestringdep +hack2setup-changed
Dependencies added: base, bytestring, hack2, hack2-handler-snap-server
Files
- Guardfile +27/−0
- LICENSE +31/−0
- Nemesis +25/−0
- Setup.lhs +4/−0
- chu2.cabal +36/−0
- readme.md +35/−0
- src/Chu2.agda +139/−0
- src/Chu2/ByteString.agda +17/−0
- src/Chu2/FFI.hs +84/−0
- src/Chu2/Handler/SnapServerFFI.hs +8/−0
- src/Chu2/Interface/Hack2.hs +91/−0
- src/Hello.agda +21/−0
+ Guardfile view
@@ -0,0 +1,27 @@+# A sample Agda Guardfile+# More info at https://github.com/guard/guard#readme++guard :shell, :all_on_start => true do+ + # watch /.*\.l?agda$/ do |m|+ # puts "\n\n\nCompiling..."+ # `agda -i ~/scm/lib/git/agda/standard-library/src -i . -c #{m[0]} && echo "Compiled!"`+ # end+ + # watch "hello.agda" do+ # puts "\n\n\nCompiling..."+ # `agda -i ~/scm/lib/git/agda/standard-library/src -i . -c hello.agda && echo "Compiled!" && ./hello`+ # end++ watch /.*\.l?hs$/ do |m|+ if m[0].scan("MAlonzo").empty?+ puts "\n\n\nCompiling #{m[0]} ..."+ `runghc -isrc #{m[0]} && echo "Compiled!"`+ end+ end+ + watch "src/Hello" do+ puts "Running Hello ..."+ `./src/Hello`+ end+end
+ LICENSE view
@@ -0,0 +1,31 @@+Copyright (c) 2012, Jinjing Wang++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are+met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Jinjing Wang nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Nemesis view
@@ -0,0 +1,25 @@+import System.Nemesis.Env+import Air.Env ((-))+import Prelude hiding ((-))++main = run nemesis++nemesis = do+ clean - + [+ "**/MAlonzo"+ , "**/*.hi"+ , "**/*.agdai"+ , "**/*.o"+ , "dist"+ , "log"+ ]+ ++++ desc "prepare cabal dist"+ task "dist" $ do+ sh "cabal clean"+ sh "cabal configure"+ sh "cabal sdist"
+ Setup.lhs view
@@ -0,0 +1,4 @@+#! /usr/bin/env runhaskell++> import Distribution.Simple+> main = defaultMain
+ chu2.cabal view
@@ -0,0 +1,36 @@+Name: chu2+Version: 2012.11.16+Build-type: Simple+Synopsis: FFI for Chu2 Agda Web Server Interface+Description:+ + FFI for Chu2 Agda Web Server Interface++License: BSD3+License-file: LICENSE+Author: Jinjing Wang+Maintainer: Jinjing Wang <nfjinjing@gmail.com>+Build-Depends: base+Cabal-version: >= 1.2+category: Web+homepage: https://github.com/nfjinjing/chu2+data-files: readme.md+ Nemesis+ Guardfile+ src/Chu2.agda+ src/Hello.agda+ src/Chu2/ByteString.agda+ ++library+ build-depends: + base >= 4 && < 5+ , bytestring+ , hack2+ , hack2-handler-snap-server+ + hs-source-dirs: src/+ exposed-modules: + Chu2.FFI+ Chu2.Handler.SnapServerFFI+ Chu2.Interface.Hack2
+ readme.md view
@@ -0,0 +1,35 @@+Example Chu2 Application in Agda+==================================++```agda++module Hello where++import IO.Primitive as Prim+open import Chu2+open import Foreign.Haskell+open import Data.List+open import Chu2.ByteString++{-# IMPORT Chu2.Handler.SnapServerFFI #-}++postulate+ runChu2 : Application -> Prim.IO Unit++{-# COMPILED runChu2 Chu2.Handler.SnapServerFFI.runChu2 #-}++hello_world_response = response OK [] (pack "Hello Agda!")++hello_world_app : Application+hello_world_app = \_ -> Prim.return hello_world_response++main = runChu2 hello_world_app+++```++Note+====++* need the Agda standard library: <http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibrary>+* need to read the Agda tutorial and be able to run Agda script from emacs: <http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf>
+ src/Chu2.agda view
@@ -0,0 +1,139 @@+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+
+ src/Chu2/ByteString.agda view
@@ -0,0 +1,17 @@+module Chu2.ByteString where++open import Data.String+import IO.Primitive as Prim++{-# IMPORT Data.Word #-}+{-# IMPORT Data.ByteString.Internal #-}+{-# IMPORT Data.ByteString.Char8 #-}++postulate+ ByteString : Set+ pack : String -> ByteString+ unpack : ByteString -> String++{-# COMPILED_TYPE ByteString Data.ByteString.Char8.ByteString #-}+{-# COMPILED pack Data.ByteString.Char8.pack #-}+{-# COMPILED unpack Data.ByteString.Char8.unpack #-}
+ src/Chu2/FFI.hs view
@@ -0,0 +1,84 @@+module Chu2.FFI where++import Data.ByteString (ByteString)+import Data.ByteString.Char8 (pack)+++data Header = Header ByteString ByteString+ deriving (Show)+ +data RequestMethod =+ OPTIONS+ | GET+ | HEAD+ | POST+ | PUT+ | DELETE+ | TRACE+ | CONNECT+ deriving (Show, Read, Eq)++++data Status = + OK+ | Created+ | Accepted+ | NoContent+ | MultipleChoices+ | MovedPermanently+ | SeeOther+ | NotModified+ | MovedTemporarily+ | BadRequest+ | Unauthorized+ | Forbidden+ | NotFound+ | MethodNotAllowed+ | NotAcceptable+ | Conflict+ | Gone+ | PreconditionFailed+ | RequestEntityTooLarge+ | RequestURItooLong+ | UnsupportedMediaType+ | NotImplemented+ | ServiceUnavailable+ deriving (Show)+ +type Headers = [Header]+++type Chu2Errors = ByteString -> IO ()++data Chu2UrlScheme = HTTP | HTTPS+ deriving (Show)+ ++data Env = Env+ { requestMethod :: RequestMethod+ , scriptName :: ByteString+ , pathInfo :: ByteString+ , queryString :: ByteString+ , serverName :: ByteString+ , serverPort :: ByteString+ , httpHeaders :: Headers+ , chu2Version :: ByteString+ , chu2UrlScheme :: Chu2UrlScheme+ , chu2Input :: ByteString+ , chu2Errors :: Chu2Errors+ , chu2Headers :: Headers+ }++++data Response = Response+ { status :: Status+ , headers :: Headers+ , body :: ByteString+ }+ deriving (Show)+++type Application = Env -> IO Response+
+ src/Chu2/Handler/SnapServerFFI.hs view
@@ -0,0 +1,8 @@+module Chu2.Handler.SnapServerFFI where+ +import Chu2.FFI+import Chu2.Interface.Hack2+import Hack2.Handler.SnapServer++runChu2 :: Application -> IO ()+runChu2 app = run (chu2AppplicationToHack2Application app)
+ src/Chu2/Interface/Hack2.hs view
@@ -0,0 +1,91 @@+module Chu2.Interface.Hack2 where++import Data.ByteString (ByteString)+import qualified Hack2 as Hack2+import Data.ByteString.Char8 (pack)++import Chu2.FFI++chu2RequestMethodFromHack2RequestMethod :: Hack2.RequestMethod -> RequestMethod+chu2RequestMethodFromHack2RequestMethod Hack2.OPTIONS = OPTIONS+chu2RequestMethodFromHack2RequestMethod Hack2.GET = GET+chu2RequestMethodFromHack2RequestMethod Hack2.HEAD = HEAD+chu2RequestMethodFromHack2RequestMethod Hack2.POST = POST+chu2RequestMethodFromHack2RequestMethod Hack2.PUT = PUT+chu2RequestMethodFromHack2RequestMethod Hack2.DELETE = DELETE+chu2RequestMethodFromHack2RequestMethod Hack2.TRACE = TRACE+chu2RequestMethodFromHack2RequestMethod Hack2.CONNECT = CONNECT+++chu2UrlSchemeFromHack2UrlScheme :: Hack2.HackUrlScheme -> Chu2UrlScheme+chu2UrlSchemeFromHack2UrlScheme Hack2.HTTP = HTTP+chu2UrlSchemeFromHack2UrlScheme Hack2.HTTPS = HTTPS++chu2ErrorsFromHack2Errors :: Hack2.HackErrors -> Chu2Errors+chu2ErrorsFromHack2Errors = Hack2.unHackErrors++tupleToHeader :: (ByteString, ByteString) -> Header+tupleToHeader (x,y) = Header x y++chu2EnvFromHack2Env :: Hack2.Env -> Env+chu2EnvFromHack2Env e = + Env+ {+ requestMethod = chu2RequestMethodFromHack2RequestMethod $ Hack2.requestMethod e+ , scriptName = Hack2.scriptName e+ , pathInfo = Hack2.pathInfo e+ , queryString = Hack2.queryString e+ , serverName = Hack2.serverName e+ , serverPort = pack $ show $ Hack2.serverPort e+ , httpHeaders = map tupleToHeader (Hack2.httpHeaders e)+ , chu2Version = pack $ show $ Hack2.hackVersion e+ , chu2UrlScheme = chu2UrlSchemeFromHack2UrlScheme $ Hack2.hackUrlScheme e+ , chu2Input = Hack2.hackInput e+ , chu2Errors = chu2ErrorsFromHack2Errors $ Hack2.hackErrors e+ , chu2Headers = map tupleToHeader (Hack2.hackHeaders e)+ }+ +headerToTuple :: Header -> (ByteString, ByteString)+headerToTuple (Header x y) = (x,y)++chu2ResponseToHack2Response :: Response -> Hack2.Response+chu2ResponseToHack2Response r =+ Hack2.Response+ {+ Hack2.status = showStatus $ status r+ , Hack2.headers = map headerToTuple (headers r)+ , Hack2.body = body r+ }++showStatus :: Status -> Int+showStatus OK = 200+showStatus Created = 201+showStatus Accepted = 202+showStatus NoContent = 204+showStatus MultipleChoices = 300+showStatus MovedPermanently = 301+showStatus SeeOther = 303+showStatus NotModified = 304+showStatus MovedTemporarily = 307+showStatus BadRequest = 400+showStatus Unauthorized = 401+showStatus Forbidden = 403+showStatus NotFound = 404+showStatus MethodNotAllowed = 405+showStatus NotAcceptable = 406+showStatus Conflict = 409+showStatus Gone = 410+showStatus PreconditionFailed = 412+showStatus RequestEntityTooLarge = 413+showStatus RequestURItooLong = 414+showStatus UnsupportedMediaType = 415+showStatus NotImplemented = 501+showStatus ServiceUnavailable = 503+++chu2AppplicationToHack2Application :: Application -> Hack2.Application+chu2AppplicationToHack2Application app = \hack2Env -> do+ chu2Response <- app (chu2EnvFromHack2Env hack2Env)+ return (chu2ResponseToHack2Response chu2Response)+ +
+ src/Hello.agda view
@@ -0,0 +1,21 @@+module Hello where++import IO.Primitive as Prim+open import Chu2+open import Foreign.Haskell+open import Data.List+open import Chu2.ByteString++{-# IMPORT Chu2.Handler.SnapServerFFI #-}++postulate+ runChu2 : Application -> Prim.IO Unit++{-# COMPILED runChu2 Chu2.Handler.SnapServerFFI.runChu2 #-}++hello_world_response = response OK [] (pack "Hello Agda!")++hello_world_app : Application+hello_world_app = \_ -> Prim.return hello_world_response++main = runChu2 hello_world_app