packages feed

type-natural 1.0.0.0 → 1.1.0.0

raw patch · 5 files changed

+39/−19 lines, 5 filesdep −tasty-expected-failuredep ~ghc-typelits-presburgerPVP ok

version bump matches the API change (PVP)

Dependencies removed: tasty-expected-failure

Dependency ranges changed: ghc-typelits-presburger

API changes (from Hackage documentation)

- Data.Type.Natural: [NonEqual] :: ((n === m) ~ 'False, (n == m) ~ 'False, Empty (n :~: m)) => Equality n m
+ Data.Type.Natural: [NonEqual] :: ((n === m) ~ 'False, (n == m) ~ 'False) => Equality n m
- Data.Type.Natural.Lemma.Order: cmpSuccStepR :: SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
+ Data.Type.Natural.Lemma.Order: cmpSuccStepR :: forall n m. SNat n -> SNat m -> (CmpNat n m :~: 'LT) -> CmpNat n (Succ m) :~: 'LT
- Data.Type.Natural.Lemma.Order: leqStep :: SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
+ Data.Type.Natural.Lemma.Order: leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> ((n + l) :~: m) -> IsTrue (n <=? m)
- Data.Type.Natural.Lemma.Order: leqWitness :: SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m
+ Data.Type.Natural.Lemma.Order: leqWitness :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m

Files

src/Data/Type/Natural/Core.hs view
@@ -48,6 +48,7 @@     sZero,     sOne,     Equality (..),+    equalAbsurdFromBool,     type (===),     (%~),     sFlipOrdering,@@ -122,12 +123,17 @@       then Just trustMe       else Nothing +-- | Since 1.1.0.0 (Type changed) data Equality n m where   Equal :: ((n == n) ~ 'True) => Equality n n   NonEqual ::-    ((n === m) ~ 'False, (n == m) ~ 'False, Empty (n :~: m)) =>+    ((n === m) ~ 'False, (n == m) ~ 'False) =>     Equality n m +equalAbsurdFromBool ::+  (x === y) ~ 'False => x :~: y -> a+equalAbsurdFromBool = \case+ type family a === b where   a === a = 'True   _ === _ = 'False@@ -185,9 +191,9 @@  viewNat :: forall n. SNat n -> ZeroOrSucc n viewNat n =-  case n `testEquality` sNat @0 of-    Just Refl -> IsZero-    Nothing -> gcastWith (trustMe @(1 <=? n) @ 'True) $ IsSucc (sPred n)+  case n %~ sNat @0 of+    Equal -> IsZero+    NonEqual -> IsSucc (sPred n)  type family FlipOrdering ord where   FlipOrdering 'LT = 'GT
src/Data/Type/Natural/Lemma/Order.hs view
@@ -502,16 +502,17 @@           === SLT `because` ih  cmpSuccStepR ::+  forall n m.   SNat n ->   SNat m ->   CmpNat n m :~: 'LT ->   CmpNat n (Succ m) :~: 'LT-cmpSuccStepR = proofCmpSuccStepR . induction base step+cmpSuccStepR = \sn -> proofCmpSuccStepR (induction base step sn) @m   where     base :: CmpSuccStepR 0     base = CmpSuccStepR $ \m _ -> cmpZero m -    step :: SNat n -> CmpSuccStepR n -> CmpSuccStepR (Succ n)+    step :: SNat x -> CmpSuccStepR x -> CmpSuccStepR (Succ x)     step n (CmpSuccStepR ih) = CmpSuccStepR $ \m snltm ->       case zeroOrSucc m of         IsZero -> absurd $ zeroNoLT (sSucc n) snltm@@ -579,26 +580,26 @@           n'LTm' = cmpSucc n' m' `trans` compareCongR n (sym sm'EQm) `trans` nLTm        in gcastWith (sym sm'EQm) $ LeqSucc n' m' $ ltToLeq n' m' n'LTm' -leqWitness :: SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m-leqWitness = leqWitPf . induction base step+leqWitness :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> DiffNat n m+leqWitness = \sn -> leqWitPf (induction base step sn) @m   where     base :: LeqWitPf 0     base = LeqWitPf $ \sm _ -> gcastWith (plusZeroL sm) $ DiffNat sZero sm -    step :: SNat n -> LeqWitPf n -> LeqWitPf (Succ n)-    step (n :: SNat n) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->+    step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)+    step (n :: SNat x) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->       case viewLeq (sSucc n) m snLEQm of         LeqZero _ -> absurd $ succNonCyclic n Refl         LeqSucc (_ :: SNat n') pm nLEQpm ->-          succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: n) pm nLEQpm+          succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: x) pm nLEQpm -leqStep :: SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)-leqStep = leqStepPf . induction base step+leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m)+leqStep sn = leqStepPf (induction base step sn) @m @l   where     base :: LeqStepPf 0     base = LeqStepPf $ \k _ _ -> leqZero k -    step :: SNat n -> LeqStepPf n -> LeqStepPf (Succ n)+    step :: forall k. SNat k -> LeqStepPf k -> LeqStepPf (Succ k)     step n (LeqStepPf ih) =       LeqStepPf $ \k l snPlEqk ->         let kEQspk =
src/Data/Type/Natural/Presburger/MinMaxSolver.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE CPP #-}+ {- | This module provides a variant of `ghc-typelits-presburger`,  which can be also solve symbols added in this package, such as  @Min@, @Max@, @<@, @>@, and @>=@.@@ -5,8 +7,19 @@ module Data.Type.Natural.Presburger.MinMaxSolver (plugin) where  import Control.Monad (mzero)-import GHC.TypeLits.Presburger.Compat (lookupModule)+import GHC.TypeLits.Presburger.Compat import GHC.TypeLits.Presburger.Types++#if MIN_VERSION_ghc(9,0,0)+import GHC.Plugins+  ( Plugin,+    fsLit,+    mkModuleName,+    mkTcOcc,+    splitTyConApp_maybe,+  )+import GHC.Tc.Plugin+#else import GhcPlugins   ( Plugin,     fsLit,@@ -15,6 +28,7 @@     splitTyConApp_maybe,   ) import TcPluginM+#endif  plugin :: Plugin plugin =
tests/Data/Type/Natural/Presburger/Cases.hs view
@@ -24,4 +24,4 @@ maxComm _ _ = Refl  falsity :: n <= m => p n -> q m -> Min n m :~: m-falsity = Refl+falsity _ _  = Refl
type-natural.cabal view
@@ -1,6 +1,6 @@ cabal-version: >=1.10 name:          type-natural-version:       1.0.0.0+version:       1.1.0.0 license:       BSD3 license-file:  LICENSE copyright:     (C) Hiromi ISHII 2013-2014@@ -55,7 +55,7 @@         template-haskell >=2.8,         constraints >=0.3,         ghc-typelits-natnormalise >=0.4,-        ghc-typelits-presburger >=0.5,+        ghc-typelits-presburger >=0.5.1,         ghc-typelits-knownnat -any,         integer-logarithms -any @@ -88,7 +88,6 @@         tasty-hunit -any,         tasty-discover -any,         template-haskell -any,-        tasty-expected-failure -any,         base -any,         type-natural -any,         equational-reasoning -any