Open martijnbastiaan opened 2 years ago
A workaround would be to define:
import Data.Type.Equality ((:~:)(Refl))
import Unsafe.Coerce (unsafeCoerce)
clog2axiom :: (CLog 2 (n * 2)) :~: ((CLog 2 n) + 1)
clog2axiom = unsafeCoerce Refl
And use it like:
coerceIndices :: forall n. (KnownNat n, 1 <= n) => Index (n*2) -> (Index n, Bool)
coerceIndices = case clog2axiom @n of Refl -> bitCoerce
@rowanG077 mentioned that we should be able to add this derivation by patching:
Finally, some "proof" that this equation holds:
>>> import Clash.Util (clogBase)
>>> import Test.QuickCheck (quickCheck, withMaxSuccess)
>>> clog2 = clogBase 2
>>> prop_eq n = (clog2 (n*2)) == (succ <$> clog2 n)
>>> quickCheck (withMaxSuccess 1000000 prop_eq)
+++ OK, passed 1000000 tests.
This should hold for all
n
*, but the plugin doesn't infer it.*For n ~ 0 the answer is undefined in both cases