From 2cb9c9c2c3121ad83666c0a97412a627f5e11eb2 Mon Sep 17 00:00:00 2001
From: wadler <wadler@inf.ed.ac.uk>
Date: Tue, 3 Jul 2018 10:20:40 -0300
Subject: [PATCH] fixed line in Statistics

---
 hs/agda-count.hs          | 76 ---------------------------------------
 hs/config.txt             |  2 +-
 src/plta/Statistics.lagda |  2 +-
 3 files changed, 2 insertions(+), 78 deletions(-)
 delete mode 100644 hs/agda-count.hs

diff --git a/hs/agda-count.hs b/hs/agda-count.hs
deleted file mode 100644
index f6136b6b..00000000
--- a/hs/agda-count.hs
+++ /dev/null
@@ -1,76 +0,0 @@
-import Prelude
-
-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 -> Int
-agda =  count (prefix begin) (prefix end) . lines
-  where
-  begin  =  "\\begin{code}"
-  end    =  "\\end{code}"
-
-wc :: String -> Int
-wc =  length . lines
-
-type Name = String
-
-info :: String -> (Int, Int)
-info xs = (wc xs, agda xs)
-
-pad :: Int -> String -> String
-pad n s  =  take n (s ++ repeat ' ')
-
-rjust :: Int -> String -> String
-rjust n = reverse . pad n . reverse
-
-format :: Name -> (Int, Int) -> String
-format name (wc, ag) =
-  (replicate 4 ' ' ++
-   pad 28 name ++
-   rjust 4 (show wc) ++
-   replicate 4 ' ' ++
-   rjust 4 (show ag))
-
-process :: Name -> IO String
-process "--"  =  return ""
-process name  =
-  do xs <- readFile (pre ++ name ++ post)
-     return (format name (info xs))
-  where
-  pre  = "../src/plta/"
-  post = ".lagda"
-
-header :: String
-header =
-  unlines
-    ["                                total   code",
-     "                                -----   ----"]
-main :: IO ()
-main =
-  do config <- readFile "config.txt"
-     content <- sequence (map process (lines config))
-     putStrLn (header ++ unlines content)
diff --git a/hs/config.txt b/hs/config.txt
index 195ab4a8..3b445750 100644
--- a/hs/config.txt
+++ b/hs/config.txt
@@ -1,7 +1,7 @@
 Preface
 --
 Naturals
-Properties
+Induction
 Relations
 Equality
 Isomorphism
diff --git a/src/plta/Statistics.lagda b/src/plta/Statistics.lagda
index d73561a4..6ba3b802 100644
--- a/src/plta/Statistics.lagda
+++ b/src/plta/Statistics.lagda
@@ -16,7 +16,7 @@ Total number of lines and number of lines of Agda code in each chapter
     Preface                       99       1
 
     Naturals                     900      86
-    Properties                  1533     724
+    Induction                    770     107
     Relations                    608      93
     Equality                     595     128
     Isomorphism                  403     170