-
Notifications
You must be signed in to change notification settings - Fork 10
/
Copy pathMain.lean
67 lines (57 loc) · 1.77 KB
/
Main.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
import Socket
def mkSocketV4: IO (Socket × Socket.SockAddr) := do
let sock ← Socket.mk .inet .stream
pure (sock, Socket.SockAddr4.v4 (.mk 127 0 0 1) 8888)
def mkSocketV6: IO (Socket × Socket.SockAddr) := do
let sock ← Socket.mk .inet6 .stream
pure (sock, Socket.SockAddr6.v6 (.mk 0 0 0 0 0 0 0 1) 8888)
def mkSocketUnix: IO (Socket × Socket.SockAddr) := do
let sock ← Socket.mk .unix .stream
pure (sock, Socket.SockAddrUnix.unix "./unix.addr")
def client (arg : String) (input : Socket × Socket.SockAddr): IO Unit := do
let (sock, sa) := input
sock.connect sa
let bytes := arg.toUTF8
let _ ← sock.send bytes
let recv ← sock.recv 4096
if recv.size == 0 then
return ()
let str := String.fromUTF8! recv
assert! str == arg
def handle (client : Socket) : IO Unit := do
let recv ← client.recv 4096
if recv.size == 0 then
return ()
let _ ← client.send recv
IO.println "Done handling"
def server (input : Socket × Socket.SockAddr) : IO Unit := do
let (sock, sa) := input
sock.bind sa
sock.listen 1
while true do
let (client, _sa) ← sock.accept
handle client
return ()
def main (args : List String) : IO Unit := do
let mode := args.get! 0
if mode == "client" then do
let type := args.get! 1
if type == "v4" then
mkSocketV4 >>= client (args.get! 2)
else if type == "v6" then
mkSocketV6 >>= client (args.get! 2)
else if type == "unix" then
mkSocketUnix >>= client (args.get! 2)
else
mkSocketV4 >>= client type
else if mode == "server" then
let type := args.get! 1
if type == "unix" then
mkSocketUnix >>= server
else if type == "v6" then
mkSocketV6 >>= server
else
mkSocketV4 >>= server
else
IO.println "Unknown mode"
return ()