updated statistics
This commit is contained in:
parent
155375a559
commit
1fe5d6d852
6 changed files with 94 additions and 47 deletions
BIN
hs/agda-count
Executable file
BIN
hs/agda-count
Executable file
Binary file not shown.
|
@ -1,11 +1,5 @@
|
||||||
import Prelude
|
import Prelude
|
||||||
|
|
||||||
begin :: String
|
|
||||||
begin = "\\begin{code}"
|
|
||||||
|
|
||||||
end :: String
|
|
||||||
end = "\\end{code}"
|
|
||||||
|
|
||||||
prefix :: Eq a => [a] -> [a] -> Bool
|
prefix :: Eq a => [a] -> [a] -> Bool
|
||||||
prefix xs ys = take (length xs) ys == xs
|
prefix xs ys = take (length xs) ys == xs
|
||||||
|
|
||||||
|
@ -33,11 +27,19 @@ count b e = sum . map length . strip b e
|
||||||
test2 :: Bool
|
test2 :: Bool
|
||||||
test2 = count (== 'b') (== 'e') ex1 == 6
|
test2 = count (== 'b') (== 'e') ex1 == 6
|
||||||
|
|
||||||
info :: String -> IO (Int , Int)
|
agda :: String -> Int
|
||||||
info f =
|
agda = count (prefix begin) (prefix end) . lines
|
||||||
do xs <- readFile f
|
where
|
||||||
return ((length . lines) xs),
|
begin = "\\begin{code}"
|
||||||
(count (prefix begin) (prefix end) . lines) xs)
|
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 :: Int -> String -> String
|
||||||
pad n s = take n (s ++ repeat ' ')
|
pad n s = take n (s ++ repeat ' ')
|
||||||
|
@ -45,21 +47,30 @@ pad n s = take n (s ++ repeat ' ')
|
||||||
rjust :: Int -> String -> String
|
rjust :: Int -> String -> String
|
||||||
rjust n = reverse . pad n . reverse
|
rjust n = reverse . pad n . reverse
|
||||||
|
|
||||||
format :: String -> IO String
|
format :: Name -> (Int, Int) -> String
|
||||||
format "--" = ""
|
format name (wc, ag) =
|
||||||
format f =
|
(replicate 4 ' ' ++
|
||||||
do (lines, code) <- info f
|
pad 28 name ++
|
||||||
return (replicate 4 ' ' ++
|
rjust 4 (show wc) ++
|
||||||
pad 28 f ++
|
replicate 4 ' ' ++
|
||||||
rjust 4 lines ++
|
rjust 4 (show ag))
|
||||||
replicate 4 ' ' ++
|
|
||||||
rjust 4 ' ')
|
|
||||||
|
|
||||||
config : IO [String]
|
process :: Name -> IO String
|
||||||
config =
|
process "--" = return ""
|
||||||
do stuff <- readFile "config.txt"
|
process name =
|
||||||
return (lines stuff)
|
do xs <- readFile (pre ++ name ++ post)
|
||||||
|
return (format name (info xs))
|
||||||
|
where
|
||||||
|
pre = "../src/plta/"
|
||||||
|
post = ".lagda"
|
||||||
|
|
||||||
answer : IO String
|
header :: String
|
||||||
answer =
|
header =
|
||||||
do
|
unlines
|
||||||
|
[" total code",
|
||||||
|
" ----- ----"]
|
||||||
|
main :: IO ()
|
||||||
|
main =
|
||||||
|
do config <- readFile "config.txt"
|
||||||
|
content <- sequence (map process (lines config))
|
||||||
|
putStrLn (header ++ unlines content)
|
||||||
|
|
23
hs/config.txt
Normal file
23
hs/config.txt
Normal file
|
@ -0,0 +1,23 @@
|
||||||
|
Preface
|
||||||
|
--
|
||||||
|
Naturals
|
||||||
|
Properties
|
||||||
|
Relations
|
||||||
|
Equality
|
||||||
|
Isomorphism
|
||||||
|
Connectives
|
||||||
|
Negation
|
||||||
|
Quantifiers
|
||||||
|
Lists
|
||||||
|
Decidable
|
||||||
|
--
|
||||||
|
Lambda
|
||||||
|
Properties
|
||||||
|
DeBruijn
|
||||||
|
Extensions
|
||||||
|
Inference
|
||||||
|
Untyped
|
||||||
|
--
|
||||||
|
Acknowledgements
|
||||||
|
Fonts
|
||||||
|
Statistics
|
|
@ -330,13 +330,13 @@ judgements:
|
||||||
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ ``
|
* `` ∅ , "s" ⦂ `ℕ ⇒ `ℕ , "z" ⦂ `ℕ ∋ "s" ⦂ `ℕ ⇒ `ℕ ``
|
||||||
|
|
||||||
They correspond to the following inherently-typed variables.
|
They correspond to the following inherently-typed variables.
|
||||||
\begin{code}
|
-- \begin{code}
|
||||||
_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ
|
_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ
|
||||||
_ = Z
|
_ = Z
|
||||||
|
|
||||||
_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ ⇒ `ℕ
|
_ : ∅ , `ℕ ⇒ `ℕ , `ℕ ∋ `ℕ ⇒ `ℕ
|
||||||
_ = S Z
|
_ = S Z
|
||||||
\end{code}
|
-- \end{code}
|
||||||
In the given context, `"z"` is represented by `Z`, and `"s"` by `S Z`.
|
In the given context, `"z"` is represented by `Z`, and `"s"` by `S Z`.
|
||||||
|
|
||||||
### Terms and the typing judgement
|
### Terms and the typing judgement
|
||||||
|
@ -1348,4 +1348,16 @@ tedious and almost identical to the previous proof.
|
||||||
|
|
||||||
Counting the lines of code is instructive. While this chapter
|
Counting the lines of code is instructive. While this chapter
|
||||||
covers the same formal development as the previous two
|
covers the same formal development as the previous two
|
||||||
chapters, it has about half the number of lines of code.
|
chapters, it has much less code. Omitting all the examples,
|
||||||
|
and all proofs that appear in Properties but not DeBruijn
|
||||||
|
(such as the proof that reduction is deterministic), the
|
||||||
|
number of lines of code is as follows.
|
||||||
|
|
||||||
|
Lambda 216
|
||||||
|
Properties 235
|
||||||
|
DeBruijn 275
|
||||||
|
|
||||||
|
The relation between the two approaches approximates the
|
||||||
|
golden ratio: raw terms with a separate typing relation
|
||||||
|
require about 1.6 times as much code as inherently-typed terms
|
||||||
|
with de Bruijn indices.
|
||||||
|
|
|
@ -1369,7 +1369,7 @@ det β-zero β-zero = refl
|
||||||
det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V¬—→ (V-suc VL) L—→L″)
|
det (β-suc VL) (ξ-case L—→L″) = ⊥-elim (V¬—→ (V-suc VL) L—→L″)
|
||||||
det (β-suc _) (β-suc _) = refl
|
det (β-suc _) (β-suc _) = refl
|
||||||
det β-μ β-μ = refl
|
det β-μ β-μ = refl
|
||||||
\end{code}
|
-- \end{code}
|
||||||
The proof is by induction over possible reductions. We consider
|
The proof is by induction over possible reductions. We consider
|
||||||
three typical cases.
|
three typical cases.
|
||||||
|
|
||||||
|
|
|
@ -9,29 +9,30 @@ module plta.Statistics where
|
||||||
\end{code}
|
\end{code}
|
||||||
|
|
||||||
Total number of lines and number of lines of Agda code in each chapter
|
Total number of lines and number of lines of Agda code in each chapter
|
||||||
(as of 11 June 2018).
|
(as of 2 July 2018).
|
||||||
|
|
||||||
total code
|
total code
|
||||||
Preface 94 1
|
----- ----
|
||||||
|
Preface 99 1
|
||||||
|
|
||||||
Naturals 900 86
|
Naturals 900 86
|
||||||
Properties 766 107
|
Properties 1533 724
|
||||||
Relations 608 93
|
Relations 608 93
|
||||||
Equality 669 141
|
Equality 595 128
|
||||||
Isomorphism 310 153
|
Isomorphism 403 170
|
||||||
Connectives 826 245
|
Connectives 827 243
|
||||||
Negation 354 47
|
Negation 354 47
|
||||||
Quantifiers 399 82
|
Quantifiers 390 79
|
||||||
Lists 901 414
|
Lists 893 412
|
||||||
Decidable 566 170
|
Decidable 566 170
|
||||||
|
|
||||||
Lambda 1114 345
|
Lambda 1300 386
|
||||||
Properties 827 450
|
Properties 1533 724
|
||||||
DeBruijn 477 351
|
DeBruijn 1363 627
|
||||||
Extensions 603 524
|
Extensions 603 524
|
||||||
Inference 428 350
|
Inference 431 350
|
||||||
Untyped 346 265
|
Untyped 362 281
|
||||||
|
|
||||||
Acknowledgements 46 1
|
Acknowledgements 46 1
|
||||||
Fonts 61 23
|
Fonts 62 44
|
||||||
Statistics 34 1
|
Statistics 38 1
|
||||||
|
|
Loading…
Reference in a new issue