michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fixed rendering errors.

Browse source
This commit is contained in:
Wen Kokke 2020-10-23 11:21:02 +02:00
parent 17a68514b1
commit 3d4c9f7a1d
20 changed files with 251 additions and 171 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
README.md
View file

@ -261,7 +261,7 @@ You'll see the key sequence of the character in mini buffer.
## Dependencies for developers
PLFA is written in literate Agda with [Pandoc Markdown][pandoc].
PLFA is written in literate Agda with [CommonMark][commonmark].
PLFA is available as both a website and an EPUB e-book, both of which can be built on UNIX and macOS.
Finally, to help developers avoid common mistakes, we provide a set of Git hooks.
@ -348,6 +348,7 @@ If you want Stack to use your system installation of GHC, follow the instruction
[ruby-html-proofer]: https://github.com/gjtorikian/html-proofer
[hakyll]: https://jaspervdj.be/hakyll/
[pandoc]: https://pandoc.org/installing.html
[commonmark]: https://commonmark.org/
[epubcheck]: https://github.com/w3c/epubcheck
[xcode]: https://developer.apple.com/xcode/
[font-sourcecodepro]: https://github.com/adobe-fonts/source-code-pro

29
hs/Hakyll/Web/Template/Context/Title.hs Normal file
View file

@ -0,0 +1,29 @@
module Hakyll.Web.Template.Context.Title
( titlerunningField
, subtitleField
) where
import Hakyll
import Data.List.Extra as L
import Text.Printf (printf)
titlerunningField :: Context String
titlerunningField = Context go
where
go "titlerunning" _ i = do
title <- maybe (fail "No title") return =<< getMetadataField (itemIdentifier i) "title"
case L.stripInfix ":" title of
Nothing -> fail "No titlerunning/subtitle distinction"
Just (titlerunning, _) -> return . StringField $ titlerunning
go k _ i = fail $ printf "Missing field %s in context for item %s" k (show (itemIdentifier i))
subtitleField :: Context String
subtitleField = Context go
where
go "subtitle" _ i = do
title <- maybe (fail "No title") return =<< getMetadataField (itemIdentifier i) "title"
case L.stripInfix ":" title of
Nothing -> fail "No titlerunning/subtitle distinction"
Just (_, subtitle) -> return . StringField $ L.trim subtitle
go k _ i = fail $ printf "Missing field %s in context for item %s" k (show (itemIdentifier i))

23
hs/Hakyll/Web/Template/Numeric.hs Normal file
View file

@ -0,0 +1,23 @@
{-# LANGUAGE TupleSections #-}
module Hakyll.Web.Template.Numeric
( byNumericFieldAsc
, byNumericFieldDesc
) where
import Hakyll
import Data.List as L
import Data.Maybe (fromMaybe)
import Data.Ord (comparing)
import Text.Read (readMaybe)
byNumericFieldAsc :: MonadMetadata m => String -> [Item a] -> m [Item a]
byNumericFieldAsc key = sortOnM $ \i -> do
maybeInt <- getMetadataField (itemIdentifier i) key
return $ fromMaybe (0 :: Int) (readMaybe =<< maybeInt)
where
sortOnM :: (Monad m, Ord k) => (a -> m k) -> [a] -> m [a]
sortOnM f xs = map fst . L.sortBy (comparing snd) <$> mapM (\ x -> (x,) <$> f x) xs
byNumericFieldDesc :: MonadMetadata m => String -> [Item a] -> m [Item a]
byNumericFieldDesc key is = reverse <$> byNumericFieldAsc key is

204
hs/Main.hs
View file

@ -1,32 +1,48 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
import Control.Monad ((<=<), forM_)
import qualified Data.ByteString.Lazy as BL
import Data.List as L
import Data.List.Extra as L
import Data.Maybe (fromMaybe)
import Data.Ord (comparing)
import Data.Functor ((<&>))
import qualified Data.Text as T
import Hakyll
import Hakyll.Web.Agda
import Hakyll.Web.Template.Numeric
import Hakyll.Web.Template.Context.Metadata
import Hakyll.Web.Template.Context.Title
import Hakyll.Web.Sass
import Hakyll.Web.Routes.Permalink
import System.FilePath ((</>), takeDirectory)
import Text.Pandoc as Pandoc
import Text.Pandoc.Filter
import Text.Printf (printf)
import Text.Read (readMaybe)
import Text.Pandoc (Pandoc(..), ReaderOptions(..), WriterOptions(..), Extension(..))
import qualified Text.Pandoc as Pandoc
import qualified Text.Pandoc.Filter as Pandoc (Filter(..), applyFilters)
--------------------------------------------------------------------------------
-- Configuration
--------------------------------------------------------------------------------
tocContext :: Context String -> Context String
tocContext ctx = Context $ \k a _ -> do
m <- makeItem <=< getMetadata $ "src/plfa/toc.metadata"
unContext (objectContext ctx) k a m
siteReaderOptions :: ReaderOptions
siteReaderOptions = defaultHakyllReaderOptions
{ readerExtensions = Pandoc.extensionsFromList
[ Ext_all_symbols_escapable
, Ext_auto_identifiers
, Ext_backtick_code_blocks
, Ext_citations
, Ext_footnotes
, Ext_header_attributes
, Ext_implicit_header_references
, Ext_intraword_underscores
, Ext_markdown_in_html_blocks
, Ext_raw_html
, Ext_shortcut_reference_links
, Ext_smart
, Ext_superscript
, Ext_subscript
, Ext_yaml_metadata_block
]
}
siteWriterOptions :: WriterOptions
siteWriterOptions = defaultHakyllWriterOptions
siteContext :: Context String
siteContext = mconcat
@ -56,6 +72,11 @@ siteSectionContext = mconcat
, siteContext
]
tableOfContentsContext :: Context String -> Context String
tableOfContentsContext ctx = Context $ \k a _ -> do
m <- makeItem <=< getMetadata $ "src/plfa/toc.metadata"
unContext (objectContext ctx) k a m
acknowledgementsContext :: Context String
acknowledgementsContext = mconcat
[ listField "contributors" defaultContext $
@ -100,6 +121,30 @@ sassOptions = defaultSassOptions
{ sassIncludePaths = Just ["css"]
}
epubSectionContext :: Context String
epubSectionContext = mconcat
[ contentField "content" "content"
, titlerunningField
, subtitleField
]
epubReaderOptions :: ReaderOptions
epubReaderOptions = siteReaderOptions
{ readerStandalone = True
, readerStripComments = True
}
epubWriterOptions :: WriterOptions
epubWriterOptions = siteWriterOptions
{ writerTableOfContents = True
, writerTOCDepth = 2
, writerEpubFonts = [ "public/webfonts/DejaVuSansMono.woff"
, "public/webfonts/FreeMono.woff"
, "public/webfonts/mononoki.woff"
]
, writerEpubChapterLevel = 2
}
--------------------------------------------------------------------------------
-- Build site
--------------------------------------------------------------------------------
@ -115,7 +160,9 @@ main = do
-- Build compiler for Markdown pages
let pageCompiler :: Compiler (Item String)
pageCompiler = pandocCompiler
pageCompiler = getResourceBody
>>= readMarkdownWith siteReaderOptions
<&> writeHTML5With siteWriterOptions
>>= saveSnapshot "content"
>>= loadAndApplyTemplate "templates/page.html" siteContext
>>= loadAndApplyTemplate "templates/default.html" siteContext
@ -126,7 +173,8 @@ main = do
pageWithAgdaCompiler opts = agdaCompilerWith opts
>>= withItemBody (return . withUrls fixStdlibLink)
>>= withItemBody (return . withUrls fixLocalLink)
>>= renderPandoc
>>= readMarkdownWith siteReaderOptions
<&> writeHTML5With siteWriterOptions
>>= saveSnapshot "content"
>>= loadAndApplyTemplate "templates/page.html" siteContext
>>= loadAndApplyTemplate "templates/default.html" siteContext
@ -150,14 +198,14 @@ main = do
compile $ do
epubTemplate <- load "templates/epub.html"
>>= compilePandocTemplate
epubMetadata <- load "src/plfa/meta.xml"
epubMetadata <- load "src/plfa/epub.xml"
let ropt = epubReaderOptions
let wopt = epubWriterOptions
{ writerTemplate = Just . itemBody $ epubTemplate
, writerEpubMetadata = Just . T.pack . itemBody $ epubMetadata
}
getResourceBody
>>= applyAsTemplate (tocContext epubSectionContext)
>>= applyAsTemplate (tableOfContentsContext epubSectionContext)
>>= readPandocWith ropt
>>= applyPandocFilters ropt [] "epub3"
>>= writeEPUB3With wopt
@ -166,7 +214,7 @@ main = do
compile $ getResourceBody
>>= applyAsTemplate siteContext
match "src/plfa/meta.xml" $
match "src/plfa/epub.xml" $
compile $ getResourceBody
>>= applyAsTemplate siteContext
@ -174,8 +222,9 @@ main = do
match "src/plfa/index.md" $ do
route permalinkRoute
compile $ getResourceBody
>>= applyAsTemplate (tocContext siteSectionContext)
>>= renderPandoc
>>= applyAsTemplate (tableOfContentsContext siteSectionContext)
>>= readMarkdownWith siteReaderOptions
<&> writeHTML5With siteWriterOptions
>>= loadAndApplyTemplate "templates/page.html" siteContext
>>= loadAndApplyTemplate "templates/default.html" siteContext
>>= relativizeUrls
@ -188,7 +237,8 @@ main = do
route permalinkRoute
compile $ getResourceBody
>>= applyAsTemplate acknowledgementsContext
>>= renderPandoc
>>= readMarkdownWith siteReaderOptions
<&> writeHTML5With siteWriterOptions
>>= saveSnapshot "content"
>>= loadAndApplyTemplate "templates/page.html" siteContext
>>= loadAndApplyTemplate "templates/default.html" siteContext
@ -211,7 +261,9 @@ main = do
match "posts/*" $ do
route $ setExtension "html"
compile $ pandocCompiler
compile $ getResourceBody
>>= readMarkdownWith siteReaderOptions
<&> writeHTML5With siteWriterOptions
>>= saveSnapshot "content"
>>= loadAndApplyTemplate "templates/post.html" postContext
>>= loadAndApplyTemplate "templates/default.html" siteContext
@ -223,7 +275,7 @@ main = do
compile $ pageWithAgdaCompiler agdaOptions
-- Compile other sections and pages
match ("README.md" .||. "src/**.md") $ do
match ("README.md" .||. "src/**.md" .&&. complement "src/plfa/epub.md") $ do
route permalinkRoute
compile pageCompiler
@ -248,7 +300,7 @@ main = do
-- Compile 404 page
match "404.html" $ do
route idRoute
compile $ pandocCompiler
compile $ getResourceBody
>>= loadAndApplyTemplate "templates/default.html" siteContext
-- Compile templates
@ -279,47 +331,62 @@ main = do
-- Relativise URLs in HTML files
match (fromGlob $ "versions" </> v </> "**.html") $ do
route $ gsubRoute ".versions/" (const "")
route $ gsubRoute "versions/" (const "")
compile $ getResourceBody
>>= relativizeUrls
-- Copy other files
match (fromGlob $ "versions" </> v </> "**") $ do
route $ gsubRoute ".versions/" (const "")
route $ gsubRoute "versions/" (const "")
compile copyFileCompiler
--------------------------------------------------------------------------------
-- EPUB generation
-- Custom readers and writers
--------------------------------------------------------------------------------
epubSectionContext :: Context String
epubSectionContext = mconcat
[ contentField "content" "content"
, titlerunningField
, subtitleField
]
-- | Read a CommonMark string using Pandoc, with the supplied options.
readCommonMarkWith :: ReaderOptions -- ^ Parser options
-> Item String -- ^ String to read
-> Compiler (Item Pandoc) -- ^ Resulting document
readCommonMarkWith ropt item =
case Pandoc.runPure $ traverse (Pandoc.readCommonMark ropt) (fmap T.pack item) of
Left err -> fail $
"Hakyll.Web.Pandoc.readPandocWith: parse failed: " ++ show err
Right item' -> return item'
epubReaderOptions :: ReaderOptions
epubReaderOptions = defaultHakyllReaderOptions
{ readerStandalone = True
, readerStripComments = True
}
-- | Read a Markdown string using Pandoc, with the supplied options.
readMarkdownWith :: ReaderOptions -- ^ Parser options
-> Item String -- ^ String to read
-> Compiler (Item Pandoc) -- ^ Resulting document
readMarkdownWith ropt item =
case Pandoc.runPure $ traverse (Pandoc.readMarkdown ropt) (fmap T.pack item) of
Left err -> fail $
"Hakyll.Web.Pandoc.readPandocWith: parse failed: " ++ show err
Right item' -> return item'
epubWriterOptions :: WriterOptions
epubWriterOptions = defaultHakyllWriterOptions
{ writerTableOfContents = True
, writerTOCDepth = 2
, writerEpubFonts = [ "public/webfonts/DejaVuSansMono.woff"
, "public/webfonts/FreeMono.woff"
, "public/webfonts/mononoki.woff"
]
, writerEpubChapterLevel = 2
}
-- | Write a document as HTML using Pandoc, with the supplied options.
writeHTML5With :: WriterOptions -- ^ Writer options for pandoc
-> Item Pandoc -- ^ Document to write
-> Item String -- ^ Resulting HTML
writeHTML5With wopt (Item itemi doc) =
case Pandoc.runPure $ Pandoc.writeHtml5String wopt doc of
Left err -> error $ "Hakyll.Web.Pandoc.writePandocWith: " ++ show err
Right item' -> Item itemi $ T.unpack item'
applyPandocFilters :: ReaderOptions -> [Filter] -> String -> Item Pandoc -> Compiler (Item Pandoc)
-- | Write a document as EPUB3 using Pandoc, with the supplied options.
writeEPUB3With :: WriterOptions -> Item Pandoc -> Compiler (Item BL.ByteString)
writeEPUB3With wopt (Item itemi doc) =
return $ case Pandoc.runPure $ Pandoc.writeEPUB3 wopt doc of
Left err -> error $ "Hakyll.Web.Pandoc.writeEPUB3With: " ++ show err
Right doc' -> Item itemi doc'
-- | Apply a filter to a Pandoc document.
applyPandocFilters :: ReaderOptions -> [Pandoc.Filter] -> String -> Item Pandoc -> Compiler (Item Pandoc)
applyPandocFilters ropt filters fmt = withItemBody $
unsafeCompiler . runIOorExplode . applyFilters ropt filters [fmt]
unsafeCompiler . Pandoc.runIOorExplode . Pandoc.applyFilters ropt filters [fmt]
-- | Compile a Pandoc template (as opposed to a Hakyll template).
compilePandocTemplate :: Item String -> Compiler (Item (Pandoc.Template T.Text))
compilePandocTemplate i = do
let templatePath = toFilePath $ itemIdentifier i
@ -328,48 +395,11 @@ compilePandocTemplate i = do
template <- either fail return templateOrError
makeItem template
writeEPUB3With :: WriterOptions -> Item Pandoc -> Compiler (Item BL.ByteString)
writeEPUB3With wopt (Item itemi doc) = do
return $ case runPure $ writeEPUB3 wopt doc of
Left err -> error $ "Hakyll.Web.Pandoc.writeEPUB3With: " ++ show err
Right doc' -> Item itemi doc'
--------------------------------------------------------------------------------
-- Supply snapshot as a field to the template
--------------------------------------------------------------------------------
subtitleField :: Context String
subtitleField = Context go
where
go "subtitle" _ i = do
title <- maybe (fail "No title") return =<< getMetadataField (itemIdentifier i) "title"
case L.stripInfix ":" title of
Nothing -> fail "No titlerunning/subtitle distinction"
Just (_, subtitle) -> return . StringField $ L.trim subtitle
go k _ i = fail $ printf "Missing field %s in context for item %s" k (show (itemIdentifier i))
titlerunningField :: Context String
titlerunningField = Context go
where
go "titlerunning" _ i = do
title <- maybe (fail "No title") return =<< getMetadataField (itemIdentifier i) "title"
case L.stripInfix ":" title of
Nothing -> fail "No titlerunning/subtitle distinction"
Just (titlerunning, _) -> return . StringField $ titlerunning
go k _ i = fail $ printf "Missing field %s in context for item %s" k (show (itemIdentifier i))
contentField :: String -> Snapshot -> Context String
contentField key snapshot = field key $ \item ->
itemBody <$> loadSnapshot (itemIdentifier item) snapshot
byNumericFieldAsc :: MonadMetadata m => String -> [Item a] -> m [Item a]
byNumericFieldAsc key = sortOnM $ \i -> do
maybeInt <- getMetadataField (itemIdentifier i) key
return $ fromMaybe (0 :: Int) (readMaybe =<< maybeInt)
byNumericFieldDesc :: MonadMetadata m => String -> [Item a] -> m [Item a]
byNumericFieldDesc key is = reverse <$> byNumericFieldAsc key is
sortOnM :: (Monad m, Ord k) => (a -> m k) -> [a] -> m [a]
sortOnM f xs = map fst . L.sortBy (comparing snd) <$> mapM (\ x -> (x,) <$> f x) xs

2
plfa.cabal
View file

@ -35,7 +35,9 @@ library
import: shared-properties
hs-source-dirs: hs
exposed-modules: Hakyll.Web.Agda
, Hakyll.Web.Template.Numeric
, Hakyll.Web.Template.Context.Metadata
, Hakyll.Web.Template.Context.Title
, Hakyll.Web.Sass
, Hakyll.Web.Routes.Permalink
build-depends: Agda ==2.6.1.1

2
src/pages/announcements.html
View file

@ -17,5 +17,5 @@ $if(posts)$
$endif$
</li>
$endfor$
</ul>
</div>
$endif$

0
src/plfa/meta.xml → src/plfa/epub.xml
View file

2
src/plfa/part1/Connectives.lagda.md
View file

@ -536,7 +536,7 @@ Show empty is the right identity of sums up to isomorphism.
-- Your code goes here
```
## Implication is function {#implication}
## Implication is function {name=implication}
Given two propositions `A` and `B`, the implication `A → B` holds if
whenever `A` holds then `B` must also hold. We formalise implication using

2
src/plfa/part1/Decidable.lagda.md
View file

@ -561,7 +561,7 @@ postulate
-- Your code goes here
```
## Proof by reflection {#proof-by-reflection}
## Proof by reflection {name=proof-by-reflection}
Let's revisit our definition of monus from
Chapter [Naturals](/Naturals/).

4
src/plfa/part1/Equality.lagda.md
View file

@ -132,7 +132,7 @@ Again, a useful exercise is to carry out an interactive development,
checking how Agda's knowledge changes as each of the two arguments is
instantiated.
## Congruence and substitution {#cong}
## Congruence and substitution {name=cong}
Equality satisfies _congruence_. If two terms are equal,
they remain so after the same function is applied to both:
@ -627,7 +627,7 @@ Jesper Cockx, Dominique Devries, Andreas Nuyts, and Philip Wadler,
draft, 2017.)
## Universe polymorphism {#unipoly}
## Universe polymorphism {name=unipoly}
As we have seen, not every type belongs to `Set`, but instead every
type belongs somewhere in the hierarchy `Set₀`, `Set₁`, `Set₂`, and so on,

