From b3feeda7c63a28feda4232936b60fedee6b37d4e Mon Sep 17 00:00:00 2001
From: Rachel Lambda Samuelsson <depsterr@protonmail.com>
Date: Wed, 19 Jul 2023 23:12:02 +0200
Subject: [PATCH] :3

---
 .gitignore |  3 +++
 basic.agda | 62 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 shell.nix  | 13 ++++++++++++
 3 files changed, 78 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 basic.agda
 create mode 100644 shell.nix

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..efd0d42
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,3 @@
+*.js
+*.~undo-tree~
+*.agdai
diff --git a/basic.agda b/basic.agda
new file mode 100644
index 0000000..dc14d50
--- /dev/null
+++ b/basic.agda
@@ -0,0 +1,62 @@
+module basic where
+
+open import Agda.Primitive renaming (Set to Type)
+open import Agda.Builtin.Float
+open import Agda.Builtin.String
+open import Agda.Builtin.IO
+open import Agda.Builtin.Unit
+
+postulate
+  HTTPModule : Type
+  http : HTTPModule
+  HTTPServer : Type
+  HTTPReq : Type
+  HTTPRes : Type
+  modify : Type → Type
+  modLog : {A : Type} → modify A
+  setStatusCode : Float → modify HTTPRes
+  setHeader : String → String → modify HTTPRes
+  setEnd : String → modify HTTPRes
+  pure : {A : Type} → A → modify A
+  _>>=_ : {A : Type} → modify A → (A → modify A) → modify A
+  _>>_ : {A : Type} → modify A → modify A → modify A
+  createServer : HTTPModule → (HTTPReq → modify HTTPRes) → HTTPServer
+  serverListen : HTTPServer → Float → String → IO ⊤ → IO ⊤
+  doNothing : IO ⊤
+  putStrLn : String → IO ⊤
+
+{-# COMPILE JS putStrLn = (str) => { console.log(str); } #-}
+  
+{-# COMPILE JS http = require('http') #-}
+
+{-# COMPILE JS setStatusCode = ((float) => { return (res) => { res.statusCode = float; }}) #-}
+{-# COMPILE JS setHeader = ((header) => { return (content) => { return (res) => { res.setHeader(header, content); }}}) #-}
+{-# COMPILE JS setEnd = ((content) => { return (res) => { res.end(content); }}) #-}
+
+{-# COMPILE JS modLog = ((a) => { return (res) => { console.log(res); }}) #-}
+{-# COMPILE JS pure = ((a) => { return (res) => { return structuredClone(a); }}) #-}
+{-# COMPILE JS _>>=_ = ((a) => { return (ma) => { return (amb) => { return (res) => { amb(ma(res)); }}}}) #-}
+{-# COMPILE JS _>>_ = ((a) => { return (ma) => { return (mb) => { return (res) => { ma(res); mb(res); }}}}) #-}
+
+{-# COMPILE JS createServer = ((http) => { return (handler) => { return http.createServer((req, res) => { handler(req)(res); }); }}) #-}
+{-# COMPILE JS serverListen = ((serv) => { return (port) => { return (host) => { return (action) => { return () => { serv.listen(port, host, action) }}}}}) #-}
+
+{-# COMPILE JS doNothing = (() => {}) #-}
+
+port : Float
+port = 3000.0
+
+hostname : String
+hostname = "localhost"
+
+handleReg : modify HTTPRes
+handleReg = do
+  setStatusCode 200.0
+  setHeader "Content-Type" "text/plain"
+  setEnd "Hello World"
+
+server : HTTPServer
+server = createServer http (λ _ → handleReg)
+
+main : IO ⊤
+main = serverListen server port hostname (putStrLn "served request")
diff --git a/shell.nix b/shell.nix
new file mode 100644
index 0000000..ae06152
--- /dev/null
+++ b/shell.nix
@@ -0,0 +1,13 @@
+let pkgs = import <nixpkgs> {};
+in with pkgs; mkShell {
+  packages = [
+    agda
+    nodejs
+  ];
+
+  shellHook = ''
+  rename() {
+    for f in *.js; do sed -i 's/require("\(.*\)");/require(".\/\1");/g' "$f"; done
+  }
+  '';
+}