alt-romes / alt-romes/hegg

Scheduler: Allow configuring max number of iterations of rewrites

未关闭
#43 1 条评论 0 个 reaction 已指派 0 人 在 GitHub 查看
enhancement good first issue help wanted
主要语言
Haskell
星标
98
派生
17
PR 合并指标
30 天内没有已合并 PR

描述

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:

```diff
- runEqualitySaturation defaultBackoffScheduler
+ runEqualitySaturation (WithMaxIterations @5 defaultBackoffScheduler)
```

贡献指南

这个仓库没有索引到贡献指南

评估

这个 Issue 还没有评估数据。

把新 issue 发到你的邮箱

精选适合新手参与的 GitHub issue 摘要。