ghc-typelits-natnormalise 0.4.1 → 0.4.2
raw patch · 4 files changed
+66/−10 lines, 4 files
Files
- CHANGELOG.md +6/−0
- ghc-typelits-natnormalise.cabal +1/−1
- src/GHC/TypeLits/Normalise/SOP.hs +18/−6
- src/GHC/TypeLits/Normalise/Unify.hs +41/−3
CHANGELOG.md view
@@ -1,5 +1,11 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.4.2 *July 8th 2016*+* Find more unifications:+ * `(2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]`+ * `a^d * a^e ~ a^c ==> [c := d + e]`+ * `x+5 ~ y ==> [x := y - 5]`, but only when `x+5 ~ y` is a given constraint+ ## 0.4.1 *February 4th 2016* * Find more unifications: * `F x y k z ~ F x y (k-1+1) z` ==> [k := k], where `F` can be any type function
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.4.1+version: 0.4.2 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
src/GHC/TypeLits/Normalise/SOP.hs view
@@ -272,18 +272,30 @@ zeroP (P ((I 0):_)) = True zeroP _ = False +mkNonEmpty :: SOP v c -> SOP v c+mkNonEmpty (S []) = S [P [(I 0)]]+mkNonEmpty s = s+ -- | Simplifies SOP terms using -- -- * 'mergeS' -- * 'mergeP' -- * 'reduceExp' simplifySOP :: (Ord v, Ord c) => SOP v c -> SOP v c-simplifySOP- = S- . sort . filter (not . zeroP)- . mergeWith mergeP- . map (P . sort . map reduceExp . mergeWith mergeS . unP)- . unS+simplifySOP = repeatF go+ where+ go = mkNonEmpty+ . S+ . sort . filter (not . zeroP)+ . mergeWith mergeP+ . map (P . sort . map reduceExp . mergeWith mergeS . unP)+ . unS++ repeatF f x =+ let x' = f x+ in if x' == x+ then x+ else repeatF f x' {-# INLINEABLE simplifySOP #-} -- | Merge two SOP terms by additions
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -6,6 +6,7 @@ {-# LANGUAGE CPP #-} {-# LANGUAGE RecordWildCards #-}+ {-# OPTIONS_GHC -fno-warn-unused-imports #-} module GHC.TypeLits.Normalise.Unify@@ -30,7 +31,7 @@ -- External import Data.Function (on)-import Data.List ((\\), intersect)+import Data.List ((\\), intersect, mapAccumL) -- GHC API import Outputable (Outputable (..), (<+>), ($$), text)@@ -85,7 +86,7 @@ reifySOP = combineP . map negateP . unS where negateP :: CoreProduct -> Either CoreProduct CoreProduct- negateP (P ((I i):ps)) | i < 0 = Left (P ps)+ negateP (P ((I i):ps)) | i < 0 = Left (P ((I (abs i)):ps)) negateP ps = Right ps combineP :: [Either CoreProduct CoreProduct] -> Type@@ -263,6 +264,19 @@ unifiers' ct (S [P [E s1 p1]]) (S [P [E s2 p2]]) | s1 == s2 = unifiers' ct (S [p1]) (S [p2]) +-- (2*e ^ d) ~ (2*e*a*c) ==> [a*c := 2*e ^ (d-1)]+unifiers' ct (S [P [E (S [P s1]) p1]]) (S [P p2])+ | all (`elem` p2) s1+ = let base = intersect s1 p2+ diff = p2 \\ s1+ in unifiers ct (S [P diff]) (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]])++unifiers' ct (S [P p2]) (S [P [E (S [P s1]) p1]])+ | all (`elem` p2) s1+ = let base = intersect s1 p2+ diff = p2 \\ s1+ in unifiers ct (S [P [E (S [P base]) (P [I (-1)]),E (S [P base]) p1]]) (S [P diff])+ -- (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]])@@ -283,6 +297,17 @@ kC = ceiling k :: Integer kF = floor k :: Integer +-- a^d * a^e ~ a^c ==> [c := d + e]+unifiers' ct (S [P [E s1 p1]]) (S [p2]) = case collectBases p2 of+ Just (b:bs,ps) | all (== s1) (b:bs) ->+ unifiers' ct (S [p1]) (S ps)+ _ -> []++unifiers' ct (S [p2]) (S [P [E s1 p1]]) = case collectBases p2 of+ Just (b:bs,ps) | all (== s1) (b:bs) ->+ unifiers' ct (S ps) (S [p1])+ _ -> []+ -- (i * a) ~ j ==> [a := div j i] -- Where 'a' is a variable, 'i' and 'j' are integer literals, and j `mod` i == 0 unifiers' ct (S [P ((I i):ps)]) (S [P [I j]]) =@@ -318,7 +343,7 @@ -- (a + c) ~ (b + c) ==> [a := b] unifiers' ct (S ps1) (S ps2)- | null psx = []+ | null psx = unifiers'' ct (S ps1) (S ps2) | otherwise = unifiers' ct (S ps1'') (S ps2'') where ps1' = ps1 \\ psx@@ -328,6 +353,19 @@ ps2'' | null ps2' = [P [I 0]] | otherwise = ps2' psx = intersect ps1 ps2++unifiers'' :: Ct -> CoreSOP -> CoreSOP -> CoreUnify Ct+unifiers'' ct (S [P [I i],P [V v]]) s2+ | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s2 (S [P [I (negate i)]])) ct]+unifiers'' ct s1 (S [P [I i],P [V v]])+ | isGiven (ctEvidence ct) = [SubstItem v (mergeSOPAdd s1 (S [P [I (negate i)]])) ct]+unifiers'' _ _ _ = []++collectBases :: CoreProduct -> Maybe ([CoreSOP],[CoreProduct])+collectBases = fmap unzip . traverse go . unP+ where+ go (E s1 p1) = Just (s1,p1)+ go _ = Nothing -- | Find the 'TyVar' in a 'CoreSOP' fvSOP :: CoreSOP -> UniqSet TyVar