From 5f98b327df735c0921931065c9f1de96c3193c79 Mon Sep 17 00:00:00 2001
From: Natalie Perna <nmperna@gmail.com>
Date: Mon, 5 Jun 2017 21:27:18 -0400
Subject: [PATCH] Sharing example

---
 Presentation/Agda/Sharing.lagda | 16 ++++++++++++++++
 Presentation/Figures/Sharing.hs | 20 ++++++++++++++++++++
 Presentation/Presentation.lhs   | 18 +++++++++++++++++-
 3 files changed, 53 insertions(+), 1 deletion(-)
 create mode 100644 Presentation/Agda/Sharing.lagda
 create mode 100644 Presentation/Figures/Sharing.hs

diff --git a/Presentation/Agda/Sharing.lagda b/Presentation/Agda/Sharing.lagda
new file mode 100644
index 0000000..5496d4a
--- /dev/null
+++ b/Presentation/Agda/Sharing.lagda
@@ -0,0 +1,16 @@
+\begin{code}
+module Sharing where
+
+data ℕ : Set where
+  zero : ℕ
+  suc : ℕ → ℕ
+
+_+_ : ℕ → ℕ → ℕ
+zero + n = n
+suc m + n = suc (m + n)
+
+one = suc zero
+
+four = let two = one + one
+       in two + two
+\end{code}
diff --git a/Presentation/Figures/Sharing.hs b/Presentation/Figures/Sharing.hs
new file mode 100644
index 0000000..b0a22d1
--- /dev/null
+++ b/Presentation/Figures/Sharing.hs
@@ -0,0 +1,20 @@
+module MAlonzo.Code.Sharing where
+
+import MAlonzo.RTE
+import qualified MAlonzo.RTE
+import qualified Data.Text
+
+name2 = "Sharing.ℕ"
+d2 = ()
+data T2 a0 = C4 | C6 a0
+name8 = "Sharing._+_"
+d8 v0 v1
+  = case coe v0 of
+      C4 -> coe v1
+      C6 v2 -> coe C6 (coe d8 v2 v1)
+      _ -> ⊥
+name16 = "Sharing.one"
+d16 = coe C6 C4
+name18 = "Sharing.four"
+d18 = coe d8 (coe d8 d16 d16)
+        (coe d8 d16 d16)
diff --git a/Presentation/Presentation.lhs b/Presentation/Presentation.lhs
index d45e91b..1efc9c4 100644
--- a/Presentation/Presentation.lhs
+++ b/Presentation/Presentation.lhs
@@ -48,7 +48,9 @@
 }
 \lstdefinestyle{haskell}{
 	language=Haskell,
-	basicstyle=\ttfamily\scriptsize
+	basicstyle=\ttfamily\scriptsize,
+	extendedchars=true,
+	literate={⊥}{{$\bot$}}1 {ℕ}{{$\mathbb{N}$}}1
 }
 
 \title{(Re-)Creating sharing in Agda's GHC backend}
@@ -99,6 +101,20 @@ Proof:\\
 \input{Agda/latex/Proof}
 \end{frame}
 
+\begin{frame}{Sharing}
+\begin{figure}[h]
+\hspace{-1.5cm}
+\begin{subfigure}{.45\textwidth}
+\small
+\input{Agda/latex/Sharing}
+\end{subfigure}
+\hspace{1cm}
+\begin{subfigure}{.55\textwidth}
+\lstinputlisting[style=haskell]{Figures/Sharing.hs}
+\end{subfigure}
+\end{figure}
+\end{frame}
+
 \section{Compiler}
 
 \begin{frame}{Compiler}