From 2c4bf843659d7c6a9b3f65aa8aff684958dcdaf7 Mon Sep 17 00:00:00 2001 From: Wen Kokke Date: Mon, 26 Oct 2020 17:05:04 +0100 Subject: [PATCH] Added support for citations. --- bib/plfa.bib | 15 + csl/iso690-author-date-en.csl | 584 ++++++++++++++++++++++++++++++++++ hs/Main.hs | 85 +++-- src/pages/citing.md | 1 - src/pages/notes.md | 183 +++++------ 5 files changed, 747 insertions(+), 121 deletions(-) create mode 100644 bib/plfa.bib create mode 100644 csl/iso690-author-date-en.csl diff --git a/bib/plfa.bib b/bib/plfa.bib new file mode 100644 index 00000000..673d8d4a --- /dev/null +++ b/bib/plfa.bib @@ -0,0 +1,15 @@ +@BOOK{plfa20.07, + author = {Philip Wadler and Wen Kokke and Jeremy G. Siek}, + title = {Programming Language Foundations in {A}gda}, + year = {2020}, + month = jul, + url = {http://plfa.inf.ed.ac.uk/20.07/}, +} + +@BOOK{plfa19.08, + author = {Philip Wadler and Wen Kokke}, + title = {Programming Language Foundations in {A}gda}, + year = {2019}, + month = aug, + url = {http://plfa.inf.ed.ac.uk/19.08/}, +} diff --git a/csl/iso690-author-date-en.csl b/csl/iso690-author-date-en.csl new file mode 100644 index 00000000..c2f041c8 --- /dev/null +++ b/csl/iso690-author-date-en.csl @@ -0,0 +1,584 @@ + + diff --git a/hs/Main.hs b/hs/Main.hs index 93edcb47..76f14add 100644 --- a/hs/Main.hs +++ b/hs/Main.hs @@ -6,12 +6,14 @@ import Data.Functor ((<&>)) import qualified Data.Text as T import Hakyll import Hakyll.Web.Agda +import Hakyll.Web.Routes.Permalink 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 qualified Text.CSL as CSL +import qualified Text.CSL.Pandoc as CSL (processCites) import Text.Pandoc (Pandoc(..), ReaderOptions(..), WriterOptions(..), Extension(..)) import qualified Text.Pandoc as Pandoc import qualified Text.Pandoc.Filter as Pandoc (Filter(..), applyFilters) @@ -152,6 +154,9 @@ epubWriterOptions = siteWriterOptions main :: IO () main = do + let cslFileName = "csl/iso690-author-date-en.csl" + let bibFileName = "bib/plfa.bib" + -- Build function to fix standard library URLs fixStdlibLink <- mkFixStdlibLink agdaStdlibPath @@ -160,25 +165,33 @@ main = do -- Build compiler for Markdown pages let pageCompiler :: Compiler (Item String) - pageCompiler = getResourceBody - >>= readMarkdownWith siteReaderOptions - <&> writeHTML5With siteWriterOptions - >>= saveSnapshot "content" - >>= loadAndApplyTemplate "templates/page.html" siteSectionContext - >>= loadAndApplyTemplate "templates/default.html" siteSectionContext - >>= relativizeUrls + pageCompiler = do + csl <- load cslFileName + bib <- load bibFileName + getResourceBody + >>= readMarkdownWith siteReaderOptions + >>= processCites csl bib + <&> writeHTML5With siteWriterOptions + >>= saveSnapshot "content" + >>= loadAndApplyTemplate "templates/page.html" siteSectionContext + >>= loadAndApplyTemplate "templates/default.html" siteSectionContext + >>= relativizeUrls -- Build compiler for literate Agda pages let pageWithAgdaCompiler :: CommandLineOptions -> Compiler (Item String) - pageWithAgdaCompiler opts = agdaCompilerWith opts - >>= withItemBody (return . withUrls fixStdlibLink) - >>= withItemBody (return . withUrls fixLocalLink) - >>= readMarkdownWith siteReaderOptions - <&> writeHTML5With siteWriterOptions - >>= saveSnapshot "content" - >>= loadAndApplyTemplate "templates/page.html" siteSectionContext - >>= loadAndApplyTemplate "templates/default.html" siteSectionContext - >>= relativizeUrls + pageWithAgdaCompiler opts = do + csl <- load cslFileName + bib <- load bibFileName + agdaCompilerWith opts + >>= withItemBody (return . withUrls fixStdlibLink) + >>= withItemBody (return . withUrls fixLocalLink) + >>= readMarkdownWith siteReaderOptions + >>= processCites csl bib + <&> writeHTML5With siteWriterOptions + >>= saveSnapshot "content" + >>= loadAndApplyTemplate "templates/page.html" siteSectionContext + >>= loadAndApplyTemplate "templates/default.html" siteSectionContext + >>= relativizeUrls -- Run Hakyll -- @@ -260,9 +273,13 @@ main = do >>= relativizeUrls match "posts/*" $ do - route $ setExtension "html" - compile $ getResourceBody + route $ setExtension "html" + compile $ do + csl <- load cslFileName + bib <- load bibFileName + getResourceBody >>= readMarkdownWith siteReaderOptions + >>= processCites csl bib <&> writeHTML5With siteWriterOptions >>= saveSnapshot "content" >>= loadAndApplyTemplate "templates/post.html" postContext @@ -306,6 +323,10 @@ main = do -- Compile templates match "templates/*" $ compile templateBodyCompiler + -- Compile CSL and BibTeX files + match "csl/*.csl" $ compile cslCompiler + match "bib/*.bib" $ compile biblioCompiler + -- Copy resources match "public/**" $ do route idRoute @@ -345,26 +366,28 @@ main = do -- Custom readers and writers -------------------------------------------------------------------------------- --- | 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' - -- | Read a Markdown string using Pandoc, with the supplied options. readMarkdownWith :: ReaderOptions -- ^ Parser options - -> Item String -- ^ String to read - -> Compiler (Item Pandoc) -- ^ Resulting document + -> 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' +-- | Process citations in a Pandoc document. +processCites :: Item CSL -> Item Biblio -> Item Pandoc -> Compiler (Item Pandoc) +processCites csl bib item = do + -- Parse CSL file, if given + style <- unsafeCompiler $ CSL.readCSLFile Nothing . toFilePath . itemIdentifier $ csl + + -- We need to know the citation keys, add then *before* actually parsing the + -- actual page. If we don't do this, pandoc won't even consider them + -- citations! + let Biblio refs = itemBody bib + withItemBody (return . CSL.processCites style refs) item + -- | Write a document as HTML using Pandoc, with the supplied options. writeHTML5With :: WriterOptions -- ^ Writer options for pandoc -> Item Pandoc -- ^ Document to write diff --git a/src/pages/citing.md b/src/pages/citing.md index 2ff1b64d..34402fde 100644 --- a/src/pages/citing.md +++ b/src/pages/citing.md @@ -25,7 +25,6 @@ permalink : /Citing/ } ``` - ## PLFA version 19.08 ### Chicago diff --git a/src/pages/notes.md b/src/pages/notes.md index 6b466739..b4797fe5 100644 --- a/src/pages/notes.md +++ b/src/pages/notes.md @@ -7,12 +7,16 @@ permalink: /Notes/ ## To Do Changes I would like to make to the book: + - Relations, exercise `o+o≡e` --> (recommended) - Relations, exercise `≤-iff-<` --> `≤→<`, `<→≤` - Relations, exercise `Bin-predicates` --> `Bin-predicate` - change canonical form of zero to be empty string, `<>`. + Change canonical form of zero to be empty string, `<>`. Similar change to subsequent exercise. +## Citations + +You can cite works by writing `@` followed by a citation key, e.g., `@plfa20.07`. For instance, the first release of PLFA was by @plfa19.08. See the [bibliography](#bibliography) section below for the bibliography. Citations and the bibliography are currently styled according to the ISO-690 standard. ## Downloading older versions @@ -105,24 +109,26 @@ Get evidence! ## Where to put Lists? Three possible orders: - + (a) As current - + (b) Put Lists immediately after Induction. - - requires moving composition & extensionality earlier - - requires moving parameterised modules earlier for monoids - - add material to relations: - lexical ordering, subtype ordering, All, Any, All-++ iff - - add material to isomorphism: All-++ isomorphism - - retain material on decidability of All, Any in Decidable - + (c) Put Lists after Decidable - - requires moving Any-decidable from Decidable to Lists - + (d) As (b) but put parameterised modules in a separate chapter + + 1. As current + 2. Put Lists immediately after Induction. + - requires moving composition & extensionality earlier + - requires moving parameterised modules earlier for monoids + - add material to relations: + lexical ordering, subtype ordering, All, Any, All-++ iff + - add material to isomorphism: All-++ isomorphism + - retain material on decidability of All, Any in Decidable + 3. Put Lists after Decidable + - requires moving Any-decidable from Decidable to Lists + 4. As (2) but put parameterised modules in a separate chapter Tradeoffs: - + (b) Distribution of exercises near where material is taught - + (b) Additional reinforcement for simple proofs by induction - + (a,c) Can drop material if there is lack of time - + (a,c) Earlier emphasis on induction over evidence - + (c) More consistent structuring principle + + + (2) Distribution of exercises near where material is taught + + (2) Additional reinforcement for simple proofs by induction + + (1,3) Can drop material if there is lack of time + + (1,3) Earlier emphasis on induction over evidence + + (3) More consistent structuring principle ## Set up lists of exercises to do @@ -276,80 +282,79 @@ The following comments were collected on the Agda mailing list. * Chalmer Take Home exam 2017 + http://www.cse.chalmers.se/edu/year/2017/course/DAT140_Types/TakeHomeExamTypes2017.pdf -## Syntax for lambda calculus - -* ƛ \Gl- -* ∙ \. ## Adrian's comments from MeetUp -Adrian King -I think we've finally gone through the whole book now up through chapter Properties, and we've come up with just three places where we thought the book could have done a better job of preparing us for the exercises. +**Adrian King**: -Starting from the end of the book: +> I think we've finally gone through the whole book now up through chapter Properties, and we've come up with just three places where we thought the book could have done a better job of preparing us for the exercises. +> +> Starting from the end of the book: +> +> * Chapter Quantifiers, exercise Bin-isomorphism: +> +> In the `to∘from` case, we want to show that: +> +> ⟨ to (from x) , toCan {from x} ⟩ ≡ ⟨ x , canX ⟩ +> +> I found myself wanting to use a general lemma like: +> +> ``` +> exEq : +> ∀ {A : Set} {x y : A} {p : A → Set} {px : p x} {py : p y} → +> x ≡ y → +> px ≡ py → +> ⟨ x , px ⟩ ≡ ⟨ y , py ⟩ +> exEq refl refl = refl +> ``` +> +> which is in some sense true, but in Agda it doesn't typecheck, because Agda can't see that px's type and py's type are the same. My solution made explicit use of heterogeneous equality. +> +> I realize there are ways to solve this that don't explicitly use heterogeneous equality, but the surprise factor of the exercise might have been lower if heterogeneous equality had been mentioned by that point, perhaps in the Equality chapter. +> +> * Chapter Quantifiers, exercise ∀-×: +> +> I assume the intended solution looks something like: +> +> ``` +> ∀-× : ∀ {B : Tri → Set} → ((x : Tri) → B x) ≃ (B aa × B bb × B cc) +> ∀-× = record { +> to = λ f → ⟨ f aa , ⟨ f bb , f cc ⟩ ⟩ ; +> from = λ{ ⟨ baa , ⟨ bbb , bcc ⟩ ⟩ → λ{ aa → baa ; bb → bbb ; cc → bcc } } ; +> from∘to = λ f → extensionality λ{ aa → refl ; bb → refl ; cc → refl } ; +> to∘from = λ{ y → refl } } +> ``` +> +> but it doesn't typecheck; in the extensionality presented earlier (in chapter Isomorphism), type B is not dependent on type A, but it needs to be here. Agda's error message is sufficiently baffling here that you might want to warn people that they need a dependent version of extensionality, something like: +> +> ``` +> Extensionality : (a b : Level) → Set _ +> Extensionality a b = +> {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → +> (∀ x → f x ≡ g x) → f ≡ g +> +> postulate exten : ∀ {a b} → Extensionality a b +> ``` +> +> * Chapter Relations, exercise Bin-predicates: +> +> I made use here of the inspect idiom, in Aaron Stump's variant, which is syntactically more convenient: +> +> ``` +> keep : ∀ {ℓa} → {a : Set ℓa} → (x : a) → Σ a (λ y → y ≡ x) +> keep x = x , refl +> ``` +> +> Pattern matching on keep m, where m is some complicated term, lets you keep around an equality between the original term and the pattern matched, which is often convenient, as in: +> +> ``` +> roundTripTwice {x} onex with keep (from x) +> roundTripTwice {x} onex | zero , eq with oneIsMoreThanZero onex +> roundTripTwice {x} onex | zero , eq | 0 ⊥-elim (not0<0 0 roundTripTwice {x} onex | suc n , eq rewrite sym eq | toTwiceSuc {n} | +> cong x0_ (sym (roundTrip (one onex))) | sym eq = refl +> ``` +> -* Chapter Quantifiers, exercise Bin-isomorphism: - -In the to∘from case, we want to show that: - - ⟨ to (from x) , toCan {from x} ⟩ ≡ ⟨ x , canX ⟩ - -I found myself wanting to use a general lemma like: - -``` -exEq : -∀ {A : Set} {x y : A} {p : A → Set} {px : p x} {py : p y} → -x ≡ y → -px ≡ py → -⟨ x , px ⟩ ≡ ⟨ y , py ⟩ -exEq refl refl = refl -``` - -which is in some sense true, but in Agda it doesn't typecheck, because Agda can't see that px's type and py's type are the same. My solution made explicit use of heterogeneous equality. - -I realize there are ways to solve this that don't explicitly use heterogeneous equality, but the surprise factor of the exercise might have been lower if heterogeneous equality had been mentioned by that point, perhaps in the Equality chapter. - -* Chapter Quantifiers, exercise ∀-×: - -I assume the intended solution looks something like: - -``` -∀-× : ∀ {B : Tri → Set} → ((x : Tri) → B x) ≃ (B aa × B bb × B cc) -∀-× = record { -to = λ f → ⟨ f aa , ⟨ f bb , f cc ⟩ ⟩ ; -from = λ{ ⟨ baa , ⟨ bbb , bcc ⟩ ⟩ → λ{ aa → baa ; bb → bbb ; cc → bcc } } ; -from∘to = λ f → extensionality λ{ aa → refl ; bb → refl ; cc → refl } ; -to∘from = λ{ y → refl } } -``` - -but it doesn't typecheck; in the extensionality presented earlier (in chapter Isomorphism), type B is not dependent on type A, but it needs to be here. Agda's error message is sufficiently baffling here that you might want to warn people that they need a dependent version of extensionality, something like: - -``` -Extensionality : (a b : Level) → Set _ -Extensionality a b = -{A : Set a} {B : A → Set b} {f g : (x : A) → B x} → -(∀ x → f x ≡ g x) → f ≡ g - -postulate -exten : ∀ {a b} → Extensionality a b -``` - -* Chapter Relations, exercise Bin-predicates: - -I made use here of the inspect idiom, in Aaron Stump's variant, which is syntactically more convenient: - -``` -keep : ∀ {ℓa} → {a : Set ℓa} → (x : a) → Σ a (λ y → y ≡ x) -keep x = x , refl -``` - -Pattern matching on keep m, where m is some complicated term, lets you keep around an equality between the original term and the pattern matched, which is often convenient, as in: - -``` -roundTripTwice {x} onex with keep (from x) -roundTripTwice {x} onex | zero , eq with oneIsMoreThanZero onex -roundTripTwice {x} onex | zero , eq | 0