Alfa

History of Changes for 1997

Thanks to an optimization in the Fudgets library, drawing operations are now a lot faster. Redrawing the window (e.g., after using the PageUp or PageDown key) now usually takes less than 0.1s instead of 0.5s-1.0s.

Preliminary support for creating "big" operators is now available. For examples, see the file nat in the Examples directory in the standard library.

Documents can now contain unckecked declarations, i.e., declarations that aren't accepted by the type checker. Unchecked declarations are created
- when you load a file containing type errors. (Before, the editor refused to load such files, and the error message did not include an error position.)
- when you delete something that is needed to type check a later declaration.
An unckecked declaration is marked with a fat, red vertical bar. An error message is inserted as a comment before the first unckecked declaration. At present, when an erroneous declaration is encountered, all declarations after it are left unchecked too.
A limited set of editing commands, Give, Paste & Delete, are available inside unchecked declaration. There is also a command Check Again that re-checks a declaration and possibly returns it to the normal (checked) state.

The algorithm that computes the keyboard shortcuts for the menu window has ben replaced. There are two improvements that makes the shortcuts easier to use:
- It doesn't assign the same shortcut to two different menu items anymore.
- A shortcut always starts with the same character as the name it abbreviates.
A preliminary alternative editing mode can now be activated with the -completions flag. In this mode, a string entry field appears on top of a place holder when you select it. In it, you can enter a name to refine with (more precisely, any command that would be shown in the menu window in the normal mode). The Space bar is used for completion (e.g., filling in the remainender of a name if there is only one possible alternative, or listing the possible alternatives). You sometimes need to use the Tab key to activate the string entry field.
You can now use the Page Up/Down keys to scroll the document without having to activate the scroll bar first. Shifted Page Up/Down scrolls horizontally.

The algorithm that converts goal types from the proof engine's internal representation to human readable form has been improved (thanks to Magnus Carlsson). There is a new setting that can be changed from the View menu: Unfold goal types use definitions to unfold applications in goal types as far as possible. Don't unfold goal types does not unfold applications. The former option usually unfolds more than desirable, the latter less than desirable. A future version of Alfa will give the user much finer control of the unfolding.
Experimental feature: you can enter types in natural language by using the command Give in English. This uses Aarne Ranta's natural languages parser. It has a limited vocabulary: it understands some arithmetic and geometry. See Ranta/REAMDE for further information. The file Ranta/arithm.half contains some definitions referred to by the parser output.

You can now unfold/fold expressions in the goal type/constraints display and in the Evaluate Expressions window. Click on the small dots.

Added support for infix operators with 3 or 4 operands. Operands appear above and below the operator in addition to left of and right of it. (This will be replaced with some more general layout specification mechanism at some time...)
The pretty printer no longer puts superfluous parentheses around kind names (as in (Set), (Type)) in the text representation of expression.
More support for natural language: when an expression is selected, its translation into english is shown, if possible.

Improved layout: thanks to the introduction of reference points in the Fudget layout system, it is now possible to do base line alignment. Visible effects of this include improved positioning of characters from the symbol font (which are slightly smaller than ordinary characters) and more readable layout of let expressions.
There is now a choice between tall and wide layout for expression (currently implemented for case, data, struct and sig expressions). The default layout can be selected from the View menu. The layout of an individual expression can be changed by selecting it and choosing a new layout from the menu window. Layout options are not saved yet.

Hiding expressions: in addition to the argument hiding mechanism, there is now a command to hide individual expressions. Just select an expression and pick the new command Hide expression in the menu window. Use the Reveal hidden expression command to reveal the expression again.
Compact printing of nested case expressions. When the View option Compact Notation is on, nested case expressions are collapsed into single case expressions with nested patterns.

Example:
Normal Compact

More functionality on the middle mouse button: you can create case expression by shift-clicking on a variable. By clicking on a variable in a pattern you can create a nested pattern.
Added the command Font Size... to the View menu. It allows you to change the overall size of the text in the editing window, as with the command line option -fontsize, without having to restart Alfa.

Adding and deleting constructors and branches: the menu now contains commands for adding and deleting constructors in existing data types and adding and deleting branches in existing case expressions. This is explained in the User's Guide.
The error bar is explained in the User's Guide.

Bug fix: changed the lexical analyser and the parser to distinguish between identifiers and constructors at an early stage. Before, constructors were accepted in lots of places where only identifiers should be allowed.
Bug fix: pressing the Down arrow key when a declaration is selected now moves into the declaration again. (Before, it didn't do anything.)
Right/Left arrow keys now move to the next/previous leaf in the syntax tree. This is much like moving from character to character in a text editor. The old behaviour is obtained with Meta-Right/Left and is useful when moving between adjacent elements in various kinds of lists (e.g., declarations, data constructors and case branches).
The tall/wide layout option is now also available for function applications (!), function types and theory expressions.

Alfa now automatically chooses between tall and wide layout for function applications and some other syntactic entities.
Hidden arguments are now completely invisible. (Before, they were represented by a ° characters.)

Improved the support for Natural Deduction style proofs. You now click on the command ND Style proof in the menu once before you start the proof. After that, it is enough to click on the names of the proof rules you want to use. (See the 960919 entry.) Remaining weaknesses: assumptions are still presented as lambda abstractions. The cursor often moves to uninteresting place holders when a proof rule has been applied.

Alfa now uses a new, more user friendly menu bar fudget. This means for examples that you can see what the current setting of all the options in the View menu are. (There are still some minur bugs to fix. For example, the settings in the View menu are not updated when a new document is opened.)

Bug fix: The Undo/Redo commands now undo and redo all the effects of the New and Open... commands. This means that Alfa shows the right file name in the window title bar and that the Save and Save As... commands save the document to the right file.