(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-03-08 16:24:41 CET by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-03-09 18:06:46 CET by Kim Nguyen>
*)
INCLUDE "utils.ml"
open Format
open Utils
-type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon |`Is1 |`Is2 ]
-type state_ctx = { mutable left : StateSet.t;
- mutable right : StateSet.t;
- mutable up1 : StateSet.t;
- mutable up2 : StateSet.t;
- mutable epsilon : StateSet.t;
- mutable is_left : bool;
- mutable is_root : bool}
-
-type pred_ = move * bool * State.t
-let make_ctx a b c d e f g =
- { left = a; right = b; up1 = c; up2 = d; epsilon = e; is_left = f; is_root = g }
-
-let print_ctx fmt c = fprintf fmt "{ left : %a; right : %a; up1: %a ; up2 : %a; epsilon : %a ; is_left : %b; is_root : %b }"
- StateSet.print c.left StateSet.print c.right StateSet.print c.up1 StateSet.print c.up2
- StateSet.print c.epsilon
- c.is_left c.is_root
-
-module Move : (Formula.PREDICATE with type data = pred_ and type ctx = state_ctx ) =
+type predicate = | First_child
+ | Next_sibling
+ | Parent
+ | Previous_sibling
+ | Stay
+ | Is_first_child
+ | Is_next_sibling
+ | Is_attribute
+ | Has_first_child
+ | Has_next_sibling
+
+let is_move p = match p with
+| First_child | Next_sibling
+| Parent | Previous_sibling | Stay -> true
+| _ -> false
+
+
+type atom = predicate * bool * State.t
+
+module Atom : (Formula.ATOM with type data = atom) =
struct
module Node =
struct
- type t = move * bool * State.t
+ type t = atom
let equal n1 n2 = n1 = n2
let hash n = Hashtbl.hash n
end
- type ctx = state_ctx
-
-
include Hcons.Make(Node)
- let _pr_buff = Buffer.create 10
- let _str_fmt = formatter_of_buffer _pr_buff
- let _flush_str_fmt () = pp_print_flush _str_fmt ();
- let s = Buffer.contents _pr_buff in
- Buffer.clear _pr_buff; s
let print ppf a =
- let _ = _flush_str_fmt () in
-
- let m, b, s = a.node in
- let dir,num =
- match m with
- | `Left -> Pretty.down_arrow, Pretty.subscript 1
- | `Right -> Pretty.down_arrow, Pretty.subscript 2
- | `Epsilon -> Pretty.epsilon, ""
- | `Up1 -> Pretty.up_arrow, Pretty.subscript 1
- | `Up2 -> Pretty.up_arrow, Pretty.subscript 2
- | `Is1 -> "?", Pretty.subscript 1
- | `Is2 -> "?", Pretty.subscript 2
- in
- fprintf _str_fmt "%s%s" dir num;
- if s != State.dummy then State.print _str_fmt s;
- let str = _flush_str_fmt () in
- fprintf ppf "%s%s" (if b then "" else Pretty.lnot) str
- let neg p =
- let l, b, s = p.node in
- make (l, not b, s)
-
- exception NegativeAtom of (move*State.t)
-
- let eval ctx p =
- let l, b, s = p.node in
- if s == State.dummy then
- let dir =
- match l with
- | `Is1 -> ctx.is_left
- | _ -> not ctx.is_left
- in
- let res = dir && not ctx.is_root in
- res && b || (not (b || res))
- else begin
- if not b then raise (NegativeAtom(l,s));
- StateSet.mem s begin
- match l with
- `Left -> ctx.left
- | `Right -> ctx.right
- | `Up1 -> ctx.up1
- | `Up2 -> ctx.up2
- | `Epsilon -> ctx.epsilon
- | _ -> StateSet.empty
- end
- end
+ let p, b, q = a.node in
+ if not b then fprintf ppf "%s" Pretty.lnot;
+ match p with
+ | First_child -> fprintf ppf "FC(%a)" State.print q
+ | Next_sibling -> fprintf ppf "NS(%a)" State.print q
+ | Parent -> fprintf ppf "FC%s(%a)" Pretty.inverse State.print q
+ | Previous_sibling -> fprintf ppf "NS%s(%a)" Pretty.inverse State.print q
+ | Stay -> fprintf ppf "%s(%a)" Pretty.epsilon State.print q
+ | Is_first_child -> fprintf ppf "FC%s?" Pretty.inverse
+ | Is_next_sibling -> fprintf ppf "NS%s?" Pretty.inverse
+ | Is_attribute -> fprintf ppf "%s" "@?"
+ | Has_first_child -> fprintf ppf "FC?"
+ | Has_next_sibling -> fprintf ppf "NS?"
+
+ let neg a =
+ let p, b, q = a.node in
+ make (p, not b, q)
+
+
+end
+
+module SFormula =
+struct
+ include Formula.Make(Atom)
+ let mk_atom a b c = atom_ (Atom.make (a,b,c))
+ let has_first_child =
+ (mk_atom Has_first_child true State.dummy)
+
+ let has_next_sibling =
+ (mk_atom Has_next_sibling true State.dummy)
+
+ let is_first_child =
+ (mk_atom Is_first_child true State.dummy)
+
+ let is_next_sibling =
+ (mk_atom Is_next_sibling true State.dummy)
+
+ let is_attribute =
+ (mk_atom Is_attribute true State.dummy)
+
+ let first_child q =
+ and_
+ (mk_atom First_child true q)
+ has_first_child
+
+ let next_sibling q =
+ and_
+ (mk_atom Next_sibling true q)
+ has_next_sibling
+
+ let parent q =
+ and_
+ (mk_atom Parent true q)
+ is_first_child
+
+ let previous_sibling q =
+ and_
+ (mk_atom Previous_sibling true q)
+ is_next_sibling
+
+ let stay q =
+ (mk_atom Stay true q)
+
+ let get_states phi =
+ fold (fun phi acc ->
+ match expr phi with
+ | Formula.Atom a -> let _, _, q = Atom.node a in
+ if q != State.dummy then StateSet.add q acc else acc
+ | _ -> acc
+ ) phi StateSet.empty
+
end
-module SFormula = Formula.Make(Move)
type t = {
id : Uid.t;
mutable states : StateSet.t;
- mutable top_states : StateSet.t;
- mutable bottom_states: StateSet.t;
mutable selection_states: StateSet.t;
transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t;
}
let create () = { id = next ();
states = StateSet.empty;
- top_states = StateSet.empty;
- bottom_states = StateSet.empty;
selection_states = StateSet.empty;
transitions = Hashtbl.create 17;
}
fprintf fmt
"\nInternal UID: %i@\n\
States: %a@\n\
- Top states: %a@\n\
- Bottom states: %a@\n\
Selection states: %a@\n\
Alternating transitions:@\n"
(a.id :> int)
StateSet.print a.states
- StateSet.print a.top_states
- StateSet.print a.bottom_states
StateSet.print a.selection_states;
let trs =
Hashtbl.fold
Hashtbl.replace a.transitions q nqtrans
) a.states
+let cleanup_states a =
+ let memo = ref StateSet.empty in
+ let rec loop q =
+ if not (StateSet.mem q !memo) then begin
+ memo := StateSet.add q !memo;
+ let trs = try Hashtbl.find a.transitions q with Not_found -> [] in
+ List.iter (fun (_, phi) ->
+ StateSet.iter loop (SFormula.get_states phi)) trs
+ end
+ in
+ StateSet.iter loop a.selection_states;
+ let unused = StateSet.diff a.states !memo in
+ eprintf "Unused states %a\n%!" StateSet.print unused;
+ StateSet.iter (fun q -> Hashtbl.remove a.transitions q) unused;
+ a.states <- !memo
+
(* [normalize_negations a] removes negative atoms in the formula
complementing the sub-automaton in the negative states.
[TODO check the meaning of negative upward arrows]
*)
+
let normalize_negations auto =
+ eprintf "Automaton before normalize_trans:\n";
+ print err_formatter auto;
+ eprintf "--------------------\n%!";
+
let memo_state = Hashtbl.create 17 in
let todo = Queue.create () in
let rec flip b f =
| Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2)
| Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2)
| Formula.Atom(a) -> begin
- let l, b', q = Move.node a in
+ let l, b', q = Atom.node a in
if q == State.dummy then if b then f else SFormula.not_ f
else
if b == b' then begin
(* a appears positively, either no negation or double negation *)
if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo;
- SFormula.atom_ (Move.make (l, true, q))
+ SFormula.atom_ (Atom.make (l, true, q))
end else begin
(* need to reverse the atom
either we have a positive state deep below a negation
(* create a new state and add it to the todo queue *)
let nq = State.make () in
auto.states <- StateSet.add nq auto.states;
- if not (StateSet.mem q auto.bottom_states) then
- auto.bottom_states <- StateSet.add nq auto.bottom_states;
- if not (StateSet.mem q auto.top_states) then
- auto.top_states <- StateSet.add nq auto.top_states;
Hashtbl.add memo_state (q, false) nq;
Queue.add (q, false) todo; nq
in
- SFormula.atom_ (Move.make (l, true, not_q))
+ SFormula.atom_ (Atom.make (l, true, not_q))
end
end
in
let nq = if b then q else
let nq = State.make () in
auto.states <- StateSet.add nq auto.states;
- if not (StateSet.mem q auto.bottom_states) then
- auto.bottom_states <- StateSet.add nq auto.bottom_states;
- if not (StateSet.mem q auto.top_states) then
- auto.top_states <- StateSet.add nq auto.top_states;
nq
in
Hashtbl.add memo_state key nq; nq
in
let trans = Hashtbl.find auto.transitions q in
let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in
- Hashtbl.replace auto.transitions q' trans'
- done
+ Hashtbl.replace auto.transitions q' trans';
+ done;
+ cleanup_states auto
+
+