+
+ (* Builds asta for predicate and gives the formula which must be satsified *)
+ and trans_pr_path posi = function
+ | Relative [] -> if posi then Formula.true_ else Formula.false_
+ | Relative steps -> List.fold_left
+ (fun acc x -> if posi then (`Left *+ x) +| acc else (`Left *- x) +| acc)
+ Formula.false_ (trans_pr_step_l steps)
+ | AbsoluteDoS steps as x -> print pr_er x; raise Not_core_XPath
+ | Absolute steps as x -> print pr_er x; raise Not_core_XPath
+
+ (* Builds asta for a predicate query and give the formula *)
+ and trans_pr_step_l = function
+ | [step] -> trans_pr_step [] step
+ | step :: tl -> let list_top = trans_pr_step_l tl in
+ trans_pr_step list_top step
+ | [] -> failwith "Can not happened! 1"
+
+ (* Add a step on the top of a list of states in a predicate *)
+ and trans_pr_step list (ax,test,pred) =
+ let form_next =
+ if list = []
+ then trans_pr pred
+ else (trans_pr pred) *&
+ (List.fold_left (fun acc x -> (`Left *+ x) +| acc)
+ Formula.false_ list)
+ and q = Asta.new_state()
+ and Simple label = test in
+ let tr_next = (q,label, form_next)
+ and tr_propa = (q, Asta.any_label, form_propa q ax) in
+ Asta.add_reco asta q;
+ Asta.add_tr asta tr_next false;
+ Asta.add_tr asta tr_propa false;
+ [q] (* always one element here, but more with self
+ axis *)
+ (* Gives the propagation formula *)