From 7374b9ba45921140939fccadce6d1adf78da16a2 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Sat, 10 Jul 2021 16:38:32 -0700
Subject: [PATCH] chore: update webserver demo

---
 tests/playground/webserver/Webserver.lean | 164 ++++++++++++----------
 1 file changed, 87 insertions(+), 77 deletions(-)

diff --git a/tests/playground/webserver/Webserver.lean b/tests/playground/webserver/Webserver.lean
index 71e716b6b5..55dafc7e9c 100644
--- a/tests/playground/webserver/Webserver.lean
+++ b/tests/playground/webserver/Webserver.lean
@@ -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>)