search

clash-lang / ghc-typelits-extra

Extra type-level operations on GHC.TypeLits.Nat and a custom solver
Other
16 stars 9 forks source link

Distribute add, mul, and sub through Max and Min #36

Closed isovector closed 2 years ago

isovector commented 3 years ago

This PR rewrites terms of the form Max a b + n into Max (a + n) (b + n), also for Min, and for * and - as well. It has commutative rules for plus and mul as well.

Fixes #35

isovector commented 3 years ago

PS: kudos for how tidy the ghc-typelits-extras codebase is. This PR was a delight to put together, with none of the usual frustrations about open-source. Cheers!

martijnbastiaan commented 3 years ago

Could you add a few non-happy-path regression tests? E.g., Max (a + n) (b + m) /= Max a b + n.

Could you also check that this rule:

Max a b - n = Max (a - n) (b - n)

doesn't fire for a ~ 3, b ~ 5, and n ~ 4? That is, a - n ~ 3 - 4 which should get stuck even though Max a b - n ~ Max 3 5 - 4 ~ 5 - 4 ~ 1.

christiaanb commented 3 years ago

Also, don't forget to add the add and mul TyCons for the GHC 9+ branch: https://github.com/clash-lang/ghc-typelits-extra/pull/36/files#diff-0f6ec8cf702821024f5ca0df93a413d1bac56bd51bb87772bba6611ae6b4b960L44

christiaanb commented 3 years ago

@martijnbastiaan that "unhappy" path doesn't have to be checked. The plugin can already observe Max (3-4) (5-4) ~ 1.

@isovector I've added an additional commit so that the solver from ghc-typelits-natnormalise is called recursively.

martijnbastiaan commented 3 years ago

@martijnbastiaan that "unhappy" path doesn't have to be checked. The plugin can already observe Max (3-4) (5-4) ~ 1.

Hmm, is that what we want though? Shouldn't Max n m get stuck when either n or m is stuck?

christiaanb commented 3 years ago

@martijnbastiaan that "unhappy" path doesn't have to be checked. The plugin can already observe Max (3-4) (5-4) ~ 1.

Hmm, is that what we want though? Shouldn't Max n m get stuck when either n or m is stuck?

I think it’s more important that the result is definitely a natural number, which is something we do check.

If we do decide it needs fixing, it should go in a different PR