From 2de7a49042fff67f9ca10c85b962ffff87bd21e3 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mzhang@sift.net>
Date: Wed, 2 Feb 2022 01:25:03 -0600
Subject: [PATCH] Uncommitted changes

---
 Makefile                |  5 ++++-
 main.tex                | 15 +--------------
 src/Project/Cesk.agda   | 10 +++++++---
 src/Project/Syntax.agda | 21 ---------------------
 4 files changed, 12 insertions(+), 39 deletions(-)
 delete mode 100644 src/Project/Syntax.agda

diff --git a/Makefile b/Makefile
index fef6f09..b246b44 100644
--- a/Makefile
+++ b/Makefile
@@ -14,4 +14,7 @@ agda.sty: $(GENERATED_TEX)
 watch:
 	watchexec -e agda,tex -- make --jobs=4 main.pdf
 
-.PHONY: watch
+present: main.pdf
+	zathura --mode fullscreen main.pdf
+
+.PHONY: watch present
diff --git a/main.tex b/main.tex
index 60e1185..7e79403 100644
--- a/main.tex
+++ b/main.tex
@@ -1,4 +1,4 @@
-\documentclass[xcolor={dvipsnames}]{beamer}
+\documentclass[aspectratio=1610,xcolor={dvipsnames}]{beamer}
 \usepackage[utf8]{inputenc}
 \usepackage{relsize}
 \usepackage{amsmath}
@@ -78,19 +78,6 @@
     \item $S$tore is a mapping of addresses to values.
     \item $K$ont is what gets evaluated next.
   \end{itemize}
-
-  \vspace{.5cm}
-
-  Example on next slide.
-\end{frame}
-
-\begin{frame}
-  \begin{exampleblock}{Example}
-    \begin{equation*} \begin{split}
-      \{ C = (\lambda .\:`0 + 2) \cdot 4, E = [], K = [halt] \} \\
-      \{ C = (\lambda .\:`0 + 2), E = [4], K = [\lambda .\:`0 \cdot 4, halt] \} \\
-    \end{split} \end{equation*}
-  \end{exampleblock}
 \end{frame}
 
 \begin{frame}
diff --git a/src/Project/Cesk.agda b/src/Project/Cesk.agda
index 02c3593..663e8b2 100644
--- a/src/Project/Cesk.agda
+++ b/src/Project/Cesk.agda
@@ -75,10 +75,14 @@ eval′ (suc n) s with step s
 eval : ∀ {A} → ℕ → Exp A ∅ A → EvalResult
 eval n e = eval′ n (inject e)
 
+num : ∀ {A} → ℕ → Value A `ℕ
+num 0 = zero
+num (suc n) = suc $ num n
+
 exp : Exp `ℕ ∅ `ℕ
 exp = 
-  `let (call/cc (ƛ (`let (` zero ∘ suc (suc zero)) (abort (` zero)))))
-  ((ƛ $ atomic $ suc $ ` zero) · ` zero)
+  `let (call/cc (ƛ (`let (` zero ∘ (value $ num 2)) (abort (` zero)))))
+  ((ƛ $ atomic $ suc $ suc $ suc $ suc $ ` zero) · ` zero)
 
-expRes+ : eval 7 exp ≡ (complete $ done $ (suc (suc (suc zero))))
+expRes+ : eval 7 exp ≡ (complete $ done $ (num 6))
 expRes+ = refl
diff --git a/src/Project/Syntax.agda b/src/Project/Syntax.agda
deleted file mode 100644
index 1648806..0000000
--- a/src/Project/Syntax.agda
+++ /dev/null
@@ -1,21 +0,0 @@
-module Project.Syntax where
-
-open import Data.String using (String)
-
-data Type : Set where
-
-data Term : Set where
-  -- Natural numbers
-  zero : Term
-  suc : Term → Term
-
-  -- Functions
-  `_ : String → Term
-  ƛ_⇒_ : String → Term → Term
-
-  -- Call/cc
-  call/cc : Term → Term
-
-data TermEnv : Set where
-  ∅ : TermEnv
-  _[_∶_] : TermEnv → String → Type → TermEnv
\ No newline at end of file