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

test: Webserver: maybe-final version

Browse source
This commit is contained in:
Sebastian Ullrich 2020-06-17 17:37:08 +02:00
parent 3c547db67c
commit fff0cdc0ec
2 changed files with 33 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/playground/webserver/README.md
View file

@ -10,7 +10,7 @@ Content-Length: 19
<h1>Hello, me!</h1>
```
Use with e.g. GNU netcat to test in a browser:
Use with netcat to test in a browser at http://localhost:1234:
```bash
$ nix-shell -p netcat-gnu --run "nc -lp 1234 -e ./build/bin/Webserver"
bash -c 'coproc nc -lp 1234; ./build/bin/Webserver <&${COPROC[0]} >&${COPROC[1]}'
```

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

@ -1,4 +1,7 @@
-- -*- origami-fold-style: triple-braces -*-
import Lean
-- namespace Webserver {{{
namespace Webserver
structure State :=
@ -58,6 +61,7 @@ partial def run : IO.FS.Handle → IO.FS.Handle → IO Unit
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;
handler::handlers ← handlersRef.get | panic! "no handlers";
(out, st) ← handlers.foldl (fun h₁ h₂ => h₁ <|> h₂) handler { verb := verb, path := path };
@ -71,13 +75,13 @@ partial def run : IO.FS.Handle → IO.FS.Handle → IO Unit
run hIn hOut
end Webserver
--}}}
new_frontend
open Lean
open Lean.Parser
namespace LX
-- declare_syntax_cat element {{{
declare_syntax_cat element
declare_syntax_cat child
@ -85,21 +89,22 @@ syntax "<" ident "/>" : element
syntax "<" ident ">" child* "</" ident ">" : element
-- "JSXTextCharacter : SourceCharacter but not one of {, <, > or }"
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;
mkNodeToken `LX.text startPos c s }
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;
mkNodeToken `LX.text startPos c s } -- }}}
syntax text : child
syntax "{" term "}" : child
syntax element : child
syntax text : child
syntax element : term
macro_rules
| `(<$n/>) => mkStxStrLit ("<" ++ toString n.getId ++ ">")
| `(<$n>$cs*</$m>) =>
| `(<$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!
@ -109,20 +114,13 @@ macro_rules
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 ++ ">")
-- }}}
-- }}}
end LX
#eval
let name := "PLDI";
<html>
<h1>Hello, {name}!</h1>
<button/>
</html>
--#eval <h1>oh no</h2>
-- open Webserver {{{
open Webserver
-- declare_syntax_cat pathItem {{{
declare_syntax_cat pathItem
declare_syntax_cat verb
@ -139,22 +137,22 @@ syntax path := pathItem*
syntax "GET" : verb
syntax "POST" : verb
macro v:verb p:path " => " t:term : command => do
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;
`(
def handler : Handler := do
checkVerb $(mkStxStrLit (v.getArg 0).getAtomVal!);
$t:term
`(def handler : Handler := do
checkVerb $(mkStxStrLit (v.getArg 0).getAtomVal!);
$t:term
@[init] def reg : IO Unit := registerHandler handler
)
@[init] def reg : IO Unit := registerHandler handler)
-- }}}
-- }}}
GET / => redirect "/greet/stranger"
GET / =>
redirect "/greet/stranger"
GET /greet/{name} => pure
<html>
<h1>Hello, {name}!</h1>
@ -164,3 +162,7 @@ def main : IO Unit := do
hIn ← IO.stdin;
hOut ← IO.stdout;
Webserver.run hIn hOut
-- }}}
#eval let name := "PLDI"; <h1>Hello, {name ++ name}!</h1>
#eval <h1>hi</h2>