Permalink
Browse files

Make it possible to use Lemmachine as a library to compile & run any

resource, not just the provided Default anymore.
  • Loading branch information...
1 parent 176867b commit 515c47337748992882fef2bf23b28ea6c65500aa Larry Diehl committed May 23, 2010
Showing with 80 additions and 67 deletions.
  1. +1 −1 .gitignore
  2. +4 −1 Lemmachine.agda
  3. +2 −0 Lemmachine/Default.agda
  4. +1 −1 Lemmachine/Resolve.agda
  5. +1 −1 Lemmachine/Response.agda
  6. +60 −56 Lemmachine/Runner.agda
  7. +11 −7 README.md
View
@@ -9,4 +9,4 @@
*.el
*.agdai
MAlonzo
-Runner
+Default
View
@@ -1,11 +1,14 @@
module Lemmachine where
open import Lemmachine.Request public
open import Lemmachine.Response public
-open import Lemmachine.Response.Status public
open import Lemmachine.Resource public
open import Lemmachine.Resource.Configure public
open import Lemmachine.Resolve public
open import Lemmachine.Utils public
+open import Lemmachine.Runner public
open import Data.Bool public hiding (_≟_)
open import Data.List public
+
+toApp : Hooks Application
+toApp hs = resolve (toResource hs)
View
@@ -3,3 +3,5 @@ open import Lemmachine
resource : Hooks
resource = []
+
+main = runResolve (toApp resource)
View
@@ -226,5 +226,5 @@ B13 r with Resource.serviceAvailable c r
... | true = B12 r
... | false = ServiceUnavailable
-resolve : Request Status
+resolve : Application
resolve r = B13 r
View
@@ -1,5 +1,5 @@
module Lemmachine.Response where
-open import Lemmachine.Response.Status
+open import Lemmachine.Response.Status public
open import Data.Product
open import Data.List
open import Data.String
View
@@ -1,70 +1,74 @@
module Lemmachine.Runner where
{-# IMPORT Lemmachine.FFI #-}
-open import Lemmachine
-import Lemmachine.Resource.Default as Default
+open import Lemmachine.Resource
+open import Lemmachine.Resource.Configure
+open import Lemmachine.Request
+open import Lemmachine.Response
+open import Lemmachine.Utils
+open import Lemmachine.Resolve
open import Data.Unit
open import Data.Nat
open import Data.String
open import Data.Function
open import Foreign.Haskell
open import IO.Primitive
-data Data-Request : Set where
- request :
- Method
- Version
- IP
- LocalPath
- Path
- RawPath
- PathTokens
- RequestHeaders
- Body
- Cookie
- QueryString
- Port
- Data-Request
+private
+ data Data-Request : Set where
+ request :
+ Method
+ Version
+ IP
+ LocalPath
+ Path
+ RawPath
+ PathTokens
+ RequestHeaders
+ Body
+ Cookie
+ QueryString
+ Port
+ Data-Request
-{-# COMPILED_DATA Data-Request
- Lemmachine.FFI.Request
- Lemmachine.FFI.Request
-#-}
+ {-# COMPILED_DATA Data-Request
+ Lemmachine.FFI.Request
+ Lemmachine.FFI.Request
+ #-}
-toRequest : Data-Request Request
-toRequest (request
- method
- version
- peer
- dispPath
- path
- rawPath
- pathTokens
- headers
- body
- cookie
- queryString
- port
- ) = record {
- method = method
- ; version = version
- ; peer = peer
- ; dispPath = dispPath
- ; path = path
- ; rawPath = rawPath
- ; pathTokens = pathTokens
- ; headers = headers
- ; body = body
- ; cookie = cookie
- ; queryString = queryString
- ; port = port
- }
+ toRequest : Data-Request Request
+ toRequest (request
+ method
+ version
+ peer
+ dispPath
+ path
+ rawPath
+ pathTokens
+ headers
+ body
+ cookie
+ queryString
+ port
+ ) = record {
+ method = method
+ ; version = version
+ ; peer = peer
+ ; dispPath = dispPath
+ ; path = path
+ ; rawPath = rawPath
+ ; pathTokens = pathTokens
+ ; headers = headers
+ ; body = body
+ ; cookie = cookie
+ ; queryString = queryString
+ ; port = port
+ }
-Data-resolveStatus : Resource Data-Request Status
-Data-resolveStatus res req = resolveStatus res $ toRequest req
+ Data-resolve : Application Data-Request Status
+ Data-resolve app req = app $ toRequest req
-postulate run : (Data-Request Status) IO Unit
-
-{-# COMPILED run Lemmachine.FFI.run #-}
-
-main = run $ Data-resolveStatus (toResource Default.resource)
+ postulate run : (Data-Request Status) IO Unit
+ {-# COMPILED run Lemmachine.FFI.run #-}
+runResolve : Application IO Unit
+runResolve app = run $ Data-resolve app
View
@@ -4,9 +4,9 @@ Lemmachine
Lemmachine is a REST'ful web framework that makes it easy to get HTTP right by exposing users to overridable hooks with sane defaults. The main architecture is a copy of Erlang-based [Webmachine](http://webmachine.basho.com), which is currently the best documentation reference (for hooks & general design).
Lemmachine stands out from the dynamically typed Webmachine by being written in dependently typed
-[Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php). The goal of the project is to show the advantages gained from compositional testing by taking advantage of proofs being inherently compositional. See [proofs](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Proofs.agda) for examples of universally quantified proofs (tests over all possible input values) written against the [default resource](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Resource/Default.agda), which does not override any hooks.
+[Agda](http://wiki.portal.chalmers.se/agda/pmwiki.php). The goal of the project is to show the advantages gained from compositional testing by taking advantage of proofs being inherently compositional. See [proofs](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Default/Proofs.agda) for examples of universally quantified proofs (tests over all possible input values) written against the [default resource](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Default.agda), which does not override any hooks.
-When a user implements their own resource, they can write simple lemmas ("unit tests") against the resource's hooks, but then literally reuse those lemmas to write more complex proofs ("integration tests"). For examples see some reuse of [lemmas](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Lemmas.agda) in [proofs](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Proofs.agda).
+When a user implements their own resource, they can write simple lemmas ("unit tests") against the resource's hooks, but then literally reuse those lemmas to write more complex proofs ("integration tests"). For examples see some reuse of [lemmas](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Default/Lemmas.agda) in [proofs](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Default/Proofs.agda).
The big goal is to show that in service oriented architectures, proofs of individual [middlewares](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Utils.agda) can themselves be reused to write cross-service proofs (even higher level "integration tests") for a consumer application that mounts those middlewares. See [this post](http://vision-media.ca/resources/ruby/ruby-rack-middleware-tutorial) for what is meant by middleware.
@@ -46,12 +46,11 @@ Then add this to `Agda2 Include Dirs`:
## Running ##
-Lemmachine currently supports resolving HTTP status codes (resolving
-headers & body will come later).
+Lemmachine currently supports resolving HTTP status codes (resolving headers & body will come later).
-Run the following to see this in action for [Lemmachine.Resource.Default](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Resource/Default.agda):
- agda -c -i . -i ./vendor/stdlib/src Lemmachine/Runner.agda
- ./Runner
+Run the following to see this in action for [Lemmachine.Default](http://github.com/larrytheliquid/Lemmachine/blob/master/Lemmachine/Default.agda):
+ agda -c -i . -i ./vendor/stdlib/src Lemmachine/Default.agda
+ ./Default
In a separate terminal, see a `200` response:
curl -X GET -H "Accept: text/html" -i http://localhost:3000 && echo
@@ -63,3 +62,8 @@ In a separate terminal, see a `200` response:
curl -X POST -H "Accept: text/html" -i http://localhost:3000 && echo
All of this is just default behavior and can be overridden by defining appropriate hook methods.
+
+Even though we are working in a language with a lot of verification power, the amount of code required for a complete runnable application remains competitive with more mainstream languages:
+ module ItsSoEasy where
+ open import Lemmachine
+ main = runResolve (toApp [])

0 comments on commit 515c473

Please sign in to comment.