Alfa

History of Changes for 1996

960220

• When deleting expressions, only the deleted expression is redrawn. (Before, the entire document was redrawn.) (Quick fix, needs to be verified.)
• When deleting expressions, the cursor is placed on the newly created place holder rather than on some other place holder.
• When the last goal is instantiated, the resulting expression remain selected. (Before, the entire document became selected.)
• Shift-Space now jumps to the previous place holder. (Space without shift jumps to the next place holder as before.)
• The type display below the editing window no longer steals keyboard focus.
• New menu entry "Function Type with given names".
• When a place holder (near the edge of the window) is instantiated Alfa tries to make the new expression visible, not just the subexpression where the cursor is placed.

960221

• Strings in popup windows are now selected when the window pops up, so that you don't have to erase them manually to enter something new.

960222

• Compact notation, (a:A, b:B) -> C and \ a b -> c, is implemented. It can be switch on/off from the new View menu.
• Argument hiding is now supported. The number of hidden arguments for an identifier can be set by clicking on the binding occurence of an identifier and selecting Change hiding from the editing menu. Hiding can be globally whiched on/off from the view menu. Note that argument hiding is a lexical property of an identifer. It applies to all occurences of the identifier.

960225

• Improved the efficency of layout compuations by 30% by using customized placers.
• Compact notation: now printing (a1:A, a2:A) -> B as (a1, a2:A) -> B. BUG: if you change A to A' you will see (a1,a2:A') -> B but you get (a1:A, a2:A') -> B. (Some extra redrawing is needed.) Workaround: select the type and pick Redraw from the View menu after such a change (or switch off compact notation).

960226

• There now are (invisible) place holders between declarations on the top level. This allows you to insert new declarations anywhere. You can also copy and paste declarations.

960229

• Better parser. Syntax errors are reported with line and column indications.

960304

• All input in popup windows is now immediately check for syntax errors. A "smiley" indicates whether your input is correct or not. If an error is present when you press Return an error message is shown in the popup window and the cursor moves to the position where the error was detected. (Before, errors were reported in the main editing window, after the popup window disappeared.)
• The Intro command can now introduce theories.

960308

• A simple module system is now available. A new Import... command is provided in the File menu. When loading a module (file), all directly and indirectly imported modules are also loaded.
• The file menu now has both Save, which saves the current module to the file it was loaded from, and Save As..., which allows you to choose a different name/place using the file selection window.
• While testing Alfa, I encountered problems where the proof engines allow you to construct type incorrect terms. The proof engine may also loop when trying to construct certain type incorrect terms. These problems are not fixed yet. The flag -simplerefine removes some looping problems, but not all.
• Bengt presented the following pathological, but correct declarations:

  Nat = data {$true , $false } : (Set),

Nat = Nat : Nat

960312

• Applied Thierry's fix for the problem where type incorrect terms could be constructed.
• Added more explanatory text in some popup windows.

960326

• Name of file being edited is now shown in the window title.
• Some error messages that were shown on stderr are now shown in the main editing window.
• Added keyboard shortcuts to the menus (File, Edit and View). Use the Meta key or the Control key together with the key indicated in the menu.
• Some editing operations were moved to the Edit menu.

960327

• Parser now understands goals in square brackets. Any text inside the square brackets is ignored.
• You can now delete expressions and declarations with the BackSpace key and the Delete key.

960328

• Rewrote the expression parser. Syntax change: a b.c now means a (b.c). (Before it meant (a b).c).

960329

• Bug fix: import file names are now interpreted relative to the directory of the importing file.

960330

• Implemented Undo/Redo. At present you can even undo the New and Load commands. This means that Alfa may run out of memory if you do Load very often. The length limit of the undo history has (arbitrarily) been set to 10 steps. The Undo/Redo commands redraw the entire window.

960422

• Alfa sources have been converted to Haskell 1.3. (User should not notice any difference.)

960430

• Alfa now use Half syntax for equality constraints in data expressions. The editor has no commands for editing them, but they can be entered using the Give command. For example, to define the Id relation,

  Id (A:Set,x:A,y:A) = data {$Ref <x=y>} : Set,

  you would enter data {$Ref <x=y>} using the Give command.

960522

• Alfa has been adapted to Fudget version h10. (No user visible changes.)
• To reduce mouse movements, the commands in the menu window are now available in a pop-up menu as well. Use the right mouse button.

960612

• Added the Utils menu with the command Evaluate Expressions. This command pops up a window where you can enter expression to be evaluated. If you select a place holder first, the expressions will be evaulated in the context of that place holder.
• Increased the default heap size to 25MB.

960612

• Fixed a bug that caused the Import... command in the File menu to access the imported file via a relative path and sometimes fail to find it.

960618

• Added simple infix notation. Symbolic identifiers, i.e. sequences of the characters ! % & * + - / ? @ ^ | ~ = < > ., are allowed. When they occur applied to two (unhidden) arguments they will be displayed as infix operators. For example, instead of + (+ a b) c, you will see (a + b) + c.

960627

• Arbitrary identifiers can now be turned into infix operators. You can also set the precedence and associativity. This works as an extension of the argument hiding mechanism. Hiding info in files saved with older versions of Alfa will not be understood by this version. (There is still a problem with this info being saved in more than one file.)
• Some new editing operations:
  • Inserting new declarations at arbitrary places in let expressions.
  • Replacing an arbitrary expression e with let decls in e.
  • Pasting sequences of declarations instead of just one declaration.

960705

• You can now replace an expression or declaration by pasting. You don't have to delete it first.
• Added the command Abstract many to abstract as far as possible. Removed the old command Abstraction since Intro does the same thing for goals of function type.

960707

• You can now refine a goal by clicking on a any name with the middle mouse button.

960708

• Bug fix: the default text in popup windows wasn't always selected initially. (See 960221.)

960714

• More functionality on the middle mouse button:
  • You can click on an import declaration to view the imported module in a separate window.
  • In addition to clicking on a name to refine a goal you can now also construct case, let, data expressions, etc, by clicking on existing expressions.
• You can now convert declarations back and forth between the forms

  f = \ x1 ... xn -> e : (x1:A1,...,xn:An) -> B

  and

  f (x1:A1,...,xn:A2) = e : B

  Alfa currently provides no editing operations on the parameter list in the second form (except for editing the expressions A1 ... An).
• Fixed some (but not all) space leaks.
• A new command Edit as text is available when an expression is selected. It allows you to edit an expression in the build-in one-line string editor. Large expressions can be edited in any external text editor by using Copy/Paste.

960830

• Fixed a bug in the lexical analyser that caused the parsing of equality constraints in data expressions to fail.

960911

• The file selection window now supports file name completion. Type the beginning of a name and press Space to have it completed. If there are several possible completions, they are highlighted in the directory listing. You can also use the Up/Down arrow keys to walk through the directory listing.

960919

• Preliminary support for building in proofs Natural Deduction style is now available. The terms have to be build in a special way by using the ND Style let command in the menu at every new subgoal. (This is meant to be automated...) There are some new alternatives in the View menu for choosing between different proof styles.

960925

• Renamed the File menu command Load... to Open.... Changed the keyboard shortcut to O.
• Added a new button Library to the file selection window. This takes you to ~/etc/Alfa/Library if you have such a directory, otherwise /usr/local/lib/Alfa/Library.
• The command line flag -untypedmenu makes the menu show all identifiers in scope instead of only those that can be used to refine the current goal. (This seems to be faster although the menu usually becomes larger.)

960926

• Alfa now preserves and displays comments between top level declarations. The comments can not be edited inside Alfa yet, but you can use copy/paste to edit them in an external text editor.
• Added the command line options -fontfamily and -commentfont. (See the User's Guide.)

961004

• Alfa now uses John Hughes' pretty printing library to produce more readable text in saved files.

961226

• Improvements from the latest version of Fudgets: better looking scroll bars; the main editing window no longer grows larger than the screen because of big constraints.
• Comments before includes are now discarded instead of causing a syntax error. (This is a temporary fix. They should of course be preserved.)