Fix: Creation of an empty entry

An empty entry in the proof context has to be created from scratch,
because it has mutable fields. If the entry is reused, it might no
longer be empty because the mutable fields might have changed.

	modified:   ocaml/proof_context.ml
Fix: Features do not arrive in ascending sequence

In the interface file the features can be defined in a different
sequence than in the implementation file. The class table stores
in each class the deferred and effective features in a list and in
a term table. But a term table requires that the terms added to the
table arrive in ascending sequence.

The bug has been fixed by introducing a wrapper for the term table which
stores the indices as they arrive in an array appending it to the end
and puts the array index of the appended element (which is guaranteed to
be ascending) into the term table.

	modified:   ocaml/class_table.ml
Fix: Do inheritance for exported features

Features which are defined in the implementation file and exported
in the interface file have to be prepared for inheritance:

- They have to be added to the features of the owner class
- If effective they have to be inherited to all descendant
  classes of the owner class (in case there are already
  descendants)

	modified:   ocaml/feature_table.ml
Minor edits (prints)

	modified:   ocaml/class_table.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/module_table.ml
	modified:   ocaml/proof_context.ml
A fix and check deferred features and assertions

Fix: All assertions which are exported in the interface file but
already present in the implementation file must be put into the
class table (deferred and effective assertions) and inherited to
descendants of the owner class.

All deferred features and assertions must be exported. This is now
checked at the end of the verification of interface files.

	modified:   ocaml/container.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Adapted printouts

	modified:   ocaml/class_table.ml
	modified:   ocaml/feature_table.ml
	modified:   ocaml/proof_context.ml
Added functions to 'Module_table'

	modified:   ocaml/module_table.ml
	modified:   ocaml/module_table.mli
New version of the compiler

'alba.ml' replaces 'eiffelc.ml'. 'eiffel.ml' is not yet removed,
but will be removed soon.

'alba.ml' does dependency checking and compiles only modules which
are affected by changes.

	new file:   ocaml/alba.ml
	new file:   ocaml/ast.ml
Compound module names introduced (name,lib)

A module name consists of a library part and a simple module name.
E.g.

    alba.base.boolean   -- lib = [alba,base], name = boolean

	modified:   ocaml/alba.ml
	modified:   ocaml/class_table.ml
	modified:   ocaml/class_table.mli
	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/module_table.ml
	modified:   ocaml/module_table.mli
	modified:   ocaml/parser.mly
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/proof_table.ml
	modified:   ocaml/proof_table.mli
Preparation for library usage

	modified:   ocaml/alba.ml
	modified:   ocaml/container.ml
	modified:   ocaml/module_table.ml
	modified:   ocaml/module_table.mli
	modified:   ocaml/parser.mly
	modified:   ocaml/support.ml
Libraries now usable

Each module can use modules of other libraries in its use block.
E.g. the statement

   use  alba.base.lattice end
   ...

uses the module 'lattice' of the library 'alba.base'.

	modified:   ocaml/alba.ml
Some more keywords reserved

assert, from, proof, variant, while

	modified:   ocaml/lexer.mll
	modified:   ocaml/parser.mly
Prepared term level calculation and refactored backward analysis of terms

1. There is still a potential infinite loop in forward and backward reasoning.
Currently a term is considered not more complicated than another if it has
not more nodes than the other. This should avoid that terms can grow
unlimited in the prover.

But due to function expansions it might be the case that e.g. a premise
has fewer nodes than or the same number of nodes as the target in
backward reasoning, but the premise allows more function expansions
than the target.

In order to handle this case properly we introduce for each function a
level. Basic functions have level 0 and function with definitions have
a level one more than the highest level of the used functions in its
definition.

This level calculation has been prepared but not yet activated.

2. Analysis of backward terms have been done in two places. The common part
has been factored out.

	modified:   ocaml/context.ml
	modified:   ocaml/context.mli
	modified:   ocaml/feature_table.ml
	modified:   ocaml/feature_table.mli
	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_table.ml
	modified:   ocaml/prover.ml
	modified:   ocaml/typer.ml
Term levels integrated into backward reasoning

Now a premise of a backward rule is considered not more complicated
than the target if it doesn't have a higher level (i.e. function level) and if
it doesn't have more nodes.

Basic functions have level zero, functions with a definition have a level
which is one plus the level of the definition term.

	modified:   ocaml/proof_context.ml
	modified:   ocaml/proof_context.mli
	modified:   ocaml/prover.ml
Fix: calculation of the module string

	modified:   ocaml/support.ml
Minor refactoring in the analysis of backward rules

	modified:   ocaml/proof_context.ml
Term levels integrated into forward reasoning

	modified:   ocaml/proof_context.ml
Parser enhancements

- Allow unary '+' and unary '*' operator

- Allow sets like {a}, {a,b,c}

Expressions like

     {a,b,...}

are expanded to

     singleton(a) + singleton(b) + ...

The expansion is purely syntactical and done by the parser. If there are
no functions 'singleton' and '+' such that the expanded expression can be
typed then the compiler issues a type error.

	modified:   ocaml/parser.mly
	modified:   ocaml/support.ml