Unbind Variables On Backtracking

Stratego -- Strategies for Program Transformation
After a strategy fails, variables that have been bound in matches should be unbound. This is not supported by the current compilation scheme. The following example illustrates the problem. The strategy f should behave the same as the choice between g and h.

module unbind-on-backtrack 
  f = (?(x, y); ?(x, x) <+ ?(y, x)); ![y,x]  

  g = ?(x, y); ?(x, x); ![y,x] 
  h = ?(y, x); ![y,x]  

  main = 
    <g <+ h> ("a", "b") => ["a", "b"]
  ; <f> ("a", "b") => ["a", "b"]               

-- EelcoVisser - 22 Nov 2001

One way: only bind unbound variables when choice is committed: Consider

  ?F(x, y); s1 <+ s2
and assume that x is bound before invocation of this strategy and that y is not (y value is looked for). transform this into
  {y: ?F(x, y); s1; split(id,!y)}; ?(_,y); Fst <+ s2
This has the same effect as the earlier expression (can this insight be made more efficient? turned into primitive operations?)

Note: this assume one can determine statically which variables are unbound when entering a choice. Although this scheme works when y is bound, it might turn out very expensive, because a failing match to y is discovered after doing s1.

-- EelcoVisser - 2000

Solution: Save (the status of) all variables that are bound in the left branch of a choice and restore after failure. Shouldn't be too difficult.

-- EelcoVisser - 22 Nov 2001