ghc-typelits-natnormalise 0.3 → 0.3.1

raw patch · 6 files changed

+71/−6 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• ghc-typelits-natnormalise.cabal +1/−1
• src/GHC/TypeLits/Normalise/SOP.hs +7/−1
• src/GHC/TypeLits/Normalise/Unify.hs +19/−4
• tests/ErrorTests.hs +30/−0
• tests/Tests.hs +9/−0

@@ -1,5 +1,10 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.3.1 *October 19th 2015*+* Find more unifications:+  * `(i * a) ~ j ==> [a := div j i]`, when `i` and `j` are integers, and `mod j i == 0`.+  * `(i * a) + j ~ k  ==> [a := div (k-j) i]`, when `i`, `j`, and `k` are integers, and `k-j >= 0` and `mod (k-j) i == 0`.+ ## 0.3 *June 3rd 2015* * Find more unifications:   * `<TyApp xs> + x ~ 2 + x ==> [<TyApp xs> ~ 2]`

@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.3+version:             0.3.1 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

@@ -102,7 +102,13 @@   deriving (Eq,Ord)  newtype Product v c = P { unP :: [Symbol v c] }-  deriving (Eq,Ord)+  deriving (Eq)++instance (Ord v, Ord c) => Ord (Product v c) where+  compare (P [x])   (P [y])   = compare x y+  compare (P [_])   (P (_:_)) = LT+  compare (P (_:_)) (P [_])   = GT+  compare (P xs)    (P ys)    = compare xs ys  newtype SOP v c = S { unS :: [Product v c] }   deriving (Ord)

@@ -189,7 +189,7 @@ -- (a + c) ~ (b + c)  ==>  \[a := b\] -- (2*a) ~ (2*b)      ==>  [a := b] -- (2 + a) ~ 5        ==>  [a := 3]--- (3 * a) ~ 0        ==>  [a := 0]+-- (i * a) ~ j        ==>  [a := div j i], when (mod j i == 0) -- @ -- -- However, given a wanted:@@ -233,10 +233,18 @@ unifiers' ct s1@(S [P [C _]]) s2               = [UnifyItem s1 s2 ct] unifiers' ct s1               s2@(S [P [C _]]) = [UnifyItem s1 s2 ct] --- (3 * a) ~ 0 ==> [a := 0]-unifiers' ct (S [P ((I _):ps)]) (S [P [I 0]]) = unifiers' ct (S [P ps]) (S [P [I 0]])-unifiers' ct (S [P [I 0]]) (S [P ((I _):ps)]) = unifiers' ct (S [P ps]) (S [P [I 0]])+-- (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]]) =+  case safeDiv j i of+    Just k  -> unifiers' ct (S [P ps]) (S [P [I k]])+    _       -> [] +unifiers' ct (S [P [I j]]) (S [P ((I i):ps)]) =+  case safeDiv j i of+    Just k  -> unifiers' ct (S [P ps]) (S [P [I k]])+    _       -> []+ -- (2*a) ~ (2*b) ==> [a := b] -- unifiers' ct (S [P (p:ps1)]) (S [P (p':ps2)]) --     | p == p'   = unifiers' ct (S [P ps1]) (S [P ps2])@@ -289,3 +297,10 @@  containsConstants :: CoreSOP -> Bool containsConstants = any (any (\c -> case c of {(C _) -> True; _ -> False}) . unP) . unS++safeDiv :: Integer -> Integer -> Maybe Integer+safeDiv i j+  | j == 0    = Just 0+  | otherwise = case divMod i j of+                  (k,0) -> Just k+                  _     -> Nothing

@@ -26,3 +26,33 @@   ["Expected type: Proxy (GCD 6 8 + x) -> Proxy (x + GCD 9 6)"   ,"Actual type: Proxy (x + 3) -> Proxy (x + 3)"   ]++proxyFun3 :: Proxy (x + x + x) -> ()+proxyFun3 = const ()++testProxy3 :: Proxy 8 -> ()+testProxy3 = proxyFun3++testProxy3Errors =+  ["Expected type: Proxy 8 -> ()"+  ,"Actual type: Proxy ((x0 + x0) + x0) -> ()"+  ]++proxyFun4 :: Proxy ((2*y)+4) -> ()+proxyFun4 = const ()++testProxy4 :: Proxy 2 -> ()+testProxy4 = proxyFun4++testProxy4Errors =+  ["Expected type: Proxy 2 -> ()"+  ,"Actual type: Proxy ((2 * y0) + 4) -> ()"+  ]++testProxy5 :: Proxy 7 -> ()+testProxy5 = proxyFun4++testProxy5Errors =+  ["Expected type: Proxy 7 -> ()"+  ,"Actual type: Proxy ((2 * y1) + 4) -> ()"+  ]

@@ -260,10 +260,19 @@     , testCase "show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil))" $       show (unconcat (snat :: SNat 4) (1:>2:>3:>4:>5:>6:>7:>8:>9:>10:>11:>12:>Nil)) @?=       "<<1,2,3,4>,<5,6,7,8>,<9,10,11,12>>"+    , testCase "show (proxyFun3 (Proxy :: Proxy 9))" $+      show (proxyFun3 (Proxy :: Proxy 9)) @?=+      "()"+    , testCase "show (proxyFun4 (Proxy :: Proxy 8))" $+      show (proxyFun4 (Proxy :: Proxy 8)) @?=+      "()"     ]   , testGroup "errors"     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors     , testCase "GCD 6 8 + x ~ x + GCD 9 6" $ testProxy2 `throws` testProxy2Errors+    , testCase "Unify \"x + x + x\" with \"8\"" $ testProxy3 `throws` testProxy3Errors+    , testCase "Unify \"(2*x)+4\" with \"2\"" $ testProxy4 `throws` testProxy4Errors+    , testCase "Unify \"(2*x)+4\" with \"7\"" $ testProxy5 `throws` testProxy5Errors     ]   ]