Content-Type now filled in by framework rather than former FFI stub.

Lemmachine/FFI.hs

@@ -31,11 +31,6 @@ data Request = Request {
   queryString :: QueryString,
   port :: Port
   }
-
-data Response = Response {
-  status :: String,
-  respBody :: String
-  }
 
 toRequest :: Hack.Env -> Request
 toRequest e = Request {
@@ -54,14 +49,24 @@ toRequest e = Request {
   }
   where toHeader h = RequestHeader (fst h) (snd h)
 
+data ResponseHeader = ResponseHeader String String
+type ResponseHeaders = [ResponseHeader]
+
+data Response = Response {
+  status :: String,
+  respHeaders :: ResponseHeaders,
+  respBody :: String
+  }
+
 run :: (Request -> Response) -> IO ()
 run f = Handler.run $ return . \env -> 
   let response = f $ toRequest env in
-  Hack.Response 
-    { Hack.status = read $ status response
-    , Hack.headers = [ ("Content-Type", "text/html") ]
-    , Hack.body = pack $ respBody response
+  Hack.Response { 
+    Hack.status = read $ status response,
+    Hack.headers = map fromHeader $ respHeaders response, 
+    Hack.body = pack $ respBody response
     }
+    where fromHeader (ResponseHeader k v) = (k , v)
 
 
 

Lemmachine/Resolve.agda

@@ -1,7 +1,7 @@
 open import Lemmachine.Resource
 module Lemmachine.Resolve (c : Resource) where
 open import Lemmachine.Request
-open import Lemmachine.Response.Status
+open import Lemmachine.Response
 open import Lemmachine.Utils
 open import Data.Bool
 open import Data.Nat
@@ -165,10 +165,10 @@ D4+D5 r with fetchHeader "Accept-Language" (Request.headers r)
 C3+C4 : Request → Status
 C3+C4 r with fetchHeader "Accept" (Request.headers r)
 ... | nothing = D4+D5 r
-... | just contentType with any (_==_ contentType) 
-                                (Resource.contentTypesProvided c r)
-... | true  = D4+D5 r
-... | false = NotAcceptable
+... | just contentType with fetchContentType contentType
+                              (Resource.contentTypesProvided c r)
+... | just _  = D4+D5 r
+... | nothing = NotAcceptable
 
 B3 : Request → Status
 B3 r with eqMethod (Request.method r) OPTIONS
@@ -233,7 +233,10 @@ resolveStatus r = B13 r
 resolve : Application
 resolve r = record {
     status = s
-  ; headers = []
-  ; body = Resource.body c s 
+  ; headers = hs $ fetchAccept (Request.headers r) (Resource.contentTypesProvided c r)
+  ; body = Resource.body c s
   } where
   s = resolveStatus r
+  hs : Maybe String → List ResponseHeader
+  hs (just s) = [ "Content-Type" , s ]
+  hs nothing = []

Lemmachine/Response.agda

@@ -5,12 +5,20 @@ open import Data.List hiding (_++_)
 open import Data.Nat
 open import Data.String
 
-ResponseHeader = String × String
+data ResponseHeader : Set where
+  _,_ : String → String → ResponseHeader
+
+{-# COMPILED_DATA ResponseHeader
+    Lemmachine.FFI.ResponseHeader
+    Lemmachine.FFI.ResponseHeader
+#-}
+
+ResponseHeaders = List ResponseHeader
 
 record Response : Set where 
   field 
     status : Status
-    headers : List ResponseHeader
+    headers : ResponseHeaders
     body : String
 
 showStatus : Status → String

Lemmachine/Runner.agda

@@ -65,7 +65,7 @@ private
     }
 
   data Data-Response : Set where
-    response : String → String → Data-Response
+    response : String → ResponseHeaders → String → Data-Response
 
   {-# COMPILED_DATA Data-Response
       Lemmachine.FFI.Response 
@@ -75,6 +75,7 @@ private
   fromResponse : Response → Data-Response
   fromResponse resp = response
     (showStatus $ Response.status resp)
+    (Response.headers resp)
     (Response.body resp)
 
   Data-resolve : Application → Data-Request → Data-Response

Lemmachine/Utils.agda

@@ -19,12 +19,6 @@ fetch x xs with any (_≟_ x ∘ proj₁) xs
 ... | yes p = just (proj₂ (proj₁ (find p)))
 ... | no _ = nothing
 
-fetchContentType : String → List (String × String) → Maybe String
-fetchContentType _ [] = nothing
-fetchContentType "*" (x ∷ _) = just (proj₂ x)
-fetchContentType "*/*" (x ∷ _) = just (proj₂ x)
-fetchContentType c (x ∷ xs) = fetch c (x ∷ xs)
-
 private
   fromHeaders : RequestHeaders → List (String × String)
   fromHeaders xs = Data.List.map f xs where
@@ -36,6 +30,20 @@ fetchHeader x xs with any (_≟_ x ∘ headerKey) xs
 ... | yes p = just (headerValue (proj₁ (find p)))
 ... | no _ = nothing
 
+fetchContentType : String → List String → Maybe String
+fetchContentType _ [] = nothing
+fetchContentType "*" (y ∷ _) = just y
+fetchContentType "*/*" (y ∷ _) = just y
+fetchContentType x (y ∷ ys) with x == y
+... | true = just y
+... | false = fetchContentType x ys
+
+fetchAccept : RequestHeaders → List String → Maybe String
+fetchAccept hs cs with fetchHeader "Accept" hs
+fetchAccept hs _ | nothing = nothing
+fetchAccept _ [] | just _ = nothing
+fetchAccept _ xss | just y = fetchContentType y xss
+
 postulate
   isDate : String → Bool
   isModified : String → String → Bool

README.md

@@ -16,7 +16,7 @@ Lemmachine currently uses the Haskell [Hack](http://github.com/nfjinjing/hack) a
 
 ## Status ##
 
-This project is still very much an early-stage work in progress, without guarantees for API stability. It currently only renders response statuses (not headers or body). Lemmas and proofs exist for the status resolution, and now there is a real runner hardcoded against the default resource!
+The project is still in development and rapidly changing. Lemmas and proofs exist for status resolution, and you can now run resources! The focus will now comprise of a gradual direct translation of RFC 2616 sections into dependent type theory.
 
 ## Setup ##
 
@@ -46,8 +46,6 @@ Then add this to `Agda2 Include Dirs`:
 
 ## Running ##
 
-Lemmachine currently supports resolving HTTP status codes (resolving headers & body will come later).
-
 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