updated normal forms in Untyped
This commit is contained in:
parent
6b570da469
commit
14f2d569fb
5 changed files with 102 additions and 8 deletions
40
hs/agda-count.hs
Normal file
40
hs/agda-count.hs
Normal file
|
@ -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)
|
||||||
|
|
1
index.md
1
index.md
|
@ -50,6 +50,7 @@ fixes are encouraged.
|
||||||
|
|
||||||
- [Acknowledgements]({{ site.baseurl }}{% link out/plta/Acknowledgements.md %})
|
- [Acknowledgements]({{ site.baseurl }}{% link out/plta/Acknowledgements.md %})
|
||||||
- [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/plta/Fonts.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/
|
[sf]: https://softwarefoundations.cis.upenn.edu/
|
||||||
[wen]: https://github.com/wenkokke
|
[wen]: https://github.com/wenkokke
|
||||||
|
|
|
@ -72,7 +72,7 @@ Three are for the naturals:
|
||||||
|
|
||||||
* Zero, `` `zero ``
|
* Zero, `` `zero ``
|
||||||
* Successor, `` `suc ``
|
* Successor, `` `suc ``
|
||||||
* Case, `` `case L [zero⇒ M |suc x⇒ N ]
|
* Case, `` `case L [zero⇒ M |suc x⇒ N ] ``
|
||||||
|
|
||||||
And one is for recursion:
|
And one is for recursion:
|
||||||
|
|
||||||
|
|
37
src/plta/Statistics.lagda
Normal file
37
src/plta/Statistics.lagda
Normal file
|
@ -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
|
|
@ -130,16 +130,32 @@ _[_] {n} N M = subst {suc n} {n} ρ N
|
||||||
## Normal
|
## Normal
|
||||||
|
|
||||||
\begin{code}
|
\begin{code}
|
||||||
data Normal : ∀ {n} → Term n → Set
|
|
||||||
data Neutral : ∀ {n} → Term n → Set
|
data Neutral : ∀ {n} → Term n → Set
|
||||||
|
data Normal : ∀ {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 Neutral where
|
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}
|
\end{code}
|
||||||
|
|
||||||
## Reduction step
|
## Reduction step
|
||||||
|
|
Loading…
Reference in a new issue