ghc-typelits-natnormalise 0.5.6 → 0.5.7

raw patch · 4 files changed

+34/−2 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• ghc-typelits-natnormalise.cabal +1/−1
• src/GHC/TypeLits/Normalise/Unify.hs +12/−1
• tests/Tests.hs +18/−0

@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.5.7 *November 7th 2017*+* Solve inequalities such as: `1 <= a + 3`+ ## 0.5.6 *October 31st 2017* * Fixes bugs:   * `(x + 1) ~ (2 * y)` no longer implies `((2 * (y - 1)) + 1) ~ x`

@@ -1,5 +1,5 @@ name:                ghc-typelits-natnormalise-version:             0.5.6+version:             0.5.7 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

@@ -469,4 +469,15 @@ -- -- > (1 <=? a^b) ~ True isNatural (S [P [I (-1)],P [E s p]]) = (&&) <$> isNatural s <*> isNatural (S [p])-isNatural _ = Nothing+-- We give up for all other products for now+isNatural (S [P _]) = Nothing+-- Adding two natural numbers is also a natural number+isNatural (S (p:ps)) = do+  pN <- isNatural (S [p])+  pK <- isNatural (S ps)+  case (pN,pK) of+    (True,True)   -> return True  -- both are natural+    (False,False) -> return False -- both are non-natural+    _             -> Nothing+    -- if one is natural and the other isn't, then their sum *might* be natural,+    -- but we simply cant be sure.

@@ -3,7 +3,9 @@ {-# LANGUAGE KindSignatures      #-} {-# LANGUAGE TypeOperators       #-} {-# LANGUAGE NoImplicitPrelude   #-}+{-# LANGUAGE Rank2Types          #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications    #-}  {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} @@ -233,6 +235,16 @@ at :: SNat m -> Vec (m + (n + 1)) a -> a at n xs = head $ snd $ splitAt n xs +leToPlus+  :: forall (k :: Nat) (n :: Nat) f r+   . (k <= n)+  => f n+  -- ^ Argument with the @(k <= n)@ constraint+  -> (forall m . f (m + k) -> r)+  -- ^ Function with the @(n + k)@ constraint+  -> r+leToPlus a f = f @ (n-k) a+ proxyInEq1 :: Proxy a -> Proxy (a+1) -> () proxyInEq1 = proxyInEq @@ -248,6 +260,9 @@ proxyInEq5 :: Proxy 1 -> Proxy (2^a) -> () proxyInEq5 = proxyInEq +proxyInEq6 :: Proxy 1 -> Proxy (a + 3) -> ()+proxyInEq6 = proxyInEq+ proxyEq1 :: Proxy ((2 ^ x) * (2 ^ (x + x))) -> Proxy (2 * (2 ^ ((x + (x + x)) - 1))) proxyEq1 = id @@ -344,6 +359,9 @@     , testCase "`(2 <= (2 ^ (n + d)))` implies `(2 <= (2 ^ (d + n)))`" $       show (proxyInEqImplication (Proxy :: Proxy 3) (Proxy :: Proxy 4)) @?=       "Proxy"+    , testCase "1 <= a+3" $+      show (proxyInEq6 (Proxy :: Proxy 1) (Proxy :: Proxy 8)) @?=+      "()"     ]   , testGroup "errors"     [ testCase "x + 2 ~ 3 + x" $ testProxy1 `throws` testProxy1Errors