ensure_wd_node([N | Ns], H, RemainingPOs, [Wd|Wds]) :-
!, % Special case: List.
ensure_wd_node_list([N | Ns], H, NestedRemainingPOs, [Wd|Wds]),
append(NestedRemainingPOs, RemainingPOs).
ensure_wd_node(field(Name,Expr), H, RemainingPOs, NewAst) :-
% special case for records b(rec([field(Name,Expr),...]),_,_)
!,
ensure_wd_node(Expr, H, RemainingPOs, WdExpr),
NewAst = field(Name,WdExpr).
ensure_wd_node(b(record_field(Id,Atom),Type,Info), _, [], NewAst) :-
!,
NewAst = b(record_field(Id,Atom),Type,Info).
ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
% Special cases: POs to LHS (middle child)
Cases = [general_sum, general_product, quantified_intersection, quantified_union, lambda, forall],
node_split(Node, Name, [Ids, Pred, Expr]),
member(Name, Cases),
!,
wd_to_lhs(Pred, Expr, H, WdPred, WdExpr),
node_split(WdNode, Name, [Ids, WdPred, WdExpr]),
WdAst = b(WdNode, Type, Info),
toplevel_wd_pos(WdAst, H, RootPOs),
conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
% Special cases: POs to RHS (last child)
Cases = [event_b_comprehension_set],
node_split(Node, Name, [Ids, Expr, Pred]),
member(Name, Cases),
!,
wd_to_rhs(Expr, Pred, H, WdExpr, WdPred),
node_split(WdNode, Name, [Ids, WdExpr, WdPred]),
WdAst = b(WdNode, Type, Info),
toplevel_wd_pos(WdAst, H, RootPOs),
conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
ensure_wd_node(b(assertion_expression(Test, ErrText, Value), Type, Info), H, POs, Result) :-
Result = b(assertion_expression(Test, ErrText, WdValue), Type, Info),
ensure_wd_node(Value, H, POs, WdValue).
ensure_wd_node(b(if_then_else(If, Then, Else), Type, Info), H, POs, WdIfThenElse) :-
Type \= pred, !, % Special case for If-Expressions.
ensure_wd_node(If, H, [], WdIf),
push_hyp(H, If, [create_full_po], ThenH),
transform_wd(Then, H, [discharge_po], TThen),
ensure_wd_node(TThen, ThenH, ThenPOs, WdThen),
negate_hyp(If, NotIf),
push_hyp(H, NotIf, [create_full_po], ElseH),
ensure_wd_node(Else, ElseH, ElsePOs, WdElse),
if_then_else_po(WdIf, ThenPOs, IfThen),
ensure_wd_node(NotIf, H, [], WdNotIf),
if_then_else_po(WdNotIf, ElsePOs, NotIfElse),
WdIfThenElse = b(if_then_else(WdIf, WdThen, WdElse), Type, Info),
append(IfThen, NotIfElse, POs).
ensure_wd_node(b(Node, Type, Info), H, RemainingPOs, NewAst) :-
% Special cases: WD constraints from LHS chain into RHS
Cases = [conjunct,implication],
node_split(Node, Name, [Lhs, Rhs]),
member(Name, Cases),
!,
ensure_wd_node(Lhs, H, [], WdLhs),
push_hyp(H, WdLhs, [create_full_po], RhsH),
ensure_wd_node(Rhs, RhsH, [], WdRhs),
node_split(WdNode, Name, [WdLhs, WdRhs]),
WdAst = b(WdNode, Type, Info),
toplevel_wd_pos(WdAst, H, RootPOs),
conjunct_or_propagate_pos(WdAst, RootPOs, NewAst, RemainingPOs).
ensure_wd_node(Node, H, RemainderPOs, WdPred) :-
wd_children_and_pos(Node, H, POs, InterNode),
conjunct_or_propagate_pos(InterNode, POs, WdPred, RemainderPOs).