22
src/plfa/part1/Induction.lagda.md
View file

@ -71,7 +71,7 @@ distributes over another operator. A careful author will often call
out these properties---or their lack---for instance by pointing out
that a newly introduced operator is associative but not commutative.
#### Exercise `operators` (practice) {#operators}
#### Exercise `operators` (practice) {name=operators}
Give another example of a pair of operators that have an identity
and are associative, commutative, and distribute over one another.
@ -599,7 +599,7 @@ the main proposition first, and the equations required to do so
will suggest what lemmas to prove.
## Our first corollary: rearranging {#sections}
## Our first corollary: rearranging {name=sections}
We can apply associativity to rearrange parentheses however we like.
Here is an example:
@ -695,7 +695,7 @@ judgments where the first number is less than _m_.
There is also a completely finite approach to generating the same equations,
which is left as an exercise for the reader.
#### Exercise `finite-+-assoc` (stretch) {#finite-plus-assoc}
#### Exercise `finite-|-assoc` (stretch) {name=finite-plus-assoc}
Write out what is known about associativity of addition on each of the
first four days using a finite story of creation, as
@ -857,7 +857,7 @@ typing `C-c C-r` will fill it in, completing the proof:
+-assoc′ (suc m) n p rewrite +-assoc′ m n p = refl
#### Exercise `+-swap` (recommended) {#plus-swap}
#### Exercise `+-swap` (recommended) {name=plus-swap}
Show
@ -872,7 +872,7 @@ is associative and commutative.
```
#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
#### Exercise `*-distrib-+` (recommended) {name=times-distrib-plus}
Show multiplication distributes over addition, that is,
@ -885,7 +885,7 @@ for all naturals `m`, `n`, and `p`.
```
#### Exercise `*-assoc` (recommended) {#times-assoc}
#### Exercise `*-assoc` (recommended) {name=times-assoc}
Show multiplication is associative, that is,
@ -898,7 +898,7 @@ for all naturals `m`, `n`, and `p`.
```
#### Exercise `*-comm` (practice) {#times-comm}
#### Exercise `*-comm` (practice) {name=times-comm}
Show multiplication is commutative, that is,
@ -912,7 +912,7 @@ you will need to formulate and prove suitable lemmas.
```
#### Exercise `0∸n≡0` (practice) {#zero-monus}
#### Exercise `0∸n≡0` (practice) {name=zero-monus}
Show
@ -925,7 +925,7 @@ for all naturals `n`. Did your proof require induction?
```
#### Exercise `∸-+-assoc` (practice) {#monus-plus-assoc}
#### Exercise `∸-|-assoc` (practice) {name=monus-plus-assoc}
Show that monus associates with addition, that is,
@ -942,14 +942,14 @@ for all naturals `m`, `n`, and `p`.
Show the following three laws
m ^ (n + p) ≡ (m ^ n) * (m ^ p) (^-distribˡ-+-*)
m ^ (n + p) ≡ (m ^ n) * (m ^ p) (^-distribˡ-|-*)
(m * n) ^ p ≡ (m ^ p) * (n ^ p) (^-distribʳ-*)
(m ^ n) ^ p ≡ m ^ (n * p) (^-*-assoc)
for all `m`, `n`, and `p`.
#### Exercise `Bin-laws` (stretch) {#Bin-laws}
#### Exercise `Bin-laws` (stretch) {name=Bin-laws}
Recall that
Exercise [Bin](/Naturals/#Bin)

6
src/plfa/part1/Isomorphism.lagda.md
View file

@ -83,7 +83,7 @@ g ∘′ f = λ x → g (f x)
```
## Extensionality {#extensionality}
## Extensionality {name=extensionality}
Extensionality asserts that the only way to distinguish functions is
by applying them; if two functions applied to the same argument always
@ -450,7 +450,7 @@ postulate
-- Your code goes here
```
#### Exercise `_⇔_` (practice) {#iff}
#### Exercise `_⇔_` (practice) {name=iff}
Define equivalence of propositions (also known as "if and only if") as follows:
```
@ -465,7 +465,7 @@ Show that equivalence is reflexive, symmetric, and transitive.
-- Your code goes here
```
#### Exercise `Bin-embedding` (stretch) {#Bin-embedding}
#### Exercise `Bin-embedding` (stretch) {name=Bin-embedding}
Recall that Exercises
[Bin](/Naturals/#Bin) and

6
src/plfa/part1/Lists.lagda.md
View file

@ -458,7 +458,7 @@ _ =
```
Now the time to reverse a list is linear in the length of the list.
## Map {#Map}
## Map {name=Map}
Map applies a function to every element of a list to generate a corresponding list.
Map is an example of a _higher-order function_, one which takes a function as an
@ -558,7 +558,7 @@ Define a suitable map operator over trees:
-- Your code goes here
```
## Fold {#Fold}
## Fold {name=Fold}
Fold takes an operator and a value, and uses the operator to combine
each of the elements of the list, taking the given value as the result
@ -833,7 +833,7 @@ Show that if `_⊗_` and `e` form a monoid, then `foldr _⊗_ e` and
```
## All {#All}
## All {name=All}
We can also define predicates over lists. Two of the most important
are `All` and `Any`.

