Features of Alfa
Alfa is a largely inspired by
implemented by Lena Magnusson
and Johan Nordlander, and has a similar user
The plan is that Alfa should improve on Window-Alf by
Many of these features are available in the current version of Alfa, although
some of them are still in a experimental stage of development.
- allowing the user
to define how proof terms should be presented on the screen (and on
paper). This includes simple things like argument hiding and
but also more advanced mathematical notation and natural deduction
style proof trees and other representations of proofs. Alfa should
also allow you to produce documents where explanatory text and
proof fragments are interleaved.
- using ideas from hypertext and Web browsers to allow the user
to efficiently navigate through large proofs and libraries.
Below you can read more about:
- uses the proof engine Agda by
Catarina Coquand, based on V3 by
Thierry Coquand. Alfa uses Agda's
parser and pretty printer when loading and saving files.
- allows some editing operations not directly supported by the
proof engine: deleting expressions and declarations, adding new
declarations to let expressions and at arbitrary places in the
top level declaration sequence.
- supports argument hiding and infix operators with user defined
precedence and associativity.
- allows you to construct proofs in natural deduction style.
- supports cut-and-paste of expressions and declarations.
You can move expressions between Alfa and an ordinary text
editor (e.g., emacs).
- has an undo/redo history mechanism.
- has a simple module system. When loading a module, other modules
it imports are automatically loaded as necessary.
less switching between keyboard
- For most editing operations, you can choose to perform it
either with the mouse or with the keyboard.
- You don't have to move the pointer to a pop-up window to
enter text in it.
- When loading files, syntax error reports include file name,
line & column number.
- When entering expressions as text, immediate syntax checking is
performed and feedback is given via a smiley.
- works on both color screens and black & white screens.
Before you start playing with Alfa, please note that Alfa
- has some known bugs. See the
Known Bugs page.
- doesn't fully support all of the features of the language
defined by Agda. For example, there is no command to create package
- The built-in formatting is sometimes rather stupid
(produces very long lines).
- doesn't allow all kinds of expressions and declarations to be
entered using the
mouse. Instead you have to enter the text representation in a
pop-up window. This currently affects package/record field selection,
open declarations, and probably some more I forgot.
- does not warn you about destructive operations, like
quitting without saving or overwriting existing files. Destructive
editing operations can be undone and redone using the undo/redo history.
- has a command to ask for the type of an arbitrary subexpression, but it
doesn't always work because of limitations of the type checker.
- does some unnecessary redrawing of the screen, e.g., when you
delete a declaration or expression or when using undo/redo.
- needs to be made more efficent
(both the proof engine and the user interface code). Alfa has
some space leaks, so you have to restart it every now and then.
- everything about Alfa is still very
preliminary. Don't take it for granted that you will be able to
load documents saved with the current Alfa
in future versions of Alfa.
(Not updated recently.)
was implemented in
Standard ML (proof engine) and C++ & Interviews (user interface),
Alfa is implemented entirely in
using Fudgets for the user interface.
The source code currently
(16 April 1996)
consists of about 6000 lines, distributed as follows:
Update 10 April 1997: The total size now is 9500
lines. This includes 2100 lines from
Aarne Ranta with
support for natural language.
- The proof engine by
2400 lines. Includes parsing and parser combinators (450 lines).
- Extensions and improvements of the Fudget library. 1900
lines. The largest part of this is the new fudgets for
displaying structured graphics and syntax-directed editing. It
also includes a new file selection window and a string entry window
with immediate syntax checking and feedback via a smiley.
Although the development of these were prompted the Alfa project, they
are of course general enough to be used in other contexts.
- The Alfa User Interface. 1900 lines. The largest parts are the
implementation of the WYSIWYG style editing operations (600
lines) and the code for drawing/building abstract syntax trees
used by the syntax-directed editor fudget (350 lines).
Update 18 March 1999: The total size now is 16738
lines. The proof engine (Agda) consists of 9999 lines. The rest, 6739
lines, is user interface stuff. (Aarne Ranta's stuff is currently not
part of Alfa.)
Update 27 February 2000: The total size now is 18756 lines.
Agda consists of 10548 lines. The user interface is 8208 lines.
GF, which is included through the plugin interface, is 5802 lines long.