-
-type predicate = Move of move * State.t
- | Is_first_child
- | Is_next_sibling
- | Is of Tree.NodeKind.t
- | Has_first_child
- | Has_next_sibling
-
-val is_move : predicate -> bool
-
-module Atom : Boolean.ATOM with type data = predicate
+(** Type of moves an automaton can perform *)
+
+type predicate =
+ Move of move * State.t (** In the [move] direction, the automaton must be in the given state *)
+ | Is_first_child (** True iff the node is the first child of its parent *)
+ | Is_next_sibling (** True iff the node is the next sibling of its parent *)
+ | Is of Tree.NodeKind.t (** True iff the node is of the given kind *)
+ | Has_first_child (** True iff the node has a first child *)
+ | Has_next_sibling (** True iff the node has a next sibling *)
+(** Type of the predicates that can occur in the Boolean formulae that are in the transitions of the automaton *)
+
+module Atom : sig
+ include Hcons.S with type data = predicate
+ include Common_sig.Printable with type t:= t
+end
+(** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)