16
src/plfa/part1/Naturals.lagda.md
View file

@ -76,7 +76,7 @@ after zero; and `2` is shorthand for `suc (suc zero)`, which is the
same as `suc 1`, the successor of one; and `3` is shorthand for the
successor of two; and so on.
#### Exercise `seven` (practice) {#seven}
#### Exercise `seven` (practice) {name=seven}
Write out `7` in longhand.
@ -287,7 +287,7 @@ Parentheses and semicolons are among the few characters that cannot
appear in names, so we do not need extra spaces in the `using` list.
## Operations on naturals are recursive functions {#plus}
## Operations on naturals are recursive functions {name=plus}
Now that we have the natural numbers, what can we do with them?
For instance, can we define arithmetic operations such as
@ -425,7 +425,7 @@ is not like testimony in a court which must be weighed to determine
whether the witness is trustworthy. Rather, it is ironclad. The
other word for evidence, which we will use interchangeably, is _proof_.
#### Exercise `+-example` (practice) {#plus-example}
#### Exercise `+-example` (practice) {name=plus-example}
Compute `3 + 4`, writing out your reasoning as a chain of equations, using the equations for `+`.
@ -486,7 +486,7 @@ Here we have omitted the signature declaring `_ : 2 * 3 ≡ 6`, since
it can easily be inferred from the corresponding term.
#### Exercise `*-example` (practice) {#times-example}
#### Exercise `*-example` (practice) {name=times-example}
Compute `3 * 4`, writing out your reasoning as a chain of equations, using the equations for `*`.
(You do not need to step through the evaluation of `+`.)
@ -496,7 +496,7 @@ Compute `3 * 4`, writing out your reasoning as a chain of equations, using the e
```
#### Exercise `_^_` (recommended) {#power}
#### Exercise `_^_` (recommended) {name=power}
Define exponentiation, which is given by the following equations:
@ -566,7 +566,7 @@ _ =
∎
```
#### Exercise `∸-example₁` and `∸-example₂` (recommended) {#monus-examples}
#### Exercise `∸-example₁` and `∸-example₂` (recommended) {name=monus-examples}
Compute `5 ∸ 3` and `3 ∸ 5`, writing out your reasoning as a chain of equations.
@ -701,7 +701,7 @@ definitions is quite similar. They might be considered two sides of
the same coin.
## The story of creation, finitely {#finite-creation}
## The story of creation, finitely {name=finite-creation}
The above story was told in a stratified way. First, we create
the infinite set of naturals. We take that set as given when
@ -872,7 +872,7 @@ Haskell requires time proportional to the sum of the logarithms of
_m_ and _n_.
#### Exercise `Bin` (stretch) {#Bin}
#### Exercise `Bin` (stretch) {name=Bin}
A more efficient representation of natural numbers uses a binary
rather than a unary system. We represent a number as a bitstring:

