From 48dcc99152fd043f98bc8d92b042e8320a430e16 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Tue, 14 Jul 2020 18:12:21 +0100 Subject: [PATCH] Removed statistics page. --- hs/Makefile | 8 ----- hs/agda-count.hs | 79 ----------------------------------------- hs/config.txt | 24 ------------- index.md | 1 - src/plfa/Fonts.lagda.md | 3 +- src/plfa/statistics.md | 36 ------------------- 6 files changed, 1 insertion(+), 150 deletions(-) delete mode 100644 hs/Makefile delete mode 100644 hs/agda-count.hs delete mode 100644 hs/config.txt delete mode 100644 src/plfa/statistics.md diff --git a/hs/Makefile b/hs/Makefile deleted file mode 100644 index de8709a1..00000000 --- a/hs/Makefile +++ /dev/null @@ -1,8 +0,0 @@ -statistics: - ./agda-count - -compile: - ghc -o agda-count agda-count.hs - -clean: - rm *.hi *.o diff --git a/hs/agda-count.hs b/hs/agda-count.hs deleted file mode 100644 index ad4e5014..00000000 --- a/hs/agda-count.hs +++ /dev/null @@ -1,79 +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",""] - -test2 :: Bool -test2 = (sum . map length . strip (== 'b') (== 'e')) ex1 == 6 - -nonblank :: String -> Bool -nonblank = not . all (== ' ') - -count :: [[String]] -> Int -count = sum . map length . map (filter nonblank) - -agda :: String -> Int -agda = count . strip begin end . lines - where - begin = prefix "\\begin{code}" - end = prefix "\\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/plfa/" - 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 deleted file mode 100644 index d07941d5..00000000 --- a/hs/config.txt +++ /dev/null @@ -1,24 +0,0 @@ -Preface --- -Naturals -Induction -Relations -Equality -Isomorphism -Connectives -Negation -Quantifiers -Decidable -Lists --- -Lambda -Properties -DeBruijn -More -Bisimulation -Inference -Untyped --- -Acknowledgements -Fonts -Statistics diff --git a/index.md b/index.md index 59fbb5a6..16f82e94 100644 --- a/index.md +++ b/index.md @@ -58,7 +58,6 @@ Pull requests are encouraged. - [Acknowledgements]({{ site.baseurl }}/Acknowledgements/) - [Fonts]({{ site.baseurl }}/Fonts/): Test page for fonts - - [Statistics]({{ site.baseurl }}/Statistics/): Line counts for each chapter ## Related diff --git a/src/plfa/Fonts.lagda.md b/src/plfa/Fonts.lagda.md index 865660b5..d9e63ff2 100644 --- a/src/plfa/Fonts.lagda.md +++ b/src/plfa/Fonts.lagda.md @@ -3,14 +3,13 @@ title : "Fonts" layout : page prev : /Acknowledgements/ permalink : /Fonts/ -next : /Statistics/ --- ``` module plfa.Fonts where ``` -Test page for fonts. Preferably, all vertical bars should line up. +Preferably, all vertical bars should line up. ``` {- diff --git a/src/plfa/statistics.md b/src/plfa/statistics.md deleted file mode 100644 index 208a186c..00000000 --- a/src/plfa/statistics.md +++ /dev/null @@ -1,36 +0,0 @@ ---- -title : "Statistics: Line counts for each chapter" -layout : page -prev : /Fonts/ -permalink : /Statistics/ ---- - -Total number of lines and number of lines of Agda code in each chapter -(as of 16 March 2019). - - total code - ----- ---- - Preface 110 0 - - Naturals 975 96 - Induction 926 129 - Relations 792 158 - Equality 722 189 - Isomorphism 505 209 - Connectives 787 219 - Negation 417 65 - Quantifiers 469 104 - Decidable 587 167 - Lists 1052 448 - - Lambda 1385 362 - Properties 1580 544 - DeBruijn 1366 587 - More 1222 464 - Bisimulation 486 96 - Inference 1124 333 - Untyped 777 299 - - Acknowledgements 55 0 - Fonts 82 64 - Statistics 36 0