Add residuation
Basically, implement ensureNotFree
and concurrent conjunction &
.
For instance,
Prelude> x+2 =:= y & x=:=1 where x,y free
{x=1, y=3} True
should be successful instead of producing a run-time error.
e1 & e2
could be implemented by starting goroutines to evaluate e1
and e2
concurrently.
ensureNotFree x
does not fail if x
is unbound but should suspend until x
is bound to some value
(in the current search branch). Note that there might be some interaction between
concurrency of &
and non-determinism.
Start this development in a new experimental branch.