0ca6e5578e6213a90f78e90845cbe0df696d2f9e
[tatoo.git] / src / auto / ata.mli
1 (***********************************************************************)
2 (*                                                                     *)
3 (*                               TAToo                                 *)
4 (*                                                                     *)
5 (*                     Kim Nguyen, LRI UMR8623                         *)
6 (*                   Universit√© Paris-Sud & CNRS                       *)
7 (*                                                                     *)
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   *)
12 (*  ../LICENSE.                                                        *)
13 (*                                                                     *)
14 (***********************************************************************)
15
16 (*
17   Time-stamp: <Last modified on 2013-03-15 18:18:23 CET by Kim Nguyen>
18 *)
19
20 type predicate =
21     First_child
22   | Next_sibling
23   | Parent
24   | Previous_sibling
25   | Stay
26   | Is_first_child
27   | Is_next_sibling
28   | Is of Tree.Common.NodeKind.t
29   | Has_first_child
30   | Has_next_sibling
31
32 val is_move : predicate -> bool
33
34 type atom = predicate * bool * State.t
35
36 module Atom : Formula.ATOM with type data = atom
37
38 module SFormula :
39   sig
40     include module type of Formula.Make(Atom)
41     val mk_atom : predicate -> bool -> State.t -> t
42     val mk_kind : Tree.Common.NodeKind.t -> t
43     val has_first_child : t
44     val has_next_sibling : t
45     val is_first_child : t
46     val is_next_sibling : t
47     val is_attribute : t
48     val is_element : t
49     val is_processing_instruction : t
50     val is_comment : t
51     val first_child : State.t -> t
52     val next_sibling : State.t -> t
53     val parent : State.t -> t
54     val previous_sibling : State.t -> t
55     val stay : State.t -> t
56     val get_states : t -> StateSet.t
57   end
58
59
60 module Transition : Utils.Hcons.S with
61             type data = State.t * Utils.QNameSet.t * SFormula.t
62
63 module TransList : sig
64   include Utils.Hlist.S with type elt = Transition.t
65   val print : Format.formatter -> ?sep:string -> t -> unit
66 end
67
68
69 type t = private {
70   id : Utils.Uid.t;
71   mutable states : StateSet.t;
72   mutable selection_states: StateSet.t;
73   transitions: (State.t, (Utils.QNameSet.t*SFormula.t) list) Hashtbl.t;
74   mutable cache2 : TransList.t Utils.Cache.N2.t;
75   mutable cache6 : (TransList.t*StateSet.t) Utils.Cache.N6.t;
76 }
77
78
79
80 val create : StateSet.t -> StateSet.t -> t
81 val reset : t -> unit
82 val get_trans : t -> Utils.QNameSet.elt -> StateSet.t -> TransList.t
83
84 val eval_trans : t -> TransList.t
85   -> StateSet.t -> StateSet.t -> StateSet.t -> StateSet.t
86   -> bool -> bool -> bool -> bool -> Tree.Common.NodeKind.t
87   -> TransList.t*StateSet.t
88
89 val add_trans : t -> State.t -> Utils.QNameSet.t -> SFormula.t -> unit
90 val print : Format.formatter -> t -> unit
91 val complete_transitions : t -> unit
92 val cleanup_states : t -> unit
93 val normalize_negations : t -> unit