Previous Up Next

3  User interface

When you run Bedwyr, you specify a list of definition files, which contain objects to be declared and defined. You can then use the toplevel to ask queries against those definitions.

There is also a special brand of commands, meta-commands, which can appear anywhere.

As a general rule, any kind of input ends with a full-stop. Commands start with uppercase letters, meta-commands with hashes, and queries are just formulae.

3.1  Definition files

Definition files are usually named with a .def extension. You can find several of them in the examples/ directory of the Bedwyr distribution. They contain declarations for types ( Kind <id> type.), declarations for constants ( Type <id> type.), declarations and definitions for predicates ( Define <id> : <type> by <definitions>.), and theorems ( Theorem <id> : <formula>.).

The only meta-command that is really intended for definition files is the include command: #include "another/file.def". This can really be seen as the plain inclusion of another file, as Bedwyr doesn’t have any namespace or module system. If the path is not absolute, it is relative to the path of the current file, or the execution path for the toplevel.

3.1.1  Emacs mode

Assuming Bedwyr is installed in standard Linux system folders, you can use the Emacs mode for Bedwyr by adding these two lines to your  /.emacs file:

(load "/usr/share/bedwyr/contrib/emacs/bedwyr.el")
(setq bedwyr-program "/usr/bin/bedwyr")
;; Of course you can change both locations to wherever you want.

Then you should be able to load any .def file and have syntax highlighting and some rough auto-indenting. Also if you do C-c C-c it will start Bedwyr and load the current file you are working on.

3.1.2  Vim syntax highlighting

There is also a basic syntax highlighting file for Vim. With a standard system installation, the files /usr/share/vim/vimfiles/[ftdetect|syntax]/bedwyr.vim should suffice; otherwise do the following:

3.2  Toplevel

The interactive toplevel is automatically launched once the files have been parsed, unless the flag -I is passed to Bedwyr. In it, you can either query a formula, or run a meta-command. In queries, free and bound variables are the only objects that can be used without prior declaration, and the solutions are displayed as instantiations of free variables.

Queries can also be given in batch mode, to a non-interactive toplevel, via the command-line option -e (e.g. bedwyr -e 'X = 0.'). In this case, they are processed after the files and before the interactive toplevel.

In 1 we load a set of definitions and prove (twice) that the untyped λ-term λ x.x x has no simple type.


Listing 1: Run on examples/lambda.def.

?= (exists T, wt void (abs x\ app x x) T). No. ?= (exists T, wt void (abs x\ app x x) T) -> false. Yes. More [y] ? No more solutions. ?=

Notice that we had to use the term (abs xapp x x) instead of (x1x1 x1): the former encodes the untyped λ-term λ x.x x by mapping object-level abstraction to abs and object-level application to app, while the latter would map them directly to logic-level abstraction and application, and therefore is not a legal term in Bedwyr. (Prior to version 1.3, this was allowed as Bedwyr did not use simple typing on its own terms.)

Most of the errors that can stop the reading of a file (parsing or typing error, undeclared object, etc.) are correctly caught by the toplevel, though the line number reported for the error is often not useful.

3.2.1  Line editing

Bedwyr has no line editing facilities at all. Thus, we recommend using ledit or rlwrap, which provides such features. Get one of them from your usual package manager or at http://pauillac.inria.fr/~ddr/ledit/ or http://utopia.knoware.nl/~hlub/rlwrap/#rlwrap.

Then you can simply run ledit bedwyr. One can also define an alias in his  /.bashrc, such as the following which also makes use of  /.bedwyr_history to remember history from one session to another:

alias bedwyr="ledit -h ~/.bedwyr_history -x /path/to/bedwyr"

3.3  Meta-commands

Meta-commands are used to change the state or the program, or for non-logical tasks. They can be used any time a command or query is allowed.

3.3.1  Session management

Those commands alter the set of definitions the current session of Bedwyr holds. An empty session actually means that only pervasive types, constants and predicates are known. The session’s initial state is the list of files given on the command-line, and it can grow anytime with the use of #include. It should be noted that, although Bedwyr has no solid notion of what a module is, it tries to do the smart thing by ignoring the request to include a file if it appears to be already loaded in the current session, as failure to do this would result in fatal multiple declarations. This only works if the same path is used for each inclusion; for instance, ./file.def and file.def will be seen as different files.

3.3.2  Assertions

Three kinds of assertions can be used in definition files. These tests are not executed unless the -t flag has been passed on Bedwyr’s command-line, in which case any assertion failure is fatal.

Our examples include a lot of assertions, to make sure that definitions have (and keep) the intended meaning. These assertions are also the basis of Bedwyr’s correctness and performance tests ran using make test.

3.3.3  Other commands


Previous Up Next