(***********************************************************************)
(*                                                                     *)
(*                               TAToo                                 *)
(*                                                                     *)
(*                     Kim Nguyen, LRI UMR8623                         *)
(*                   Université Paris-Sud & CNRS                       *)
(*                                                                     *)
(*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
(*  Recherche Scientifique. All rights reserved.  This file is         *)
(*  distributed under the terms of the GNU Lesser General Public       *)
(*  License, with the special exception on linking described in file   *)
(*  ../LICENSE.                                                        *)
(*                                                                     *)
(***********************************************************************)

(** Implementation of 2-way Selecting Alternating Tree Automata *)


type move = [ `First_child
            | `Next_sibling
            | `Parent
            | `Previous_sibling
            | `Stay ]
(** 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 *)

module Formula :
  sig
    include module type of Boolean.Make(Atom)
    val first_child : State.t -> t
    val next_sibling : State.t -> t
    val parent : State.t -> t
    val previous_sibling : State.t -> t
    val stay : State.t -> t
      (** [first_child], [next_sibling], [parent], [previous_sibling], [stay] create a formula which consists only
          of the corresponding [move] atom. *)
    val is_first_child : t
    val is_next_sibling : t
    val has_first_child : t
    val has_next_sibling : t
      (** [is_first_child], [is_next_sibling], [has_first_child], [has_next_sibling] are constant formulae which consist
          only of the corresponding atom
      *)
    val is : Tree.NodeKind.t -> t
      (** [is k] creates a formula that tests the kind of the current node *)
    val is_attribute : t
    val is_element : t
    val is_processing_instruction : t
    val is_comment : t
      (** [is_attribute], [is_element], [is_processing_instruction], [is_comment] are constant formulae that tests a
          particular kind *)
    val get_states : t -> StateSet.t
      (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
  end
(** Modules representing the Boolean formulae used in transitions *)

module Transition : sig
  include Hcons.S with type data = State.t * QNameSet.t * Formula.t
  val print : Format.formatter -> t -> unit
end
(** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)


module TransList : sig
  include Hlist.S with type elt = Transition.t
  val print : Format.formatter -> ?sep:string -> t -> unit
end
(** Hashconsed lists of transitions, with a printing facility *)


type t
(** 2-way Selecting Alternating Tree Automata *)

val uid : t -> Uid.t
(** return the internal unique ID of the automaton *)

val get_states : t -> StateSet.t
(** return the set of states of the automaton *)

val get_starting_states : t -> StateSet.t
(** return the set of starting states of the automaton *)

val get_selecting_states : t -> StateSet.t
(** return the set of selecting states of the automaton *)

val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
(** [get_trans auto l q] returns the list of transitions taken by [auto]
    for label [l] in state [q]. Takes time proportional to the number of
    transitions in the automaton.
 *)

val get_form : t -> QNameSet.elt -> State.t -> Formula.t
(** [get_form auto l q] returns a single formula for label [l] in state [q].
    Takes time proportional to the number of transitions in the automaton.
 *)

val print : Format.formatter -> t -> unit
(** Pretty printing of the automaton *)

val copy : t -> t
(** [copy a] creates a copy of automaton [a], that is a new automaton with
    the same transitions but with fresh states, such that [get_states a] and
    [get_states (copy a)] are distinct
*)
val concat : t -> t -> t
(** [concat a a'] creates a new automaton [a''] such that, given a set of tree
    nodes [N], [a'' N = a' (a N)].
*)

val merge : t -> t -> t
(** [merge a a'] creates a new automaton [a''] that evaluates both [a] and [a'']
    in parallel
*)

val union : t -> t -> t
(** [union a a'] creates a new automaton [a''] that selects node
    selected by either [a] or [a']
*)

val inter : t -> t -> t
(** [inter a a'] creates a new automaton [a''] that selects node
    selected by both [a] and [a']
*)

val neg : t -> t
(** [neg a] creates a new automaton [a'] that selects the nodes not
    selected by [a]
*)

val diff : t -> t -> t
(** [diff a a'] creates a new automaton [a''] that select nodes selected
    by [a] but not selected by [a']
*)

module Builder :
sig
  type auto = t
    (** Alias type for the automata type *)

  type t
    (** Abstract type for a builder *)

  val make : unit -> t
    (** Create a fresh builder *)

  val add_state : t -> ?starting:bool -> ?selecting:bool -> State.t -> unit
  (** Add a state to the set of states of the automaton. The
      optional arguments [?starting] and [?selecting] (defaulting
      to [false]) allow one to specify whether the state is
      starting/selecting. *)

  val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
    (** Add a transition to the automaton *)

  val finalize : t  -> auto
    (** Finalize the automaton and return it. Clean-up unused states (states that
        do not occur in any transitions and remove instantes of negative [move] atoms
        by creating fresh states that accept the complement of the negated state.
    *)
end
  (** Builder facility for the automaton *)