From 14f2d569fb2962566abe409d4fc4128a134946d7 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Mon, 11 Jun 2018 21:24:45 -0700
Subject: [PATCH] updated normal forms in Untyped

---
 hs/agda-count.hs          | 40 +++++++++++++++++++++++++++++++++++++++
 index.md                  |  1 +
 src/plta/Lambda.lagda     |  2 +-
 src/plta/Statistics.lagda | 37 ++++++++++++++++++++++++++++++++++++
 src/plta/Untyped.lagda    | 30 ++++++++++++++++++++++-------
 5 files changed, 102 insertions(+), 8 deletions(-)
 create mode 100644 hs/agda-count.hs
 create mode 100644 src/plta/Statistics.lagda

diff --git a/hs/agda-count.hs b/hs/agda-count.hs
new file mode 100644
index 00000000..4514d9a7
--- /dev/null
+++ b/hs/agda-count.hs
@@ -0,0 +1,40 @@
+import Prelude
+
+begin :: String
+begin =  "\\begin{code}"
+
+end :: String
+end =  "\\end{code}"
+
+prefix :: Eq a => [a] -> [a] -> Bool
+prefix xs ys  =  take (length xs) ys == xs
+
+test0 :: Bool
+test0 =  prefix "abc" "abcde" &&
+         prefix "abc" "abc"   &&
+         not (prefix "abc" "ab")
+
+strip :: (a -> Bool) -> (a -> Bool) -> [a] -> [[a]]
+strip b e []  =  []
+strip b e xs  =
+  let  us = (drop 1 . dropWhile (not . b)) xs  in
+  let  vs = takeWhile (not . e) us  in
+  let  ws = (drop 1 . dropWhile (not . e)) us  in
+  vs : strip b e ws
+
+ex1 = "xbyexxbyyexxxbyyyexxxx"
+
+test1 :: Bool
+test1 =  strip (== 'b') (== 'e') ex1 == ["y","yy","yyy",""]
+
+count :: (a -> Bool) -> (a -> Bool) -> [a] -> Int
+count b e = sum . map length . strip b e
+
+test2 :: Bool
+test2 =  count (== 'b') (== 'e') ex1 == 6
+
+agda :: String -> IO Int
+agda f =
+  do xs <- readFile f
+     return ((count (prefix begin) (prefix end) . lines) xs)
+     
\ No newline at end of file
diff --git a/index.md b/index.md
index fb1c395b..d76c8f84 100644
--- a/index.md
+++ b/index.md
@@ -50,6 +50,7 @@ fixes are encouraged.
 
   - [Acknowledgements]({{ site.baseurl }}{% link out/plta/Acknowledgements.md %})
   - [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/plta/Fonts.md %})
+  - [Statistics: Line counts for each chapter]({{ site.baseurl }}{% link out/plta/Statistics.md %})
 
 [sf]: https://softwarefoundations.cis.upenn.edu/
 [wen]: https://github.com/wenkokke
diff --git a/src/plta/Lambda.lagda b/src/plta/Lambda.lagda
index c2bc17a0..647bb933 100644
--- a/src/plta/Lambda.lagda
+++ b/src/plta/Lambda.lagda
@@ -72,7 +72,7 @@ Three are for the naturals:
 
   * Zero, `` `zero ``
   * Successor, `` `suc ``
-  * Case, `` `case L [zero⇒ M |suc x⇒ N ]
+  * Case, `` `case L [zero⇒ M |suc x⇒ N ] ``
 
 And one is for recursion:
 
diff --git a/src/plta/Statistics.lagda b/src/plta/Statistics.lagda
new file mode 100644
index 00000000..245f9c63
--- /dev/null
+++ b/src/plta/Statistics.lagda
@@ -0,0 +1,37 @@
+---
+title     : "Statistics: Line counts for each chapter"
+layout    : page
+permalink : /Statistics/
+---
+
+\begin{code}
+module plta.Statistics where
+\end{code}
+
+Total number of lines and number of lines of Agda code in each chapter
+(as of 11 June 2018).
+
+                                total   code
+    Preface                       94       1
+
+    Naturals                     900      86
+    Properties                   766     107
+    Relations                    608      93    
+    Equality                     669     141
+    Isomorphism                  310     153
+    Connectives                  826     245
+    Negation                     354      47
+    Quantifiers                  399      82
+    Lists                        901     414
+    Decidable                    566     170
+
+    Lambda                      1114     345
+    LambdaProp                   827     450
+    DeBruijn                     477     351
+    Extensions                   603     524
+    Inference                    428     350
+    Untyped                      346     265
+
+    Acknowledgements              46       1
+    Fonts                         61      23
+    Statistics                    34       1
diff --git a/src/plta/Untyped.lagda b/src/plta/Untyped.lagda
index 6d5c1847..b332f282 100644
--- a/src/plta/Untyped.lagda
+++ b/src/plta/Untyped.lagda
@@ -130,16 +130,32 @@ _[_] {n} N M  =  subst {suc n} {n} ρ N
 ## Normal
 
 \begin{code}
-data Normal  : ∀ {n} → Term n → Set
 data Neutral : ∀ {n} → Term n → Set
-
-data Normal where
-  ƛ_  : ∀ {n} {N : Term (suc n)} → Normal N → Normal (ƛ N)
-  ⌈_⌉ : ∀ {n} {M : Term n} → Neutral M → Normal M
+data Normal  : ∀ {n} → Term n → Set
 
 data Neutral where
-  ⌊_⌋  : ∀ {n} → (k : Var n) → Neutral ⌊ k ⌋
-  _·_  : ∀ {n} → {L : Term n} {M : Term n} → Neutral L → Normal M → Neutral (L · M)
+
+  ⌊_⌋  : ∀ {n}
+    → (k : Var n)
+      -------------
+    → Neutral ⌊ k ⌋
+
+  _·_  : ∀ {n} {L : Term n} {M : Term n}
+    → Neutral L
+    → Normal M
+      ---------------
+    → Neutral (L · M)
+
+data Normal where
+
+  ƛ_  : ∀ {n} {N : Term (suc n)}
+    → Normal N
+      ------------
+    → Normal (ƛ N)
+
+  ⌈_⌉ : ∀ {n} {M : Term n}
+    → Neutral M
+    → Normal M
 \end{code}
 
 ## Reduction step