Open axch opened 8 years ago
Why do they have AAALKernels?
https://github.com/probcomp/Venturecxx/blob/master/examples/tutorial-2015/regress_mem.py#L85
@luac Considered the version suggested above and was weirded out by the concept of mutating the aux of a procedure that was passed in from outside the abstraction boundary. One resolution is to call it _regress_mem
and explain only the compound that uses it. In any case, the compound should solve the "first package" and "second package" bugs, by avoiding a primitive that needs to return two SP objects. And now that we have assume_values
, that compound is even reasonable to use.
I thought about this a bit more, and this actually doesn't change anything with respect to the possibility of "first package" bug, but now I'm unconvinced that it ever really existed, because the type of AAA procedure that would expose it might break some other contracts anyway.
(Basically, the "first package" bug is the fact that we pull out the spAux from the input procedure, and an AAA update that changes the identity of the spAux would fail to propagate through, but AAA updates are kind of defined as being conditioned on the spAux, so I'm not sure such a situation would make sense to begin with.)
Then define gpmem in terms of it, as