type-natural 0.8.3.1 → 0.9.0.0
raw patch · 5 files changed
+47/−17 lines, 5 filesdep ~ghc-typelits-presburgerdep ~singletonsdep ~singletons-presburger
Dependency ranges changed: ghc-typelits-presburger, singletons, singletons-presburger
Files
- Data/Type/Natural/Class/Arithmetic.hs +1/−1
- Data/Type/Natural/Class/Order.hs +24/−4
- Data/Type/Natural/Definitions.hs +4/−0
- Data/Type/Ordinal.hs +14/−9
- type-natural.cabal +4/−3
Data/Type/Natural/Class/Arithmetic.hs view
@@ -294,7 +294,7 @@ multZeroR sn0 = multZeroRProof $ induction base step sn0 where base :: MultZeroR (Zero nat)- base = MultZeroR (multZeroR sZero)+ base = MultZeroR (multZeroL sZero) step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k) step sk (MultZeroR ih) = MultZeroR $
Data/Type/Natural/Class/Order.hs view
@@ -2,6 +2,10 @@ {-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810+{-# LANGUAGE StandaloneKindSignatures #-}+#endif+ module Data.Type.Natural.Class.Order (PeanoOrder(..), DiffNat(..), LeqView(..), FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,@@ -62,12 +66,28 @@ => Sing n -> Sing m -> DiffNat (n :: nat) m -> DiffNat (Succ n) (Succ m) succDiffNat _ _ (DiffNat n m) = coerce (plusSuccL n m) $ DiffNat (sSucc n) m -coerceLeqL :: forall (n :: nat) m l . IsPeano nat => n :~: m -> Sing l- -> IsTrue (n <= l) -> IsTrue (m <= l)+-- | Since 0.9.0.0 (type changed)+coerceLeqL+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810+ :: forall nat (n :: nat) m l.+#else+ :: forall (n :: nat) m l .+#endif+ IsPeano nat+ => n :~: m -> Sing l+ -> IsTrue (n <= l) -> IsTrue (m <= l) coerceLeqL Refl _ Witness = Witness -coerceLeqR :: forall (n :: nat) m l . IsPeano nat => Sing l -> n :~: m- -> IsTrue (l <= n) -> IsTrue (l <= m)+-- | Since 0.9.0.0 (type changed)+coerceLeqR+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810+ :: forall nat (n :: nat) m l .+#else+ :: forall (n :: nat) m l .+#endif+ IsPeano nat+ => Sing l -> n :~: m+ -> IsTrue (l <= n) -> IsTrue (l <= m) coerceLeqR _ Refl Witness = Witness singletonsOnly [d|
Data/Type/Natural/Definitions.hs view
@@ -3,6 +3,10 @@ {-# LANGUAGE KindSignatures, MultiParamTypeClasses, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-} {-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-}+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 810+{-# LANGUAGE StandaloneKindSignatures #-}+#endif+ module Data.Type.Natural.Definitions (module Data.Type.Natural.Definitions, module Data.Singletons.Prelude,
Data/Type/Ordinal.hs view
@@ -122,7 +122,8 @@ enumFrom = enumFromOrd enumFromTo = enumFromToOrd -enumFromToOrd :: forall (n :: nat).+-- | Since 0.9.0.0 (type changed)+enumFromToOrd :: forall nat (n :: nat). (HasOrdinal nat, SingI n) => Ordinal n -> Ordinal n -> [Ordinal n] enumFromToOrd ok ol =@@ -130,7 +131,8 @@ l = ordToInt ol in genericTake (l - k + 1) $ enumFromOrd ok -enumFromOrd :: forall (n :: nat).+-- | Since 0.9.0.0 (type changed)+enumFromOrd :: forall nat (n :: nat). (HasOrdinal nat, SingI n) => Ordinal n -> [Ordinal n] enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n)@@ -139,7 +141,8 @@ enumOrdinal :: (PeanoOrder nat) => Sing (n :: nat) -> [Ordinal n] enumOrdinal sn = withSingI sn $ map (reallyUnsafeNaturalToOrd Proxy) [0..toNatural sn - 1] -succOrd :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n)+-- | Since 0.9.0.0 (type changed)+succOrd :: forall nat (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n) succOrd (OLt n) = withRefl (succLneqSucc n (sing :: Sing n)) $ OLt (sSucc n)@@ -163,8 +166,8 @@ {-# INLINE maxBound #-} {-# DEPRECATED unsafeFromInt "Use unsafeNaturalToOrd instead" #-}--- | Since 0.8.0.0-unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))+-- | Since 0.9.0.0 (type changed)+unsafeFromInt :: forall nat (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Int -> Ordinal n unsafeFromInt = unsafeNaturalToOrd . fromIntegral @@ -172,7 +175,7 @@ -- If the given natural is greater or equal to @n@, raises exception. -- -- Since 0.8.0.0-unsafeNaturalToOrd :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat))+unsafeNaturalToOrd :: forall nat (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Natural -> Ordinal n unsafeNaturalToOrd k = fromMaybe (error "unsafeNaturalToOrd Out of bound") $@@ -180,12 +183,12 @@ {-# DEPRECATED unsafeFromInt' "Use unsafeNaturalToOrd' instead" #-} -- | Since 0.8.0.0-unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)+unsafeFromInt' :: forall proxy nat (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Int -> Ordinal n unsafeFromInt' p = unsafeNaturalToOrd' p . fromIntegral -- | Since 0.8.0.0-unsafeNaturalToOrd' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)+unsafeNaturalToOrd' :: forall proxy nat (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Natural -> Ordinal n unsafeNaturalToOrd' _ n = case fromNatural n of@@ -269,7 +272,9 @@ -- | Ordinal addition.-(@+) :: forall n m. (PeanoOrder nat, SingI (n :: nat), SingI m)+--+-- Since 0.9.0.0 (type changed)+(@+) :: forall nat (n :: nat) m. (PeanoOrder nat, SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n + m) OLt k @+ OLt l = let (n, m) = (n :: Sing n, m :: Sing m)
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.8.3.1+version: 0.9.0.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. .@@ -18,7 +18,8 @@ category: Math build-type: Simple cabal-version: >= 1.10-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3, GHC == 8.6.3, GHC == 8.8.2+tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3,+ GHC == 8.6.3, GHC == 8.8.3, GHC == 8.10.1 source-repository head Type: git@@ -47,7 +48,7 @@ , template-haskell >= 2.8 , constraints >= 0.3 , ghc-typelits-natnormalise >= 0.4- , singletons >= 2.2 && < 2.6+ , singletons >= 2.2 && < 2.8 default-language: Haskell2010 default-extensions: DataKinds