agda.sty

   1 % ----------------------------------------------------------------------
   2 % Some useful commands when doing highlighting of Agda code in LaTeX.
   3 % ----------------------------------------------------------------------
   4
   5 \ProvidesPackage{agda}
   6
   7 \usepackage{ifxetex, polytable, ifthen}
   8
   9 % XeLaTeX
  10 \ifxetex
  11     \usepackage{polyglossia}
  12     \usepackage{fontspec}
  13     \usepackage[]{unicode-math}
  14
  15 % pdfLaTeX
  16 \else
  17     \usepackage{ucs, amsfonts, amssymb}
  18     \usepackage[safe]{tipa} % See page 12 of the tipa manual for what
  19                             % safe does.
  20
  21     % FIX: This doesn't seem to help solve the pipe problem?
  22     % http://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
  23     \usepackage[T1]{fontenc}
  24     \usepackage[utf8x]{inputenc}
  25
  26     % FIX: Complete the list and send it upstream to the ucs package devs.
  27     \DeclareUnicodeCharacter{9657}{$\triangleright$}
  28     \DeclareUnicodeCharacter{8759}{::}
  29     \DeclareUnicodeCharacter{8263}{$?\!?$}
  30     \DeclareUnicodeCharacter{737} {$^l$}  % FIX: Ugly, apparently ^r is
  31                                           % defined, I can't find the
  32                                           % definition though.
  33     \DeclareUnicodeCharacter{8718}{$\blacksquare$}
  34     \DeclareUnicodeCharacter{8255}{$\_$} % FIX: Couldn't find \undertie.
  35     \DeclareUnicodeCharacter{9667}{$\triangleleft$}
  36     \DeclareUnicodeCharacter{10218}{$\langle\!\langle$}
  37     \DeclareUnicodeCharacter{10219}{$\rangle\!\rangle$}
  38 \fi
  39
  40 % ----------------------------------------------------------------------
  41 % Colour schemes.
  42
  43 \newcommand{\AgdaColourScheme}{standard}
  44
  45 \DeclareOption{bw}   {\renewcommand{\AgdaColourScheme}{bw}}
  46 \DeclareOption{conor}{\renewcommand{\AgdaColourScheme}{conor}}
  47 \ProcessOptions\relax
  48
  49 % ----------------------------------------------------------------------
  50 % Font styles.
  51
  52 % Default font style.
  53 \newcommand{\AgdaFontStyle}[1]{\textsf{#1}}
  54
  55 % Keyword font style.
  56 \ifthenelse{\equal{\AgdaColourScheme}{bw}}{
  57     \newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
  58 }{
  59     \newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}
  60 }
  61
  62 % String font style.
  63 \newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}
  64
  65 % Comment font style.
  66 \newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}
  67
  68 % Bounded variables font style.
  69 \newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}
  70
  71 % ----------------------------------------------------------------------
  72 % Colours.
  73
  74 % ----------------------------------
  75 % The black and white colour scheme.
  76 \ifthenelse{\equal{\AgdaColourScheme}{bw}}{
  77
  78     % Aspect colours.
  79     \definecolor{AgdaComment}      {HTML}{000000}
  80     \definecolor{AgdaKeyword}      {HTML}{000000}
  81     \definecolor{AgdaString}       {HTML}{000000}
  82     \definecolor{AgdaNumber}       {HTML}{000000}
  83     \definecolor{AgdaSymbol}       {HTML}{000000}
  84     \definecolor{AgdaPrimitiveType}{HTML}{000000}
  85     \definecolor{AgdaOperator}     {HTML}{000000}
  86
  87     % NameKind colours.
  88     \definecolor{AgdaBound}                 {HTML}{000000}
  89     \definecolor{AgdaInductiveConstructor}  {HTML}{000000}
  90     \definecolor{AgdaCoinductiveConstructor}{HTML}{000000}
  91     \definecolor{AgdaDatatype}              {HTML}{000000}
  92     \definecolor{AgdaField}                 {HTML}{000000}
  93     \definecolor{AgdaFunction}              {HTML}{000000}
  94     \definecolor{AgdaModule}                {HTML}{000000}
  95     \definecolor{AgdaPostulate}             {HTML}{000000}
  96     \definecolor{AgdaPrimitive}             {HTML}{000000}
  97     \definecolor{AgdaRecord}                {HTML}{000000}
  98
  99     % Other aspect colours.
 100     \definecolor{AgdaDottedPattern}     {HTML}{000000}
 101     \definecolor{AgdaUnsolvedMeta}      {HTML}{D3D3D3}
 102     \definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}
 103     \definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}
 104     \definecolor{AgdaError}             {HTML}{696969}
 105
 106     % Misc.
 107     \definecolor{AgdaHole}              {HTML}{BEBEBE}
 108
 109 % ----------------------------------
 110 % Conor McBride's colour scheme.
 111 }{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{
 112
 113     % Aspect colours.
 114     \definecolor{AgdaComment}      {HTML}{B22222}
 115     \definecolor{AgdaKeyword}      {HTML}{000000}
 116     \definecolor{AgdaString}       {HTML}{000000}
 117     \definecolor{AgdaNumber}       {HTML}{000000}
 118     \definecolor{AgdaSymbol}       {HTML}{000000}
 119     \definecolor{AgdaPrimitiveType}{HTML}{0000CD}
 120     \definecolor{AgdaOperator}     {HTML}{000000}
 121
 122     % NameKind colours.
 123     \definecolor{AgdaBound}                 {HTML}{A020F0}
 124     \definecolor{AgdaInductiveConstructor}  {HTML}{8B0000}
 125     \definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}
 126     \definecolor{AgdaDatatype}              {HTML}{0000CD}
 127     \definecolor{AgdaField}                 {HTML}{8B0000}
 128     \definecolor{AgdaFunction}              {HTML}{006400}
 129     \definecolor{AgdaModule}                {HTML}{006400}
 130     \definecolor{AgdaPostulate}             {HTML}{006400}
 131     \definecolor{AgdaPrimitive}             {HTML}{006400}
 132     \definecolor{AgdaRecord}                {HTML}{0000CD}
 133
 134     % Other aspect colours.
 135     \definecolor{AgdaDottedPattern}     {HTML}{000000}
 136     \definecolor{AgdaUnsolvedMeta}      {HTML}{FFD700}
 137     \definecolor{AgdaTerminationProblem}{HTML}{FF0000}
 138     \definecolor{AgdaIncompletePattern} {HTML}{A020F0}
 139     \definecolor{AgdaError}             {HTML}{F4A460}
 140
 141     % Misc.
 142     \definecolor{AgdaHole}              {HTML}{9DFF9D}
 143
 144 % ----------------------------------
 145 % The standard colour scheme.
 146 }{
 147     % Aspect colours.
 148     \definecolor{AgdaComment}      {HTML}{B22222}
 149     \definecolor{AgdaKeyword}      {HTML}{CD6600}
 150     \definecolor{AgdaString}       {HTML}{B22222}
 151     \definecolor{AgdaNumber}       {HTML}{A020F0}
 152     \definecolor{AgdaSymbol}       {HTML}{404040}
 153     \definecolor{AgdaPrimitiveType}{HTML}{0000CD}
 154     \definecolor{AgdaOperator}     {HTML}{000000}
 155
 156     % NameKind colours.
 157     \definecolor{AgdaBound}                 {HTML}{000000}
 158     \definecolor{AgdaInductiveConstructor}  {HTML}{008B00}
 159     \definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}
 160     \definecolor{AgdaDatatype}              {HTML}{0000CD}
 161     \definecolor{AgdaField}                 {HTML}{EE1289}
 162     \definecolor{AgdaFunction}              {HTML}{0000CD}
 163     \definecolor{AgdaModule}                {HTML}{A020F0}
 164     \definecolor{AgdaPostulate}             {HTML}{0000CD}
 165     \definecolor{AgdaPrimitive}             {HTML}{0000CD}
 166     \definecolor{AgdaRecord}                {HTML}{0000CD}
 167
 168     % Other aspect colours.
 169     \definecolor{AgdaDottedPattern}     {HTML}{000000}
 170     \definecolor{AgdaUnsolvedMeta}      {HTML}{FFFF00}
 171     \definecolor{AgdaTerminationProblem}{HTML}{FFA07A}
 172     \definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}
 173     \definecolor{AgdaError}             {HTML}{FF0000}
 174
 175     % Misc.
 176     \definecolor{AgdaHole}              {HTML}{9DFF9D}
 177 }}
 178
 179 % ----------------------------------------------------------------------
 180 % Commands.
 181
 182 % Aspect commands.
 183 \newcommand{\AgdaComment}     [1]
 184     {\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}
 185 \newcommand{\AgdaKeyword}     [1]
 186     {\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}
 187 \newcommand{\AgdaString}      [1]{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}
 188 \newcommand{\AgdaNumber}      [1]{\textcolor{AgdaNumber}{#1}}
 189 \newcommand{\AgdaSymbol}      [1]{\textcolor{AgdaSymbol}{#1}}
 190 \newcommand{\AgdaPrimitiveType}[1]
 191     {\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}
 192 \newcommand{\AgdaOperator}    [1]{\textcolor{AgdaOperator}{#1}}
 193
 194 % NameKind commands.
 195 \newcommand{\AgdaBound}    [1]{\AgdaBoundFontStyle{\textcolor{AgdaBound}{#1}}}
 196 \newcommand{\AgdaInductiveConstructor}[1]
 197     {\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{#1}}}
 198 \newcommand{\AgdaCoinductiveConstructor}[1]
 199     {\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{#1}}}
 200 \newcommand{\AgdaDatatype} [1]{\AgdaFontStyle{\textcolor{AgdaDatatype}{#1}}}
 201 \newcommand{\AgdaField}    [1]{\AgdaFontStyle{\textcolor{AgdaField}{#1}}}
 202 \newcommand{\AgdaFunction} [1]{\AgdaFontStyle{\textcolor{AgdaFunction}{#1}}}
 203 \newcommand{\AgdaModule}   [1]{\AgdaFontStyle{\textcolor{AgdaModule}{#1}}}
 204 \newcommand{\AgdaPostulate}[1]{\AgdaFontStyle{\textcolor{AgdaPostulate}{#1}}}
 205 \newcommand{\AgdaPrimitive}[1]{\AgdaFontStyle{\textcolor{AgdaPrimitive}{#1}}}
 206 \newcommand{\AgdaRecord}   [1]{\AgdaFontStyle{\textcolor{AgdaRecord}{#1}}}
 207
 208 % Other aspect commands.
 209 \newcommand{\AgdaDottedPattern}     [1]{\textcolor{AgdaDottedPattern}{#1}}
 210 \newcommand{\AgdaUnsolvedMeta}      [1]
 211     {\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}
 212 \newcommand{\AgdaTerminationProblem}[1]
 213     {\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}
 214 \newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}
 215 \newcommand{\AgdaError}             [1]
 216     {\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}}
 217
 218 % Misc.
 219 \newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
 220 \long\def\AgdaHide#1{} % Used to hide code from LaTeX.
 221
 222 \newcommand{\AgdaIndent}[1]{\quad}
 223
 224 % ----------------------------------------------------------------------
 225 % The code environment.
 226
 227 \newcommand{\AgdaCodeStyle}{}
 228 % \newcommand{\AgdaCodeStyle}{\tiny}
 229
 230 \ifdefined\mathindent
 231   {}
 232 \else
 233   \newdimen\mathindent\mathindent\leftmargini
 234 \fi
 235
 236 \newenvironment{code}%
 237 {\noindent\ignorespaces\advance\leftskip\mathindent\AgdaCodeStyle\pboxed}%
 238 {\endpboxed\par\noindent%
 239 \ignorespacesafterend}
 240
 241 % Default column for polytable.
 242 \defaultcolumn{l}