Overview of the menus
Alfa's main editing window has a menu bar contaning the
Below, we give a brief description of the purpose of all the commands you
find in these menus.
The edit menu contains the following editing operations, some of which
should be familiar from other editors.
The last two commands are only applicable when a place holder is
selected, but there is no visual feedback for this at present.
- Undo and Redo. If the effect
of a command was not what you expected, you can undo it by using
the undo command. You can go back several steps (10 by default,
but you can change this with a command line option). If you went
back too far, you can go forward again with the
Redo command. An unusual feature of Alfa's undo
mechanism is that even the file menu commands
New... and Open... can be undone.
- Copy, Paste and
These are fairly standard, except that there is no Cut
command. Use Copy, followed by Delete instead.
- New Declaration.... This adds a top level
declaration to the end of the document. Futher commands shown in the
menu window allow you to insert declarations of various kinds, and
at arbitrary places.
- Give.... This command allows you to replace a place
holder with an expression entered as text. It is thus only
applicable when a place holder is selected. The expression can
contain place holders.
- Refine.... This commands allows you to replace
a place holder with an expression, applied to the appropriate number of
arguments determined by the system. This is the most common step
in proof development (since it corresponds to applying a proof
rule) and there are several, more convenient ways, to invoke
this command. (See
ways to fill in a place holder.)
These commands affect how you input commands when a place holder is
selected and what is shown in the menu window.
- This is the original mode,
where each command is assigned a unique keyboard shortcut,
which is displayed in the menu window. A
problem with this solution is that the abbreviations are
computed dynamically and the same command can be assigned
different abbreviations in different context. This means that
you have to look in the menu all the time to find out what to
type, and this slows down the editing. (The first character in
the abbriviation is always the same, so you can always enter the
first letter of an identifier without looking in the menu...)
- Completions (Under construction)
- In this mode, a text entry field appears on top of a
place holder when it is selected. You have to enter the
full commands, but there is a completion mechanism that
fills in the rest when you hit the Tab key, if there is
only one matching command, or displays a list of matching
commands in the menu window, if there are several.
The up/down arrow keys steps throuh the list
of available commands. You may
have to hit the F1 key to activate the text
entry field. (Clicking in the field doesn't seem to work...)
These options control what is shown in the menu window.
- Show everything in scope
- All identifiers in scope are shown. Status lights
indicate which identifiers can be used to refine the
selected place holder.
- Show everything, no status
- As above, but the status lights are omitted. Use this if
computing the status light is too slow.
- Filter through type checker.
- This is the original mode where only identifiers that
can be used to refine the
current goal are shown. This can be slow if there
are many identifiers in scope.
If Alfa becomes too slow when you make big proofs, selecting
and Show everything, no
is likely to make it a lot faster.
- Only refinements from context
- Although it is based on the lambda calculus, the expression
language used in Alfa is enriched with a number of
constructions, such as records, projections, data types, case
expressions and local definitions. With this option turned on,
most commands to construct these fancy kinds of expressions are
removed from the menu, leaving commands to construct terms in the
pure lambda calculus. This might be useful when you are working
with a plugin module based on a simpler expression language.
Plugin modules can supply alternative ways to display the commands that
appear in the menu window. These options allows you to select which view
- When no plugin modules are active, this is the only option.
(At the time of this writing, this possibility has been used
only in the GF plugin, which allows expressions to be translated into various
natural languages. This is why this options are referred to as languages.)
- Auto Solve Constraints
- When a place holder is
instantiated, constraints may arise on the possible values of other
place holders. When this options is switched on,
such constraints are solved and
the affected place holders are instantiated, in cases where this is safe,
i.e., there is really only one possible solution.
When this option is off, no constraints are solved automatically.
Instead, commands to apply the automatic solution appear in the menu.
You can also manually instantiate the affected place holder. This gives
you more control, e.g. if you have a definition
a = b
and a constraint
?1 = b,
the automatic constraint solver would instantiate ?1 to b, but
you might prefer to instatiate ?1 to a.
- Auto Scroll to center cursor
- With this option, Alfa tries to keep the cursor in the center of
the window. With this option turned off, the part of the
document you are working on might end up near the edge of the
window, making it difficult to see what you are doing. With this
option turned on, things might jump around too much.
These commands open (or close) auxiliary windows.
- Evaluate Expressions.
This command opens an auxiliary window where you can enter expressions
and evaluate them (compute their normal forms).
- Menu Window.
The menu window is opened automatically when Alfa is started, but if you
close it, you can re-open it with this command.