| `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
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
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