Skip to content
Permalink
Browse files

Minted lexer (minimal) for PML + example

  • Loading branch information...
rlepigre committed Apr 9, 2019
1 parent ee45339 commit d4f1054bad040b364352ae82fe9040fc621eb8aa
Showing with 108 additions and 3 deletions.
  1. +4 −2 GNUmakefile
  2. +40 −0 book/part1_intro/intro.tex
  3. +1 −1 book/part2_theory/chap1_machine/machine.tex
  4. +48 −0 book/pml.py
  5. +15 −0 book/pml_book.tex
@@ -12,8 +12,9 @@ bin:
.PHONY: book
book: book/pml_book.pdf

book/pml_book.pdf: book/biblio.bib $(shell find book -name "*.tex")
@cd book && rubber -W all --pdf pml_book.tex
book/pml_book.pdf: book/biblio.bib book/pml.py $(shell find book -name "*.tex")
@rm -rf book/_minted*
@cd book && rubber --unsafe -W all --pdf pml_book.tex

# Checks on the source code.
check:
@@ -46,6 +47,7 @@ clean:
@dune clean

distclean: clean
@rm -rf book/_minted*
@find . -type f -name "*~" -exec rm {} \;
@find . -type f -name \#\* -exec rm {} \;
@find . -type f -name .\#\* -exec rm {} \;
@@ -0,0 +1,40 @@
% Test for “minted”
The identity function is \dupml{fun x { x }} in \pml, and it is \ducaml{fun x
-> x} in OCaml. The following is an example of \pml code.
\begin{pmlcode}
include lib.option
include lib.nat

type rec list⟨a⟩ = [Nil ; Cons of {hd : a ; tl : list}]

val rec length : ∀a, list⟨a⟩ ⇒ nat =
fun l {
case l {
[] → zero
hd :: tl → succ (length tl)
}
}

val rec map : ∀a b, (a ⇒ b) ⇒ list⟨a⟩ ⇒ list⟨b⟩ =
fun fn l {
case l {
[] → []
hd :: tl → fn hd :: map fn tl
}
}
\end{pmlcode}

And we can do some OCaml code as well to compare.
\begin{camlcode}
type 'a list = Nil | Cons of 'a * 'a list

let rec length : 'a list -> int = fun l ->
match l with
| Nil -> 0
| Cons(_,l) -> 1 + length l

let rec map : ('a -> 'b) -> 'a list -> 'b list = fun f l ->
match l with
| Nil -> Nil
| Cons(x,l) -> Cons(f x, map f l)
\end{camlcode}
@@ -1131,7 +1131,7 @@ \section{Canonical values}
showing that $$ is only equivalent to itself among all values. Similarly, it
is possible to show that $λ$-variables are only equivalent to themselves.
\begin{theorem}[canonicity for $$]\label{thm:canonbox}%
Let $v ∈ Λ_{ι}$ be a value. We have $\v{□}\v{v}$ if and only if $v = □$.
Let $v ∈ Λ_{ι}$ be a value. We have $v$ if and only if $v = □$.
\end{theorem}
\begin{proof}
If $v = □$ then we immediately have $□ ≡ v$ by reflexivity. It remains to
@@ -0,0 +1,48 @@
#!/usr/bin/env python
# -*- coding: utf-8 -*-
#
# This file contains provides a Pygments lexer for PML, that may be used to
# display PML code in LaTeX documents thanks to the “minted” package.
#
# Requirements: pygmentize >= 2.2.0 (check with “pygmentize -V”)
#
# \usepackage{minted}
# \begin{minted}{pml.py:PMLLexer -x}
# ...
# \end{minted}

from pygments.lexer import RegexLexer, bygroups, combined, include
from pygments.token import Text, Comment, Operator, Keyword, Name, String
from pygments.token import Number, Punctuation, Whitespace

class PMLLexer(RegexLexer):
"""
A Pygments lexer for the PML language
"""

name = 'PML'
aliases = ['pml']
filenames = ['*.pml']

keywords = [
'assert', 'assume', 'because', 'bool', 'by', 'case', 'check', 'corec',
'deduce', 'delim', 'def', 'else', 'eqns', 'fix', 'for', 'fun', 'if',
'include', 'infix', 'know', 'let', 'of', 'print', 'qed', 'rec',
'restore', 'save', 'set', 'show', 'showing', 'sort', 'such', 'suppose',
'take', 'that', 'type', 'unsafe', 'use', 'using', 'val'
]

special = [
'', '', ',', '', '', '', '', '=', '', '{', '}', '\(', '\)', '\[',
'\]', '\:', '\.', ';', '', ''
]

tokens = {
'root': [
(r'\s+', Text),
(r'\b(%s)\b' % '|'.join(keywords), Keyword),
(r'(%s)' % '|'.join(special), Keyword),
(r'//.*$', Comment.Single),
(r'\w+', Name.Variable),
]
}
@@ -13,6 +13,21 @@
\usepackage{geometry}
\usepackage{mdframed}
\usepackage{thmbox}
\usepackage{minted}

% PML environment and macro
\newenvironment{pmlcode}
{\VerbatimEnvironment\begin{minted}{pml.py:PMLLexer -x}}
{\end{minted}}

\newcommand{\dupml}[1]{\mintinline{pml.py:PMLLexer -x}{#1}}

% OCaml environment and macro
\newenvironment{camlcode}
{\VerbatimEnvironment\begin{minted}{ocaml}}
{\end{minted}}

\newcommand{\ducaml}[1]{\mintinline{ocaml}{#1}}

% Boxed figures
\usepackage{float}

0 comments on commit d4f1054

Please sign in to comment.
You can’t perform that action at this time.