Features of Alfa

The plan is that Alfa should improve on Window-Alf by

• 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 infix operators, 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:

• Features
• Limitations of the current version
• The implementation of Alfa

Features

• 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.
• requires less switching between keyboard and mouse:
  • 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.

Limitations of the current version

• 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 instance declarations.
• 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.

About the implementation of Alfa

Whereas Window-Alf was implemented in Standard ML (proof engine) and C++ & Interviews (user interface), Alfa is implemented entirely in Haskell, using Fudgets for the user interface. The source code currently (16 April 1996) consists of about 6000 lines, distributed as follows:

• The proof engine by Thierry Coquand. 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.