Agda -> Hack Status passover

.gitignore

@@ -8,3 +8,5 @@
 *.flymake
 *.el
 *.agdai
+MAlonzo
+Runner

FFI.hs

@@ -0,0 +1,45 @@
+module FFI where
+import Hack
+import Hack.Handler.Happstack as Handler
+import Data.ByteString.Lazy.Char8 (pack)
+
+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
+
+fromStatus :: Status -> Int
+fromStatus OK = 200
+fromStatus Created = 201
+fromStatus Accepted = 202
+fromStatus NoContent = 204
+fromStatus MultipleChoices = 300
+fromStatus MovedPermanently = 301
+fromStatus SeeOther = 303
+fromStatus NotModified = 304
+fromStatus MovedTemporarily = 307
+fromStatus BadRequest = 400
+fromStatus Unauthorized = 401
+fromStatus Forbidden = 403
+fromStatus NotFound = 404
+fromStatus MethodNotAllowed = 405
+fromStatus NotAcceptable = 406
+fromStatus Conflict = 409
+fromStatus Gone = 410
+fromStatus PreconditionFailed = 412
+fromStatus RequestEntityTooLarge = 413
+fromStatus RequestURItooLong = 414
+fromStatus UnsupportedMediaType = 415
+fromStatus NotImplemented = 501
+fromStatus ServiceUnavailable = 503
+
+run :: Status -> IO ()
+run status = Handler.run $ return . \env -> Response 
+    { status  = code
+    , headers = [ ("Content-Type", "text/plain") ]
+    , body    = pack ("This HTTP status (" ++ show code ++ ") is brought to you by Lemmachine!")
+    }
+      where code = fromStatus status

Lemmachine.agda

@@ -4,6 +4,7 @@ open import Lemmachine.Response public
 open import Lemmachine.Response.Status public
 open import Lemmachine.Resource public
 open import Lemmachine.Resource.Universe public
+open import Lemmachine.Resource.Configure public
 open import Lemmachine.Resolve public
 open import Lemmachine.Utils public
 

Lemmachine/Lemmas.agda

@@ -1,6 +1,5 @@
 open import Lemmachine
 module Lemmachine.Lemmas (properties : Properties) where
-open import Lemmachine.Resource.Configure
 open import Data.Empty
 open import Data.String
 open import Data.Maybe

Lemmachine/Response/Status.agda

@@ -14,27 +14,12 @@ data Status : Set where
   -- 5xx: Server Error - The server failed to fulfill an apparently valid request
   NotImplemented ServiceUnavailable : Status
 
-toℕ : Status → ℕ
-toℕ OK = 200
-toℕ Created = 201
-toℕ Accepted = 202
-toℕ NoContent = 204
-toℕ MultipleChoices = 300
-toℕ MovedPermanently = 301
-toℕ SeeOther = 303
-toℕ NotModified = 304
-toℕ MovedTemporarily = 307
-toℕ BadRequest = 400
-toℕ Unauthorized = 401
-toℕ Forbidden = 403
-toℕ NotFound = 404
-toℕ MethodNotAllowed = 405
-toℕ NotAcceptable = 406
-toℕ Conflict = 409
-toℕ Gone = 410
-toℕ PreconditionFailed = 412
-toℕ RequestEntityTooLarge = 413
-toℕ RequestURItooLong = 414
-toℕ UnsupportedMediaType = 415
-toℕ NotImplemented = 501
-toℕ ServiceUnavailable = 503
+{-# IMPORT FFI #-}
+{-# COMPILED_DATA Status FFI.Status
+    FFI.OK FFI.Created FFI.Accepted FFI.NoContent
+    FFI.MultipleChoices FFI.MovedPermanently FFI.SeeOther FFI.NotModified FFI.MovedTemporarily
+    FFI.BadRequest FFI.Unauthorized FFI.Forbidden FFI.NotFound FFI.MethodNotAllowed 
+    FFI.NotAcceptable FFI.Conflict FFI.Gone FFI.PreconditionFailed
+    FFI.RequestEntityTooLarge FFI.RequestURItooLong FFI.UnsupportedMediaType
+    FFI.NotImplemented FFI.ServiceUnavailable
+#-}

Lemmachine/Runner.agda

@@ -0,0 +1,15 @@
+module Lemmachine.Runner where
+open import Lemmachine
+import Lemmachine.Resource.Default as Default
+open import Data.Unit
+open import Data.Nat
+open import Data.String
+open import Foreign.Haskell
+open import IO.Primitive
+
+{-# IMPORT FFI #-}
+postulate run : Status → IO Unit
+{-# COMPILED run FFI.run #-}
+
+main = run OK -- (resolve (toResource Default.resource))
+