src/compil.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                   Lucca Hirschi, LRI UMR8623                        *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   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   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 open XPath.Ast
  17 open Formula.Infix
  18
  19 exception Not_core_XPath
  20 (** Raised whenever the XPath query contains not implemented structures *)
  21
  22 let pr_er = Format.err_formatter
  23
  24 let ax_ (a,b,c) = a
  25
  26 let trans query =
  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
  32     | [s] -> trans_last s
  33     | s :: tl -> trans tl; trans_step s (ax_(List.hd tl))
  34     | [] -> ()
  35
  36   (* Add THE top most state for top-level query (done in the end) *)
  37   and trans_init () =
  38     let top_st = Asta.new_state () in
  39     let or_top =
  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;
  43     Asta.init_top asta;
  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
  47
  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';
  53     Asta.add_quer asta q;
  54     Asta.add_quer asta q';
  55     Asta.add_top asta q;
  56     Asta.add_top 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
  63
  64   and form_next_step ax_next top_states_next form_pred =
  65     match ax_next with
  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)
  75
  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
  84     Asta.add_quer asta q;
  85     Asta.add_top asta q;
  86     Asta.add_bot asta q;
  87     Asta.add_tr asta tr_next true;
  88     Asta.add_tr asta tr_propa true;
  89     Asta.init_top asta;
  90     Asta.add_top asta q
  91
  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
 102
 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_
 106     | Relative steps ->
 107       let dir = match ax_ (List.hd steps) with
 108         | Self -> `Self
 109         | FollowingSibling -> `Right
 110         | _ -> `Left in
 111       List.fold_left
 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
 116
 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"
 123
 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 =
 126     let form_next =
 127       if list = []
 128       then trans_pr pred
 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
 138                                            axis *)
 139   (* Gives the propagation formula *)
 140   and form_propa q = function
 141     | Child -> `Right *+ q
 142     | Descendant -> (`Left *+ q +| `Right *+ q)
 143     | Self -> `Self *+ q
 144     | FollowingSibling -> `Right *+ q
 145     | x -> print_axis pr_er x; raise Not_core_XPath
 146
 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
 154
 155   in
 156   (* Match the top-level query *)
 157   match query with
 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