ghc-typelits-natnormalise 0.1.2 → 0.2
raw patch · 4 files changed
+62/−11 lines, 4 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- CHANGELOG.md +6/−1
- ghc-typelits-natnormalise.cabal +1/−1
- src/GHC/TypeLits/Normalise.hs +37/−7
- src/GHC/TypeLits/Normalise/Unify.hs +18/−2
CHANGELOG.md view
@@ -1,7 +1,12 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.2 *April 22nd 2015*+* Finds more unifications:+ * `(2 + a) ~ 5 ==> [a := 3]`+ * `(3 * a) ~ 0 ==> [a := 0]`+ ## 0.1.2 *April 21st 2015*-* Don't simply expressions with negative exponents+* Don't simplify expressions with negative exponents ## 0.1.1 *April 17th 2015* * Add workaround for https://ghc.haskell.org/trac/ghc/ticket/10301
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.1.2+version: 0.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.hs view
@@ -1,5 +1,6 @@-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TupleSections #-} {-# OPTIONS_HADDOCK show-extensions #-} @@ -52,7 +53,7 @@ -- GHC API import Coercion (Role (Nominal), mkUnivCo) import FastString (fsLit)-import Outputable (Outputable (..), (<+>), ($$), text)+import Outputable (Outputable (..), (<+>), ($$), empty, text) import Plugins (Plugin (..), defaultPlugin) import TcEvidence (EvTerm (EvCoercion), TcCoercion (..)) import TcPluginM (TcPluginM, tcPluginTrace, unsafeTcPluginTcM, zonkCt)@@ -90,7 +91,7 @@ plugin = defaultPlugin { tcPlugin = const $ Just normalisePlugin } normalisePlugin :: TcPlugin-normalisePlugin =+normalisePlugin = tracePlugin "ghc-typelits-natnormalise" TcPlugin { tcPluginInit = return () , tcPluginSolve = decideEqualSOP , tcPluginStop = const (return ())@@ -99,9 +100,9 @@ decideEqualSOP :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult decideEqualSOP _ _givens _deriveds [] = return (TcPluginOk [] []) decideEqualSOP _ givens _deriveds wanteds = do- -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301- initializeStaticFlags- let unit_wanteds = mapMaybe toNatEquality wanteds+ -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out+ let wanteds' = filter (isWanted . ctEvidence) wanteds+ let unit_wanteds = mapMaybe toNatEquality wanteds' case unit_wanteds of [] -> return (TcPluginOk [] []) _ -> do@@ -189,6 +190,35 @@ evByFiat :: String -> (Type, Type) -> EvTerm evByFiat name (t1,t2) = EvCoercion $ TcCoercion $ mkUnivCo (fsLit name) Nominal t1 t2++tracePlugin :: String -> TcPlugin -> TcPlugin+tracePlugin s TcPlugin{..} = TcPlugin { tcPluginInit = traceInit+ , tcPluginSolve = traceSolve+ , tcPluginStop = traceStop+ }+ where+ traceInit = do -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301+ initializeStaticFlags+ tcPluginTrace ("tcPluginInit " ++ s) empty >> tcPluginInit+ traceStop z = do -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301+ initializeStaticFlags+ tcPluginTrace ("tcPluginStop " ++ s) empty >> tcPluginStop z++ traceSolve z given derived wanted = do+ -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301+ initializeStaticFlags+ tcPluginTrace ("tcPluginSolve start " ++ s)+ (text "given =" <+> ppr given+ $$ text "derived =" <+> ppr derived+ $$ text "wanted =" <+> ppr wanted)+ r <- tcPluginSolve z given derived wanted+ case r of+ TcPluginOk solved new -> tcPluginTrace ("tcPluginSolve ok " ++ s)+ (text "solved =" <+> ppr solved+ $$ text "new =" <+> ppr new)+ TcPluginContradiction bad -> tcPluginTrace ("tcPluginSolve contradiction " ++ s)+ (text "bad =" <+> ppr bad)+ return r -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301 initializeStaticFlags :: TcPluginM ()
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -174,6 +174,8 @@ -- a + b ~ t ==> [t := a + b] -- (a + c) ~ (b + c) ==> \[a := b\] -- (2*a) ~ (2*b) ==> [a := b]+-- (2 + a) ~ 5 ==> [a := 3]+-- (3 * a) ~ 0 ==> [a := 0] -- @ -- -- However, given a wanted:@@ -182,7 +184,7 @@ -- [W] t ~ a + b -- @ ----- this function returns @[]@, or otherwise we \"solve\" the contstraint by+-- this function returns @[]@, or otherwise we \"solve\" the constraint by -- finding a unifier equal to the constraint. -- -- However, given a wanted:@@ -208,11 +210,25 @@ unifiers' :: Ct -> CoreSOP -> CoreSOP -> CoreSubst unifiers' ct (S [P [V x]]) (S []) = [SubstItem x (S [P [I 0]]) ct] unifiers' ct (S []) (S [P [V x]]) = [SubstItem x (S [P [I 0]]) ct]+ unifiers' ct (S [P [V x]]) s = [SubstItem x s ct] unifiers' ct s (S [P [V x]]) = [SubstItem x s 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]])++-- (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])+ | p == p' = unifiers' ct (S [P ps1]) (S [P ps2]) | otherwise = []++-- (2 + a) ~ 5 ==> [a := 3]+unifiers' ct (S ((P [I i]):ps1)) (S ((P [I j]):ps2))+ | i < j = unifiers' ct (S ps1) (S ((P [I (j-i)]):ps2))+ | i > j = unifiers' ct (S ((P [I (i-j)]):ps1)) (S ps2)++-- (a + c) ~ (b + c) ==> [a := b] unifiers' ct (S ps1) (S ps2) | null psx = [] | otherwise = unifiers' ct (S (ps1 \\ psx)) (S (ps2 \\ psx))