Sharing example

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}

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)

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}