+ 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) -> Formula.true_ (* todo *)
+ | Expr Path q -> Formula.true_ (* todo *)
+ | x -> print_predicate pr_er x; raise Not_core_XPath
+
+ and form_propa q = function
+ | Child -> `Right *+ q
+ | Descendant -> (`Left *+ q +| `Right *+ q)
+ | x -> print_axis pr_er x; raise Not_core_XPath