max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: final webserver demo

Browse source
This commit is contained in:
Sebastian Ullrich 2020-06-25 10:48:38 +02:00
parent 80bb6f174d
commit 95e24371f5
1 changed files with 26 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
tests/playground/webserver/Webserver.lean
View file

@ -9,17 +9,18 @@ structure State :=
(path : String)
(status := "200 OK")
(outHeaders : Array String := #[])
(out : String := "")
(tryNextHandler := false)
abbrev HandlerM := StateT State IO
abbrev Handler := HandlerM String
abbrev Handler := HandlerM Unit
def checkVerb (verb : String) : HandlerM Unit := do
def checkVerb (verb : String) : Handler := do
st ← get;
when (st.verb != verb) $
throw $ IO.userError "invalid verb"
def checkPathLiteral (p : String) : HandlerM Unit := do
def checkPathLiteral (p : String) : Handler := do
st ← get;
if p.isPrefixOf st.path then
set { st with path := st.path.extract p.bsize st.path.bsize }
@ -32,14 +33,20 @@ let stop := st.path.posOf '/';
set { st with path := st.path.extract stop st.path.bsize };
pure $ st.path.extract 0 stop
def checkPathConsumed : HandlerM Unit := do
def checkPathConsumed : Handler := do
st ← get;
when (st.path != "") $
throw $ IO.userError "invalid path"
def write (out : String) : Handler := do
modify fun st => { st with out := st.out ++ out }
def redirect (url : String) : Handler := do
modify $ fun st => { st with status := "301 Moved Permanently", outHeaders := #["Location: " ++ url] };
pure ""
modify fun st => { st with status := "307 Temporary Redirect", outHeaders := #["Location: " ++ url] }
def notFound : Handler := do
modify fun st => { st with status := "404 Not Found" };
write "whoops"
def mkHandlersRef : IO (IO.Ref (List Handler)) :=
IO.mkRef ∅
@ -63,14 +70,15 @@ partial def run : IO.FS.Handle → IO.FS.Handle → IO Unit
| panic! "failed to parse request: " ++ line;
stderr ← IO.stderr; stderr.putStrLn $ "=> " ++ verb ++ " " ++ path;
headers ← parseHeaders hIn;
handler::handlers ← handlersRef.get | panic! "no handlers";
(out, st) ← handlers.foldl (fun h₁ h₂ => h₁ <|> h₂) handler { verb := verb, path := path };
handlers ← handlersRef.get | panic! "no handlers";
(_, st) ← handlers.foldr (fun h₁ h₂ => h₁ <|> h₂) notFound { verb := verb, path := path };
stderr ← IO.stderr; stderr.putStrLn $ "<= " ++ st.status;
hOut.putStrLn $ "HTTP/1.1 " ++ st.status;
hOut.putStrLn "Content-Type: text/html";
hOut.putStrLn $ "Content-Length: " ++ toString out.bsize;
hOut.putStrLn $ "Content-Length: " ++ toString st.out.bsize;
st.outHeaders.forM hOut.putStrLn;
hOut.putStrLn "";
hOut.putStr out;
hOut.putStr st.out;
hOut.flush;
run hIn hOut
@ -93,7 +101,7 @@ def text : Parser := -- {{{
withAntiquot (mkAntiquot "text" `LX.text) {
fn := fun c s =>
let startPos := s.pos;
let s := takeWhile1Fn (fun c => not ("{<>}$".contains c)) "HTML text" c s;
let s := takeWhile1Fn (not ∘ "{<>}$".contains) "HTML text" c s;
mkNodeToken `LX.text startPos c s } -- }}}
syntax text : child
@ -120,20 +128,19 @@ macro_rules
-- open Webserver {{{
open Webserver
-- declare_syntax_cat pathItem {{{
declare_syntax_cat pathItem
declare_syntax_cat verb
def pathLiteral : Parser := withAntiquot (mkAntiquot "pathLiteral" `pathLiteral) {
def pathLiteral : Parser := -- {{{
withAntiquot (mkAntiquot "pathLiteral" `pathLiteral) {
fn := fun c s =>
let startPos := s.pos;
let s := takeWhile1Fn (fun c => c == '/' || c.isAlphanum) "URL path" c s;
mkNodeToken `pathLiteral startPos c s }
mkNodeToken `pathLiteral startPos c s } -- }}}
declare_syntax_cat pathItem
syntax pathLiteral : pathItem
syntax "{" ident "}" : pathItem
syntax path := pathItem*
declare_syntax_cat verb
syntax "GET" : verb
syntax "POST" : verb
@ -149,11 +156,10 @@ macro v:verb p:path " => " t:term : command => do -- {{{
@[init] def reg : IO Unit := registerHandler handler)
-- }}}
-- }}}
GET / => redirect "/greet/stranger"
GET /greet/{name} => pure
GET /greet/{name} => write
<html>
<h1>Hello, {name}!</h1>
</html>
@ -164,5 +170,4 @@ def main : IO Unit := do
Webserver.run hIn hOut
-- }}}
#eval let name := "PLDI"; <h1>Hello, {name ++ name}!</h1>
#eval <h1>hi</h2>
#check let name := "PLDI"; <h1>Hello, {name}!<br/></h1>