G3Kappa
commented
1 year ago As it turns out, I was simply ignorant of the fact that an elegant TCO solution was just behind the corner. There was no need to refactor the mutual recursion away; instead, SolveTerm() now returns a "dummy" solution when the callee is tail recursive. SolveQuery() then erases the current stack frame by reassigning the goals variable to the body of the callee, and by keeping track of the substitutions contained in the dummy solution in a separate list. So, yes, LCO was only a matter of reassigning some variables and issuing a goto... And fortunately, it didn't require a messy rewrite.
The current solver architecture doesn't provide the flexibility of a virtual machine. In particular, it makes it complicated to reason about choice points and stack frames, obstructing several optimization paths.
A blocking issue is that, with the current architecture, I can't find a way to implement last call optimization. The Solve() method is implemented as a pair of mutually recursive
IAsyncEnumerables: one acting on queries and one acting on terms. It's reasonable to assume that the first method could be refactored away, leaving only the iteration constructs. At that point LCO is only a matter of reassigning some variables and issuing agoto.There are more elegant solutions. The next logical step would be refactoring the mess of loops into a state machine. This is where we can introduce concepts such as the stack and the trail in a way that mirrors the WAM without mirroring its internals. After all, the WAM works on compiled Prolog while Ergo is still completely interpreted. This step should however lay the groundwork for what will eventually become the Ergo Abstract Machine, so it is very important.