1 (***********************************************************************)
5 (* Lucca Hirschi, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2012 Université Paris-Sud and Centre National de la *)
9 (* Recherche Scientifique. All rights reserved. This file is *)
10 (* distributed under the terms of the GNU Lesser General Public *)
11 (* License, with the special exception on linking described in file *)
14 (***********************************************************************)
19 exception Not_core_XPath
20 (** Raised whenever the XPath query contains not implemented structures *)
22 let pr_er = Format.err_formatter
27 (* Buidling of the ASTA step by step with a special case for the last
28 step. Then add a top most state. Each function modifies asta. *)
29 let asta = Asta.empty in
30 (* builds asta from the bottom of the query *)
31 let rec trans = function
33 | s :: tl -> trans tl; trans_step s (ax_(List.hd tl))
36 (* Add THE top most state for top-level query (done in the end) *)
38 let top_st = Asta.new_state () in
40 List.fold_left (fun acc x -> ((`Left *+ x) +| acc))
41 (Formula.false_) (Asta.top_states asta) in
42 Asta.add_quer asta top_st;
44 Asta.add_top asta top_st;
45 Asta.add_bot asta top_st; (* for trees which are leaves *)
46 Asta.add_tr asta (top_st, Asta.any_label, or_top) true
48 (* A selecting state is needed *)
49 and trans_last (ax,test,pred) =
50 let fo_p = trans_pr pred in (* TODO (if ax=Self, only q *)
51 let q,q' = Asta.new_state(), Asta.new_state() in
52 Asta.add_selec asta q';
54 Asta.add_quer asta q';
57 Asta.add_bot asta q; (* q' \notin B !! *)
58 let Simple lab = test in
59 let tr_selec = (q', lab, fo_p)
60 and tr_q = (q, Asta.any_label, form_propa_selec q q' ax) in
61 Asta.add_tr asta tr_selec true;
62 Asta.add_tr asta tr_q true
64 and form_next_step ax_next top_states_next form_pred =
66 | Self -> (form_pred) *& (* (\/ top_next) /\ predicate *)
67 (List.fold_left (fun acc x -> (`Self *+ x ) +| acc)
68 Formula.false_ top_states_next)
69 | FollowingSibling -> (form_pred) *& (* (\/ top_next) /\ predicate *)
70 (List.fold_left (fun acc x -> (`Right *+ x ) +| acc)
71 Formula.false_ top_states_next)
72 | _ -> (form_pred) *& (* (\/ top_next) /\ predicate *)
73 (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)
74 Formula.false_ top_states_next)
76 (* Add a new state and its transitions for the step *)
77 and trans_step (ax,test,pred) ax_next =
78 let fo_p = trans_pr pred
79 and q = Asta.new_state() in
80 let Simple label = test
81 and form_next = form_next_step ax_next (Asta.top_states asta) fo_p in
82 let tr_next = (q, label, form_next)
83 and tr_propa = (q, Asta.any_label, form_propa q ax) in
87 Asta.add_tr asta tr_next true;
88 Asta.add_tr asta tr_propa true;
92 (* Translating of predicates. Either we apply De Morgan rules
93 in xPath.parse or here *)
94 and trans_pr = function
95 | Expr True -> Formula.true_
96 | Expr False -> Formula.false_
97 | Or (p_1,p_2) -> trans_pr(p_1) +| trans_pr(p_2)
98 | And (p_1,p_2) -> trans_pr(p_1) *& trans_pr(p_2)
99 | Not (Expr Path q) -> (trans_pr_path false q)
100 | Expr Path q -> (trans_pr_path true q)
101 | x -> print_predicate pr_er x; raise Not_core_XPath
103 (* Builds asta for predicate and gives the formula which must be satsified *)
104 and trans_pr_path posi = function
105 | Relative [] -> if posi then Formula.true_ else Formula.false_
107 let dir = match ax_ (List.hd steps) with
109 | FollowingSibling -> `Right
112 (fun acc x -> if posi then (dir *+ x) +| acc else (dir *- x) +| acc)
113 Formula.false_ (trans_pr_step_l steps)
114 | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
115 | Absolute steps as x -> print pr_er x; raise Not_core_XPath
117 (* Builds asta for a predicate query and give the formula *)
118 and trans_pr_step_l = function
119 | [step] -> trans_pr_step [] step (Self) (* Self doesn't matter since [] *)
120 | step :: tl -> let list_top = trans_pr_step_l tl in
121 trans_pr_step list_top step (ax_ (List.hd tl))
122 | [] -> failwith "Can not happened! 1"
124 (* Add a step on the top of a list of states in a predicate *)
125 and trans_pr_step list (ax,test,pred) ax_next =
129 else form_next_step ax_next list (trans_pr pred)
130 and q = Asta.new_state()
131 and Simple label = test in
132 let tr_next = (q,label, form_next)
133 and tr_propa = (q, Asta.any_label, form_propa q ax) in
134 Asta.add_reco asta q;
135 Asta.add_tr asta tr_next false;
136 Asta.add_tr asta tr_propa false;
137 [q] (* always one element here, but more with self
139 (* Gives the propagation formula *)
140 and form_propa q = function
141 | Child -> `Right *+ q
142 | Descendant -> (`Left *+ q +| `Right *+ q)
144 | FollowingSibling -> `Right *+ q
145 | x -> print_axis pr_er x; raise Not_core_XPath
147 (* The same with a selecting state *)
148 and form_propa_selec q q' = function
149 | Child -> `Right *+ q +| `Right *+ q'
150 | Descendant -> (`Left *+ q +| `Right *+ q) +| (`Left *+ q' +| `Right *+ q')
151 | Self -> `Self *+ q'
152 | FollowingSibling -> `Right *+ q +| `Right *+ q'
153 | x -> print_axis pr_er x; raise Not_core_XPath
156 (* Match the top-level query *)
158 | Absolute steps -> trans steps; trans_init(); asta
159 | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
160 | Relative steps as x -> print pr_er x; raise Not_core_XPath