Compare commits
28 commits
Author | Date | ||
---|---|---|---|
cb8431dbcc | |||
fbc44a0f78 | |||
8c4fe03730 | |||
d24d992786 | |||
367d61bdd5 | |||
bc087ff31e | |||
dcb4cbb360 | |||
7dff3e17e8 | |||
0eec924486 | |||
7149274cf4 | |||
87fafc7a15 | |||
8b1fbba12a | |||
658bd841f0 | |||
8d0bebab0b | |||
fceaaa8f83 | |||
32ed3d6920 | |||
93f496e3c0 | |||
bf178e1b8b | |||
3830722f67 | |||
583e0fb344 | |||
00ec52d94a | |||
|
84840b0d4d | ||
|
efd14e775f | ||
|
9dc763832f | ||
|
b6700e732c | ||
|
c2c3cce920 | ||
|
0c7bf0508a | ||
|
61b2259d99 |
80 changed files with 2672 additions and 1355 deletions
9
.envrc
Normal file
9
.envrc
Normal file
|
@ -0,0 +1,9 @@
|
|||
use_flake() {
|
||||
watch_file flake.nix
|
||||
watch_file flake.lock
|
||||
eval "$(nix print-dev-env --profile "$(direnv_layout_dir)/flake-profile")"
|
||||
}
|
||||
|
||||
mkdir -p .direnv
|
||||
|
||||
use_flake
|
117
.github/workflows/build.yml
vendored
117
.github/workflows/build.yml
vendored
|
@ -1,117 +0,0 @@
|
|||
on: [push, pull_request]
|
||||
|
||||
name: Build
|
||||
|
||||
jobs:
|
||||
build:
|
||||
runs-on: ${{ matrix.os }}
|
||||
|
||||
strategy:
|
||||
matrix:
|
||||
os: [macOS-latest]
|
||||
ghc: ['8.10.5']
|
||||
agda: ['2.6.1.3']
|
||||
|
||||
steps:
|
||||
|
||||
|
||||
# Checkout
|
||||
|
||||
- name: Checkout
|
||||
uses: actions/checkout@v2
|
||||
with:
|
||||
ref: dev
|
||||
fetch-depth: 1
|
||||
submodules: true
|
||||
|
||||
- name: Update stack.yaml
|
||||
run: |
|
||||
stack config set system-ghc true
|
||||
stack config set install-ghc false
|
||||
shell: bash
|
||||
|
||||
|
||||
# Setup & Cache Haskell
|
||||
|
||||
- name: Cache Haskell
|
||||
uses: actions/cache@v2
|
||||
id: cache-haskell
|
||||
with:
|
||||
path: |
|
||||
~/.ghcup
|
||||
key: ${{ matrix.os }}-ghc-${{ matrix.ghc }}
|
||||
|
||||
|
||||
- name: Setup Haskell
|
||||
if: steps.cache-haskell.outputs.cache-hit != 'true'
|
||||
uses: haskell/actions/setup@v1
|
||||
with:
|
||||
enable-stack: true
|
||||
ghc-version: ${{ matrix.ghc }}
|
||||
cabal-version: 'latest'
|
||||
stack-version: 'latest'
|
||||
|
||||
|
||||
# Setup & Cache HTMLProofer
|
||||
|
||||
- name: Get Ruby Info
|
||||
id: ruby-info
|
||||
run: |
|
||||
echo "::set-output name=ruby::$(ruby -e 'puts RUBY_VERSION')"
|
||||
echo "::set-output name=gem::$(gem --version)"
|
||||
echo "::set-output name=gemdir::$(gem env gemdir)"
|
||||
shell: bash
|
||||
|
||||
- name: Cache HTMLProofer
|
||||
uses: actions/cache@v2
|
||||
id: cache-htmlproofer
|
||||
with:
|
||||
path: ${{ steps.ruby-info.outputs.gemdir }}
|
||||
key: ${{ matrix.os }}-ruby-${{ steps.ruby-info.outputs.ruby }}-gem-${{ steps.ruby-info.outputs.gem }}
|
||||
|
||||
- name: Setup HTMLProofer
|
||||
if: steps.cache-htmlproofer.outputs.cache-hit != 'true'
|
||||
run: sudo gem install html-proofer
|
||||
shell: bash
|
||||
|
||||
|
||||
|
||||
# Setup & Cache Agda, pandoc, and site builder
|
||||
|
||||
- name: Cache .stack-work
|
||||
uses: actions/cache@v2
|
||||
id: cache-stack-work
|
||||
with:
|
||||
path: $GITHUB_WORKSPACE/.stack-work
|
||||
key: ${{ matrix.os }}-ghc-${{ matrix.ghc }}-agda-${{ matrix.agda }}
|
||||
|
||||
- name: Build Agda
|
||||
if: steps.cache-site-builder.outputs.cache-hit != 'true'
|
||||
run: stack build Agda-${{ matrix.agda }}
|
||||
shell: bash
|
||||
|
||||
- name: Build Pandoc
|
||||
if: steps.cache-site-builder.outputs.cache-hit != 'true'
|
||||
run: stack build pandoc-2.10.1
|
||||
shell: bash
|
||||
|
||||
- name: Build other dependencies
|
||||
if: steps.cache-site-builder.outputs.cache-hit != 'true'
|
||||
run: stack build --only-dependencies
|
||||
shell: bash
|
||||
|
||||
- name: Build Site Builder
|
||||
if: steps.cache-site-builder.outputs.cache-hit != 'true'
|
||||
run: stack build
|
||||
shell: bash
|
||||
|
||||
|
||||
# Build & Test Website
|
||||
|
||||
- name: Build Website
|
||||
run: make build
|
||||
shell: bash
|
||||
|
||||
- name: Test Website
|
||||
run: make test
|
||||
shell: bash
|
7
.gitignore
vendored
7
.gitignore
vendored
|
@ -1,5 +1,4 @@
|
|||
## Agda files
|
||||
_build/
|
||||
*.agdai
|
||||
.agda-stdlib.sed
|
||||
.links-*.sed
|
||||
|
@ -12,6 +11,7 @@ stack.yaml.lock
|
|||
dist-newstyle
|
||||
|
||||
## Jekyll files
|
||||
_site/
|
||||
.sass-cache/
|
||||
.agda-stdlib.sed
|
||||
.jekyll-metadata
|
||||
|
@ -30,10 +30,9 @@ Gemfile.lock
|
|||
|
||||
## Emacs files
|
||||
auto/
|
||||
\#*\#
|
||||
|
||||
## Misc build files
|
||||
out/
|
||||
*.zip
|
||||
versions/plfa.github.io-web-*/
|
||||
|
||||
## Include plfa.pdf
|
||||
!plfa.pdf
|
||||
|
|
1
.gitmodules
vendored
1
.gitmodules
vendored
|
@ -1,4 +1,3 @@
|
|||
[submodule "standard-library"]
|
||||
path = standard-library
|
||||
url = https://github.com/agda/agda-stdlib.git
|
||||
shallow = true
|
||||
|
|
7
.vscode/settings.json
vendored
Normal file
7
.vscode/settings.json
vendored
Normal file
|
@ -0,0 +1,7 @@
|
|||
{
|
||||
"editor.fontSize": 15,
|
||||
"vim.insertModeKeyBindings": [
|
||||
{ "before": ["k", "j"], "after": ["<Esc>"] }
|
||||
],
|
||||
"editor.fontFamily": "\"PragmataPro Mono Liga\", \"Roboto Mono\", 'Droid Sans Mono', 'monospace', monospace, 'Droid Sans Fallback'"
|
||||
}
|
174
Makefile
174
Makefile
|
@ -1,35 +1,11 @@
|
|||
|
||||
#################################################################################
|
||||
# Configuration
|
||||
#################################################################################
|
||||
|
||||
MAKE ?= make
|
||||
STACK ?= stack
|
||||
|
||||
SITE_DIR := _site
|
||||
RAW_DIR := $(SITE_DIR)/raw
|
||||
SITE_DIR := _site
|
||||
CACHE_DIR := _cache
|
||||
TMP_DIR := $(CACHE_DIR)/tmp
|
||||
TMP_DIR := $(CACHE_DIR)/tmp
|
||||
|
||||
AGDA := $(STACK) exec agda -- --no-libraries --include-path=standard-library/src
|
||||
PANDOC := $(STACK) exec pandoc --
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Build PLFA site, EPUB, and PDF
|
||||
#################################################################################
|
||||
|
||||
.PHONY: all
|
||||
all:
|
||||
$(MAKE) build
|
||||
$(MAKE) epub-build
|
||||
$(MAKE) pdf-build
|
||||
|
||||
.PHONY: all-clean
|
||||
all-clean:
|
||||
$(MAKE) clean
|
||||
$(MAKE) epub-clean
|
||||
$(MAKE) pdf-clean
|
||||
|
||||
#################################################################################
|
||||
# Setup Git Hooks
|
||||
|
@ -37,7 +13,6 @@ all-clean:
|
|||
|
||||
.PHONY: init
|
||||
init: setup-check-fix-whitespace setup-install-htmlproofer
|
||||
@echo "Setting up Git Hooks"
|
||||
git config core.hooksPath .githooks
|
||||
|
||||
|
||||
|
@ -45,52 +20,51 @@ init: setup-check-fix-whitespace setup-install-htmlproofer
|
|||
# Build PLFA site
|
||||
#################################################################################
|
||||
|
||||
.PHONY: build-deps
|
||||
build-deps:
|
||||
$(STACK) build --only-dependencies
|
||||
|
||||
.PHONY: build
|
||||
build: standard-library/ChangeLog.md | build-deps
|
||||
@echo "Building website"
|
||||
$(STACK) build
|
||||
$(STACK) exec site build
|
||||
build: \
|
||||
standard-library/ChangeLog.md
|
||||
stack build && stack exec site build
|
||||
|
||||
standard-library/ChangeLog.md:
|
||||
@echo "Updating Agda standard library"
|
||||
git submodule init
|
||||
git submodule update --recursive
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Test generated site with HTMLProofer
|
||||
#################################################################################
|
||||
|
||||
.PHONY: test
|
||||
test: setup-install-htmlproofer build
|
||||
@echo "Testing generated HTML using HTMLProofer"
|
||||
cd $(SITE_DIR) && htmlproofer \
|
||||
--check-html \
|
||||
--disable-external \
|
||||
--report-invalid-tags \
|
||||
--report-missing-names \
|
||||
--report-script-embeds \
|
||||
--report-missing-doctype \
|
||||
--report-eof-tags \
|
||||
--report-mismatched-tags \
|
||||
--check-img-http \
|
||||
--check-opengraph \
|
||||
cd $(SITE_DIR) && htmlproofer \
|
||||
--check-html \
|
||||
--disable-external \
|
||||
--report-invalid-tags \
|
||||
--report-missing-names \
|
||||
--report-script-embeds \
|
||||
--report-missing-doctype \
|
||||
--report-eof-tags \
|
||||
--report-mismatched-tags \
|
||||
--check-img-http \
|
||||
--check-opengraph \
|
||||
.
|
||||
|
||||
#################################################################################
|
||||
# Test generated EPUB with EPUBCheck
|
||||
#################################################################################
|
||||
|
||||
.PHONY: test-epub
|
||||
test-epub: setup-check-epubcheck build
|
||||
epubcheck $(SITE_DIR)/plfa.epub
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Automatically rebuild the site on changes, and start a preview server
|
||||
#################################################################################
|
||||
|
||||
.PHONY: watch
|
||||
watch: standard-library/ChangeLog.md | build-deps
|
||||
@echo "Watching for changes and rebuilding"
|
||||
$(STACK) build
|
||||
$(STACK) exec site watch
|
||||
watch: \
|
||||
standard-library/ChangeLog.md
|
||||
stack build && stack exec site watch
|
||||
|
||||
|
||||
#################################################################################
|
||||
|
@ -98,10 +72,8 @@ watch: standard-library/ChangeLog.md | build-deps
|
|||
#################################################################################
|
||||
|
||||
.PHONY: update-contributors
|
||||
update-contributors: | build-deps
|
||||
@echo "Updating contributors from GitHub"
|
||||
$(STACK) build
|
||||
$(STACK) exec update-contributors
|
||||
update-contributors:
|
||||
stack build && stack exec update-contributors
|
||||
|
||||
|
||||
#################################################################################
|
||||
|
@ -109,10 +81,9 @@ update-contributors: | build-deps
|
|||
#################################################################################
|
||||
|
||||
.PHONY: clean
|
||||
clean: standard-library/ChangeLog.md | build-deps
|
||||
@echo "Cleaning generated files for site"
|
||||
$(STACK) build
|
||||
$(STACK) exec site clean
|
||||
clean: \
|
||||
standard-library/ChangeLog.md
|
||||
stack build && stack exec site clean
|
||||
|
||||
|
||||
#################################################################################
|
||||
|
@ -131,28 +102,28 @@ list:
|
|||
|
||||
.PHONY: publish
|
||||
publish: setup-check-rsync
|
||||
$(MAKE) all
|
||||
@echo "Cleaning intermediate files"
|
||||
rm -rf $(RAW_DIR)
|
||||
$(MAKE) test
|
||||
@echo "Creating web branch"
|
||||
@echo "Building site..."
|
||||
make build
|
||||
@echo "Testing site..."
|
||||
make test
|
||||
@echo "Creating web branch..."
|
||||
git fetch --all
|
||||
git checkout -b web --track origin/web
|
||||
rsync -a \
|
||||
--filter='P $(SITE_DIR)/' \
|
||||
--filter='P $(CACHE_DIR)/' \
|
||||
--filter='P .git/' \
|
||||
--filter='P .gitignore' \
|
||||
--filter='P .stack-work' \
|
||||
--filter='P .nojekyll' \
|
||||
--filter='P CNAME' \
|
||||
--delete-excluded \
|
||||
$(SITE_DIR) .
|
||||
rsync -a \
|
||||
--filter='P _site/' \
|
||||
--filter='P _cache/' \
|
||||
--filter='P .git/' \
|
||||
--filter='P .gitignore' \
|
||||
--filter='P .stack-work' \
|
||||
--filter='P .nojekyll' \
|
||||
--filter='P CNAME' \
|
||||
--delete-excluded \
|
||||
_site/ .
|
||||
git add -A
|
||||
@echo "Publishing web branch"
|
||||
@echo "Publishing web branch..."
|
||||
git commit -m "Publish."
|
||||
git push origin web:web
|
||||
@echo "Deleting web branch"
|
||||
@echo "Deleting web branch..."
|
||||
git checkout dev
|
||||
git branch -D web
|
||||
|
||||
|
@ -171,35 +142,18 @@ ifeq (,$(wildcard $(PLFA_AFS_DIR)))
|
|||
@exit 1
|
||||
else
|
||||
ifeq (,$(wildcard $(PLFA_AFS_DIR)/html))
|
||||
@echo "Checkout latest version from GitHub"
|
||||
git clone https://github.com/plfa/plfa.github.io.git --branch web --single-branch --depth 1 html
|
||||
endif
|
||||
@echo "Checkout latest version from GitHub"
|
||||
@cd $(PLFA_AFS_DIR)/html \
|
||||
cd $(PLFA_AFS_DIR)/html \
|
||||
&& git fetch --depth 1 \
|
||||
&& git reset --hard origin/web \
|
||||
&& git clean -dfx
|
||||
@echo "Setting permissions to include web server"
|
||||
@fsr setacl $(PLFA_AFS_DIR)/html system:groupwebserver rl
|
||||
fsr setacl $(PLFA_AFS_DIR)/html system:groupwebserver rl
|
||||
endif
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Build EPUB
|
||||
#################################################################################
|
||||
|
||||
include book/epub.mk
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Build PDF
|
||||
#################################################################################
|
||||
|
||||
include book/pdf.mk
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Setup or check dependencies
|
||||
# Setup dependencies
|
||||
#################################################################################
|
||||
|
||||
.PHONY: setup-check-stack
|
||||
|
@ -235,12 +189,11 @@ ifeq (,$(wildcard $(shell which fix-whitespace)))
|
|||
@echo " stack install --stack-yaml stack-8.8.3.yaml"
|
||||
endif
|
||||
|
||||
.PHONY: setup-check-latexmk
|
||||
setup-check-latexmk:
|
||||
ifeq (,$(wildcard $(shell which latexmk)))
|
||||
@echo "The command you called requires Latexmk"
|
||||
@echo "Latemk is included in MacTeX and MikTeX"
|
||||
@echo "See: https://mg.readthedocs.io/latexmk.html"
|
||||
.PHONY: setup-check-epubcheck
|
||||
setup-check-epubcheck:
|
||||
ifeq (,$(wildcard $(shell which epubcheck)))
|
||||
@echo "The command you called requires EPUBCheck"
|
||||
@echo "See: https://github.com/w3c/epubcheck"
|
||||
endif
|
||||
|
||||
.PHONY: setup-check-rsync
|
||||
|
@ -265,19 +218,6 @@ ifeq (,$(wildcard $(shell which bundle)))
|
|||
gem install bundle
|
||||
endif
|
||||
|
||||
.PHONY: setup-install-agda
|
||||
setup-install-agda: setup-check-stack
|
||||
ifeq (,$(wildcard $(shell stack exec which -- agda)))
|
||||
@echo "Installing Agda"
|
||||
stack build --only-dependencies
|
||||
endif
|
||||
|
||||
.PHONY: setup-install-pandoc
|
||||
setup-install-pandoc: setup-check-stack
|
||||
ifeq (,$(wildcard $(shell stack exec which -- pandoc)))
|
||||
@echo "Installing Pandoc"
|
||||
stack build --only-dependencies
|
||||
endif
|
||||
|
||||
#################################################################################
|
||||
# Build legacy versions of website using Jekyll
|
||||
|
|
15
README.md
15
README.md
|
@ -94,21 +94,20 @@ Finished hello.
|
|||
### Install PLFA and the Agda standard library
|
||||
You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading [the zip archive][plfa-dev]:
|
||||
```bash
|
||||
git clone --depth 1 --recurse-submodules --shallow-submodules https://github.com/plfa/plfa.github.io plfa
|
||||
# Remove `--depth 1` and `--shallow-submodules` if you want the complete git history of PLFA and the standard library.
|
||||
git clone --recurse-submodules https://github.com/plfa/plfa.github.io plfa
|
||||
```
|
||||
PLFA ships with the required version of the Agda standard library, so if you cloned with the `--recurse-submodules` flag, you’ve already got, in the `standard-library` directory!
|
||||
|
||||
If you forgot to add the `--recurse-submodules` flag, no worries, we can fix that!
|
||||
```bash
|
||||
cd plfa/
|
||||
git submodule update --init --recursive --depth 1
|
||||
# Remove `--depth 1` if you want the complete git history of the standard library.
|
||||
git submodule update --init --recursive
|
||||
```
|
||||
If you obtained PLFA by downloading the zip archive, you can get the required version of the Agda standard library from GitHub. You can either clone the repository and switch to the correct branch, or you can download the [the zip archive][agda-stdlib]:
|
||||
```bash
|
||||
git clone https://github.com/agda/agda-stdlib.git --branch v1.6 --depth 1 agda-stdlib
|
||||
# Remove `--depth 1` if you want the complete git history of the standard library.
|
||||
git clone https://github.com/agda/agda-stdlib.git agda-stdlib
|
||||
cd agda-stdlib
|
||||
git checkout v1.3
|
||||
```
|
||||
Finally, we need to let Agda know where to find the Agda standard library.
|
||||
You'll need the path where you installed the standard library. Check to see that the file “standard-library.agda-lib” exists, and make a note of the path to this file.
|
||||
|
@ -319,7 +318,9 @@ The repository comes with several Git hooks:
|
|||
You can install these Git hooks by calling `make init`.
|
||||
You can install [fix-whitespace][fix-whitespace] by running:
|
||||
```bash
|
||||
stack install fix-whitespace
|
||||
git clone https://github.com/agda/fix-whitespace
|
||||
cd fix-whitespace/
|
||||
stack install --stack-yaml stack-8.8.3.yaml
|
||||
```
|
||||
If you want Stack to use your system installation of GHC, follow the instructions for [Using an existing installation of GHC](#using-an-existing-installation-of-ghc).
|
||||
|
||||
|
|
Binary file not shown.
|
@ -1,90 +0,0 @@
|
|||
/* This is Pandoc's default ebook CSS, modified slightly. */
|
||||
/* https://github.com/jgm/pandoc/blob/master/data/epub.css */
|
||||
@font-face {
|
||||
font-family: 'DejaVu-mononoki-Symbola-Droid';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../fonts/DejaVu-mononoki-Symbola-Droid.woff');
|
||||
}
|
||||
|
||||
body {
|
||||
margin: 5%;
|
||||
text-align: justify;
|
||||
font-size: medium;
|
||||
}
|
||||
|
||||
code {
|
||||
font-family: 'DejaVu-mononoki-Symbola-Droid', monospace;
|
||||
}
|
||||
|
||||
h1,
|
||||
h2,
|
||||
h3,
|
||||
h4,
|
||||
h5,
|
||||
h6 {
|
||||
text-align: left;
|
||||
}
|
||||
|
||||
nav#toc ol,
|
||||
nav#landmarks ol {
|
||||
padding: 0;
|
||||
margin-left: 1em;
|
||||
}
|
||||
|
||||
nav#toc ol li,
|
||||
nav#landmarks ol li {
|
||||
list-style-type: none;
|
||||
margin: 0;
|
||||
padding: 0;
|
||||
}
|
||||
|
||||
a.footnote-ref {
|
||||
vertical-align: super;
|
||||
}
|
||||
|
||||
em,
|
||||
em em em,
|
||||
em em em em em {
|
||||
font-style: italic;
|
||||
}
|
||||
|
||||
em em,
|
||||
em em em em {
|
||||
font-style: normal;
|
||||
}
|
||||
|
||||
code {
|
||||
white-space: pre-wrap;
|
||||
}
|
||||
|
||||
span.smallcaps {
|
||||
font-variant: small-caps;
|
||||
}
|
||||
|
||||
span.underline {
|
||||
text-decoration: underline;
|
||||
}
|
||||
|
||||
q {
|
||||
quotes: "“""”""‘""’";
|
||||
}
|
||||
|
||||
div.column {
|
||||
display: inline-block;
|
||||
vertical-align: top;
|
||||
width: 50%;
|
||||
}
|
||||
|
||||
div.hanging-indent {
|
||||
margin-left: 1.5em;
|
||||
text-indent: -1.5em;
|
||||
}
|
||||
|
||||
/* Workaround for iBooks issue; see #6242 */
|
||||
@media screen {
|
||||
.sourceCode {
|
||||
overflow: visible !important;
|
||||
white-space: pre-wrap !important;
|
||||
}
|
||||
}
|
80
book/epub.mk
80
book/epub.mk
|
@ -1,80 +0,0 @@
|
|||
#################################################################################
|
||||
# Configuration
|
||||
#################################################################################
|
||||
|
||||
EPUB_DIR := book
|
||||
EPUB_TEMPLATE_DIR := $(EPUB_DIR)/templates
|
||||
EPUB_LUA_DIR := $(EPUB_DIR)/lua
|
||||
EPUB_LUA_SCRIPTS := $(wildcard $(EPUB_LUA_DIR)/*.lua)
|
||||
MD_DIR := src
|
||||
MD_FILES := README.md $(wildcard $(MD_DIR)/plfa/**/*.md)
|
||||
FRANKENFONT := public/webfonts/DejaVu-mononoki-Symbola-Droid.woff
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Compile PLFA to an EPUB using Pandoc
|
||||
#################################################################################
|
||||
|
||||
.PHONY: epub epub-build
|
||||
epub: epub-build
|
||||
epub-build: $(SITE_DIR)/plfa.epub
|
||||
|
||||
$(SITE_DIR)/plfa.epub: \
|
||||
$(RAW_DIR)/epub.md $(EPUB_DIR)/epub.css $(RAW_DIR)/epub.xml $(FRANKENFONT) \
|
||||
$(MD_FILES) $(EPUB_LUA_SCRIPTS) | setup-install-pandoc
|
||||
@echo "Building EPUB"
|
||||
@$(PANDOC) \
|
||||
--strip-comments \
|
||||
--css=$(EPUB_DIR)/epub.css \
|
||||
--epub-embed-font=$(FRANKENFONT) \
|
||||
--epub-metadata=$(RAW_DIR)/epub.xml \
|
||||
--indented-code-class=default \
|
||||
--lua-filter=$(EPUB_LUA_DIR)/set-default-code-class.lua -M default-code-class=agda \
|
||||
--lua-filter=$(EPUB_LUA_DIR)/remove-badges.lua -M badge-url=https://img.shields.io/badge/ \
|
||||
--lua-filter=$(EPUB_LUA_DIR)/epub-clean-html.lua \
|
||||
--lua-filter=$(EPUB_LUA_DIR)/single-file-links.lua \
|
||||
--lua-filter=$(EPUB_LUA_DIR)/single-file-identifiers.lua \
|
||||
--standalone \
|
||||
--toc --toc-depth=2 \
|
||||
--epub-chapter-level=2 \
|
||||
$< -o $@
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Test EPUB with EPUBCheck
|
||||
#################################################################################
|
||||
|
||||
.PHONY: epub-test
|
||||
epub-test: $(SITE_DIR)/plfa.epub | setup-check-epubcheck
|
||||
@echo "Testing EPUB with EPUBCheck"
|
||||
@epubcheck $(SITE_DIR)/plfa.epub
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Tasks for files that are generated by Hakyll
|
||||
#################################################################################
|
||||
|
||||
$(RAW_DIR)/epub.xml: $(EPUB_DIR)/epub.xml
|
||||
@make build
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Clean up and remove generated EPUB
|
||||
#################################################################################
|
||||
|
||||
.PHONY: epub-clean
|
||||
epub-clean:
|
||||
@echo "Cleaning generated files for EPUB"
|
||||
@rm -f $(SITE_DIR)/plfa.epub
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Setup or check dependencies
|
||||
#################################################################################
|
||||
|
||||
.PHONY: setup-check-epubcheck
|
||||
setup-check-epubcheck:
|
||||
ifeq (,$(wildcard $(shell which epubcheck)))
|
||||
@echo "The command you called requires EPUBCheck"
|
||||
@echo "See: https://github.com/w3c/epubcheck"
|
||||
endif
|
|
@ -1,5 +0,0 @@
|
|||
function RawBlock(el)
|
||||
-- Transforms '<ul class={something}>' into '<ul>'.
|
||||
el.text = el.text:gsub('%s*<%s*ul%s*class=%s*"?[%w-]+"?%s*>%s*', '<ul>')
|
||||
return el
|
||||
end
|
|
@ -1,47 +0,0 @@
|
|||
local unchecked_files = {}
|
||||
|
||||
local function is_checked()
|
||||
-- Check if any of our input files is an unchecked file.
|
||||
for _, input_file in pairs(PANDOC_STATE.input_files) do
|
||||
if unchecked_files[input_file] then
|
||||
if #PANDOC_STATE.input_files > 1 then
|
||||
error("Cannot handle multiple unchecked input files.")
|
||||
else
|
||||
return false
|
||||
end
|
||||
end
|
||||
end
|
||||
return true
|
||||
end
|
||||
|
||||
local function render_codeblock(cb)
|
||||
-- If a code block has class Agda or its class is omitted, format it as...
|
||||
--
|
||||
-- \begin{agda}\begin{code} .. \end{agda}\end{code}
|
||||
--
|
||||
-- ...otherwise, format it as...
|
||||
--
|
||||
-- \begin{pre} .. \end{pre}
|
||||
--
|
||||
-- Any file which is not checked by Agda must have its code blocks typeset in the latter style.
|
||||
-- Specify these files via the UNCHECKED_FILES environment variable.
|
||||
if is_checked() then
|
||||
if #cb.classes == 0 or cb.classes[1] == 'agda' then
|
||||
return pandoc.RawBlock('tex', '\\begin{agda}\n\\begin{code}\n' .. cb.text .. '\n\\end{code}\n\\end{agda}')
|
||||
end
|
||||
end
|
||||
return pandoc.RawBlock('tex', '\\begin{pre}\n' .. cb.text .. '\n\\end{pre}')
|
||||
end
|
||||
|
||||
local function get_unchecked_files(meta)
|
||||
if meta['unchecked-files'] then
|
||||
for unchecked_file in string.gmatch(pandoc.utils.stringify(meta['unchecked-files']), "([^ ]+)") do
|
||||
unchecked_files[unchecked_file] = true
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
return {
|
||||
{ Meta = get_unchecked_files },
|
||||
{ CodeBlock = render_codeblock }
|
||||
}
|
|
@ -1,22 +0,0 @@
|
|||
local badge_url = nil
|
||||
|
||||
local function remove_badges(ln)
|
||||
-- Remove link elements if their first child is a badge.
|
||||
if #ln.content > 0 and ln.content[1].t == "Image" then
|
||||
if string.find(ln.content[1].src, badge_url, 1, true) then
|
||||
return pandoc.Null()
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
local function get_badge_url(meta)
|
||||
if meta['badge-url'] then
|
||||
badge_url = pandoc.utils.stringify(meta['badge-url'])
|
||||
end
|
||||
end
|
||||
|
||||
|
||||
return {
|
||||
{ Meta = get_badge_url },
|
||||
{ Link = remove_badges }
|
||||
}
|
|
@ -1,31 +0,0 @@
|
|||
local chapter = nil
|
||||
|
||||
function Header(el)
|
||||
if el.level == 2 then
|
||||
chapter = el.attr.identifier
|
||||
end
|
||||
if el.level >= 3 then
|
||||
if el.attr.attributes.name then
|
||||
el.attr.identifier = chapter .. '-' .. el.attr.attributes.name
|
||||
el.attr.attributes.name = nil
|
||||
else
|
||||
el.attr.identifier = chapter .. '-' .. el.attr.identifier
|
||||
end
|
||||
end
|
||||
end
|
||||
|
||||
function show(t)
|
||||
local str = ''
|
||||
str = str .. '{'
|
||||
for k,v in pairs(t) do
|
||||
str = str .. k
|
||||
str = str .. ':'
|
||||
if type(v) == 'table' then
|
||||
str = str .. show(v)
|
||||
else
|
||||
str = str .. v
|
||||
end
|
||||
end
|
||||
str = str .. '}'
|
||||
return str
|
||||
end
|
|
@ -1,24 +0,0 @@
|
|||
-- from https://github.com/plfa/plfa.github.io/blob/dev/epub/rewrite-links.lua
|
||||
-- Performs the following transformations on Link targets:
|
||||
--
|
||||
-- Case 1:
|
||||
-- [text](/chapter/#more-stuff) -> [text](#chapter-more-stuff)
|
||||
--
|
||||
-- Case 2:
|
||||
-- [text](/chapter/) -> [text](#chapter)
|
||||
--
|
||||
-- All other Links are ignored.
|
||||
function Link(el)
|
||||
local n
|
||||
-- Case 1:
|
||||
el.target, n = el.target:gsub("^/(%w+)/#([%w-]+)$", "#%1-%2")
|
||||
-- Case 2:
|
||||
if n == 0 then
|
||||
el.target, n = el.target:gsub("^/(%w+)/$", "#%1")
|
||||
end
|
||||
-- If either Case 1 or Case 2, lowercase target:
|
||||
if n ~= 0 then
|
||||
el.target = string.lower(el.target)
|
||||
end
|
||||
return el
|
||||
end
|
164
book/pdf.mk
164
book/pdf.mk
|
@ -1,164 +0,0 @@
|
|||
#################################################################################
|
||||
# Configuration
|
||||
#################################################################################
|
||||
|
||||
PDF_DIR := book
|
||||
PDF_TEMPLATE_DIR := $(PDF_DIR)/templates
|
||||
PDF_LUA_DIR := $(PDF_DIR)/lua
|
||||
MD_DIR := src
|
||||
LAGDA_TEX_DIR := $(TMP_DIR)/lagda_tex
|
||||
TEX_DIR := $(TMP_DIR)/tex
|
||||
FRANKENFONT := $(PDF_DIR)/DejaVu-mononoki-Symbola-Droid.ttf
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Helper functions for translating paths
|
||||
#################################################################################
|
||||
|
||||
# Convert MD_DIR/%.md to its modified source path
|
||||
define MD_PATH
|
||||
$(patsubst $(MD_DIR)/%/acknowledgements.md,$(RAW_DIR)/%/acknowledgements.md,\
|
||||
$(patsubst $(PDF_DIR)/pdf.tex,$(RAW_DIR)/pdf.tex,$(1)))
|
||||
endef
|
||||
|
||||
# Convert MD_DIR/%.lagda.md to LAGDA_TEX_DIR/%.lagda.tex
|
||||
define LAGDA_TEX_PATH
|
||||
$(patsubst $(MD_DIR)/%.lagda.md,$(LAGDA_TEX_DIR)/%.lagda.tex,$(1))
|
||||
endef
|
||||
|
||||
# Convert MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex or TEX_DIR/%.tex
|
||||
#
|
||||
# NOTE: This logic is partially duplicated in hs/Main.hs:addTexPath:texPath.
|
||||
#
|
||||
define TEX_PATH
|
||||
$(patsubst $(RAW_DIR)/%,$(TEX_DIR)/%,\
|
||||
$(patsubst $(PDF_DIR)/%,$(TEX_DIR)/%,\
|
||||
$(patsubst README.md,$(TEX_DIR)/plfa/frontmatter/README.tex,\
|
||||
$(patsubst $(MD_DIR)/%.md,$(TEX_DIR)/%.tex,\
|
||||
$(patsubst $(MD_DIR)/%.lagda.md,$(TEX_DIR)/%.tex,$(1))))))
|
||||
endef
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Lists of source and intermediate files
|
||||
#################################################################################
|
||||
|
||||
PDF_LUA_SCRIPTS := $(wildcard $(PDF_LUA_DIR)/*.lua)
|
||||
PDF_STATIC_FILES := $(PDF_DIR)/pdf.tex $(FRANKENFONT)
|
||||
MD_FILES := README.md $(wildcard $(MD_DIR)/plfa/**/*.md)
|
||||
LAGDA_MD_FILES := $(filter %.lagda.md,$(MD_FILES))
|
||||
LAGDA_TEX_FILES := $(call LAGDA_TEX_PATH,$(LAGDA_MD_FILES))
|
||||
TEX_FILES := $(call TEX_PATH,$(MD_FILES) $(RAW_DIR)/pdf.tex $(PDF_STATIC_FILES))
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Compile PLFA to a PDF using Pandoc and Latexmk
|
||||
#################################################################################
|
||||
|
||||
.PHONY: pdf pdf-build
|
||||
pdf: pdf-build
|
||||
pdf-build: $(SITE_DIR)/plfa.pdf
|
||||
|
||||
$(SITE_DIR)/plfa.pdf: $(TEX_FILES)
|
||||
@echo "Building PDF"
|
||||
@cd $(TEX_DIR) && latexmk -pdf -lualatex -use-make -halt-on-error pdf.tex
|
||||
@cp $(TEX_DIR)/pdf.pdf $(SITE_DIR)/plfa.pdf
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Definitions of various compilation tasks
|
||||
#################################################################################
|
||||
|
||||
# Copy static files needed by PDF compilation
|
||||
define MK_COPYSTATIC_RULE
|
||||
src := $(1)
|
||||
dst := $(2)
|
||||
$$(dst): $$(src)
|
||||
@echo "Copy $$< to $$@"
|
||||
@mkdir -p '$$(@D)'
|
||||
@cp $$< $$@
|
||||
endef
|
||||
|
||||
# Copy static files from PDF_DIR/% to TEX_DIR/%
|
||||
$(foreach static_file,\
|
||||
$(PDF_STATIC_FILES),\
|
||||
$(eval $(call MK_COPYSTATIC_RULE,\
|
||||
$(call MD_PATH,$(static_file)),\
|
||||
$(call TEX_PATH,$(static_file)))))
|
||||
|
||||
|
||||
# Compile Markdown files to LaTeX
|
||||
#
|
||||
# NOTE: Passing --indented-code-classes=default sets the class for /indented/ code blocks
|
||||
# to 'default', which lets us distinguish them from /fenced/ code blocks without a
|
||||
# class. That's important, since fenced code blocks are checked by Agda, but indented
|
||||
# code blocks are /not/, so latex-render-codeblocks.lua needs to be able to tell the
|
||||
# difference.
|
||||
#
|
||||
define MK_MD2TEX_RULE
|
||||
src := $(1)
|
||||
dst := $(2)
|
||||
$$(dst): $$(src) $(PDF_LUA_SCRIPTS) | setup-install-pandoc
|
||||
@echo "Compile $$< to $$@"
|
||||
@mkdir -p '$$(@D)'
|
||||
@$(PANDOC) \
|
||||
--top-level-division=chapter \
|
||||
--indented-code-classes=default \
|
||||
--lua-filter=$(PDF_LUA_DIR)/remove-badges.lua -M badge-url=https://img.shields.io/badge/ \
|
||||
--lua-filter=$(PDF_LUA_DIR)/latex-render-codeblocks.lua -M unchecked-files=README.md \
|
||||
--lua-filter=$(PDF_LUA_DIR)/single-file-links.lua \
|
||||
$$< -o $$@
|
||||
endef
|
||||
|
||||
# Compile .md files (from MD_DIR/%.md to TEX_DIR/%.tex)
|
||||
$(foreach md_file,\
|
||||
$(filter-out %.lagda.md,$(MD_FILES)),\
|
||||
$(eval $(call MK_MD2TEX_RULE,\
|
||||
$(call MD_PATH,$(md_file)),\
|
||||
$(call TEX_PATH,$(md_file)))))
|
||||
|
||||
# Compile .lagda.md files (from MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex)
|
||||
$(foreach lagda_md_file,\
|
||||
$(LAGDA_MD_FILES),\
|
||||
$(eval $(call MK_MD2TEX_RULE,\
|
||||
$(lagda_md_file),\
|
||||
$(call LAGDA_TEX_PATH,$(lagda_md_file)))))
|
||||
|
||||
|
||||
# Compile Literate Agda files to LaTeX
|
||||
define MK_LAGDA_MD2TEX_RULE
|
||||
src := $(1)
|
||||
dst := $(2)
|
||||
$$(dst): $$(src) $(LAGDA_TEX_FILES) | setup-install-agda setup-check-latexmk
|
||||
@$(AGDA) --include-path=$(LAGDA_TEX_DIR) --latex --latex-dir=$(TEX_DIR) $$<
|
||||
endef
|
||||
|
||||
# Compile .lagda.tex files (from LAGDA_TEX_DIR/%.lagda.tex to TEX_DIR/%.tex)
|
||||
$(foreach lagda_md_file,\
|
||||
$(LAGDA_MD_FILES),\
|
||||
$(eval $(call MK_LAGDA_MD2TEX_RULE,\
|
||||
$(call LAGDA_TEX_PATH,$(lagda_md_file)),\
|
||||
$(call TEX_PATH,$(lagda_md_file)))))
|
||||
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Tasks for files that are generated by Hakyll
|
||||
#################################################################################
|
||||
|
||||
$(RAW_DIR)/pdf.tex: $(PDF_DIR)/pdf.tex $(MD_DIR)/plfa/toc.metadata
|
||||
@make build
|
||||
|
||||
# Generated by Hakyll
|
||||
$(RAW_DIR)/plfa/backmatter/acknowledgements.md: $(MD_DIR)/plfa/backmatter/acknowledgements.md
|
||||
@make build
|
||||
|
||||
|
||||
#################################################################################
|
||||
# Clean up and remove generated PDF
|
||||
#################################################################################
|
||||
|
||||
.PHONY: pdf-clean
|
||||
pdf-clean:
|
||||
@echo "Cleaning generated files for PDF"
|
||||
@rm -rf $(SITE_DIR)/plfa.pdf $(LAGDA_TEX_DIR) $(TEX_DIR)
|
166
book/pdf.tex
166
book/pdf.tex
|
@ -1,166 +0,0 @@
|
|||
\documentclass[10pt]{book}
|
||||
|
||||
\usepackage{hyperref}
|
||||
\usepackage[links]{agda}
|
||||
\usepackage{fontspec}
|
||||
\setmainfont{DejaVu Sans}
|
||||
\setsansfont{DejaVu Sans}
|
||||
\setmonofont{[DejaVu-mononoki-Symbola-Droid.ttf]}
|
||||
\usepackage{soul}
|
||||
\usepackage{tcolorbox}
|
||||
\tcbuselibrary{skins,breakable}
|
||||
\usepackage{fancyvrb}
|
||||
\usepackage{xcolor}
|
||||
\usepackage{tikz}
|
||||
\usepackage{setspace}
|
||||
\usepackage{geometry}
|
||||
\geometry{
|
||||
a4paper,
|
||||
total={170mm,257mm},
|
||||
left=20mm,
|
||||
top=20mm,
|
||||
}
|
||||
|
||||
|
||||
% Wrap texttt lines
|
||||
\sloppy
|
||||
|
||||
% Disable section numbering
|
||||
\setcounter{secnumdepth}{0}
|
||||
|
||||
% Set the global text color:
|
||||
\definecolor{textcolor}{HTML}{111111}
|
||||
\color{textcolor}
|
||||
|
||||
% Change background color for inline code in markdown files.
|
||||
% The following code does not work well for long text as the
|
||||
% text will exceed the page boundary.
|
||||
\definecolor{background-color}{HTML}{EEEEFF}
|
||||
\let\oldtexttt\texttt%
|
||||
\renewcommand{\texttt}[1]{\colorbox{background-color}{\oldtexttt{#1}}}
|
||||
|
||||
% Box with background colour similar to web version:
|
||||
\newtcolorbox{agda}[1][]{
|
||||
frame hidden,
|
||||
colback=background-color,
|
||||
spartan,
|
||||
left=5pt,
|
||||
boxrule=0pt,
|
||||
breakable,
|
||||
}
|
||||
|
||||
% Verbatim environment similarly indented to Agda code blocks.
|
||||
\DefineVerbatimEnvironment{verbatim}{Verbatim}{xleftmargin=0pt}%
|
||||
|
||||
% Adding backgrounds to verbatim environments.
|
||||
\newenvironment{pre}{
|
||||
\VerbatimEnvironment
|
||||
\begin{agda}
|
||||
\begin{verbatim}
|
||||
}{\end{verbatim}
|
||||
\end{agda}
|
||||
}
|
||||
|
||||
% Use special font families without TeX ligatures for Agda code.
|
||||
% Solution inspired by a comment by Enrico Gregorio:
|
||||
% https://tex.stackexchange.com/a/103078
|
||||
\newfontfamily{\AgdaSerifFont}{DejaVu-Serif}
|
||||
\newfontfamily{\AgdaSansSerifFont}{DejaVu-Sans}
|
||||
\newfontfamily{\AgdaTypewriterFont}{DejaVu-mononoki-Symbola-Droid}
|
||||
\renewcommand{\AgdaFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
||||
\renewcommand{\AgdaKeywordFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
||||
\renewcommand{\AgdaStringFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
||||
\renewcommand{\AgdaCommentFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
||||
\renewcommand{\AgdaBoundFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
||||
|
||||
\AgdaNoSpaceAroundCode{}
|
||||
|
||||
% Adjust spacing after toc numbering
|
||||
\usepackage{tocloft}
|
||||
\setlength\cftchapnumwidth{3em}
|
||||
\cftsetpnumwidth{4em}
|
||||
|
||||
% Style links with colors instead of boxes:
|
||||
% https://tex.stackexchange.com/q/823
|
||||
\definecolor{linkcolor}{HTML}{2A7AE2}
|
||||
\hypersetup{
|
||||
colorlinks,
|
||||
linkcolor={linkcolor},
|
||||
citecolor={linkcolor},
|
||||
urlcolor={linkcolor}
|
||||
}
|
||||
|
||||
\begin{document}
|
||||
|
||||
% Adjust indentation of Agda code blocks
|
||||
\setlength{\mathindent}{0pt}
|
||||
\setlength{\parindent}{0em}
|
||||
\setlength{\parskip}{1em}
|
||||
|
||||
% Provide \tightlist environment
|
||||
% https://tex.stackexchange.com/q/257418
|
||||
\providecommand{\tightlist}{%
|
||||
\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
|
||||
|
||||
% Based on \titleAM:
|
||||
% https://ctan.org/pkg/titlepages
|
||||
\begin{titlepage}
|
||||
\newlength{\drop}%
|
||||
\setlength{\drop}{0.12\textheight}%
|
||||
\centering%
|
||||
\vspace*{\drop}
|
||||
\begingroup% Ancient Mariner, AW p. 151
|
||||
{\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip]
|
||||
{\Huge PROGRAMMING LANGUAGE}\\[\baselineskip]
|
||||
{\Huge FOUNDATIONS}\\[\baselineskip]
|
||||
{\Large IN}\\[\baselineskip]
|
||||
{\Huge Agda}\\[\drop]
|
||||
\vfill%
|
||||
{\small\scshape 2021}\par%
|
||||
\null\endgroup
|
||||
\end{titlepage}
|
||||
|
||||
$for(parts)$
|
||||
|
||||
% Open front, main, and back matter sections:
|
||||
$if(frontmatter)$
|
||||
\frontmatter%
|
||||
\setcounter{tocdepth}{0}
|
||||
|
||||
\tableofcontents%
|
||||
\setcounter{tocdepth}{1}
|
||||
$endif$
|
||||
$if(mainmatter)$
|
||||
\mainmatter%
|
||||
$endif$
|
||||
$if(backmatter)$
|
||||
\appendix
|
||||
\addcontentsline{toc}{part}{Appendices}
|
||||
$endif$
|
||||
|
||||
% Only print title for main and back matter:
|
||||
$if(frontmatter)$
|
||||
% NOTE: Front matter titles are inserted via book/lua/single-file-headers.lua.
|
||||
$else$
|
||||
\part{$title$}
|
||||
$endif$
|
||||
|
||||
% Include each section.
|
||||
$for(sections)$
|
||||
\hypertarget{$anchor$}{%
|
||||
\chapter{$title$}\label{$anchor$}}
|
||||
\input{$tex_path$}
|
||||
$endfor$
|
||||
|
||||
% Close front, main, and back matter sections:
|
||||
$if(frontmatter)$
|
||||
$endif$
|
||||
$if(mainmatter)$
|
||||
\cleardoublepage%
|
||||
\phantomsection%
|
||||
$endif$
|
||||
$if(backmatter)$
|
||||
$endif$
|
||||
$endfor$
|
||||
|
||||
\end{document}
|
|
@ -982,15 +982,15 @@ Remember to indent all code by two spaces.
|
|||
```
|
||||
ext∋ : ∀ {Γ B x y}
|
||||
→ x ≢ y
|
||||
→ ¬ ∃[ A ]( Γ ∋ x ⦂ A )
|
||||
→ ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
|
||||
-----------------------------
|
||||
→ ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
|
||||
→ ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
|
||||
ext∋ x≢y _ ⟨ A , Z ⟩ = x≢y refl
|
||||
ext∋ _ ¬∃ ⟨ A , S _ ⊢x ⟩ = ¬∃ ⟨ A , ⊢x ⟩
|
||||
|
||||
lookup : ∀ (Γ : Context) (x : Id)
|
||||
------------------------
|
||||
→ Dec (∃[ A ]( Γ ∋ x ⦂ A ))
|
||||
-----------------------
|
||||
→ Dec (∃[ A ](Γ ∋ x ⦂ A))
|
||||
lookup ∅ x = no (λ ())
|
||||
lookup (Γ , y ⦂ B) x with x ≟ y
|
||||
... | yes refl = yes ⟨ B , Z ⟩
|
||||
|
@ -1006,7 +1006,7 @@ Remember to indent all code by two spaces.
|
|||
→ Γ ⊢ L ↑ A ⇒ B
|
||||
→ ¬ Γ ⊢ M ↓ A
|
||||
----------------------------
|
||||
→ ¬ ∃[ B′ ]( Γ ⊢ L · M ↑ B′ )
|
||||
→ ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
|
||||
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
|
||||
|
||||
¬switch : ∀ {Γ M A B}
|
||||
|
@ -1022,12 +1022,12 @@ Remember to indent all code by two spaces.
|
|||
|
||||
```
|
||||
synthesize : ∀ (Γ : Context) (M : Term⁺)
|
||||
-----------------------
|
||||
→ Dec (∃[ A ]( Γ ⊢ M ↑ A ))
|
||||
-----------------------
|
||||
→ Dec (∃[ A ](Γ ⊢ M ↑ A))
|
||||
|
||||
inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
|
||||
---------------
|
||||
→ Dec (Γ ⊢ M ↓ A)
|
||||
---------------
|
||||
→ Dec (Γ ⊢ M ↓ A)
|
||||
|
||||
synthesize Γ (` x) with lookup Γ x
|
||||
... | no ¬∃ = no (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
|
||||
|
|
|
@ -589,9 +589,9 @@ module Problem3 where
|
|||
```
|
||||
ext∋ : ∀ {Γ B x y}
|
||||
→ x ≢ y
|
||||
→ ¬ ∃[ A ]( Γ ∋ x ⦂ A )
|
||||
→ ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
|
||||
-----------------------------
|
||||
→ ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
|
||||
→ ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
|
||||
ext∋ x≢y _ ⟨ A , Z ⟩ = x≢y refl
|
||||
ext∋ _ ¬∃ ⟨ A , S _ ⊢x ⟩ = ¬∃ ⟨ A , ⊢x ⟩
|
||||
|
||||
|
@ -614,7 +614,7 @@ module Problem3 where
|
|||
→ Γ ⊢ L ↑ A ⇒ B
|
||||
→ ¬ Γ ⊢ M ↓ A
|
||||
----------------------------
|
||||
→ ¬ ∃[ B′ ]( Γ ⊢ L · M ↑ B′ )
|
||||
→ ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
|
||||
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
|
||||
|
||||
¬switch : ∀ {Γ M A B}
|
||||
|
@ -631,7 +631,7 @@ module Problem3 where
|
|||
```
|
||||
synthesize : ∀ (Γ : Context) (M : Term⁺)
|
||||
-----------------------
|
||||
→ Dec (∃[ A ]( Γ ⊢ M ↑ A ))
|
||||
→ Dec (∃[ A ](Γ ⊢ M ↑ A))
|
||||
|
||||
inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
|
||||
---------------
|
||||
|
|
42
css/epub.css
Normal file
42
css/epub.css
Normal file
|
@ -0,0 +1,42 @@
|
|||
/* This is Pandoc's default ebook CSS, modified slightly. */
|
||||
/* https://github.com/jgm/pandoc/blob/master/data/epub.css */
|
||||
@font-face {
|
||||
font-family: 'mononoki';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../webfonts/mononoki.woff');
|
||||
}
|
||||
@font-face {
|
||||
font-family: 'FreeMono';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../webfonts/FreeMono.woff');
|
||||
}
|
||||
@font-face {
|
||||
font-family: 'DejaVuSansMono';
|
||||
font-weight: normal;
|
||||
font-style: normal;
|
||||
src: url('../webfonts/DejaVuSansMono.woff');
|
||||
}
|
||||
body { margin: 5%; text-align: justify; font-size: medium; }
|
||||
code { font-family: 'mononoki', 'FreeMono', 'DejaVuSansMono', monospace; }
|
||||
h1, h2, h3, h4, h5, h6 { text-align: left; }
|
||||
nav#toc ol, nav#landmarks ol { padding: 0; margin-left: 1em; }
|
||||
nav#toc ol li, nav#landmarks ol li { list-style-type: none; margin: 0; padding: 0; }
|
||||
a.footnote-ref { vertical-align: super; }
|
||||
em, em em em, em em em em em { font-style: italic;}
|
||||
em em, em em em em { font-style: normal; }
|
||||
code{ white-space: pre-wrap; }
|
||||
span.smallcaps{ font-variant: small-caps; }
|
||||
span.underline{ text-decoration: underline; }
|
||||
q { quotes: "“" "”" "‘" "’"; }
|
||||
div.column{ display: inline-block; vertical-align: top; width: 50%; }
|
||||
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
|
||||
|
||||
/* Workaround for iBooks issue; see #6242 */
|
||||
@media screen {
|
||||
.sourceCode {
|
||||
overflow: visible !important;
|
||||
white-space: pre-wrap !important;
|
||||
}
|
||||
}
|
|
@ -1,8 +1,3 @@
|
|||
@font-face{
|
||||
font-family: DejaVu mononoki Symbola Droid;
|
||||
src:
|
||||
url('../webfonts/DejaVu-mononoki-Symbola-Droid.woff') format('woff')
|
||||
}
|
||||
@font-face {
|
||||
font-family: 'mononoki';
|
||||
src: url('../webfonts/mononoki.woff2') format('woff2'),
|
||||
|
@ -24,7 +19,7 @@
|
|||
}
|
||||
|
||||
@mixin code-font {
|
||||
font-family: 'DejaVu mononoki Symbola Droid', 'mononoki', 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif;
|
||||
font-family: 'mononoki', 'DejaVu Sans Mono', 'Source Code Pro', 'Bitstream Vera Sans Mono', 'FreeMono', 'Courier New', 'Monaco', 'Menlo', monospace, serif;
|
||||
font-size: .85em;
|
||||
}
|
||||
@mixin code-container {
|
||||
|
|
26
emacs/init.el
Normal file
26
emacs/init.el
Normal file
|
@ -0,0 +1,26 @@
|
|||
(require 'use-package)
|
||||
(require 'use-package-ensure)
|
||||
(setq use-package-always-ensure t)
|
||||
|
||||
(use-package evil)
|
||||
(use-package agda2-mode)
|
||||
(use-package gruvbox-theme)
|
||||
|
||||
(setq evil-undo-system 'undo-tree)
|
||||
(require 'evil)
|
||||
(evil-mode 1)
|
||||
|
||||
(load-theme 'gruvbox t)
|
||||
|
||||
(menu-bar-mode -1)
|
||||
(tool-bar-mode -1)
|
||||
(toggle-scroll-bar -1)
|
||||
|
||||
(load-file (let ((coding-system-for-read 'utf-8))
|
||||
(shell-command-to-string "agda-mode locate")))
|
||||
|
||||
(setq auto-mode-alist
|
||||
(append
|
||||
'(("\\.agda\\'" . agda2-mode)
|
||||
("\\.lagda.md\\'" . agda2-mode))
|
||||
auto-mode-alist))
|
|
@ -8,21 +8,19 @@
|
|||
|
||||
local default_code_classes = {}
|
||||
|
||||
local function add_default_code_class(el)
|
||||
function add_default_code_class(el)
|
||||
if #(el.classes) == 0 then
|
||||
el.classes = default_code_classes
|
||||
return el
|
||||
end
|
||||
end
|
||||
|
||||
local function get_default_code_class(meta)
|
||||
function get_default_code_class(meta)
|
||||
if meta['default-code-class'] then
|
||||
default_code_classes = {pandoc.utils.stringify(meta['default-code-class'])}
|
||||
end
|
||||
end
|
||||
|
||||
return {
|
||||
{Meta = get_default_code_class},
|
||||
{Code = add_default_code_class},
|
||||
{CodeBlock = add_default_code_class}
|
||||
}
|
||||
return {{Meta = get_default_code_class},
|
||||
{Code = add_default_code_class},
|
||||
{CodeBlock = add_default_code_class}}
|
61
epub/include-files.lua
Normal file
61
epub/include-files.lua
Normal file
|
@ -0,0 +1,61 @@
|
|||
--- include-files.lua – filter to include Markdown files
|
||||
---
|
||||
--- Copyright: © 2019–2020 Albert Krewinkel
|
||||
--- Copyright: © 2020 Michael Reed
|
||||
--- License: MIT – see LICENSE file for details
|
||||
---
|
||||
--- Created by Albert Krewinkel. Slightly modified by Michael Reed for use in
|
||||
--- generating the EPUB for "Programming Language Foundations in Agda".
|
||||
---
|
||||
--- For documentation, see: https://github.com/pandoc/lua-filters/tree/master/include-files
|
||||
|
||||
-- pandoc's List type
|
||||
local List = require 'pandoc.List'
|
||||
|
||||
--- Shift headings in block list by given number
|
||||
function shift_headings(blocks, shift_by)
|
||||
if not shift_by then
|
||||
return blocks
|
||||
end
|
||||
|
||||
local shift_headings_filter = {
|
||||
Header = function (header)
|
||||
header.level = header.level + shift_by
|
||||
return header
|
||||
end
|
||||
}
|
||||
|
||||
return pandoc.walk_block(pandoc.Div(blocks), shift_headings_filter).content
|
||||
end
|
||||
|
||||
--- Filter function for code blocks
|
||||
function CodeBlock(cb)
|
||||
-- ignore code blocks which are not of class "include".
|
||||
if not cb.classes:includes 'include' then
|
||||
return
|
||||
end
|
||||
|
||||
-- Markdown is used if this is nil.
|
||||
local format = cb.attributes['format']
|
||||
local shift_heading_level_by =
|
||||
tonumber(cb.attributes['shift-heading-level-by'])
|
||||
|
||||
|
||||
local blocks = List:new()
|
||||
for line in cb.text:gmatch('[^\n]+') do
|
||||
if line:sub(1,2) ~= '//' then
|
||||
-- Read in the document at the file path specified by `line`.
|
||||
local fh = io.open(line)
|
||||
local document = pandoc.read(fh:read '*a', format)
|
||||
-- Before shifting headings, add a title heading at the beginning of the chapter.
|
||||
local heading = pandoc.Header(1, pandoc.Str(pandoc.utils.stringify(document.meta.title)))
|
||||
document.blocks:insert(1, heading)
|
||||
-- Shift all headings by the user-specified amount, which is 0 by default.
|
||||
local chapter = shift_headings(document.blocks, shift_heading_level_by)
|
||||
-- Concatenate the chapter blocks (discarding the metadata) to the current document.
|
||||
blocks:extend(chapter)
|
||||
fh:close()
|
||||
end
|
||||
end
|
||||
return blocks
|
||||
end
|
19
epub/render-liquid-template.rb
Normal file
19
epub/render-liquid-template.rb
Normal file
|
@ -0,0 +1,19 @@
|
|||
#!/usr/bin/env ruby
|
||||
require 'yaml'
|
||||
require 'liquid'
|
||||
|
||||
unless ARGV.length == 3
|
||||
abort "Usage: render-liquid-template.rb [yaml_file] [markdown_in_file] [markdown_out_file]"
|
||||
end
|
||||
|
||||
yaml_file, markdown_file_in, markdown_file_out = ARGV
|
||||
|
||||
[yaml_file, markdown_file_in].each do |file|
|
||||
unless File.file? file
|
||||
abort "File does not exist: '%s'" % [file]
|
||||
end
|
||||
end
|
||||
|
||||
metadata = { 'site' => (YAML.load (File.read yaml_file)) }
|
||||
template = Liquid::Template.parse (File.read markdown_file_in)
|
||||
File.write markdown_file_out, (template.render metadata)
|
5
epub/rewrite-html-ul.lua
Normal file
5
epub/rewrite-html-ul.lua
Normal file
|
@ -0,0 +1,5 @@
|
|||
-- Transforms '<ul class={something}>' into '<ul>'.
|
||||
function RawBlock (el)
|
||||
el.text = el.text:gsub('%s*<%s*ul%s*class=%s*"?[%w-]+"?%s*>%s*', '<ul>')
|
||||
return el
|
||||
end
|
19
epub/rewrite-links.lua
Normal file
19
epub/rewrite-links.lua
Normal file
|
@ -0,0 +1,19 @@
|
|||
-- Performs the following transformations on Link targets:
|
||||
--
|
||||
-- Case 1:
|
||||
-- [text](/chapter/#more-stuff) -> [text](#chapter-more-stuff)
|
||||
--
|
||||
-- Case 2:
|
||||
-- [text](/chapter/) -> [text](#chapter)
|
||||
--
|
||||
-- All other Links are ignored.
|
||||
function Link (el)
|
||||
local n
|
||||
-- Case 1:
|
||||
el.target, n = el.target:gsub("^/(%w+)/#([%w-]+)$", "#%1-%2")
|
||||
-- Case 2:
|
||||
if n == 0 then
|
||||
el.target = el.target:gsub("^/(%w+)/$", "#%1")
|
||||
end
|
||||
return el
|
||||
end
|
77
flake.lock
Normal file
77
flake.lock
Normal file
|
@ -0,0 +1,77 @@
|
|||
{
|
||||
"nodes": {
|
||||
"flake-utils": {
|
||||
"locked": {
|
||||
"lastModified": 1631561581,
|
||||
"narHash": "sha256-3VQMV5zvxaVLvqqUrNz3iJelLw30mIVSfZmAaauM3dA=",
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"rev": "7e5bf3925f6fbdfaf50a2a7ca0be2879c4261d19",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "numtide",
|
||||
"repo": "flake-utils",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs": {
|
||||
"locked": {
|
||||
"lastModified": 1634090417,
|
||||
"narHash": "sha256-GGRQSC+dBFtynnwHCG65bdzygXK058NJ92boHGXz8Gg=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "c9ddb803ce95c0ec2ab4d57ba29f136b8ce9fe71",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"nixpkgs-agda": {
|
||||
"locked": {
|
||||
"lastModified": 1624913309,
|
||||
"narHash": "sha256-HHZTzHgLuoOmTrHckl9eGG8UWTp32pYXmCoOjgQYIB4=",
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "860b56be91fb874d48e23a950815969a7b832fbc",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "nixos",
|
||||
"repo": "nixpkgs",
|
||||
"rev": "860b56be91fb874d48e23a950815969a7b832fbc",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"plfa": {
|
||||
"flake": false,
|
||||
"locked": {
|
||||
"lastModified": 1628614312,
|
||||
"narHash": "sha256-e5wLKKjabrZesjAd5p5sXeYW28LXoZPGY2jp6cnB9qM=",
|
||||
"owner": "plfa",
|
||||
"repo": "plfa.github.io",
|
||||
"rev": "8fec0eb208e48401908414347d060767af48309f",
|
||||
"type": "github"
|
||||
},
|
||||
"original": {
|
||||
"owner": "plfa",
|
||||
"repo": "plfa.github.io",
|
||||
"rev": "8fec0eb208e48401908414347d060767af48309f",
|
||||
"type": "github"
|
||||
}
|
||||
},
|
||||
"root": {
|
||||
"inputs": {
|
||||
"flake-utils": "flake-utils",
|
||||
"nixpkgs": "nixpkgs",
|
||||
"nixpkgs-agda": "nixpkgs-agda",
|
||||
"plfa": "plfa"
|
||||
}
|
||||
}
|
||||
},
|
||||
"root": "root",
|
||||
"version": 7
|
||||
}
|
69
flake.nix
Normal file
69
flake.nix
Normal file
|
@ -0,0 +1,69 @@
|
|||
{
|
||||
inputs = {
|
||||
nixpkgs.url = "github:nixos/nixpkgs";
|
||||
flake-utils.url = "github:numtide/flake-utils";
|
||||
|
||||
nixpkgs-agda.url = "github:nixos/nixpkgs?rev=860b56be91fb874d48e23a950815969a7b832fbc";
|
||||
plfa = {
|
||||
flake = false;
|
||||
url = "github:plfa/plfa.github.io?rev=8fec0eb208e48401908414347d060767af48309f";
|
||||
};
|
||||
};
|
||||
|
||||
outputs = { self, nixpkgs, nixpkgs-agda, flake-utils, plfa }:
|
||||
flake-utils.lib.eachDefaultSystem (system:
|
||||
let
|
||||
pkgs = nixpkgs.legacyPackages.${system};
|
||||
|
||||
myPkgs = rec {
|
||||
agda = import ./nix/agda.nix {
|
||||
inherit system plfa;
|
||||
nixpkgs = nixpkgs-agda;
|
||||
};
|
||||
nvim-agda = import ./nix/nvim-agda {
|
||||
inherit system;
|
||||
nixpkgs = nixpkgs-agda;
|
||||
};
|
||||
|
||||
neovim = pkgs.callPackage ./nix/neovim.nix { inherit nvim-agda; };
|
||||
};
|
||||
|
||||
vscode-agda-mode = pkgs.vscode-utils.extensionFromVscodeMarketplace {
|
||||
name = "agda-mode";
|
||||
publisher = "banacorn";
|
||||
version = "0.2.19";
|
||||
sha256 = "2PFfFySOoxFEZdYb2BF6XQeYEygbTn/WJub/8IKfc1Y=";
|
||||
};
|
||||
combinedExtensionsDrv = pkgs.buildEnv {
|
||||
name = "vscodium-extensions";
|
||||
paths = [
|
||||
vscode-agda-mode
|
||||
pkgs.vscode-extensions.vscodevim.vim
|
||||
];
|
||||
};
|
||||
vscodium = pkgs.runCommand "vscodium-with-extensions" {
|
||||
nativeBuildInputs = [ pkgs.makeWrapper ];
|
||||
buildInputs = [ pkgs.vscodium ];
|
||||
meta = pkgs.vscodium.meta;
|
||||
} ''
|
||||
mkdir -p $out/bin
|
||||
makeWrapper "${pkgs.vscodium}/bin/codium" "$out/bin/codium" \
|
||||
--add-flags "--extensions-dir ${combinedExtensionsDrv}/share/vscode/extensions"
|
||||
'';
|
||||
in
|
||||
{
|
||||
packages = flake-utils.lib.flattenTree myPkgs;
|
||||
|
||||
devShell = pkgs.mkShell {
|
||||
buildInputs = with pkgs; with myPkgs; [
|
||||
agda
|
||||
vscodium
|
||||
neovim
|
||||
nvim-agda
|
||||
lua51Packages.luautf8
|
||||
];
|
||||
};
|
||||
}
|
||||
);
|
||||
}
|
||||
|
|
@ -5,7 +5,6 @@
|
|||
module Hakyll.Web.Agda
|
||||
( agdaCompilerWith
|
||||
, agdaVerbosityQuiet
|
||||
, compileAgdaWith
|
||||
, CommandLineOptions(..)
|
||||
, PragmaOptions(..)
|
||||
, defaultAgdaOptions
|
||||
|
@ -51,12 +50,8 @@ defaultAgdaPragmaOptions = defaultPragmaOptions
|
|||
|
||||
-- |Compile literate Agda to HTML
|
||||
agdaCompilerWith :: CommandLineOptions -> Compiler (Item String)
|
||||
agdaCompilerWith agdaOptions =
|
||||
getResourceBody >>= compileAgdaWith agdaOptions
|
||||
|
||||
-- |Compile literate Agda to HTML
|
||||
compileAgdaWith :: CommandLineOptions -> Item String -> Compiler (Item String)
|
||||
compileAgdaWith agdaOptions item = cached "Hakyll.Web.Agda.agdaCompilerWith" $ do
|
||||
agdaCompilerWith agdaOptions = cached "Hakyll.Web.Agda.agdaCompilerWith" $ do
|
||||
item <- getResourceBody
|
||||
let agdaPath = toFilePath (itemIdentifier item)
|
||||
let moduleName = agdaModule (itemBody item)
|
||||
TmpFile tmpPath <- newTmpFile ".lock"
|
||||
|
@ -125,7 +120,7 @@ readStdlibVersion stdlibPath = do
|
|||
changelog <- T.readFile changelogPath
|
||||
let versionLine = head (T.lines changelog)
|
||||
case T.stripPrefix "Version " versionLine of
|
||||
Just versionStr -> return $ T.unpack ("v" <> T.strip versionStr)
|
||||
Just versionStr -> return . T.unpack $ "v" <> T.strip versionStr
|
||||
Nothing -> error $ printf "Could not read version from '%s'" changelogPath
|
||||
|
||||
-- |Fix references to the Agda standard library.
|
||||
|
|
|
@ -3,6 +3,7 @@
|
|||
module Hakyll.Web.Routes.Permalink
|
||||
( convertPermalink
|
||||
, permalinkRoute
|
||||
, permalinkRouteWithDefault
|
||||
, stripIndexFile
|
||||
) where
|
||||
|
||||
|
@ -18,12 +19,11 @@ convertPermalink :: FilePath -> FilePath
|
|||
convertPermalink link = fromMaybe link (stripPrefix "/" link) </> "index.html"
|
||||
|
||||
permalinkRoute :: Routes
|
||||
permalinkRoute = metadataRoute $ \metadata ->
|
||||
case lookupString "permalink" metadata of
|
||||
Nothing ->
|
||||
customRoute (\identifier -> error $ "missing field 'permalink' in metadata " <> toFilePath identifier)
|
||||
Just permalink ->
|
||||
constRoute (convertPermalink permalink)
|
||||
permalinkRoute = permalinkRouteWithDefault (error "Missing field 'permalink'.")
|
||||
|
||||
permalinkRouteWithDefault :: Routes -> Routes
|
||||
permalinkRouteWithDefault def = metadataRoute $ \metadata ->
|
||||
maybe def (constRoute . convertPermalink) (lookupString "permalink" metadata)
|
||||
|
||||
-- Removes "index.html" from URLs.
|
||||
stripIndexFile :: String -> String
|
||||
|
|
|
@ -1,33 +0,0 @@
|
|||
{-# LANGUAGE RankNTypes #-}
|
||||
|
||||
module Hakyll.Web.Template.Context.Derived where
|
||||
|
||||
import Hakyll
|
||||
import Text.Printf
|
||||
|
||||
addDerivedField
|
||||
:: String
|
||||
-> (forall b. Context b -> [String] -> Item b -> Compiler ContextField)
|
||||
-> Context a
|
||||
-> Context a
|
||||
addDerivedField key derive ctx = Context $ \k a i ->
|
||||
if k == key then
|
||||
derive ctx a i
|
||||
else do
|
||||
fld <- unContext ctx k a i
|
||||
return $
|
||||
case fld of
|
||||
-- If the field is a list, recursively derive the field for any list items.
|
||||
ListField itemCtx items -> ListField (addDerivedField key derive itemCtx) items
|
||||
-- Otherwise, simply return the field.
|
||||
otherFld -> otherFld
|
||||
|
||||
|
||||
|
||||
-- Retrieve a String from the context
|
||||
getString :: String -> Context a -> [String] -> Item a -> Compiler String
|
||||
getString key ctx a i = do
|
||||
fld <- unContext ctx key a i
|
||||
case fld of
|
||||
StringField str -> return str
|
||||
_ -> fail $ printf "Key '%s' does not return a String" key
|
|
@ -1,85 +1,53 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
module Hakyll.Web.Template.Context.Metadata
|
||||
( includeContext
|
||||
, metadataContext
|
||||
, objectContext
|
||||
, restoreMetadata
|
||||
) where
|
||||
module Hakyll.Web.Template.Context.Metadata where
|
||||
|
||||
import Control.Monad ((<=<))
|
||||
import Data.Aeson (Object, Value(..))
|
||||
import qualified Data.ByteString.Char8 as BS
|
||||
import qualified Data.HashMap.Strict as H
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Vector as V
|
||||
import Hakyll
|
||||
import Text.Printf (printf)
|
||||
import qualified Data.Yaml as Y
|
||||
|
||||
-- |Create a Context based on a JSON Object.
|
||||
objectContext :: Context String -> Context Object
|
||||
objectContext ctx = Context $ \k _ i ->
|
||||
let o = itemBody i in
|
||||
case H.lookup (T.pack k) o of
|
||||
Just v -> decodeValue ctx v
|
||||
Nothing -> fail $ printf "Key '%s' undefined in context '%s'" k (show o)
|
||||
|
||||
-- |Create a |Context| from the |Metadata| associated with an |Item|.
|
||||
metadataContext
|
||||
:: Context String -- ^ |Context| used when unfolding a JSON |Array| into a |ListField|.
|
||||
-> Context String
|
||||
metadataContext ctx = Context $ \k a i -> do
|
||||
let identifier = itemIdentifier i
|
||||
metadata <- getMetadata identifier
|
||||
item <- makeItem metadata
|
||||
unContext (objectContext ctx) k a item
|
||||
isObject :: Value -> Bool
|
||||
isObject (Object _) = True
|
||||
isObject _ = False
|
||||
|
||||
-- |Create a |Context| from a JSON |Object| which loads data from files under "include" keys.
|
||||
includeContext
|
||||
:: Context String -- ^ |Context| used when unfolding a JSON |Array| into a |ListField|.
|
||||
-> Context Object
|
||||
includeContext ctx = Context $ \k a i -> do
|
||||
let o = itemBody i
|
||||
v <- lookupObject "include" o
|
||||
identifier <- fromFilePath <$> toString v
|
||||
unContext (ctx <> metadataContext ctx) k a =<< load identifier
|
||||
isString :: Value -> Bool
|
||||
isString (String _) = True
|
||||
isString _ = False
|
||||
|
||||
-- |Create a |Context| from a JSON |Object|.
|
||||
objectContext
|
||||
:: Context String -- ^ |Context| used when unfolding a JSON |Array| into a |ListField|.
|
||||
-> Context Object
|
||||
objectContext ctx = Context $ \k _ i -> do
|
||||
let o = itemBody i
|
||||
decodeValue ctx =<< lookupObject k o
|
||||
|
||||
-- |Decode a JSON Value to a context field.
|
||||
decodeValue :: Context String -> Value -> Compiler ContextField
|
||||
decodeValue ctx (Array a) = do
|
||||
objs <- mapM (makeItem <=< toObject) (V.toList a)
|
||||
return $ ListField (includeContext ctx <> objectContext ctx) objs
|
||||
decodeValue _ctx (String s) = return . StringField $ T.unpack s
|
||||
decodeValue _ctx (Number n) = return . StringField $ show n
|
||||
decodeValue _ctx (Bool b) = return . StringField $ show b
|
||||
decodeValue _ctx v = fail $ printf "Unsupported value '%s'" (show v)
|
||||
|
||||
-- |Lookup the |Value| stored in an |Object| at the given key.
|
||||
lookupObject :: MonadFail m => String -> Object -> m Value
|
||||
lookupObject k o = maybe ifNotFound ifFound (H.lookup (T.pack k) o)
|
||||
where
|
||||
ifFound = return
|
||||
ifNotFound = fail $ printf "Key '%s' undefined in context '%s'" k (show o)
|
||||
|
||||
-- |Convert a |Value| to an |Object|, or fail.
|
||||
toObject :: MonadFail m => Value -> m Object
|
||||
toObject (Object o) = return o
|
||||
toObject v = fail $ printf "Not an object '%s'" (show v)
|
||||
|
||||
-- |Convert a |Value| to an |String|, or fail.
|
||||
toString :: MonadFail m => Value -> m String
|
||||
toString (String s) = return (T.unpack s)
|
||||
toString v = fail $ printf "Not a string '%s'" (show v)
|
||||
|
||||
-- |Decode a JSON Value to a context field.
|
||||
decodeValue :: Context String -> Value -> Compiler ContextField
|
||||
decodeValue ctx (Array a)
|
||||
| V.all isObject a = do
|
||||
objs <- mapM (makeItem <=< toObject) (V.toList a)
|
||||
return $ ListField (objectContext ctx) objs
|
||||
| V.all isString a = do
|
||||
items <- mapM (load . fromFilePath <=< toString) (V.toList a)
|
||||
return $ ListField ctx items
|
||||
decodeValue _ (String s) = return . StringField $ T.unpack s
|
||||
decodeValue _ (Number n) = return . StringField $ show n
|
||||
decodeValue _ (Bool b) = return . StringField $ show b
|
||||
decodeValue _ v = fail $ printf "Unsupported value '%s'" (show v)
|
||||
|
||||
-- |Create a Context based on the Metadata.
|
||||
metadataContext :: Context String -> Context String
|
||||
metadataContext ctx = Context $ \k a i ->
|
||||
unContext (objectContext ctx) k a <=< makeItem <=< getMetadata $ itemIdentifier i
|
||||
|
||||
-- |Add the original |Metadata| block back to the file.
|
||||
restoreMetadata :: Item String -> Compiler (Item String)
|
||||
restoreMetadata item = do
|
||||
metadata <- getMetadata (itemIdentifier item)
|
||||
if H.null metadata then
|
||||
return item
|
||||
else do
|
||||
let yaml = "---\n" <> BS.unpack (Y.encode metadata) <> "---\n\n"
|
||||
withItemBody (\body -> return (yaml <> body)) item
|
||||
|
|
255
hs/Main.hs
255
hs/Main.hs
|
@ -1,26 +1,22 @@
|
|||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
import Control.Monad ((<=<), (>=>), forM_)
|
||||
import Data.Char (toLower)
|
||||
import Control.Monad ((<=<), forM_)
|
||||
import qualified Data.ByteString.Lazy as BL
|
||||
import Data.Functor ((<&>))
|
||||
import Data.List (isPrefixOf, stripPrefix)
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Text.ICU as RE
|
||||
import qualified Data.Text.ICU.Replace as T
|
||||
import Hakyll
|
||||
import Hakyll.Web.Agda
|
||||
import Hakyll.Web.Routes.Permalink
|
||||
import Hakyll.Web.Template.Numeric
|
||||
import Hakyll.Web.Template.Context.Derived
|
||||
import Hakyll.Web.Template.Context.Metadata
|
||||
import Hakyll.Web.Template.Context.Title
|
||||
import Hakyll.Web.Sass
|
||||
import System.FilePath ((</>), takeDirectory, replaceExtensions, splitPath, joinPath)
|
||||
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 Text.Printf
|
||||
import qualified Text.Pandoc.Filter as Pandoc (Filter(..), applyFilters)
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Configuration
|
||||
|
@ -69,22 +65,20 @@ siteContext = mconcat
|
|||
, "authors/jsiek.metadata"
|
||||
]
|
||||
, constField "google_analytics" "UA-125055580-1"
|
||||
, addAnchor defaultContext
|
||||
, defaultContext
|
||||
]
|
||||
|
||||
siteSectionContext :: Context String
|
||||
siteSectionContext = mconcat
|
||||
[ titlerunningField
|
||||
, subtitleField
|
||||
, addShiftedBody "raw" (contentField "raw" "raw")
|
||||
, siteContext
|
||||
]
|
||||
|
||||
tableOfContentsContext :: Context String -> Context String
|
||||
tableOfContentsContext ctx = Context $ \k a _ ->
|
||||
unContext (objectContext ctx) k a
|
||||
=<< makeItem
|
||||
=<< getMetadata "src/plfa/toc.metadata"
|
||||
tableOfContentsContext ctx = Context $ \k a _ -> do
|
||||
m <- makeItem <=< getMetadata $ "src/plfa/toc.metadata"
|
||||
unContext (objectContext ctx) k a m
|
||||
|
||||
acknowledgementsContext :: Context String
|
||||
acknowledgementsContext = mconcat
|
||||
|
@ -130,6 +124,29 @@ 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
|
||||
|
@ -147,29 +164,32 @@ main = do
|
|||
-- Build function to fix local URLs
|
||||
fixLocalLink <- mkFixLocalLink "src"
|
||||
|
||||
let maybeCompileAgda
|
||||
:: Maybe CommandLineOptions -- ^ If this argument is passed, Agda compilation is used.
|
||||
-> Item String
|
||||
-> Compiler (Item String)
|
||||
maybeCompileAgda Nothing = return
|
||||
maybeCompileAgda (Just opts) =
|
||||
compileAgdaWith opts >=>
|
||||
withItemBody (return . withUrls fixStdlibLink) >=>
|
||||
withItemBody (return . withUrls fixLocalLink)
|
||||
|
||||
-- Build compiler for Markdown pages with optional Literate Agda
|
||||
let pageCompiler
|
||||
:: Maybe CommandLineOptions -- ^ If this argument is passed, Agda compilation is used.
|
||||
-> Compiler (Item String)
|
||||
pageCompiler maybeOpts = do
|
||||
-- Build compiler for Markdown pages
|
||||
let pageCompiler :: Compiler (Item String)
|
||||
pageCompiler = do
|
||||
csl <- load cslFileName
|
||||
bib <- load bibFileName
|
||||
getResourceBody
|
||||
>>= saveSnapshot "raw"
|
||||
>>= maybeCompileAgda maybeOpts
|
||||
>>= readMarkdownWith siteReaderOptions
|
||||
>>= processCites csl bib
|
||||
<&> writeHTML5With siteWriterOptions
|
||||
>>= saveSnapshot "content"
|
||||
>>= loadAndApplyTemplate "templates/page.html" siteSectionContext
|
||||
>>= loadAndApplyTemplate "templates/default.html" siteSectionContext
|
||||
>>= prettifyUrls
|
||||
|
||||
-- Build compiler for literate Agda pages
|
||||
let pageWithAgdaCompiler :: CommandLineOptions -> Compiler (Item String)
|
||||
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
|
||||
>>= prettifyUrls
|
||||
|
@ -178,14 +198,40 @@ main = do
|
|||
--
|
||||
-- NOTE: The order of the various match expressions is important:
|
||||
-- Special-case compilation instructions for files such as
|
||||
-- "src/plfa/index.md" would be overwritten by the general
|
||||
-- purpose compilers for "src/**.md", which would
|
||||
-- "src/plfa/epub.md" and "src/plfa/index.md" would be overwritten
|
||||
-- by the general purpose compilers for "src/**.md", which would
|
||||
-- cause them to render incorrectly. It is possible to explicitly
|
||||
-- exclude such files using `complement` patterns, but this vastly
|
||||
-- complicates the match patterns.
|
||||
--
|
||||
hakyll $ do
|
||||
|
||||
-- Compile EPUB
|
||||
match "src/plfa/epub.md" $ do
|
||||
route $ constRoute "plfa.epub"
|
||||
compile $ do
|
||||
epubTemplate <- load "templates/epub.html"
|
||||
>>= compilePandocTemplate
|
||||
epubMetadata <- load "src/plfa/epub.xml"
|
||||
let ropt = epubReaderOptions
|
||||
let wopt = epubWriterOptions
|
||||
{ writerTemplate = Just . itemBody $ epubTemplate
|
||||
, writerEpubMetadata = Just . T.pack . itemBody $ epubMetadata
|
||||
}
|
||||
getResourceBody
|
||||
>>= applyAsTemplate (tableOfContentsContext epubSectionContext)
|
||||
>>= readPandocWith ropt
|
||||
>>= applyPandocFilters ropt [] "epub3"
|
||||
>>= writeEPUB3With wopt
|
||||
|
||||
match "templates/epub.html" $
|
||||
compile $ getResourceBody
|
||||
>>= applyAsTemplate siteContext
|
||||
|
||||
match "src/plfa/epub.xml" $
|
||||
compile $ getResourceBody
|
||||
>>= applyAsTemplate siteContext
|
||||
|
||||
-- Compile Table of Contents
|
||||
match "src/plfa/index.md" $ do
|
||||
route permalinkRoute
|
||||
|
@ -205,9 +251,9 @@ main = do
|
|||
route permalinkRoute
|
||||
compile $ getResourceBody
|
||||
>>= applyAsTemplate acknowledgementsContext
|
||||
>>= saveSnapshot "raw"
|
||||
>>= readMarkdownWith siteReaderOptions
|
||||
<&> writeHTML5With siteWriterOptions
|
||||
>>= saveSnapshot "content"
|
||||
>>= loadAndApplyTemplate "templates/page.html" siteContext
|
||||
>>= loadAndApplyTemplate "templates/default.html" siteContext
|
||||
>>= prettifyUrls
|
||||
|
@ -236,7 +282,7 @@ main = do
|
|||
>>= readMarkdownWith siteReaderOptions
|
||||
>>= processCites csl bib
|
||||
<&> writeHTML5With siteWriterOptions
|
||||
>>= saveSnapshot "content" -- used for teaser
|
||||
>>= saveSnapshot "content"
|
||||
>>= loadAndApplyTemplate "templates/post.html" postContext
|
||||
>>= loadAndApplyTemplate "templates/default.html" siteContext
|
||||
>>= prettifyUrls
|
||||
|
@ -244,12 +290,12 @@ main = do
|
|||
-- Compile sections using literate Agda
|
||||
match "src/**.lagda.md" $ do
|
||||
route permalinkRoute
|
||||
compile $ pageCompiler (Just agdaOptions)
|
||||
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 Nothing)
|
||||
compile pageCompiler
|
||||
|
||||
-- Compile course pages
|
||||
match "courses/**.lagda.md" $ do
|
||||
|
@ -259,11 +305,11 @@ main = do
|
|||
let courseOptions = agdaOptions
|
||||
{ optIncludePaths = courseDir : optIncludePaths agdaOptions
|
||||
}
|
||||
pageCompiler (Just courseOptions)
|
||||
pageWithAgdaCompiler courseOptions
|
||||
|
||||
match "courses/**.md" $ do
|
||||
route permalinkRoute
|
||||
compile $ pageCompiler Nothing
|
||||
compile pageCompiler
|
||||
|
||||
match "courses/**.pdf" $ do
|
||||
route idRoute
|
||||
|
@ -298,10 +344,9 @@ main = do
|
|||
create ["public/css/style.css"] $ do
|
||||
route idRoute
|
||||
compile $ do
|
||||
csses <- loadAll ("css/*.css" .||. "css/*.scss")
|
||||
csses <- loadAll ("css/*.css" .||. "css/*.scss" .&&. complement "css/epub.css")
|
||||
makeItem $ unlines $ map itemBody csses
|
||||
|
||||
|
||||
-- Copy versions
|
||||
let versions = ["19.08", "20.07"]
|
||||
forM_ versions $ \v -> do
|
||||
|
@ -318,35 +363,6 @@ main = do
|
|||
compile copyFileCompiler
|
||||
|
||||
|
||||
-- Raw versions used from Makefile for PDF and EPUB construction
|
||||
|
||||
-- Compile raw version of acknowledgements used in constructing the PDF
|
||||
match "src/plfa/backmatter/acknowledgements.md" $ version "raw" $ do
|
||||
route $ gsubRoute "src/" (const "raw/")
|
||||
compile $ getResourceBody
|
||||
>>= applyAsTemplate acknowledgementsContext
|
||||
>>= restoreMetadata
|
||||
|
||||
-- Compile raw version of index used in constructing the PDF
|
||||
match "book/pdf.tex" $ version "raw" $ do
|
||||
route $ gsubRoute "book/" (const "raw/")
|
||||
compile $ getResourceBody
|
||||
>>= applyAsTemplate (addTexPath (tableOfContentsContext siteSectionContext))
|
||||
|
||||
-- Compile raw version of index used in constructing the EPUB
|
||||
match "book/epub.md" $ version "raw" $ do
|
||||
route $ gsubRoute "book/" (const "raw/")
|
||||
compile $ getResourceBody
|
||||
>>= applyAsTemplate (tableOfContentsContext siteSectionContext)
|
||||
>>= loadAndApplyTemplate "templates/metadata.md" siteContext
|
||||
|
||||
-- Compile metadata XML used in constructing the EPUB
|
||||
match "book/epub.xml" $ version "raw" $ do
|
||||
route $ gsubRoute "book/" (const "raw/")
|
||||
compile $ getResourceBody
|
||||
>>= applyAsTemplate siteContext
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Custom readers and writers
|
||||
--------------------------------------------------------------------------------
|
||||
|
@ -374,7 +390,7 @@ processCites csl bib item = do
|
|||
withItemBody (return . CSL.processCites style refs) item
|
||||
|
||||
-- | Write a document as HTML using Pandoc, with the supplied options.
|
||||
writeHTML5With :: WriterOptions -- ^ Writer options for Pandoc
|
||||
writeHTML5With :: WriterOptions -- ^ Writer options for pandoc
|
||||
-> Item Pandoc -- ^ Document to write
|
||||
-> Item String -- ^ Resulting HTML
|
||||
writeHTML5With wopt (Item itemi doc) =
|
||||
|
@ -382,6 +398,27 @@ writeHTML5With wopt (Item itemi doc) =
|
|||
Left err -> error $ "Hakyll.Web.Pandoc.writePandocWith: " ++ show err
|
||||
Right item' -> Item itemi $ T.unpack item'
|
||||
|
||||
-- | 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 . 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
|
||||
let templateBody = T.pack $ itemBody i
|
||||
templateOrError <- unsafeCompiler $ Pandoc.compileTemplate templatePath templateBody
|
||||
template <- either fail return templateOrError
|
||||
makeItem template
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Supply snapshot as a field to the template
|
||||
|
@ -391,83 +428,9 @@ contentField :: String -> Snapshot -> Context String
|
|||
contentField key snapshot = field key $ \item ->
|
||||
itemBody <$> loadSnapshot (itemIdentifier item) snapshot
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Relativise URLs and strip "index.html" suffixes
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
prettifyUrls :: Item String -> Compiler (Item String)
|
||||
prettifyUrls = relativizeUrls <=< withItemBody (return . stripIndexFile)
|
||||
|
||||
|
||||
--------------------------------------------------------------------------------
|
||||
-- Text wrangling for EPUB and PDF
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- Convert MD_DIR/%.md to LAGDA_TEX_DIR/%.lagda.tex or TEX_DIR/%.tex
|
||||
--
|
||||
-- NOTE: This logic is partially duplicated in book/pdf.mk:TEX_PATH.
|
||||
--
|
||||
-- NOTE: This function assumes pdf.tex will be at TEX_DIR/.
|
||||
--
|
||||
addTexPath :: Context a -> Context a
|
||||
addTexPath = addDerivedField "tex_path" deriveTexPath
|
||||
where
|
||||
deriveTexPath :: Context a -> [String] -> Item a -> Compiler ContextField
|
||||
deriveTexPath ctx a i = do
|
||||
includePath <- getString "include" ctx a i
|
||||
return $ StringField (texPath includePath)
|
||||
|
||||
texPath :: FilePath -> FilePath
|
||||
texPath fnDotMd
|
||||
| fnDotMd == "README.md" = "plfa/frontmatter/README.tex"
|
||||
| any (`isPrefixOf` fnDotMd) ["src/", "book/"] = dropTopDirectory (replaceExtensions fnDotMd ".tex")
|
||||
| otherwise = error ("textPath: cannot map " <> fnDotMd)
|
||||
|
||||
dropTopDirectory :: FilePath -> FilePath
|
||||
dropTopDirectory = joinPath . tail . splitPath
|
||||
|
||||
-- Add an anchor based on the permalink, to be used as the header id.
|
||||
addAnchor :: Context a -> Context a
|
||||
addAnchor = addDerivedField "anchor" deriveAnchor
|
||||
where
|
||||
deriveAnchor :: Context a -> [String] -> Item a -> Compiler ContextField
|
||||
deriveAnchor ctx a i = do
|
||||
permalink <- getString "permalink" ctx a i
|
||||
StringField <$> anchor permalink
|
||||
|
||||
anchor :: String -> Compiler String
|
||||
anchor permalink =
|
||||
let maybeAnchor = map toLower <$> (stripSuffix "/" <=< stripPrefix "/") permalink
|
||||
in maybe (fail $ printf "Key 'permalink' malformed '%s'" permalink) return maybeAnchor
|
||||
|
||||
stripSuffix :: String -> String -> Maybe String
|
||||
stripSuffix suf str = reverse <$> stripPrefix (reverse suf) (reverse str)
|
||||
|
||||
|
||||
-- Add a variant of 'key' where all headers have been shifted by 1.
|
||||
addShiftedBody :: String -> Context a -> Context a
|
||||
addShiftedBody key = addDerivedField ("shifted_" <> key) deriveShiftedBody
|
||||
where
|
||||
deriveShiftedBody :: Context a -> [String] -> Item a -> Compiler ContextField
|
||||
deriveShiftedBody ctx a i = do
|
||||
body <- getString key ctx a i
|
||||
return $ StringField (shiftHeadersBy body)
|
||||
|
||||
-- Shift all headers by a given value.
|
||||
--
|
||||
-- NOTE: This is the /proper/ implementation of shift headers.
|
||||
-- In practice, we use the fast one, which uses regular
|
||||
-- expressions and only works on Markdown '#' headers.
|
||||
--
|
||||
-- shiftHeadersBy :: Int -> Pandoc -> Pandoc
|
||||
-- shiftHeadersBy n = walk shiftHeader
|
||||
-- where
|
||||
-- shiftHeader :: Block -> Block
|
||||
-- shiftHeader (Header level attr inlines) = Header (level + n) attr inlines
|
||||
-- shiftHeader block = block
|
||||
--
|
||||
shiftHeadersBy :: String -> String
|
||||
shiftHeadersBy body = T.unpack (T.replaceAll re "#$1" (T.pack body))
|
||||
where
|
||||
re = RE.regex [RE.Multiline] "^(#+)"
|
||||
|
|
20
nix/agda.nix
Normal file
20
nix/agda.nix
Normal file
|
@ -0,0 +1,20 @@
|
|||
{ nixpkgs, system, plfa, ... }:
|
||||
|
||||
let
|
||||
pkgs = nixpkgs.legacyPackages.${system};
|
||||
in
|
||||
pkgs.agda.withPackages (p: [
|
||||
p.standard-library
|
||||
(p.mkDerivation {
|
||||
pname = "plfa";
|
||||
meta = null;
|
||||
version = "1.0.0";
|
||||
buildInputs = [ p.standard-library ];
|
||||
preBuild = ''
|
||||
echo "module Everything where" > Everything.agda
|
||||
find src -name '*.lagda.md' | sed -e 's/src\///' -e 's/\.lagda\.md//' -e 's/\//\./g' -e 's/^/import /' | grep -Ev '^import plfa\.part1\.Equality|Naturals$' >> Everything.agda
|
||||
export LANG=C.UTF-8
|
||||
'';
|
||||
src = plfa;
|
||||
})
|
||||
])
|
36
nix/neovim.nix
Normal file
36
nix/neovim.nix
Normal file
|
@ -0,0 +1,36 @@
|
|||
{ neovim, vimPlugins, luajitPackages, nvim-agda }:
|
||||
|
||||
neovim.override {
|
||||
configure = {
|
||||
plug = {
|
||||
plugins = with vimPlugins; [
|
||||
ctrlp-vim
|
||||
nerdtree
|
||||
nvim-agda
|
||||
vim-code-dark
|
||||
vim-polyglot
|
||||
];
|
||||
};
|
||||
|
||||
customRC = ''
|
||||
lua << EOF
|
||||
package.cpath = package.cpath .. ";${luajitPackages.luautf8}/lib/lua/5.1/lua-utf8.so"
|
||||
EOF
|
||||
|
||||
set hidden
|
||||
set cursorline
|
||||
set number
|
||||
set splitright
|
||||
set modeline
|
||||
set expandtab
|
||||
set colorcolumn=80
|
||||
syntax on
|
||||
filetype on
|
||||
filetype plugin indent on
|
||||
colorscheme codedark
|
||||
|
||||
nnoremap <C-n> :NERDTreeToggle<CR>
|
||||
imap kj <Esc>
|
||||
'';
|
||||
};
|
||||
}
|
24
nix/nvim-agda/agda-vim-excerpts/LICENSE
Normal file
24
nix/nvim-agda/agda-vim-excerpts/LICENSE
Normal file
|
@ -0,0 +1,24 @@
|
|||
Copyright (c) 2013, Derek Elkins
|
||||
All rights reserved.
|
||||
|
||||
Redistribution and use in source and binary forms, with or without
|
||||
modification, are permitted provided that the following conditions are met:
|
||||
|
||||
Redistributions of source code must retain the above copyright notice, this
|
||||
list of conditions and the following disclaimer.
|
||||
|
||||
Redistributions in binary form must reproduce the above copyright
|
||||
notice, this list of conditions and the following disclaimer in the
|
||||
documentation and/or other materials provided with the distribution.
|
||||
|
||||
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
|
||||
IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
|
||||
TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
|
||||
PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
|
||||
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
|
||||
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
|
||||
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
|
||||
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
|
||||
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
|
||||
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
|
||||
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|
2
nix/nvim-agda/agda-vim-excerpts/README
Normal file
2
nix/nvim-agda/agda-vim-excerpts/README
Normal file
|
@ -0,0 +1,2 @@
|
|||
autoload.vim and ftplugin.vim are mostly taken from
|
||||
https://github.com/derekelkins/agda-vim, with slight modification.
|
668
nix/nvim-agda/agda-vim-excerpts/autoload.vim
Normal file
668
nix/nvim-agda/agda-vim-excerpts/autoload.vim
Normal file
|
@ -0,0 +1,668 @@
|
|||
" Agda Input Abbreviations
|
||||
"
|
||||
let s:cpo_save = &cpo
|
||||
set cpo&vim
|
||||
|
||||
" Public to allow referencing in custom overrides.
|
||||
if !exists('g:agda#default_glyphs')
|
||||
let g:agda#default_glyphs = {}
|
||||
|
||||
" Extra Shit
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'Gl-': 'ƛ',
|
||||
\ '==': '≡',
|
||||
\ '<': '⟨',
|
||||
\ '>': '⟩',
|
||||
\ 'em': '—',
|
||||
\ '=>': '⇒',
|
||||
\ '~-': '≃',
|
||||
\ 'r': '→',
|
||||
\ '0': '∅',
|
||||
\})
|
||||
|
||||
" Combining marks
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'over`': ' ̀',
|
||||
\ "over'": ' ́',
|
||||
\ 'over^': ' ̂',
|
||||
\ 'overv': ' ̌',
|
||||
\ 'over~': ' ̃',
|
||||
\ 'over-': ' ̄',
|
||||
\ 'over_': ' ̅',
|
||||
\ 'over–': ' ̅',
|
||||
\ 'over—': ' ̅',
|
||||
\ 'overcup': ' ̆',
|
||||
\ 'overcap': ' ̑',
|
||||
\ 'over.': ' ̇',
|
||||
\ 'over..': ' ̈',
|
||||
\ 'over"': ' ̈',
|
||||
\ 'over...': ' ⃛',
|
||||
\ 'overright.': ' ͘',
|
||||
\ 'overo': ' ̊',
|
||||
\ 'over``': ' ̏',
|
||||
\ "over''": ' ̋',
|
||||
\ 'overvec': ' ⃑',
|
||||
\ 'vec': ' ⃑',
|
||||
\ 'overlvec': ' ⃐',
|
||||
\ 'lvec': ' ⃐',
|
||||
\ 'overarc': ' ⃕',
|
||||
\ 'overlarc': ' ⃔',
|
||||
\ 'overto': ' ⃗',
|
||||
\ 'overfrom': ' ⃖',
|
||||
\ 'overfromto': ' ⃡',
|
||||
\ 'over*': ' ⃰',
|
||||
\ 'under`': ' ̖',
|
||||
\ "under'": ' ̗',
|
||||
\ 'under,': ' ̗',
|
||||
\ 'under.': ' ̣',
|
||||
\ 'under..': ' ̤',
|
||||
\ 'under"': ' ̤',
|
||||
\ 'undero': ' ̥',
|
||||
\ 'under-': ' ̱',
|
||||
\ 'under_': ' ̲',
|
||||
\ 'under–': ' ̲',
|
||||
\ 'under—': ' ̲',
|
||||
\ 'through~': ' ̴',
|
||||
\ 'through-': ' ̵',
|
||||
\ 'through_': ' ̶',
|
||||
\ 'through–': ' ̶',
|
||||
\ 'through—': ' ̶',
|
||||
\ 'through/': ' ̷',
|
||||
\ 'not': ' ̷',
|
||||
\ 'through?': ' ̸',
|
||||
\ 'Not': ' ̸',
|
||||
\ 'through\|': ' ⃒',
|
||||
\ 'throughshortmid': ' ⃓',
|
||||
\ 'througho': ' ⃘',
|
||||
\})
|
||||
|
||||
" Math
|
||||
" \ ':': '∶',
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ '{{': '⦃',
|
||||
\ '}}': '⦄',
|
||||
\ ':': '⦂',
|
||||
\ '::': '∷',
|
||||
\ ';': '﹔',
|
||||
\ '..': '‥',
|
||||
\ '=?': '≟',
|
||||
\ 'all': '∀',
|
||||
\ 'always': '□',
|
||||
\ 'approx': '≈',
|
||||
\ 'bot': '⊥',
|
||||
\ 'box': '□',
|
||||
\ 'boxdot': '⊡',
|
||||
\ 'box.': '⊡',
|
||||
\ 'boxminus': '⊟',
|
||||
\ 'box-': '⊟',
|
||||
\ 'boxplus': '⊞',
|
||||
\ 'box+': '⊞',
|
||||
\ 'boxtimes': '⊠',
|
||||
\ 'box*': '⊠',
|
||||
\ 'bul': '•',
|
||||
\ 'C': 'ℂ',
|
||||
\ 'cdot': '·',
|
||||
\ '.': '∙',
|
||||
\ 'cdots': '⋯',
|
||||
\ 'check': '✓',
|
||||
\ 'yes': '✓',
|
||||
\ 'Check': '✔',
|
||||
\ 'Yes': '✔',
|
||||
\ 'circ': '∘',
|
||||
\ 'clock': '↻',
|
||||
\ 'cclock': '↺',
|
||||
\ 'comp': '∘',
|
||||
\ 'contra': '↯',
|
||||
\ 'deg': '°',
|
||||
\ 'den': '⟦⟧<left>',
|
||||
\ 'diamond': '◇',
|
||||
\ 'dots': '…',
|
||||
\ 'down': '↓',
|
||||
\ 'downtri': '▼',
|
||||
\ 'Down': '⇓',
|
||||
\ 'dunion': '⊎',
|
||||
\ 'du': '⊎',
|
||||
\ 'ell': 'ℓ',
|
||||
\ 'empty': '∅',
|
||||
\ 'equiv': '≡',
|
||||
\ 'eq': '≡',
|
||||
\ 'eventually': '◇',
|
||||
\ 'exists': '∃',
|
||||
\ 'flat': '♭',
|
||||
\ 'fold': '⦇⦈<left>',
|
||||
\ '(\|': '⦇',
|
||||
\ '\|)': '⦈',
|
||||
\ 'forall': '∀',
|
||||
\ 'from': '←',
|
||||
\ '<-': '←',
|
||||
\ 'From': '⇐',
|
||||
\ 'fromto': '↔',
|
||||
\ 'Fromto': '⇔',
|
||||
\ 'ge': '≥',
|
||||
\ 'glub': '⊓',
|
||||
\ 'iff': '⇔',
|
||||
\ 'implies': '⇒',
|
||||
\ 'impliedby': '⇐',
|
||||
\ 'in': '∈',
|
||||
\ 'infty': '∞',
|
||||
\ 'inf': '∞',
|
||||
\ 'int': '∫',
|
||||
\ 'intersect': '∩',
|
||||
\ 'iso': '≅',
|
||||
\ 'join': '⋈',
|
||||
\ 'land': '∧',
|
||||
\ 'langle': '⟨',
|
||||
\ 'lbrac': '⟦',
|
||||
\ '[[': '⟦',
|
||||
\ 'ldots': '…',
|
||||
\ 'ldown': '⇃',
|
||||
\ 'leadsto': '⇝',
|
||||
\ '~>': '⇝',
|
||||
\ 'le': '≤',
|
||||
\ 'lift': '⌊⌋<left>',
|
||||
\ 'floor': '⌊⌋<left>',
|
||||
\ 'llangle': '⟪',
|
||||
\ 'longto': '⟶ ',
|
||||
\ '--': '⟶ ',
|
||||
\ '–': '⟶ ',
|
||||
\ 'lor': '∨',
|
||||
\ 'lower': '⌈⌉<left>',
|
||||
\ 'ceil': '⌈⌉<left>',
|
||||
\ 'lub': '⊔',
|
||||
\ 'lup': '↿',
|
||||
\ 'mapsto': '↦',
|
||||
\ 'map': '↦',
|
||||
\ 'mid': '∣',
|
||||
\ 'models': '⊨',
|
||||
\ '\|=': '⊨',
|
||||
\ 'N': 'ℕ',
|
||||
\ 'ne': '≠',
|
||||
\ 'nearrow': '↗',
|
||||
\ 'Nearrow': '⇗',
|
||||
\ 'neg': '¬',
|
||||
\ '/=': '≠',
|
||||
\ 'nequiv': '≢',
|
||||
\ 'neq': '≢',
|
||||
\ 'nexist': '∄',
|
||||
\ 'none': '∄',
|
||||
\ 'ni': '∋',
|
||||
\ 'nin': '∉',
|
||||
\ 'niso': '≇',
|
||||
\ 'notin': '∉',
|
||||
\ 'nwarrow': '↖',
|
||||
\ 'Nwarrow': '⇖',
|
||||
\ 'oast': '⊛',
|
||||
\ 'odot': '⊙',
|
||||
\ 'o.': '⊙',
|
||||
\ 'of': '∘',
|
||||
\ 'o': '∘',
|
||||
\ 'ominus': '⊖',
|
||||
\ 'o-': '⊖',
|
||||
\ 'oplus': '⊕',
|
||||
\ 'o+': '⊕',
|
||||
\ 'oslash': '⊘',
|
||||
\ 'o/': '⊘',
|
||||
\ 'otimes': '⊗',
|
||||
\ 'o*': '⊗',
|
||||
\ 'par': '∂',
|
||||
\ 'pge': '≽',
|
||||
\ 'pgt': '≻',
|
||||
\ 'ple': '≼',
|
||||
\ 'plt': '≺',
|
||||
\ 'p≥': '≽',
|
||||
\ 'p>': '≻',
|
||||
\ 'p≤': '≼',
|
||||
\ 'p<': '≺',
|
||||
\ 'pm': '±',
|
||||
\ 'prec': '≼',
|
||||
\ 'prod': '∏',
|
||||
\ 'proves': '⊢',
|
||||
\ '\|-': '⊢',
|
||||
\ 'provedby': '⊣',
|
||||
\ 'Q': 'ℚ',
|
||||
\ 'qed': '∎',
|
||||
\ 'R': 'ℝ',
|
||||
\ 'rangle': '⟩',
|
||||
\ 'rbrac': '⟧',
|
||||
\ ']]': '⟧',
|
||||
\ 'rdown': '⇂',
|
||||
\ 'righttri': '▸',
|
||||
\ 'rrangle': '⟫',
|
||||
\ 'rup': '↾',
|
||||
\ 'searrow': '↘',
|
||||
\ 'Searrow': '⇘',
|
||||
\ 'setminus': '∖',
|
||||
\ 'sharp': '♯',
|
||||
\ '#': '♯',
|
||||
\ 'sim': '∼',
|
||||
\ 'simeq': '≃',
|
||||
\ 'some': '∃',
|
||||
\ 'sqge': '⊒',
|
||||
\ 'sqgt': '⊐',
|
||||
\ 'sqle': '⊑',
|
||||
\ 'sqlt': '⊏',
|
||||
\ 's≥': '⊒',
|
||||
\ 's>': '⊐',
|
||||
\ 's≤': '⊑',
|
||||
\ 's<': '⊏',
|
||||
\ 'sqr': '²',
|
||||
\ 'sqrt': '√',
|
||||
\ 'star': '✭',
|
||||
\ 'subset': '⊂',
|
||||
\ 'sub': '⊂',
|
||||
\ 'subseteq': '⊆',
|
||||
\ 'subeq': '⊆',
|
||||
\ 'subsetneq': '⊊',
|
||||
\ 'subneq': '⊊',
|
||||
\ 'sum': '∑',
|
||||
\ 'supset': '⊃',
|
||||
\ 'sup': '⊃',
|
||||
\ 'supseteq': '⊇',
|
||||
\ 'supeq': '⊇',
|
||||
\ 'supsetneq': '⊋',
|
||||
\ 'supneq': '⊋',
|
||||
\ 'swarrow': '↙',
|
||||
\ 'Swarrow': '⇙',
|
||||
\ 'thus': '∴',
|
||||
\ 'times': '×',
|
||||
\ '*': '×',
|
||||
\ 'to': '→',
|
||||
\ '-': '→',
|
||||
\ 'To': '⇒',
|
||||
\ '=': '⇒',
|
||||
\ 'top': '⊤',
|
||||
\ 'tuple': '⟨⟩<left>',
|
||||
\ 'up': '↑',
|
||||
\ 'updown': '↕',
|
||||
\ 'ud': '↕',
|
||||
\ 'unfold': '⦉⦊<left>',
|
||||
\ '<\|': '⦉',
|
||||
\ '\|>': '⦊',
|
||||
\ 'up;down': '⇅',
|
||||
\ 'u;d': '⇅',
|
||||
\ 'uptri': '▲',
|
||||
\ 'Up': '⇑',
|
||||
\ 'union': '∪',
|
||||
\ 'vdots': '⋮',
|
||||
\ 'voltage': '⚡',
|
||||
\ 'xmark': '✗',
|
||||
\ 'no': '✗',
|
||||
\ 'Xmark': '✘',
|
||||
\ 'No': '✘',
|
||||
\ 'Z': 'ℤ',
|
||||
\})
|
||||
|
||||
" Not math
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'sec': '§',
|
||||
\})
|
||||
|
||||
" Superscripts
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ '^0': '⁰',
|
||||
\ '^1': '¹',
|
||||
\ '^2': '²',
|
||||
\ '^3': '³',
|
||||
\ '^4': '⁴',
|
||||
\ '^5': '⁵',
|
||||
\ '^6': '⁶',
|
||||
\ '^7': '⁷',
|
||||
\ '^8': '⁸',
|
||||
\ '^9': '⁹',
|
||||
\ '^A': 'ᴬ',
|
||||
\ '^B': 'ᴮ',
|
||||
\ '^D': 'ᴰ',
|
||||
\ '^E': 'ᴱ',
|
||||
\ '^G': 'ᴳ',
|
||||
\ '^H': 'ᴴ',
|
||||
\ '^I': 'ᴵ',
|
||||
\ '^J': 'ᴶ',
|
||||
\ '^K': 'ᴷ',
|
||||
\ '^L': 'ᴸ',
|
||||
\ '^M': 'ᴹ',
|
||||
\ '^N': 'ᴺ',
|
||||
\ '^O': 'ᴼ',
|
||||
\ '^P': 'ᴾ',
|
||||
\ '^R': 'ᴿ',
|
||||
\ '^T': 'ᵀ',
|
||||
\ '^U': 'ᵁ',
|
||||
\ '^V': 'ⱽ',
|
||||
\ '^W': 'ᵂ',
|
||||
\ '^a': 'ᵃ',
|
||||
\ '^b': 'ᵇ',
|
||||
\ '^c': 'ᶜ',
|
||||
\ '^d': 'ᵈ',
|
||||
\ '^e': 'ᵉ',
|
||||
\ '^f': 'ᶠ',
|
||||
\ '^g': 'ᵍ',
|
||||
\ '^h': 'ʰ',
|
||||
\ '^i': 'ⁱ',
|
||||
\ '^j': 'ʲ',
|
||||
\ '^k': 'ᵏ',
|
||||
\ '^l': 'ˡ',
|
||||
\ '^m': 'ᵐ',
|
||||
\ '^n': 'ⁿ',
|
||||
\ '^o': 'ᵒ',
|
||||
\ '^p': 'ᵖ',
|
||||
\ '^r': 'ʳ',
|
||||
\ '^s': 'ˢ',
|
||||
\ '^t': 'ᵗ',
|
||||
\ '^u': 'ᵘ',
|
||||
\ '^v': 'ᵛ',
|
||||
\ '^w': 'ʷ',
|
||||
\ '^x': 'ˣ',
|
||||
\ '^y': 'ʸ',
|
||||
\ '^z': 'ᶻ',
|
||||
\ '^+': '⁺',
|
||||
\ '^-': '⁻',
|
||||
\ '^=': '⁼',
|
||||
\ '^(': '⁽',
|
||||
\ '^)': '⁾',
|
||||
\ "'": '′',
|
||||
\ "''": '″',
|
||||
\ "'''": '‴',
|
||||
\ "''''": '⁗',
|
||||
\ '"': '″',
|
||||
\ '""': '⁗',
|
||||
\ '`': '‵',
|
||||
\ '``': '‶',
|
||||
\ '```': '‷',
|
||||
\})
|
||||
|
||||
" Subscripts
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ '_0': '₀',
|
||||
\ '_1': '₁',
|
||||
\ '_2': '₂',
|
||||
\ '_3': '₃',
|
||||
\ '_4': '₄',
|
||||
\ '_5': '₅',
|
||||
\ '_6': '₆',
|
||||
\ '_7': '₇',
|
||||
\ '_8': '₈',
|
||||
\ '_9': '₉',
|
||||
\ '_a': 'ₐ',
|
||||
\ '_e': 'ₑ',
|
||||
\ '_h': 'ₕ',
|
||||
\ '_i': 'ᵢ',
|
||||
\ '_j': 'ⱼ',
|
||||
\ '_k': 'ₖ',
|
||||
\ '_l': 'ₗ',
|
||||
\ '_m': 'ₘ',
|
||||
\ '_n': 'ₙ',
|
||||
\ '_o': 'ₒ',
|
||||
\ '_p': 'ₚ',
|
||||
\ '_r': 'ᵣ',
|
||||
\ '_s': 'ₛ',
|
||||
\ '_t': 'ₜ',
|
||||
\ '_u': 'ᵤ',
|
||||
\ '_v': 'ᵥ',
|
||||
\ '_x': 'ₓ',
|
||||
\ '_+': '₊',
|
||||
\ '_-': '₋',
|
||||
\ '_=': '₌',
|
||||
\ '_(': '₍',
|
||||
\ '_)': '₎',
|
||||
\ 'p0': 'π₀',
|
||||
\ 'p1': 'π₁',
|
||||
\ 'p2': 'π₂',
|
||||
\ 'p3': 'π₃',
|
||||
\ 'p4': 'π₄',
|
||||
\ 'p5': 'π₅',
|
||||
\ 'p6': 'π₆',
|
||||
\ 'p7': 'π₇',
|
||||
\ 'p8': 'π₈',
|
||||
\ 'p9': 'π₉',
|
||||
\ 'i0': 'ι₀',
|
||||
\ 'i1': 'ι₁',
|
||||
\ 'i2': 'ι₂',
|
||||
\ 'i3': 'ι₃',
|
||||
\ 'i4': 'ι₄',
|
||||
\ 'i5': 'ι₅',
|
||||
\ 'i6': 'ι₆',
|
||||
\ 'i7': 'ι₇',
|
||||
\ 'i8': 'ι₈',
|
||||
\ 'i9': 'ι₉',
|
||||
\})
|
||||
|
||||
" Greek (lower)
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'alpha': 'α',
|
||||
\ 'a': 'α',
|
||||
\ 'beta': 'β',
|
||||
\ 'b': 'β',
|
||||
\ 'gamma': 'γ',
|
||||
\ 'g': 'γ',
|
||||
\ 'delta': 'δ',
|
||||
\ 'd': 'δ',
|
||||
\ 'epsilon': 'ε',
|
||||
\ 'e': 'ε',
|
||||
\ 'zeta': 'ζ',
|
||||
\ 'z': 'ζ',
|
||||
\ 'eta': 'η',
|
||||
\ 'h': 'η',
|
||||
\ 'theta': 'θ',
|
||||
\ 'iota': 'ι',
|
||||
\ 'i': 'ι',
|
||||
\ 'kappa': 'κ',
|
||||
\ 'k': 'κ',
|
||||
\ 'lambda': 'λ',
|
||||
\ 'l': 'λ',
|
||||
\ 'mu': 'μ',
|
||||
\ 'm': 'μ',
|
||||
\ 'nu': 'ν',
|
||||
\ 'n': 'ν',
|
||||
\ 'xi': 'ξ',
|
||||
\ 'omicron': 'ο',
|
||||
\ 'pi': 'π',
|
||||
\ 'p': 'π',
|
||||
\ 'rho': 'ρ',
|
||||
\ 'sigma': 'σ',
|
||||
\ 's': 'σ',
|
||||
\ 'varsigma': 'ς',
|
||||
\ 'vars': 'ς',
|
||||
\ 'tau': 'τ',
|
||||
\ 't': 'τ',
|
||||
\ 'u': 'υ',
|
||||
\ 'phi': 'φ',
|
||||
\ 'f': 'φ',
|
||||
\ 'chi': 'χ',
|
||||
\ 'x': 'χ',
|
||||
\ 'psi': 'ψ',
|
||||
\ 'c': 'ψ',
|
||||
\ 'omega': 'ω',
|
||||
\ 'v': 'ω',
|
||||
\})
|
||||
|
||||
" Greek (upper)
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'Alpha': 'Α',
|
||||
\ 'Beta': 'Β',
|
||||
\ 'Gamma': 'Γ',
|
||||
\ 'G': 'Γ',
|
||||
\ 'Delta': 'Δ',
|
||||
\ 'D': 'Δ',
|
||||
\ 'Epsilon': 'Ε',
|
||||
\ 'Zeta': 'Ζ',
|
||||
\ 'Eta': 'Η',
|
||||
\ 'Theta': 'Θ',
|
||||
\ 'Iota': 'Ι',
|
||||
\ 'Kappa': 'Κ',
|
||||
\ 'Lambda': 'Λ',
|
||||
\ 'L': 'Λ',
|
||||
\ 'Mu': 'Μ',
|
||||
\ 'Nu': 'Ν',
|
||||
\ 'Xi': 'Ξ',
|
||||
\ 'Omicron': 'Ο',
|
||||
\ 'Pi': 'Π',
|
||||
\ 'P': 'Π',
|
||||
\ 'Rho': 'Ρ',
|
||||
\ 'Sigma': 'Σ',
|
||||
\ 'S': 'Σ',
|
||||
\ 'Tau': 'Τ',
|
||||
\ 'Upsilon': 'Υ',
|
||||
\ 'Phi': 'Φ',
|
||||
\ 'F': 'Φ',
|
||||
\ 'Chi': 'Χ',
|
||||
\ 'Psi': 'Ψ',
|
||||
\ 'Omega': 'Ω',
|
||||
\ 'V': 'Ω',
|
||||
\})
|
||||
|
||||
" Blackboard
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'bA': '𝔸',
|
||||
\ 'bB': '𝔹',
|
||||
\ 'bC': 'ℂ',
|
||||
\ 'bD': '𝔻',
|
||||
\ 'bE': '𝔼',
|
||||
\ 'bF': '𝔽',
|
||||
\ 'bG': '𝔾',
|
||||
\ 'bH': 'ℍ',
|
||||
\ 'bI': '𝕀',
|
||||
\ 'bJ': '𝕁',
|
||||
\ 'bK': '𝕂',
|
||||
\ 'bL': '𝕃',
|
||||
\ 'bM': '𝕄',
|
||||
\ 'bN': 'ℕ',
|
||||
\ 'bO': '𝕆',
|
||||
\ 'bP': 'ℙ',
|
||||
\ 'bQ': 'ℚ',
|
||||
\ 'bR': 'ℝ',
|
||||
\ 'bS': '𝕊',
|
||||
\ 'bT': '𝕋',
|
||||
\ 'bU': '𝕌',
|
||||
\ 'bV': '𝕍',
|
||||
\ 'bW': '𝕎',
|
||||
\ 'bX': '𝕏',
|
||||
\ 'bY': '𝕐',
|
||||
\ 'bZ': 'ℤ',
|
||||
\ 'b0': '𝟘',
|
||||
\ 'b1': '𝟙',
|
||||
\ 'b2': '𝟚',
|
||||
\ 'b3': '𝟛',
|
||||
\ 'b4': '𝟜',
|
||||
\ 'b5': '𝟝',
|
||||
\ 'b6': '𝟞',
|
||||
\ 'b7': '𝟟',
|
||||
\ 'b8': '𝟠',
|
||||
\ 'b9': '𝟡',
|
||||
\ 'bsum': '⅀',
|
||||
\})
|
||||
|
||||
" Math chars
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'McA': '𝓐',
|
||||
\ 'McB': '𝓑',
|
||||
\ 'McC': '𝓒',
|
||||
\ 'McD': '𝓓',
|
||||
\ 'McE': '𝓔',
|
||||
\ 'McF': '𝓕',
|
||||
\ 'McG': '𝓖',
|
||||
\ 'McH': '𝓗',
|
||||
\ 'McI': '𝓘',
|
||||
\ 'McJ': '𝓙',
|
||||
\ 'McK': '𝓚',
|
||||
\ 'McL': '𝓛',
|
||||
\ 'McM': '𝓜',
|
||||
\ 'McN': '𝓝',
|
||||
\ 'McO': '𝓞',
|
||||
\ 'McP': '𝓟',
|
||||
\ 'McQ': '𝓠',
|
||||
\ 'McR': '𝓡',
|
||||
\ 'McS': '𝓢',
|
||||
\ 'McT': '𝓣',
|
||||
\ 'McU': '𝓤',
|
||||
\ 'McV': '𝓥',
|
||||
\ 'McW': '𝓦',
|
||||
\ 'McX': '𝓧',
|
||||
\ 'McY': '𝓨',
|
||||
\ 'McZ': '𝓩',
|
||||
\ 'Mca': '𝒶',
|
||||
\ 'Mcb': '𝒷',
|
||||
\ 'Mcc': '𝒸',
|
||||
\ 'Mcd': '𝒹',
|
||||
\ 'Mcf': '𝒻',
|
||||
\ 'Mch': '𝒽',
|
||||
\ 'Mci': '𝒾',
|
||||
\ 'Mcj': '𝒿',
|
||||
\ 'Mck': '𝓀',
|
||||
\ 'Mcl': '𝓁',
|
||||
\ 'Mcm': '𝓂',
|
||||
\ 'Mcn': '𝓃',
|
||||
\ 'Mcp': '𝓅',
|
||||
\ 'Mcq': '𝓆',
|
||||
\ 'Mcr': '𝓇',
|
||||
\ 'Mcs': '𝓈',
|
||||
\ 'Mct': '𝓉',
|
||||
\ 'Mcu': '𝓊',
|
||||
\ 'Mcv': '𝓋',
|
||||
\ 'Mcw': '𝓌',
|
||||
\ 'Mcx': '𝓍',
|
||||
\ 'Mcy': '𝓎',
|
||||
\ 'Mcz': '𝓏',
|
||||
\ 'MfA': '𝔄',
|
||||
\ 'MfB': '𝔅',
|
||||
\ 'MfD': '𝔇',
|
||||
\ 'MfE': '𝔈',
|
||||
\ 'MfF': '𝔉',
|
||||
\ 'MfG': '𝔊',
|
||||
\ 'MfJ': '𝔍',
|
||||
\ 'MfK': '𝔎',
|
||||
\ 'MfL': '𝔏',
|
||||
\ 'MfM': '𝔐',
|
||||
\ 'MfN': '𝔑',
|
||||
\ 'MfO': '𝔒',
|
||||
\ 'MfP': '𝔓',
|
||||
\ 'MfQ': '𝔔',
|
||||
\ 'MfS': '𝔖',
|
||||
\ 'MfT': '𝔗',
|
||||
\ 'MfU': '𝔘',
|
||||
\ 'MfV': '𝔙',
|
||||
\ 'MfW': '𝔚',
|
||||
\ 'MfX': '𝔛',
|
||||
\ 'MfY': '𝔜',
|
||||
\ 'Mfa': '𝔞',
|
||||
\ 'Mfb': '𝔟',
|
||||
\ 'Mfc': '𝔠',
|
||||
\ 'Mfd': '𝔡',
|
||||
\ 'Mfe': '𝔢',
|
||||
\ 'Mff': '𝔣',
|
||||
\ 'Mfg': '𝔤',
|
||||
\ 'Mfh': '𝔥',
|
||||
\ 'Mfi': '𝔦',
|
||||
\ 'Mfj': '𝔧',
|
||||
\ 'Mfk': '𝔨',
|
||||
\ 'Mfl': '𝔩',
|
||||
\ 'Mfm': '𝔪',
|
||||
\ 'Mfn': '𝔫',
|
||||
\ 'Mfo': '𝔬',
|
||||
\ 'Mfp': '𝔭',
|
||||
\ 'Mfq': '𝔮',
|
||||
\ 'Mfr': '𝔯',
|
||||
\ 'Mfs': '𝔰',
|
||||
\ 'Mft': '𝔱',
|
||||
\ 'Mfu': '𝔲',
|
||||
\ 'Mfv': '𝔳',
|
||||
\ 'Mfw': '𝔴',
|
||||
\ 'Mfx': '𝔵',
|
||||
\ 'Mfy': '𝔶',
|
||||
\ 'Mfz': '𝔷',
|
||||
\})
|
||||
|
||||
" From Favonia
|
||||
call extend(g:agda#default_glyphs, {
|
||||
\ 'breve': '˘',
|
||||
\ 'monus': '∸',
|
||||
\ '<>': '⟨⟩<left>',
|
||||
\ 'greekq': ';',
|
||||
\})
|
||||
|
||||
lockvar g:agda#default_glyphs
|
||||
endif
|
||||
|
||||
if !exists('g:agda#glyphs')
|
||||
let g:agda#glyphs = deepcopy(g:agda#default_glyphs)
|
||||
endif
|
||||
|
||||
let &cpo = s:cpo_save
|
88
nix/nvim-agda/agda-vim-excerpts/ftplugin.vim
Normal file
88
nix/nvim-agda/agda-vim-excerpts/ftplugin.vim
Normal file
|
@ -0,0 +1,88 @@
|
|||
let s:cpo_save = &cpo
|
||||
set cpo&vim
|
||||
|
||||
let b:undo_ftplugin = ''
|
||||
|
||||
for [sequence, symbol] in items(g:agda#glyphs)
|
||||
execute printf('noremap! <buffer> <LocalLeader>%s %s', sequence, symbol)
|
||||
endfor
|
||||
|
||||
setlocal matchpairs&vim
|
||||
setlocal matchpairs+=(:)
|
||||
setlocal matchpairs+=<:>
|
||||
setlocal matchpairs+=[:]
|
||||
setlocal matchpairs+={:}
|
||||
setlocal matchpairs+=«:»
|
||||
setlocal matchpairs+=‹:›
|
||||
setlocal matchpairs+=⁅:⁆
|
||||
setlocal matchpairs+=⁽:⁾
|
||||
setlocal matchpairs+=₍:₎
|
||||
setlocal matchpairs+=⌈:⌉
|
||||
setlocal matchpairs+=⌊:⌋
|
||||
setlocal matchpairs+=〈:〉
|
||||
setlocal matchpairs+=⎛:⎞
|
||||
setlocal matchpairs+=⎝:⎠
|
||||
setlocal matchpairs+=⎡:⎤
|
||||
setlocal matchpairs+=⎣:⎦
|
||||
setlocal matchpairs+=⎧:⎫
|
||||
setlocal matchpairs+=⎨:⎬
|
||||
setlocal matchpairs+=⎩:⎭
|
||||
setlocal matchpairs+=⎴:⎵
|
||||
setlocal matchpairs+=❨:❩
|
||||
setlocal matchpairs+=❪:❫
|
||||
setlocal matchpairs+=❬:❭
|
||||
setlocal matchpairs+=❮:❯
|
||||
setlocal matchpairs+=❰:❱
|
||||
setlocal matchpairs+=❲:❳
|
||||
setlocal matchpairs+=❴:❵
|
||||
setlocal matchpairs+=⟅:⟆
|
||||
setlocal matchpairs+=⟦:⟧
|
||||
setlocal matchpairs+=⟨:⟩
|
||||
setlocal matchpairs+=⟪:⟫
|
||||
setlocal matchpairs+=⦃:⦄
|
||||
setlocal matchpairs+=⦅:⦆
|
||||
setlocal matchpairs+=⦇:⦈
|
||||
setlocal matchpairs+=⦉:⦊
|
||||
setlocal matchpairs+=⦋:⦌
|
||||
setlocal matchpairs+=⦍:⦎
|
||||
setlocal matchpairs+=⦏:⦐
|
||||
setlocal matchpairs+=⦑:⦒
|
||||
setlocal matchpairs+=⦓:⦔
|
||||
setlocal matchpairs+=⦕:⦖
|
||||
setlocal matchpairs+=⦗:⦘
|
||||
setlocal matchpairs+=⸠:⸡
|
||||
setlocal matchpairs+=⸢:⸣
|
||||
setlocal matchpairs+=⸤:⸥
|
||||
setlocal matchpairs+=⸦:⸧
|
||||
setlocal matchpairs+=⸨:⸩
|
||||
setlocal matchpairs+=〈:〉
|
||||
setlocal matchpairs+=《:》
|
||||
setlocal matchpairs+=「:」
|
||||
setlocal matchpairs+=『:』
|
||||
setlocal matchpairs+=【:】
|
||||
setlocal matchpairs+=〔:〕
|
||||
setlocal matchpairs+=〖:〗
|
||||
setlocal matchpairs+=〘:〙
|
||||
setlocal matchpairs+=〚:〛
|
||||
setlocal matchpairs+=︗:︘
|
||||
setlocal matchpairs+=︵:︶
|
||||
setlocal matchpairs+=︷:︸
|
||||
setlocal matchpairs+=︹:︺
|
||||
setlocal matchpairs+=︻:︼
|
||||
setlocal matchpairs+=︽:︾
|
||||
setlocal matchpairs+=︿:﹀
|
||||
setlocal matchpairs+=﹁:﹂
|
||||
setlocal matchpairs+=﹃:﹄
|
||||
setlocal matchpairs+=﹇:﹈
|
||||
setlocal matchpairs+=﹙:﹚
|
||||
setlocal matchpairs+=﹛:﹜
|
||||
setlocal matchpairs+=﹝:﹞
|
||||
setlocal matchpairs+=(:)
|
||||
setlocal matchpairs+=<:>
|
||||
setlocal matchpairs+=[:]
|
||||
setlocal matchpairs+={:}
|
||||
setlocal matchpairs+=⦅:⦆
|
||||
setlocal matchpairs+=「:」
|
||||
let b:undo_ftplugin .= ' | setlocal matchpairs<'
|
||||
|
||||
let &cpo = s:cpo_save
|
26
nix/nvim-agda/default.nix
Normal file
26
nix/nvim-agda/default.nix
Normal file
|
@ -0,0 +1,26 @@
|
|||
{ nixpkgs, system, ... }:
|
||||
|
||||
let
|
||||
pkgs = nixpkgs.legacyPackages.${system};
|
||||
in
|
||||
pkgs.vimUtils.buildVimPlugin rec {
|
||||
pname = "nvim-agda";
|
||||
version = "2bed0b9a1d42f20438d22a3229c59faaf2b6a8df";
|
||||
src = pkgs.fetchFromGitHub {
|
||||
owner = "ashinkarov";
|
||||
repo = pname;
|
||||
rev = version;
|
||||
hash = "sha256-cMEOSGMyFHp/iABjpbxb3GFi4lBFYOhIDcI/EwgVgdw=";
|
||||
};
|
||||
buildPhase = ''
|
||||
for patch in ${./patches}/*; do
|
||||
echo Applying $patch...
|
||||
patch -p1 --verbose < $patch
|
||||
done
|
||||
|
||||
mkdir autoload
|
||||
cp ${agda-vim-excerpts/autoload.vim} autoload/agda.vim
|
||||
cat ${agda-vim-excerpts/ftplugin.vim} >> ftplugin/agda.vim
|
||||
cat ${./keybinds.vim} >> ftplugin/agda.vim
|
||||
'';
|
||||
}
|
11
nix/nvim-agda/keybinds.vim
Normal file
11
nix/nvim-agda/keybinds.vim
Normal file
|
@ -0,0 +1,11 @@
|
|||
nnoremap <buffer> <LocalLeader>r :<c-u>AgdaLoad<cr>
|
||||
nnoremap <buffer> <LocalLeader>t :<c-u>AgdaInfer<cr>
|
||||
nnoremap <buffer> <LocalLeader>q :<c-u>AgdaCloseMsg<cr>
|
||||
nnoremap <buffer> <LocalLeader>x :<c-u>AgdaCompute<cr>
|
||||
nnoremap <buffer> <LocalLeader>a :<c-u>AgdaRefine<cr>
|
||||
nnoremap <buffer> <LocalLeader>A :<c-u>AgdaAuto<cr>
|
||||
nnoremap <buffer> <LocalLeader>c :<c-u>AgdaMakeCase<cr>
|
||||
nmap <buffer> K :<c-u>AgdaTypeContext<cr>
|
||||
nnoremap <buffer> [g :<c-u>GoalPrev<cr>
|
||||
nnoremap <buffer> ]g :<c-u>GoalNext<cr>
|
||||
nnoremap <buffer> gd :<c-u>AgdaWhyInscope<cr>
|
31
nix/nvim-agda/patches/0001-remove-default-keybinds.patch
Normal file
31
nix/nvim-agda/patches/0001-remove-default-keybinds.patch
Normal file
|
@ -0,0 +1,31 @@
|
|||
diff --git a/ftplugin/agda.vim b/ftplugin/agda.vim
|
||||
index f3264b5..2585b54 100644
|
||||
--- a/ftplugin/agda.vim
|
||||
+++ b/ftplugin/agda.vim
|
||||
@@ -39,26 +39,3 @@ command! GoalPrev :call AgdaMod.agda_goal_prev(expand("%:p"))
|
||||
command! AgdaCloseMsg :call AgdaMod.close_msg_win()
|
||||
command! GoalContent :call AgdaMod.gc()
|
||||
command! GetEvbuf :call AgdaMod.getevbuf()
|
||||
-
|
||||
-
|
||||
-" Key mappings
|
||||
-nm <buffer> <LocalLeader>l :<c-u>AgdaLoad<cr>
|
||||
-nm <buffer> <LocalLeader>q :<c-u>AgdaCloseMsg<cr>
|
||||
-nm <buffer> <LocalLeader>, :<c-u>AgdaTypeContext<cr>
|
||||
-nm <buffer> <LocalLeader>u, :<c-u>AgdaTypeContextNorm<cr>
|
||||
-nm <buffer> <LocalLeader>d :<c-u>AgdaInfer<cr>
|
||||
-nm <buffer> <LocalLeader>r :<c-u>AgdaRefine<cr>
|
||||
-nm <buffer> <LocalLeader>c :<c-u>AgdaMakeCase<cr>
|
||||
-nm <buffer> <LocalLeader>n :<c-u>AgdaCompute<cr>
|
||||
-nm <buffer> <LocalLeader>a :<c-u>AgdaAuto<cr>
|
||||
-nm <buffer> <LocalLeader>h :<c-u>AgdaHelperFun<cr>
|
||||
-nm <buffer> <LocalLeader>o :<c-u>AgdaModuleContents<cr>
|
||||
-nm <buffer> <LocalLeader>w :<c-u>AgdaWhyInscope<cr>
|
||||
-nm <buffer> <LocalLeader>e :<c-u>MkPrompt<cr>
|
||||
-nm <buffer> <LocalLeader>? :<c-u>PrintGoals<cr>
|
||||
-nm <buffer> <LocalLeader>f :<c-u>GoalNext<cr>
|
||||
-nm <buffer> <LocalLeader>b :<c-u>GoalPrev<cr>
|
||||
-
|
||||
-
|
||||
-" mappings
|
||||
-runtime agda-input.vim
|
41
plfa.cabal
41
plfa.cabal
|
@ -12,33 +12,30 @@ build-type: Simple
|
|||
common shared-properties
|
||||
ghc-options: -Wall
|
||||
default-language: Haskell2010
|
||||
build-depends: aeson >=1.4 && <1.6
|
||||
, base >=4.6 && <5
|
||||
, bytestring >=0.10 && <0.11
|
||||
, containers >=0.6 && <0.7
|
||||
, directory >=1.2 && <1.4
|
||||
, doctemplates >=0.8 && <1.0
|
||||
, extra >=1.7 && <1.8
|
||||
, filemanip >=0.3 && <0.4
|
||||
, filepath >=1.3 && <1.5
|
||||
, frontmatter >=0.1 && <0.2
|
||||
, hakyll >=4.10 && <4.15
|
||||
, pandoc >=2.1 && <2.11
|
||||
, pandoc-types >=1.20 && <1.23
|
||||
, pandoc-citeproc >=0.17 && <0.18
|
||||
, text >=1.2 && <1.3
|
||||
, text-icu >=0.7.1 && <0.8
|
||||
, text-regex-replace >=0.1 && <0.2
|
||||
, unordered-containers >=0.2 && <0.3
|
||||
, vector >=0.12 && <0.13
|
||||
, yaml >=0.11 && <0.12
|
||||
build-depends: aeson >=1.4 && <1.5
|
||||
, base >=4.6 && <5
|
||||
, bytestring >=0.10 && <0.11
|
||||
, containers >=0.6 && <0.7
|
||||
, directory >=1.2 && <1.4
|
||||
, doctemplates >=0.8 && <0.9
|
||||
, extra >=1.7 && <1.8
|
||||
, filemanip >=0.3 && <0.4
|
||||
, filepath >=1.3 && <1.5
|
||||
, frontmatter >=0.1 && <0.2
|
||||
, hakyll >=4.10 && <4.15
|
||||
, pandoc >=2.1 && <2.11
|
||||
, pandoc-types >=1.20 && <1.21
|
||||
, pandoc-citeproc >=0.17 && <0.18
|
||||
, text >=1.2 && <1.3
|
||||
, unordered-containers >=0.2 && <0.3
|
||||
, vector >=0.12 && <0.13
|
||||
, yaml >=0.11 && <0.12
|
||||
|
||||
library
|
||||
import: shared-properties
|
||||
hs-source-dirs: hs
|
||||
exposed-modules: Hakyll.Web.Agda
|
||||
, Hakyll.Web.Template.Numeric
|
||||
, Hakyll.Web.Template.Context.Derived
|
||||
, Hakyll.Web.Template.Context.Metadata
|
||||
, Hakyll.Web.Template.Context.Title
|
||||
, Hakyll.Web.Sass
|
||||
|
@ -46,6 +43,8 @@ library
|
|||
build-depends: Agda ==2.6.1.3
|
||||
, hsass >=0.8 && <0.9
|
||||
, regex-tdfa >=1.3 && <1.4
|
||||
, text-icu >=0.7.1 && <0.8
|
||||
, text-regex-replace >=0.1 && <0.2
|
||||
|
||||
executable site
|
||||
import: shared-properties
|
||||
|
|
|
@ -4,6 +4,6 @@ title: "PLFA as EPUB"
|
|||
|
||||
It has been just over a year and a half since this feature was first requested in [#112][issue112]… Thanks to hard work by [Michael Reed][mreed20], and a little elbow grease on our part, it is finally here! [An EPUB version of PLFA!][EPUB]
|
||||
|
||||
[EPUB]: https://plfa.github.io/epub/plfa.epub
|
||||
[EPUB]: https://plfa.github.io/out/epub/plfa.epub
|
||||
[issue112]: https://github.com/plfa/plfa.github.io/issues/112
|
||||
[mreed20]: https://github.com/mreed20
|
||||
|
|
|
@ -1,31 +0,0 @@
|
|||
---
|
||||
title: "PLFA as PDF and EPUB"
|
||||
---
|
||||
|
||||
We’re pleased to announce that PLFA is now available as both [a PDF][PDF] and [an EPUB][EPUB]! Thanks to hard work by [Yuanting Mao][Altariarite], who did an internship with Phil at the University of Edinburgh, and a little elbow grease on our part, we're finally compiling to PDF!
|
||||
|
||||
In a double whammy, we’ve recently fixed compilation to EPUB as well! Compilation to EPUB never quite survived the move to Hakyll, and the EPUB available on the website was broken for quite a while. Fortunately, we’ve fixed the EPUB compilation, based on [Yuanting Mao][Altariarite] work on PDF compilation and [Michael Reed][mreed20]’s original work on EPUB compilation.
|
||||
|
||||
There’s still several kinks to even out in the process:
|
||||
|
||||
- ([#577][issue577]) EPUB generation breaks internal links;
|
||||
- ([#578][issue578]) EPUB fragment identifier is not defined;
|
||||
- ([#579][issue579]) EPUB font cannot be found;
|
||||
- ([#580][issue580]) EPUB attribute "name" not allowed;
|
||||
- ([#581][issue581]) PDF code overflows margins;
|
||||
|
||||
And probably tons of other little bugs I've missed!
|
||||
|
||||
As always, bug reports and pull requests are very, very welcome!
|
||||
|
||||
[Altariarite]: https://github.com/Altariarite
|
||||
[mreed20]: https://github.com/mreed20
|
||||
|
||||
[PDF]: https://plfa.github.io/plfa.pdf
|
||||
[EPUB]: https://plfa.github.io/plfa.epub
|
||||
|
||||
[issue577]: https://github.com/plfa/plfa.github.io/issues/577
|
||||
[issue578]: https://github.com/plfa/plfa.github.io/issues/578
|
||||
[issue579]: https://github.com/plfa/plfa.github.io/issues/579
|
||||
[issue580]: https://github.com/plfa/plfa.github.io/issues/580
|
||||
[issue581]: https://github.com/plfa/plfa.github.io/issues/581
|
Binary file not shown.
1
questions.txt
Normal file
1
questions.txt
Normal file
|
@ -0,0 +1 @@
|
|||
_<_ why is one constructor allowed to only have one
|
34
src/Extra2.agda
Normal file
34
src/Extra2.agda
Normal file
|
@ -0,0 +1,34 @@
|
|||
module _ where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
|
||||
record ⊤ : Set where
|
||||
constructor tt
|
||||
|
||||
postulate
|
||||
tt′ : ⊤
|
||||
|
||||
lemma₀ : tt ≡ tt′
|
||||
lemma₀ = refl
|
||||
|
||||
open import Data.Nat
|
||||
open import Data.Nat.Properties
|
||||
|
||||
record Terminating (n : ℕ) : Set where
|
||||
inductive
|
||||
constructor box
|
||||
field
|
||||
call : ∀ {m : ℕ} → m <′ n → Terminating m
|
||||
open Terminating
|
||||
|
||||
term : ∀ (n : ℕ) → Terminating n
|
||||
term 0 .call ()
|
||||
term (suc n) .call ≤′-refl = term n
|
||||
term (suc n) .call (≤′-step sm≤n) = term n .call sm≤n
|
||||
|
||||
postulate
|
||||
_/2 : ℕ → ℕ
|
||||
/2-<′ : ∀ (n : ℕ) → n /2 <′ n
|
||||
|
||||
merge : (n : ℕ) → Terminating n → ℕ
|
||||
merge n (box caller) = merge (n /2) (caller (/2-<′ n))
|
87
src/Extra3.agda
Normal file
87
src/Extra3.agda
Normal file
|
@ -0,0 +1,87 @@
|
|||
module _ where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
open ≡-Reasoning
|
||||
open import Function
|
||||
open import Data.Nat
|
||||
open import Data.Fin hiding (_+_)
|
||||
open import Data.Product hiding (map)
|
||||
|
||||
-- Functions as Lists
|
||||
|
||||
Vec : Set → ℕ → Set
|
||||
Vec A n = Fin n → A
|
||||
|
||||
map-Vec : {A B : Set} {n : ℕ} → (A → B) → Vec A n → Vec B n
|
||||
map-Vec f v = f ∘′ v
|
||||
|
||||
map-Vec-compose : {A B C : Set} {n : ℕ} (f : B → C) (g : A → B) (v : Vec A n)
|
||||
→ map-Vec (f ∘ g) v ≡ map-Vec f (map-Vec g v)
|
||||
map-Vec-compose f g v = refl
|
||||
|
||||
List : Set → Set
|
||||
List A = Σ ℕ (λ n → Vec A n)
|
||||
|
||||
map : {A B : Set} → (A → B) → List A → List B
|
||||
map f (n , v) = n , (f ∘′ v)
|
||||
|
||||
map-compose : {A B C : Set} (f : B → C) (g : A → B) (l : List A)
|
||||
→ map (f ∘ g) l ≡ map f (map g l)
|
||||
map-compose f g l = refl
|
||||
|
||||
[] : {A : Set} → List A
|
||||
[] = 0 , λ ()
|
||||
|
||||
_∷_ : {A : Set} → A → List A → List A
|
||||
a ∷ (n , v) = (suc n) , λ{ zero → a ; (suc n) → v n }
|
||||
|
||||
--- Questions
|
||||
|
||||
-- Q1: Instance arguments...
|
||||
-- A1: Don't abuse it
|
||||
|
||||
-- Q2: Convervativity of the eta rule of sigma types
|
||||
-- A2: this is a very interesting question!!!
|
||||
--
|
||||
-- ETT is conservative with respect to (ITT + K) + function ext, by Martin Hofmann
|
||||
|
||||
-- Q3: Differences between judgmental eq, propositional eq, and isomorphisms
|
||||
|
||||
-- A3: Judgmental equality is given
|
||||
|
||||
_ = 1 + 1 ≡ 2
|
||||
_ = refl
|
||||
|
||||
-- Propositional equality is a type that can be either
|
||||
|
||||
-- 1. the inductive types generated by reflexivity, or
|
||||
-- 2. ...
|
||||
-- 3. ...
|
||||
|
||||
-- Isomorphisms only make sense between two types.
|
||||
|
||||
-- Q4: syntax
|
||||
|
||||
postulate
|
||||
F : (Set → Set) → (Set → Set)
|
||||
|
||||
syntax F (λ x → e) (λ y → f) = e - x - y - f
|
||||
|
||||
-- Q5. subtying in kinds
|
||||
|
||||
-- Speed coding
|
||||
|
||||
+-comm : ∀ n m → n + m ≡ m + n
|
||||
+-comm 0 m = ?
|
||||
+-comm (suc n) m =
|
||||
begin
|
||||
suc n + m
|
||||
≡⟨ ? ⟩
|
||||
suc n + m
|
||||
≡⟨ ? ⟩
|
||||
suc n + m
|
||||
≡⟨ ? ⟩
|
||||
suc n + m
|
||||
≡⟨ ? ⟩
|
||||
m + suc n
|
||||
∎
|
221
src/Homework1.agda
Normal file
221
src/Homework1.agda
Normal file
|
@ -0,0 +1,221 @@
|
|||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; module ≡-Reasoning)
|
||||
open ≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
|
||||
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _^_)
|
||||
open import Data.Nat.Properties using (+-identityʳ; +-assoc; +-suc; +-comm)
|
||||
|
||||
module Homework1 where
|
||||
|
||||
-- zero property
|
||||
0-prop : ∀ (n : ℕ) → n * 0 ≡ 0
|
||||
0-prop zero = refl
|
||||
0-prop (suc n) = 0-prop n
|
||||
|
||||
-- multiplicative identity
|
||||
*-identity : ∀ (n : ℕ) → n * 1 ≡ n
|
||||
*-identity zero = refl
|
||||
*-identity (suc n) =
|
||||
begin
|
||||
suc n * 1
|
||||
≡⟨⟩
|
||||
1 + n * 1
|
||||
≡⟨ cong (1 +_) (*-identity n) ⟩
|
||||
1 + n
|
||||
∎
|
||||
|
||||
|
||||
-- multiplicative commutativity
|
||||
-- using induction on both variables
|
||||
*-comm : ∀ (a b : ℕ) → a * b ≡ b * a
|
||||
*-comm zero zero = refl
|
||||
*-comm a zero = 0-prop a
|
||||
*-comm zero b = sym (0-prop b)
|
||||
*-comm (suc a) (suc b) =
|
||||
begin
|
||||
suc a * suc b
|
||||
≡⟨⟩
|
||||
suc b + a * suc b
|
||||
≡⟨ cong (suc b +_) (*-comm a (suc b)) ⟩
|
||||
suc b + suc b * a
|
||||
≡⟨⟩
|
||||
suc b + (a + b * a)
|
||||
≡⟨ sym (+-assoc (suc b) a (b * a)) ⟩
|
||||
suc b + a + b * a
|
||||
≡⟨ cong (_+ (b * a)) (+-comm (suc b) a) ⟩
|
||||
a + suc b + b * a
|
||||
≡⟨ cong (_+ (b * a)) (+-suc a b) ⟩
|
||||
suc (a + b) + b * a
|
||||
≡⟨ cong (_+ (b * a)) (cong suc (+-comm a b)) ⟩
|
||||
suc (b + a) + b * a
|
||||
≡⟨ cong (_+ (b * a)) (sym (+-suc b a)) ⟩
|
||||
b + suc a + b * a
|
||||
≡⟨ cong (_+ (b * a)) (+-comm b (suc a)) ⟩
|
||||
suc a + b + b * a
|
||||
≡⟨ cong (suc a + b +_) (*-comm b a) ⟩
|
||||
suc a + b + a * b
|
||||
≡⟨ +-assoc (suc a) b (a * b) ⟩
|
||||
suc a + (b + a * b)
|
||||
≡⟨⟩
|
||||
suc a + suc a * b
|
||||
≡⟨ cong (suc a +_) (*-comm (suc a) b) ⟩
|
||||
suc a + b * suc a
|
||||
≡⟨⟩
|
||||
suc b * suc a
|
||||
∎
|
||||
|
||||
-- multiplication distributive property
|
||||
*-distrib-+ : ∀ (a b c : ℕ) → a * (b + c) ≡ (a * b) + (a * c)
|
||||
*-distrib-+ a zero c =
|
||||
begin
|
||||
a * (zero + c)
|
||||
≡⟨⟩
|
||||
a * c
|
||||
≡⟨⟩
|
||||
zero + (a * c)
|
||||
≡⟨ cong (_+ (a * c)) (sym (0-prop a)) ⟩
|
||||
(a * zero) + (a * c)
|
||||
∎
|
||||
*-distrib-+ a (suc b) c =
|
||||
begin
|
||||
a * (suc b + c)
|
||||
≡⟨⟩
|
||||
a * suc (b + c)
|
||||
≡⟨ *-comm a (suc (b + c)) ⟩
|
||||
suc (b + c) * a
|
||||
≡⟨⟩
|
||||
a + (b + c) * a
|
||||
≡⟨ cong (a +_) (*-comm (b + c) a) ⟩
|
||||
a + a * (b + c)
|
||||
≡⟨ cong (a +_) (*-distrib-+ a b c) ⟩
|
||||
a + ((a * b) + (a * c))
|
||||
≡⟨ cong (a +_) (cong (_+ (a * c)) (*-comm a b)) ⟩
|
||||
a + ((b * a) + (a * c))
|
||||
≡⟨ sym (+-assoc a (b * a) (a * c)) ⟩
|
||||
a + (b * a) + (a * c)
|
||||
≡⟨⟩
|
||||
(suc b * a) + (a * c)
|
||||
≡⟨ cong (_+ (a * c)) (*-comm (suc b) a) ⟩
|
||||
(a * suc b) + (a * c)
|
||||
∎
|
||||
|
||||
|
||||
-- multiplicative associativity
|
||||
*-assoc : ∀ (a b c : ℕ) → (a * b) * c ≡ a * (b * c)
|
||||
*-assoc zero b c = refl
|
||||
*-assoc (suc a) b c =
|
||||
begin
|
||||
(suc a * b) * c
|
||||
≡⟨⟩
|
||||
(b + a * b) * c
|
||||
≡⟨ *-comm (b + a * b) c ⟩
|
||||
c * (b + a * b)
|
||||
≡⟨ *-distrib-+ c b (a * b) ⟩
|
||||
(c * b) + (c * (a * b))
|
||||
≡⟨ cong ((c * b) +_) (sym (*-assoc c a b)) ⟩
|
||||
(c * b) + (c * a * b)
|
||||
≡⟨ cong (_+ (c * a * b)) (*-comm c b) ⟩
|
||||
(b * c) + (c * a * b)
|
||||
≡⟨ cong ((b * c) +_) (cong (_* b) (*-comm c a)) ⟩
|
||||
(b * c) + (a * c * b)
|
||||
≡⟨ cong ((b * c) +_) (*-assoc a c b) ⟩
|
||||
(b * c) + (a * (c * b))
|
||||
≡⟨ cong ((b * c) +_) (cong (a *_) (*-comm c b)) ⟩
|
||||
(b * c) + (a * (b * c))
|
||||
∎
|
||||
|
||||
|
||||
-- 1-identity
|
||||
1-identity : ∀ (n : ℕ) → 1 * n ≡ n
|
||||
1-identity n =
|
||||
begin
|
||||
1 * n
|
||||
≡⟨⟩
|
||||
n + 0 * n
|
||||
≡⟨⟩
|
||||
n + 0
|
||||
≡⟨ +-comm n 0 ⟩
|
||||
0 + n
|
||||
≡⟨⟩
|
||||
n
|
||||
∎
|
||||
|
||||
-- exponentiation distributive property
|
||||
^-distribˡ-|-* : ∀ (m n p : ℕ) → m ^ (n + p) ≡ (m ^ n) * (m ^ p)
|
||||
^-distribˡ-|-* m zero p =
|
||||
begin
|
||||
m ^ (zero + p)
|
||||
≡⟨⟩
|
||||
m ^ p
|
||||
≡⟨ sym (1-identity (m ^ p)) ⟩
|
||||
1 * (m ^ p)
|
||||
≡⟨⟩
|
||||
(m ^ zero) * (m ^ p)
|
||||
∎
|
||||
^-distribˡ-|-* m (suc n) p =
|
||||
begin
|
||||
m ^ (suc n + p)
|
||||
≡⟨⟩
|
||||
m ^ (suc (n + p))
|
||||
≡⟨⟩
|
||||
m * (m ^ (n + p))
|
||||
≡⟨ cong (m *_) (^-distribˡ-|-* m n p) ⟩
|
||||
m * ((m ^ n) * (m ^ p))
|
||||
≡⟨ sym (*-assoc m (m ^ n) (m ^ p)) ⟩
|
||||
(m * (m ^ n)) * (m ^ p)
|
||||
≡⟨⟩
|
||||
(m ^ suc n) * (m ^ p)
|
||||
∎
|
||||
|
||||
-- exponential distribution from the right
|
||||
^-distribʳ-* : ∀ (m n p : ℕ) → (m * n) ^ p ≡ (m ^ p) * (n ^ p)
|
||||
^-distribʳ-* m n zero = refl
|
||||
^-distribʳ-* m n (suc p) =
|
||||
begin
|
||||
(m * n) ^ (suc p)
|
||||
≡⟨⟩
|
||||
(m * n) * (m * n) ^ p
|
||||
≡⟨ cong (m * n *_) (^-distribʳ-* m n p) ⟩
|
||||
(m * n) * ((m ^ p) * (n ^ p))
|
||||
≡⟨ sym (*-assoc (m * n) (m ^ p) (n ^ p)) ⟩
|
||||
(m * n) * (m ^ p) * (n ^ p)
|
||||
≡⟨ cong (_* (n ^ p)) (*-assoc m n (m ^ p)) ⟩
|
||||
(m * (n * (m ^ p))) * (n ^ p)
|
||||
≡⟨ cong (_* (n ^ p)) (cong (m *_) (*-comm n (m ^ p))) ⟩
|
||||
(m * ((m ^ p) * n)) * (n ^ p)
|
||||
≡⟨ cong (_* (n ^ p)) (sym (*-assoc m (m ^ p) n)) ⟩
|
||||
m * (m ^ p) * n * (n ^ p)
|
||||
≡⟨⟩
|
||||
(m ^ suc p) * n * (n ^ p)
|
||||
≡⟨ *-assoc (m ^ suc p) n (n ^ p) ⟩
|
||||
(m ^ suc p) * (n * (n ^ p))
|
||||
≡⟨⟩
|
||||
(m ^ suc p) * (n ^ suc p)
|
||||
∎
|
||||
|
||||
-- exponential association
|
||||
^-*-assoc : ∀ (m n p : ℕ) → (m ^ n) ^ p ≡ m ^ (n * p)
|
||||
^-*-assoc m n zero =
|
||||
begin
|
||||
(m ^ n) ^ zero
|
||||
≡⟨⟩
|
||||
1
|
||||
≡⟨⟩
|
||||
m ^ zero
|
||||
≡⟨ cong (m ^_) (sym (0-prop n)) ⟩
|
||||
m ^ (n * zero)
|
||||
∎
|
||||
^-*-assoc m n (suc p) =
|
||||
begin
|
||||
(m ^ n) ^ (suc p)
|
||||
≡⟨⟩
|
||||
(m ^ n) * (m ^ n) ^ p
|
||||
≡⟨ cong (m ^ n *_) (^-*-assoc m n p) ⟩
|
||||
(m ^ n) * m ^ (n * p)
|
||||
≡⟨ sym (^-distribˡ-|-* m n (n * p)) ⟩
|
||||
m ^ (n + n * p)
|
||||
≡⟨ cong (m ^_) (cong (n +_) (*-comm n p)) ⟩
|
||||
m ^ (n + p * n)
|
||||
≡⟨⟩
|
||||
m ^ (suc p * n)
|
||||
≡⟨ cong (m ^_) (*-comm (suc p) n) ⟩
|
||||
m ^ (n * suc p)
|
||||
∎
|
77
src/Homework2.agda
Normal file
77
src/Homework2.agda
Normal file
|
@ -0,0 +1,77 @@
|
|||
open import Relation.Binary.PropositionalEquality
|
||||
open ≡-Reasoning
|
||||
open import Data.Nat
|
||||
open import Data.Nat.Properties
|
||||
|
||||
module Homework2 where
|
||||
|
||||
data Bin : Set where
|
||||
O : Bin
|
||||
_I : Bin → Bin
|
||||
_II : Bin → Bin
|
||||
|
||||
-------------------------------------------------------
|
||||
-- from
|
||||
-------------------------------------------------------
|
||||
|
||||
from : Bin → ℕ
|
||||
from O = 0
|
||||
from (b I) = 1 + (from b) * 2
|
||||
from (b II) = 2 + (from b) * 2
|
||||
|
||||
-------------------------------------------------------
|
||||
-- to
|
||||
-------------------------------------------------------
|
||||
|
||||
inc : Bin → Bin
|
||||
inc O = O I
|
||||
inc (b I) = b II
|
||||
inc (b II) = (inc b) I
|
||||
|
||||
to : ℕ → Bin
|
||||
to 0 = O
|
||||
to (suc n) = inc (to n)
|
||||
|
||||
-------------------------------------------------------
|
||||
-- from∘to
|
||||
-------------------------------------------------------
|
||||
|
||||
from-inc : ∀ (b : Bin) → from (inc b) ≡ suc (from b)
|
||||
from-inc O = refl
|
||||
from-inc (n I) = refl
|
||||
from-inc (n II) = cong suc (cong (_* 2) (from-inc n))
|
||||
|
||||
from∘to : ∀ n → from (to n) ≡ n
|
||||
from∘to zero = refl
|
||||
from∘to (suc n) = trans (from-inc (to n)) (cong suc (from∘to n))
|
||||
|
||||
-------------------------------------------------------
|
||||
-- to∘from
|
||||
-------------------------------------------------------
|
||||
|
||||
toI : ∀ (n : ℕ) → to (1 + n * 2) ≡ (to n) I
|
||||
toI zero = refl
|
||||
toI (suc n) = cong inc (cong inc (toI n))
|
||||
|
||||
to∘from : ∀ b → to (from b) ≡ b
|
||||
to∘from O = refl
|
||||
to∘from (n I) =
|
||||
begin
|
||||
to (1 + (from n) * 2)
|
||||
≡⟨ toI (from n) ⟩
|
||||
(to (from n)) I
|
||||
≡⟨ cong _I (to∘from n) ⟩
|
||||
n I
|
||||
∎
|
||||
to∘from (n II) =
|
||||
begin
|
||||
to (from (n II))
|
||||
≡⟨⟩
|
||||
to (2 + (from n) * 2)
|
||||
≡⟨⟩
|
||||
inc (to (1 + (from n) * 2))
|
||||
≡⟨ cong inc (toI (from n)) ⟩
|
||||
inc ((to (from n)) I)
|
||||
≡⟨ cong inc (cong _I (to∘from n)) ⟩
|
||||
n II
|
||||
∎
|
77
src/Homework3.agda
Normal file
77
src/Homework3.agda
Normal file
|
@ -0,0 +1,77 @@
|
|||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Nullary.Decidable using (True; toWitness)
|
||||
open import Homework3Prelude
|
||||
|
||||
module Homework3 where
|
||||
|
||||
---------------------------------------------------------
|
||||
-- task 1
|
||||
---------------------------------------------------------
|
||||
|
||||
V¬—→ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ ⊢ A}
|
||||
→ Value M
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
|
||||
|
||||
---------------------------------------------------------
|
||||
-- task 2
|
||||
---------------------------------------------------------
|
||||
|
||||
mul : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
mul = μ -- *
|
||||
ƛ -- m
|
||||
ƛ -- n
|
||||
(case (# 1) -- match on m
|
||||
-- case `zero → return 0
|
||||
(`zero)
|
||||
|
||||
-- case `suc m₁ → return n + (m₁ * n)
|
||||
(plus · # 1 · (# 3 · # 0 · # 1))
|
||||
)
|
||||
|
||||
task2 : mul {∅} · one · one —↠ one
|
||||
task2 =
|
||||
begin
|
||||
mul · one · one
|
||||
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
|
||||
(ƛ ƛ (case (# 1) `zero (plus · # 1 · (mul · # 0 · # 1)))) · one · one
|
||||
—→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
|
||||
(ƛ (case one `zero (plus · # 1 · (mul · # 0 · # 1)))) · one
|
||||
—→⟨ β-ƛ (V-suc V-zero) ⟩
|
||||
case one `zero (plus · one · (mul · # 0 · one))
|
||||
—→⟨ β-suc V-zero ⟩
|
||||
plus · one · (mul · `zero · one)
|
||||
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
|
||||
(ƛ ƛ (case (# 1) (# 0) (`suc (plus · # 0 · # 1)))) · one · (mul · `zero · one)
|
||||
—→⟨ ξ-·₁ (β-ƛ (V-suc V-zero)) ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) · (mul · `zero · one)
|
||||
—→⟨ ξ-·₂ V-ƛ (ξ-·₁ (ξ-·₁ β-μ)) ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
|
||||
((ƛ ƛ (case (# 1) `zero (plus · # 1 · (mul · # 0 · # 1)))) · `zero · one)
|
||||
—→⟨ ξ-·₂ V-ƛ (ξ-·₁ (β-ƛ V-zero)) ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
|
||||
((ƛ (case `zero `zero (plus · # 1 · (mul · # 0 · # 1)))) · one)
|
||||
—→⟨ ξ-·₂ V-ƛ (β-ƛ (V-suc V-zero)) ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) ·
|
||||
(case `zero `zero (plus · one · (mul · # 0 · one)))
|
||||
—→⟨ ξ-·₂ V-ƛ β-zero ⟩
|
||||
(ƛ (case one (# 0) (`suc (plus · # 0 · # 1)))) · `zero
|
||||
—→⟨ β-ƛ V-zero ⟩
|
||||
case one `zero (`suc (plus · # 0 · `zero))
|
||||
—→⟨ β-suc V-zero ⟩
|
||||
`suc (plus · `zero · `zero)
|
||||
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
|
||||
`suc ((ƛ ƛ (case (# 1) (# 0) (`suc (plus · # 0 · # 1)))) · `zero · `zero)
|
||||
—→⟨ ξ-suc (ξ-·₁ (β-ƛ V-zero)) ⟩
|
||||
`suc ((ƛ (case `zero (# 0) (`suc (plus · # 0 · # 1)))) · `zero)
|
||||
—→⟨ ξ-suc (β-ƛ V-zero) ⟩
|
||||
`suc (case `zero `zero (`suc (plus · # 0 · `zero)))
|
||||
—→⟨ ξ-suc β-zero ⟩
|
||||
one
|
||||
∎
|
241
src/Homework3Prelude.agda
Normal file
241
src/Homework3Prelude.agda
Normal file
|
@ -0,0 +1,241 @@
|
|||
-- This file contains the code extracted from the DeBruijn chapter in PLFA
|
||||
|
||||
import Relation.Binary.PropositionalEquality as Eq
|
||||
open Eq using (_≡_; refl)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Nat using (ℕ; zero; suc; _<_; _≤?_; z≤n; s≤s)
|
||||
open import Relation.Nullary using (¬_)
|
||||
open import Relation.Nullary.Decidable using (True; toWitness)
|
||||
|
||||
module Homework3Prelude where
|
||||
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
|
||||
infixr 7 _⇒_
|
||||
|
||||
infix 5 ƛ_
|
||||
infix 5 μ_
|
||||
infixl 7 _·_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
infix 9 S_
|
||||
infix 9 #_
|
||||
|
||||
data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_,_ : Context → Type → Context
|
||||
|
||||
data _∋_ : Context → Type → Set where
|
||||
|
||||
Z : ∀ {Γ A}
|
||||
---------
|
||||
→ Γ , A ∋ A
|
||||
|
||||
S_ : ∀ {Γ A B}
|
||||
→ Γ ∋ A
|
||||
---------
|
||||
→ Γ , B ∋ A
|
||||
|
||||
data _⊢_ : Context → Type → Set where
|
||||
|
||||
`_ : ∀ {Γ A}
|
||||
→ Γ ∋ A
|
||||
-----
|
||||
→ Γ ⊢ A
|
||||
|
||||
ƛ_ : ∀ {Γ A B}
|
||||
→ Γ , A ⊢ B
|
||||
---------
|
||||
→ Γ ⊢ A ⇒ B
|
||||
|
||||
_·_ : ∀ {Γ A B}
|
||||
→ Γ ⊢ A ⇒ B
|
||||
→ Γ ⊢ A
|
||||
---------
|
||||
→ Γ ⊢ B
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
---------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`suc_ : ∀ {Γ}
|
||||
→ Γ ⊢ `ℕ
|
||||
------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
case : ∀ {Γ A}
|
||||
→ Γ ⊢ `ℕ
|
||||
→ Γ ⊢ A
|
||||
→ Γ , `ℕ ⊢ A
|
||||
----------
|
||||
→ Γ ⊢ A
|
||||
|
||||
μ_ : ∀ {Γ A}
|
||||
→ Γ , A ⊢ A
|
||||
---------
|
||||
→ Γ ⊢ A
|
||||
|
||||
length : Context → ℕ
|
||||
length ∅ = zero
|
||||
length (Γ , _) = suc (length Γ)
|
||||
|
||||
lookup : {Γ : Context} → {n : ℕ} → (p : n < length Γ) → Type
|
||||
lookup {(_ , A)} {zero} (s≤s z≤n) = A
|
||||
lookup {(Γ , _)} {(suc n)} (s≤s p) = lookup p
|
||||
|
||||
count : ∀ {Γ} → {n : ℕ} → (p : n < length Γ) → Γ ∋ lookup p
|
||||
count {_ , _} {zero} (s≤s z≤n) = Z
|
||||
count {Γ , _} {(suc n)} (s≤s p) = S (count p)
|
||||
|
||||
#_ : ∀ {Γ}
|
||||
→ (n : ℕ)
|
||||
→ {n∈Γ : True (suc n ≤? length Γ)}
|
||||
--------------------------------
|
||||
→ Γ ⊢ lookup (toWitness n∈Γ)
|
||||
#_ n {n∈Γ} = ` count (toWitness n∈Γ)
|
||||
|
||||
one : ∀ {Γ} → Γ ⊢ `ℕ
|
||||
one = `suc `zero
|
||||
|
||||
two : ∀ {Γ} → Γ ⊢ `ℕ
|
||||
two = `suc `suc `zero
|
||||
|
||||
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
|
||||
|
||||
ext : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
|
||||
---------------------------------
|
||||
→ (∀ {A B} → Γ , B ∋ A → Δ , B ∋ A)
|
||||
ext ρ Z = Z
|
||||
ext ρ (S x) = S (ρ x)
|
||||
|
||||
rename : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ∋ A)
|
||||
-----------------------
|
||||
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||
rename ρ (` x) = ` (ρ x)
|
||||
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
|
||||
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
|
||||
rename ρ (`zero) = `zero
|
||||
rename ρ (`suc M) = `suc (rename ρ M)
|
||||
rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ (μ N) = μ (rename (ext ρ) N)
|
||||
|
||||
exts : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
|
||||
---------------------------------
|
||||
→ (∀ {A B} → Γ , B ∋ A → Δ , B ⊢ A)
|
||||
exts σ Z = ` Z
|
||||
exts σ (S x) = rename S_ (σ x)
|
||||
|
||||
subst : ∀ {Γ Δ}
|
||||
→ (∀ {A} → Γ ∋ A → Δ ⊢ A)
|
||||
-----------------------
|
||||
→ (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||
subst σ (` k) = σ k
|
||||
subst σ (ƛ N) = ƛ (subst (exts σ) N)
|
||||
subst σ (L · M) = (subst σ L) · (subst σ M)
|
||||
subst σ (`zero) = `zero
|
||||
subst σ (`suc M) = `suc (subst σ M)
|
||||
subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N)
|
||||
subst σ (μ N) = μ (subst (exts σ) N)
|
||||
|
||||
_[_] : ∀ {Γ A B}
|
||||
→ Γ , B ⊢ A
|
||||
→ Γ ⊢ B
|
||||
---------
|
||||
→ Γ ⊢ A
|
||||
_[_] {Γ} {A} {B} N M = subst {Γ , B} {Γ} σ {A} N
|
||||
where
|
||||
σ : ∀ {A} → Γ , B ∋ A → Γ ⊢ A
|
||||
σ Z = M
|
||||
σ (S x) = ` x
|
||||
|
||||
data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
||||
|
||||
V-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B}
|
||||
---------------------------
|
||||
→ Value (ƛ N)
|
||||
|
||||
V-zero : ∀ {Γ}
|
||||
-----------------
|
||||
→ Value (`zero {Γ})
|
||||
|
||||
V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
|
||||
→ Value V
|
||||
--------------
|
||||
→ Value (`suc V)
|
||||
|
||||
infix 2 _—→_
|
||||
|
||||
data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
|
||||
→ L —→ L′
|
||||
---------------
|
||||
→ L · M —→ L′ · M
|
||||
|
||||
ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
|
||||
→ Value V
|
||||
→ M —→ M′
|
||||
---------------
|
||||
→ V · M —→ V · M′
|
||||
|
||||
β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
|
||||
→ Value W
|
||||
--------------------
|
||||
→ (ƛ N) · W —→ N [ W ]
|
||||
|
||||
ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
|
||||
→ M —→ M′
|
||||
-----------------
|
||||
→ `suc M —→ `suc M′
|
||||
|
||||
ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ L —→ L′
|
||||
-------------------------
|
||||
→ case L M N —→ case L′ M N
|
||||
|
||||
β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
-------------------
|
||||
→ case `zero M N —→ M
|
||||
|
||||
β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ Value V
|
||||
----------------------------
|
||||
→ case (`suc V) M N —→ N [ V ]
|
||||
|
||||
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
|
||||
----------------
|
||||
→ μ N —→ N [ μ N ]
|
||||
|
||||
infix 2 _—↠_
|
||||
infix 1 begin_
|
||||
infixr 2 _—→⟨_⟩_
|
||||
infix 3 _∎
|
||||
|
||||
data _—↠_ {Γ A} : (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
_∎ : (M : Γ ⊢ A)
|
||||
------
|
||||
→ M —↠ M
|
||||
|
||||
_—→⟨_⟩_ : (L : Γ ⊢ A) {M N : Γ ⊢ A}
|
||||
→ L —→ M
|
||||
-- → L —↠ M
|
||||
→ M —↠ N
|
||||
------
|
||||
→ L —↠ N
|
||||
|
||||
begin_ : ∀ {Γ A} {M N : Γ ⊢ A}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
begin M—↠N = M—↠N
|
81
src/LambdaPi.agda
Normal file
81
src/LambdaPi.agda
Normal file
|
@ -0,0 +1,81 @@
|
|||
module LambdaPi where
|
||||
|
||||
open import Data.Nat using (ℕ; suc; _≟_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_)
|
||||
open import Relation.Nullary using (yes; no; ¬_)
|
||||
|
||||
infix 4 _—→_
|
||||
infix 5 ƛ_
|
||||
infixl 7 _·_
|
||||
infix 9 `_
|
||||
infix 9 _[_:=_]
|
||||
|
||||
data Term : Set where
|
||||
-- var
|
||||
`_ : ℕ → Term
|
||||
|
||||
-- lam
|
||||
ƛ_ : Term → Term
|
||||
|
||||
-- app
|
||||
_·_ : Term → Term → Term
|
||||
|
||||
data Value : Term → Set where
|
||||
-- lam is a value
|
||||
V-ƛ : ∀ {N} → Value (ƛ N)
|
||||
|
||||
----------------------------------------------------
|
||||
-- substitution
|
||||
----------------------------------------------------
|
||||
_[_:=_] : Term → ℕ → Term → Term
|
||||
|
||||
-- var
|
||||
(` n₁) [ n₂ := V ] with n₁ ≟ n₂
|
||||
... | yes _ = V
|
||||
... | no _ = ` n₁
|
||||
|
||||
-- lam
|
||||
(ƛ N) [ n := V ] = ƛ (N [ suc n := V ])
|
||||
|
||||
-- app
|
||||
(L · M) [ y := V ] = L [ y := V ] · M [ y := V ]
|
||||
|
||||
----------------------------------------------------
|
||||
-- reduction
|
||||
----------------------------------------------------
|
||||
data _—→_ : Term → Term → Set where
|
||||
-- beta reduction for lambda applications
|
||||
β-ƛ : ∀ {x N V} → Value V → (ƛ N) · V —→ N [ x := V ]
|
||||
|
||||
----------------------------------------------------
|
||||
-- typing
|
||||
----------------------------------------------------
|
||||
data Type : Set where
|
||||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
|
||||
----------------------------------------------------
|
||||
-- typing context
|
||||
----------------------------------------------------
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_::_ : Type → Context
|
||||
|
||||
----------------------------------------------------
|
||||
-- typing judgment
|
||||
----------------------------------------------------
|
||||
data _⊢_⦂_ : Context → Term → Type → Set where
|
||||
|
||||
----------------------------------------------------
|
||||
-- progress
|
||||
----------------------------------------------------
|
||||
data Progress (M : Term) : Set where
|
||||
step : ∀ {N} → M —→ N → Progress M
|
||||
done : Value M → Progress M
|
||||
|
||||
progress : ∀ {M A} → ∅ ⊢ M ⦂ A → Progress M
|
||||
|
||||
----------------------------------------------------
|
||||
-- preservation
|
||||
----------------------------------------------------
|
||||
preserve : ∀ {M N A} → ∅ ⊢ M ⦂ A → M —→ N → ∅ ⊢ N ⦂ A
|
27
src/LambdaTest.agda
Normal file
27
src/LambdaTest.agda
Normal file
|
@ -0,0 +1,27 @@
|
|||
module LambdaTest where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
using (_≡_; _≢_; refl; sym; cong; cong₂)
|
||||
open import Data.String using (String; _≟_)
|
||||
open import Data.Nat using (ℕ; zero; suc)
|
||||
open import Data.Empty using (⊥; ⊥-elim)
|
||||
open import Data.Product
|
||||
using (_×_; proj₁; proj₂; ∃; ∃-syntax)
|
||||
renaming (_,_ to ⟨_,_⟩)
|
||||
open import Data.Sum using (_⊎_; inj₁; inj₂)
|
||||
open import Relation.Nullary using (¬_; Dec; yes; no)
|
||||
open import Function using (_∘_)
|
||||
V¬—→ V-ƛ = ?
|
||||
V¬—→ V-zero = ?
|
||||
V¬—→ (V-suc v) (ξ-suc m) = ?
|
||||
V¬—→ V-zero = ?
|
||||
V¬—→ (V-suc v) = ?
|
||||
open import plfa.part2.Lambda
|
||||
|
||||
V¬—→ : ∀ {M N}
|
||||
→ Value M
|
||||
----------
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc v) (ξ-suc m) = V¬—→ v m
|
30
src/OtherShit.agda
Normal file
30
src/OtherShit.agda
Normal file
|
@ -0,0 +1,30 @@
|
|||
module OtherShit where
|
||||
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
open ≡-Reasoning
|
||||
open import Data.Nat
|
||||
open import Data.Nat.Properties
|
||||
open import Data.Unit
|
||||
open import Data.Empty
|
||||
|
||||
data Bin : Set where
|
||||
O : Bin
|
||||
_I : Bin → Bin
|
||||
_II : Bin → Bin
|
||||
|
||||
data even : ℕ → Set
|
||||
data odd : ℕ → Set
|
||||
|
||||
data even where
|
||||
zero : even zero
|
||||
suc : ∀ {n : ℕ} → odd n → even (suc n)
|
||||
|
||||
data odd where
|
||||
suc : ∀ {n : ℕ} → even n → odd (suc n)
|
||||
|
||||
to : ℕ → Bin
|
||||
to zero = O
|
||||
to n with odd n
|
||||
... | x = O I
|
||||
to n with even n
|
||||
... | x = O II
|
19
src/Project/Lambda1.agda
Normal file
19
src/Project/Lambda1.agda
Normal file
|
@ -0,0 +1,19 @@
|
|||
module Project.Lambda1 where
|
||||
|
||||
open import Data.Nat using (ℕ; suc; _≟_)
|
||||
open import Relation.Binary.PropositionalEquality using (_≡_)
|
||||
open import Relation.Nullary using (yes; no; ¬_)
|
||||
|
||||
data Term : Set where
|
||||
`_ : ℕ → Term
|
||||
ƛ_ : Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
|
||||
`suc _ : Term → Term
|
||||
`zero : Term
|
||||
|
||||
data Value : Term → Set where
|
||||
V-ƛ : ∀ {N} → Value (ƛ N)
|
||||
|
||||
data Context : Set where
|
||||
⊙ : Context
|
|
@ -1,7 +1,7 @@
|
|||
$for(parts)$
|
||||
# $title$
|
||||
$for(sections)$
|
||||
## $title$ {#$anchor$}
|
||||
$shifted_raw$
|
||||
$content$
|
||||
$endfor$
|
||||
$endfor$
|
||||
|
|
@ -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
|
||||
|
|
|
@ -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/).
|
||||
|
|
|
@ -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:
|
||||
|
@ -635,7 +635,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,
|
||||
|
|
|
@ -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
|
||||
|
||||
|
@ -868,11 +868,21 @@ just apply the previous results which show addition
|
|||
is associative and commutative.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
+-swap : ∀ (m n p : ℕ) → m + (n + p) ≡ n + (m + p)
|
||||
+-swap m n p =
|
||||
begin
|
||||
m + (n + p)
|
||||
≡⟨ sym (+-assoc m n p) ⟩
|
||||
(m + n) + p
|
||||
≡⟨ cong (_+ p) (+-comm m n) ⟩
|
||||
(n + m) + p
|
||||
≡⟨ +-assoc n m p ⟩
|
||||
n + (m + p)
|
||||
∎
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `*-distrib-+` (recommended) {#times-distrib-plus}
|
||||
#### Exercise `*-distrib-+` (recommended) {name=times-distrib-plus}
|
||||
|
||||
Show multiplication distributes over addition, that is,
|
||||
|
||||
|
@ -881,11 +891,37 @@ Show multiplication distributes over addition, that is,
|
|||
for all naturals `m`, `n`, and `p`.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
|
||||
*-distrib-+ zero n p =
|
||||
begin
|
||||
(zero + n) * p
|
||||
≡⟨ cong (_* p) (+-comm zero n) ⟩
|
||||
(n + zero) * p
|
||||
≡⟨ cong (_* p) (+-identityʳ n) ⟩
|
||||
n * p
|
||||
∎
|
||||
*-distrib-+ (suc m) n p =
|
||||
begin
|
||||
(suc m + n) * p
|
||||
≡⟨ cong (_* p) (+-comm (suc m) n) ⟩
|
||||
(n + suc m) * p
|
||||
≡⟨ cong (_* p) (+-suc n m) ⟩
|
||||
suc (n + m) * p
|
||||
≡⟨ cong (_* p) (cong suc (+-comm n m)) ⟩
|
||||
suc (m + n) * p
|
||||
≡⟨⟩
|
||||
p + (m + n) * p
|
||||
≡⟨ cong (p +_) (*-distrib-+ m n p) ⟩
|
||||
p + (m * p + n * p)
|
||||
≡⟨ sym (+-assoc p (m * p) (n * p)) ⟩
|
||||
p + m * p + n * p
|
||||
≡⟨⟩
|
||||
suc m * p + n * p
|
||||
∎
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `*-assoc` (recommended) {#times-assoc}
|
||||
#### Exercise `*-assoc` (recommended) {name=times-assoc}
|
||||
|
||||
Show multiplication is associative, that is,
|
||||
|
||||
|
@ -895,10 +931,21 @@ for all naturals `m`, `n`, and `p`.
|
|||
|
||||
```
|
||||
-- Your code goes here
|
||||
*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
|
||||
*-assoc zero n p =
|
||||
begin
|
||||
(zero * n) * p
|
||||
∎
|
||||
*-assoc (suc m) n p =
|
||||
begin
|
||||
(suc m * n) * p
|
||||
≡⟨ ⟩
|
||||
|
||||
∎
|
||||
```
|
||||
|
||||
|
||||
#### Exercise `*-comm` (practice) {#times-comm}
|
||||
#### Exercise `*-comm` (practice) {name=times-comm}
|
||||
|
||||
Show multiplication is commutative, that is,
|
||||
|
||||
|
@ -912,7 +959,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 +972,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,
|
||||
|
||||
|
@ -949,7 +996,7 @@ Show the following three laws
|
|||
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)
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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`.
|
||||
|
@ -990,7 +990,7 @@ You will need to use extensionality.
|
|||
|
||||
#### Exercise `All-∀` (practice)
|
||||
|
||||
Show that `All P xs` is isomorphic to `∀ x → x ∈ xs → P x`.
|
||||
Show that `All P xs` is isomorphic to `∀ {x} → x ∈ xs → P x`.
|
||||
|
||||
```
|
||||
-- You code goes here
|
||||
|
|
|
@ -76,12 +76,12 @@ 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.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
_ = suc (suc (suc (suc (suc (suc (suc zero))))))
|
||||
```
|
||||
|
||||
|
||||
|
@ -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,9 +425,10 @@ 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 `+`.
|
||||
Compute `3 + 4`, writing out your reasoning as a chain of equations, using the
|
||||
equations for `+`.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
|
@ -486,7 +487,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 +497,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:
|
||||
|
||||
|
@ -506,7 +507,9 @@ Define exponentiation, which is given by the following equations:
|
|||
Check that `3 ^ 4` is `81`.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
_^_ : ℕ → ℕ → ℕ
|
||||
m ^ zero = 1
|
||||
m ^ suc n = m * ( m ^ n)
|
||||
```
|
||||
|
||||
|
||||
|
@ -566,7 +569,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 +704,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 +875,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:
|
||||
|
@ -919,6 +922,29 @@ Confirm that these both give the correct answer for zero through four.
|
|||
|
||||
```
|
||||
-- Your code goes here
|
||||
inc : Bin → Bin
|
||||
inc ⟨⟩ = ⟨⟩ O
|
||||
inc (n O) = n I
|
||||
inc (⟨⟩ I) = ⟨⟩ I O
|
||||
inc (n I) = (inc n) O
|
||||
|
||||
_ : inc (⟨⟩ I O I I) ≡ ⟨⟩ I I O O
|
||||
_ = refl
|
||||
|
||||
to : ℕ → Bin
|
||||
to zero = ⟨⟩ O
|
||||
to (suc n) = inc (to n)
|
||||
|
||||
from : Bin → ℕ
|
||||
from ⟨⟩ = 0
|
||||
from (n O) = 2 * (from n)
|
||||
from (n I) = 2 * (from n) + 1
|
||||
|
||||
_ : to 12 ≡ ⟨⟩ I I O O
|
||||
_ = refl
|
||||
|
||||
_ : from (⟨⟩ I O I I) ≡ 11
|
||||
_ = refl
|
||||
```
|
||||
|
||||
|
||||
|
|
|
@ -105,7 +105,7 @@ Show that a disjunction of universals implies a universal of disjunctions:
|
|||
```
|
||||
postulate
|
||||
⊎∀-implies-∀⊎ : ∀ {A : Set} {B C : A → Set} →
|
||||
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
|
||||
(∀ (x : A) → B x) ⊎ (∀ (x : A) → C x) → ∀ (x : A) → B x ⊎ C x
|
||||
```
|
||||
Does the converse hold? If so, prove; if not, explain why.
|
||||
|
||||
|
@ -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),
|
||||
|
@ -463,21 +463,21 @@ And to establish the following properties:
|
|||
to (from b) ≡ b
|
||||
|
||||
Using the above, establish that there is an isomorphism between `ℕ` and
|
||||
`∃[ b ] Can b`.
|
||||
`∃[ b ](Can b)`.
|
||||
|
||||
We recommend proving the following lemmas which show that, for a given
|
||||
binary number `b`, there is only one proof of `One b` and similarly
|
||||
for `Can b`.
|
||||
|
||||
≡One : ∀ {b : Bin} (o o′ : One b) → o ≡ o′
|
||||
≡One : ∀{b : Bin} (o o' : One b) → o ≡ o'
|
||||
|
||||
≡Can : ∀ {b : Bin} (cb cb′ : Can b) → cb ≡ cb′
|
||||
≡Can : ∀{b : Bin} (cb : Can b) (cb' : Can b) → cb ≡ cb'
|
||||
|
||||
Many of the alternatives for proving `to∘from` turn out to be tricky.
|
||||
However, the proof can be straightforward if you use the following lemma,
|
||||
which is a corollary of `≡Can`.
|
||||
|
||||
proj₁≡→Can≡ : {cb cb′ : ∃[ b ] Can b} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
|
||||
proj₁≡→Can≡ : {cb cb′ : ∃[ b ](Can b)} → proj₁ cb ≡ proj₁ cb′ → cb ≡ cb′
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
|
|
|
@ -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,15 +749,23 @@ 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.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
import Data.Nat.Properties
|
||||
open Data.Nat.Properties using (+-suc)
|
||||
|
||||
o+o≡e : ∀ {m n : ℕ}
|
||||
→ odd m → odd n
|
||||
→ even (m + n)
|
||||
|
||||
-- o+o≡e om (suc en) = suc (+-suc (o+e≡o om en))
|
||||
o+o≡e om (suc en) = +-suc ?
|
||||
```
|
||||
|
||||
#### Exercise `Bin-predicates` (stretch) {#Bin-predicates}
|
||||
#### Exercise `Bin-predicates` (stretch) {name=Bin-predicates}
|
||||
|
||||
Recall that
|
||||
Exercise [Bin](/Naturals/#Bin)
|
||||
|
|
|
@ -1388,12 +1388,3 @@ This chapter uses the following unicode:
|
|||
₆ U+2086 SUBSCRIPT SIX (\_6)
|
||||
₇ U+2087 SUBSCRIPT SEVEN (\_7)
|
||||
≠ U+2260 NOT EQUAL TO (\=n)
|
||||
|
||||
```
|
||||
mul : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
mul = μ ƛ ƛ (case (# 1) `zero (plus · # 1 · (# 3 · # 0 · # 1)))
|
||||
```
|
||||
|
||||
_ : eval (gas 100) (mul · two · two) ≡ [code generated by ctrl+c ctrl+n]
|
||||
|
||||
_ = refl
|
||||
|
|
|
@ -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,
|
||||
|
@ -208,11 +208,11 @@ _decidable_:
|
|||
|
||||
synthesize : ∀ (Γ : Context) (M : Term⁺)
|
||||
-----------------------
|
||||
→ Dec (∃[ A ]( Γ ⊢ M ↑ A ))
|
||||
→ Dec (∃[ A ](Γ ⊢ M ↑ A))
|
||||
|
||||
inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
|
||||
---------------
|
||||
→ Dec (Γ ⊢ M ↓ A)
|
||||
---------------
|
||||
→ Dec (Γ ⊢ M ↓ A)
|
||||
|
||||
Given context `Γ` and synthesised term `M`, we must decide whether
|
||||
there exists a type `A` such that `Γ ⊢ M ↑ A` holds, or its negation.
|
||||
|
@ -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/).
|
||||
|
@ -580,9 +580,9 @@ such that `Γ ∋ x ⦂ A` holds, then there is also no type `A` such that
|
|||
```
|
||||
ext∋ : ∀ {Γ B x y}
|
||||
→ x ≢ y
|
||||
→ ¬ ∃[ A ]( Γ ∋ x ⦂ A )
|
||||
→ ¬ ( ∃[ A ] Γ ∋ x ⦂ A )
|
||||
-----------------------------
|
||||
→ ¬ ∃[ A ]( Γ , y ⦂ B ∋ x ⦂ A )
|
||||
→ ¬ ( ∃[ A ] Γ , y ⦂ B ∋ x ⦂ A )
|
||||
ext∋ x≢y _ ⟨ A , Z ⟩ = x≢y refl
|
||||
ext∋ _ ¬∃ ⟨ A , S _ ∋x ⟩ = ¬∃ ⟨ A , ∋x ⟩
|
||||
```
|
||||
|
@ -597,8 +597,8 @@ there exists a type `A` such that `Γ ∋ x ⦂ A` holds, or its
|
|||
negation:
|
||||
```
|
||||
lookup : ∀ (Γ : Context) (x : Id)
|
||||
-------------------------
|
||||
→ Dec (∃[ A ]( Γ ∋ x ⦂ A ))
|
||||
-----------------------
|
||||
→ Dec (∃[ A ](Γ ∋ x ⦂ A))
|
||||
lookup ∅ x = no (λ ())
|
||||
lookup (Γ , y ⦂ B) x with x ≟ y
|
||||
... | yes refl = yes ⟨ B , Z ⟩
|
||||
|
@ -639,7 +639,7 @@ there is no term `B′` such that `Γ ⊢ L · M ↑ B′` holds:
|
|||
→ Γ ⊢ L ↑ A ⇒ B
|
||||
→ ¬ Γ ⊢ M ↓ A
|
||||
----------------------------
|
||||
→ ¬ ∃[ B′ ]( Γ ⊢ L · M ↑ B′ )
|
||||
→ ¬ ( ∃[ B′ ] Γ ⊢ L · M ↑ B′ )
|
||||
¬arg ⊢L ¬⊢M ⟨ B′ , ⊢L′ · ⊢M′ ⟩ rewrite dom≡ (uniq-↑ ⊢L ⊢L′) = ¬⊢M ⊢M′
|
||||
```
|
||||
Let `⊢L` be evidence that `Γ ⊢ L ↑ A ⇒ B` holds and `¬⊢M` be evidence
|
||||
|
@ -686,8 +686,8 @@ and a type `A` and either returns evidence that `Γ ⊢ M ↓ A`,
|
|||
or its negation:
|
||||
```
|
||||
synthesize : ∀ (Γ : Context) (M : Term⁺)
|
||||
---------------------------
|
||||
→ Dec (∃[ A ]( Γ ⊢ M ↑ A ))
|
||||
-----------------------
|
||||
→ Dec (∃[ A ](Γ ⊢ M ↑ A))
|
||||
|
||||
inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
|
||||
---------------
|
||||
|
|
|
@ -197,7 +197,11 @@ two natural numbers. Your definition may use `plus` as
|
|||
defined earlier.
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
mul : Term
|
||||
mul = μ "*" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
|
||||
case ` "m"
|
||||
[zero⇒ ` "n"
|
||||
|suc "m" ⇒ ` "+" · ` "n" · (` "*" · ` "m" · ` "n") ]
|
||||
```
|
||||
|
||||
|
||||
|
@ -209,11 +213,12 @@ definition may use `plusᶜ` as defined earlier (or may not
|
|||
— there are nice definitions both ways).
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
mulᶜ : Term
|
||||
mulᶜ = ƛ "m" ⇒ ƛ "n" ⇒ ƛ "s" ⇒ ƛ "z" ⇒ (` "m" · (` "n" · ` "s") · ` "z")
|
||||
```
|
||||
|
||||
|
||||
#### 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
|
||||
|
@ -262,6 +267,18 @@ plus′ = μ′ + ⇒ ƛ′ m ⇒ ƛ′ n ⇒
|
|||
```
|
||||
Write out the definition of multiplication in the same style.
|
||||
|
||||
```
|
||||
mul′ : Term
|
||||
mul′ = μ′ * ⇒ ƛ′ m ⇒ ƛ′ n ⇒
|
||||
case′ m
|
||||
[zero⇒ n
|
||||
|suc m ⇒ plus′ · n · (* · m · n) ]
|
||||
where
|
||||
* = ` "*"
|
||||
m = ` "m"
|
||||
n = ` "n"
|
||||
```
|
||||
|
||||
|
||||
### Formal vs informal
|
||||
|
||||
|
@ -542,6 +559,7 @@ substitution.
|
|||
|
||||
```
|
||||
-- Your code goes here
|
||||
|
||||
```
|
||||
|
||||
|
||||
|
@ -1038,7 +1056,34 @@ to the list
|
|||
[ ⟨ "z" , `ℕ ⟩ , ⟨ "s" , `ℕ ⇒ `ℕ ⟩ ]
|
||||
|
||||
```
|
||||
-- Your code goes here
|
||||
open import plfa.part1.Isomorphism using (_≃_)
|
||||
open import Data.Product using (_×_; _,_)
|
||||
open import Relation.Binary.PropositionalEquality
|
||||
open ≡-Reasoning renaming (begin_ to begin-≡_; _∎ to _∎-≡)
|
||||
|
||||
contextOfList : (l : List (Id × Type)) → Context
|
||||
contextOfList [] = ∅
|
||||
contextOfList ((id , type) ∷ l) = (contextOfList l) , id ⦂ type
|
||||
|
||||
listOfContext : (c : Context) → List (Id × Type)
|
||||
listOfContext ∅ = []
|
||||
listOfContext (c , x ⦂ x₁) = (x , x₁) ∷ listOfContext c
|
||||
|
||||
contextListIso : (c : Context) → contextOfList (listOfContext c) ≡ c
|
||||
contextListIso ∅ = refl
|
||||
contextListIso (c , x ⦂ x₁) = cong (_, x ⦂ x₁) (contextListIso c)
|
||||
|
||||
listContextIso : (l : List (Id × Type)) → listOfContext (contextOfList l) ≡ l
|
||||
listContextIso [] = refl
|
||||
listContextIso (x ∷ l) = cong (x ∷_) (listContextIso l)
|
||||
|
||||
Context≃List : Context ≃ List (Id × Type)
|
||||
Context≃List = record
|
||||
{ from = contextOfList
|
||||
; to = listOfContext
|
||||
; from∘to = contextListIso
|
||||
; to∘from = listContextIso
|
||||
}
|
||||
```
|
||||
|
||||
### Lookup judgment
|
||||
|
@ -1201,7 +1246,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,
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -195,7 +195,7 @@ distinct? (x ∷ xs)
|
|||
... | no x∉xs
|
||||
with distinct? xs
|
||||
... | yes dxs = yes ⟨ x∉xs , dxs ⟩
|
||||
... | no ¬dxs = no λ z → ¬dxs (proj₂ z)
|
||||
... | no ¬dxs = no λ x₁ → ¬dxs (proj₂ x₁)
|
||||
```
|
||||
|
||||
With this decision procedure in hand, we define the following
|
||||
|
@ -879,7 +879,7 @@ typed (C-suc c) = ⊢suc (typed c)
|
|||
typed (C-rcd ⊢Ms dks As<:Bs) = ⊢<: (⊢rcd ⊢Ms dks) As<:Bs
|
||||
```
|
||||
|
||||
## Progress {#subtyping-progress}
|
||||
## Progress <a name="subtyping-progress"></a>
|
||||
|
||||
The Progress theorem states that a well-typed term may either take a
|
||||
reduction step or it is already a value. The proof of Progress is like
|
||||
|
@ -952,7 +952,7 @@ progress (⊢<: {A = A}{B} ⊢M A<:B) = progress ⊢M
|
|||
* Case `⊢<:`: we invoke the induction hypothesis on sub-derivation of `Γ ⊢ M ⦂ A`.
|
||||
|
||||
|
||||
## Preservation {#subtyping-preservation}
|
||||
## Preservation <a name="subtyping-preservation"></a>
|
||||
|
||||
In this section we prove that when a well-typed term takes a reduction
|
||||
step, the result is another well-typed term with the same type.
|
||||
|
|
|
@ -1012,7 +1012,7 @@ all-funs∈ {⊥} f with f {⊥} refl
|
|||
... | fun ()
|
||||
all-funs∈ {v ↦ w} f = ⟨ v , ⟨ w , refl ⟩ ⟩
|
||||
all-funs∈ {u ⊔ u′} f
|
||||
with all-funs∈ (λ z → f (inj₁ z))
|
||||
with all-funs∈ λ z → f (inj₁ z)
|
||||
... | ⟨ v , ⟨ w , m ⟩ ⟩ = ⟨ v , ⟨ w , (inj₁ m) ⟩ ⟩
|
||||
```
|
||||
|
||||
|
|
|
@ -1,48 +1,45 @@
|
|||
---
|
||||
parts:
|
||||
- frontmatter: True
|
||||
title: "Front matter"
|
||||
- title: "Front matter"
|
||||
sections:
|
||||
- include: src/plfa/frontmatter/dedication.md
|
||||
- include: src/plfa/frontmatter/preface.md
|
||||
- include: README.md
|
||||
- mainmatter: True
|
||||
title: "Part 1: Logical Foundations"
|
||||
- src/plfa/frontmatter/dedication.md
|
||||
- src/plfa/frontmatter/preface.md
|
||||
- README.md
|
||||
- title: "Part 1: Logical Foundations"
|
||||
sections:
|
||||
- include: src/plfa/part1/Naturals.lagda.md
|
||||
- include: src/plfa/part1/Induction.lagda.md
|
||||
- include: src/plfa/part1/Relations.lagda.md
|
||||
- include: src/plfa/part1/Equality.lagda.md
|
||||
- include: src/plfa/part1/Isomorphism.lagda.md
|
||||
- include: src/plfa/part1/Connectives.lagda.md
|
||||
- include: src/plfa/part1/Negation.lagda.md
|
||||
- include: src/plfa/part1/Quantifiers.lagda.md
|
||||
- include: src/plfa/part1/Decidable.lagda.md
|
||||
- include: src/plfa/part1/Lists.lagda.md
|
||||
- src/plfa/part1/Naturals.lagda.md
|
||||
- src/plfa/part1/Induction.lagda.md
|
||||
- src/plfa/part1/Relations.lagda.md
|
||||
- src/plfa/part1/Equality.lagda.md
|
||||
- src/plfa/part1/Isomorphism.lagda.md
|
||||
- src/plfa/part1/Connectives.lagda.md
|
||||
- src/plfa/part1/Negation.lagda.md
|
||||
- src/plfa/part1/Quantifiers.lagda.md
|
||||
- src/plfa/part1/Decidable.lagda.md
|
||||
- src/plfa/part1/Lists.lagda.md
|
||||
- title: "Part 2: Programming Language Foundations"
|
||||
sections:
|
||||
- include: src/plfa/part2/Lambda.lagda.md
|
||||
- include: src/plfa/part2/Properties.lagda.md
|
||||
- include: src/plfa/part2/DeBruijn.lagda.md
|
||||
- include: src/plfa/part2/More.lagda.md
|
||||
- include: src/plfa/part2/Bisimulation.lagda.md
|
||||
- include: src/plfa/part2/Inference.lagda.md
|
||||
- include: src/plfa/part2/Untyped.lagda.md
|
||||
- include: src/plfa/part2/Confluence.lagda.md
|
||||
- include: src/plfa/part2/BigStep.lagda.md
|
||||
- src/plfa/part2/Lambda.lagda.md
|
||||
- src/plfa/part2/Properties.lagda.md
|
||||
- src/plfa/part2/DeBruijn.lagda.md
|
||||
- src/plfa/part2/More.lagda.md
|
||||
- src/plfa/part2/Bisimulation.lagda.md
|
||||
- src/plfa/part2/Inference.lagda.md
|
||||
- src/plfa/part2/Untyped.lagda.md
|
||||
- src/plfa/part2/Confluence.lagda.md
|
||||
- src/plfa/part2/BigStep.lagda.md
|
||||
- title: "Part 3: Denotational Semantics"
|
||||
sections:
|
||||
- include: src/plfa/part3/Denotational.lagda.md
|
||||
- include: src/plfa/part3/Compositional.lagda.md
|
||||
- include: src/plfa/part3/Soundness.lagda.md
|
||||
- include: src/plfa/part3/Adequacy.lagda.md
|
||||
- include: src/plfa/part3/ContextualEquivalence.lagda.md
|
||||
- backmatter: True
|
||||
title: "Appendix"
|
||||
- src/plfa/part3/Denotational.lagda.md
|
||||
- src/plfa/part3/Compositional.lagda.md
|
||||
- src/plfa/part3/Soundness.lagda.md
|
||||
- src/plfa/part3/Adequacy.lagda.md
|
||||
- src/plfa/part3/ContextualEquivalence.lagda.md
|
||||
- title: "Appendix"
|
||||
sections:
|
||||
- include: src/plfa/part2/Substitution.lagda.md
|
||||
- src/plfa/part2/Substitution.lagda.md
|
||||
- title: "Back matter"
|
||||
sections:
|
||||
- include: src/plfa/backmatter/acknowledgements.md
|
||||
- include: src/plfa/backmatter/Fonts.lagda.md
|
||||
---
|
||||
- src/plfa/backmatter/acknowledgements.md
|
||||
- src/plfa/backmatter/Fonts.lagda.md
|
||||
---
|
16
stack.yaml
16
stack.yaml
|
@ -1,8 +1,10 @@
|
|||
resolver: lts-17.2
|
||||
|
||||
compiler: ghc-8.10.5
|
||||
# Use GHC 8.10.3
|
||||
compiler: ghc-8.10.3
|
||||
compiler-check: match-exact
|
||||
|
||||
# Allow never versions of packages
|
||||
allow-newer: true
|
||||
|
||||
flags:
|
||||
|
@ -13,16 +15,28 @@ packages:
|
|||
- .
|
||||
|
||||
extra-deps:
|
||||
|
||||
# Agda dependencies:
|
||||
- Agda-2.6.1.3@sha256:87769ebab4259b184c5b11d5beaff39b88bcc37902dfb3341f4fc46c5c7d3134,32945
|
||||
|
||||
# Hakyll dependencies:
|
||||
- hakyll-4.13.4.1
|
||||
- pandoc-2.10.1@sha256:23d7ec480c7cb86740475a419d6ca4819987b6dd23bbae9b50bc3d42a7ed2f9f,36933
|
||||
- pandoc-citeproc-0.17.0.2@sha256:39c5c60a5eca2c1cb50ae9a00dc7093ca1baac78ad5be4e222505de257dce456,8737
|
||||
- commonmark-0.1.1.4@sha256:8717891c53c124ff64187c463619450241a41c0951cda2a43267d40f78992362,3278
|
||||
- commonmark-extensions-0.2.0.4@sha256:6a437bcfa3c757af4262b71336513619990eafb5cfdc33e57a499c93ad225608,3184
|
||||
- commonmark-pandoc-0.2.0.1@sha256:529c6e2c6cabf61558b66a28123eafc1d90d3324be29819f59f024e430312c1f,1105
|
||||
|
||||
# Sass dependencies:
|
||||
- hsass-0.8.0@sha256:05fb3d435dbdf9f66a98db4e1ee57a313170a677e52ab3a5a05ced1fc42b0834,2899
|
||||
- hlibsass-0.1.10.1@sha256:08db56c633e9a83a642d8ea57dffa93112b092d05bf8f3b07491cfee9ee0dfa5,2565
|
||||
|
||||
# GitHub API dependencies:
|
||||
- github-0.26@sha256:a9d4046325c3eb28cdc7bef2c3f5bb213328caeae0b7dce6f51de655f0bffaa1,7162
|
||||
- binary-instances-1.0.0.1@sha256:e234be994da675479a3661f050d4a1d53565c9ed7786d9a68b7a29ba8b54b5a7,2659
|
||||
|
||||
# Regex dependencies:
|
||||
- text-regex-replace-0.1.1.3@sha256:e7f612df671c93ced54a3d26528db37852069884e5cb67d5afbb49d3defb5eb9,1627
|
||||
|
||||
# Version of text-icu compatible with icu68+
|
||||
- text-icu-0.7.1.0@sha256:44e8b5966fcf61356a7356f3d2e8a5c5cc538170a15e94ff7b79b9f48ce9fd2f,3497
|
||||
|
|
26
templates/epub.html
Normal file
26
templates/epub.html
Normal file
|
@ -0,0 +1,26 @@
|
|||
<?xml version="1.0" encoding="UTF-8"?>
|
||||
<!DOCTYPE html>
|
||||
<html xmlns="http://www.w3.org/1999/xhtml" xmlns:epub="http://www.idpf.org/2007/ops" xml:lang="$language$">
|
||||
<head>
|
||||
<meta charset="utf-8" />
|
||||
<title>$pagetitle$</title>
|
||||
<link rel="stylesheet" type="text/css" href="css/agda.css" />
|
||||
<link rel="stylesheet" type="text/css" href="css/epub.css" />
|
||||
</head>
|
||||
<body>
|
||||
<section epub:type="titlepage" class="titlepage">
|
||||
<h1 class="title">$pagetitle$</h1>
|
||||
$for(authors)$
|
||||
<p class="author">$name$</p>
|
||||
$endfor$
|
||||
$if(rights)$
|
||||
<div class="rights">$rights$</div>
|
||||
$endif$
|
||||
</section>
|
||||
<!-- NOTE: body is escaped because it is filled in by the Pandoc template engine, -->
|
||||
<!-- whereas the rest is filled in by the Hakyll template engine, both of -->
|
||||
<!-- which use the same syntax. Yes, this is confusing. -->
|
||||
$$body$$
|
||||
</body>
|
||||
</html>
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
---
|
||||
comment: This file exists to save the correct metadata to the generated `epub.md` file.
|
||||
---
|
||||
|
||||
---
|
||||
lang : $language$
|
||||
pagetitle : $pagetitle$
|
||||
title : $pagetitle$
|
||||
titlepage : true
|
||||
description : $description$
|
||||
author :
|
||||
$for(authors)$
|
||||
- $name$
|
||||
$endfor$
|
||||
date : $modified$
|
||||
rights : $rights$
|
||||
---
|
||||
|
||||
$body$
|
|
@ -1,7 +1,7 @@
|
|||
<article class="post">
|
||||
$partial("templates/next.html")$
|
||||
<header class="post-header">
|
||||
<h1 class="post-title" $if(anchor)$id="$anchor$"$endif$>$title$</h1>
|
||||
<h1 class="post-title">$title$</h1>
|
||||
</header>
|
||||
<div class="post-content">
|
||||
$body$
|
||||
|
|
Loading…
Reference in a new issue