lstpi.sty

% lstlisting pi-forall style
% Based on Coq lstlisting style
%
\lstdefinelanguage{PiForall}{
%
% Anything betweeen $ becomes LaTeX math mode
mathescape=true,
%
% Comments may or not include Latex commands
texcl=false,
%
morekeywords=[1]{module,import},
morekeywords=[2]{let, in, if, then, else, case, of, data, where, Type},
morekeywords=[3]{},
morekeywords=[4]{True, False, Refl, Cons, Nil, Zero, Succ},
morekeywords=[5]{Bool, Vec, Nat, Unit, Fin},
%
% Comments delimiter
morecomment=[s]{{-}{-}},
morecomment=[l]{--},
%
% Spaces are not displayed as a special character
showstringspaces=false,
%
upquote          = true,
% String delimiters
morestring=[b]",
%
% Size of tabulations
tabsize=3,
%
% Enables ASCII chars 128 to 255
extendedchars=false,
%
% Case sensitivity
sensitive=true,
%
% Automatic breaking of long lines
breaklines=false,
%
% Default style for listings
basicstyle=\small\ttfamily,
%
% Position of captions is bottom
captionpos=b,
%
% flexible columns
columns=[l]flexible,
%
% Style for (listings') identifiers
identifierstyle={\ttfamily\color{black}},
keywordstyle=[1]{\ttfamily\color{Plum}},
keywordstyle=[2]{\ttfamily\color{PineGreen}},
keywordstyle=[3]{\ttfamily\color{BlueGreen}},
keywordstyle=[4]{\ttfamily\color{BlueViolet}},
keywordstyle=[5]{\ttfamily\color{Maroon}},
% Style for strings
stringstyle=\ttfamily,
% Style for comments
commentstyle={\ttfamily\color{PineGreen}},
%
literate=
    {\\}{{\color{PineGreen}{$\lambda$}}}1
    {\\forall}{{\color{green}{$\forall\;$}}}1
    {\\exists}{{$\exists\;$}}1
    {<-}{{$\leftarrow\;$}}1
    {=>}{{$\Rightarrow\;$}}1
    {==}{{\code{==}\;}}1
    {==>}{{\code{==>}\;}}1
    {->}{{$\rightarrow\;$}}1
    {<->}{{$\leftrightarrow\;$}}1
    {<==}{{$\leq\;$}}1
    {\#}{{$^\star$}}1
    {\\o}{{$\circ\;$}}1
    {\/\\}{{$\wedge\;$}}1
    {\\\/}{{$\vee\;$}}1
    {++}{{\code{++}}}1
    {\\mapsto}{{$\mapsto\;$}}1
    {\\hline}{{\rule{\linewidth}{0.5pt}}}1
%
}[keywords,comments,strings]

\lstnewenvironment{piforall}{\lstset{language=PiForall}}{}

\def\piforalle{\lstinline[language=PiForall, basicstyle=\small]}
\def\piforalls{\lstinline[language=PiForall, basicstyle=\scriptsize]}