graymalkin / bohm Goto Github PK

This is a restoration attempt for the Bologna Optimal Higher-order Machine,
which was originally written between '95 and '97. The source is still available
from the University of Bologna, but I have had to make some changes to restore
it to working condition. The original README file is below.

/***************************************************************/
/*		             README 			       */
/***************************************************************/

The Bologna Optimal Higher-order Machine (BOHM) is a prototype
implementation of an extension of a variant of Lamping-Gonthier's
optimal graph reduction technique to a lambda-calculus enriched with
primitive data types (boolean, integers, and lists).

BOHM has been developed by A.Asperti, J.Chroboczek, C.Giovannetti,
C.Laneve, P.Gruppioni and A. Naletto at the Department of
Mathematics of the University of Bologna, Italy.  The main authors can
be reached by e-mail as <[email protected]>.

The machine reduces terms to their weak head normal forms,
according to a lazy-family strategy (i.e. it always reduces the
whole redex-family of the leftmost outermost one, until a weak
head normal form is reached).

This work has been partially supported by

	   ESPRIT Basic Research Project 6454 - CONFER.



INSTALLATION

In order to compile BOHM, simply cd to the directory where you
untarred the distribution and type:

  make

or

  make CC=gcc CFLAGS=-O2

if you want to use the GNU C compiler.  This step will create an
executable called `opt'.  You may always return to the original state
of the distribution by typing

  make distclean

USAGE

Calling opt will open an interactive environment. You may now
introduce a term ended by a double semicolon, that will be immediately
reduced by the interpreter.

The source language is a sugared lambda-calculus enriched by primitive
data types and basic operations over them:

- Integers and mathematical operations.
- Booleans and relational operations.
- Lists and related operators.
- Fixed point operator for recursive definitions.

More precisely, the syntax of expressions is given by the following
grammar: (out of date -- no patterns, no tuples)

     <expr> ::= <expr0>
        |  <expr> < <expr>
        |  <expr> == <expr>
        |  <expr> > <expr>
        |  <expr> <= <expr>
        |  <expr> >= <expr>
        |  <expr> <> <expr>
        |  <expr> + <expr>
        |  <expr> - <expr>
        |  <expr> * <expr>
        |  <expr> div <expr>
        |  <expr> mod <expr>
        |  - <expr>   	

     <expr0> ::= true
        |  false
        |  <num\_const>
        |  <identifier>
        |  (<applist>)
        |  \ <identifier> . <expr>
        |  let <identifier> = <expr> in  <expr>
        |  rec <identifier> = <expr>
        |  if <expr> then  <expr> else  <expr>
        |  <expr> and  <expr>
        |  <expr> or  <expr>
        |  not <expr>
        |  <list>
        |  cons (<expr>,<expr>)
        |  head (<expr>)
        |  tail (<expr>)
        |  isnil (<expr>)

    <list> ::= nil
	| [<exprlist>]

    <exprlist> ::=                  (* empty *)
        | <expr>
	| <expr>,<exprlist>
        | <expr>|<expr>

    <applist> ::= <expr>
       |  <applist> <expr0>

The <expr0> nonterminal represents an expression that cannot begin
with a unary minus sign; it serves to avoid conflicts between f(-g)
and (f-g).  Remember to paranthesize arithmetic and boolean
expressions when passing them as an argument to a function.

Furthermore, any string between `{' and `}' is treated as whitespace.

See the subdirectory "examples" for some examples of programs.

There is also a global let instuction, to build up a global
environment. The syntax for such a global declaration is:

	def x = e ;;

The exact semantics of the def declaration is subject to change;
beware of name collisions!

The directive

	#quit;;

terminates the session (you may also quit by typing ^D).

After compiling a term, you may visit its graph representation by
typing the directive

	#inspect;;

This enters in "inspection mode". You are at the root form of the
term. To move along the graph, type the number of the port you wish to
exit through: you will move to the next form connected with the
previous one at the specified port. You may also inspect a previously
defined term, by typing

	#inspect term_name;;

You may also save it typing the directive

	#save file_name;;

for the last term; otherwise for a generic term

	#save "file_name" term_name;;

The directive

	#load "file_name";;

allows the user to compile an external file file_name.

The directive

	#option;;

allows you to choose a garbage strategie during execution, by
presenting a series of menus containing the possible modalities.  Such
menus can also be obtained at the beginning of execution by calling
opt with option "-s".

Garbage collection can also be explicitly invoked by the user by
calling the directive

	#garbage;;

The interpreter also displays some data about the computation, such as
the dimension of the graph or the time required for reduction.  These
informations can be viewed by typing the directive

	#info;;

and selecting the parameter of interest from the displayed menus.
These menus are also presented if the program is called with option
"-i".