From ade961bcf35fcde834605f3c8abf47f805f7bcff Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 16 Jun 2020 22:09:18 +0200 Subject: [PATCH] test: webserver demo --- tests/playground/webserver/README.md | 16 ++ tests/playground/webserver/Webserver.lean | 184 ++++++++++++++++++++++ 2 files changed, 200 insertions(+) create mode 100644 tests/playground/webserver/README.md create mode 100644 tests/playground/webserver/Webserver.lean diff --git a/tests/playground/webserver/README.md b/tests/playground/webserver/README.md new file mode 100644 index 0000000000..0e63822b82 --- /dev/null +++ b/tests/playground/webserver/README.md @@ -0,0 +1,16 @@ +Example of a super-simple web server using custom syntax for registering routes and emitting HTML + +Compile with `leanmake bin` to get the `./build/bin/Webserver` executable listening on stdin and +responding on stdout: +```bash +$ echo "GET /greet/me HTTP/1.1" | ./build/bin/Webserver +HTTP/1.1 200 OK +Content-Type: text/html +Content-Length: 19 + +

Hello, me!

+``` +Use with e.g. GNU netcat to test in a browser: +```bash +$ nix-shell -p netcat-gnu --run "nc -lp 1234 -e ./build/bin/Webserver" +``` diff --git a/tests/playground/webserver/Webserver.lean b/tests/playground/webserver/Webserver.lean new file mode 100644 index 0000000000..e3e426a71c --- /dev/null +++ b/tests/playground/webserver/Webserver.lean @@ -0,0 +1,184 @@ +import Lean +namespace Webserver + +structure State := +(verb : String) +(path : String) +(status := "200 OK") +(outHeaders : Array String := #[]) +(tryNextHandler := false) + +abbrev HandlerM := StateT State IO +abbrev Handler := HandlerM String + +def checkVerb (verb : String) : HandlerM Unit := do +st ← get; +when (st.verb != verb) $ + throw $ IO.userError "invalid verb" + +def checkPathLiteral (p : String) : HandlerM Unit := 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" + +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 + +def checkPathConsumed : HandlerM Unit := do +st ← get; +when (st.path != "") $ + throw $ IO.userError "invalid path" + +def redirect (url : String) : Handler := do +modify $ fun st => { st with status := "301 Moved Permanently", outHeaders := #["Location: " ++ url] }; +pure "" + +def mkHandlersRef : IO (IO.Ref (List Handler)) := +IO.mkRef ∅ + +@[init mkHandlersRef] +constant handlersRef : IO.Ref (List Handler) := arbitrary _ + +def registerHandler (h : Handler) : IO Unit := do +handlersRef.modify fun hs => h::hs + +partial def parseHeaders : IO.FS.Handle → IO Unit +| hIn => do + 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; + headers ← parseHeaders hIn; + handler::handlers ← handlersRef.get | panic! "no handlers"; + (out, st) ← handlers.foldl (fun h₁ h₂ => h₁ <|> h₂) handler { verb := verb, path := path }; + hOut.putStrLn $ "HTTP/1.1 " ++ st.status; + hOut.putStrLn "Content-Type: text/html"; + hOut.putStrLn $ "Content-Length: " ++ toString out.bsize; + st.outHeaders.forM hOut.putStrLn; + hOut.putStrLn ""; + hOut.putStr out; + hOut.flush; + run hIn hOut + +end Webserver + +new_frontend +open Lean + +namespace Prelim +open Lean.Parser + +-- for declaring simple parsers I can still use within other `syntax` +@[commandParser] def syntaxAbbrev := parser! symbol "syntax " >> ident >> symbol " := " >> many1 syntaxParser +@[macro Prelim.syntaxAbbrev] def elabSyntaxAbbrev : Macro := +fun stx => match_syntax stx with +| `(syntax $id := $p*) => `(declare_syntax_cat $id syntax:0 $p* : $id) +| _ => Macro.throwUnsupported + +-- "JSXTextCharacter : SourceCharacter but not one of {, <, > or }" +def text : Parser := { + fn := fun c s => + let startPos := s.pos; + let s := takeWhile1Fn (fun c => not ("{<>}$".contains c)) "HTML text" c s; + mkNodeToken `LX.text startPos c s } + +def pathLiteral : Parser := { + 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 } + +end Prelim + +-- HACK: get `text` into `syntax` world +declare_syntax_cat text +@[textParser] def text := Prelim.text + +declare_syntax_cat pathLiteral +@[pathLiteralParser] def pathLiteral := Prelim.pathLiteral + +namespace LX + +declare_syntax_cat element +declare_syntax_cat child + +syntax "<" ident "/>" : element +syntax "<" ident ">" child* "" : element + +syntax text : child +syntax element : child +syntax "{" term "}" : child + +syntax element : term + +macro_rules +| `(<$n/>) => mkStxStrLit ("<" ++ toString n.getId ++ ">") +| `(<$n>$cs*) => + 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 ("")); + cs.foldlM (fun s e => `($s ++ $e)) (mkStxStrLit ("<" ++ toString n.getId ++ ">")) + else Macro.throwError m ("expected ") + +end LX + +#eval + let name := "PLDI"; + +

Hello, {name}!

+