Files for the next step: run.ml?
[tatoo.git] / src / compil.ml
1 (***********************************************************************)
2 (*                                                                     *)
3 (*                               TAToo                                 *)
4 (*                                                                     *)
5 (*                  Lucca Hirschi, ?   *)
6 (*                  ?   *)
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 trans query =
25   let asta = Asta.empty in
26   (* Buidling of the ASTA step by step with a special case for the last
27      step. Then add a top most state. Each function modifies asta. *)
28   let rec trans = function              (* builds asta from the bottom of the query *)
29     | [s] -> trans_last s
30     | s :: tl ->  trans tl; trans_step s
31     | [] -> ()
32       
33   and trans_init () =                   (* add THE top most state  *)
34     let top_st = Asta.new_state () in
35     let or_top = 
36       List.fold_left (fun acc x -> ((`Left *+ x) +| acc))
37         (Formula.false_) (Asta.top_states asta)
38     in
39     Asta.add_quer asta top_st;
40     Asta.init_top asta;
41     Asta.add_top asta top_st;
42     Asta.add_tr asta (top_st, Asta.any_label, or_top) true
43       
44   and trans_last (ax,test,pred) =       (* a selecting state is needed *)
45     let fo_p = trans_pr pred in
46     let q,q' = Asta.new_state(), Asta.new_state() in
47     Asta.add_selec asta q';
48     Asta.add_quer asta q;
49     Asta.add_quer asta q';
50     Asta.add_top asta q;
51     Asta.add_top asta q';
52     Asta.add_bot asta q;
53     Asta.add_bot asta q';
54     let Simple lab = test in
55     let tr_selec = (q', lab, fo_p)
56     and tr_q = (q, Asta.any_label, form_propa_selec q q' ax) in
57     Asta.add_tr asta tr_selec true;
58     Asta.add_tr asta tr_q true
59     
60   and trans_step (ax,test,pred) =       (* add a new state for the step *)
61     let fo_p = trans_pr pred
62     and q = Asta.new_state() in
63     let Simple label = test
64     and form_next = (fo_p) *&                    (* (\/ top_next) /\ predicat *)
65       (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)
66          Formula.false_ (Asta.top_states asta)) in
67     let tr_next = (q, label, form_next)
68     and tr_propa = (q, Asta.any_label, form_propa q ax) in
69     Asta.add_quer asta q;
70     Asta.add_top asta q;
71     Asta.add_bot asta q;
72     Asta.add_tr asta tr_next true;
73     Asta.add_tr asta tr_propa true;
74     Asta.init_top asta;
75     Asta.add_top asta q
76       
77   and trans_pr  = function              (* either we apply De Morgan rules
78                                            in xPath.parse or here *)
79     | Expr True -> Formula.true_
80     | Expr False -> Formula.false_
81     | Or (p_1,p_2) -> trans_pr(p_1) +| trans_pr(p_2)
82     | And (p_1,p_2) -> trans_pr(p_1) *& trans_pr(p_2)
83     | Not (Expr Path q) -> (trans_pr_path false q)
84     | Expr Path q -> (trans_pr_path true q)
85     | x -> print_predicate pr_er x; raise Not_core_XPath
86       
87   and trans_pr_path posi = function             (* builds asta for predicate and gives
88                                                    the formula which must be satsified *)
89     | Relative [] -> if posi then Formula.true_ else Formula.false_
90     | Relative steps -> List.fold_left
91       (fun acc x -> if posi then (`Left *+ x) +| acc else (`Left *- x) +| acc)
92       Formula.false_ (trans_pr_step_l steps)
93     | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
94     | Absolute steps as x -> print pr_er x; raise Not_core_XPath
95       
96   and trans_pr_step_l = function        (* builds asta for a predicate query *)
97     | [step] -> trans_pr_step [] step
98     | step :: tl -> let list_top = trans_pr_step_l tl in
99                     trans_pr_step list_top step
100     | [] -> failwith "Can not happened! 1"
101
102   and trans_pr_step list (ax,test,pred) = (* add a step on the top of
103                                              list in a predicate *)
104     let form_next =
105       if list = []
106       then trans_pr pred
107       else (trans_pr pred) *&
108         (List.fold_left (fun acc x -> (`Left *+ x) +| acc)
109            Formula.false_ list)
110     and q = Asta.new_state() 
111     and Simple label = test in
112     let tr_next = (q,label, form_next)
113     and tr_propa = (q, Asta.any_label, form_propa q ax) in
114     Asta.add_reco asta q;
115     Asta.add_tr asta tr_next false;
116     Asta.add_tr asta tr_propa false;
117     [q]                                 (* always one element here, but not with self
118                                            axis*)
119
120   and form_propa q = function           (* gives the propagation formula *)
121     | Child -> `Right *+ q
122     | Descendant -> (`Left *+ q +| `Right *+ q)
123     | x -> print_axis pr_er x; raise Not_core_XPath 
124
125   and form_propa_selec q q' = function  (* the same with a  selecting state *)
126     | Child -> `Right *+ q +| `Right *+ q'
127     | Descendant -> (`Left *+ q +| `Right *+ q) +| (`Left *+ q' +| `Right *+ q')
128     | x -> print_axis pr_er x; raise Not_core_XPath 
129       
130   in
131   match query with                      (* match the top-level query *)
132     | Absolute steps -> trans steps; trans_init(); asta
133     | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
134     | Relative steps as x -> print pr_er x; raise Not_core_XPath