version 3.6 coming up soon

This evening I committed the core changes I've done to the TWB in the last month or so. I committed all the changes
in one batch and now I'll be adding bug fixes till the next major release of the code.

The major changes in the upcoming release will be:

* '''new connectives and grammar definition.''' The connective definition in the previous release
wasn't flexible enough to define complicated grammars ala' PDL. Now the user is in charge of
defining both the connectives and the grammar used in the rule definition. For example, a
definition for PDL will be of the form:

CONNECTIVES
[ "~";"&";"v";"<";">";"U";"*";"->";"<->";"[";"]" ]
GRAMMAR
program :=
* program
| program U program
| Atom ;
formula :=
Atom | Verum | Falsum
| formula & formula
| formula v formula
| formula -> formula
| formula <-> formula
| < program > formula
| [ program ] formula
| ~ formula ;
expr := formula ;
END

* '''printers and constructors.''' With each user defined grammar entry, the TWB will generate a
printer function and for the special "expr" and "formula" entry the TWB will generate a
constructor to be used to write ocaml functions: EX:


let a = formula ( Verum )
let b = formula ( a v D )
let c = formula ( b & ( a v b ) )
let d = formula ( < B > c )
let e = formula ( < * A U B > c & ( c v d ) )
let f = formula ( <> c )
let g = formula ( { formula ( A ) } v B )
let g = formula ( { nnf c } )

let ff = function
|formula ( D ) -> 1
|formula ( < * A U B > e & ( c v d ) ) -> 1
|formula ( a & _ ) -> failwith "ff"

* '''labels.''' the basic grammar entry that is considered by the TWB is the entry "expr"
An expression can be decorated with an arbitrary label by specifing its type in the grammar
definition: EX:
expr := int list : formula

* '''new type system.''' Now users are in charge of defining their own data types. For example to declare
a simple set of formulae as a history the definition will be like :


module FormulaSet = TwbSet.Make(
struct
type t = formula
let to_string = formula_printer
let copy s = s
end
)

HISTORIES
(DIAMONDS : FormulaSet.set := new FormulaSet.set);
(BOXES : FormulaSet.set := new FormulaSet.set)
END

of course a number of useful data structure will be defined in the library itself.

* '''Refactoring of the internal libraries.''' I've re-factored the internal library to be generic in the datatype
used. My goal was to maximize code re-use and to abstract the internal data structures from the
user types.

* '''Sequent interface.''' Not yet fully implemented.
* '''Many other minor modifications.''' ...