diff --git a/Guardfile b/Guardfile new file mode 100644 --- /dev/null +++ b/Guardfile @@ -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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Nemesis b/Nemesis new file mode 100644 --- /dev/null +++ b/Nemesis @@ -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" diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,4 @@ +#! /usr/bin/env runhaskell + +> import Distribution.Simple +> main = defaultMain diff --git a/chu2.cabal b/chu2.cabal new file mode 100644 --- /dev/null +++ b/chu2.cabal @@ -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 +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 diff --git a/readme.md b/readme.md new file mode 100644 --- /dev/null +++ b/readme.md @@ -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: +* need to read the Agda tutorial and be able to run Agda script from emacs: diff --git a/src/Chu2.agda b/src/Chu2.agda new file mode 100644 --- /dev/null +++ b/src/Chu2.agda @@ -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 + diff --git a/src/Chu2/ByteString.agda b/src/Chu2/ByteString.agda new file mode 100644 --- /dev/null +++ b/src/Chu2/ByteString.agda @@ -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 #-} diff --git a/src/Chu2/FFI.hs b/src/Chu2/FFI.hs new file mode 100644 --- /dev/null +++ b/src/Chu2/FFI.hs @@ -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 + diff --git a/src/Chu2/Handler/SnapServerFFI.hs b/src/Chu2/Handler/SnapServerFFI.hs new file mode 100644 --- /dev/null +++ b/src/Chu2/Handler/SnapServerFFI.hs @@ -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) diff --git a/src/Chu2/Interface/Hack2.hs b/src/Chu2/Interface/Hack2.hs new file mode 100644 --- /dev/null +++ b/src/Chu2/Interface/Hack2.hs @@ -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) + + diff --git a/src/Hello.agda b/src/Hello.agda new file mode 100644 --- /dev/null +++ b/src/Hello.agda @@ -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