diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.2.1 *September 29th 2016* +* Reduce `Max n n` to `n` +* Reduce `Min n n` to `n` + # 0.2 *August 19th 2016* * New type-level operations: * `Max`: type-level `max` diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # ghc-typelits-extra -[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-extra.png?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-extra) +[![Build Status](https://secure.travis-ci.org/clash-lang/ghc-typelits-extra.svg?branch=master)](http://travis-ci.org/clash-lang/ghc-typelits-extra) [![Hackage](https://img.shields.io/hackage/v/ghc-typelits-extra.svg)](https://hackage.haskell.org/package/ghc-typelits-extra) [![Hackage Dependencies](https://img.shields.io/hackage-deps/v/ghc-typelits-extra.svg?style=flat)](http://packdeps.haskellers.com/feed?needle=exact%3Aghc-typelits-extra) 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 +version: 0.2.1 synopsis: Additional type-level operations on GHC.TypeLits.Nat description: Additional type-level operations on @GHC.TypeLits.Nat@: @@ -13,13 +13,13 @@ * @Mod@: type-level . * @FLog@: type-level equivalent of - .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" + i.e. the exact integer equivalent to @floor (logBase x y)@ . * @CLog@: type-level equivalent of /the ceiling of/ - .i.e. the exact integer equivalent to "@'ceiling' ('logBase' x y)@" + i.e. the exact integer equivalent to @ceiling (logBase x y)@ . * @Log@: type-level equivalent of - where the operation only reduces when "@'floor' ('logBase' b x) ~ 'ceiling' ('logBase' b x)@" + where the operation only reduces when @floor (logBase b x) ~ ceiling (logBase b x)@ . * @GCD@: a type-level . @@ -98,10 +98,12 @@ ghc-typelits-knownnat >= 0.2, ghc-typelits-natnormalise >= 0.4.1, tasty >= 0.10, - tasty-hunit >= 0.9 + tasty-hunit >= 0.9, + template-haskell >= 2.11.0.0 hs-source-dirs: tests default-language: Haskell2010 other-extensions: DataKinds + TemplateHaskell TypeOperators if flag(deverror) ghc-options: -O0 -dcore-lint 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 @@ -85,6 +85,8 @@ -- | 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 genDefunSymbols [''Max] @@ -96,6 +98,8 @@ -- | 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 genDefunSymbols [''Min] @@ -115,7 +119,7 @@ instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where type KnownNatF2 $(nameToSymbol ''Div) = DivSym0 - natSing2 = SNatKn (div (natVal (Proxy @x)) (natVal (Proxy @y))) + natSing2 = SNatKn (quot (natVal (Proxy @x)) (natVal (Proxy @y))) -- | Type-level 'mod' -- @@ -128,7 +132,7 @@ instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where type KnownNatF2 $(nameToSymbol ''Mod) = ModSym0 - natSing2 = SNatKn (mod (natVal (Proxy @x)) (natVal (Proxy @y))) + natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y))) -- | Type-level equivalent of -- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@" diff --git a/src/GHC/TypeLits/Extra/Solver.hs b/src/GHC/TypeLits/Extra/Solver.hs --- a/src/GHC/TypeLits/Extra/Solver.hs +++ b/src/GHC/TypeLits/Extra/Solver.hs @@ -49,10 +49,6 @@ -- | A solver implement as a type-checker plugin for: -- --- * 'Max': type-level 'max' --- --- * 'Min': type-level 'min' --- -- * 'Div': type-level 'div' -- -- * 'Mod': type-level 'mod' 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 @@ -139,6 +139,7 @@ reifyEOP defs (Exp x y) = mkTyConApp typeNatExpTyCon [reifyEOP defs x ,reifyEOP defs y] + containsConstants :: ExtraOp -> Bool containsConstants (I _) = False containsConstants (V _) = False diff --git a/tests/ErrorTests.hs b/tests/ErrorTests.hs --- a/tests/ErrorTests.hs +++ b/tests/ErrorTests.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE DataKinds, TypeOperators #-} +{-# LANGUAGE DataKinds, TypeOperators, TemplateHaskell #-} {-# OPTIONS_GHC -fdefer-type-errors #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} @@ -11,6 +11,10 @@ import GHC.TypeLits import GHC.TypeLits.Extra +import GHC.IO.Encoding (getLocaleEncoding, textEncodingName, utf8) +import Language.Haskell.TH (litE, stringL) +import Language.Haskell.TH.Syntax (runIO) + testFail1 :: Proxy (GCD 6 8) -> Proxy 4 testFail1 = id @@ -117,10 +121,18 @@ ] testFail10Errors = - ["Couldn't match type ‘'False’ with ‘'True’"] + [$(do localeEncoding <- runIO (getLocaleEncoding) + if textEncodingName localeEncoding == textEncodingName utf8 + then litE $ stringL "Couldn't match type ‘'False’ with ‘'True’" + else litE $ stringL "Couldn't match type 'False with 'True" + )] testFail11Errors = - ["Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’"] + [$(do localeEncoding <- runIO (getLocaleEncoding) + if textEncodingName localeEncoding == textEncodingName utf8 + then litE $ stringL "Couldn't match type ‘CLog 2 4 <=? CLog 4 4’ with ‘'True’" + else litE $ stringL "Couldn't match type `CLog 2 4 <=? CLog 4 4' with 'True" + )] testFail12Errors = ["Expected type: Proxy (Div 4 0) -> Proxy 4" @@ -158,7 +170,15 @@ ] testFail19Errors = - ["Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’"] + [$(do localeEncoding <- runIO (getLocaleEncoding) + if textEncodingName localeEncoding == textEncodingName utf8 + then litE $ stringL "Couldn't match type ‘FLog 3 0’ with ‘CLog 3 0’" + else litE $ stringL "Couldn't match type `FLog 3 0' with `CLog 3 0'" + )] testFail20Errors = - ["Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"] + [$(do localeEncoding <- runIO (getLocaleEncoding) + if textEncodingName localeEncoding == textEncodingName utf8 + then litE $ stringL "Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’" + else litE $ stringL "Couldn't match type `FLog 3 10' with `CLog 3 10'" + )] diff --git a/tests/Main.hs b/tests/Main.hs --- a/tests/Main.hs +++ b/tests/Main.hs @@ -94,6 +94,18 @@ test26 :: Proxy (b ^ (Log b y)) -> Proxy y test26 = id +test27 :: Proxy (Max n n) -> Proxy n +test27 = id + +test28 :: Proxy (Min n n) -> Proxy n +test28 = id + +test29 :: Proxy (Max n n + 1) -> Proxy (1 + n) +test29 = id + +test30 :: Proxy n -> Proxy (1 + Max n n) -> Proxy (Min n n + 1) +test30 _ = id + main :: IO () main = defaultMain tests @@ -177,6 +189,18 @@ "Proxy" , testCase "forall x>1 . x ^ (Log x y) ~ y" $ show (test26 Proxy) @?= + "Proxy" + , testCase "forall x . Max x x ~ x" $ + show (test27 Proxy) @?= + "Proxy" + , testCase "forall x . Min x x ~ x" $ + show (test28 Proxy) @?= + "Proxy" + , testCase "forall x . (Max x x + 1) ~ (1 + x)" $ + show (test29 Proxy) @?= + "Proxy" + , testCase "forall x . (Min x x + 1) ~ (1 + Max x x)" $ + show (test30 Proxy Proxy) @?= "Proxy" ] , testGroup "errors"