WIP

.devcontainer/Dockerfile

@@ -0,0 +1,22 @@
+FROM gitpod/workspace-full
+
+# Install custom tools, runtime, etc.
+RUN brew install agda; \
+  brew install haskell-language-server; \ 
+  brew uninstall --ignore-dependencies emacs; brew deps emacs | xargs -n 1 brew uninstall --ignore-dependencies; \
+  rm -rf /home/linuxbrew/.linuxbrew/etc/unbound; \
+  rm -rf /home/linuxbrew/.linuxbrew/etc/gnutls; \
+  rm -rf /home/linuxbrew/.linuxbrew/etc/openssl@1.1; \
+  rm -rf /home/linuxbrew/.linuxbrew/etc/ca-certificates; \
+  rm -rf /home/linuxbrew/.linuxbrew/share/emacs/site-lisp/agda; \
+  sed -i -e 's/gcc-5/gcc-9/g' /home/linuxbrew/.linuxbrew/Cellar/ghc/8.10.7_1/lib/ghc-8.10.7/settings; \
+  cabal update; cabal install --lib ieee754; cabal install --lib network; cabal install --lib async; \
+  mkdir ~/.agda; \
+  echo /workspaces/agda-base/base-library.agda-lib >> ~/.agda/libraries; \
+  echo base-library >> ~/.agda/defaults; \
+  echo "set ttimeoutlen=25" >> ~/.vimrc; \
+  echo "set hidden" >> ~/.vimrc; \
+  echo "set noswapfile" >> ~/.vimrc; \
+  echo "syntax off" >> ~/.vimrc; \
+  echo "stty -ixon" >> ~/.bashrc; \
+  echo "export EDITOR=vim" >> ~/.bashrc

.devcontainer/devcontainer.json

@@ -0,0 +1,30 @@
+// For format details, see https://aka.ms/devcontainer.json. For config options, see the
+// README at: https://github.com/devcontainers/templates/tree/main/src/universal
+{
+	"name": "agda-base (gitpod)",
+	// Or use a Dockerfile or Docker Compose file. More info: https://containers.dev/guide/dockerfile
+	"build": {
+		"dockerfile": "Dockerfile"
+	},
+
+	// Features to add to the dev container. More info: https://containers.dev/features.
+	// "features": {},
+
+	// Use 'forwardPorts' to make a list of ports inside the container available locally.
+	// "forwardPorts": [],
+
+	// Use 'postCreateCommand' to run commands after the container is created.
+	// "postCreateCommand": "",
+
+	// Configure tool-specific properties.
+	"customizations": {
+		"vscode": {
+			"extensions": [
+				"banacorn.agda-mode"
+			]
+		}
+	},
+
+	// Uncomment to connect as root instead. More info: https://aka.ms/dev-containers-non-root.
+	"remoteUser": "gitpod"
+}

.gitignore

@@ -0,0 +1,2 @@
+*.agdai
+*MAlonzo

.gitpod.Dockerfile

@@ -0,0 +1,20 @@
+FROM gitpod/workspace-full
+
+# Install custom tools, runtime, etc.
+RUN brew install agda; \
+  brew install haskell-language-server; \ 
+  brew uninstall --ignore-dependencies emacs; brew deps emacs | xargs -n 1 brew uninstall --ignore-dependencies; \
+  rm -rf /home/linuxbrew/.linuxbrew/etc/unbound; \
+  rm -rf /home/linuxbrew/.linuxbrew/etc/gnutls; \
+  rm -rf /home/linuxbrew/.linuxbrew/etc/openssl@1.1; \
+  rm -rf /home/linuxbrew/.linuxbrew/etc/ca-certificates; \
+  rm -rf /home/linuxbrew/.linuxbrew/share/emacs/site-lisp/agda; \
+  sed -i -e 's/gcc-5/gcc-9/g' /home/linuxbrew/.linuxbrew/Cellar/ghc/8.10.7_1/lib/ghc-8.10.7/settings; \
+  cabal update; cabal install --lib ieee754; cabal install --lib network; \
+  mkdir ~/.agda; \
+  echo /workspace/agda-base/base-library.agda-lib >> ~/.agda/libraries; \
+  echo base-library >> ~/.agda/defaults; \
+  echo "set hidden" >> ~/.vimrc; \
+  echo "set noswapfile" >> ~/.vimrc; \
+  echo "syntax off" >> ~/.vimrc; \
+  echo "stty -ixon" >> ~/.bashrc

.gitpod.yml

@@ -0,0 +1,2 @@
+image:
+    file: .gitpod.Dockerfile

README.md

