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.''' ...