1 (***********************************************************************)
5 (* Kim Nguyen, LRI UMR8623 *)
6 (* Université Paris-Sud & CNRS *)
8 (* Copyright 2010-2013 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 (***********************************************************************)
17 Time-stamp: <Last modified on 2013-03-04 17:55:28 CET by Kim Nguyen>
25 Ata.SFormula.atom_ (Ata.Move.make (l,b,q))
27 let ( => ) a b = (a, b)
28 let ( ** ) l q = mk_atom l true q
29 let ( ++ ) a b = Ata.SFormula.or_ a b
30 let ( %% ) a b = Ata.SFormula.and_ a b
31 let ( @: ) a b = StateSet.add a b
33 (* [compile_axis_test axis test q phi trans states] Takes an xpath
34 [axis] and node [test], a formula [phi], a list of [trans]itions
35 and a set of [states] and returns a formula [phi'], a new set of
36 transitions, and a new set of states such that [phi'] holds iff
37 there exists a node reachable through [axis]::[test] where [phi]
41 let compile_axis_test axis test phi trans states =
42 let q = State.make () in
43 let phi', trans', states' =
47 (q, [ test => phi ]) :: trans,
53 QNameSet.any => (`Right ** q) ]) :: trans,
57 (if self then (`Epsilon ** q) else (`Left ** q)),
59 QNameSet.any => (`Left ** q) %% (`Right ** q) ]) :: trans,
63 let q' = State.make () in
64 let move = (`Up1 ** q) ++ (`Up2 ** q') in
67 :: (q', [ QNameSet.any => move ]) :: trans,
71 let q' = State.make () in
72 let move = (`Up1 ** q) ++ (`Up2 ** q') in
73 (if self then (`Epsilon ** q) else move),
75 QNameSet.any => move ])
76 :: (q', [ QNameSet.any => move ]) :: trans,
79 | FollowingSibling | PrecedingSibling ->
81 if axis = PrecedingSibling then
87 QNameSet.any => move ]) :: trans,
91 let q' = State.make () in
92 let test = if QNameSet.is_finite test then
93 QNameSet.fold (fun tag acc ->
94 QNameSet.add (QName.add_attribute_prefix tag) acc)
99 (q, [ QNameSet.singleton QName.attribute_map => (`Left ** q') ])
100 :: (q', [ test => phi;
101 QNameSet.any => (`Right ** q') ]) :: trans,
106 phi', trans', q @: states'
109 let compile_rev_axis_test axis test phi trans states =
111 | Attribute -> assert false
112 | _ -> compile_axis_test (invert_axis axis) test phi trans states
117 let rec compile_expr e trans states =
119 | Binop (e1, (And|Or as op), e2) ->
120 let phi1, trans1, states1 = compile_expr e1 trans states in
121 let phi2, trans2, states2 = compile_expr e2 trans1 states1 in
122 (if op = Or then phi1 ++ phi2 else phi1 %% phi2),
125 | Fun_call (f, [ e0 ]) when (QName.to_string f) = "not" ->
126 let phi, trans0, states0 = compile_expr e0 trans states in
127 (Ata.SFormula.not_ phi),
130 | Path p -> compile_path p trans states
133 and compile_path paths trans states =
134 List.fold_left (fun (aphi, atrans, astates) p ->
135 let phi, ntrans, nstates = compile_single_path p atrans astates in
136 (Ata.SFormula.or_ phi aphi),
138 nstates) (Ata.SFormula.false_,trans,states) paths
140 and compile_single_path p trans states =
144 (Ancestor false, QNameSet.singleton QName.document, [])::steps
145 | Relative steps -> steps
147 compile_step_list steps trans states
149 and compile_step_list l trans states =
151 | [] -> Ata.SFormula.true_, trans, states
152 | (axis, test, elist) :: ll ->
153 let phi0, trans0, states0 = compile_step_list ll trans states in
154 let phi1, trans1, states1 =
155 compile_axis_test axis test phi0 trans0 states0
157 List.fold_left (fun (aphi, atrans, astates) e ->
158 let ephi, etrans, estates = compile_expr e atrans astates in
159 aphi %% ephi, etrans, estates) (phi1, trans1, states1) elist
161 let compile_top_level_step_list l trans states =
162 let rec loop l trans states phi_above =
164 | (axis, test, elist) :: [] ->
165 let phi0, trans0, states0 =
166 compile_rev_axis_test axis QNameSet.any phi_above trans states
168 let phi1, trans1, states1 =
169 List.fold_left (fun (aphi, atrans, astates) e ->
170 let ephi, etrans, estates = compile_expr e atrans astates in
171 aphi %% ephi, etrans, estates) (phi0, trans0, states0) elist
173 let _, trans2, states2 =
174 compile_axis_test Self test phi1 trans1 states1
177 StateSet.choose (StateSet.diff states2 states1)
179 marking_state, trans2, states2
180 | (axis, test, elist) :: ll ->
181 let phi0, trans0, states0 =
182 compile_rev_axis_test axis QNameSet.any phi_above trans states
184 let phi1, trans1, states1 =
185 compile_axis_test Self test phi0 trans0 states0
187 let phi2, trans2, states2 =
188 List.fold_left (fun (aphi, atrans, astates) e ->
189 let ephi, etrans, estates = compile_expr e atrans astates in
190 aphi %% ephi, etrans, estates) (phi1, trans1, states1) elist
192 loop ll trans2 states2 phi2
195 let phi0, trans0, states0 =
198 (QNameSet.singleton QName.document)
203 loop l trans0 states0 phi0
208 let mstates, trans, states = List.fold_left (fun (ams, atrs, asts) p ->
209 let ms, natrs, nasts =
211 | Absolute l | Relative l -> compile_top_level_step_list l atrs asts
213 (StateSet.add ms ams), natrs, nasts) (StateSet.empty, [], StateSet.empty) p
215 let a = Ata.create () in
216 a.Ata.states <- states;
217 a.Ata.selection_states <- mstates;
218 List.iter (fun (q, l) ->
219 List.iter (fun (lab, phi) ->
220 Ata.add_trans a q lab phi
222 Ata.complete_transitions a;
223 Ata.normalize_negations a;