packages feed

ghc-typelits-extra 0.2 → 0.2.1

raw patch · 8 files changed

+68/−17 lines, 8 filesdep +template-haskell

Dependencies added: template-haskell

Files

CHANGELOG.md view
@@ -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`
README.md view
@@ -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)
ghc-typelits-extra.cabal view
@@ -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 <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:mod mod>   .   * @FLog@: type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#>-    .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/ <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)@"+    i.e. the exact integer equivalent to @ceiling (logBase x y)@   .   * @Log@: 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 "@'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 <http://hackage.haskell.org/package/base-4.8.2.0/docs/Prelude.html#v:gcd gcd>   .@@ -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
src/GHC/TypeLits/Extra.hs view
@@ -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 <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> -- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"
src/GHC/TypeLits/Extra/Solver.hs view
@@ -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'
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -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
tests/ErrorTests.hs view
@@ -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'"+    )]
tests/Main.hs view
@@ -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"