4
src/plfa/part1/Quantifiers.lagda.md
View file

@ -380,7 +380,7 @@ restated in this way.
-- Your code goes here
```
#### Exercise `∃-+-≤` (practice)
#### Exercise `∃-|-≤` (practice)
Show that `y ≤ z` holds if and only if there exists a `x` such that
`x + y ≡ z`.
@ -438,7 +438,7 @@ postulate
Does the converse hold? If so, prove; if not, explain why.
#### Exercise `Bin-isomorphism` (stretch) {#Bin-isomorphism}
#### Exercise `Bin-isomorphism` (stretch) {name=Bin-isomorphism}
Recall that Exercises
[Bin](/Naturals/#Bin),

20
src/plfa/part1/Relations.lagda.md
View file

@ -241,7 +241,7 @@ lack---for instance by saying that a newly introduced relation is a
partial order but not a total order.
#### Exercise `orderings` (practice) {#orderings}
#### Exercise `orderings` (practice) {name=orderings}
Give an example of a preorder that is not a partial order.
@ -359,7 +359,7 @@ and `suc n ≤ suc m` and must show `suc m ≡ suc n`. The inductive
hypothesis `≤-antisym m≤n n≤m` establishes that `m ≡ n`, and our goal
follows by congruence.
#### Exercise `≤-antisym-cases` (practice) {#leq-antisym-cases}
#### Exercise `≤-antisym-cases` (practice) {name=leq-antisym-cases}
The above proof omits cases where one argument is `z≤n` and one
argument is `s≤s`. Why is it ok to omit them?
@ -559,7 +559,7 @@ Show that multiplication is monotonic with regard to inequality.
```
## Strict inequality {#strict-inequality}
## Strict inequality {name=strict-inequality}
We can define strict inequality similarly to inequality:
```
@ -597,7 +597,7 @@ and conversely. One can then give an alternative derivation of the
properties of strict inequality, such as transitivity, by
exploiting the corresponding properties of inequality.
#### Exercise `<-trans` (recommended) {#less-trans}
#### Exercise `<-trans` (recommended) {name=less-trans}
Show that strict inequality is transitive.
@ -605,7 +605,7 @@ Show that strict inequality is transitive.
-- Your code goes here
```
#### Exercise `trichotomy` (practice) {#trichotomy}
#### Exercise `trichotomy` (practice) {name=trichotomy}
Show that strict inequality satisfies a weak version of trichotomy, in
the sense that for any `m` and `n` that one of the following holds:
@ -623,7 +623,7 @@ similar to that used for totality.
-- Your code goes here
```
#### Exercise `+-mono-<` (practice) {#plus-mono-less}
#### Exercise `+-mono-<` (practice) {name=plus-mono-less}
Show that addition is monotonic with respect to strict inequality.
As with inequality, some additional definitions may be required.
@ -632,7 +632,7 @@ As with inequality, some additional definitions may be required.
-- Your code goes here
```
#### Exercise `≤-iff-<` (recommended) {#leq-iff-less}
#### Exercise `≤-iff-<` (recommended) {name=leq-iff-less}
Show that `suc m ≤ n` implies `m < n`, and conversely.
@ -640,7 +640,7 @@ Show that `suc m ≤ n` implies `m < n`, and conversely.
-- Your code goes here
```
#### Exercise `<-trans-revisited` (practice) {#less-trans-revisited}
#### Exercise `<-trans-revisited` (practice) {name=less-trans-revisited}
Give an alternative proof that strict inequality is transitive,
using the relation between strict inequality and inequality and
@ -749,7 +749,7 @@ evidence that the first number is odd. If it is because it is the
successor of an even number, then the result is odd because it is the
successor of the sum of two even numbers, which is even.
#### Exercise `o+o≡e` (stretch) {#odd-plus-odd}
#### Exercise `o+o≡e` (stretch) {name=odd-plus-odd}
Show that the sum of two odd numbers is even.
@ -757,7 +757,7 @@ Show that the sum of two odd numbers is even.
-- Your code goes here
```
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
#### Exercise `Bin-predicates` (stretch) {name=Bin-predicates}
Recall that
Exercise [Bin](/Naturals/#Bin)

33
src/plfa/part2/DeBruijn.lagda.md
View file

@ -445,20 +445,19 @@ We can then introduce a convenient abbreviation for variables:
```
#_ : ∀ {Γ}
→ (n : ℕ)
→ {n<?length : True (suc n ≤? length Γ)}
→ {n∈Γ : True (suc n ≤? length Γ)}
--------------------------------
→ Γ ⊢ lookup (toWitness n<?length)
#_ n {n<?length} = ` count (toWitness n<?length)
→ Γ ⊢ lookup (toWitness n∈Γ)
#_ n {n∈Γ} = ` count (toWitness n∈Γ)
```
Function `#_` takes an implicit argument `n<?length` that provides
evidence for `n` to be within the context's bounds. Recall that
[`True`]({{ site.baseurl }}/Decidable/#proof-by-reflection),
[`_≤?_`]({{ site.baseurl }}/Decidable/#the-best-of-both-worlds) and
[`toWitness`]({{ site.baseurl }}/Decidable/#decidables-from-booleans-and-booleans-from-decidables)
are defined in Chapter [Decidable]({{ site.baseurl }}/Decidable/). The
type of `n<?length` guards against invoking `#_` on an `n` that is out
of context bounds. Finally, in the return type `n<?length` is
converted to a witness that `n` is within the bounds.
Function `#_` takes an implicit argument `n∈Γ` that provides evidence for `n` to
be within the context's bounds. Recall that
[`True`](/Decidable/#proof-by-reflection),
[`_≤?_`](/Decidable/#the-best-of-both-worlds) and
[`toWitness`](/Decidable/#decidables-from-booleans-and-booleans-from-decidables)
are defined in Chapter [Decidable](/Decidable/). The type of `n∈Γ` guards
against invoking `#_` on an `n` that is out of context bounds. Finally, in the
return type `n∈Γ` is converted to a witness that `n` is within the bounds.
With this abbreviation, we can rewrite the Church numeral two more compactly:
```
@ -467,13 +466,9 @@ _ = ƛ ƛ (# 1 · (# 1 · # 0))
```
### Test examples {#examples}
We repeat the test examples from
Chapter [Lambda](/Lambda/).
You can find them
[here](/Lambda/#derivation)
for comparison.
### Test examples
We repeat the test examples from Chapter [Lambda](/Lambda/). You can find them
[here](/Lambda/#derivation) for comparison.
First, computing two plus two on naturals:
```

6
src/plfa/part2/Inference.lagda.md
View file

@ -32,7 +32,7 @@ Chapter [Lambda](/Lambda/),
and from it we compute an intrinsically-typed term, in the style of
Chapter [DeBruijn](/DeBruijn/).
## Introduction: Inference rules as algorithms {#algorithms}
## Introduction: Inference rules as algorithms {name=algorithms}
In the calculus we have considered so far, a term may have more than
one type. For example,
@ -470,7 +470,7 @@ the equality test in the application rule in the first
[section](/Inference/#algorithms).
#### Exercise `bidirectional-mul` (recommended) {#bidirectional-mul}
#### Exercise `bidirectional-mul` (recommended) {name=bidirectional-mul}
Rewrite your definition of multiplication from
Chapter [Lambda](/Lambda/), decorated to support inference.
@ -480,7 +480,7 @@ Chapter [Lambda](/Lambda/), decorated to support inference.
```
#### Exercise `bidirectional-products` (recommended) {#bidirectional-products}
#### Exercise `bidirectional-products` (recommended) {name=bidirectional-products}
Extend the bidirectional type rules to include products from
Chapter [More](/More/).

4
src/plfa/part2/Lambda.lagda.md
View file

@ -213,7 +213,7 @@ definition may use `plusᶜ` as defined earlier (or may not
```
#### Exercise `primed` (stretch) {#primed}
#### Exercise `primed` (stretch) {name=primed}
Some people find it annoying to write `` ` "x" `` instead of `x`.
We can make examples with lambda terms slightly easier to write
@ -1201,7 +1201,7 @@ the three places where a bound variable is introduced.
The rules are deterministic, in that at most one rule applies to every term.
### Example type derivations {#derivation}
### Example type derivations {name=derivation}
Type derivations correspond to trees. In informal notation, here
is a type derivation for the Church numeral two,

4
src/plfa/part2/More.lagda.md
View file

@ -147,7 +147,7 @@ Here `M †` is the translation of term `M` from a calculus with the
construct to a calculus without the construct.
## Products {#products}
## Products {name=products}
### Syntax
@ -285,7 +285,7 @@ We can also translate back the other way:
(`proj₁ L) ‡ = case× (L ‡) [⟨ x , y ⟩⇒ x ]
(`proj₂ L) ‡ = case× (L ‡) [⟨ x , y ⟩⇒ y ]
## Sums {#sums}
## Sums {name=sums}
### Syntax