63 lines
2.3 KiB
Plaintext
63 lines
2.3 KiB
Plaintext
module basic where
|
||
|
||
open import Agda.Primitive renaming (Set to Type)
|
||
open import Agda.Builtin.Float
|
||
open import Agda.Builtin.String
|
||
open import Agda.Builtin.IO
|
||
open import Agda.Builtin.Unit
|
||
|
||
postulate
|
||
HTTPModule : Type
|
||
http : HTTPModule
|
||
HTTPServer : Type
|
||
HTTPReq : Type
|
||
HTTPRes : Type
|
||
modify : Type → Type
|
||
modLog : {A : Type} → modify A
|
||
setStatusCode : Float → modify HTTPRes
|
||
setHeader : String → String → modify HTTPRes
|
||
setEnd : String → modify HTTPRes
|
||
pure : {A : Type} → A → modify A
|
||
_>>=_ : {A : Type} → modify A → (A → modify A) → modify A
|
||
_>>_ : {A : Type} → modify A → modify A → modify A
|
||
createServer : HTTPModule → (HTTPReq → modify HTTPRes) → HTTPServer
|
||
serverListen : HTTPServer → Float → String → IO ⊤ → IO ⊤
|
||
doNothing : IO ⊤
|
||
putStrLn : String → IO ⊤
|
||
|
||
{-# COMPILE JS putStrLn = (str) => { console.log(str); } #-}
|
||
|
||
{-# COMPILE JS http = require('http') #-}
|
||
|
||
{-# COMPILE JS setStatusCode = ((float) => { return (res) => { res.statusCode = float; }}) #-}
|
||
{-# COMPILE JS setHeader = ((header) => { return (content) => { return (res) => { res.setHeader(header, content); }}}) #-}
|
||
{-# COMPILE JS setEnd = ((content) => { return (res) => { res.end(content); }}) #-}
|
||
|
||
{-# COMPILE JS modLog = ((a) => { return (res) => { console.log(res); }}) #-}
|
||
{-# COMPILE JS pure = ((a) => { return (res) => { return structuredClone(a); }}) #-}
|
||
{-# COMPILE JS _>>=_ = ((a) => { return (ma) => { return (amb) => { return (res) => { amb(ma(res)); }}}}) #-}
|
||
{-# COMPILE JS _>>_ = ((a) => { return (ma) => { return (mb) => { return (res) => { ma(res); mb(res); }}}}) #-}
|
||
|
||
{-# COMPILE JS createServer = ((http) => { return (handler) => { return http.createServer((req, res) => { handler(req)(res); }); }}) #-}
|
||
{-# COMPILE JS serverListen = ((serv) => { return (port) => { return (host) => { return (action) => { return () => { serv.listen(port, host, action) }}}}}) #-}
|
||
|
||
{-# COMPILE JS doNothing = (() => {}) #-}
|
||
|
||
port : Float
|
||
port = 3000.0
|
||
|
||
hostname : String
|
||
hostname = "localhost"
|
||
|
||
handleReg : modify HTTPRes
|
||
handleReg = do
|
||
setStatusCode 200.0
|
||
setHeader "Content-Type" "text/plain"
|
||
setEnd "Hello World"
|
||
|
||
server : HTTPServer
|
||
server = createServer http (λ _ → handleReg)
|
||
|
||
main : IO ⊤
|
||
main = serverListen server port hostname (putStrLn "served request")
|