@@ -0,0 +1,146 @@
+# WIP: Agda base library
+
+This is an attempt at creating a base library for Agda. Unlike the agda-stdlib
+library, which is designed with proving in mind (and requires emacs configured
+with the Agda input method in order to type all those fancy unicode symbols),
+this library is meant to be a general purpose "batteries-included" base library
+that doesn't require emacs to use and is keyboard friendly.
+
+The design is mostly based on GHC's base library, but a lot of ideas were
+"stolen" from libraries and packages from hackage, pursuit, agda-stdlib,
+agda-prelude, Idris and other sources.
+
+## How to install (Linux, macOS and other Unices)
+
+This assumes that Agda is already installed. See the next sections otherwise:
+
+```sh
+# Clone the project somewhere (or download the code and unzip it somewhere)
+git clone https://github.com/berndlosert/agda-base.git
+
+# Set up the base library
+mkdir -p ~/.agda
+echo <path to base library>/base-library.agda-lib >> ~/.agda/libraries
+echo base-library >> ~/.agda/defaults
+
+# Needed to compile agda programs into executables
+cabal update
+cabal install --lib ieee754
+cabal install --lib network # Needed by Network.Socket code
+cabal install --lib async # Needed by Control.Concurrent.Async code
+```
+
+### Install Agda via Cabal
+
+```sh
+cabal install Agda
+```
+
+### Install Agda with `brew` (macOS Mojave)
+
+```sh
+brew install agda
+```
+
+N.B. `brew install agda` will install a couple of "unnecessary" things:
+* the agda-stdlib (under /usr/local/lib/agda)
+* emacs
+
+To uninstall emacs, do the following:
+
+```sh
+# Uninstall emacs
+brew uninstall --ignore-dependencies emacs
+
+# Uninstall emacs dependencies (brew really needs an option for this)
+brew deps emacs | xargs -n 1 brew uninstall --ignore-dependencies
+
+# Uninstall leftover files
+rm -rf /usr/local/etc/unbound
+rm -rf /usr/local/etc/gnutls
+rm -rf /usr/local/etc/openssl@1.1
+rm -rf /usr/local/etc/ca-certificates
+rm -rf /usr/local/share/emacs/site-lisp/agda
+```
+
+## Hello world!
+
+Save the following code into a file called `hello.agda`.
+
+```agda
+open import Prelude
+open import System.IO
+
+main : IO Unit
+main = print "Hello world!"
+```
+
+Compile it like so:
+
+```
+agda --compile hello.agda
+```
+
+## A more complex example
+
+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
+```
+
+Compile this code by running `agda --compile echo-server.agda`. If you get the
+following errors:
+
+```
+Compilation error:
+
+MAlonzo/Code/Network/Socket.hs:17:1: error:
+    Could not find module ‘Network.Socket.ByteString’
+    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
+   |
+17 | import Network.Socket.ByteString
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+MAlonzo/Code/Network/Socket.hs:18:1: error:
+    Could not find module ‘Network.Socket’
+    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
+   |
+18 | import Network.Socket
+   | ^^^^^^^^^^^^^^^^^^^^^
+```
+
+then you need to make sure you have the `network` package installed. Run `cabal
+install --lib network` to install it and try compiling again. Once it compiles,
+start the program by running `./echo-server`. In a different terminal
+tab/window, run `telnet localhost 7000` and type in `Hello World!`. The
+`echo-server` will echo what you just typed and exit.

base-library.agda-lib

@@ -0,0 +1,8 @@
+name: base-library
+include: src
+flags:
+  --no-import-sorts
+  --type-in-type
+  --guardedness
+  --no-positivity-check
+  --no-termination-check

examples/ap.agda

@@ -0,0 +1,39 @@
+open import Prelude
+
+open import Control.Applicative.FreeAp
+open import Data.String as String using ()
+open import System.IO
+
+variable
+  a : Type
+
+data Resource : Type -> Type where
+  file : FilePath -> Resource String
+
+fetchResource : Resource a -> IO a
+fetchResource (file path) = readFile utf8 path
+
+record External (a : Type) : Type where
+  constructor external
+  field
+    {r} : Type
+    resource : Resource r
+    cont : r -> a
+
+foo : FreeAp External Nat
+foo = _+_ <$> liftFreeAp (external (file "foo.txt") String.length) <*> liftFreeAp (external (file "bar.txt") String.length)
+
+listRequiredFiles : FreeAp External a -> List FilePath
+listRequiredFiles (Pure _) = []
+listRequiredFiles (Ap f (external (file path) _)) = path :: listRequiredFiles f
+
+bar : IO Nat
+bar = flip runFreeAp foo \ where
+  (external r k) -> k <$> fetchResource r
+
+main : IO Unit
+main = do
+  print (listRequiredFiles foo)
+  writeFile utf8 "foo.txt" "123"
+  writeFile utf8 "bar.txt" "4567"
+  print =<< bar

examples/applyN.agda

@@ -0,0 +1,37 @@
+open import Prelude
+
+open import Data.Monoid.Sum
+open import System.IO
+
+-- Maximum resident set size (kbytes): 6483656
+-- Elapsed (wall clock) time (h:mm:ss or m:ss): 0:16.10
+n : Nat
+n = applyN 100_000_000 (_+ 1) 0
+
+-- Maximum resident set size (kbytes): 11484
+-- Elapsed (wall clock) time (h:mm:ss or m:ss): 0:01.22
+n' : Nat
+n' = applyN' 100_000_000 (_+ 1) 0
+
+-- Maximum resident set size (kbytes): 8128528
+-- Elapsed (wall clock) time (h:mm:ss or m:ss): 0:16.97
+m : Sum Nat1
+m = stimes 100_000_000 (asSum 1)
+
+-- Maximum resident set size (kbytes): 12024
+-- Elapsed (wall clock) time (h:mm:ss or m:ss): 0:01.55
+m' : Sum Nat1
+m' = stimes' 100_000_000 (asSum 1)
+
+-- Maximum resident set size (kbytes): 8114992
+-- Elapsed (wall clock) time (h:mm:ss or m:ss): 0:19.27
+k : Sum Nat
+k = mtimes 100_000_000 (asSum 1)
+
+-- Maximum resident set size (kbytes): 11732
+-- Elapsed (wall clock) time (h:mm:ss or m:ss): 0:01.35
+k' : Sum Nat
+k' = mtimes' 100_000_000 (asSum 1)
+
+main : IO Unit
+main = print k'

examples/base-library-examples.agda-lib

@@ -0,0 +1,8 @@
+name: agda-base-examples
+include: ../src/ .
+flags:
+  --no-import-sorts
+  --type-in-type
+  --guardedness
+  --no-positivity-check
+  --no-termination-check