Alfa

History of Changes for 1999

990115

In addition to Set (#0) and Type (#1), Alfa now understands #2, #3, and so on.
When you zoom in to a Natural Deduction style proof, it is placed at the bottom of the window. This is more natural, since proofs grow upward.
I case your mouse doesn't have a middle mouse button, you can now use Ctrl+Left Mouse Button instead.
Two new commands to add and remove type signatures are now available in the menu window when one or more declarations are selected. The type checker may fail on the resulting declarations, in which case you get an error bar.

990127

Alfa now preserves comments in a lot more places than before. (Before, only comments between top level declarations were preserved.) But there are some cases when Alfa has to use the output of the proof engine where comments and some syntactic sugar have been removed.
The above also means that layout and hiding options are preserved in saved documents.
There are some new commands to choose in what level of detail a declaration is displayed. These appear in the menu window when one or more declarations are selected. The default setting can be changed with some new alternatives in the View menu.
Bug fix: the settings shown in the View menu are now updated to reflect the new settings after the New or the Open... command has been used. (See the 970902 entry.)

990128

You can now edit declarations as text. You can also insert and edit comments between declarations.
When editing expressions and declarations as text, you now get a multiple line text editor. In most other cases when you enter text you get the old single line editor. In the latter case the Return is a keyboard shortcut for the OK button, while in the former, you have to press Meta-Return. (The command line option -multiline no longer has any effect.)

990209

Alfa now support declaration properties (abstract/concrete/private/public). New commands for changing the properties of declarations appear in the menu window when one or more declarations are selected.
The drawing of quantifiers changed. Since the lambda abstractions now are typed, Alfa uses this type when displaying the domain of quantification. Quantifiers are thus expected to have exactly one visible argument. You can now choose, in the layout editor window, whether the domain of quantification should be visible or not.

Example:
Visible domain Hidden domain

990219

Bug fix: Alfa used to save layout options for top level identifiers only, but now all layout option settings are saved. For example, you can now set layout options for things defined in packages.
Bug fix: you can refine by clicking with the middle mouse button on a constructor.
$ is no more! One (the last?) remnant from the V3 proof engine is gone. (In the V3 syntax, all constructor names began with $, and this still showed up in some places in Alfa.) (The command line option -boldconstrs no longer has any effect.)

990223

Bug fix: when loading files, Alfa swapped the arguments of infix operators.
There is still no efficient way for Alfa to ask the proof engine for the type of an arbitrary expression, but there are two new ways to make Alfa display the type of a selected expressions:
- After a place holder has been instantiated, you can select the resulting expression to see its type. (Alfa remembers the number of the place holder and uses this to ask the proof engine for the type.)
- If you want to know the type of a selected expression and Alfa doesn't show it, you can use the new command Type of this expression?. This is a bit inefficient and currently doesn't work for all kinds of expressions.

990313

Some support for packages:
- Added commands for creating package declarations. These appear in the menu window together with commands for creating ordinary declarations.
- Added a command for creating open expressions. It works the same way as the command for creating case expressions. It allows both packages and structures to be opened.
- Shift-clicking with the middle mouse button on an identifier now creates either a case or an open expression, depending on the type of the variable.
To do: add a command to create open declarations. Make it possible to choose what to use when opening a package. Add commands to create package instance declarations.
Slightly more flexible cut-and-paste of expressions and declarations: trying to paste declarations where an expression is required creates a let expression and vice versa. open declarations/expressions are recognized as a special case.

990316

Bug fix: Alfa now preserves comments between local declarations, not just between top level declarations.
In the Evaluate Expressions windows, there are now extra buttons to step through the evaluation of the expressions.

990317

Changed the display of constructor applications: layout options now apply in the same way as for ordinary function applications. (Before, constructors could be made infix, but other layout options were ignored.)

990324

GUI: there is now a "split bar" between the main editing area and the info display at the bottom of the window. By dragging the spit bar, the user can control the size of the info display.
Experimental: there is now a command to run the termination checker on selected declaration(s). This will give an error message if you check a declaration that seems to use infinite recursion. If the definitions seems OK, nothing happens. Note: The termination checker is work in progress!

990503

Changed the presentation of quantifiers without domains to agree more with the notation found in modern literature on logic. (Suggested by Eric Palmgren.)

Example:
Old New

You can get back the old notation by using the flag -quantifierdots.

990506

Alfa now displays a version number on stdout when it starts and in the main window title bar.
Added a parameter in the start script alfa to specify a bitmap directory. This should be changed when installing Alfa on systems where X11 bitmaps aren't located in the usual place (i.e., /usr/X11/include/X11/bitmaps/).

990619

The contents of packages is now shown also when "Show type signatures only" is in effect.
The equals symbol in definition is now the one with three lines instead of the usual one, = with two lines.

990625

Magnus added the button Cwd in the file selection window. This takes you to the current working directory. (It can be turned of with a setting in the script alfa.)

990705

Magnus has fixed some bugs in HBC's generational garbage collector, so hopefully, it will not cause Alfa to crash anymore.
An Options menu has been added. It presently contains commands for switching between two input modes: abbreviation mode, which is the usual mode, and completions mode, which is a new experimental input mode. There are two advantages with the new mode:
- You don't get the problem with dynamically changing abbreviations, so you don't have to look in the menu to find out what keys to press if you know the name of something you want to use.
- When you edit large documents, the menu can become quiet slow, and with completions, the menu is only generated on demand, and then only to show possible completions, so it doesn't necessarily have to show everything in scope.
(Completions mode actually has been available through a command line switch for some time. You can now switch it on and off dynamically, and it has also been slightly improved.)

990809

Added two quick reference pages to the documentation: Overview of the menus and Command line syntax and options.
The Options menu contains new settings corresponding to the command line option -untypedmenu. The setting Show everything in scope is now the default, since...
...each item in the menu window is now preceded by a status light, which is green if the command is applicable, and red if it is not. This means that at the same time as you can see the type of all identifiers in scope, you can see which identifiers can be used to refine the selected goal. The colors of the status lights are computed lazily, so no time is wasted on status lights that aren't visible.

990810

The number of hidden arguments now affect also how the type signature of a function is printed, not just how function applications are printed.

Example:
Old:
New:
This applies to type signatures in the menu window too.
Added the option Show everything, no status to the Options menu.

Example:
Old:
New:

990811

Added the option Auto Solve Constraints to the Options menu.

990813

Alfa now displays a message in the info display after a successful termination check and after a file has been successfully saved.

990818

Catarina has extended the termination checker to check that data type definitions doesn't contain negative occurences of the type(s) being defined.
Syntax change: data, sig and case expressions are now restricted to occur only at the top level of expressions. This means that expressions of these kinds can always be referred to by name, which is good, since the type checker uses name equivalence.
The error messages from the termination checker are now slightly more informative.

990820

Added commands for creating open declarations. Known bug: the declaration is always created in the top level environment, so it might not work properly in other places.
Added support for "independ" function types (where the argument does not have a name).
Added rewind and fast forward buttons to the Evaluate Expressions window.

990827

Various small proof engine and user interface improvements and bug fixes has been made during the week, as part of preparations for the Types Summer School.

990902

Alfa now searches for imported files both in the directory of the imported document and in the library directory (i.e., the directory selected by the Library button in the file selection window).
Added support for "distfix" operators (aka mixfix operators). They are activated by selecting the alternative Distfix operator, use _ in name in the Layout Editor. The name of the operator is expected to contain a number of _ (underscores), indicating the placement of the arguments.

990910

Added the command Browse... to the File menu. This allows you to open an arbitrary fiel in the browser menu.
Added a File menu to the browser window. Like the editor's File menu, it contains a command to browse arbitrary files. It also contains a command to open the currently displayed file in the editor.
Added the command Auto Scroll to center cursor to the Options menu. Previously, Alfa tried to keep the cursor in the center of the window, but some users thought things jumped around too much. With this option turned off (which is the default) things jumps around less, but the cursor may end up close to the edge of the window most of the time.

990917

Alfa now allows local definitions in signatures, but there are no commands for inserting them, yet.
A pretty printing bug affecting structures and definitions in signatures was corrected.

991015

Bug fix: when opening a file, type errors in imported files were silently ignored. Now they are reported, and the file isn't opened.
Alfa now retains some position information, to make error messages that refer to things in imported files more informative.
Error messages shown at the bottom of the editing window are now also copied to the standard output.

991016

To make it easier to distinguish the builtin language constructs from user defined syntax, keywords and delimiters are now shown in a different color (dark brown by default). The color can be changed with the new command line option -keywordcolor.

991018

Changed the syntax for layout options in saved files. The new format is intended to be human readable and easier to extend in a backwards compatible way. The old format is still recognized.
Bug fix: layout options for constructors and variables of the same name can be set independetly again.

991213

Bug fix: Alfa sometimes changed expressions of the form let x=e in x into let x=e in e.