Scheduler: Allow configuring max number of iterations of rewrites

[alt-romes]

As mentioned in #42, in runEqualitySaturation, we seemingly stop after 30 iterations.

This both seems ad-hoc and would be useful if it were configurable, so users could iteratively experiment running a few iterations of rewrites and observing it afterwards without reaching saturation.

I was thinking we could implement this by adding a method "maxRewriteIterations" to the Scheduler class. We try reaching saturation up to maxRewriteIterations and there we simply exit.

Then, we could have some datatype + instance like

newtype WithMaxIterations (n :: Nat) a = WithMaxIterations a

instance (KnownNat a, Scheduler a) => Scheduler n a where
    maxIterations (WithMaxIterations @n) = natVal (Proxy @n)
    -- for other methods delegate to `Scheduler a`

From a user perspective, to run N iterations of equality saturation you'd now have:

- runEqualitySaturation defaultBackoffScheduler <rewrites>
+ runEqualitySaturation (WithMaxIterations @5 defaultBackoffScheduler) <rewrites>

[ren-zeng]

Hi @alt-romes, thanks for opening a thread for this feature. I'm thinking out loud in terms of the extensibility of API.

Wouldn't it be nice if the scheduler, which I think conceptually manages the "priorities" of rewritings, is decoupled (thus freely composed) with an abstract "early termination condition" (which could be timeout, max iteration, size of the graph, etc)?

Let's say if a user wants to use the a scheduler sche but wants to use an early termination condition, the user might want an interface like

runEqSatEarlyTerm :: (..) => earlyTermCond -> sche -> [Rewrite a l] -> EGraphM a l () 

This way the user can freely match any combination of earlyTermCond and sche without needing to create a new data type and instance for scheduler.

One challenging scenario to consider is that the user might want to log some statistics every let's say 5 iterations, and they want the same scheduler to retain its internal states between each "run 5" operation. Maybe using runEqSatEarlyTerm inside a state monad

StateT (Stat sche) (EGraphM a l)

I haven't thought of a clear future-proof extensible API for this kind of need, but here is the summary of the design challenge:

1. the user might want to freely match early termination condition with rule prioritization
2. the user might want to early terminate while retaining the scheduler's state