From b0e214adbbbaae5e057db7d81517f6fcf04b974e Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Mon, 13 Nov 2023 00:20:05 +0000 Subject: [PATCH] feat: add Lean4 syntax highlighting support to template --- paper.tex | 24 +++++++++++ tools/Lean4Lexer.py | 100 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 124 insertions(+) create mode 100644 tools/Lean4Lexer.py diff --git a/paper.tex b/paper.tex index 22b0f35..7d27c46 100644 --- a/paper.tex +++ b/paper.tex @@ -70,10 +70,12 @@ { \newminted[mlir]{tools/MLIRLexer.py:MLIRLexerOnlyOps}{customlexer, mathescape} \newminted[xdsl]{tools/MLIRLexer.py:MLIRLexer}{customlexer, mathescape, style=murphy} +\newminted[lean4]{tools/Lean4Lexer.py:Lean4Lexer}{customlexer, mathescape} } { \newminted[mlir]{tools/MLIRLexer.py:MLIRLexerOnlyOps -x}{mathescape} \newminted[xdsl]{tools/MLIRLexer.py:MLIRLexer -x}{mathescape, style=murphy} +\newminted[lean4]{tools/Lean4Lexer.py:Lean4Lexer -x}{mathescape} } \makeatother @@ -130,6 +132,14 @@ \usepackage{booktabs} \newcommand{\ra}[1]{\renewcommand{\arraystretch}{#1}} +\usepackage[verbose]{newunicodechar} +\newunicodechar{₁}{\ensuremath{_1}} +\newunicodechar{₂}{\ensuremath{_2}} +\newunicodechar{∀}{\ensuremath{\forall}} +\newunicodechar{α}{\ensuremath{\alpha}} +\newunicodechar{β}{\ensuremath{\beta}} + + % \circled command to print a colored circle. % \circled{1} pretty-prints "(1)" % This is useful to refer to labels that are embedded within figures. @@ -562,6 +572,20 @@ \subsubsection{Listings} We aim to use minted to create listings as much as \label{lst:example} \end{listing} +\begin{listing}[H] +\begin{lean4} +theorem funext {f₁ f₂ : ∀ (x : α), β x} + (h : ∀ x, f₁ x = f₂ x) : f₁ = f₂ := by + show extfunApp (Quotient.mk' f₁) = + extfunApp (Quotient.mk' f₂) + apply congrArg + apply Quotient.sound + exact h +\end{lean4} +\caption{A simple Lean4 code example, taken from + \url{https://lean-lang.org/lean4/doc/syntax\_highlight\_in\_latex.html\#example-with-minted}.} +\end{listing} + The syntax highlighting also works for xDSL-like IRs. Notice that different minted styles can be used for different environments. The xDSL environment uses the murphy-style in this case, whereas the MLIR version applies the diff --git a/tools/Lean4Lexer.py b/tools/Lean4Lexer.py new file mode 100644 index 0000000..a75b26b --- /dev/null +++ b/tools/Lean4Lexer.py @@ -0,0 +1,100 @@ +# -*- coding: utf-8 -*- +""" + pygments.lexers.theorem + ~~~~~~~~~~~~~~~~~~~~~~~ + + Lexers for theorem-proving languages. + + :copyright: Copyright 2006-2017 by the Pygments team, see AUTHORS. + :license: BSD, see LICENSE for details. +""" + +import re + +from pygments.lexer import RegexLexer, default, words +from pygments.token import Text, Comment, Operator, Keyword, Name, String, \ + Number, Punctuation, Generic + +__all__ = ['Lean4Lexer'] + +class Lean4Lexer(RegexLexer): + """ + For the `Lean 4 `_ + theorem prover. + + .. versionadded:: 2.0 + """ + name = 'Lean4' + aliases = ['lean4'] + filenames = ['*.lean'] + mimetypes = ['text/x-lean'] + + flags = re.MULTILINE | re.UNICODE + + keywords1 = ( + 'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition', + 'renaming', 'inline', 'hiding', 'parameter', 'lemma', 'variable', + 'theorem', 'axiom', 'inductive', 'structure', 'universe', 'alias', + 'help', 'options', 'precedence', 'postfix', 'prefix', + 'infix', 'infixl', 'infixr', 'notation', '#eval', + '#check', '#reduce', '#exit', 'coercion', 'end', 'private', 'using', 'namespace', + 'including', 'instance', 'section', 'context', 'protected', 'expose', + 'export', 'set_option', 'extends', 'open', 'example', + 'constant', 'constants', 'print', 'opaque', 'reducible', 'irreducible', + 'def', 'macro', 'elab', 'syntax', 'macro_rules', 'reduce', 'where', + 'abbrev', 'noncomputable', 'class', 'attribute', 'synth', 'mutual', + ) + + keywords2 = ( + 'forall', 'fun', 'Pi', 'obtain', 'from', 'have', 'show', 'assume', + 'take', 'let', 'if', 'else', 'then', 'by', 'in', 'with', 'begin', + 'proof', 'qed', 'calc', 'match', 'nomatch', 'do', 'at', + ) + + keywords3 = ( + # Sorts + 'Type', 'Prop', 'Sort', + ) + + operators = ( + u'!=', u'#', u'&', u'&&', u'*', u'+', u'-', u'/', u'@', u'!', u'`', + u'-.', u'->', u'.', u'..', u'...', u'::', u':>', u';', u';;', u'<', + u'<-', u'=', u'==', u'>', u'_', u'|', u'||', u'~', u'=>', u'<=', u'>=', + u'/\\', u'\\/', u'∀', u'Π', u'λ', u'↔', u'∧', u'∨', u'≠', u'≤', u'≥', + u'¬', u'⁻¹', u'⬝', u'▸', u'→', u'∃', u'ℕ', u'ℤ', u'≈', u'×', u'⌞', + u'⌟', u'≡', u'⟨', u'⟩', + ) + + punctuation = (u'(', u')', u':', u'{', u'}', u'[', u']', u'⦃', u'⦄', + u':=', u',') + + tokens = { + 'root': [ + (r'\s+', Text), + (r'/-', Comment, 'comment'), + (r'--.*?$', Comment.Single), + (words(keywords1, prefix=r'\b', suffix=r'\b'), Keyword.Namespace), + (words(keywords2, prefix=r'\b', suffix=r'\b'), Keyword), + (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type), + (words(operators), Name.Builtin.Pseudo), + (words(punctuation), Operator), + (u"[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]" + u"[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079" + u"\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*", Name), + (r'\d+', Number.Integer), + (r'"', String.Double, 'string'), + (r'[~?][a-z][\w\']*:', Name.Variable) + ], + 'comment': [ + # Multiline Comments + (r'[^/-]', Comment.Multiline), + (r'/-', Comment.Multiline, '#push'), + (r'-/', Comment.Multiline, '#pop'), + (r'[/-]', Comment.Multiline) + ], + 'string': [ + (r'[^\\"]+', String.Double), + (r'\\[n"\\]', String.Escape), + ('"', String.Double, '#pop'), + ], + }