ghc-typelits-natnormalise 0.5.4 → 0.5.5

raw patch · 5 files changed

+56/−12 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +6/−0
• ghc-typelits-natnormalise.cabal +1/−1
• src/GHC/TypeLits/Normalise.hs +20/−6
• src/GHC/TypeLits/Normalise/Unify.hs +5/−2
• tests/Tests.hs +24/−3

@@ -1,5 +1,11 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.5.5 *October 22nd 2017*+* Solve inequalities when their normal forms are the same, i.e.+  * `(2 <= (2 ^ (n + d)))` implies `(2 <= (2 ^ (d + n)))`+* Find more unifications:+  * `8^x - 2*4^x ~ 8^y - 2*4^y ==> [x := y]`+ ## 0.5.4 *October 14th 2017* * Perform normalisations such as: `2^x * 4^x ==> 8^x` 

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

@@ -52,6 +52,7 @@ -- external import Control.Arrow       (second) import Control.Monad       (replicateM)+import Data.Either         (rights) import Data.List           (intersect) import Data.Maybe          (mapMaybe) import GHC.TcPluginM.Extra (tracePlugin)@@ -116,7 +117,7 @@       [] -> return (TcPluginOk [] [])       _  -> do         unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens-        sr <- simplifyNats (unit_givens ++ unit_wanteds)+        sr <- simplifyNats unit_givens unit_wanteds         tcPluginTrace "normalised" (ppr sr)         case sr of           Simplified evs -> do@@ -140,10 +141,15 @@   ppr (Simplified evs) = text "Simplified" $$ ppr evs   ppr (Impossible eq)  = text "Impossible" <+> ppr eq -simplifyNats :: [Either NatEquality NatInEquality]-             -> TcPluginM SimplifyResult-simplifyNats eqs =-    tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs+simplifyNats+  :: [Either NatEquality NatInEquality]+  -- ^ Given constraints+  -> [Either NatEquality NatInEquality]+  -- ^ Wanted constraints+  -> TcPluginM SimplifyResult+simplifyNats eqsG eqsW =+    let eqs = eqsG ++ eqsW+    in  tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs   where     simples :: [CoreUnify]             -> [((EvTerm, Ct), [Ct])]@@ -175,7 +181,15 @@           evs' <- maybe evs (:evs) <$> evMagic ct []           simples subst evs' xs eqs'         Just False -> return (Impossible eq)-        Nothing    -> simples subst evs (eq:xs) eqs'+        Nothing    ->+          -- This inequality is either a given constraint, or it is a wanted+          -- constraint, which in normal form is equal to another given+          -- constraint, hence it can be solved.+          if u `elem` (map snd (rights eqsG))+             then do+               evs' <- maybe evs (:evs) <$> evMagic ct []+               simples subst evs' xs eqs'+             else simples subst evs (eq:xs) eqs'  -- Extract the Nat equality constraints toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality)

@@ -38,7 +38,7 @@  -- External import Data.Function (on)-import Data.List     ((\\), intersect, mapAccumL)+import Data.List     ((\\), intersect, mapAccumL, nub)  import GHC.Base               (isTrue#,(==#)) import GHC.Integer            (smallInteger)@@ -175,6 +175,7 @@                    | UnifyItem { siLHS  :: SOP v c                                , siRHS  :: SOP v c                                }+  deriving Eq  instance (Outputable v, Outputable c) => Outputable (UnifyItem v c) where   ppr (SubstItem {..}) = ppr siVar <+> text " := " <+> ppr siSOP@@ -388,7 +389,9 @@  -- (a + c) ~ (b + c) ==> [a := b] unifiers' ct (S ps1)       (S ps2)-    | null psx  = unifiers'' ct (S ps1) (S ps2)+    | null psx  = case zipWith (\x y -> unifiers' ct (S [x]) (S [y])) ps1 ps2 of+                    [] -> unifiers'' ct (S ps1) (S ps2)+                    ks -> nub (concat ks)     | otherwise = unifiers' ct (S ps1'') (S ps2'')   where     ps1'  = ps1 \\ psx

@@ -248,9 +248,24 @@ proxyInEq5 :: Proxy 1 -> Proxy (2^a) -> () proxyInEq5 = proxyInEq -proxyEq1 :: Proxy x -> Proxy ((2 ^ x) * (2 ^ (x + x))) -> Proxy (2 * (2 ^ ((x + (x + x)) - 1)))-proxyEq1 _ = id+proxyEq1 :: Proxy ((2 ^ x) * (2 ^ (x + x))) -> Proxy (2 * (2 ^ ((x + (x + x)) - 1)))+proxyEq1 = id +proxyEq2 :: Proxy (((2 ^ x) - 2) * (2 ^ (x + x))) -> Proxy ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))+proxyEq2 = id++proxyInEqImplication :: (2 <= (2 ^ (n + d)))+  => Proxy d+  -> Proxy n+  -> Proxy n+proxyInEqImplication = proxyInEqImplication'++proxyInEqImplication' :: (2 <= (2 ^ (d + n)))+  => Proxy d+  -> Proxy n+  -> Proxy n+proxyInEqImplication' _ = id+ main :: IO () main = defaultMain tests @@ -290,8 +305,11 @@     ]   , testGroup "Equality"     [ testCase "((2 ^ x) * (2 ^ (x + x))) ~ (2 * (2 ^ ((x + (x + x)) - 1)))" $-      show (proxyEq1 (Proxy :: Proxy 4) Proxy) @?=+      show (proxyEq1 Proxy) @?=       "Proxy"+    , testCase "(((2 ^ x) - 2) * (2 ^ (x + x))) ~ ((2 ^ ((x + (x + x)) - 1)) + ((2 ^ ((x + (x + x)) - 1)) - (2 ^ ((x + x) + 1))))" $+      show (proxyEq2 Proxy) @?=+      "Proxy"     ]   , testGroup "Inequality"     [ testCase "a <= a+1" $@@ -309,6 +327,9 @@     , testCase "1 <= 2^a" $       show (proxyInEq5 (Proxy :: Proxy 1) (Proxy :: Proxy 1)) @?=       "()"+    , testCase "`(2 <= (2 ^ (n + d)))` implies `(2 <= (2 ^ (d + n)))`" $+      show (proxyInEqImplication (Proxy :: Proxy 3) (Proxy :: Proxy 4)) @?=+      "Proxy"     ]   , testGroup "errors"     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors