(* Builds asta for predicate and gives the formula which must be satsified *)
and trans_pr_path posi = function
| Relative [] -> if posi then Formula.true_ else Formula.false_
- | Relative steps -> List.fold_left
- (fun acc x -> if posi then (`Left *+ x) +| acc else (`Left *- x) +| acc)
- Formula.false_ (trans_pr_step_l steps)
+ | Relative steps ->
+ let dir = match ax_ (List.hd steps) with
+ | Self -> `Self
+ | FollowingSibling -> `Right
+ | _ -> `Left in
+ List.fold_left
+ (fun acc x -> if posi then (dir *+ x) +| acc else (dir *- x) +| acc)
+ Formula.false_ (trans_pr_step_l steps)
| AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
| Absolute steps as x -> print pr_er x; raise Not_core_XPath
-
+
(* Builds asta for a predicate query and give the formula *)
and trans_pr_step_l = function
| [step] -> trans_pr_step [] step (Self) (* Self doesn't matter since [] *)
| step :: tl -> let list_top = trans_pr_step_l tl in
- trans_pr_step list_top step (ax_ (List.hd tl))
+ trans_pr_step list_top step (ax_ (List.hd tl))
| [] -> failwith "Can not happened! 1"
-
+
(* Add a step on the top of a list of states in a predicate *)
and trans_pr_step list (ax,test,pred) ax_next =
let form_next =
| Child -> `Right *+ q +| `Right *+ q'
| Descendant -> (`Left *+ q +| `Right *+ q) +| (`Left *+ q' +| `Right *+ q')
| Self -> `Self *+ q'
- | FollowingSibling -> `Right *+ q +| `Self *+ q'
+ | FollowingSibling -> `Right *+ q +| `Right *+ q'
| x -> print_axis pr_er x; raise Not_core_XPath
in
type 'hcons node = {
pos : 'hcons expr;
mutable neg : 'hcons;
- st : StateSet.t * StateSet.t;
+ st : StateSet.t * StateSet.t * StateSet.t;
size: int; (* Todo check if this is needed *)
}
pnode,nnode
-let empty_pair = StateSet.empty, StateSet.empty
-let true_,false_ = cons True False empty_pair empty_pair 0 0
+let empty_triple = StateSet.empty, StateSet.empty, StateSet.empty
+let true_,false_ = cons True False empty_triple empty_triple 0 0
let atom_ d p s =
let si = StateSet.singleton s in
let ss = match d with
- | `Left -> si, StateSet.empty
- | `Right -> StateSet.empty, si
- | `Self -> StateSet.empty, StateSet.empty (* TODO WHAT? *)
+ | `Left -> StateSet.empty, si, StateSet.empty
+ | `Right -> StateSet.empty, StateSet.empty, si
+ | `Self -> si, StateSet.empty, StateSet.empty
in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1)
let not_ f = f.Node.node.neg
-let union_pair (l1,r1) (l2, r2) =
+let union_triple (s1,l1,r1) (s2,l2, r2) =
+ StateSet.union s1 s2,
StateSet.union l1 l2,
StateSet.union r1 r2
let merge_states f1 f2 =
let sp =
- union_pair (st f1) (st f2)
+ union_triple (st f1) (st f2)
and sn =
- union_pair (st (not_ f1)) (st (not_ f2))
+ union_triple (st (not_ f1)) (st (not_ f2))
in
sp,sn
val expr : t -> t expr
(** Equality over formulae *)
-val st : t -> StateSet.t * StateSet.t
-(** states occuring left and right, positively or negatively *)
+val st : t -> StateSet.t * StateSet.t * StateSet.t
+(** states occuring self, left and right, positively or negatively *)
val compare : t -> t -> int
(** Comparison of formulae *)
(* compute states occuring in transition candidates *)
let rec add_st (ql,qr) = function
| [] -> ql,qr
- | f :: tl -> let sql,sqr = Formula.st f in
+ | f :: tl -> let sqs,sql,sqr = Formula.st f in
let ql' = StateSet.union sql ql
and qr' = StateSet.union sqr qr in
add_st (ql',qr') tl in
let doc = doc () in
let query = query () in
let asta = build_asta query in
- let run = compute_run doc asta in
+ let run = compute_run doc asata in
let selected_nodes = Run.selected_nodes doc asta in
Format.pp_set_margin err_formatter 80;
fprintf err_formatter "@[<v 0>##### Query #####@. %a@]\n"