From 155375a559135eb92c2658a5b856ef60bd87f0d4 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Mon, 2 Jul 2018 20:00:31 -0300
Subject: [PATCH] first draft of DeBruijn

---
 hs/agda-count.hs          | 33 ++++++++++++++++++++++++----
 src/plta/DeBruijn.lagda   | 45 ++++++++++++++++++++++++++++++++++++++-
 src/plta/Properties.lagda | 12 +++++------
 3 files changed, 79 insertions(+), 11 deletions(-)

diff --git a/hs/agda-count.hs b/hs/agda-count.hs
index 4514d9a7..eaf806ad 100644
--- a/hs/agda-count.hs
+++ b/hs/agda-count.hs
@@ -33,8 +33,33 @@ count b e = sum . map length . strip b e
 test2 :: Bool
 test2 =  count (== 'b') (== 'e') ex1 == 6
 
-agda :: String -> IO Int
-agda f =
+info :: String -> IO (Int , Int)
+info f =
   do xs <- readFile f
-     return ((count (prefix begin) (prefix end) . lines) xs)
-     
\ No newline at end of file
+     return ((length . lines) xs),
+             (count (prefix begin) (prefix end) . lines) xs)
+
+pad :: Int -> String -> String
+pad n s  =  take n (s ++ repeat ' ')
+
+rjust :: Int -> String -> String
+rjust n = reverse . pad n . reverse
+
+format :: String -> IO String
+format "--" = ""
+format f =
+  do (lines, code) <- info f
+     return (replicate 4 ' ' ++
+             pad 28 f ++
+             rjust 4 lines ++
+             replicate 4 ' ' ++
+             rjust 4 ' ')
+
+config : IO [String]
+config =
+  do stuff <- readFile "config.txt"
+     return (lines stuff)
+
+answer : IO String
+answer =
+  do 
\ No newline at end of file
diff --git a/src/plta/DeBruijn.lagda b/src/plta/DeBruijn.lagda
index 96b3fe22..dfa45cd8 100644
--- a/src/plta/DeBruijn.lagda
+++ b/src/plta/DeBruijn.lagda
@@ -1106,10 +1106,45 @@ eval (gas (suc m)) L with progress L
 ... | step {M} L—→M with eval (gas m) M
 ...    | steps M—↠N fin                  =  steps (L —→⟨ L—→M ⟩ M—↠N) fin
 \end{code}
-The definition is mu
+The definition is a little simpler than previously, as we no longer need
+to invoke preservation.
 
 ## Examples
 
+We reiterate each of our previous examples.  We re-define the term
+`sucμ` that loops forever.
+\begin{code}
+sucμ : ∅ ⊢ `ℕ
+sucμ = μ (`suc (# 0))
+\end{code}
+To compute the first three steps of the infinite reduction sequence,
+we evaluate with three steps worth of gas.
+\begin{code}
+_ : eval (gas 3) sucμ ≡
+  steps
+  (μ `suc ` Z —→⟨ β-μ ⟩
+   `suc (μ `suc ` Z) —→⟨ ξ-suc β-μ ⟩
+   `suc (`suc (μ `suc ` Z)) —→⟨ ξ-suc (ξ-suc β-μ) ⟩
+   `suc (`suc (`suc (μ `suc ` Z))) ∎)
+  out-of-gas
+_ = refl
+\end{code}
+
+The Church numeral two applied to successor and zero.
+\begin{code}
+_ : eval (gas 100) (twoᶜ · sucᶜ · `zero) ≡
+  steps
+  ((ƛ (ƛ ` (S Z) · (` (S Z) · ` Z))) · (ƛ `suc ` Z) · `zero —→⟨
+   ξ-·₁ (β-ƛ V-ƛ) ⟩
+   (ƛ (ƛ `suc ` Z) · ((ƛ `suc ` Z) · ` Z)) · `zero —→⟨ β-ƛ V-zero ⟩
+   (ƛ `suc ` Z) · ((ƛ `suc ` Z) · `zero) —→⟨ ξ-·₂ V-ƛ (β-ƛ V-zero) ⟩
+   (ƛ `suc ` Z) · `suc `zero —→⟨ β-ƛ (V-suc V-zero) ⟩
+   `suc (`suc `zero) ∎)
+  (done (V-suc (V-suc V-zero)))
+_ = refl
+\end{code}
+
+Two plus two is four.
 \begin{code}
 _ : eval (gas 100) (plus · two · two) ≡
   steps
@@ -1249,6 +1284,7 @@ _ : eval (gas 100) (plus · two · two) ≡
 _ = refl
 \end{code}
 
+And the corresponding term for Church numerals.
 \begin{code}
 _ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
   steps
@@ -1306,3 +1342,10 @@ _ : eval (gas 100) (plusᶜ · twoᶜ · twoᶜ · sucᶜ · `zero) ≡
   (done (V-suc (V-suc (V-suc (V-suc V-zero)))))
 _ = refl
 \end{code}
+
+We omit the proof that reduction is deterministic, since it is
+tedious and almost identical to the previous proof.
+
+Counting the lines of code is instructive.  While this chapter
+covers the same formal development as the previous two
+chapters, it has about half the number of lines of code.
diff --git a/src/plta/Properties.lagda b/src/plta/Properties.lagda
index a8f723bb..cf889d69 100644
--- a/src/plta/Properties.lagda
+++ b/src/plta/Properties.lagda
@@ -1376,7 +1376,7 @@ three typical cases.
 * Two instances of `ξ-·₁`.
 
       L —→ L′                 L —→ L″
-      -------------- ξ-·₁    -------------- ξ-·₁
+      --------------- ξ-·₁    --------------- ξ-·₁
       L · M —→ L′ · M         L · M —→ L″ · M
 
   By induction we have `L′ ≡ L″`, and hence by congruence
@@ -1384,9 +1384,9 @@ three typical cases.
   
 * An instance of `ξ-·₁` and an instance of `ξ-·₂`.
 
-                             Value L
+                              Value L
       L —→ L′                 M —→ M″
-      -------------- ξ-·₁    -------------- ξ-·₂
+      --------------- ξ-·₁    --------------- ξ-·₂
       L · M —→ L′ · M         L · M —→ L · M″
 
   The rule on the left requires `L` to reduce, but the rule on the right
@@ -1396,12 +1396,12 @@ three typical cases.
 
 * Two instances of `β-ƛ`.
 
-      Value V                             Value V                         
-      ---------------------------- β-ƛ    ---------------------------- β-ƛ
+      Value V                              Value V                         
+      ----------------------------- β-ƛ    ----------------------------- β-ƛ
       (ƛ x ⇒ N) · V —→ N [ x := V ]        (ƛ x ⇒ N) · V —→ N [ x := V ]
 
   Since the left-hand sides are identical, the right-hand sides are
-  also identical.
+  also identical. The formal proof invokes `refl`.
 
 Almost half the lines in the above proof are redundant, e.g., the case
 when one rule is `ξ-·₁` and the other is `ξ-·₂` is considered twice,