From: Kim Nguyễn Date: Tue, 5 Mar 2013 18:22:09 +0000 (+0100) Subject: Working for element only document (with arbitrary paths & negation). X-Git-Tag: v0.1~161 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=249bd234500a64919cf00f4a59ab4927a068d689 Working for element only document (with arbitrary paths & negation). - Need to fix attributes handling - Need to add preceding/following --- diff --git a/src/auto/ata.ml b/src/auto/ata.ml index f4f11db..275d657 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,27 +14,30 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" open Format open Utils -type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ] +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 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 = - { left = a; right = b; up1 = c; up2 = d; epsilon = e } +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 }" +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 ) = struct @@ -67,27 +70,40 @@ struct | `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; - State.print _str_fmt s; + if s != State.dummy then State.print _str_fmt s; let str = _flush_str_fmt () in - if b then fprintf ppf "%s" str - else Pretty.pp_overline ppf str - + 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 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 + 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 end @@ -234,11 +250,13 @@ let normalize_negations auto = | 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 - if b == b' then begin + 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)) - end else begin + if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo; + SFormula.atom_ (Move.make (l, true, 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 @@ -253,10 +271,11 @@ let normalize_negations auto = Not_found -> (* create a new state and add it to the todo queue *) let nq = State.make () in - if not (StateSet.mem q auto.bottom_states) then + 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; + auto.top_states <- StateSet.add nq auto.top_states; *) Hashtbl.add memo_state (q, false) nq; Queue.add (q, false) todo; nq in @@ -276,10 +295,11 @@ let normalize_negations auto = Not_found -> let nq = if b then q else let nq = State.make () in - if not (StateSet.mem q auto.bottom_states) then + 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; + auto.top_states <- StateSet.add nq auto.top_states; *) nq in Hashtbl.add memo_state key nq; nq diff --git a/src/auto/eval.ml b/src/auto/eval.ml index 4647b84..f3b81cb 100644 --- a/src/auto/eval.ml +++ b/src/auto/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -33,6 +33,7 @@ module Make (T : Tree.Sig.S) = struct let eval_trans l ctx acc = List.fold_left (fun (acct, accs) ((q, phi) as trs) -> + if StateSet.mem q accs then (acct, accs) else if Ata.SFormula.eval ctx phi then (acct, StateSet.add q accs) else @@ -49,18 +50,19 @@ module Make (T : Tree.Sig.S) = struct let states0 = get cache tree node in let tag = T.tag tree node in let trans0 = Ata.get_trans auto auto.Ata.states tag in - let parent_states = if parent == T.nil then auto.Ata.top_states else get cache tree parent in - let fc_states = if fc == T.nil then auto.Ata.bottom_states else get cache tree fc in - let ns_states = if ns == T.nil then auto.Ata.bottom_states else get cache tree ns in + let parent_states = (*if parent == T.nil then auto.Ata.top_states else*) get cache tree parent in + let fc_states = (*if fc == T.nil then auto.Ata.bottom_states else*) get cache tree fc in + let ns_states = (*if ns == T.nil then auto.Ata.bottom_states else*) get cache tree ns in + let is_root = parent == T.nil in let ctx0 = if is_left then - Ata.make_ctx fc_states ns_states parent_states StateSet.empty states0 + Ata.make_ctx fc_states ns_states parent_states StateSet.empty states0 is_left is_root else - Ata.make_ctx fc_states ns_states StateSet.empty parent_states states0 + Ata.make_ctx fc_states ns_states StateSet.empty parent_states states0 is_left is_root in - eprintf "[Iteration % 4d] node: %a, context: %a\n%!" + eprintf "-- [Iteration % 4d] --\n node: %a\n context: %a\n%!" i T.print_node node Ata.print_ctx ctx0; - List.iter (fun (q, phi) -> eprintf "%a -> %a\n" State.print q Ata.SFormula.print phi) trans0; + List.iter (fun (q, phi) -> eprintf " %a -> %a\n" State.print q Ata.SFormula.print phi) trans0; eprintf "----------------------\n%!"; let trans1, states1 = eval_trans trans0 ctx0 StateSet.empty in if states1 != states0 then set cache tree node states1; diff --git a/src/xpath/compile.ml b/src/xpath/compile.ml index f1212f2..15a5c60 100644 --- a/src/xpath/compile.ml +++ b/src/xpath/compile.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) open Ast @@ -26,10 +26,20 @@ let mk_atom l b q = let ( => ) a b = (a, b) let ( ** ) l q = mk_atom l true q +let is_left = mk_atom `Is1 true State.dummy +let is_right = mk_atom `Is2 true State.dummy let ( ++ ) a b = Ata.SFormula.or_ a b let ( %% ) a b = Ata.SFormula.and_ a b let ( @: ) a b = StateSet.add a b +let node_set = QNameSet.remove QName.document QNameSet.any +let star_set = QNameSet.diff QNameSet.any ( + List.fold_right (QNameSet.add) + [ QName.document; QName.text; QName.attribute_map ] + QNameSet.empty) +let attribute = QNameSet.singleton QName.attribute_map +let root_set = QNameSet.singleton QName.document + (* [compile_axis_test axis test q phi trans states] Takes an xpath [axis] and node [test], a formula [phi], a list of [trans]itions and a set of [states] and returns a formula [phi'], a new set of @@ -56,12 +66,13 @@ let compile_axis_test axis test phi trans states = | Descendant self -> (if self then (`Epsilon ** q) else (`Left ** q)), (q, [ test => phi; - QNameSet.any => (`Left ** q) ++ (`Right ** q) ]) :: trans, + QNameSet.any => (`Left ** q); + QNameSet.any => (`Right ** q) ]) :: trans, states | Parent -> let q' = State.make () in - let move = (`Up1 ** q) ++ (`Up2 ** q') in + let move = (`Up1 ** q %% is_left) ++ (`Up2 ** q' %% is_right) in move, (q, [ test => phi ]) :: (q', [ QNameSet.any => move ]) :: trans, @@ -69,10 +80,10 @@ let compile_axis_test axis test phi trans states = | Ancestor self -> let q' = State.make () in - let move = (`Up1 ** q) ++ (`Up2 ** q') in + let move = (`Up1 ** q %% is_left) ++ (`Up2 ** q' %% is_right) in (if self then (`Epsilon ** q) else move), (q, [ test => phi; - QNameSet.any => move ]) + star_set => move ]) :: (q', [ QNameSet.any => move ]) :: trans, (q' @: states) @@ -80,11 +91,11 @@ let compile_axis_test axis test phi trans states = let move = if axis = PrecedingSibling then (`Up2 ** q) - else (`Right ** q) + else (`Right ** q %% is_right) in move, (q, [ test => phi; - QNameSet.any => move ]) :: trans, + star_set => move ]) :: trans, states | Attribute ->