(** Implementation of hashconsed Boolean formulae *)
-type move = [ `Left |`Right ]
+type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ]
+
(** Direction for automata predicates *)
-type 'hcons expr =
- False
- | True
- | Or of 'hcons * 'hcons
- | And of 'hcons * 'hcons
- | Atom of (move * bool * State.t)
+type 'formula expr =
+ | False
+ | True
+ | Or of 'formula * 'formula
+ | And of 'formula * 'formula
+ | Move of move * bool * State.t
-(** Partial internal representation of a formula,
+(** View of the internal representation of a formula,
used for pattern matching *)
type t
+
(** Abstract type representing hashconsed formulae *)
val hash : t -> int
val expr : t -> t expr
(** Equality over formulae *)
-val st : t -> StateSet.t * StateSet.t
+(*val st : t -> StateSet.t * StateSet.t
(** states occuring left and right, positively or negatively *)
+*)
val compare : t -> t -> int
(** Comparison of formulae *)
-val size : t -> int
-(** Syntactic size of the formula *)
-
val print : Format.formatter -> t -> unit
(** Pretty printer *)
val of_bool : bool -> t
(** Convert an ocaml Boolean value to a formula *)
-
-module Infix : sig
- val ( +| ) : t -> t -> t
- val ( *& ) : t -> t -> t
- val ( *+ ) : move -> StateSet.elt -> t
- val ( *- ) : move -> StateSet.elt -> t
-end
-(** Module to facilitate infix notations of formulae.
- Just [open Formla.Infix] and write:
- [let f = `Left *+ q1 +| `Right *+ q2 in ...]
-*)