Antelatex is a pre-processor for TeX/LaTeX, written in OCaml.
The source code can be found at http://github.com/malo-denielou/antelatex.
You only need OCaml to compile antelatex, and a simple make will do. See the README file for more information. It is known to run under Linux although it should run under other operating systems where OCaml can be installed (Windows, MacOS).
When writing in LaTeX, it is often frustrating to use so many backslashes and to define so complex macros to represent simple things.
Why can't we write in our source file something like that:
Gamma |- e : T |
instead of | \Gamma \Mturnstile e \!:\! T |
E::= [__] || E|T || T|E || E;T |
instead of | \econtext \Mbnfeq [ \Mhole] \;\;\MPar\;\; \econtext \mid T \;\;\MPar\;\; T \mid \econtext \;\;\MPar\;\; \econtext; T |
if true then P else P' --> P |
instead of | \ls|if| \ls|true|
\mathrel{\ls|then|} P
\mathrel{\ls|else|} P'\Mreductionarrow P |
infrule |- ni ok ++ i=1,2 ------------- |- n1 || n2 ok endinf |
instead of | \infrule{ \Mturnstile n_i \Mok \quad i \Meq1,2 }
{ \Mturnstile n_1 \MPar n_2 \Mok }
|
Pi x:pub.mu X.Pi y:sub.x->y ty {"Msg"};X |
instead of | \Pi x \!:\! \text{pub}. \mu X.
\Pi y \!:\! \text{sub}.
x \Mtypearrow y \ENCan{ { \mbox{Msg}}}; X |
antelatex allows you to do such things, within the delimiters of your choosing, in complete integration with your existing TeX/LaTeX macros.
antelatex takes as arguments a grammar file, which contains the definitions of the substitutions you want to apply, and the files that you want to pre-process.
For example,
antelatex -g grammar.gra myfile.ant
will process the grammar file grammar.gra and apply it to the file myfile.ant and produce a file myfile.tex. The choice of extension for myfile or grammar.gra does not matter, as long as it is not .tex.
Grammar files are text files that define the substitutions that should be applied within some sets of delimiters.
A simple first line of a grammar file can be:
Delimiters:{{[[}{]]}{$}{$}}
The braces are separators, and within the braces are the delimiters. In this case, the grammar declares that the substitutions that are to follow should be applied within double brackets [[ and ]] and that the result of the substitution should appear in the TeX file between $ and $. The keyword Delimiters is actually optional.
The delimiters should always be 2 characters long. In the same line it is possible to declare several delimiters for the same set of substitutions, as in:
Delimiters:{{[[}{]]}{$}{$}}{{<[}{]>}{}{}}
This declaration defines the delimiters [[ ]] and <[ ]> such that [[ ]] introduces the math mode while <[ ]> does not.
Following the delimiters declaration, there should be a number of substitutions. Each substitution definition takes exactly one line, of the form (the number of spaces does not matter before the =:
0 {alpha} = \alpha
where 0 is the arity, 'alpha' the sequence of characters (between curly braces) to by substituted and '\alpha' (anything after the '=' and before the end of line) what it should be substituted to. The arity is optional and can be inferred by antelatex. An example of a substitution with arity 2:
{-->} = \xlongarrow{#1}_{#2}
When the arity is more than 0, the arguments are substituted in the positions materialised by #1, #2, ...
The following special characters cannot appear on the left-hand side of these substitution definitions:
{ } [ ] ( )
The following characters cannot be in a word to be substituted unless that word has no alpha-numerical characters:
, . ; *
These symbols are interpreted literally by antelatex, except for the curly braces { and }, which are used for grouping.
To finish this simple introduction to grammars, here is a sample grammar file:
Delimiters: {{[[}{]]}{$}{$}}{{<[}{]>}{}{}}
{a} = a
{ab} = a^{\bullet}
{ac} = a^{\circ}
{a0} = a_0
{a1} = a_1
{an} = a_n
{ll} = \ell
{C} = \mathcal{C}_{#1}^{#2}(#3)
{Tv} = \vec{T}
{|-} = \Mturnstile
{==>} = \Longrightarrow
{++} = \quad
{:} = \!:\!
{&} = &
{\\} = \\
{\/} = \vee
{/\} = \wedge
{=~} = \approx
{===} = \Mstructcong
{vec} = \smash[t]{\overrightarrow{#1}}
{forall} = \forall
{in} = \!\in\!
{\} = \lambda
{#} = \{#1/#2\}
{alpha} = \alpha
{infrule} = \infrule{
{-----} = }{
{endinf} = }
Note that on the right hand side are LaTeX macros and expressions that you should define like any other Latex macros.
Antelatex applies the substitutions in certain delimited parts of a text files.
Suppose a file contains the following line:
We know that [[1 plus 1]] is equal to <[two]>.
if the grammar file is like:
{{[[}{]]}{$}{$}}{{<[}{]>}{}{}}
{plus} = +
{two} = 2
Then antelatex will produce a file containing the line:
We know that $1 + 1$ is equal to 2.
Notice that the double brackets [[ ]] introduce the dollar signs of the math mode. This is the only difference between the two delimiters in this case.
It is important to define in the grammar all the syntactic elements that appear within the delimiters. Only the numbers, and a few characters ('[ ] ( ) , . ; *' are automatically defined.
Within the delimiters, the use of double quotes tells antelatex not to interpret a chunk of text. Antelatex surrounds that bit with \mbox.
[[2 "is" 2]]
is translated in
$2 \mbox{is} 2$
Within the delimiters, portions that are within (* and *) are considered as comments and are not substituted.
antelatex can help you write and read your LaTeX formulae more efficiently. antelatex cannot handle macros with optional arguments. antelatex allows to go around the LaTeX syntax (notably with the braces and backslashes) for some complex macros. antelatex cannot do conditional compilation, like some other pre-processors, although antelatex substitutions can introduce LaTeX conditionals. antelatex can prevent some mistakes by checking that antelatex macros are applied with the correct number of arguments. antelatex cannot check that the substitutions you define make sense.