Alfa

Printing

Alfa supports printing proofs on paper by providing a command to generate LaTeX code from Alfa documents.

There are two ways to print a document:

From an interactive Alfa session: a document can be printed by opening it in Alfa and then selecting the command Print To File... from the File menu. Alfa then suggests a file name ending in .tex in which the LaTeX code will be put.
You can also print directly from the command line, without starting an interactive Alfa session, by starting Alfa with the command line option -print. For example, the command
alfa evenodd.alfa -print
will save LaTeX code for the Alfa document evenodd.alfa in the file evenodd.alfa.tex.

The LaTeX code produced by Alfa is designed to be self-contained, but it is not a complete LaTeX document, but rather someting that can be used as part of an article (for example), by including it in the article with the LaTeX command \input.

Example

Assume we want to print the example from the keyboard tutorial, which in the current version of Alfa would look something like this on the screen:

We would then use the Print To File... command in the File menu to obtain a LaTeX file called (for example) evenodd.alfa.tex.

As the next step, we create a main LaTeX file in which we include evenodd.alfa.tex:

Assuming we store this in a file called tst.tex, we can obtain a DVI file with the command

latex tst

and a PostScript file with

dvips tst.dvi -o tst.ps

Take a look at the result:

User influence on how things are printed

The LaTeX code generated is designed to closely resemble what you see on the screen. This means that user defined layout options (argument hiding, infix operator precedence, quantifier notation, etc) are taken into account.

In addition, most of the options in the view menu, and layout options set for individual definitions and expressions, affect what is printed. This is particularly useful in combination with plugin modules that provide alternate views of expressions and definitions. For example, the GF Plugin allows you to produce natural language translation of proofs.

Comments

Any comment in the Alfa document is assumed to contain correct LaTeX code and is thus copied as is to the LaTeX file. This allows you create, e.g., section headings by including them in comments.

LaTeX macros

Alfa uses a small number of LaTeX macros with default definitions that you can override by providing your own definitions:

alfaimport: This macro defines how import definitions are printed. The defualt is to print them as import filename.
alfadeclcomment: This macro defines how comments between definitions are printed. The default is to print them as the are.
alfaexpcomment: This macro defines how comments in expressions are printed. The default is to print them as the are.

As an example, to print comments between definitions in italic, you could include the following definition in your main latex file (the LaTeX file generated by Alfa can be left unchanged):

\newcommand{\alfadeclcomment}[1]{\it #1}

Limitations

LaTeX printing was added to Alfa fairly recently (September 2000), and still has some limitations.

Alfa makes extensive use of math mode in the generated LaTeX code. Unfortunately LaTeX doesn't make any clever choices as how to layout things to make them fit on the page in math mode, so big definitions can easily become too wide or too tall. This almost inevitably causes problems when you print natural deduction style proofs.
Although the layout editor allows you to use arbitrary characters from the Latin1 and the Symbol character sets in identifiers, only a small subset of these can be translated into LaTeX.

Hopefully, this can be improved in a future version of Alfa.