Allow limiting search time using fuel

[flodiebold]

To use Chalk in an IDE environment (i.e. rust-analyzer), we need to be able to prevent it from taking
too much time, even if that means getting a wrong or incomplete answer.
This is an attempt to do so by specifying an amount of 'fuel'; each iteration of the top-level
search loop takes one unit of fuel, and when it runs out, we return.

I'm not sure what answer to return if fuel runs out, or if there's some other big problem with this approach; I've tested it with rust-analyzer though, and it fixes (or rather limits) the slow cases I've run into. Also, maybe you have a better suggestion for the name ;)

[shepmaster]

maybe you have a better suggestion for the name

Etherium uses the term "gas" for a similar concept, so "fuel" doesn't seem outrageous.

[matklad]

Fuel could be encapsulated:

enum Fuel {
    Unlimited,
    Limited(usize)
}

impl Fuel {
    fn try_spend(&mut self) -> Result<(), ()> { ... }
}

[nikomatsakis]

I think if we're going to have fuel, then the return type of this function needs to change to something like Result<Option<..>, OutOfFuel>, so we can return Err(OutOfFuel) here. Returning None will (incorrectly) cause the system to conclude that there are no more possible answers, which will (I believe..) affect caching and future answers. That's not really what we want.

That said, I'm not yet 100% sold on the concept of fuel -- we may want it eventually, but I think I'd prefer to push on addressing the slowdown issues in other ways to start.

Although I suppose that, in the end, the system is turing complete, and it's possible for users to put us in a computationally expensive position no matter what. The current system guarantees termination but only by bounding the maximum size of types we can create and other such tricks, which means that recursion may wind up taking quite a bit of time and wasting quite a bit of resources before ultimately terminating.

Actually, I think that I'd prefer not to add a fuel parameter here in any case, but instead to make this function return a Result and then propagate back the QuantumExceeded failures (instead of looping). Then we can move the loop further out, which seems fine. (The more we can push fuel out from the "inner loop", I think, the better.)

[matklad]

Then we can move the loop further out, which seems fine. (The more we can push fuel out from the "inner loop", I think, the better.)

A related thing we've discussed is that we might want to enable cancellation of chalk queries. That might also benefit from pushing logic for "stop/continue" to the outer loop.

[flodiebold]

I'll get back to this after I'm done with rust-lang/rust-analyzer#1408. I also think moving the outer loop further out might be a good idea because it'll allow us to add cancellation checks as well.

[flodiebold]

I've tried a bit to find a good way to push the outer loop to rust-analyzer, but haven't had success so far. The problem is that constructing an answer requires searching until we've found one, and then continuing until it's clear whether there's a second answer, so something needs to keep that state...

[flodiebold]

This is clearly superseded by #321 now 😄