From fe255ba70e3dada4bc082246345b760c1b8c0060 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Fri, 2 Oct 2020 01:22:21 +0100
Subject: [PATCH] Code for non-local exits

---
 macros.tex |  5 ++++-
 thesis.tex | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 40 insertions(+), 1 deletion(-)

diff --git a/macros.tex b/macros.tex
index 15661b2..68fbf5a 100644
--- a/macros.tex
+++ b/macros.tex
@@ -330,7 +330,10 @@
 
 % UNIX example
 \newcommand{\OSname}[0]{Tiny UNIX}
-\newcommand{\Uexit}{\dec{exit}}
+\newcommand{\exit}{\dec{exit}}
+\newcommand{\Exit}{\dec{Exit}}
+\newcommand{\Status}{\dec{Status}}
+\newcommand{\status}{\dec{status}}
 \newcommand{\basicIO}{\dec{basicIO}}
 \newcommand{\Putc}{\dec{Putc}}
 \newcommand{\putc}{\dec{putc}}
diff --git a/thesis.tex b/thesis.tex
index 33a14ce..0a55334 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -2121,6 +2121,42 @@ We can now write some contents to the file and observe the effects.
 \subsection{Exceptions: non-local exits}
 \label{sec:tiny-unix-exit}
 
+\[
+  \Status \defas \{\Exit : \Int \opto \Zero\}
+\]
+
+\[
+  \bl
+    \exit : \Int \to \alpha \eff \Status\\
+    \exit~n \defas \Absurd\;(\Do\;\Exit~n)
+  \el
+\]
+
+\[
+  \bl
+    \status : (\UnitType \to \alpha \eff \Status) \to \Int\\
+    \status~m \defas
+       \ba[t]{@{~}l}
+         \Handle\;m\,\Unit\;\With\\
+           ~\ba{@{~}l@{~}c@{~}l}
+              \Return\;\_ &\mapsto& 0\\
+              \Exit~n~\_ &\mapsto& n
+           \ea
+       \ea
+  \el
+\]
+
+\[
+  \ba{@{~}l@{~}l}
+    &\bl
+      \basicIO\,(\lambda\Unit.
+         \status\,(\lambda\Unit.
+            \fwrite\,\Record{\stdout;\texttt{"dead"}};\exit~1;\fwrite\,\Record{\stdout;\texttt{"code"}}))
+     \el\\
+    \reducesto^+& \Record{1;\texttt{"dead"}} : \Record{\Int;\UFile}
+  \ea
+\]
+
 \subsection{Dynamic binding: user-specific environments}
 \label{sec:tiny-unix-env}