From fa863817c02e5a1dfe99312b91ea69888dd39f87 Mon Sep 17 00:00:00 2001
From: Bernd Losert <berndlosert@gmail.com>
Date: Tue, 12 Dec 2023 23:20:52 +0000
Subject: [PATCH] WIP

---
 README.md                 | 35 +++--------------------------------
 examples/echo-server.agda |  2 ++
 2 files changed, 5 insertions(+), 32 deletions(-)

diff --git a/README.md b/README.md
index ae7eb016..cb462750 100644
--- a/README.md
+++ b/README.md
@@ -68,6 +68,8 @@ rm -rf /usr/local/share/emacs/site-lisp/agda
 Save the following code into a file called `hello.agda`.
 
 ```agda
+{-# OPTIONS --guardedness #-}
+
 open import Prelude
 open import System.IO
 
@@ -85,38 +87,7 @@ agda --compile hello.agda
 
 Save the following code into a file called `echo-server.agda`:
 
-```agda
-{-# OPTIONS --guardedness #-}
-
-open import Prelude
-
-open import Data.Bytes as Bytes using ()
-open import Data.List as List using ()
-open import Data.String.Encoding
-open import Network.Socket
-open import System.IO
-
-runTCPEchoServer : IO Unit
-runTCPEchoServer = do
-  (serverAddr , _) <- getAddrInfo nothing (just "127.0.0.1") (just "7000")
-  serverSocket <- socket (addrFamily serverAddr) sockStream defaultProtocol
-  setSocketOption serverSocket reuseAddr 1
-  bind serverSocket (addrAddress serverAddr)
-  listen serverSocket 1
-  (clientSocket , _) <- accept serverSocket
-  print {String} "Waiting for a message..."
-  message <- recv clientSocket 1024
-  unless (Bytes.null message) do
-    print ("Received: " <> decodeUtf8 message)
-    print {String} "Echoing..."
-    sendAll clientSocket message
-  print {String} "Closing..."
-  close clientSocket
-  close serverSocket
-
-main : IO Unit
-main = runTCPEchoServer
-```
+https://github.com/berndlosert/agda-base/blob/master/examples/echo-server.agda#L1-L30
 
 Compile this code by running `agda --compile echo-server.agda`. If you get the
 following errors:
diff --git a/examples/echo-server.agda b/examples/echo-server.agda
index bf09afbc..c924b8a0 100644
--- a/examples/echo-server.agda
+++ b/examples/echo-server.agda
@@ -1,3 +1,5 @@
+{-# OPTIONS --guardedness #-}
+
 open import Prelude
 
 open import Data.Bytes as Bytes using ()