1 (***********************************************************************)
5 (* Kim Nguyen, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
9 (* Recherche Scientifique. All rights reserved. This file is *)
10 (* distributed under the terms of the GNU Lesser General Public *)
11 (* License, with the special exception on linking described in file *)
14 (***********************************************************************)
16 (** Implementation of 2-way Selecting Alternating Tree Automata *)
19 type move = [ `First_child
29 val create_table : 'a -> 'a table
30 val get : 'a table -> t -> 'a
31 val set : 'a table -> t -> 'a -> unit
32 val iter : (t -> 'a -> unit) -> 'a table -> unit
33 val fold : (t -> 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
34 val for_all : (t -> 'a -> bool) -> 'a table -> bool
35 val for_all2 : (t -> 'a -> 'b -> bool) -> 'a table -> 'b table -> bool
36 val exists : (t -> 'a -> bool) -> 'a table -> bool
39 (** Type of moves an automaton can perform *)
42 Move of move * State.t (** In the [move] direction, the automaton must be in the given state *)
43 | Is_first_child (** True iff the node is the first child of its parent *)
44 | Is_next_sibling (** True iff the node is the next sibling of its parent *)
45 | Is of Tree.NodeKind.t (** True iff the node is of the given kind *)
46 | Has_first_child (** True iff the node has a first child *)
47 | Has_next_sibling (** True iff the node has a next sibling *)
48 (** Type of the predicates that can occur in the Boolean formulae that are in the transitions of the automaton *)
51 include Hcons.S with type data = predicate
52 include Common_sig.Printable with type t := t
54 (** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *)
58 include module type of Boolean.Make(Atom)
59 val first_child : State.t -> t
60 val next_sibling : State.t -> t
61 val parent : State.t -> t
62 val previous_sibling : State.t -> t
63 val stay : State.t -> t
64 (** [first_child], [next_sibling], [parent], [previous_sibling], [stay] create a formula which consists only
65 of the corresponding [move] atom. *)
66 val is_first_child : t
67 val is_next_sibling : t
68 val has_first_child : t
69 val has_next_sibling : t
70 (** [is_first_child], [is_next_sibling], [has_first_child], [has_next_sibling] are constant formulae which consist
71 only of the corresponding atom
73 val is : Tree.NodeKind.t -> t
74 (** [is k] creates a formula that tests the kind of the current node *)
77 val is_processing_instruction : t
79 (** [is_attribute], [is_element], [is_processing_instruction], [is_comment] are constant formulae that tests a
81 val get_states : t -> StateSet.t
82 (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
83 val get_states_by_move : t -> StateSet.t Move.table
85 (** Modules representing the Boolean formulae used in transitions *)
87 module Transition : sig
88 include Hcons.S with type data = State.t * QNameSet.t * Formula.t
89 val print : Format.formatter -> t -> unit
91 (** A [Transition.t] is a hashconsed triple of the state, the set of labels and the formula *)
94 module TransList : sig
95 include Hlist.S with type elt = Transition.t
96 val print : Format.formatter -> ?sep:string -> t -> unit
98 (** Hashconsed lists of transitions, with a printing facility *)
102 (** 2-way Selecting Alternating Tree Automata *)
105 (** return the internal unique ID of the automaton *)
107 val get_states : t -> StateSet.t
108 (** return the set of states of the automaton *)
110 val get_starting_states : t -> StateSet.t
111 (** return the set of starting states of the automaton *)
113 val get_selecting_states : t -> StateSet.t
114 (** return the set of selecting states of the automaton *)
116 val get_states_by_rank : t -> StateSet.t array
117 (** return an array of states ordered by ranks.
120 val get_max_rank : t -> int
121 (** return the maximal rank of a state in the automaton, that is the
122 maximum number of runs needed to fuly evaluate the automaton.
125 val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t
126 (** [get_trans auto l q] returns the list of transitions taken by [auto]
127 for label [l] in state [q]. Takes time proportional to the number of
128 transitions in the automaton.
131 val get_form : t -> QNameSet.elt -> State.t -> Formula.t
132 (** [get_form auto l q] returns a single formula for label [l] in state [q].
133 Takes time proportional to the number of transitions in the automaton.
136 val print : Format.formatter -> t -> unit
137 (** Pretty printing of the automaton *)
140 (** [copy a] creates a copy of automaton [a], that is a new automaton with
141 the same transitions but with fresh states, such that [get_states a] and
142 [get_states (copy a)] are distinct
144 val concat : t -> t -> t
145 (** [concat a a'] creates a new automaton [a''] such that, given a set of tree
146 nodes [N], [a'' N = a' (a N)].
149 val merge : t -> t -> t
150 (** [merge a a'] creates a new automaton [a''] that evaluates both [a] and [a'']
154 val union : t -> t -> t
155 (** [union a a'] creates a new automaton [a''] that selects node
156 selected by either [a] or [a']
159 val inter : t -> t -> t
160 (** [inter a a'] creates a new automaton [a''] that selects node
161 selected by both [a] and [a']
165 (** [neg a] creates a new automaton [a'] that selects the nodes not
169 val diff : t -> t -> t
170 (** [diff a a'] creates a new automaton [a''] that select nodes selected
171 by [a] but not selected by [a']
177 (** Alias type for the automata type *)
180 (** Abstract type for a builder *)
183 (** Create a fresh builder *)
185 val add_state : t -> ?starting:bool -> ?selecting:bool -> State.t -> unit
186 (** Add a state to the set of states of the automaton. The
187 optional arguments [?starting] and [?selecting] (defaulting
188 to [false]) allow one to specify whether the state is
189 starting/selecting. *)
191 val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit
192 (** Add a transition to the automaton *)
194 val finalize : t -> auto
195 (** Finalize the automaton and return it. Clean-up unused states (states that
196 do not occur in any transitions and remove instantes of negative [move] atoms
197 by creating fresh states that accept the complement of the negated state.
200 (** Builder facility for the automaton *)