diff --git a/README.md b/README.md index 38139335..667b48bc 100644 --- a/README.md +++ b/README.md @@ -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 diff --git a/hs/Hakyll/Web/Template/Context/Title.hs b/hs/Hakyll/Web/Template/Context/Title.hs new file mode 100644 index 00000000..7c36975d --- /dev/null +++ b/hs/Hakyll/Web/Template/Context/Title.hs @@ -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)) diff --git a/hs/Hakyll/Web/Template/Numeric.hs b/hs/Hakyll/Web/Template/Numeric.hs new file mode 100644 index 00000000..23ed169b --- /dev/null +++ b/hs/Hakyll/Web/Template/Numeric.hs @@ -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 diff --git a/hs/Main.hs b/hs/Main.hs index ba96f941..d8a31dc7 100644 --- a/hs/Main.hs +++ b/hs/Main.hs @@ -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 @@ -187,12 +236,13 @@ main = do match "src/plfa/backmatter/acknowledgements.md" $ do route permalinkRoute compile $ getResourceBody - >>= applyAsTemplate acknowledgementsContext - >>= renderPandoc - >>= saveSnapshot "content" - >>= loadAndApplyTemplate "templates/page.html" siteContext - >>= loadAndApplyTemplate "templates/default.html" siteContext - >>= relativizeUrls + >>= applyAsTemplate acknowledgementsContext + >>= readMarkdownWith siteReaderOptions + <&> writeHTML5With siteWriterOptions + >>= saveSnapshot "content" + >>= loadAndApplyTemplate "templates/page.html" siteContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls match "authors/*.metadata" $ compile getResourceBody @@ -204,18 +254,20 @@ main = do match "src/pages/announcements.html" $ do route permalinkRoute compile $ getResourceBody - >>= applyAsTemplate postListContext - >>= loadAndApplyTemplate "templates/page.html" siteContext - >>= loadAndApplyTemplate "templates/default.html" siteContext - >>= relativizeUrls + >>= applyAsTemplate postListContext + >>= loadAndApplyTemplate "templates/page.html" siteContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls match "posts/*" $ do route $ setExtension "html" - compile $ pandocCompiler - >>= saveSnapshot "content" - >>= loadAndApplyTemplate "templates/post.html" postContext - >>= loadAndApplyTemplate "templates/default.html" siteContext - >>= relativizeUrls + compile $ getResourceBody + >>= readMarkdownWith siteReaderOptions + <&> writeHTML5With siteWriterOptions + >>= saveSnapshot "content" + >>= loadAndApplyTemplate "templates/post.html" postContext + >>= loadAndApplyTemplate "templates/default.html" siteContext + >>= relativizeUrls -- Compile sections using literate Agda match "src/**.lagda.md" $ do @@ -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,8 +300,8 @@ main = do -- Compile 404 page match "404.html" $ do route idRoute - compile $ pandocCompiler - >>= loadAndApplyTemplate "templates/default.html" siteContext + compile $ getResourceBody + >>= loadAndApplyTemplate "templates/default.html" siteContext -- Compile templates match "templates/*" $ compile templateBodyCompiler @@ -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 + >>= 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 diff --git a/plfa.cabal b/plfa.cabal index 8029e1d8..256b0472 100644 --- a/plfa.cabal +++ b/plfa.cabal @@ -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 diff --git a/src/pages/announcements.html b/src/pages/announcements.html index 3514c5d6..f0964ba1 100644 --- a/src/pages/announcements.html +++ b/src/pages/announcements.html @@ -17,5 +17,5 @@ $if(posts)$ $endif$ $endfor$ - + $endif$ diff --git a/src/plfa/meta.xml b/src/plfa/epub.xml similarity index 100% rename from src/plfa/meta.xml rename to src/plfa/epub.xml diff --git a/src/plfa/part1/Connectives.lagda.md b/src/plfa/part1/Connectives.lagda.md index de454e20..17d73e33 100644 --- a/src/plfa/part1/Connectives.lagda.md +++ b/src/plfa/part1/Connectives.lagda.md @@ -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 diff --git a/src/plfa/part1/Decidable.lagda.md b/src/plfa/part1/Decidable.lagda.md index 59805ba3..97b67500 100644 --- a/src/plfa/part1/Decidable.lagda.md +++ b/src/plfa/part1/Decidable.lagda.md @@ -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/). diff --git a/src/plfa/part1/Equality.lagda.md b/src/plfa/part1/Equality.lagda.md index 51ac3041..84653fbd 100644 --- a/src/plfa/part1/Equality.lagda.md +++ b/src/plfa/part1/Equality.lagda.md @@ -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, diff --git a/src/plfa/part1/Induction.lagda.md b/src/plfa/part1/Induction.lagda.md index 70468189..bd20dd19 100644 --- a/src/plfa/part1/Induction.lagda.md +++ b/src/plfa/part1/Induction.lagda.md @@ -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) diff --git a/src/plfa/part1/Isomorphism.lagda.md b/src/plfa/part1/Isomorphism.lagda.md index 9b3f5334..2cee9aac 100644 --- a/src/plfa/part1/Isomorphism.lagda.md +++ b/src/plfa/part1/Isomorphism.lagda.md @@ -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 diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 8dcc3541..38d1e66e 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -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`. diff --git a/src/plfa/part1/Naturals.lagda.md b/src/plfa/part1/Naturals.lagda.md index f6f1c199..08931fb4 100644 --- a/src/plfa/part1/Naturals.lagda.md +++ b/src/plfa/part1/Naturals.lagda.md @@ -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: diff --git a/src/plfa/part1/Quantifiers.lagda.md b/src/plfa/part1/Quantifiers.lagda.md index a51d91b2..d44b71ff 100644 --- a/src/plfa/part1/Quantifiers.lagda.md +++ b/src/plfa/part1/Quantifiers.lagda.md @@ -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), diff --git a/src/plfa/part1/Relations.lagda.md b/src/plfa/part1/Relations.lagda.md index 7c35c4b5..5263b14a 100644 --- a/src/plfa/part1/Relations.lagda.md +++ b/src/plfa/part1/Relations.lagda.md @@ -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) diff --git a/src/plfa/part2/DeBruijn.lagda.md b/src/plfa/part2/DeBruijn.lagda.md index 63c9e707..8f66902a 100644 --- a/src/plfa/part2/DeBruijn.lagda.md +++ b/src/plfa/part2/DeBruijn.lagda.md @@ -445,20 +445,19 @@ We can then introduce a convenient abbreviation for variables: ``` #_ : ∀ {Γ} → (n : ℕ) - → {n