Use Continuation Passing Style #3
Description
After tinkering around with variational arithmetic I've concluded I need a zipper to handle deeply nested choices. Consider this formula:
deepChoicesLHS :: IO Result
deepChoicesLHS = flip sat Nothing $
(1 - 2 - (3 - c)) .== 23
where c = iChc "AA" (iRef ("Aleft" :: Text)) (iRef "Aright") +
iChc "BB" (iRef "Bleft") (iRef "BRight")
The trick for the booleans was to rotate the AST hence allows plain values to be accumulated/evaluated thereby lifting choices, but for arithmetic this does not work because - is neither commutative or associative, and thus the only way to get to the choice here is to crawl the tree, capturing the context until we find the choice. In Vsat I used a zipper for this before I understood the tree rotations. For VSMT CPS will likely be faster than a zipper and more memory efficient, thus it is desirable. Furthermore, I conjectured and am pretty confident that continuations are the essence of variation and so the fact that CPS sticks out to me is likely an indication of this conjecture.