From c36250a4de897883d0080fc369d784abf0e2ebe8 Mon Sep 17 00:00:00 2001
From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= <kn@lri.fr>
Date: Wed, 20 Nov 2013 22:50:56 +0100
Subject: [PATCH] Put the move type of automata in a Move module and add
 auxiliary function to create and maintain tables indexed by moves. Use it to
 return the states of a forumla by move.

---
 src/ata.ml  | 79 +++++++++++++++++++++++++++++++++++++++++++----------
 src/ata.mli | 15 ++++++++++
 2 files changed, 80 insertions(+), 14 deletions(-)

diff --git a/src/ata.ml b/src/ata.ml
index a4ea306..3263e46 100644
--- a/src/ata.ml
+++ b/src/ata.ml
@@ -22,6 +22,57 @@ type move = [ `First_child
             | `Previous_sibling
             | `Stay ]
 
+module Move =
+  struct
+    type t = move
+    type 'a table = 'a array
+    let idx = function
+      | `First_child -> 0
+      | `Next_sibling -> 1
+      | `Parent -> 2
+      | `Previous_sibling -> 3
+      | `Stay -> 4
+    let ridx = function
+      | 0 -> `First_child
+      | 1 -> `Next_sibling
+      | 2 -> `Parent
+      | 3 -> `Previous_sibling
+      | 4 -> `Stay
+      | _ -> assert false
+
+    let create_table a = Array.make 5 a
+    let get m k = m.(idx k)
+    let set m k v = m.(idx k) <- v
+    let iter f m = Array.iteri (fun i v -> f (ridx i) v) m
+    let fold f m acc =
+      let acc = ref acc in
+      iter (fun i v -> acc := f i v !acc) m;
+      !acc
+    let for_all p m =
+      try
+        iter (fun i v -> if not (p i v) then raise Exit) m;
+        true
+      with
+        Exit -> false
+    let exists p m =
+      try
+        iter (fun i v -> if p i v then raise Exit) m;
+        false
+      with
+        Exit -> true
+    let print ppf m =
+      match m with
+        `First_child -> fprintf ppf "%s" Pretty.down_arrow
+      | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow
+      | `Parent -> fprintf ppf "%s" Pretty.up_arrow
+      | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow
+      | `Stay -> fprintf ppf "%s" Pretty.bullet
+
+    let print_table pr_e ppf m =
+      iter (fun i v -> fprintf ppf "%a: %a" print i pr_e v;
+        if (idx i) < 4 then fprintf ppf ", ") m
+  end
+
 type predicate = Move of move * State.t
                  | Is_first_child
                  | Is_next_sibling
@@ -43,15 +94,8 @@ struct
 
   let print ppf a =
     match a.node with
-    | Move (m, q) -> begin
-      match m with
-        `First_child -> fprintf ppf "%s" Pretty.down_arrow
-      | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow
-      | `Parent -> fprintf ppf "%s" Pretty.up_arrow
-      | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow
-      | `Stay -> fprintf ppf "%s" Pretty.bullet
-    end;
-        fprintf ppf "%a" State.print q
+    | Move (m, q) ->
+      fprintf ppf "%a%a" Move.print m State.print q
     | Is_first_child -> fprintf ppf "%s?" Pretty.up_arrow
     | Is_next_sibling -> fprintf ppf "%s?" Pretty.left_arrow
     | Is k -> fprintf ppf "is-%a?" Tree.NodeKind.print k
@@ -107,12 +151,19 @@ struct
 
   let stay q = mk_move `Stay q
 
-  let get_states phi =
-    fold (fun phi acc ->
+  let get_states_by_move phi =
+    let table = Move.create_table StateSet.empty in
+    iter (fun phi ->
       match expr phi with
-      | Boolean.Atom ({ Atom.node = Move(_,q) ; _ }, _) ->  StateSet.add q acc
-      | _ -> acc
-    ) phi StateSet.empty
+      | Boolean.Atom ({ Atom.node = Move(v,q) ; _ }, _) ->
+        let s = Move.get table v in
+        Move.set table v (StateSet.add q s)
+      | _ -> ()
+    ) phi;
+    table
+  let get_states phi =
+    let table = get_states_by_move phi in
+    Move.fold (fun _ s acc -> StateSet.union s acc) table StateSet.empty
 
 end
 
diff --git a/src/ata.mli b/src/ata.mli
index 00070d4..650673e 100644
--- a/src/ata.mli
+++ b/src/ata.mli
@@ -21,6 +21,20 @@ type move = [ `First_child
             | `Parent
             | `Previous_sibling
             | `Stay ]
+
+module Move :
+  sig
+    type t = move
+    type 'a table
+    val create_table : 'a -> 'a table
+    val get : 'a table -> t -> 'a
+    val set : 'a table -> t -> 'a -> unit
+    val iter : (t -> 'a -> unit) -> 'a table -> unit
+    val fold : (t -> 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b
+    val for_all : (t -> 'a -> bool) -> 'a table -> bool
+    val exists : (t -> 'a -> bool) -> 'a table -> bool
+  end
+
 (** Type of moves an automaton can perform *)
 
 type predicate =
@@ -65,6 +79,7 @@ module Formula :
           particular kind *)
     val get_states : t -> StateSet.t
       (** [get_state f] retrieves all the states occuring in [move] predicates in [f] *)
+    val get_states_by_move : t -> StateSet.t Move.table
   end
 (** Modules representing the Boolean formulae used in transitions *)
 
-- 
2.17.1