idrislang.sty

%% --------------------------------------------------- [ Idris Styling Package ]
%%
%% A set of LaTeX macros and styling for working with Idris in LaTeX
%%
%%   + Provides a listings bindings:
%%      + idris         :: default ascii
%%      + literateidris :: convert ascii maths to math symbols.
%%   + Defines a `numbers', `default', and `stdout' listings style.
%%      + default :: Uses TT font for code and SF font for comments,
%%                   and indented by parident.
%%      + numbers :: default but with numbers.
%%      + beamer  :: default minus parindent
%%      + stdout  :: for formatting stdout.
%%   + Defines a `code' environment for typesetting idris.
%%      + \begin{code}[...] ... \end{code}
%%   + Defines an input command for externally defined idris files.
%%      + \\idrisinput[...]{file.idr}
%%   + Provides definitions (from Idris Compiler) for pretty-printing Idris
%%     code using Fancy Verbatim and colour commands.
%%      + Sets commandchars for latex commands.
%%   + Defines commands typesetting the name Idris.
%%      + \Idris{}
%%      + \idris{}
%%
%% Options:
%%    - literate :: turn on literate idris for code environments.
%%
%% ----------------------------------------------------------- [ Begin Package ]
\ProvidesPackage{idrislang}

\RequirePackage{ifthen}
\RequirePackage{xcolor}
\RequirePackage{fancyvrb}
\RequirePackage[final]{listings}
\RequirePackage{xspace}
\RequirePackage{textcomp}
\RequirePackage{setspace}
%% ----------------------------------------------------------------- [ Options ]
\newboolean{literate}
\setboolean{literate}{false}

\DeclareOption{literate}{%
  \setboolean{literate}{true}}

\newboolean{styles}
\setboolean{styles}{false}

\DeclareOption{styles}{%
  \setboolean{styles}{true}}

\ProcessOptions\relax

%% ---------------------------------------------------------------- [ Commands ]
\newcommand{\Idris}{Idris\xspace}
\newcommand{\idris}{Idris\xspace}
\newcommand{\IdrisLineSpacing}{\singlespacing}
%% ---------------------------------------------------------- [ Color Commands ]
\newcommand{\IdrisData}[1]{\textcolor{red}{#1}}
\newcommand{\IdrisType}[1]{\textcolor{blue}{#1}}
\newcommand{\IdrisBound}[1]{\textcolor{magenta}{#1}}
\newcommand{\IdrisFunction}[1]{\textcolor{green}{#1}}
\newcommand{\IdrisKeyword}[1]{{\underline{#1}}}
\newcommand{\IdrisImplicit}[1]{{\itshape \IdrisBound{#1}}}

\fvset{commandchars=\\\{\}}

%% --------------------------------------------------- [ Define Idris Listings ]
\lstdefinelanguage{idris}{%
  sensitive,%
%% ----------------------------------------------------------- [ Default Style ]
  tabsize=2,
  upquote=true,
  basicstyle=\ttfamily\footnotesize,
  flexiblecolumns=false,
  keywordstyle=\color{black}\bfseries\underbar,
%  commentstyle=\footnotesize,
%% ---------------------------------------------------------------- [ Keywords ]
%% From Idris Parser and idris-mode and vimscript
  keywords={%
    abstract, attack, case, compute, do, dsl, else, exact, focus, if,
    import, in, infix, infixl, infixr, instance, intros, module,
    mutual, namespace, of, let, parameters, partial, pattern, prefix,
    private, public, refine, rewrite, solve, syntax, term, then,
    total, trivial, try, using, where, with, constructor, interface, implementation
},
%% ------------------------------------------------------- [ Prelude Functions ]
  morekeywords={%
    class, data, instance, record, dsl, postulate, default,
    lambda, variable, index_first, index_next
  },
%% ---------------------------------------------------------------- [ Comments ]
   morecomment=[l]--,%
   morecomment=[n]{\{-}{-\}}
}[keywords,comments,strings]%

%% ---------------------------------------- [ Define Idris with Literate Stuff ]
\lstdefinelanguage{literateidris}[]{idris}{
  literate= {+}{{$+$}}1
            {/}{{$/$}}1
            {*}{{$*$}}1
            {=}{{$=$}}1
            {>}{{$>$}}1
            {<}{{$<$}}1
            {\\}{{$\lambda$}}1
            {\\\\}{{\char`\\\char`\\}}1
            {->}{{$\rightarrow$}}2
            {>=}{{$\geq$}}2
            {<-}{{$\leftarrow$}}2
            {<=}{{$\leq$}}2
            {=>}{{$\Rightarrow$}}2
            {==}{{$\equiv$}}2
            {\ .}{{$\circ$}}2
            {\ .\ }{{$\circ$}}2
            {>>}{{>>}}2
            {>>=}{{>>=}}2
            {|}{{$\mid$}}1,
}
%% -------------------------------------------------- [ Default Listings Style ]

\ifthenelse{\boolean{styles}}{
  \lstdefinestyle{default}{%
    basicstyle=\ttfamily\normalsize,
  }

  \lstdefinestyle{numbers}{%
    numbers=left,
    numbersep=10pt,
    numberstyle=\footnotesize\sffamily,
    frame=leftline
  }

  \lstdefinestyle{stdout}{%
    xleftmargin=\parindent,
    tabsize=2,
    basicstyle=\ttfamily\normalsize,
    showstringspaces=false,
    escapechar=^
  }

  \lstdefinestyle{beamer}{%
    basicstyle=\ttfamily\normalsize,
    escapechar=^
  }
}{}

%% ------------------------------------------------------ [ A Code Environment ]
%% Replicate the existence of literate haskell code environments,
%% option to make pretty with numbers.
\lstnewenvironment{code}[1][]
    {\ifthenelse{\boolean{literate}}{%
        \lstset{language=literateidris,#1}}{%
        \lstset{language=idris,#1}}
    \IdrisLineSpacing{}
    }{}
\lstnewenvironment{idrislisting}[1][]
    {\ifthenelse{\boolean{literate}}{%
        \lstset{language=literateidris,#1}}{%
        \lstset{language=idris,#1}}
    \IdrisLineSpacing{}
    }{}
%% ---------------------------------------------------------- [ Input Listings ]
%% Command to add externally defined Idris code to the document.
\newcommand{\idrisinput}[2][]{%
\begingroup
    \ifthenelse{\boolean{literate}}{%
      \lstset{language=literateidris}}{%
      \lstset{language=idris}}
    \IdrisLineSpacing{}
    \lstinputlisting[#1]{#2}
\endgroup
}

\newcommand{\idrisinline}[1]{%
\ifthenelse{\boolean{literate}}{%
  \lstset{language=literateidris}}{%
  \lstset{language=idris}}%
  \lstinline[language=idris]{#1}}

\endinput
%% --------------------------------------------------------------------- [ EOF ]