From 246d80eea2aab402793dc8c79f9af730cb606e7d Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 5 Nov 2023 15:48:01 +0100
Subject: [PATCH] add io.quox

---
 examples/io.quox | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 examples/io.quox

diff --git a/examples/io.quox b/examples/io.quox
new file mode 100644
index 0000000..2b6ed66
--- /dev/null
+++ b/examples/io.quox
@@ -0,0 +1,31 @@
+load "misc.quox"
+
+namespace io {
+
+def0 IORes : ★ → ★ = λ A ⇒ A × IOState
+
+def0 IO : ★ → ★ = λ A ⇒ IOState → IORes A
+
+def pure : 0.(A : ★) → A → IO A = λ A x s ⇒ (x, s)
+
+def bind : 0.(A B : ★) → IO A → (A → IO B) → IO B =
+  λ A B m k s0 ⇒
+  case m s0 return IORes B of { (x, s1) ⇒ k x s1 }
+
+def seq : 0.(B : ★) → IO True → IO B → IO B =
+  λ B x y ⇒ bind True B x (λ u ⇒ case u return IO B of { 'true ⇒ y })
+
+def seq' : IO True → IO True → IO True = seq True
+
+#[compile-scheme "(lambda (str) (builtin-io (display str) 'true))"]
+postulate print : String → IO True
+
+def newline = print "\n"
+
+def println : String → IO True =
+  λ str ⇒ seq' (print str) newline
+
+#[compile-scheme "(builtin-io (get-line (current-input-port)))"]
+postulate readln : IO String
+
+}