Removed statistics page.
This commit is contained in:
parent
033e0db57a
commit
48dcc99152
6 changed files with 1 additions and 150 deletions
|
@ -1,8 +0,0 @@
|
||||||
statistics:
|
|
||||||
./agda-count
|
|
||||||
|
|
||||||
compile:
|
|
||||||
ghc -o agda-count agda-count.hs
|
|
||||||
|
|
||||||
clean:
|
|
||||||
rm *.hi *.o
|
|
|
@ -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)
|
|
|
@ -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
|
|
1
index.md
1
index.md
|
@ -58,7 +58,6 @@ Pull requests are encouraged.
|
||||||
|
|
||||||
- [Acknowledgements]({{ site.baseurl }}/Acknowledgements/)
|
- [Acknowledgements]({{ site.baseurl }}/Acknowledgements/)
|
||||||
- [Fonts]({{ site.baseurl }}/Fonts/): Test page for fonts
|
- [Fonts]({{ site.baseurl }}/Fonts/): Test page for fonts
|
||||||
- [Statistics]({{ site.baseurl }}/Statistics/): Line counts for each chapter
|
|
||||||
|
|
||||||
## Related
|
## Related
|
||||||
|
|
||||||
|
|
|
@ -3,14 +3,13 @@ title : "Fonts"
|
||||||
layout : page
|
layout : page
|
||||||
prev : /Acknowledgements/
|
prev : /Acknowledgements/
|
||||||
permalink : /Fonts/
|
permalink : /Fonts/
|
||||||
next : /Statistics/
|
|
||||||
---
|
---
|
||||||
|
|
||||||
```
|
```
|
||||||
module plfa.Fonts where
|
module plfa.Fonts where
|
||||||
```
|
```
|
||||||
|
|
||||||
Test page for fonts. Preferably, all vertical bars should line up.
|
Preferably, all vertical bars should line up.
|
||||||
|
|
||||||
```
|
```
|
||||||
{-
|
{-
|
||||||
|
|
|
@ -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
|
|
Loading…
Reference in a new issue