new support data structures (towards a sequent interface)

Last week I've started working toward the new sequent interface. After a bit of brainstorming I've soon realized that to implement the new frontend I've to change the way I handle generic data types in the TWB.

At the moment generic data types (for example how formulae are represented) are barried inside the TWB library, making very painful for the user to add a new datatype or a new container (for example a queue of tuples). Decoupling my generic types from the TWB library is conceptually easy, but technically complicated because of the ocaml type system.

This week I've re-learned about polimorphic variants and read a number of paper from Jacques Garrigue
http://www.math.nagoya-u.ac.jp/~garrigue/papers/ and of course the updated ocaml manual http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html

Polimorphic variants and private rows should allow me to define a number of generic and extensible data structures that I can re-use all throught my code. At the moment I'm a bit strugling to define the hash table to handle histories as by definition these are heterogeneus objects.

I've also done a bit of work to use polomorphic variants to handle formulae and allow the user to build functions modularly. For example this is an example on how to build a nnf function for modal logic K on top of the nnf function for pc.


(* my basic data type *)
type 'a termpc =
[`And of 'a * 'a
|`Or of 'a * 'a
|`Not of 'a
|`Atom of string
]
;;

(* a simple normal form function *)
let nnfpc_aux f : [> 'a termpc] termpc -> 'a = function
|`Not ( `Not x ) -> f x
|`Not ( `And(x,y) ) -> `Or (f (`Not x), f (`Not y) )
|`Not ( `Or (x,y) ) -> `And (f (`Not x), f (`Not y) )
|`And (x,y) -> `And (f x, f y)
|`Or (x,y) -> `Or (f x, f y)
|`Not ( `Atom _) as x -> x
|`Atom _ as x -> x
|`Not _ -> failwith "impossible pc"
;;

let rec nnfpc t = nnfpc_aux nnfpc t;;

(* extension of the basic data type *)
type 'a termk =
[`Dia of 'a
|`Box of 'a
|'a termpc
]
;;

let nnfk_aux f : [> 'a termk] termk -> 'a = function
|`Not (`Dia x ) -> `Box (f (`Not x))
|`Not (`Box x ) -> `Dia (f (`Not x))
|`Dia x -> `Dia (f x)
|`Box x -> `Box (f x)
|#termpc as x -> nnfpc_aux f x
;;

let rec nnfk t = nnfk_aux nnfk t;;

still not perfect, but a good starting point.

On other news I've read this paper about ATL:
http://dx.doi.org/10.1016/j.tcs.2005.07.043