packages feed

ghc-typelits-natnormalise 0.4.5 → 0.4.6

raw patch · 4 files changed

+63/−28 lines, 4 files

Files

CHANGELOG.md view
@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.4.6 *July 21th 2016*+* Reduce "x^(-y) * x^y" to 1+* Fixes bugs:+  * Subtraction in exponent induces infinite loop+ ## 0.4.5 *July 20th 2016* * Fixes bugs:   * Reifying negative exponent causes GHC panic
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.4.5+version:             0.4.6 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
@@ -205,6 +205,20 @@       (S [P [e]]) -> Left  e       _           -> Right l +-- x^y * x^(-y) ==> 1+mergeS (E s1 (P p1)) (E s2 (P (I i:p2)))+  | i == (-1)+  , s1 == s2+  , p1 == p2+  = Left (I 1)++-- x^(-y) * x^y ==> 1+mergeS (E s1 (P (I i:p1))) (E s2 (P p2))+  | i == (-1)+  , s1 == s2+  , p1 == p2+  = Left (I 1)+ mergeS l _ = Right l  -- | Merge two products of a SOP term@@ -259,7 +273,9 @@   foldr1 mergeSOPMul (replicate (fromInteger i) b)  -- (x + 2)^(2x) ==> (x^2 + 4xy + 4)^x-normaliseExp b (S [P (e@(I _):es)]) =+normaliseExp b (S [P (e@(I i):es)]) | i >= 0 =+  -- Without the "| i >= 0" guard, normaliseExp can loop with itself+  -- for exponentials such as: 2^(n-k)   normaliseExp (normaliseExp b (S [P [e]])) (S [P es])  -- (x + 2)^(xy) ==> (x+2)^(xy)
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -91,21 +91,40 @@ reifySOP = combineP . map negateP . unS   where     negateP :: CoreProduct -> Either CoreProduct CoreProduct-    negateP (P ((I i):ps)) | i < 0 = Left  (P ((I (abs i)):ps))-    negateP ps                     = Right ps+    negateP (P ((I i):ps@(_:_))) | i == (-1) = 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     combineP []     = mkNumLitTy 0     combineP [p]    = either (\p' -> mkTyConApp typeNatSubTyCon                                                 [mkNumLitTy 0, reifyProduct p'])                              reifyProduct p-    combineP (p:ps) = let es = combineP ps-                      in  either (\x -> mkTyConApp typeNatSubTyCon-                                                   [es, reifyProduct x])-                                 (\x -> mkTyConApp typeNatAddTyCon-                                                  [reifyProduct x, es])-                                 p+    combineP [p1,p2] = either+      (\x -> either+               -- x neg, y neg+               (\y -> let r = mkTyConApp typeNatSubTyCon [reifyProduct x+                                                         ,reifyProduct y]+                      in  mkTyConApp typeNatSubTyCon [mkNumLitTy 0, r])+               -- x neg, y pos+               (\y -> mkTyConApp typeNatSubTyCon [reifyProduct y, reifyProduct x])+               p2)+      (\x -> either+               -- x pos, y neg+               (\y -> mkTyConApp typeNatSubTyCon [reifyProduct x, reifyProduct y])+               -- x pos, y pos+               (\y -> mkTyConApp typeNatAddTyCon [reifyProduct x, reifyProduct y])+               p2)+      p1 ++    combineP (p:ps)  = let es = combineP ps+                       in  either (\x -> mkTyConApp typeNatSubTyCon+                                                    [es, reifyProduct x])+                                  (\x -> mkTyConApp typeNatAddTyCon+                                                   [reifyProduct x, es])+                                  p+ reifyProduct :: CoreProduct -> Type reifyProduct (P ps) =     let ps' = map reifySymbol (foldr mergeExp [] ps)@@ -113,30 +132,25 @@   where     -- "2 ^ -1 * 2 ^ a" must be merged into "2 ^ (a-1)", otherwise GHC barfs     -- at the "2 ^ -1" because of the negative exponent.-    mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,CoreProduct,Integer)]-                           -> [Either CoreSymbol (CoreSOP,CoreProduct,Integer)]-    mergeExp (E s1 (P [I i])) (y:ys)-      | i < 0-      , Left (E s2 p2) <- y-      , s1 == s2-      = Right (s1,p2,negate i) : ys-      | i < 0-      , Right (s2,p2,j) <- y+    mergeExp :: CoreSymbol -> [Either CoreSymbol (CoreSOP,[CoreProduct])]+                           -> [Either CoreSymbol (CoreSOP,[CoreProduct])]+    mergeExp (E s p)   []     = [Right (s,[p])]+    mergeExp (E s1 p1) (y:ys)+      | Right (s2,p2) <- y       , s1 == s2-      = Right (s1,p2,j+negate i) : ys-    mergeExp x ys = Left x:ys+      = Right (s1,(p1:p2)) : ys+      | otherwise+      = Right (s1,[p1]) : ys+    mergeExp x ys = Left x : ys -reifySymbol :: Either CoreSymbol (CoreSOP,CoreProduct,Integer) -> Type+reifySymbol :: Either CoreSymbol (CoreSOP,[CoreProduct]) -> Type reifySymbol (Left (I i)  )  = mkNumLitTy i reifySymbol (Left (C c)  )  = c reifySymbol (Left (V v)  )  = mkTyVarTy v reifySymbol (Left (E s p))  = mkTyConApp typeNatExpTyCon [reifySOP s,reifyProduct p]-reifySymbol (Right (s,p,i)) = mkTyConApp typeNatExpTyCon-                                         [reifySOP s-                                         ,mkTyConApp typeNatSubTyCon-                                                     [reifyProduct p-                                                     ,mkNumLitTy i-                                                     ]+reifySymbol (Right (s1,s2)) = mkTyConApp typeNatExpTyCon+                                         [reifySOP s1+                                         ,reifySOP (S s2)                                          ]  -- | A substitution is essentially a list of (variable, 'SOP') pairs,