From 90ce5857f6cad2ebc753fdbc8e37882a1ff47415 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Wed, 17 Jul 2013 17:59:01 +0200 Subject: [PATCH] Sanitize the representation of formula - rename the toplevel Formula module to Boolean - rename Ata.SFormula to Formula - move the flag saying whether an atom is positive or negative to Boolean - distinguish predicates that are moves from generic predicates. --- src/ata.ml | 223 ++++++++++++++----------------- src/ata.mli | 39 +++--- src/{formula.ml => boolean.ml} | 36 ++--- src/{formula.mli => boolean.mli} | 15 +-- src/xpath/compile.ml | 18 +-- 5 files changed, 148 insertions(+), 183 deletions(-) rename src/{formula.ml => boolean.ml} (81%) rename src/{formula.mli => boolean.mli} (88%) diff --git a/src/ata.ml b/src/ata.ml index df43392..3fa2698 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -15,32 +15,27 @@ INCLUDE "utils.ml" open Format +type move = [ `First_child + | `Next_sibling + | `Parent + | `Previous_sibling + | `Stay ] -type predicate = | First_child - | Next_sibling - | Parent - | Previous_sibling - | Stay +type predicate = Move of move * State.t | Is_first_child | Is_next_sibling - | Is of (Tree.NodeKind.t) + | Is of Tree.NodeKind.t | Has_first_child | Has_next_sibling -let is_move p = match p with -| First_child | Next_sibling -| Parent | Previous_sibling | Stay -> true -| _ -> false +let is_move = function Move _ -> true | _ -> false - -type atom = predicate * bool * State.t - -module Atom : (Formula.ATOM with type data = atom) = +module Atom : (Boolean.ATOM with type data = predicate) = struct module Node = struct - type t = atom + type t = predicate let equal n1 n2 = n1 = n2 let hash n = Hashtbl.hash n end @@ -48,85 +43,74 @@ struct include Hcons.Make(Node) let print ppf a = - 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 + 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 + | 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 - | 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) - + | Has_first_child -> fprintf ppf "%s?" Pretty.down_arrow + | Has_next_sibling -> fprintf ppf "%s?" Pretty.right_arrow end -module SFormula = +module Formula = struct - include Formula.Make(Atom) + include Boolean.Make(Atom) open Tree.NodeKind - let mk_atom a b c = atom_ (Atom.make (a,b,c)) - let mk_kind k = mk_atom (Is k) true State.dummy - let has_first_child = - (mk_atom Has_first_child true State.dummy) + let mk_atom a = atom_ (Atom.make a) + let mk_kind k = mk_atom (Is k) + + let has_first_child = mk_atom Has_first_child - let has_next_sibling = - (mk_atom Has_next_sibling true State.dummy) + let has_next_sibling = mk_atom Has_next_sibling - let is_first_child = - (mk_atom Is_first_child true State.dummy) + let is_first_child = mk_atom Is_first_child - let is_next_sibling = - (mk_atom Is_next_sibling true State.dummy) + let is_next_sibling = mk_atom Is_next_sibling - let is_attribute = - (mk_atom (Is Attribute) true State.dummy) + let is_attribute = mk_atom (Is Attribute) - let is_element = - (mk_atom (Is Element) true State.dummy) + let is_element = mk_atom (Is Element) - let is_processing_instruction = - (mk_atom (Is ProcessingInstruction) true State.dummy) + let is_processing_instruction = mk_atom (Is ProcessingInstruction) - let is_comment = - (mk_atom (Is Comment) true State.dummy) + let is_comment = mk_atom (Is Comment) + let mk_move m q = mk_atom (Move(m,q)) let first_child q = - and_ - (mk_atom First_child true q) - has_first_child + and_ + (mk_move `First_child q) + has_first_child let next_sibling q = and_ - (mk_atom Next_sibling true q) + (mk_move `Next_sibling q) has_next_sibling let parent q = and_ - (mk_atom Parent true q) + (mk_move `Parent q) is_first_child let previous_sibling q = and_ - (mk_atom Previous_sibling true q) + (mk_move `Previous_sibling q) is_next_sibling - let stay q = - (mk_atom Stay true q) + let stay q = mk_move `Stay 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 + | Boolean.Atom ({ Atom.node = Move(_,q) ; _ }, _) -> StateSet.add q acc | _ -> acc ) phi StateSet.empty @@ -134,11 +118,11 @@ end module Transition = Hcons.Make (struct - type t = State.t * QNameSet.t * SFormula.t + type t = State.t * QNameSet.t * Formula.t let equal (a, b, c) (d, e, f) = a == d && b == e && c == f let hash (a, b, c) = - HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((SFormula.uid c) :> int)) + HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int)) end) @@ -151,7 +135,7 @@ end = let print ppf ?(sep="\n") l = iter (fun t -> let q, lab, f = Transition.node t in - fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab SFormula.print f sep) l + fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab Formula.print f sep) l end @@ -218,7 +202,7 @@ type t = { id : Uid.t; mutable states : StateSet.t; mutable selection_states: StateSet.t; - transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; + transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t; mutable cache2 : TransList.t Cache.N2.t; mutable cache4 : Config.t Cache.N4.t; } @@ -226,7 +210,7 @@ type t = { let next = Uid.make_maker () let dummy2 = TransList.cons - (Transition.make (State.dummy,QNameSet.empty, SFormula.false_)) + (Transition.make (State.dummy,QNameSet.empty, Formula.false_)) TransList.nil @@ -300,30 +284,33 @@ let get_trans a tag states = let simplify_atom atom pos q { Config.node=config; _ } = if (pos && StateSet.mem q config.sat) - || ((not pos) && StateSet.mem q config.unsat) then SFormula.true_ + || ((not pos) && StateSet.mem q config.unsat) then Formula.true_ else if (pos && StateSet.mem q config.unsat) - || ((not pos) && StateSet.mem q config.sat) then SFormula.false_ + || ((not pos) && StateSet.mem q config.sat) then Formula.false_ else atom let eval_form phi fcs nss ps ss summary = let rec loop phi = - begin match SFormula.expr phi with - Formula.True | Formula.False -> phi - | Formula.Atom a -> - let p, b, q = Atom.node a in begin - match p with - | First_child -> simplify_atom phi b q fcs - | Next_sibling -> simplify_atom phi b q nss - | Parent | Previous_sibling -> simplify_atom phi b q ps - | Stay -> simplify_atom phi b q ss - | Is_first_child -> SFormula.of_bool (b == (is_left summary)) - | Is_next_sibling -> SFormula.of_bool (b == (is_right summary)) - | Is k -> SFormula.of_bool (b == (k == (kind summary))) - | Has_first_child -> SFormula.of_bool (b == (has_left summary)) - | Has_next_sibling -> SFormula.of_bool (b == (has_right summary)) + begin match Formula.expr phi with + Boolean.True | Boolean.False -> phi + | Boolean.Atom (a, b) -> + begin + match a.Atom.node with + | Move (m, q) -> + let states = match m with + `First_child -> fcs + | `Next_sibling -> nss + | `Parent | `Previous_sibling -> ps + | `Stay -> ss + in simplify_atom phi b q states + | Is_first_child -> Formula.of_bool (b == (is_left summary)) + | Is_next_sibling -> Formula.of_bool (b == (is_right summary)) + | Is k -> Formula.of_bool (b == (k == (kind summary))) + | Has_first_child -> Formula.of_bool (b == (has_left summary)) + | Has_next_sibling -> Formula.of_bool (b == (has_right summary)) end - | Formula.And(phi1, phi2) -> SFormula.and_ (loop phi1) (loop phi2) - | Formula.Or (phi1, phi2) -> SFormula.or_ (loop phi1) (loop phi2) + | Boolean.And(phi1, phi2) -> Formula.and_ (loop phi1) (loop phi2) + | Boolean.Or (phi1, phi2) -> Formula.or_ (loop phi1) (loop phi2) end in loop phi @@ -354,9 +341,9 @@ let eval_trans auto fcs nss ps ss = let new_phi = eval_form phi fcs nss ps old_config old_summary in - if SFormula.is_true new_phi then + if Formula.is_true new_phi then StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo - else if SFormula.is_false new_phi then + else if Formula.is_false new_phi then a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo else let new_tr = Transition.make (q, lab, new_phi) in @@ -389,11 +376,11 @@ let add_trans a q s f = let lab2 = QNameSet.diff labs s in let tr1 = if QNameSet.is_empty lab1 then [] - else [ (lab1, SFormula.or_ phi f) ] + else [ (lab1, Formula.or_ phi f) ] in let tr2 = if QNameSet.is_empty lab2 then [] - else [ (lab2, SFormula.or_ phi f) ] + else [ (lab2, Formula.or_ phi f) ] in (QNameSet.union acup labs, tr1@ tr2 @ atrs) ) (QNameSet.empty, []) trs @@ -433,7 +420,7 @@ let print fmt a = let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) -> let s1 = State.print _str_fmt q; _flush_str_fmt () in let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in - let s3 = SFormula.print _str_fmt f; _flush_str_fmt () in + let s3 = Formula.print _str_fmt f; _flush_str_fmt () in let pre = Pretty.length s1 + Pretty.length s2 in let all = Pretty.length s3 in ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) @@ -467,7 +454,7 @@ let complete_transitions a = let nqtrans = if QNameSet.is_empty rem then qtrans else - (rem, SFormula.false_) :: qtrans + (rem, Formula.false_) :: qtrans in Hashtbl.replace a.transitions q nqtrans ) a.states @@ -479,7 +466,7 @@ let cleanup_states a = 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 + StateSet.iter loop (Formula.get_states phi)) trs end in StateSet.iter loop a.selection_states; @@ -496,39 +483,39 @@ let normalize_negations auto = let memo_state = Hashtbl.create 17 in let todo = Queue.create () in let rec flip b f = - match SFormula.expr f with - Formula.True | Formula.False -> if b then f else SFormula.not_ 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 = 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_ (Atom.make (l, true, q)) - end else begin + match Formula.expr f with + Boolean.True | Boolean.False -> if b then f else Formula.not_ f + | Boolean.Or(f1, f2) -> (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2) + | Boolean.And(f1, f2) -> (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2) + | Boolean.Atom(a, b') -> begin + match a.Atom.node with + | Move (m, q) -> + 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; + Formula.mk_atom (Move(m, q)) + end else begin (* need to reverse the atom either we have a positive state deep below a negation or we have a negative state in a positive formula b' = sign of the state b = sign of the enclosing formula *) - let not_q = - try + let not_q = + try (* does the inverted state of q exist ? *) - Hashtbl.find memo_state (q, false) - with - Not_found -> + Hashtbl.find memo_state (q, false) + with + Not_found -> (* create a new state and add it to the todo queue *) - let nq = State.make () in - auto.states <- StateSet.add nq auto.states; - Hashtbl.add memo_state (q, false) nq; - Queue.add (q, false) todo; nq - in - SFormula.atom_ (Atom.make (l, true, not_q)) - end + let nq = State.make () in + auto.states <- StateSet.add nq auto.states; + Hashtbl.add memo_state (q, false) nq; + Queue.add (q, false) todo; nq + in + Formula.mk_atom (Move (m,not_q)) + end + | _ -> if b then f else Formula.not_ f end in (* states that are not reachable from a selection stat are not interesting *) @@ -553,5 +540,3 @@ let normalize_negations auto = Hashtbl.replace auto.transitions q' trans'; done; cleanup_states auto - - diff --git a/src/ata.mli b/src/ata.mli index d65fabb..e4f0ffd 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -13,28 +13,27 @@ (* *) (***********************************************************************) -type predicate = - First_child - | Next_sibling - | Parent - | Previous_sibling - | Stay - | Is_first_child - | Is_next_sibling - | Is of Tree.NodeKind.t - | Has_first_child - | Has_next_sibling +type move = [ `First_child + | `Next_sibling + | `Parent + | `Previous_sibling + | `Stay ] + +type predicate = Move of move * State.t + | Is_first_child + | Is_next_sibling + | Is of Tree.NodeKind.t + | Has_first_child + | Has_next_sibling val is_move : predicate -> bool -type atom = predicate * bool * State.t +module Atom : Boolean.ATOM with type data = predicate -module Atom : Formula.ATOM with type data = atom - -module SFormula : +module Formula : sig - include module type of Formula.Make(Atom) - val mk_atom : predicate -> bool -> State.t -> t + include module type of Boolean.Make(Atom) + val mk_atom : predicate -> t val mk_kind : Tree.NodeKind.t -> t val has_first_child : t val has_next_sibling : t @@ -54,7 +53,7 @@ module SFormula : module Transition : Hcons.S with - type data = State.t * QNameSet.t * SFormula.t + type data = State.t * QNameSet.t * Formula.t module TransList : sig include Hlist.S with type elt = Transition.t @@ -79,7 +78,7 @@ type t = private { id : Uid.t; mutable states : StateSet.t; mutable selection_states: StateSet.t; - transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; + transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t; mutable cache2 : TransList.t Cache.N2.t; mutable cache4 : Config.t Cache.N4.t; } @@ -94,7 +93,7 @@ val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t val eval_trans : t -> Config.t -> Config.t -> Config.t -> Config.t -> Config.t -val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit +val add_trans : t -> State.t -> QNameSet.t -> Formula.t -> unit val print : Format.formatter -> t -> unit val complete_transitions : t -> unit val cleanup_states : t -> unit diff --git a/src/formula.ml b/src/boolean.ml similarity index 81% rename from src/formula.ml rename to src/boolean.ml index 1e440bc..296f7a6 100644 --- a/src/formula.ml +++ b/src/boolean.ml @@ -16,6 +16,7 @@ INCLUDE "utils.ml" open Format +open Misc (* @@ -24,9 +25,7 @@ open Format *) module type ATOM = sig - type t - val neg : t -> t - include Hcons.Abstract with type t := t + include Hcons.S include Common_sig.Printable with type t := t end @@ -35,14 +34,14 @@ type ('formula,'atom) expr = | True | Or of 'formula * 'formula | And of 'formula * 'formula - | Atom of 'atom + | Atom of 'atom * bool -module Make (P: ATOM) = +module Make (A: ATOM) = struct type 'hcons node = { - pos : ('hcons,P.t) expr; + pos : ('hcons,A.t) expr; mutable neg : 'hcons; } @@ -59,7 +58,7 @@ struct | a,b when a == b -> true | Or(xf1, xf2), Or(yf1, yf2) | And(xf1, xf2), And(yf1,yf2) -> xf1 == yf1 && xf2 == yf2 - | Atom(p1), Atom(p2) -> p1 == p2 + | Atom(p1, b1), Atom(p2, b2) -> p1 == p2 && b1 == b2 | _ -> false let hash f = @@ -70,7 +69,7 @@ struct HASHINT3 (PRIME1, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id) | And (f1, f2) -> HASHINT3(PRIME3, Uid.to_int f1.Node.id, Uid.to_int f2.Node.id) - | Atom(p) -> HASHINT2(PRIME5, Uid.to_int (P.uid p)) + | Atom(p, b) -> HASHINT3(PRIME5, Uid.to_int (A.uid p), int_of_bool b) end type t = Node.t @@ -100,22 +99,7 @@ struct (print ppf f1); fprintf ppf " %s " Pretty.vee; (print ppf f2); - | Atom(p) -> fprintf ppf "%a" P.print p -(* let _ = flush_str_formatter() in - let fmt = str_formatter in - let a_str, d_str = - match dir 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 - in - fprintf fmt "%s%s" a_str d_str; - State.print fmt s; - let str = flush_str_formatter() in - if b then fprintf ppf "%s" str - else Pretty.pp_overline ppf str *) + | Atom(p,b) -> fprintf ppf "%s%a" (if b then "" else Pretty.lnot) A.print p in if parent then fprintf ppf ")" @@ -124,7 +108,6 @@ let print ppf f = print ~parent:false ppf f let is_true f = (expr f) == True let is_false f = (expr f) == False - let cons pos neg = let nnode = Node.make { pos = neg; neg = Obj.magic 0 } in let pnode = Node.make { pos = pos; neg = nnode } in @@ -135,7 +118,8 @@ let cons pos neg = let true_,false_ = cons True False -let atom_ p = fst (cons (Atom(p)) (Atom(P.neg p))) +let atom_ p = + let a, _ = cons (Atom(p, true)) (Atom(p, false)) in a let not_ f = f.Node.node.neg diff --git a/src/formula.mli b/src/boolean.mli similarity index 88% rename from src/formula.mli rename to src/boolean.mli index f69a40d..73af3c1 100644 --- a/src/formula.mli +++ b/src/boolean.mli @@ -15,9 +15,7 @@ module type ATOM = sig - type t - val neg : t -> t - include Hcons.Abstract with type t := t + include Hcons.S include Common_sig.Printable with type t := t end @@ -26,12 +24,12 @@ type ('formula,'atom) expr = | True | Or of 'formula * 'formula | And of 'formula * 'formula - | Atom of 'atom + | Atom of 'atom * bool (** View of the internal representation of a formula, used for pattern matching *) -module Make(P : ATOM) : +module Make(A : ATOM) : sig type t @@ -46,7 +44,7 @@ sig val equal : t -> t -> bool (** Equality over formulae *) - val expr : t -> (t,P.t) expr + val expr : t -> (t,A.t) expr (** Return a view of the formulae *) val compare : t -> t -> int @@ -67,9 +65,8 @@ sig val false_ : t (** Atom False *) - val atom_ : P.t -> t - (** [atom_ dir b q] creates a down_left or down_right atom for state - [q]. The atom is positive if [b == true]. + val atom_ : A.t -> t + (** [atom_ a] creates a new formula consisting of the atome a. *) val not_ : t -> t diff --git a/src/xpath/compile.ml b/src/xpath/compile.ml index c52c720..8ab26fb 100644 --- a/src/xpath/compile.ml +++ b/src/xpath/compile.ml @@ -17,11 +17,11 @@ open Ast let ( => ) a b = (a, b) -let ( ++ ) a b = Ata.SFormula.or_ a b -let ( %% ) a b = Ata.SFormula.and_ a b +let ( ++ ) a b = Ata.Formula.or_ a b +let ( %% ) a b = Ata.Formula.and_ a b let ( @: ) a b = StateSet.add a b -module F = Ata.SFormula +module F = Ata.Formula let node_set = QNameSet.remove QName.document QNameSet.any @@ -121,7 +121,7 @@ let rec compile_expr e trans states = states2 | Fun_call (f, [ e0 ]) when (QName.to_string f) = "not" -> let phi, trans0, states0 = compile_expr e0 trans states in - (Ata.SFormula.not_ phi), + (F.not_ phi), trans0, states0 | Path p -> compile_path p trans states @@ -130,9 +130,9 @@ let rec compile_expr e trans states = and compile_path paths trans states = List.fold_left (fun (aphi, atrans, astates) p -> let phi, ntrans, nstates = compile_single_path p atrans astates in - (Ata.SFormula.or_ phi aphi), + (F.or_ phi aphi), ntrans, - nstates) (Ata.SFormula.false_,trans,states) paths + nstates) (F.false_,trans,states) paths and compile_single_path p trans states = let steps = @@ -147,7 +147,7 @@ and compile_single_path p trans states = and compile_step_list l trans states = match l with - | [] -> Ata.SFormula.true_, trans, states + | [] -> F.true_, trans, states | (axis, test, elist) :: ll -> let phi0, trans0, states0 = compile_step_list ll trans states in let phi1, trans1, states1 = @@ -182,7 +182,7 @@ let compile_top_level_step_list l trans states = is attribute *) let phi0 = if axis != Attribute then - phi0 %% (Ata.SFormula.not_ Ata.SFormula.is_attribute) + phi0 %% (F.not_ F.is_attribute) else phi0 in match ll with @@ -214,7 +214,7 @@ let compile_top_level_step_list l trans states = compile_axis_test Self (QNameSet.singleton QName.document, Tree.NodeKind.Node) - Ata.SFormula.true_ + F.true_ trans states in -- 2.17.1