diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,20 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.2.3 *May 15th 2017* +* Support GHC 8.2 +* `Max`, `Min`, `GCD`, and `LCM` now have a commutativity property [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `GCD 0 x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `GCD 1 x` to `1` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `GCD x x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `LCM 0 x` to `0` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `LCM 1 x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `LCM x x` to `x` [#9](https://github.com/clash-lang/ghc-typelits-extra/issues/9) +* Reduce `Max (0-1) 0` to `0` [#10](https://github.com/clash-lang/ghc-typelits-extra/issues/10) +* Reduce `Min (0-1) 0` to `0 - 1` [#10](https://github.com/clash-lang/ghc-typelits-extra/issues/10) +* Fixes bugs: + * Solver turns LCM into GCD [#8](https://github.com/clash-lang/ghc-typelits-extra/issues/8) + * Solver turns Max into Min + # 0.2.2 *January 15th 2017* * Reduce `Min n (n+1)` to `n` * Reduce `Max n (n+1)` to `n+1` diff --git a/ghc-typelits-extra.cabal b/ghc-typelits-extra.cabal --- a/ghc-typelits-extra.cabal +++ b/ghc-typelits-extra.cabal @@ -1,5 +1,5 @@ name: ghc-typelits-extra -version: 0.2.2 +version: 0.2.3 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@: @@ -63,9 +63,10 @@ other-modules: GHC.TypeLits.Extra.Solver.Unify GHC.TypeLits.Extra.Solver.Operations build-depends: base >= 4.8 && <5, - ghc >= 7.10 && <8.2, + ghc >= 7.10 && <8.4, + ghc-prim >= 0.5 && <1.0, ghc-tcplugins-extra >= 0.2, - ghc-typelits-knownnat >= 0.2 && <0.3, + ghc-typelits-knownnat >= 0.2 && <0.4, ghc-typelits-natnormalise >= 0.5 && <0.6, integer-gmp >= 1.0 && <1.1, singletons >= 2.2 && <3, diff --git a/src/GHC/TypeLits/Extra.hs b/src/GHC/TypeLits/Extra.hs --- a/src/GHC/TypeLits/Extra.hs +++ b/src/GHC/TypeLits/Extra.hs @@ -37,6 +37,7 @@ pragma to the header of your file. -} +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} @@ -79,17 +80,31 @@ import Data.Proxy (Proxy (..)) import Data.Singletons.TH (genDefunSymbols) import Data.Type.Bool (If) -import GHC.Base (isTrue#,(==#),(+#)) -import GHC.Integer (smallInteger) +import GHC.Base (Int#,isTrue#,(==#),(+#)) import GHC.Integer.Logarithms (integerLogBase#) +#if MIN_VERSION_ghc(8,2,0) +import qualified GHC.TypeNats as N +import GHC.Natural +import GHC.Prim (int2Word#) import GHC.TypeLits +#else +import GHC.Integer (smallInteger) +import GHC.TypeLits as N +#endif (KnownNat, Nat, type (+), type (-), type (<=), type (<=?), natVal) import GHC.TypeLits.KnownNat (KnownNat2 (..), SNatKn (..), nameToSymbol) +#if MIN_VERSION_ghc(8,2,0) +intToNumber :: Int# -> Natural +intToNumber x = NatS# (int2Word# x) +#else +intToNumber :: Int# -> Integer +intToNumber x = smallInteger x +#endif +{-# INLINE intToNumber #-} + -- | Type-level 'max' type family Max (x :: Nat) (y :: Nat) :: Nat where - Max 0 y = y - Max x 0 = x Max n n = n Max x y = If (x <=? y) y x @@ -97,12 +112,10 @@ instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Max) x y where type KnownNatF2 $(nameToSymbol ''Max) = MaxSym0 - natSing2 = SNatKn (max (natVal (Proxy @x)) (natVal (Proxy @y))) + natSing2 = SNatKn (max (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) -- | Type-level 'min' type family Min (x :: Nat) (y :: Nat) :: Nat where - Min 0 y = 0 - Min x 0 = 0 Min n n = n Min x y = If (x <=? y) x y @@ -110,7 +123,7 @@ instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''Min) x y where type KnownNatF2 $(nameToSymbol ''Min) = MinSym0 - natSing2 = SNatKn (min (natVal (Proxy @x)) (natVal (Proxy @y))) + natSing2 = SNatKn (min (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) -- | Type-level 'div' -- @@ -126,7 +139,7 @@ instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where type KnownNatF2 $(nameToSymbol ''Div) = DivSym0 - natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y))) + natSing2 = SNatKn (quot (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) -- | Type-level 'mod' -- @@ -139,7 +152,7 @@ instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where type KnownNatF2 $(nameToSymbol ''Mod) = ModSym0 - natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y))) + natSing2 = SNatKn (rem (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) -- | Type-level `divMod` type DivMod n d = '(Div n d, Mod n d) @@ -156,7 +169,11 @@ instance (KnownNat x, KnownNat y, 2 <= x, 1 <= y) => KnownNat2 $(nameToSymbol ''FLog) x y where type KnownNatF2 $(nameToSymbol ''FLog) = FLogSym0 - natSing2 = SNatKn (smallInteger (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) +#if MIN_VERSION_ghc (8,2,0) + natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) +#else + natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) +#endif -- | Type-level equivalent of /the ceiling of/ -- .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" @@ -176,8 +193,8 @@ z2 = integerLogBase# x (y-1) in case y of 1 -> SNatKn 0 - _ | isTrue# (z1 ==# z2) -> SNatKn (smallInteger (z1 +# 1#)) - | otherwise -> SNatKn (smallInteger z1) + _ | isTrue# (z1 ==# z2) -> SNatKn (intToNumber (z1 +# 1#)) + | otherwise -> SNatKn (intToNumber z1) -- | Type-level equivalent of -- where the operation only reduces when: @@ -199,30 +216,40 @@ instance (KnownNat x, KnownNat y, FLog x y ~ CLog x y) => KnownNat2 $(nameToSymbol ''Log) x y where type KnownNatF2 $(nameToSymbol ''Log) = LogSym0 - natSing2 = SNatKn (smallInteger (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) + natSing2 = SNatKn (intToNumber (integerLogBase# (natVal (Proxy @x)) (natVal (Proxy @y)))) -- | Type-level greatest common denominator (GCD). -- -- Note that additional equations are provided by the type-checker plugin solver -- "GHC.TypeLits.Extra.Solver". type family GCD (x :: Nat) (y :: Nat) :: Nat where - GCD 0 x = x -- Additional equations are provided by the custom solver + GCD 0 x = x + GCD x 0 = x + GCD 1 x = 1 + GCD x 1 = 1 + GCD x x = x + -- Additional equations are provided by the custom solver genDefunSymbols [''GCD] instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''GCD) x y where type KnownNatF2 $(nameToSymbol ''GCD) = GCDSym0 - natSing2 = SNatKn (gcd (natVal (Proxy @x)) (natVal (Proxy @y))) + natSing2 = SNatKn (gcd (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) -- | Type-level least common multiple (LCM). -- -- Note that additional equations are provided by the type-checker plugin solver -- "GHC.TypeLits.Extra.Solver". type family LCM (x :: Nat) (y :: Nat) :: Nat where - LCM 0 x = 0 -- Additional equations are provided by the custom solver + LCM 0 x = 0 + LCM x 0 = 0 + LCM 1 x = x + LCM x 1 = x + LCM x x = x + -- Additional equations are provided by the custom solver genDefunSymbols [''LCM] instance (KnownNat x, KnownNat y) => KnownNat2 $(nameToSymbol ''LCM) x y where type KnownNatF2 $(nameToSymbol ''LCM) = LCMSym0 - natSing2 = SNatKn (lcm (natVal (Proxy @x)) (natVal (Proxy @y))) + natSing2 = SNatKn (lcm (N.natVal (Proxy @x)) (N.natVal (Proxy @y))) diff --git a/src/GHC/TypeLits/Extra/Solver/Operations.hs b/src/GHC/TypeLits/Extra/Solver/Operations.hs --- a/src/GHC/TypeLits/Extra/Solver/Operations.hs +++ b/src/GHC/TypeLits/Extra/Solver/Operations.hs @@ -121,7 +121,7 @@ in case isNatural z of Just True -> x Just False -> y - _ -> Max x y + _ -> Min x y mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp mergeDiv _ (I 0) = Nothing @@ -157,7 +157,7 @@ mergeLCM :: ExtraOp -> ExtraOp -> ExtraOp mergeLCM (I i) (I j) = I (lcm i j) -mergeLCM x y = GCD x y +mergeLCM x y = LCM x y mergeExp :: ExtraOp -> ExtraOp -> ExtraOp mergeExp (I i) (I j) = I (i^j) diff --git a/src/GHC/TypeLits/Extra/Solver/Unify.hs b/src/GHC/TypeLits/Extra/Solver/Unify.hs --- a/src/GHC/TypeLits/Extra/Solver/Unify.hs +++ b/src/GHC/TypeLits/Extra/Solver/Unify.hs @@ -4,6 +4,8 @@ Maintainer : Christiaan Baaij -} +{-# LANGUAGE CPP #-} + module GHC.TypeLits.Extra.Solver.Unify ( ExtraDefs (..) , UnifyResult (..) @@ -85,15 +87,29 @@ unifyExtra :: Ct -> ExtraOp -> ExtraOp -> TcPluginM UnifyResult unifyExtra ct u v = do tcPluginTrace "unifyExtra" (ppr ct $$ ppr u $$ ppr v) - return (unifyExtra' ct u v) + return (unifyExtra' u v) -unifyExtra' :: Ct -> ExtraOp -> ExtraOp -> UnifyResult -unifyExtra' _ u v - | eqFV u v = if u == v then Win - else if containsConstants u || containsConstants v - then Draw - else Lose - | otherwise = Draw +unifyExtra' :: ExtraOp -> ExtraOp -> UnifyResult +unifyExtra' u v + | eqFV u v + = go u v + | otherwise + = Draw + where + go a b | a == b = Win + -- The following operations commute + go (Max a b) (Max x y) = commuteResult (go a y) (go b x) + go (Min a b) (Min x y) = commuteResult (go a y) (go b x) + go (GCD a b) (GCD x y) = commuteResult (go a y) (go b x) + go (LCM a b) (LCM x y) = commuteResult (go a y) (go b x) + -- If there are operations contained in the type which this solver does + -- not understand, then the result is a Draw + go a b = if containsConstants a || containsConstants b then Draw else Lose + + commuteResult Win Win = Win + commuteResult Lose _ = Lose + commuteResult _ Lose = Lose + commuteResult _ _ = Draw fvOP :: ExtraOp -> UniqSet TyVar fvOP (I _) = emptyUniqSet diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -127,6 +127,24 @@ test37 :: (1 <= Div l r) => Proxy l -> Proxy r -> () test37 _ _ = () +test38 :: Proxy (Min (0-1) 0) -> Proxy (0-1) +test38 = id + +test39 :: Proxy (Max (0-1) 0) -> Proxy 0 +test39 = id + +test40 :: Proxy x -> Proxy y -> Proxy (Max x y) -> Proxy (Max y x) +test40 _ _ = id + +test41 :: Proxy x -> Proxy y -> Proxy (Min x y) -> Proxy (Min y x) +test41 _ _ = id + +test42 :: Proxy x -> Proxy y -> Proxy (GCD x y) -> Proxy (GCD y x) +test42 _ _ = id + +test43 :: Proxy x -> Proxy y -> Proxy (LCM x y) -> Proxy (LCM y x) +test43 _ _ = id + main :: IO () main = defaultMain tests @@ -244,6 +262,24 @@ , testCase "1 <= Div 18 3" $ show (test37 (Proxy @18) (Proxy @3)) @?= "()" + , testCase "Min (0-1) 0 ~ (0-1)" $ + show (test38 Proxy) @?= + "Proxy" + , testCase "Max (0-1) 0 ~ 0" $ + show (test39 Proxy) @?= + "Proxy" + , testCase "forall x y . Max x y ~ Max y x" $ + show (test40 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y . Min x y ~ Min y x" $ + show (test41 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y . GCD x y ~ GCD y x" $ + show (test42 Proxy Proxy Proxy) @?= + "Proxy" + , testCase "forall x y . LCM x y ~ LCM y x" $ + show (test43 Proxy Proxy Proxy) @?= + "Proxy" ] , testGroup "errors" [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors