ghc-typelits-natnormalise 0.4.3 → 0.4.4

raw patch · 3 files changed

+30/−16 lines, 3 filesdep +integer-gmp

Dependencies added: integer-gmp

Files

• CHANGELOG.md +4/−0
• ghc-typelits-natnormalise.cabal +3/−2
• src/GHC/TypeLits/Normalise/Unify.hs +23/−14

@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.4.4 *July 19th 2016*+* Fixes bugs:+  * Rounding error in `logBase` calculation+ ## 0.4.3 *July 18th 2016* * Fixes bugs:   * False positive: "f :: (CLog 2 (2 ^ n) ~ n, (1 <=? n) ~ True) => Proxy n -> Proxy (n+d)"

@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.4.3+version:             0.4.4 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:   A type checker plugin for GHC that can solve /equalities/ of types of kind@@ -65,7 +65,8 @@   Other-Modules:       GHC.Extra.Instances   build-depends:       base >=4.8  && <5,                        ghc  >=7.10 && <8.2,-                       ghc-tcplugins-extra >= 0.2+                       ghc-tcplugins-extra >= 0.2,+                       integer-gmp >= 1.0 && < 1.1   hs-source-dirs:      src   default-language:    Haskell2010   other-extensions:    CPP

@@ -5,6 +5,7 @@ -}  {-# LANGUAGE CPP             #-}+{-# LANGUAGE MagicHash       #-} {-# LANGUAGE RecordWildCards #-}  {-# OPTIONS_GHC -fno-warn-unused-imports #-}@@ -33,6 +34,10 @@ import Data.Function (on) import Data.List     ((\\), intersect, mapAccumL) +import GHC.Base               (isTrue#,(==#))+import GHC.Integer            (smallInteger)+import GHC.Integer.Logarithms (integerLogBase#)+ -- GHC API import Outputable    (Outputable (..), (<+>), ($$), text) import TcPluginM     (TcPluginM, tcPluginTrace)@@ -280,22 +285,14 @@ -- (i ^ a) ~ j ==> [a := round (logBase i j)], when `i` and `j` are integers, -- and `ceiling (logBase i j) == floor (logBase i j)` unifiers' ct (S [P [E (S [P [I i]]) p]]) (S [P [I j]])-    = if kC == kF-         then unifiers' ct (S [p]) (S [P [I kC]])-         else []-  where-    k  = logBase (fromInteger i :: Double) (fromInteger j)-    kC = ceiling k :: Integer-    kF = floor k :: Integer+  = case integerLogBase i j of+      Just k  -> unifiers' ct (S [p]) (S [P [I k]])+      Nothing -> []  unifiers' ct (S [P [I j]]) (S [P [E (S [P [I i]]) p]])-    = if kC == kF-         then unifiers' ct (S [p]) (S [P [I kC]])-         else []-  where-    k  = logBase (fromInteger i :: Double) (fromInteger j)-    kC = ceiling k :: Integer-    kF = floor k :: Integer+  = case integerLogBase i j of+      Just k  -> unifiers' ct (S [p]) (S [P [I k]])+      Nothing -> []  -- a^d * a^e ~ a^c ==> [c := d + e] unifiers' ct (S [P [E s1 p1]]) (S [p2]) = case collectBases p2 of@@ -392,3 +389,15 @@   | otherwise = case divMod i j of                   (k,0) -> Just k                   _     -> Nothing++-- | Given `x` and `y`, return `Just n` when+--+-- `ceiling (logBase x y) == floor (logBase x y)`+integerLogBase :: Integer -> Integer -> Maybe Integer+integerLogBase x y | x > 1 && y > 0 =+  let z1 = integerLogBase# x y+      z2 = integerLogBase# x (y-1)+  in  if isTrue# (z1 ==# z2)+         then Nothing+         else Just (smallInteger z1)+integerLogBase _ _ = Nothing