Fixed PDF generation.
This commit is contained in:
Wen Kokke
parent
7345c36d80
commit
d14b04ebf2
17 changed files with 315 additions and 1172 deletions
140
Makefile
140
Makefile
|
|
@ -6,6 +6,13 @@ SITE_DIR := _site
|
||||||
CACHE_DIR := _cache
|
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 -- \
|
||||||
|
--indented-code-classes=default
|
||||||
|
--top-level-division=chapter
|
||||||
|
|
||||||
|
|
||||||
#################################################################################
|
#################################################################################
|
||||||
# Setup Git Hooks
|
# Setup Git Hooks
|
||||||
|
|
@ -29,6 +36,7 @@ standard-library/ChangeLog.md:
|
||||||
git submodule init
|
git submodule init
|
||||||
git submodule update --recursive
|
git submodule update --recursive
|
||||||
|
|
||||||
|
|
||||||
#################################################################################
|
#################################################################################
|
||||||
# Test generated site with HTMLProofer
|
# Test generated site with HTMLProofer
|
||||||
#################################################################################
|
#################################################################################
|
||||||
|
|
@ -48,6 +56,7 @@ test: setup-install-htmlproofer build
|
||||||
--check-opengraph \
|
--check-opengraph \
|
||||||
.
|
.
|
||||||
|
|
||||||
|
|
||||||
#################################################################################
|
#################################################################################
|
||||||
# Test generated EPUB with EPUBCheck
|
# Test generated EPUB with EPUBCheck
|
||||||
#################################################################################
|
#################################################################################
|
||||||
|
|
@ -152,6 +161,120 @@ endif
|
||||||
endif
|
endif
|
||||||
|
|
||||||
|
|
||||||
|
#################################################################################
|
||||||
|
# Build PDF
|
||||||
|
#################################################################################
|
||||||
|
|
||||||
|
PDF_DIR := pdf
|
||||||
|
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
|
||||||
|
|
||||||
|
# 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
|
||||||
|
define TEX_PATH
|
||||||
|
$(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
|
||||||
|
|
||||||
|
# List source and intermediate files
|
||||||
|
PDF_LUA_SCRIPTS := $(wildcard $(PDF_LUA_DIR)/*.lua)
|
||||||
|
PDF_STATIC_FILES := $(wildcard pdf/*.*)
|
||||||
|
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) $(PDF_STATIC_FILES))
|
||||||
|
|
||||||
|
# Compile PLFA to a PDF
|
||||||
|
.PHONY: pdf
|
||||||
|
pdf: $(SITE_DIR)/plfa.pdf
|
||||||
|
|
||||||
|
$(SITE_DIR)/plfa.pdf: $(TEX_FILES)
|
||||||
|
@cd $(TEX_DIR) && latexmk -pdf -lualatex -use-make -halt-on-error plfa.tex
|
||||||
|
@cp $(TEX_DIR)/plfa.pdf $(SITE_DIR)/plfa.pdf
|
||||||
|
|
||||||
|
|
||||||
|
# Copy static files needed by PDF compilation
|
||||||
|
define MK_COPYSTATIC_RULE
|
||||||
|
src := $(1)
|
||||||
|
dst := $(2)
|
||||||
|
$$(dst): $$(src)
|
||||||
|
@echo "Copy $$< to $$@"
|
||||||
|
@cp $$< $$@
|
||||||
|
endef
|
||||||
|
|
||||||
|
# Compile Markdown files to LaTeX
|
||||||
|
define MK_MD2TEX_RULE
|
||||||
|
src := $(1)
|
||||||
|
dst := $(2)
|
||||||
|
tpl := $(3)
|
||||||
|
$$(dst): export UNCHECKED_FILES = README.md
|
||||||
|
$$(dst): $$(src) $$(tpl) $(PDF_LUA_SCRIPTS) | setup-install-pandoc
|
||||||
|
@echo "Compile $$< to $$@"
|
||||||
|
@mkdir -p '$$(@D)'
|
||||||
|
@$(PANDOC) \
|
||||||
|
--lua-filter=$(PDF_LUA_DIR)/remove-badges.lua \
|
||||||
|
--lua-filter=$(PDF_LUA_DIR)/typeset-codeblocks.lua \
|
||||||
|
--lua-filter=$(PDF_LUA_DIR)/rewrite-links.lua \
|
||||||
|
--lua-filter=$(PDF_LUA_DIR)/single-file-headers-ids.lua \
|
||||||
|
--template=$$(tpl) \
|
||||||
|
$$< -o $$@
|
||||||
|
endef
|
||||||
|
|
||||||
|
# Compile Literate Agda files to LaTeX
|
||||||
|
define MK_LAGDA_MD2TEX_RULE
|
||||||
|
src := $(1)
|
||||||
|
dst := $(2)
|
||||||
|
$$(dst): $$(src) $(LAGDA_TEX_FILES) | setup-install-agda
|
||||||
|
@$(AGDA) --include-path=$(LAGDA_TEX_DIR) --latex --latex-dir=$(TEX_DIR) $$<
|
||||||
|
endef
|
||||||
|
|
||||||
|
|
||||||
|
# Copy static files (from PDF_DIR/% to TEX_DIR/%)
|
||||||
|
$(foreach static_file,\
|
||||||
|
$(PDF_STATIC_FILES),\
|
||||||
|
$(eval $(call MK_COPYSTATIC_RULE,\
|
||||||
|
$(static_file),\
|
||||||
|
$(call TEX_PATH,$(static_file)))))
|
||||||
|
|
||||||
|
# Compile .md files (from MD_DIR/%.md to TEX_DIR/%.tex)
|
||||||
|
$(foreach md_file,\
|
||||||
|
$(filter-out %acknowledgements.md %.lagda.md,$(MD_FILES)),\
|
||||||
|
$(eval $(call MK_MD2TEX_RULE,\
|
||||||
|
$(md_file),\
|
||||||
|
$(call TEX_PATH,$(md_file)),\
|
||||||
|
$(PDF_TEMPLATE_DIR)/chapter.latex)))
|
||||||
|
|
||||||
|
# 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)),\
|
||||||
|
$(PDF_TEMPLATE_DIR)/chapter.latex)))
|
||||||
|
|
||||||
|
# Compile acknowledgements (from SITE_DIR/acknowledgements.md to TEX_DIR/acknowledgements.tex)
|
||||||
|
$(eval $(call MK_MD2TEX_RULE,\
|
||||||
|
$(SITE_DIR)/acknowledgements.md,\
|
||||||
|
$(TEX_DIR)/plfa/backmatter/acknowledgements.tex,\
|
||||||
|
$(PDF_TEMPLATE_DIR)/acknowledgements.latex))
|
||||||
|
|
||||||
|
# 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)))))
|
||||||
|
|
||||||
|
|
||||||
#################################################################################
|
#################################################################################
|
||||||
# Setup dependencies
|
# Setup dependencies
|
||||||
#################################################################################
|
#################################################################################
|
||||||
|
|
@ -218,6 +341,19 @@ ifeq (,$(wildcard $(shell which bundle)))
|
||||||
gem install bundle
|
gem install bundle
|
||||||
endif
|
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
|
# Build legacy versions of website using Jekyll
|
||||||
|
|
@ -269,7 +405,3 @@ versions/$$(out): $$(tmp_dir)
|
||||||
endef
|
endef
|
||||||
|
|
||||||
$(foreach legacy_version,$(LEGACY_VERSIONS),$(eval $(call build_legacy_version,$(legacy_version))))
|
$(foreach legacy_version,$(LEGACY_VERSIONS),$(eval $(call build_legacy_version,$(legacy_version))))
|
||||||
|
|
||||||
.PHONY: pdf
|
|
||||||
pdf:
|
|
||||||
make -C pdf
|
|
||||||
128
pdf/Makefile
128
pdf/Makefile
|
|
@ -1,128 +0,0 @@
|
||||||
# To use the makefile, specify the path to source files under SRC
|
|
||||||
# and the path to pandoc-filters under FILTERS
|
|
||||||
|
|
||||||
|
|
||||||
.PHONY: all clean
|
|
||||||
|
|
||||||
SRC := ../src
|
|
||||||
SITE := ../_site
|
|
||||||
front_and_back := latex/plfa/frontmatter/dedication.tex latex/plfa/frontmatter/README.tex\
|
|
||||||
latex/plfa/frontmatter/preface.tex latex/plfa/backmatter/acknowledgements.tex
|
|
||||||
lagda_md_files := $(shell find $(SRC) -name '*.lagda.md')
|
|
||||||
transpiled_files := $(patsubst $(SRC)/%.md,lagda_tex/%.tex,$(lagda_md_files))
|
|
||||||
latex_files := $(patsubst $(SRC)/%.lagda.md,latex/%.tex,$(lagda_md_files))
|
|
||||||
pdfs := $(patsubst $(SRC)/%.lagda.md,pdf/%.pdf,$(lagda_md_files))
|
|
||||||
|
|
||||||
# for make to clean file in subdirectories
|
|
||||||
# https://stackoverflow.com/questions/4210042/exclude-directory-from-find-command
|
|
||||||
SUBDIR_ROOTS := tex latex
|
|
||||||
DIRS := . $(shell find $(SUBDIR_ROOTS) -type d)
|
|
||||||
GARBAGE_TYPES := *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls
|
|
||||||
GARBAGE_TYPED_FOLDERS := $(foreach DIR, $(DIRS), $(addprefix $(DIR)/,$(GARBAGE_TYPES)))
|
|
||||||
|
|
||||||
all: all_tex plfa.pdf
|
|
||||||
|
|
||||||
# A pdf for the whole book
|
|
||||||
plfa.pdf: $(latex_files) plfa.tex $(front_and_back)
|
|
||||||
latexmk -pdf -lualatex -use-make plfa.tex
|
|
||||||
|
|
||||||
plfa-sample.pdf: $(latex_files) plfa-sample.tex $(front_and_back)
|
|
||||||
latexmk -pdf -lualatex -use-make plfa-sample.tex
|
|
||||||
|
|
||||||
all_tex: $(transpiled_files)
|
|
||||||
all_latex: $(latex_files)
|
|
||||||
all_pdfs : $(pdfs)
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
# General Rules
|
|
||||||
|
|
||||||
# from https://stackoverflow.com/questions/48267813/makefile-compile-objects-to-different-directory-and-build-from-there
|
|
||||||
# make a different directory for lagda.tex
|
|
||||||
# --shift-heading-level-by=-1 is a good choice
|
|
||||||
# when converting HTML or Markdown documents that use an initial level-1 heading
|
|
||||||
# also can try treat first heading as chapter
|
|
||||||
# by using --top-level-division=chapter
|
|
||||||
# for the document title and level-2+ headings for sections.
|
|
||||||
lagda_tex/%.lagda.tex : $(SRC)/%.lagda.md \
|
|
||||||
codeblocks.lua rewrite-links.lua header-id.lua \
|
|
||||||
lagdamd2tex_chapter.latex
|
|
||||||
@echo "Transpiling $< into $@"
|
|
||||||
@mkdir -p '$(@D)'
|
|
||||||
pandoc $< --indented-code-classes=default \
|
|
||||||
--lua-filter ./codeblocks.lua \
|
|
||||||
--lua-filter ./rewrite-links.lua \
|
|
||||||
--lua-filter ./header-id.lua \
|
|
||||||
--top-level-division=chapter \
|
|
||||||
-o $@ \
|
|
||||||
--template=lagdamd2tex_chapter.latex
|
|
||||||
|
|
||||||
# run agda under same directory with lagda.tex
|
|
||||||
latex/%.tex : lagda_tex/%.lagda.tex
|
|
||||||
cd lagda_tex; agda --latex-dir=../latex \
|
|
||||||
--latex $(subst lagda_tex/,,$<)
|
|
||||||
|
|
||||||
|
|
||||||
pdf/%.pdf: latex/%.tex
|
|
||||||
@echo $<
|
|
||||||
latexmk -pdf -output-directory="pdf" -lualatex -use-make $<
|
|
||||||
|
|
||||||
# Specific rules for .md files, could be optimized!
|
|
||||||
# for general frontmatter
|
|
||||||
latex/plfa/frontmatter/%.tex : $(SRC)/plfa/frontmatter/%.md codeblocks-readme.lua
|
|
||||||
@echo "Transpiling $< into $@"
|
|
||||||
@mkdir -p '$(@D)'
|
|
||||||
pandoc $< --indented-code-classes=default \
|
|
||||||
--lua-filter ./codeblocks-readme.lua \
|
|
||||||
--lua-filter ./header-id.lua \
|
|
||||||
--top-level-division=chapter \
|
|
||||||
-o $@ \
|
|
||||||
--template=lagdamd2tex_chapter.latex
|
|
||||||
# for readme
|
|
||||||
latex/plfa/frontmatter/README.tex : ../README.md codeblocks-readme.lua header-id.lua handle-badges.lua \
|
|
||||||
lagdamd2tex_chapter.latex
|
|
||||||
@echo "Transpiling $< into $@"
|
|
||||||
@mkdir -p '$(@D)'
|
|
||||||
pandoc $< --indented-code-classes=default \
|
|
||||||
--lua-filter ./codeblocks-readme.lua \
|
|
||||||
--lua-filter ./header-id.lua \
|
|
||||||
--lua-filter ./handle-badges.lua \
|
|
||||||
--top-level-division=chapter \
|
|
||||||
-o $@ \
|
|
||||||
--template=lagdamd2tex_chapter.latex
|
|
||||||
|
|
||||||
# process for acknowledgements
|
|
||||||
# generate in _site/acknowledgements.md
|
|
||||||
../_site/acknowledgements.md : $(SRC)/plfa/backmatter/acknowledgements.md
|
|
||||||
cd ..; stack build && stack exec site build
|
|
||||||
|
|
||||||
# transpile once to html to unify the lists
|
|
||||||
acknowledgements.html : $(SITE)/acknowledgements.md
|
|
||||||
pandoc -o $@ $<
|
|
||||||
|
|
||||||
# compile the above version to latex
|
|
||||||
latex/plfa/backmatter/acknowledgements.tex : acknowledgements.html lagdamd2tex_acknowledgement.latex
|
|
||||||
@echo "Transpiling $< into $@"
|
|
||||||
@mkdir -p '$(@D)'
|
|
||||||
pandoc $< --indented-code-classes=default \
|
|
||||||
--top-level-division=chapter \
|
|
||||||
-o $@ \
|
|
||||||
--template=lagdamd2tex_acknowledgement.latex
|
|
||||||
|
|
||||||
|
|
||||||
# general backmatter
|
|
||||||
latex/plfa/backmatter/%.tex : $(SRC)/plfa/backmatter/%.md codeblocks-readme.lua lagdamd2tex_chapter.latex
|
|
||||||
@echo "Transpiling $< into $@"
|
|
||||||
@mkdir -p '$(@D)'
|
|
||||||
pandoc $< --indented-code-classes=default \
|
|
||||||
--lua-filter ./codeblocks-readme.lua \
|
|
||||||
--lua-filter ./header-id.lua \
|
|
||||||
--top-level-division=chapter \
|
|
||||||
-o $@ \
|
|
||||||
--template=lagdamd2tex_chapter.latex
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
clean:
|
|
||||||
$(RM) -rf $(GARBAGE_TYPED_FOLDERS)
|
|
||||||
|
|
||||||
|
|
@ -1,20 +0,0 @@
|
||||||
This directory contains the files needed for building a pdf version of the book. Notice the structure is important here: the makefile and latex commands are written based on relative paths.
|
|
||||||
|
|
||||||
Dependencies (relative to the root):
|
|
||||||
- all things under `pdf/` except `lagda_tex/` and `latex/`. The latter two are generated by the makefile and uploaded for compiling speed.
|
|
||||||
- agda source files under `src/`
|
|
||||||
- `_site/acknowledgements.md` generated when building the site
|
|
||||||
- `README.md`
|
|
||||||
- the font `DejaVu mononoki Symbola Droid` installed globally. (Could change to local?)
|
|
||||||
|
|
||||||
First, run `stack build && stack exec site rebuild` from the parent directory to generate acknowledgements.md under `_site`, which is needed by the pdf (Only need to do this once).
|
|
||||||
|
|
||||||
Then, running `make pdf` from the parent directory should be sufficient to compile the book. The book will be generated in this folder as `plfa.pdf`.
|
|
||||||
|
|
||||||
Alternatively, makefile in this directory provide these options:
|
|
||||||
|
|
||||||
```make
|
|
||||||
all # Build plfa.pdf (can also run from the parent as "make pdf")
|
|
||||||
plfa-sample.pdf # Build a shrinked version of the book for testing
|
|
||||||
all_tex # generate all tex version of lagda files under tex/
|
|
||||||
```
|
|
||||||
708
pdf/agda.sty
708
pdf/agda.sty
|
|
@ -1,708 +0,0 @@
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% Some useful commands when doing highlighting of Agda code in LaTeX.
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
|
|
||||||
\ProvidesPackage{agda}
|
|
||||||
|
|
||||||
\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
|
|
||||||
calc, environ, xparse, xkeyval}
|
|
||||||
|
|
||||||
% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation
|
|
||||||
\newif\ifxetexorluatex
|
|
||||||
\ifxetex
|
|
||||||
\xetexorluatextrue
|
|
||||||
\else
|
|
||||||
\ifluatex
|
|
||||||
\xetexorluatextrue
|
|
||||||
\else
|
|
||||||
\xetexorluatexfalse
|
|
||||||
\fi
|
|
||||||
\fi
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% Options
|
|
||||||
|
|
||||||
\DeclareOption{bw} {\newcommand{\AgdaColourScheme}{bw}}
|
|
||||||
\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}}
|
|
||||||
|
|
||||||
\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse
|
|
||||||
\DeclareOption{references}{
|
|
||||||
\@AgdaEnableReferencestrue
|
|
||||||
}
|
|
||||||
|
|
||||||
\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse
|
|
||||||
\DeclareOption{links}{
|
|
||||||
\@AgdaEnableLinkstrue
|
|
||||||
}
|
|
||||||
|
|
||||||
\ProcessOptions\relax
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% Font setup
|
|
||||||
|
|
||||||
\tracinglostchars=2 % If the font is missing some symbol, then say
|
|
||||||
% so in the compilation output.
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% Colour schemes.
|
|
||||||
|
|
||||||
\providecommand{\AgdaColourScheme}{standard}
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% References to code (needs additional post-processing of tex files to
|
|
||||||
% work, see wiki for details).
|
|
||||||
|
|
||||||
\if@AgdaEnableReferences
|
|
||||||
\RequirePackage{catchfilebetweentags, xstring}
|
|
||||||
\newcommand{\AgdaRef}[2][]{%
|
|
||||||
\StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]%
|
|
||||||
\ifthenelse{\isempty{#1}}%
|
|
||||||
{\ExecuteMetaData{AgdaTag-\tmp}}%
|
|
||||||
{\ExecuteMetaData{#1}{AgdaTag-\tmp}}
|
|
||||||
}
|
|
||||||
\fi
|
|
||||||
|
|
||||||
\providecommand{\AgdaRef}[2][]{#2}
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% Links (only done if the option is passed and the user has loaded the
|
|
||||||
% hyperref package).
|
|
||||||
|
|
||||||
\if@AgdaEnableLinks
|
|
||||||
\@ifpackageloaded{hyperref}{
|
|
||||||
|
|
||||||
% List that holds added targets.
|
|
||||||
\newcommand{\AgdaList}[0]{}
|
|
||||||
|
|
||||||
\newtoggle{AgdaIsElem}
|
|
||||||
\newcounter{AgdaIndex}
|
|
||||||
\newcommand{\AgdaLookup}[3]{%
|
|
||||||
\togglefalse{AgdaIsElem}%
|
|
||||||
\setcounter{AgdaIndex}{0}%
|
|
||||||
\renewcommand*{\do}[1]{%
|
|
||||||
\ifstrequal{#1}{##1}%
|
|
||||||
{\toggletrue{AgdaIsElem}\listbreak}%
|
|
||||||
{\stepcounter{AgdaIndex}}}%
|
|
||||||
\dolistloop{\AgdaList}%
|
|
||||||
\iftoggle{AgdaIsElem}{#2}{#3}%
|
|
||||||
}
|
|
||||||
|
|
||||||
\newcommand*{\AgdaTargetHelper}[1]{%
|
|
||||||
\AgdaLookup{#1}%
|
|
||||||
{\PackageError{agda}{``#1'' used as target more than once}%
|
|
||||||
{Overloaded identifiers and links do not%
|
|
||||||
work well, consider using unique%
|
|
||||||
\MessageBreak identifiers instead.}%
|
|
||||||
}%
|
|
||||||
{\listadd{\AgdaList}{#1}%
|
|
||||||
\hypertarget{Agda\theAgdaIndex}{}%
|
|
||||||
}%
|
|
||||||
}
|
|
||||||
|
|
||||||
\newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}}
|
|
||||||
|
|
||||||
\newcommand{\AgdaLink}[1]{%
|
|
||||||
\AgdaLookup{#1}%
|
|
||||||
{\hyperlink{Agda\theAgdaIndex}{#1}}%
|
|
||||||
{#1}%
|
|
||||||
}
|
|
||||||
}{\PackageError{agda}{Load the hyperref package before the agda package}{}}
|
|
||||||
\fi
|
|
||||||
|
|
||||||
\providecommand{\AgdaTarget}[1]{}
|
|
||||||
\providecommand{\AgdaLink}[1]{#1}
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% Font styles.
|
|
||||||
|
|
||||||
\newcommand{\AgdaFontStyle}[1]{\texttt{#1}}
|
|
||||||
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
|
|
||||||
\newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
|
|
||||||
}{
|
|
||||||
\newcommand{\AgdaKeywordFontStyle}[1]{\texttt{#1}}
|
|
||||||
}
|
|
||||||
\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}
|
|
||||||
\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}
|
|
||||||
\newcommand{\AgdaBoundFontStyle}[1]{\texttt{#1}}
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% Colours.
|
|
||||||
|
|
||||||
% ----------------------------------
|
|
||||||
% The black and white colour scheme.
|
|
||||||
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
|
|
||||||
|
|
||||||
% Aspect colours.
|
|
||||||
\definecolor{AgdaComment} {HTML}{000000}
|
|
||||||
\definecolor{AgdaPragma} {HTML}{000000}
|
|
||||||
\definecolor{AgdaKeyword} {HTML}{000000}
|
|
||||||
\definecolor{AgdaString} {HTML}{000000}
|
|
||||||
\definecolor{AgdaNumber} {HTML}{000000}
|
|
||||||
\definecolor{AgdaSymbol} {HTML}{000000}
|
|
||||||
\definecolor{AgdaPrimitiveType}{HTML}{000000}
|
|
||||||
|
|
||||||
% NameKind colours.
|
|
||||||
\definecolor{AgdaBound} {HTML}{000000}
|
|
||||||
\definecolor{AgdaGeneralizable} {HTML}{000000}
|
|
||||||
\definecolor{AgdaInductiveConstructor} {HTML}{000000}
|
|
||||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{000000}
|
|
||||||
\definecolor{AgdaDatatype} {HTML}{000000}
|
|
||||||
\definecolor{AgdaField} {HTML}{000000}
|
|
||||||
\definecolor{AgdaFunction} {HTML}{000000}
|
|
||||||
\definecolor{AgdaMacro} {HTML}{000000}
|
|
||||||
\definecolor{AgdaModule} {HTML}{000000}
|
|
||||||
\definecolor{AgdaPostulate} {HTML}{000000}
|
|
||||||
\definecolor{AgdaPrimitive} {HTML}{000000}
|
|
||||||
\definecolor{AgdaRecord} {HTML}{000000}
|
|
||||||
\definecolor{AgdaArgument} {HTML}{000000}
|
|
||||||
|
|
||||||
% Other aspect colours.
|
|
||||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
|
||||||
\definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3}
|
|
||||||
\definecolor{AgdaUnsolvedConstraint}{HTML}{D3D3D3}
|
|
||||||
\definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}
|
|
||||||
\definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}
|
|
||||||
\definecolor{AgdaError} {HTML}{696969}
|
|
||||||
|
|
||||||
% Misc.
|
|
||||||
\definecolor{AgdaHole} {HTML}{BEBEBE}
|
|
||||||
|
|
||||||
% ----------------------------------
|
|
||||||
% Conor McBride's colour scheme.
|
|
||||||
}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{
|
|
||||||
|
|
||||||
% Aspect colours.
|
|
||||||
\definecolor{AgdaComment} {HTML}{B22222}
|
|
||||||
\definecolor{AgdaPragma} {HTML}{000000}
|
|
||||||
\definecolor{AgdaKeyword} {HTML}{000000}
|
|
||||||
\definecolor{AgdaString} {HTML}{000000}
|
|
||||||
\definecolor{AgdaNumber} {HTML}{000000}
|
|
||||||
\definecolor{AgdaSymbol} {HTML}{000000}
|
|
||||||
\definecolor{AgdaPrimitiveType}{HTML}{0000CD}
|
|
||||||
|
|
||||||
% NameKind colours.
|
|
||||||
\definecolor{AgdaBound} {HTML}{A020F0}
|
|
||||||
\definecolor{AgdaGeneralizable} {HTML}{A020F0}
|
|
||||||
\definecolor{AgdaInductiveConstructor} {HTML}{8B0000}
|
|
||||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}
|
|
||||||
\definecolor{AgdaDatatype} {HTML}{0000CD}
|
|
||||||
\definecolor{AgdaField} {HTML}{8B0000}
|
|
||||||
\definecolor{AgdaFunction} {HTML}{006400}
|
|
||||||
\definecolor{AgdaMacro} {HTML}{006400}
|
|
||||||
\definecolor{AgdaModule} {HTML}{006400}
|
|
||||||
\definecolor{AgdaPostulate} {HTML}{006400}
|
|
||||||
\definecolor{AgdaPrimitive} {HTML}{006400}
|
|
||||||
\definecolor{AgdaRecord} {HTML}{0000CD}
|
|
||||||
\definecolor{AgdaArgument} {HTML}{404040}
|
|
||||||
|
|
||||||
% Other aspect colours.
|
|
||||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
|
||||||
\definecolor{AgdaUnsolvedMeta} {HTML}{FFD700}
|
|
||||||
\definecolor{AgdaUnsolvedConstraint}{HTML}{FFD700}
|
|
||||||
\definecolor{AgdaTerminationProblem}{HTML}{FF0000}
|
|
||||||
\definecolor{AgdaIncompletePattern} {HTML}{A020F0}
|
|
||||||
\definecolor{AgdaError} {HTML}{F4A460}
|
|
||||||
|
|
||||||
% Misc.
|
|
||||||
\definecolor{AgdaHole} {HTML}{9DFF9D}
|
|
||||||
|
|
||||||
% ----------------------------------
|
|
||||||
% The standard colour scheme.
|
|
||||||
}{
|
|
||||||
% Aspect colours.
|
|
||||||
\definecolor{AgdaComment} {HTML}{B22222}
|
|
||||||
\definecolor{AgdaPragma} {HTML}{000000}
|
|
||||||
\definecolor{AgdaKeyword} {HTML}{CD6600}
|
|
||||||
\definecolor{AgdaString} {HTML}{B22222}
|
|
||||||
\definecolor{AgdaNumber} {HTML}{A020F0}
|
|
||||||
\definecolor{AgdaSymbol} {HTML}{404040}
|
|
||||||
\definecolor{AgdaPrimitiveType}{HTML}{0000CD}
|
|
||||||
|
|
||||||
% NameKind colours.
|
|
||||||
\definecolor{AgdaBound} {HTML}{000000}
|
|
||||||
\definecolor{AgdaGeneralizable} {HTML}{000000}
|
|
||||||
\definecolor{AgdaInductiveConstructor} {HTML}{008B00}
|
|
||||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}
|
|
||||||
\definecolor{AgdaDatatype} {HTML}{0000CD}
|
|
||||||
\definecolor{AgdaField} {HTML}{EE1289}
|
|
||||||
\definecolor{AgdaFunction} {HTML}{0000CD}
|
|
||||||
\definecolor{AgdaMacro} {HTML}{458B74}
|
|
||||||
\definecolor{AgdaModule} {HTML}{A020F0}
|
|
||||||
\definecolor{AgdaPostulate} {HTML}{0000CD}
|
|
||||||
\definecolor{AgdaPrimitive} {HTML}{0000CD}
|
|
||||||
\definecolor{AgdaRecord} {HTML}{0000CD}
|
|
||||||
\definecolor{AgdaArgument} {HTML}{404040}
|
|
||||||
|
|
||||||
% Other aspect colours.
|
|
||||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
|
||||||
\definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00}
|
|
||||||
\definecolor{AgdaUnsolvedConstraint}{HTML}{FFFF00}
|
|
||||||
\definecolor{AgdaTerminationProblem}{HTML}{FFA07A}
|
|
||||||
\definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}
|
|
||||||
\definecolor{AgdaError} {HTML}{FF0000}
|
|
||||||
|
|
||||||
% Misc.
|
|
||||||
\definecolor{AgdaHole} {HTML}{9DFF9D}
|
|
||||||
}}
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% Commands.
|
|
||||||
|
|
||||||
\newcommand{\AgdaNoSpaceMath}[1]
|
|
||||||
{\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}
|
|
||||||
|
|
||||||
% Aspect commands.
|
|
||||||
\newcommand{\AgdaComment} [1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}}
|
|
||||||
\newcommand{\AgdaPragma} [1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaPragma}{#1}}}}
|
|
||||||
\newcommand{\AgdaKeyword} [1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}}
|
|
||||||
\newcommand{\AgdaString} [1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}}
|
|
||||||
\newcommand{\AgdaNumber} [1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}}
|
|
||||||
\newcommand{\AgdaSymbol} [1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}}
|
|
||||||
\newcommand{\AgdaPrimitiveType}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}}
|
|
||||||
% Note that, in code generated by the LaTeX backend, \AgdaOperator is
|
|
||||||
% always applied to a NameKind command.
|
|
||||||
\newcommand{\AgdaOperator} [1]{#1}
|
|
||||||
|
|
||||||
% NameKind commands.
|
|
||||||
|
|
||||||
% The user can control the typesetting of (certain) individual tokens
|
|
||||||
% by redefining the following command. The first argument is the token
|
|
||||||
% and the second argument the thing to be typeset (sometimes just the
|
|
||||||
% token, sometimes \AgdaLink{<the token>}). Example:
|
|
||||||
%
|
|
||||||
% \usepackage{ifthen}
|
|
||||||
%
|
|
||||||
% % Insert extra space before some tokens.
|
|
||||||
% \DeclareRobustCommand{\AgdaFormat}[2]{%
|
|
||||||
% \ifthenelse{
|
|
||||||
% \equal{#1}{≡⟨} \OR
|
|
||||||
% \equal{#1}{≡⟨⟩} \OR
|
|
||||||
% \equal{#1}{∎}
|
|
||||||
% }{\ }{}#2}
|
|
||||||
%
|
|
||||||
% Note the use of \DeclareRobustCommand.
|
|
||||||
|
|
||||||
\newcommand{\AgdaFormat}[2]{#2}
|
|
||||||
|
|
||||||
\newcommand{\AgdaBound}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}}
|
|
||||||
\newcommand{\AgdaGeneralizable}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaGeneralizable}{\AgdaFormat{#1}{#1}}}}}
|
|
||||||
\newcommand{\AgdaInductiveConstructor}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaCoinductiveConstructor}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaDatatype}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaField}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaFunction}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaMacro}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaModule}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaPostulate}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaPrimitive}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}}
|
|
||||||
\newcommand{\AgdaRecord}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
|
||||||
\newcommand{\AgdaArgument}[1]
|
|
||||||
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\AgdaFormat{#1}{#1}}}}}
|
|
||||||
|
|
||||||
% Other aspect commands.
|
|
||||||
\newcommand{\AgdaFixityOp} [1]{\AgdaNoSpaceMath{$#1$}}
|
|
||||||
\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}}
|
|
||||||
\newcommand{\AgdaUnsolvedMeta} [1]
|
|
||||||
{\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}
|
|
||||||
\newcommand{\AgdaUnsolvedConstraint}[1]
|
|
||||||
{\AgdaFontStyle{\colorbox{AgdaUnsolvedConstraint}{#1}}}
|
|
||||||
\newcommand{\AgdaTerminationProblem}[1]
|
|
||||||
{\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}
|
|
||||||
\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}
|
|
||||||
\newcommand{\AgdaError} [1]
|
|
||||||
{\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}}
|
|
||||||
\newcommand{\AgdaCatchallClause} [1]{#1} % feel free to change this
|
|
||||||
|
|
||||||
% Used to hide code from LaTeX.
|
|
||||||
%
|
|
||||||
% Note that this macro has been deprecated in favour of giving the
|
|
||||||
% hide argument to the code environment.
|
|
||||||
\long\def\AgdaHide#1{\ignorespaces}
|
|
||||||
|
|
||||||
% Misc.
|
|
||||||
\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
|
|
||||||
|
|
||||||
% ----------------------------------------------------------------------
|
|
||||||
% The code environment.
|
|
||||||
|
|
||||||
\newcommand{\AgdaCodeStyle}{}
|
|
||||||
% \newcommand{\AgdaCodeStyle}{\tiny}
|
|
||||||
|
|
||||||
\ifdefined\mathindent
|
|
||||||
{}
|
|
||||||
\else
|
|
||||||
\newdimen\mathindent\mathindent\leftmargini
|
|
||||||
\fi
|
|
||||||
|
|
||||||
% Adds the given amount of vertical space and starts a new line.
|
|
||||||
%
|
|
||||||
% The implementation comes from lhs2TeX's polycode.fmt, written by
|
|
||||||
% Andres Löh.
|
|
||||||
\newcommand{\Agda@NewlineWithVerticalSpace}[1]{%
|
|
||||||
{\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}
|
|
||||||
|
|
||||||
% Should there be space around code?
|
|
||||||
\newboolean{Agda@SpaceAroundCode}
|
|
||||||
|
|
||||||
% Use this command to avoid extra space around code blocks.
|
|
||||||
\newcommand{\AgdaNoSpaceAroundCode}{%
|
|
||||||
\setboolean{Agda@SpaceAroundCode}{false}}
|
|
||||||
|
|
||||||
% Use this command to include extra space around code blocks.
|
|
||||||
\newcommand{\AgdaSpaceAroundCode}{%
|
|
||||||
\setboolean{Agda@SpaceAroundCode}{true}}
|
|
||||||
|
|
||||||
% By default space is inserted around code blocks.
|
|
||||||
\AgdaSpaceAroundCode{}
|
|
||||||
|
|
||||||
% Sometimes one might want to break up a code block into multiple
|
|
||||||
% pieces, but keep code in different blocks aligned with respect to
|
|
||||||
% each other. Then one can use the AgdaAlign environment. Example
|
|
||||||
% usage:
|
|
||||||
%
|
|
||||||
% \begin{AgdaAlign}
|
|
||||||
% \begin{code}
|
|
||||||
% code
|
|
||||||
% code (more code)
|
|
||||||
% \end{code}
|
|
||||||
% Explanation...
|
|
||||||
% \begin{code}
|
|
||||||
% aligned with "code"
|
|
||||||
% code (aligned with (more code))
|
|
||||||
% \end{code}
|
|
||||||
% \end{AgdaAlign}
|
|
||||||
%
|
|
||||||
% Note that AgdaAlign environments should not be nested.
|
|
||||||
%
|
|
||||||
% Sometimes one might also want to hide code in the middle of a code
|
|
||||||
% block. This can be accomplished in the following way:
|
|
||||||
%
|
|
||||||
% \begin{AgdaAlign}
|
|
||||||
% \begin{code}
|
|
||||||
% visible
|
|
||||||
% \end{code}
|
|
||||||
% \begin{code}[hide]
|
|
||||||
% hidden
|
|
||||||
% \end{code}
|
|
||||||
% \begin{code}
|
|
||||||
% visible
|
|
||||||
% \end{code}
|
|
||||||
% \end{AgdaAlign}
|
|
||||||
%
|
|
||||||
% However, the result may be ugly: extra space is perhaps inserted
|
|
||||||
% around the code blocks.
|
|
||||||
%
|
|
||||||
% The AgdaSuppressSpace environment ensures that extra space is only
|
|
||||||
% inserted before the first code block, and after the last one (but
|
|
||||||
% not if \AgdaNoSpaceAroundCode{} is used). Example usage:
|
|
||||||
%
|
|
||||||
% \begin{AgdaAlign}
|
|
||||||
% \begin{code}
|
|
||||||
% code
|
|
||||||
% more code
|
|
||||||
% \end{code}
|
|
||||||
% Explanation...
|
|
||||||
% \begin{AgdaSuppressSpace}
|
|
||||||
% \begin{code}
|
|
||||||
% aligned with "code"
|
|
||||||
% aligned with "more code"
|
|
||||||
% \end{code}
|
|
||||||
% \begin{code}[hide]
|
|
||||||
% hidden code
|
|
||||||
% \end{code}
|
|
||||||
% \begin{code}
|
|
||||||
% also aligned with "more code"
|
|
||||||
% \end{code}
|
|
||||||
% \end{AgdaSuppressSpace}
|
|
||||||
% \end{AgdaAlign}
|
|
||||||
%
|
|
||||||
% Note that AgdaSuppressSpace environments should not be nested.
|
|
||||||
%
|
|
||||||
% There is also a combined environment, AgdaMultiCode, that combines
|
|
||||||
% the effects of AgdaAlign and AgdaSuppressSpace.
|
|
||||||
|
|
||||||
% The number of the current/next code block (excluding hidden ones).
|
|
||||||
\newcounter{Agda@Current}
|
|
||||||
\setcounter{Agda@Current}{0}
|
|
||||||
|
|
||||||
% The number of the previous code block (excluding hidden ones), used
|
|
||||||
% locally in \Agda@SuppressEnd.
|
|
||||||
\newcounter{Agda@Previous}
|
|
||||||
|
|
||||||
% Is AgdaAlign active?
|
|
||||||
\newboolean{Agda@Align}
|
|
||||||
\setboolean{Agda@Align}{false}
|
|
||||||
|
|
||||||
% The number of the first code block (if any) in a given AgdaAlign
|
|
||||||
% environment.
|
|
||||||
\newcounter{Agda@AlignStart}
|
|
||||||
|
|
||||||
\newcommand{\Agda@AlignStart}{%
|
|
||||||
\ifthenelse{\boolean{Agda@Align}}{%
|
|
||||||
\PackageError{agda}{Nested AgdaAlign environments}{%
|
|
||||||
AgdaAlign and AgdaMultiCode environments must not be
|
|
||||||
nested.}}{%
|
|
||||||
\setboolean{Agda@Align}{true}%
|
|
||||||
\setcounter{Agda@AlignStart}{\value{Agda@Current}}}}
|
|
||||||
|
|
||||||
\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}}
|
|
||||||
|
|
||||||
\newenvironment{AgdaAlign}{%
|
|
||||||
\Agda@AlignStart{}}{%
|
|
||||||
\Agda@AlignEnd{}%
|
|
||||||
\ignorespacesafterend}
|
|
||||||
|
|
||||||
% Is AgdaSuppressSpace active?
|
|
||||||
\newboolean{Agda@Suppress}
|
|
||||||
\setboolean{Agda@Suppress}{false}
|
|
||||||
|
|
||||||
% The number of the first code block (if any) in a given
|
|
||||||
% AgdaSuppressSpace environment.
|
|
||||||
\newcounter{Agda@SuppressStart}
|
|
||||||
|
|
||||||
% Does a "do not suppress space after" label exist for the current
|
|
||||||
% code block? (This boolean is used locally in the code environment's
|
|
||||||
% implementation.)
|
|
||||||
\newboolean{Agda@DoNotSuppressSpaceAfter}
|
|
||||||
|
|
||||||
\newcommand{\Agda@SuppressStart}{%
|
|
||||||
\ifthenelse{\boolean{Agda@Suppress}}{%
|
|
||||||
\PackageError{agda}{Nested AgdaSuppressSpace environments}{%
|
|
||||||
AgdaSuppressSpace and AgdaMultiCode environments must not be
|
|
||||||
nested.}}{%
|
|
||||||
\setboolean{Agda@Suppress}{true}%
|
|
||||||
\setcounter{Agda@SuppressStart}{\value{Agda@Current}}}}
|
|
||||||
|
|
||||||
% Marks the given code block as one that space should not be
|
|
||||||
% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are
|
|
||||||
% both active).
|
|
||||||
\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{%
|
|
||||||
% The use of labels is intended to ensure that LaTeX will provide a
|
|
||||||
% warning if the document needs to be recompiled.
|
|
||||||
\label{Agda@DoNotSuppressSpaceAfter@#1}}
|
|
||||||
|
|
||||||
\newcommand{\Agda@SuppressEnd}{%
|
|
||||||
\ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{%
|
|
||||||
% Mark the previous code block in the .aux file.
|
|
||||||
\setcounter{Agda@Previous}{\theAgda@Current-1}%
|
|
||||||
\immediate\write\@auxout{%
|
|
||||||
\noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}%
|
|
||||||
\setboolean{Agda@Suppress}{false}}
|
|
||||||
|
|
||||||
\newenvironment{AgdaSuppressSpace}{%
|
|
||||||
\Agda@SuppressStart{}}{%
|
|
||||||
\Agda@SuppressEnd{}%
|
|
||||||
\ignorespacesafterend}
|
|
||||||
|
|
||||||
\newenvironment{AgdaMultiCode}{%
|
|
||||||
\Agda@AlignStart{}%
|
|
||||||
\Agda@SuppressStart{}}{%
|
|
||||||
\Agda@SuppressEnd{}%
|
|
||||||
\Agda@AlignEnd{}%
|
|
||||||
\ignorespacesafterend}
|
|
||||||
|
|
||||||
% Vertical space used for empty lines. By default \abovedisplayskip.
|
|
||||||
\newlength{\AgdaEmptySkip}
|
|
||||||
\setlength{\AgdaEmptySkip}{\abovedisplayskip}
|
|
||||||
|
|
||||||
% Extra space to be inserted for empty lines (the difference between
|
|
||||||
% \AgdaEmptySkip and \baselineskip). Used internally.
|
|
||||||
\newlength{\AgdaEmptyExtraSkip}
|
|
||||||
|
|
||||||
% Counter used for code numbers.
|
|
||||||
\newcounter{AgdaCodeNumber}
|
|
||||||
% Formats a code number.
|
|
||||||
\newcommand{\AgdaFormatCodeNumber}[1]{(#1)}
|
|
||||||
|
|
||||||
% A boolean used to handle the option number.
|
|
||||||
\newboolean{Agda@Number}
|
|
||||||
\setboolean{Agda@Number}{false}
|
|
||||||
|
|
||||||
% A boolean used to handle the option inline*. (For some reason the
|
|
||||||
% approach used for hide and inline does not work for inline*.)
|
|
||||||
\newboolean{Agda@InlineStar}
|
|
||||||
\setboolean{Agda@InlineStar}{false}
|
|
||||||
|
|
||||||
% Keys used by the code environment.
|
|
||||||
\define@boolkey[Agda]{code}{hide}[true]{}
|
|
||||||
\define@boolkey[Agda]{code}{inline}[true]{}
|
|
||||||
\define@boolkey[Agda]{code}{inline*}[true]{%
|
|
||||||
\setboolean{Agda@InlineStar}{true}}
|
|
||||||
\define@key[Agda]{code}{number}[]{%
|
|
||||||
\ifthenelse{\boolean{Agda@Number}}{}{%
|
|
||||||
\setboolean{Agda@Number}{true}%
|
|
||||||
% Increase the counter if this has not already been done.
|
|
||||||
\refstepcounter{AgdaCodeNumber}}%
|
|
||||||
% If the label is non-empty, set it. Note that it is possible to
|
|
||||||
% give several labels for a single code listing.
|
|
||||||
\ifthenelse{\equal{#1}{}}{}{\label{#1}}}
|
|
||||||
|
|
||||||
% The code environment.
|
|
||||||
%
|
|
||||||
% Options:
|
|
||||||
%
|
|
||||||
% * hide: The code is hidden. Other options are ignored.
|
|
||||||
%
|
|
||||||
% * number: Give the code an equation number.
|
|
||||||
%
|
|
||||||
% * number=l: Give the code an equation number and the label l. It is
|
|
||||||
% possible to use this option several times with different labels.
|
|
||||||
%
|
|
||||||
% * inline/inline*: The code is inlined. In this case most of the
|
|
||||||
% discussion above does not apply, alignment is not respected, and so
|
|
||||||
% on. It is recommended to only use this option for a single line of
|
|
||||||
% code, and to not use two consecutive spaces in this piece of code.
|
|
||||||
%
|
|
||||||
% Note that this environment ignores spaces after its end. If a space
|
|
||||||
% (\AgdaSpace{}) should be inserted after the inline code, use
|
|
||||||
% inline*, otherwise use inline.
|
|
||||||
%
|
|
||||||
% When this option is used number is ignored.
|
|
||||||
%
|
|
||||||
% The implementation is based on plainhscode in lhs2TeX's
|
|
||||||
% polycode.fmt, written by Andres Löh.
|
|
||||||
\NewEnviron{code}[1][]{%
|
|
||||||
% Process the options. Complain about unknown options.
|
|
||||||
\setkeys[Agda]{code}[number]{#1}%
|
|
||||||
\ifAgda@code@hide%
|
|
||||||
% Hide the code.
|
|
||||||
\else%
|
|
||||||
\ifAgda@code@inline%
|
|
||||||
% Inline code.
|
|
||||||
%
|
|
||||||
% Make the polytable primitives emitted by the LaTeX backend
|
|
||||||
% do nothing.
|
|
||||||
\DeclareDocumentCommand{\>}{O{}O{}}{}%
|
|
||||||
\DeclareDocumentCommand{\<}{O{}}{}%
|
|
||||||
\AgdaCodeStyle\BODY%
|
|
||||||
\else%
|
|
||||||
\ifthenelse{\boolean{Agda@InlineStar}}{%
|
|
||||||
% Inline code with space at the end.
|
|
||||||
%
|
|
||||||
\DeclareDocumentCommand{\>}{O{}O{}}{}%
|
|
||||||
\DeclareDocumentCommand{\<}{O{}}{}%
|
|
||||||
\AgdaCodeStyle\BODY\AgdaSpace{}}{%
|
|
||||||
%
|
|
||||||
% Displayed code.
|
|
||||||
%
|
|
||||||
% Conditionally emit space before the code block. Unconditionally
|
|
||||||
% switch to a new line.
|
|
||||||
\ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
|
|
||||||
\(\not \boolean{Agda@Suppress} \or%
|
|
||||||
\value{Agda@SuppressStart} = \value{Agda@Current}\)}{%
|
|
||||||
\Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{%
|
|
||||||
\Agda@NewlineWithVerticalSpace{0pt}}%
|
|
||||||
%
|
|
||||||
% Check if numbers have been requested. If they have, then a side
|
|
||||||
% effect of this call is that Agda@Number is set to true, the code
|
|
||||||
% number counter is increased, and the label (if any) is set.
|
|
||||||
\setkeys[Agda]{code}[hide,inline,inline*]{#1}%
|
|
||||||
\ifthenelse{\boolean{Agda@Number}}{%
|
|
||||||
% Equation numbers have been requested. Use a minipage, so that
|
|
||||||
% there is room for the code number to the right, and the code
|
|
||||||
% number becomes centered vertically.
|
|
||||||
\begin{minipage}{%
|
|
||||||
\linewidth-%
|
|
||||||
\widthof{%
|
|
||||||
\AgdaSpace{}%
|
|
||||||
\AgdaFormatCodeNumber{\theAgdaCodeNumber}}}}{}%
|
|
||||||
%
|
|
||||||
% Indent the entire code block.
|
|
||||||
\advance\leftskip\mathindent%
|
|
||||||
%
|
|
||||||
% The code's style can be customised.
|
|
||||||
\AgdaCodeStyle%
|
|
||||||
%
|
|
||||||
% Used to control the height of empty lines.
|
|
||||||
\setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}%
|
|
||||||
%
|
|
||||||
% The environment used to handle indentation (of individual lines)
|
|
||||||
% and alignment.
|
|
||||||
\begin{pboxed}%
|
|
||||||
%
|
|
||||||
% Conditionally preserve alignment between code blocks.
|
|
||||||
\ifthenelse{\boolean{Agda@Align}}{%
|
|
||||||
\ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{%
|
|
||||||
\savecolumns}{%
|
|
||||||
\restorecolumns}}{}%
|
|
||||||
%
|
|
||||||
% The code.
|
|
||||||
\BODY%
|
|
||||||
\end{pboxed}%
|
|
||||||
%
|
|
||||||
\ifthenelse{\boolean{Agda@Number}}{%
|
|
||||||
% Equation numbers have been requested.
|
|
||||||
\end{minipage}%
|
|
||||||
% Insert the code number to the right.
|
|
||||||
\hfill \AgdaFormatCodeNumber{\theAgdaCodeNumber}}{}%
|
|
||||||
%
|
|
||||||
% Does the label Agda@DoNotSuppressAfter@<current code block
|
|
||||||
% number> exist?
|
|
||||||
\ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{%
|
|
||||||
\setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{%
|
|
||||||
\setboolean{Agda@DoNotSuppressSpaceAfter}{false}}%
|
|
||||||
%
|
|
||||||
% Conditionally emit space after the code block. Unconditionally
|
|
||||||
% switch to a new line.
|
|
||||||
\ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
|
|
||||||
\(\not \boolean{Agda@Suppress} \or%
|
|
||||||
\boolean{Agda@DoNotSuppressSpaceAfter}\)}{%
|
|
||||||
\Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{%
|
|
||||||
\Agda@NewlineWithVerticalSpace{0pt}}%
|
|
||||||
%
|
|
||||||
% Step the code block counter, but only for non-hidden code.
|
|
||||||
\stepcounter{Agda@Current}}%
|
|
||||||
\fi%
|
|
||||||
\fi%
|
|
||||||
% Reset Agda@Number and Agda@InlineStar.
|
|
||||||
\setboolean{Agda@Number}{false}%
|
|
||||||
\setboolean{Agda@InlineStar}{false}}
|
|
||||||
|
|
||||||
% Space inserted after tokens.
|
|
||||||
\newcommand{\AgdaSpace}{ }
|
|
||||||
|
|
||||||
% Space inserted to indent something.
|
|
||||||
\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$}
|
|
||||||
|
|
||||||
% Default column for polytable.
|
|
||||||
\defaultcolumn{@{}l@{\AgdaSpace{}}}
|
|
||||||
|
|
||||||
% \AgdaIndent expects a non-negative integer as its only argument.
|
|
||||||
% This integer should be the distance, in code blocks, to the thing
|
|
||||||
% relative to which the text is indented.
|
|
||||||
%
|
|
||||||
% The default implementation only indents if the thing that the text
|
|
||||||
% is indented relative to exists in the same code block or is wrapped
|
|
||||||
% in the same AgdaAlign or AgdaMultiCode environment.
|
|
||||||
\newcommand{\AgdaIndent}[1]{%
|
|
||||||
\ifthenelse{#1 = 0
|
|
||||||
\or
|
|
||||||
\( \boolean{Agda@Align}
|
|
||||||
\and
|
|
||||||
\cnttest{\value{Agda@Current} - #1}{>=}{
|
|
||||||
\value{Agda@AlignStart}}
|
|
||||||
\)}{\AgdaIndentSpace{}}{}}
|
|
||||||
|
|
||||||
% Underscores are typeset using \AgdaUnderscore{}.
|
|
||||||
\newcommand{\AgdaUnderscore}{\_}
|
|
||||||
|
|
||||||
\endinput
|
|
||||||
|
|
@ -1,7 +0,0 @@
|
||||||
-- tested on pandoc 2.2.3.2
|
|
||||||
-- from agda doc:
|
|
||||||
-- Code blocks start with ``` or ```agda on its own line, and end with ```, also on its own line
|
|
||||||
function CodeBlock(elem)
|
|
||||||
return pandoc.RawBlock('tex', '\\begin{myDisplay}\n' .. elem.text .. '\n\\end{myDisplay}')
|
|
||||||
end
|
|
||||||
|
|
||||||
|
|
@ -1,11 +0,0 @@
|
||||||
-- tested on pandoc 2.2.3.2
|
|
||||||
-- from agda doc:
|
|
||||||
-- Code blocks start with ``` or ```agda on its own line, and end with ```, also on its own line
|
|
||||||
function CodeBlock(elem)
|
|
||||||
if #(elem.classes)==0 or elem.classes[1]=='agda' then
|
|
||||||
return pandoc.RawBlock('tex', '\\begin{fence}\n\\begin{code}\n' .. elem.text .. '\n\\end{code}\n\\end{fence}')
|
|
||||||
else
|
|
||||||
return pandoc.RawBlock('tex', '\\begin{myDisplay}\n' .. elem.text .. '\n\\end{myDisplay}')
|
|
||||||
end
|
|
||||||
end
|
|
||||||
|
|
||||||
|
|
@ -1,5 +0,0 @@
|
||||||
function Link(el)
|
|
||||||
if el.content[1].t == "Image" then
|
|
||||||
return pandoc.RawInline('markdown','')
|
|
||||||
end
|
|
||||||
end
|
|
||||||
12
pdf/lua/remove-badges.lua
Normal file
12
pdf/lua/remove-badges.lua
Normal file
|
|
@ -0,0 +1,12 @@
|
||||||
|
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.match(ln.content[1].src, 'https://img%.shields%.io/badge/') then
|
||||||
|
return pandoc.Null()
|
||||||
|
end
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
return {
|
||||||
|
{ Link = remove_badges }
|
||||||
|
}
|
||||||
|
|
@ -3,8 +3,10 @@
|
||||||
-- Case 1:
|
-- Case 1:
|
||||||
-- /title/: "Some Title"
|
-- /title/: "Some Title"
|
||||||
-- /permalink/: /Title/ -> # Some Title {#Title}
|
-- /permalink/: /Title/ -> # Some Title {#Title}
|
||||||
|
--
|
||||||
-- Case 2:
|
-- Case 2:
|
||||||
-- ## Subsection Title {name=more-stuff} -> ## Subsection Title {#Title-more-stuff}
|
-- ## Subsection Title {name=more-stuff} -> ## Subsection Title {#Title-more-stuff}
|
||||||
|
--
|
||||||
|
|
||||||
local identifier = nil
|
local identifier = nil
|
||||||
local title = nil
|
local title = nil
|
||||||
|
|
@ -13,10 +15,9 @@ function get_identifier(meta)
|
||||||
-- get title identifier from permalinks
|
-- get title identifier from permalinks
|
||||||
for k,v in pairs(meta) do
|
for k,v in pairs(meta) do
|
||||||
if k == "title" then
|
if k == "title" then
|
||||||
title = {table.unpack(v)}
|
title = {table.unpack(v)}
|
||||||
end
|
end
|
||||||
if k == "permalink" then
|
if k == "permalink" then
|
||||||
-- print(k,type(v[1].c))
|
|
||||||
-- set lower case permalink as identifier
|
-- set lower case permalink as identifier
|
||||||
identifier = v[1].c:match("^/(%w+)/$")
|
identifier = v[1].c:match("^/(%w+)/$")
|
||||||
end
|
end
|
||||||
|
|
@ -25,25 +26,25 @@ end
|
||||||
|
|
||||||
function insert_title(doc)
|
function insert_title(doc)
|
||||||
-- insert title in front of the blocks
|
-- insert title in front of the blocks
|
||||||
-- print(doc.blocks)
|
if title then
|
||||||
header = pandoc.Header(1,title)
|
header = pandoc.Header(1,title)
|
||||||
header.identifier = identifier
|
header.identifier = identifier
|
||||||
-- print("header:" ,header.content)
|
table.insert(doc.blocks,1,header)
|
||||||
table.insert(doc.blocks,1,header)
|
end
|
||||||
return doc
|
return doc
|
||||||
end
|
end
|
||||||
|
|
||||||
function change_identifier(elem)
|
function change_identifier(elem)
|
||||||
-- change header identifier based on metadata
|
-- change header identifier based on metadata
|
||||||
|
|
||||||
local name = elem.attributes["name"]
|
local name = elem.attributes["name"]
|
||||||
if elem.t == "Header" and name then
|
if elem.t == "Header" and name then
|
||||||
-- can get labels
|
|
||||||
-- print(name, elem.identifier)
|
|
||||||
elem.identifier = identifier .. "-" .. name
|
elem.identifier = identifier .. "-" .. name
|
||||||
-- print(elem.identifier)
|
|
||||||
end
|
end
|
||||||
return elem
|
return elem
|
||||||
end
|
end
|
||||||
|
|
||||||
return {{Meta=get_identifier}, {Header=change_identifier}, {Pandoc = insert_title}}
|
return {
|
||||||
|
{Meta = get_identifier},
|
||||||
|
{Header = change_identifier},
|
||||||
|
{Pandoc = insert_title}
|
||||||
|
}
|
||||||
49
pdf/lua/typeset-codeblocks.lua
Normal file
49
pdf/lua/typeset-codeblocks.lua
Normal file
|
|
@ -0,0 +1,49 @@
|
||||||
|
local function typeset_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
|
||||||
|
|
||||||
|
-- Set of unchecked files, where the names of unchecked files are stored in the table keys.
|
||||||
|
local UNCHECKED_FILES = nil
|
||||||
|
|
||||||
|
-- Return whether the current file is checked by Agda, given by the UNCHECKED_FILES environment variable.
|
||||||
|
function is_checked()
|
||||||
|
|
||||||
|
-- Initialise the table.
|
||||||
|
if UNCHECKED_FILES == nil then
|
||||||
|
UNCHECKED_FILES = {}
|
||||||
|
for unchecked_file in string.gmatch(pandoc.system.environment().UNCHECKED_FILES, "([^ ]+)") do
|
||||||
|
UNCHECKED_FILES[unchecked_file] = true
|
||||||
|
end
|
||||||
|
end
|
||||||
|
|
||||||
|
-- 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
|
||||||
|
|
||||||
|
return {
|
||||||
|
{ CodeBlock = typeset_codeblock }
|
||||||
|
}
|
||||||
|
|
@ -1,171 +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,fancyvrb,xcolor,tikz}
|
|
||||||
\tcbuselibrary{skins,breakable}
|
|
||||||
\usepackage{setspace}
|
|
||||||
|
|
||||||
% wrap long texttt lines
|
|
||||||
\sloppy
|
|
||||||
|
|
||||||
% disable section numbering
|
|
||||||
\setcounter{secnumdepth}{0}
|
|
||||||
|
|
||||||
|
|
||||||
% 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{bgcolor}{HTML}{EEEEFF}
|
|
||||||
\let\oldtexttt\texttt
|
|
||||||
|
|
||||||
\renewcommand{\texttt}[1]{
|
|
||||||
\colorbox{bgcolor}{\oldtexttt{#1}}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
% indent verbatim to be the same as agda code blocks
|
|
||||||
\DefineVerbatimEnvironment{verbatim}{Verbatim}{xleftmargin=0pt}
|
|
||||||
|
|
||||||
% environments for adding background to agdacodeblocks and displays
|
|
||||||
\newtcolorbox{fence}[1][]{
|
|
||||||
breakable,
|
|
||||||
colback=bgcolor,
|
|
||||||
spartan,
|
|
||||||
left=5pt,
|
|
||||||
boxrule=0pt,
|
|
||||||
frame hidden
|
|
||||||
}
|
|
||||||
\newenvironment{myDisplay}
|
|
||||||
{\VerbatimEnvironment
|
|
||||||
\begin{fence}
|
|
||||||
\begin{verbatim}
|
|
||||||
}
|
|
||||||
{\end{verbatim}
|
|
||||||
\end{fence}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
\usepackage{geometry}
|
|
||||||
\geometry{
|
|
||||||
a4paper,
|
|
||||||
total={170mm,257mm},
|
|
||||||
left=20mm,
|
|
||||||
top=20mm,
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
% Use special font families without TeX ligatures for Agda code. (This
|
|
||||||
% code is inspired by a comment by Enrico Gregorio/egreg:
|
|
||||||
% 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{}
|
|
||||||
|
|
||||||
\setlength{\parindent}{0em}
|
|
||||||
\setlength{\parskip}{1em}
|
|
||||||
|
|
||||||
|
|
||||||
% adjust spacing after toc numbering
|
|
||||||
\usepackage{tocloft}
|
|
||||||
\setlength\cftchapnumwidth{4em}
|
|
||||||
|
|
||||||
% style links with colors instead of boxes
|
|
||||||
% https://tex.stackexchange.com/questions/823/remove-ugly-borders-around-clickable-cross-references-and-hyperlinks
|
|
||||||
\hypersetup{
|
|
||||||
colorlinks,
|
|
||||||
linkcolor={red!50!black},
|
|
||||||
citecolor={blue!50!black},
|
|
||||||
urlcolor={blue!80!black}
|
|
||||||
}
|
|
||||||
|
|
||||||
\begin{document}
|
|
||||||
|
|
||||||
% adjust indentation of agda codeblocks
|
|
||||||
\setlength{\mathindent}{0pt}
|
|
||||||
|
|
||||||
% Stack Overflow: (error) \tightlist (converting .md file into .pdf using pandoc)
|
|
||||||
% https://tex.stackexchange.com/questions/257418/error-tightlist-converting-md-file-into-pdf-using-pandoc/408474
|
|
||||||
\providecommand{\tightlist}{%
|
|
||||||
\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
|
|
||||||
|
|
||||||
% https://ctan.org/pkg/titlepages
|
|
||||||
% https://latex.org/forum/viewtopic.php?t=2843
|
|
||||||
\newlength{\drop}
|
|
||||||
\newcommand*{\titleAM}{\begingroup% Ancient Mariner, AW p. 151
|
|
||||||
\setlength{\drop}{0.12\textheight}
|
|
||||||
\centering
|
|
||||||
\vspace*{\drop}
|
|
||||||
{\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip]
|
|
||||||
\vspace*{\drop}
|
|
||||||
{\Huge Programming Language Foundations}\\[\baselineskip]
|
|
||||||
{\Huge in}\\[\baselineskip]
|
|
||||||
{\Huge Agda}\\[\drop]
|
|
||||||
% {\small\scshape the publisher}\par
|
|
||||||
\vfill
|
|
||||||
{\Large \scshape 2021}\par
|
|
||||||
\null\endgroup}
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
\begin{titlepage}
|
|
||||||
\titleAM
|
|
||||||
\end{titlepage}
|
|
||||||
\frontmatter
|
|
||||||
\setcounter{tocdepth}{0}
|
|
||||||
\tableofcontents
|
|
||||||
\setcounter{tocdepth}{1}
|
|
||||||
\input{ latex/plfa/frontmatter/dedication }
|
|
||||||
\input{ latex/plfa/frontmatter/preface }
|
|
||||||
\input{ latex/plfa/frontmatter/README }
|
|
||||||
|
|
||||||
\mainmatter
|
|
||||||
\part{Part 1: Logical Foundations}
|
|
||||||
\input{ latex/plfa/part1/Naturals }
|
|
||||||
\input{ latex/plfa/part1/Induction }
|
|
||||||
% \input{ latex/plfa/part1/Relations }
|
|
||||||
% \input{ latex/plfa/part1/Equality }
|
|
||||||
% \input{ latex/plfa/part1/Isomorphism }
|
|
||||||
% \input{ latex/plfa/part1/Connectives }
|
|
||||||
% \input{ latex/plfa/part1/Negation }
|
|
||||||
% \input{ latex/plfa/part1/Quantifiers }
|
|
||||||
% \input{ latex/plfa/part1/Decidable }
|
|
||||||
% \input{ latex/plfa/part1/Lists }
|
|
||||||
\part{Part 2: Programming Language Foundations}
|
|
||||||
\input{ latex/plfa/part2/Lambda}
|
|
||||||
% \input{ latex/plfa/part2/Properties}
|
|
||||||
\input{ latex/plfa/part2/DeBruijn}
|
|
||||||
% \input{ latex/plfa/part2/More}
|
|
||||||
% \input{ latex/plfa/part2/Bisimulation }
|
|
||||||
% \input{ latex/plfa/part2/Inference }
|
|
||||||
% \input{ latex/plfa/part2/Untyped }
|
|
||||||
% \input{ latex/plfa/part2/Confluence }
|
|
||||||
% \input{ latex/plfa/part2/BigStep }
|
|
||||||
\part{ Part 3: Denotational Semantics }
|
|
||||||
\input{ latex/plfa/part3/Denotational }
|
|
||||||
% \input{ latex/plfa/part3/Compositional }
|
|
||||||
% \input{ latex/plfa/part3/Soundness }
|
|
||||||
% \input{ latex/plfa/part3/Adequacy }
|
|
||||||
% \input{ latex/plfa/part3/ContextualEquivalence }
|
|
||||||
|
|
||||||
% https://tex.stackexchange.com/questions/286431/putting-appendix-outside-the-last-part
|
|
||||||
\cleardoublepage
|
|
||||||
\phantomsection
|
|
||||||
\appendix
|
|
||||||
\addcontentsline{toc}{part}{Appendices}
|
|
||||||
% \input{ latex/plfa/part2/Substitution }
|
|
||||||
\input{ latex/plfa/backmatter/acknowledgements}
|
|
||||||
\input{ latex/plfa/backmatter/Fonts }
|
|
||||||
\end{document}
|
|
||||||
|
|
@ -1,3 +0,0 @@
|
||||||
name: plfa
|
|
||||||
depend: standard-library
|
|
||||||
include: lagda_tex
|
|
||||||
198
pdf/plfa.tex
198
pdf/plfa.tex
|
|
@ -1,4 +1,5 @@
|
||||||
\documentclass[10pt]{book}
|
\documentclass[10pt]{book}
|
||||||
|
|
||||||
\usepackage{hyperref}
|
\usepackage{hyperref}
|
||||||
\usepackage[links]{agda}
|
\usepackage[links]{agda}
|
||||||
\usepackage{fontspec}
|
\usepackage{fontspec}
|
||||||
|
|
@ -6,50 +7,54 @@
|
||||||
\setsansfont{DejaVu Sans}
|
\setsansfont{DejaVu Sans}
|
||||||
\setmonofont{[DejaVu-mononoki-Symbola-Droid.ttf]}
|
\setmonofont{[DejaVu-mononoki-Symbola-Droid.ttf]}
|
||||||
\usepackage{soul}
|
\usepackage{soul}
|
||||||
\usepackage{tcolorbox,fancyvrb,xcolor,tikz}
|
\usepackage[most]{tcolorbox}
|
||||||
\tcbuselibrary{skins,breakable}
|
\tcbuselibrary{skins,breakable}
|
||||||
|
\usepackage{listings}
|
||||||
|
\usepackage{xcolor}
|
||||||
|
\usepackage{tikz}
|
||||||
\usepackage{setspace}
|
\usepackage{setspace}
|
||||||
|
|
||||||
% wrap texttt lines
|
% Wrap texttt lines
|
||||||
\sloppy
|
\sloppy
|
||||||
|
|
||||||
% disable section numbering
|
% Disable section numbering
|
||||||
\setcounter{secnumdepth}{0}
|
\setcounter{secnumdepth}{0}
|
||||||
|
|
||||||
|
% Change background color for inline code in markdown files.
|
||||||
% change background color for inline code in
|
% The following code does not work well for long text as the
|
||||||
% markdown files. The following code does not work well for
|
% text will exceed the page boundary.
|
||||||
% long text as the text will exceed the page boundary
|
|
||||||
|
|
||||||
\definecolor{bgcolor}{HTML}{EEEEFF}
|
\definecolor{bgcolor}{HTML}{EEEEFF}
|
||||||
\let\oldtexttt\texttt
|
\let\oldtexttt\texttt%
|
||||||
|
\renewcommand{\texttt}[1]{\colorbox{bgcolor}{\oldtexttt{#1}}}
|
||||||
|
|
||||||
\renewcommand{\texttt}[1]{
|
% Indent verbatim to be the same as agda code blocks.
|
||||||
\colorbox{bgcolor}{\oldtexttt{#1}}
|
\lstdefinestyle{codeBlockStyle}{
|
||||||
}
|
basicstyle=\ttfamily,
|
||||||
|
numbers=none
|
||||||
|
}
|
||||||
% indent verbatim to be the same as agda code blocks
|
\newtcolorbox{agda}[1][]{
|
||||||
\DefineVerbatimEnvironment{verbatim}{Verbatim}{xleftmargin=0pt}
|
frame hidden,
|
||||||
|
|
||||||
% environments for adding background to agdacodeblocks and displays
|
|
||||||
\newtcolorbox{fence}[1][]{
|
|
||||||
breakable,
|
|
||||||
colback=bgcolor,
|
colback=bgcolor,
|
||||||
spartan,
|
spartan,
|
||||||
left=5pt,
|
left=5pt,
|
||||||
boxrule=0pt,
|
boxrule=0pt,
|
||||||
frame hidden
|
breakable,
|
||||||
|
}
|
||||||
|
\newtcblisting{pre}{
|
||||||
|
frame hidden,
|
||||||
|
colback=bgcolor,
|
||||||
|
spartan,
|
||||||
|
width=\textwidth,
|
||||||
|
listing only,
|
||||||
|
listing options={style=codeBlockStyle},
|
||||||
|
arc=0mm,
|
||||||
|
top=0mm,
|
||||||
|
bottom=0mm,
|
||||||
|
left=0mm,
|
||||||
|
right=0mm,
|
||||||
|
boxrule=0pt,
|
||||||
|
breakable,
|
||||||
}
|
}
|
||||||
\newenvironment{myDisplay}
|
|
||||||
{\VerbatimEnvironment
|
|
||||||
\begin{fence}
|
|
||||||
\begin{verbatim}
|
|
||||||
}
|
|
||||||
{\end{verbatim}
|
|
||||||
\end{fence}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
||||||
\usepackage{geometry}
|
\usepackage{geometry}
|
||||||
\geometry{
|
\geometry{
|
||||||
|
|
@ -57,16 +62,14 @@
|
||||||
total={170mm,257mm},
|
total={170mm,257mm},
|
||||||
left=20mm,
|
left=20mm,
|
||||||
top=20mm,
|
top=20mm,
|
||||||
}
|
}
|
||||||
|
|
||||||
|
% Use special font families without TeX ligatures for Agda code.
|
||||||
|
% Solution inspired by a comment by Enrico Gregorio:
|
||||||
% Use special font families without TeX ligatures for Agda code. (This
|
% https://tex.stackexchange.com/a/103078
|
||||||
% code is inspired by a comment by Enrico Gregorio/egreg:
|
\newfontfamily{\AgdaSerifFont}{DejaVu-Serif}
|
||||||
% https://tex.stackexchange.com/a/103078.)
|
\newfontfamily{\AgdaSansSerifFont}{DejaVu-Sans}
|
||||||
\newfontfamily{\AgdaSerifFont}{DejaVu Serif}
|
\newfontfamily{\AgdaTypewriterFont}{DejaVu-mononoki-Symbola-Droid}
|
||||||
\newfontfamily{\AgdaSansSerifFont}{DejaVu Sans}
|
|
||||||
\newfontfamily{\AgdaTypewriterFont}{DejaVu mononoki Symbola Droid}
|
|
||||||
\renewcommand{\AgdaFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
\renewcommand{\AgdaFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
||||||
\renewcommand{\AgdaKeywordFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
\renewcommand{\AgdaKeywordFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
||||||
\renewcommand{\AgdaStringFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
\renewcommand{\AgdaStringFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
|
||||||
|
|
@ -78,14 +81,13 @@
|
||||||
\setlength{\parindent}{0em}
|
\setlength{\parindent}{0em}
|
||||||
\setlength{\parskip}{1em}
|
\setlength{\parskip}{1em}
|
||||||
|
|
||||||
|
% Adjust spacing after toc numbering
|
||||||
% adjust spacing after toc numbering
|
|
||||||
\usepackage{tocloft}
|
\usepackage{tocloft}
|
||||||
\setlength\cftchapnumwidth{3em}
|
\setlength\cftchapnumwidth{3em}
|
||||||
\cftsetpnumwidth{4em}
|
\cftsetpnumwidth{4em}
|
||||||
|
|
||||||
% style links with colors instead of boxes
|
% Style links with colors instead of boxes:
|
||||||
% https://tex.stackexchange.com/questions/823/remove-ugly-borders-around-clickable-cross-references-and-hyperlinks
|
% https://tex.stackexchange.com/q/823
|
||||||
\hypersetup{
|
\hypersetup{
|
||||||
colorlinks,
|
colorlinks,
|
||||||
linkcolor={red!50!black},
|
linkcolor={red!50!black},
|
||||||
|
|
@ -95,79 +97,79 @@
|
||||||
|
|
||||||
\begin{document}
|
\begin{document}
|
||||||
|
|
||||||
% adjust indentation of agda codeblocks
|
% Adjust indentation of agda codeblocks
|
||||||
\setlength{\mathindent}{0pt}
|
\setlength{\mathindent}{0pt}
|
||||||
|
|
||||||
% Stack Overflow: (error) \tightlist (converting .md file into .pdf using pandoc)
|
% Provide \tightlist environment
|
||||||
% https://tex.stackexchange.com/questions/257418/error-tightlist-converting-md-file-into-pdf-using-pandoc/408474
|
% https://tex.stackexchange.com/q/257418
|
||||||
\providecommand{\tightlist}{%
|
\providecommand{\tightlist}{%
|
||||||
\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
|
\setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
|
||||||
|
|
||||||
% https://ctan.org/pkg/titlepages
|
% https://ctan.org/pkg/titlepages
|
||||||
% https://latex.org/forum/viewtopic.php?t=2843
|
% https://latex.org/forum/viewtopic.php?t=2843
|
||||||
\newlength{\drop}
|
|
||||||
\newcommand*{\titleAM}{\begingroup% Ancient Mariner, AW p. 151
|
|
||||||
\setlength{\drop}{0.12\textheight}
|
|
||||||
\centering
|
|
||||||
\vspace*{\drop}
|
|
||||||
{\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip]
|
|
||||||
\vspace*{\drop}
|
|
||||||
{\Huge Programming Language Foundations}\\[\baselineskip]
|
|
||||||
{\Huge in}\\[\baselineskip]
|
|
||||||
{\Huge Agda}\\[\drop]
|
|
||||||
% {\small\scshape the publisher}\par
|
|
||||||
\vfill
|
|
||||||
{\Large \scshape 2021}\par
|
|
||||||
\null\endgroup}
|
|
||||||
|
|
||||||
|
|
||||||
\begin{titlepage}
|
\begin{titlepage}
|
||||||
\titleAM
|
\newlength{\drop}
|
||||||
|
\setlength{\drop}{0.12\textheight}%
|
||||||
|
\centering%
|
||||||
|
\begingroup% Ancient Mariner, AW p. 151
|
||||||
|
\vspace*{\drop}%
|
||||||
|
{\large Philip Wadler, Wen Kokke, and Jeremy G. Siek}\\[\baselineskip]
|
||||||
|
{\Huge PROGRAMMING LANGUAGE FOUNDATIONS}\\[\baselineskip]
|
||||||
|
{\Large IN}\\[\baselineskip]
|
||||||
|
{\Huge Agda}\\[\drop]
|
||||||
|
\vfill%
|
||||||
|
{\small\scshape 2021}\par%
|
||||||
|
\null\endgroup
|
||||||
\end{titlepage}
|
\end{titlepage}
|
||||||
|
|
||||||
\frontmatter
|
\frontmatter
|
||||||
\setcounter{tocdepth}{0}
|
\setcounter{tocdepth}{0}
|
||||||
|
|
||||||
\tableofcontents
|
\tableofcontents
|
||||||
\setcounter{tocdepth}{1}
|
\setcounter{tocdepth}{1}
|
||||||
|
|
||||||
\input{ latex/plfa/frontmatter/dedication }
|
\input{plfa/frontmatter/dedication}
|
||||||
\input{ latex/plfa/frontmatter/preface }
|
\input{plfa/frontmatter/preface}
|
||||||
\input{ latex/plfa/frontmatter/README }
|
\input{plfa/frontmatter/README}
|
||||||
|
|
||||||
\mainmatter
|
\mainmatter
|
||||||
\part{Part 1: Logical Foundations}
|
\part{Part 1: Logical Foundations}
|
||||||
\input{ latex/plfa/part1/Naturals }
|
\input{plfa/part1/Naturals}
|
||||||
\input{ latex/plfa/part1/Induction }
|
\input{plfa/part1/Induction}
|
||||||
\input{ latex/plfa/part1/Relations }
|
\input{plfa/part1/Relations}
|
||||||
\input{ latex/plfa/part1/Equality }
|
\input{plfa/part1/Equality}
|
||||||
\input{ latex/plfa/part1/Isomorphism }
|
\input{plfa/part1/Isomorphism}
|
||||||
\input{ latex/plfa/part1/Connectives }
|
\input{plfa/part1/Connectives}
|
||||||
\input{ latex/plfa/part1/Negation }
|
\input{plfa/part1/Negation}
|
||||||
\input{ latex/plfa/part1/Quantifiers }
|
\input{plfa/part1/Quantifiers}
|
||||||
\input{ latex/plfa/part1/Decidable }
|
\input{plfa/part1/Decidable}
|
||||||
\input{ latex/plfa/part1/Lists }
|
\input{plfa/part1/Lists}
|
||||||
\part{Part 2: Programming Language Foundations}
|
|
||||||
\input{ latex/plfa/part2/Lambda}
|
\part{Part 2: Programming Language Foundations}
|
||||||
\input{ latex/plfa/part2/Properties}
|
\input{plfa/part2/Lambda}
|
||||||
\input{ latex/plfa/part2/DeBruijn}
|
\input{plfa/part2/Properties}
|
||||||
\input{ latex/plfa/part2/More}
|
\input{plfa/part2/DeBruijn}
|
||||||
\input{ latex/plfa/part2/Bisimulation }
|
\input{plfa/part2/More}
|
||||||
\input{ latex/plfa/part2/Inference }
|
\input{plfa/part2/Bisimulation}
|
||||||
\input{ latex/plfa/part2/Untyped }
|
\input{plfa/part2/Inference}
|
||||||
\input{ latex/plfa/part2/Confluence }
|
\input{plfa/part2/Untyped}
|
||||||
\input{ latex/plfa/part2/BigStep }
|
\input{plfa/part2/Confluence}
|
||||||
\part{ Part 3: Denotational Semantics }
|
\input{plfa/part2/BigStep}
|
||||||
\input{ latex/plfa/part3/Denotational }
|
|
||||||
\input{ latex/plfa/part3/Compositional }
|
\part{Part 3: Denotational Semantics}
|
||||||
\input{ latex/plfa/part3/Soundness }
|
\input{plfa/part3/Denotational}
|
||||||
\input{ latex/plfa/part3/Adequacy }
|
\input{plfa/part3/Compositional}
|
||||||
\input{ latex/plfa/part3/ContextualEquivalence }
|
\input{plfa/part3/Soundness}
|
||||||
|
\input{plfa/part3/Adequacy}
|
||||||
|
\input{plfa/part3/ContextualEquivalence}
|
||||||
|
|
||||||
|
\cleardoublepage%
|
||||||
|
\phantomsection%
|
||||||
|
|
||||||
% https://tex.stackexchange.com/questions/286431/putting-appendix-outside-the-last-part
|
|
||||||
\cleardoublepage
|
|
||||||
\phantomsection
|
|
||||||
\appendix
|
\appendix
|
||||||
\addcontentsline{toc}{part}{Appendices}
|
\addcontentsline{toc}{part}{Appendices}
|
||||||
\input{ latex/plfa/part2/Substitution }
|
|
||||||
\input{ latex/plfa/backmatter/acknowledgements}
|
\input{plfa/part2/Substitution}
|
||||||
\input{ latex/plfa/backmatter/Fonts }
|
\input{plfa/backmatter/acknowledgements}
|
||||||
|
\input{plfa/backmatter/Fonts}
|
||||||
\end{document}
|
\end{document}
|
||||||
|
|
@ -1012,7 +1012,7 @@ all-funs∈ {⊥} f with f {⊥} refl
|
||||||
... | fun ()
|
... | fun ()
|
||||||
all-funs∈ {v ↦ w} f = ⟨ v , ⟨ w , refl ⟩ ⟩
|
all-funs∈ {v ↦ w} f = ⟨ v , ⟨ w , refl ⟩ ⟩
|
||||||
all-funs∈ {u ⊔ u′} f
|
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) ⟩ ⟩
|
... | ⟨ v , ⟨ w , m ⟩ ⟩ = ⟨ v , ⟨ w , (inj₁ m) ⟩ ⟩
|
||||||
```
|
```
|
||||||
|
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue