chore: update webserver demo
This commit is contained in:
Wojciech Nawrocki
Sebastian Ullrich
parent
eef413cec8
commit
7374b9ba45
1 changed files with 87 additions and 77 deletions
|
|
@ -5,81 +5,80 @@ import Lean
|
|||
namespace Webserver
|
||||
|
||||
structure State :=
|
||||
(verb : String)
|
||||
(path : String)
|
||||
(status := "200 OK")
|
||||
(outHeaders : Array String := #[])
|
||||
(out : String := "")
|
||||
(tryNextHandler := false)
|
||||
(verb : String)
|
||||
(path : String)
|
||||
(status := "200 OK")
|
||||
(outHeaders : Array String := #[])
|
||||
(out : String := "")
|
||||
(tryNextHandler := false)
|
||||
|
||||
abbrev HandlerM := StateT State IO
|
||||
abbrev Handler := HandlerM Unit
|
||||
|
||||
def checkVerb (verb : String) : Handler := do
|
||||
st ← get;
|
||||
when (st.verb != verb) $
|
||||
throw $ IO.userError "invalid verb"
|
||||
let st ← get
|
||||
if st.verb != verb then
|
||||
throw $ IO.userError "invalid verb"
|
||||
|
||||
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 }
|
||||
else
|
||||
throw $ IO.userError "invalid path"
|
||||
let st ← get
|
||||
if p.isPrefixOf st.path then
|
||||
set { st with path := st.path.extract p.bsize st.path.bsize }
|
||||
else
|
||||
throw $ IO.userError "invalid path"
|
||||
|
||||
def getPathPart : HandlerM String := do
|
||||
st ← get;
|
||||
let stop := st.path.posOf '/';
|
||||
set { st with path := st.path.extract stop st.path.bsize };
|
||||
pure $ st.path.extract 0 stop
|
||||
let st ← get
|
||||
let stop := st.path.posOf '/'
|
||||
set { st with path := st.path.extract stop st.path.bsize }
|
||||
pure $ st.path.extract 0 stop
|
||||
|
||||
def checkPathConsumed : Handler := do
|
||||
st ← get;
|
||||
when (st.path != "") $
|
||||
throw $ IO.userError "invalid path"
|
||||
let st ← get
|
||||
if st.path != "" then
|
||||
throw $ IO.userError "invalid path"
|
||||
|
||||
def write (out : String) : Handler := do
|
||||
modify fun st => { st with out := st.out ++ out }
|
||||
modify fun st => { st with out := st.out ++ out }
|
||||
|
||||
def redirect (url : String) : Handler := do
|
||||
modify fun st => { st with status := "307 Temporary Redirect", outHeaders := #["Location: " ++ url] }
|
||||
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"
|
||||
modify fun st => { st with status := "404 Not Found" }
|
||||
write "whoops"
|
||||
|
||||
def mkHandlersRef : IO (IO.Ref (List Handler)) :=
|
||||
IO.mkRef ∅
|
||||
IO.mkRef ∅
|
||||
|
||||
@[init mkHandlersRef]
|
||||
constant handlersRef : IO.Ref (List Handler) := arbitrary _
|
||||
constant handlersRef : IO.Ref (List Handler)
|
||||
|
||||
def registerHandler (h : Handler) : IO Unit := do
|
||||
handlersRef.modify fun hs => h::hs
|
||||
handlersRef.modify fun hs => h::hs
|
||||
|
||||
partial def parseHeaders : IO.FS.Handle → IO Unit
|
||||
| hIn => do
|
||||
line ← hIn.getLine;
|
||||
partial def parseHeaders (hIn : IO.FS.Stream) : IO Unit := do
|
||||
let line ← hIn.getLine
|
||||
if line == "" || line == "\r\n" then pure () else parseHeaders hIn
|
||||
|
||||
partial def run : IO.FS.Handle → IO.FS.Handle → IO Unit
|
||||
| hIn, hOut => do
|
||||
line ← hIn.getLine;
|
||||
when (line != "") do
|
||||
[verb, path, proto] ← pure $ line.splitOn " "
|
||||
| panic! "failed to parse request: " ++ line;
|
||||
stderr ← IO.stderr; stderr.putStrLn $ "=> " ++ verb ++ " " ++ path;
|
||||
headers ← parseHeaders hIn;
|
||||
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 st.out.bsize;
|
||||
st.outHeaders.forM hOut.putStrLn;
|
||||
hOut.putStrLn "";
|
||||
hOut.putStr st.out;
|
||||
hOut.flush;
|
||||
partial def run (hIn hOut : IO.FS.Stream) : IO Unit := do
|
||||
let line ← hIn.getLine
|
||||
if line != "" then
|
||||
let [verb, path, proto] ← line.splitOn " "
|
||||
| panic! "failed to parse request: " ++ line
|
||||
let stderr ← IO.getStderr
|
||||
stderr.putStrLn $ "=> " ++ verb ++ " " ++ path
|
||||
let headers ← parseHeaders hIn
|
||||
let handlers ← handlersRef.get
|
||||
let (_, st) ← handlers.foldr (· <|> ·) notFound { verb, path }
|
||||
stderr.putStrLn $ "<= " ++ st.status
|
||||
hOut.putStrLn $ "HTTP/1.1 " ++ st.status
|
||||
hOut.putStrLn "Content-Type: text/html"
|
||||
hOut.putStrLn $ "Content-Length: " ++ toString st.out.bsize
|
||||
st.outHeaders.forM hOut.putStrLn
|
||||
hOut.putStrLn ""
|
||||
hOut.putStr st.out
|
||||
hOut.flush
|
||||
run hIn hOut
|
||||
|
||||
end Webserver
|
||||
|
|
@ -88,6 +87,7 @@ end Webserver
|
|||
|
||||
open Lean
|
||||
open Lean.Parser
|
||||
open Lean.PrettyPrinter
|
||||
|
||||
-- declare_syntax_cat element {{{
|
||||
declare_syntax_cat element
|
||||
|
|
@ -100,28 +100,31 @@ syntax "<" ident ">" child* "</" ident ">" : element
|
|||
def text : Parser := -- {{{
|
||||
withAntiquot (mkAntiquot "text" `LX.text) {
|
||||
fn := fun c s =>
|
||||
let startPos := s.pos;
|
||||
let s := takeWhile1Fn (not ∘ "{<>}$".contains) "HTML text" c s;
|
||||
let startPos := s.pos
|
||||
let s := takeWhile1Fn (not ∘ "{<>}$".contains) "HTML text" c s
|
||||
mkNodeToken `LX.text startPos c s } -- }}}
|
||||
|
||||
@[combinatorFormatter text] def text.formatter : Formatter := pure ()
|
||||
@[combinatorParenthesizer text] def text.parenthesizer : Parenthesizer := pure ()
|
||||
|
||||
syntax text : child
|
||||
syntax "{" term "}" : child
|
||||
syntax element : child
|
||||
|
||||
syntax element : term
|
||||
syntax:max element : term
|
||||
|
||||
macro_rules
|
||||
| `(<$n/>) => mkStxStrLit ("<" ++ toString n.getId ++ ">")
|
||||
| `(<$n>$cs*</$m>) => -- {{{
|
||||
if n.getId == m.getId then do
|
||||
cs ← cs.mapM fun c => match_syntax c with
|
||||
| `(child|$t:text) => pure $ mkStxStrLit (t.getArg 0).getAtomVal!
|
||||
| `(child|{$t}) => pure t
|
||||
| `(child|$e:element) => `($e:element)
|
||||
| _ => unreachable!;
|
||||
let cs := cs.push (mkStxStrLit ("</" ++ toString m.getId ++ ">"));
|
||||
cs.foldlM (fun s e => `($s ++ $e)) (mkStxStrLit ("<" ++ toString n.getId ++ ">"))
|
||||
else Macro.throwError m ("expected </" ++ toString n.getId ++ ">")
|
||||
| `(<$n/>) => quote ("<" ++ toString n.getId ++ "/>")
|
||||
| `(<$n>$cs*</$m>) => -- {{{
|
||||
if n.getId == m.getId then do
|
||||
let cs ← cs.mapM fun c => match c with
|
||||
| `(child|$t:text) => pure $ quote t[0].getAtomVal!
|
||||
| `(child|{$t}) => pure t
|
||||
| `(child|$e:element) => `($e:element)
|
||||
| _ => unreachable!
|
||||
let cs := cs.push (quote ("</" ++ toString m.getId ++ ">"))
|
||||
cs.foldlM (fun s e => `($s ++ $e)) (quote ("<" ++ toString n.getId ++ ">"))
|
||||
else Macro.throwError ("expected </" ++ toString n.getId ++ ">")
|
||||
-- }}}
|
||||
-- }}}
|
||||
|
||||
|
|
@ -131,43 +134,50 @@ open Webserver
|
|||
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;
|
||||
let startPos := s.pos
|
||||
let s := takeWhile1Fn (fun c => c == '/' || c.isAlphanum) "URL path" c s
|
||||
mkNodeToken `pathLiteral startPos c s } -- }}}
|
||||
|
||||
@[combinatorFormatter pathLiteral] def pathLiteral.formatter : Formatter := pure ()
|
||||
@[combinatorParenthesizer pathLiteral] def pathLiteral.parenthesizer : Parenthesizer := pure ()
|
||||
|
||||
declare_syntax_cat pathItem
|
||||
syntax pathLiteral : pathItem
|
||||
syntax "{" ident "}" : pathItem
|
||||
syntax path := pathItem*
|
||||
declare_syntax_cat path
|
||||
syntax pathItem* : path
|
||||
|
||||
declare_syntax_cat verb
|
||||
syntax "GET" : verb
|
||||
syntax "POST" : verb
|
||||
|
||||
macro v:verb p:path " => " t:term : command => do -- {{{
|
||||
t ← `(do checkPathConsumed; $t:term);
|
||||
t ← p.getArgs.foldrM (fun pi t => match_syntax pi with
|
||||
| `(pathItem|$l:pathLiteral) => `(do checkPathLiteral $(mkStxStrLit (l.getArg 0).getAtomVal!); $t:term)
|
||||
| `(pathItem|{$id}) => `(do $id:ident ← getPathPart; $t:term)
|
||||
| _ => unreachable!) t;
|
||||
let `(path| $[$pis:pathItem]* ) ← p
|
||||
| unreachable!
|
||||
let t ← `(do checkPathConsumed; $t:term)
|
||||
let t ← pis.foldrM (fun pi t => match pi with
|
||||
| `(pathItem|$l:pathLiteral) => `(do checkPathLiteral $(quote l[0].getAtomVal!); $t:term)
|
||||
| `(pathItem|{$id}) => `(do let $id:ident ← getPathPart; $t:term)
|
||||
| _ => Macro.throwError s!"unknown pathItem '{Syntax.formatStx pi}'") t
|
||||
`(def handler : Handler := do
|
||||
checkVerb $(mkStxStrLit (v.getArg 0).getAtomVal!);
|
||||
$t:term
|
||||
checkVerb $(quote v[0].getAtomVal!)
|
||||
$t:term
|
||||
|
||||
@[init] def reg : IO Unit := registerHandler handler)
|
||||
-- }}}
|
||||
|
||||
GET / => redirect "/greet/stranger"
|
||||
|
||||
GET /greet/{name} => write
|
||||
GET /greet/{name} => write
|
||||
<html>
|
||||
<h1>Hello, {name}!</h1>
|
||||
</html>
|
||||
|
||||
def main : IO Unit := do
|
||||
hIn ← IO.stdin;
|
||||
hOut ← IO.stdout;
|
||||
let hIn ← IO.getStdin
|
||||
let hOut ← IO.getStdout
|
||||
Webserver.run hIn hOut
|
||||
-- }}}
|
||||
|
||||
#check let name := "PLDI"; <h1>Hello, {name}!<br/></h1>
|
||||
#check let name := "PLDI"
|
||||
(<h1>Hello, {name}!</h1>)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue