From 95e24371f595570f58fc3cc92e8096d17e78cdeb Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 25 Jun 2020 10:48:38 +0200
Subject: [PATCH] test: final webserver demo

---
 tests/playground/webserver/Webserver.lean | 47 +++++++++++++----------
 1 file changed, 26 insertions(+), 21 deletions(-)

diff --git a/tests/playground/webserver/Webserver.lean b/tests/playground/webserver/Webserver.lean
index 1514ef829a..13bc0569ca 100644
--- a/tests/playground/webserver/Webserver.lean
+++ b/tests/playground/webserver/Webserver.lean
@@ -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>