(***********************************************************************) (* *) (* TAToo *) (* *) (* Kim Nguyen, LRI UMR8623 *) (* Université Paris-Sud & CNRS *) (* *) (* Copyright 2010-2013 Université Paris-Sud and Centre National de la *) (* Recherche Scientifique. All rights reserved. This file is *) (* distributed under the terms of the GNU Lesser General Public *) (* License, with the special exception on linking described in file *) (* ../LICENSE. *) (* *) (***********************************************************************) (* Time-stamp: *) open Ast open Auto open Utils let mk_atom l b q = Ata.SFormula.atom_ (Ata.Move.make (l,b,q)) let ( => ) a b = (a, b) let ( ** ) l q = mk_atom l true q let ( ++ ) a b = Ata.SFormula.or_ a b let ( %% ) a b = Ata.SFormula.and_ a b let ( @: ) a b = StateSet.add a b (* [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 transitions, and a new set of states such that [phi'] holds iff there exists a node reachable through [axis]::[test] where [phi] holds. *) let compile_axis_test axis test phi trans states = let q = State.make () in let phi', trans', states' = match axis with | Self -> (`Epsilon ** q), (q, [ test => phi ]) :: trans, states | Child -> (`Left ** q), (q, [ test => phi; QNameSet.any => (`Right ** q) ]) :: trans, states | Descendant self -> (if self then (`Epsilon ** q) else (`Left ** q)), (q, [ test => phi; QNameSet.any => (`Left ** q) %% (`Right ** q) ]) :: trans, states | Parent -> let q' = State.make () in let move = (`Up1 ** q) ++ (`Up2 ** q') in move, (q, [ test => phi ]) :: (q', [ QNameSet.any => move ]) :: trans, (q' @: states) | Ancestor self -> let q' = State.make () in let move = (`Up1 ** q) ++ (`Up2 ** q') in (if self then (`Epsilon ** q) else move), (q, [ test => phi; QNameSet.any => move ]) :: (q', [ QNameSet.any => move ]) :: trans, (q' @: states) | FollowingSibling | PrecedingSibling -> let move = if axis = PrecedingSibling then (`Up2 ** q) else (`Right ** q) in move, (q, [ test => phi; QNameSet.any => move ]) :: trans, states | Attribute -> let q' = State.make () in let test = if QNameSet.is_finite test then QNameSet.fold (fun tag acc -> QNameSet.add (QName.add_attribute_prefix tag) acc) test QNameSet.empty else test in (`Left ** q), (q, [ QNameSet.singleton QName.attribute_map => (`Left ** q') ]) :: (q', [ test => phi; QNameSet.any => (`Right ** q') ]) :: trans, (q' @:states) | _ -> assert false in phi', trans', q @: states' let compile_rev_axis_test axis test phi trans states = match axis with | Attribute -> assert false | _ -> compile_axis_test (invert_axis axis) test phi trans states ;; let rec compile_expr e trans states = match e with | Binop (e1, (And|Or as op), e2) -> let phi1, trans1, states1 = compile_expr e1 trans states in let phi2, trans2, states2 = compile_expr e2 trans1 states1 in (if op = Or then phi1 ++ phi2 else phi1 %% phi2), trans2, 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), trans0, states0 | Path p -> compile_path p trans states | _ -> assert false 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), ntrans, nstates) (Ata.SFormula.false_,trans,states) paths and compile_single_path p trans states = let steps = match p with | Absolute steps -> (Ancestor false, QNameSet.singleton QName.document, [])::steps | Relative steps -> steps in compile_step_list steps trans states and compile_step_list l trans states = match l with | [] -> Ata.SFormula.true_, trans, states | (axis, test, elist) :: ll -> let phi0, trans0, states0 = compile_step_list ll trans states in let phi1, trans1, states1 = compile_axis_test axis test phi0 trans0 states0 in List.fold_left (fun (aphi, atrans, astates) e -> let ephi, etrans, estates = compile_expr e atrans astates in aphi %% ephi, etrans, estates) (phi1, trans1, states1) elist let compile_top_level_step_list l trans states = let rec loop l trans states phi_above = match l with | (axis, test, elist) :: [] -> let phi0, trans0, states0 = compile_rev_axis_test axis QNameSet.any phi_above trans states in let phi1, trans1, states1 = List.fold_left (fun (aphi, atrans, astates) e -> let ephi, etrans, estates = compile_expr e atrans astates in aphi %% ephi, etrans, estates) (phi0, trans0, states0) elist in let _, trans2, states2 = compile_axis_test Self test phi1 trans1 states1 in let marking_state = StateSet.choose (StateSet.diff states2 states1) in marking_state, trans2, states2 | (axis, test, elist) :: ll -> let phi0, trans0, states0 = compile_rev_axis_test axis QNameSet.any phi_above trans states in let phi1, trans1, states1 = compile_axis_test Self test phi0 trans0 states0 in let phi2, trans2, states2 = List.fold_left (fun (aphi, atrans, astates) e -> let ephi, etrans, estates = compile_expr e atrans astates in aphi %% ephi, etrans, estates) (phi1, trans1, states1) elist in loop ll trans2 states2 phi2 | _ -> assert false in let phi0, trans0, states0 = compile_axis_test Self (QNameSet.singleton QName.document) Ata.SFormula.true_ trans states in loop l trans0 states0 phi0 ;; let path p = let mstates, trans, states = List.fold_left (fun (ams, atrs, asts) p -> let ms, natrs, nasts = match p with | Absolute l | Relative l -> compile_top_level_step_list l atrs asts in (StateSet.add ms ams), natrs, nasts) (StateSet.empty, [], StateSet.empty) p in let a = Ata.create () in a.Ata.states <- states; a.Ata.selection_states <- mstates; List.iter (fun (q, l) -> List.iter (fun (lab, phi) -> Ata.add_trans a q lab phi ) l) trans; Ata.complete_transitions a; Ata.normalize_negations a; a