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

Improved Log inference #40

Open rowanG077 opened 2 years ago

rowanG077 commented 2 years ago

Normalise Log base (a * b * ... * z) to Log base a + Log base b + ... + Log base z Normalise Log b (x^y) to y * Log b x

rowanG077 commented 2 years ago

While working on it I'm not actually sure this is legal for naturals in the way the solvers function.

For example Log 10 (50 * 2) prior to this PR will reduce to Log 10 100 -> 2. But depending on the way the plugins fire after this PR it might reduce like this: Log 10 (50 * 2) -> Log 10 50 + Log 10 2 and now it will report this as unsolvable as both the logs will not cleanly reduce to a Natural.

I feel like similar issues exist for the other rule but I don't have an example handy.

I guess doing the rewrites the other way should be fine.

rowanG077 commented 2 years ago

Ready for review

I choose not to normalise x * log b a to log b a^x because I feel like dealing with exponents sucks. And the rewrite the other way around is unsound.

note that I used the withSOPNormalize from this closed PR: https://github.com/clash-lang/ghc-typelits-extra/pull/36

alex-mckenna commented 2 years ago

because I feel like dealing with exponents sucks

I can already see @christiaanb reading this and going "yep" :eyes: