+ let fo_p = trans_pr pred in
+ let q,q' = Asta.new_state(), Asta.new_state() in
+ Asta.add_selec asta q';
+ Asta.add_quer asta q;
+ Asta.add_quer asta q';
+ Asta.add_top asta q;
+ Asta.add_top asta q';
+ Asta.add_bot asta q;
+ Asta.add_bot asta q';
+ let Simple lab = test in
+ let tr_selec = (q', lab, fo_p)
+ and tr_q = (q, Asta.any_label, form_propa_selec q q' ax) in
+ Asta.add_tr asta tr_selec true;
+ Asta.add_tr asta tr_q true
+
+ and trans_step (ax,test,pred) = (* add a new state for the step *)
+ let fo_p = trans_pr pred
+ and q = Asta.new_state() in
+ let Simple label = test
+ and form_next = (fo_p) *& (* (\/ top_next) /\ predicat *)
+ (List.fold_left (fun acc x -> (`Left *+ x ) +| acc)
+ Formula.false_ (Asta.top_states asta)) in
+ let tr_next = (q, label, form_next)
+ and tr_propa = (q, Asta.any_label, form_propa q ax) in
+ Asta.add_quer asta q;
+ Asta.add_top asta q;
+ Asta.add_bot asta q;
+ Asta.add_tr asta tr_next true;
+ Asta.add_tr asta tr_propa true;
+ Asta.init_top asta;
+ Asta.add_top asta q
+
+ and trans_pr = function (* either we apply De Morgan rules
+ in xPath:parse or here *)
+ | Expr True -> Formula.true_
+ | Expr False -> Formula.false_
+ | Or (p_1,p_2) -> trans_pr(p_1) +| trans_pr(p_2)
+ | And (p_1,p_2) -> trans_pr(p_1) *& trans_pr(p_2)
+ | Not (Expr Path q) -> (trans_pr_path false q)
+ | Expr Path q -> (trans_pr_path true q)
+ | x -> print_predicate pr_er x; raise Not_core_XPath