% boogie.sty
% Boogie mode for the LaTeX listings package.
% Rustan Leino, 30 May 2008.
% Example:
% \begin{boogie}
% type Field \alpha;
% var Heap: <<\alpha>>[ref, Field \alpha]\alpha where IsHeap(Heap);
% function IsHeap(<<\alpha>>[ref, Field \alpha]\alpha) returns (bool);
% procedure Inc(x: int) returns (y: int)
%   modifies Heap;
% {
%   havoc Heap;
%   if (0 <= x && x < 100) {
%     y := x + 1;
%   }
% }
% \end{boogie}

\usepackage{listings}

\lstdefinelanguage{boogie}{
  morekeywords={type,bool,int,real,%
      bv0,bv1,bv2,bv3,bv4,bv5,bv6,bv7,bv8,bv9,%
      bv10,bv11,bv12,bv13,bv14,bv15,bv16,bv17,bv18,bv19,%
      bv20,bv21,bv22,bv23,bv24,bv25,bv26,bv27,bv28,bv29,%
      bv30,bv31,bv32,bv33,bv34,bv35,bv36,bv37,bv38,bv39,%
      bv40,bv41,bv42,bv43,bv44,bv45,bv46,bv47,bv48,bv49,%
      bv50,bv51,bv52,bv53,bv54,bv55,bv56,bv57,bv58,bv59,%
      bv60,bv61,bv62,bv63,bv64,% ...
      const,unique,complete,partition,
      axiom,
      function,returns,
      var,where,
      procedure,implementation,
      requires,modifies,ensures,free,
      % expressions
      false,true,null,old,then,div,mod,
      % statements
      assert,assume,havoc,call,if,else,while,invariant,break,return,goto,
      },
  literate=%
    {:}{$\colon$}1
    {::}{$\bullet$}2
    {:=}{$:$$=$}2
    {!}{$\lnot$}1
    {==}{$=$}1
    {!=}{$\neq$}1
    {&&}{$\land$}1
    {||}{$\lor$}1
    {<=}{$\le$}1
    {>=}{$\ge$}1
    {==>}{$\Longrightarrow$}3 
    {<==>}{$\Longleftrightarrow$}4 
    {forall}{$\forall$}1
    {exists}{$\exists$}1
    {lambda}{$\lambda$}1
    % the following isn't actually Boogie, but it gives the option to produce nicer latex
    {<<}{$\langle$}1
    {>>}{$\rangle$}1
    {\\alpha}{$\alpha$}1
    {\\beta}{$\beta$}1
    {\\gamma}{$\gamma$}1
    {\\delta}{$\delta$}1
    {\\epsilon}{$\epsilon$}1
    {\\zeta}{$\zeta$}1
    {\\eta}{$\eta$}1
    {\\theta}{$\theta$}1
    {\\iota}{$\iota$}1
    {\\kappa}{$\kappa$}1
    {\\lambda}{$\lambda$}1
    {\\mu}{$\mu$}1
    {\\nu}{$\nu$}1
    {\\xi}{$\xi$}1
    {\\pi}{$\pi$}1
    {\\rho}{$\rho$}1
    {\\sigma}{$\sigma$}1
    {\\tau}{$\tau$}1
    {\\upsilon}{$\upsilon$}1
    {\\phi}{$\phi$}1
    {\\chi}{$\chi$}1
    {\\psi}{$\psi$}1
    {\\omega}{$\omega$}1
    {\\Gamma}{$\Gamma$}1
    {\\Delta}{$\Delta$}1
    {\\Theta}{$\Theta$}1
    {\\Lambda}{$\Lambda$}1
    {\\Xi}{$\Xi$}1
    {\\Pi}{$\Pi$}1
    {\\Sigma}{$\Sigma$}1
    {\\Upsilon}{$\Upsilon$}1
    {\\Phi}{$\Phi$}1
    {\\Psi}{$\Psi$}1
    {\\Omega}{$\Omega$}1
    ,
  sensitive=true,  % case sensitive
  morecomment=[l]{//},
  morecomment=[s]{/*}{*/},
  morestring=[b]",
  numbers=none,
  firstnumber=0,
  numberstyle=\tiny,
  stepnumber=5,
  basicstyle=\scriptsize\sffamily,
  commentstyle=\itshape,
  keywordstyle=\bfseries,
  ndkeywordstyle=\bfseries,
}
\lstnewenvironment{boogie}[1][]{%
  \lstset{language=boogie,
    floatplacement={tbp},captionpos=b,
    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
\lstnewenvironment{boogieNoLines}[1][]{%
  \lstset{language=boogie,
    floatplacement={tbp},captionpos=b,
    xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,#1}}{}
\def\inlineboogie{%
    \lstinline[language=boogie,basicstyle=\ttfamily,columns=fixed]}
\newcommand{\lstfile}[1]{
  \lstinputlisting[language=boogie,%
    frame=lines,xleftmargin=8pt,xrightmargin=8pt,basicstyle=\ttfamily,columns=fixed]{#1}
}