ghc-typelits-extra 0.2.2 → 0.2.3
raw patch · 6 files changed
+126/−31 lines, 6 filesdep +ghc-primdep ~ghcdep ~ghc-typelits-knownnatPVP ok
version bump matches the API change (PVP)
Dependencies added: ghc-prim
Dependency ranges changed: ghc, ghc-typelits-knownnat
API changes (from Hackage documentation)
Files
- CHANGELOG.md +15/−0
- ghc-typelits-extra.cabal +4/−3
- src/GHC/TypeLits/Extra.hs +45/−18
- src/GHC/TypeLits/Extra/Solver/Operations.hs +2/−2
- src/GHC/TypeLits/Extra/Solver/Unify.hs +24/−8
- tests/Main.hs +36/−0
CHANGELOG.md view
@@ -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`
ghc-typelits-extra.cabal view
@@ -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,
src/GHC/TypeLits/Extra.hs view
@@ -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/ <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> -- .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 <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> -- 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)))
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -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)
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -4,6 +4,8 @@ Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -} +{-# 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
tests/Main.hs view
@@ -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