type-natural 1.2.0.1 → 1.3.0.0
raw patch · 9 files changed
+180/−86 lines, 9 filesdep ~ghc-typelits-presburger
Dependency ranges changed: ghc-typelits-presburger
Files
- Changelog.md +6/−0
- src/Data/Type/Natural.hs +15/−5
- src/Data/Type/Natural/Core.hs +105/−34
- src/Data/Type/Natural/Lemma/Order.hs +4/−4
- src/Data/Type/Ordinal.hs +3/−3
- tests/Data/Type/Natural/Lemma/OrderSpec.hs +20/−17
- tests/Data/Type/NaturalSpec.hs +13/−13
- tests/Shared.hs +1/−1
- type-natural.cabal +13/−9
+ Changelog.md view
@@ -0,0 +1,6 @@+# Changelog++## 1.3.0.0++* Supports GHC 9.6+* Adds compatibility layer for `SNat` singleton provided since base 4.18
src/Data/Type/Natural.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-}@@ -32,6 +33,7 @@ toSomeSNat, withSNat, withKnownNat,+ fromSNat, natVal, natVal', someNatVal,@@ -103,20 +105,23 @@ -- * Singletons for auxiliary types SBool (..), SOrdering (..),+ OrderingI(..),+ fromOrderingI,+ toOrderingI, FlipOrdering, sFlipOrdering, ) where -import Data.Coerce (coerce) import Data.Proxy (Proxy) import Data.Type.Natural.Core import Data.Type.Natural.Lemma.Arithmetic import Data.Type.Natural.Lemma.Order import Language.Haskell.TH (litT, numTyLit) import Language.Haskell.TH.Quote-import Numeric.Natural import Text.Read (readMaybe)+import Data.Ord (comparing)+import Data.Function (on) {- | Quotesi-quoter for SNatleton types for @'GHC.TypeLits.Nat'@. This can be used for an expression. @@ -141,7 +146,8 @@ } toNatural :: SNat n -> Natural-toNatural = coerce+{-# DEPRECATED toNatural "Use fromSNat instead" #-}+toNatural = fromSNat data SomeSNat where SomeSNat :: KnownNat n => SNat n -> SomeSNat@@ -149,8 +155,12 @@ deriving instance Show SomeSNat instance Eq SomeSNat where- SomeSNat (SNat n) == SomeSNat (SNat m) = n == m- SomeSNat (SNat n) /= SomeSNat (SNat m) = n /= m+ (==) = (==) `on` \(SomeSNat n) -> fromSNat n+ {-# INLINE (==) #-}++instance Ord SomeSNat where+ compare = comparing (\(SomeSNat n) -> fromSNat n)+ {-# INLINE compare #-} toSomeSNat :: Natural -> SomeSNat toSomeSNat n = case someNatVal n of
src/Data/Type/Natural/Core.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE EmptyCase #-}@@ -23,11 +24,16 @@ {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} module Data.Type.Natural.Core- ( SNat (.., Zero, Succ),+ ( SNat (Zero, Succ),+#if !MIN_VERSION_base(4,18,0)+ fromSNat,+ withKnownNat,+ withSomeSNat,+#endif+ unsafeLiftSBin, ZeroOrSucc (..), viewNat, sNat,- withKnownNat, (%+), (%-), (%*),@@ -56,73 +62,119 @@ FlipOrdering, SOrdering (..), SBool (..),+ Natural,+ OrderingI(..),+ fromOrderingI,+ toOrderingI, -- Re-exports module GHC.TypeNats, ) where -import Data.Coerce (coerce)-import Data.Proxy (Proxy) import Data.Type.Equality- ( TestEquality (..),- gcastWith,- type (:~:) (..),+ ( type (:~:) (..), type (==), )-import Data.Type.Natural.Utils-import GHC.Exts (Proxy#, proxy#) import GHC.TypeNats import Math.NumberTheory.Logarithms (naturalLog2)-import Numeric.Natural (Natural) import Type.Reflection (Typeable) import Unsafe.Coerce (unsafeCoerce)+import Numeric.Natural +#if MIN_VERSION_base(4,16,0)+import Data.Type.Ord (OrderingI(..))+#endif++#if !MIN_VERSION_base(4,18,0)+import Data.Proxy+import Data.Type.Equality+import GHC.Exts+#endif++#if !MIN_VERSION_base(4,18,0) -- | A singleton for type-level naturals-newtype SNat (n :: Nat) = SNat Natural+newtype SNat (n :: Nat) = UnsafeSNat Natural deriving newtype (Show, Eq, Ord) -withKnownNat :: forall n r. SNat n -> (KnownNat n => r) -> r-withKnownNat (SNat n) act =+fromSNat :: SNat n -> Natural+fromSNat = coerce++withKnownNat :: forall n rep (r :: TYPE rep). SNat n -> (KnownNat n => r) -> r+withKnownNat (UnsafeSNat n) act = case someNatVal n of SomeNat (_ :: Proxy m) ->- gcastWith (unsafeCoerce (Refl @()) :: n :~: m) act+ case unsafeCoerce (Refl @()) :: n :~: m of+ Refl -> act +data KnownNatInstance (n :: Nat) where+ KnownNatInstance :: KnownNat n => KnownNatInstance n++-- An internal function that is only used for defining the SNat pattern+-- synonym.+knownNatInstance :: SNat n -> KnownNatInstance n+knownNatInstance sn = withKnownNat sn KnownNatInstance++pattern SNat :: forall n. () => KnownNat n => SNat n+pattern SNat <- (knownNatInstance -> KnownNatInstance) + where SNat = sNat++withSomeSNat :: forall rep (r :: TYPE rep). Natural -> (forall n. SNat n -> r) -> r+withSomeSNat n f = f (UnsafeSNat n)+#endif++unsafeLiftSBin :: (Natural -> Natural -> Natural) -> SNat n -> SNat m -> SNat k+{-# INLINE unsafeLiftSBin #-}+unsafeLiftSBin f = \l r -> withSomeSNat (fromSNat l `f` fromSNat r) unsafeCoerce++unsafeLiftSUnary :: (Natural -> Natural) -> SNat n -> SNat k+{-# INLINE unsafeLiftSUnary #-}+unsafeLiftSUnary f = \l -> withSomeSNat (f $ fromSNat l) unsafeCoerce+ (%+) :: SNat n -> SNat m -> SNat (n + m)-(%+) = coerce $ (+) @Natural+{-# INLINE (%+) #-}+(%+) = unsafeLiftSBin (+) (%-) :: SNat n -> SNat m -> SNat (n - m)-(%-) = coerce $ (-) @Natural+(%-) = unsafeLiftSBin (-) (%*) :: SNat n -> SNat m -> SNat (n * m)-(%*) = coerce $ (*) @Natural+(%*) = unsafeLiftSBin (*) sDiv :: SNat n -> SNat m -> SNat (Div n m)-sDiv = coerce $ div @Natural+sDiv = unsafeLiftSBin quot sMod :: SNat n -> SNat m -> SNat (Mod n m)-sMod = coerce $ mod @Natural+sMod = unsafeLiftSBin rem (%^) :: SNat n -> SNat m -> SNat (n ^ m)-(%^) = coerce $ (^) @Natural @Natural+(%^) = unsafeLiftSBin (^) sLog2 :: SNat n -> SNat (Log2 n)-sLog2 = coerce $ fromIntegral @Int @Natural . naturalLog2+sLog2 = unsafeLiftSUnary $ fromIntegral . naturalLog2 sNat :: forall n. KnownNat n => SNat n-sNat = SNat $ natVal' (proxy# :: Proxy# n)+#if MIN_VERSION_base(4,18,0)+sNat = SNat+#else+sNat = UnsafeSNat $ natVal' (proxy# :: Proxy# n)+#endif + infixl 6 %+, %- infixl 7 %*, `sDiv`, `sMod` infixr 8 %^ +#if !MIN_VERSION_ghc(4,18,0) instance TestEquality SNat where- testEquality (SNat l) (SNat r) =+ testEquality (UnsafeSNat l) (UnsafeSNat r) = if l == r then Just trustMe else Nothing+#endif + -- | Since 1.1.0.0 (Type changed) data Equality n m where Equal :: ((n == n) ~ 'True) => Equality n n@@ -141,8 +193,8 @@ infix 4 ===, %~ (%~) :: SNat l -> SNat r -> Equality l r-SNat l %~ SNat r =- if l == r+l %~ r =+ if fromSNat l == fromSNat r then unsafeCoerce (Equal @()) else unsafeCoerce (NonEqual @0 @1) @@ -195,27 +247,45 @@ Equal -> IsZero NonEqual -> IsSucc (sPred n) ++#if !MIN_VERSION_base(4,16,0)+data OrderingI (a :: Nat) (b :: Nat) where+ LTI :: CmpNat a b ~ 'LT => OrderingI a b+ EQI :: CmpNat a b ~ 'EQ => OrderingI a b+ GTI :: CmpNat a b ~ 'GT => OrderingI a b+#endif+ type family FlipOrdering ord where FlipOrdering 'LT = 'GT FlipOrdering 'GT = 'LT FlipOrdering 'EQ = 'EQ -sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)-sFlipOrdering SLT = SGT-sFlipOrdering SEQ = SEQ-sFlipOrdering SGT = SLT- data SOrdering (ord :: Ordering) where SLT :: SOrdering 'LT SEQ :: SOrdering 'EQ SGT :: SOrdering 'GT +fromOrderingI :: OrderingI n m -> SOrdering (CmpNat n m)+fromOrderingI LTI = SLT+fromOrderingI EQI = SEQ+fromOrderingI GTI = SGT++toOrderingI :: SOrdering (CmpNat n m) -> OrderingI n m+toOrderingI SLT = LTI+toOrderingI SEQ = EQI+toOrderingI SGT = GTI+ deriving instance Show (SOrdering ord) deriving instance Eq (SOrdering ord) deriving instance Typeable SOrdering +sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)+sFlipOrdering SLT = SGT+sFlipOrdering SEQ = SEQ+sFlipOrdering SGT = SLT+ data SBool (b :: Bool) where SFalse :: SBool 'False STrue :: SBool 'True@@ -229,15 +299,16 @@ infix 4 %<=? (%<=?) :: SNat n -> SNat m -> SBool (n <=? m)-SNat n %<=? SNat m =- if n <= m+n %<=? m =+ if fromSNat n <= fromSNat m then unsafeCoerce STrue else unsafeCoerce SFalse sCmpNat, sCompare :: SNat n -> SNat m -> SOrdering (CmpNat n m) sCompare = sCmpNat-sCmpNat (SNat n) (SNat m) =- case compare n m of+sCmpNat n m =+ case compare (fromSNat n) (fromSNat m) of LT -> unsafeCoerce SLT EQ -> unsafeCoerce SEQ GT -> unsafeCoerce SGT+
src/Data/Type/Natural/Lemma/Order.hs view
@@ -154,12 +154,10 @@ ) where -import Data.Coerce (coerce) import Data.Type.Equality (gcastWith, (:~:) (..)) import Data.Type.Natural.Core import Data.Type.Natural.Lemma.Arithmetic import Data.Void (Void, absurd)-import Numeric.Natural (Natural) import Proof.Equational ( because, start,@@ -271,10 +269,12 @@ #endif sMin :: SNat n -> SNat m -> SNat (Min n m)-sMin = coerce $ min @Natural+{-# INLINE sMin #-}+sMin = unsafeLiftSBin min sMax :: SNat n -> SNat m -> SNat (Max n m)-sMax = coerce $ max @Natural+{-# INLINE sMax #-}+sMax = unsafeLiftSBin max #if MIN_VERSION_ghc(9,2,1) type Max m n = DTO.Max @Nat m n
src/Data/Type/Ordinal.hs view
@@ -137,7 +137,7 @@ (KnownNat n) => Show (Ordinal (n :: Nat)) where- showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToNatural o) . showString " / " . showsPrec d (toNatural (sNat :: SNat n)))+ showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToNatural o) . showString " / " . showsPrec d (fromSNat (sNat :: SNat n))) instance Eq (Ordinal (n :: Nat)) where o == o' = ordToNatural o == ordToNatural o'@@ -179,7 +179,7 @@ -- | Enumerate all @'Ordinal'@s less than @n@. enumOrdinal :: SNat (n :: Nat) -> [Ordinal n]-enumOrdinal sn = withKnownNat sn $ map (reallyUnsafeNaturalToOrd Proxy) [0 .. toNatural sn - 1]+enumOrdinal sn = withKnownNat sn $ map (reallyUnsafeNaturalToOrd Proxy) [0 .. fromSNat sn - 1] -- | Since 1.0.0.0 (type changed) succOrd :: forall (n :: Nat). (KnownNat n) => Ordinal n -> Ordinal (Succ n)@@ -270,7 +270,7 @@ ordToNatural :: Ordinal (n :: Nat) -> Natural-ordToNatural (OLt n) = toNatural n+ordToNatural (OLt n) = fromSNat n {- | Inclusion function for ordinals.
tests/Data/Type/Natural/Lemma/OrderSpec.hs view
@@ -127,11 +127,14 @@ eith <- try @SomeException $ evaluate contradiction case eith of Left someE -> do- pure $+ pure $ counterexample (show someE) $ property $ "Impossible" `isPrefixOf` show someE || "Non-exhaustive" `isInfixOf` show someE- Right {} -> pure $ property False+ || "missingAlt" `isInfixOf` show someE+ Right v -> + pure $ counterexample "Value of void returned..." + $ property False test_Lemmas :: TestTree test_Lemmas =@@ -146,8 +149,8 @@ \(SomeSNat sn) (SomeSNat sm) -> case succDiffNat sn (sn %+ sm) (DiffNat sn sm) of DiffNat sns sms ->- toNatural (sns %+ sms)- === toNatural sn + toNatural sm + 1+ fromSNat (sns %+ sms)+ === fromSNat sn + fromSNat sm + 1 , testProperty @(SomeSNat -> SomeSNat -> Property) "compareCongR terminates" $ \(SomeSNat a) (SomeSNat (_ :: SNat b)) ->@@ -157,9 +160,9 @@ $ \case MkSomeLeqNat a b -> case leqToCmp a b Witness of- Left Refl -> toNatural a === toNatural b+ Left Refl -> fromSNat a === fromSNat b Right Refl ->- property $ toNatural a < toNatural b+ property $ fromSNat a < fromSNat b , testProperty @(SomeSNat -> Property) "eqlCmpEQ terminates" $ \(SomeSNat n) ->@@ -248,24 +251,24 @@ , testProperty @(SomeSNat -> Property) "leqViewRefl works properly" $ \(SomeSNat sn) -> case leqViewRefl sn of LeqZero sn' ->- toNatural sn' === toNatural sn .&&. toNatural sn' === 0+ fromSNat sn' === fromSNat sn .&&. fromSNat sn' === 0 LeqSucc sn' sm' Witness ->- toNatural sn' === toNatural sm'- .&&. toNatural sn' + 1 === toNatural sn+ fromSNat sn' === fromSNat sm'+ .&&. fromSNat sn' + 1 === fromSNat sn , testProperty @(SomeLeqNat -> Property) "viewLeq works properly" $ \(MkSomeLeqNat sn sm) -> case viewLeq sn sm Witness of LeqZero sm' ->- toNatural sn === 0 .&&. toNatural sm === toNatural sm'+ fromSNat sn === 0 .&&. fromSNat sm === fromSNat sm' LeqSucc sn' sm' Witness ->- toNatural sn' + 1 === toNatural sn- .&&. toNatural sm' + 1 === toNatural sm- .&&. toNatural sn' <= toNatural sm'+ fromSNat sn' + 1 === fromSNat sn+ .&&. fromSNat sm' + 1 === fromSNat sm+ .&&. fromSNat sn' <= fromSNat sm' , testProperty @(SomeLeqNat -> Property) "leqWitness gives the difference as a witness" $ \(MkSomeLeqNat sn sm) -> case leqWitness sn sm Witness of DiffNat sn' delta ->- toNatural sn === toNatural sn'- .&&. toNatural sn' + toNatural delta === toNatural sm+ fromSNat sn === fromSNat sn'+ .&&. fromSNat sn' + fromSNat delta === fromSNat sm , testProperty @(SomeSNat -> SomeSNat -> Property) "leqStep terminates" $ \(SomeSNat n) (SomeSNat l) ->@@ -392,7 +395,7 @@ totalWitness $ maxLeqR n m , testProperty @(SomeLeqNat -> Property) "maxLeast termaxates" $ \(MkSomeLeqNat n l) ->- forAll (elements [0 .. toNatural l]) $ \m0 ->+ forAll (elements [0 .. fromSNat l]) $ \m0 -> case toSomeSNat m0 of SomeSNat m -> totalWitness $@@ -479,4 +482,4 @@ ) totalRefl :: a :~: b -> Property-totalRefl = total+totalRefl = within 10000 . total
tests/Data/Type/NaturalSpec.hs view
@@ -23,50 +23,50 @@ "Arithmetic operations on singletons behaves correctly" [ testProperty "(+), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $- toNatural (n %+ m) === (natVal n + natVal m)+ fromSNat (n %+ m) === (natVal n + natVal m) , $(testBinary "(+)" ''(+) '(%+)) , testProperty "(-), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $ disjoin- [ natVal n < natVal m .&&. toNatural (m %- n) === (natVal m - natVal n)- , toNatural (n %- m) === (natVal n - natVal m)+ [ natVal n < natVal m .&&. fromSNat (m %- n) === (natVal m - natVal n)+ , fromSNat (n %- m) === (natVal n - natVal m) ] , $(testBinaryP (>=) "(-)" ''(-) '(%-)) , testProperty "(*), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $- toNatural (n %* m) === (natVal n * natVal m)+ fromSNat (n %* m) === (natVal n * natVal m) , $(testBinary "(*)" ''(*) '(%*)) , testProperty "Div, compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $ label "divide by zero" (natVal m === 0)- .||. toNatural (n `sDiv` m) === (natVal n `div` natVal m)+ .||. fromSNat (n `sDiv` m) === (natVal n `div` natVal m) , $(testBinaryP (const $ (/= 0)) "Div" ''Div 'sDiv) , testProperty "Mod, compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $ label "divide by zero" (natVal m === 0)- .||. toNatural (n `sMod` m) === (natVal n `mod` natVal m)+ .||. fromSNat (n `sMod` m) === (natVal n `mod` natVal m) , $(testBinaryP (const $ (/= 0)) "Mod" ''Mod 'sMod) , testProperty "(^), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $- toNatural (n %^ m) === (natVal n ^ natVal m)+ fromSNat (n %^ m) === (natVal n ^ natVal m) , $(testBinaryP (\a b -> a /= 0 && b /= 0) "(^)" ''(^) '(%^)) , testProperty "(-.), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $- toNatural (n %-. m) === (if natVal n < natVal m then 0 else natVal n - natVal m)+ fromSNat (n %-. m) === (if natVal n < natVal m then 0 else natVal n - natVal m) , $(testBinary "(-.)" ''(-.) '(%-.)) , testProperty "Log2" $ \(SomeSNat n) -> tabulateDigits [natVal n] $ label "undefined" (natVal n === 0)- .||. toNatural (sLog2 n) === fromIntegral (naturalLog2 (natVal n))+ .||. fromSNat (sLog2 n) === fromIntegral (naturalLog2 (natVal n)) , $(testUnary False "Log2" ''Log2 'sLog2) , testProperty "succ" $ \(SomeSNat n) -> tabulateDigits [natVal n] $- toNatural (sSucc n) === succ (natVal n)+ fromSNat (sSucc n) === succ (natVal n) , $(testUnary True "Succ" ''Succ 'sSucc) , testProperty "pred" $ \(SomeSNat n) -> tabulateDigits [natVal n] $ label "undefiend" (natVal n === 0)- .||. toNatural (sPred n) === pred (natVal n)+ .||. fromSNat (sPred n) === pred (natVal n) , $(testUnary False "Pred" ''Pred 'sPred) ] @@ -105,11 +105,11 @@ , $(testBinary "CmpNat" ''CmpNat 'sCmpNat) , testProperty "min" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $- toNatural (n `sMin` m) === (natVal n `min` natVal m)+ fromSNat (n `sMin` m) === (natVal n `min` natVal m) , $(testBinary "min" ''Min 'sMin) , testProperty "max" $ \(SomeSNat n) (SomeSNat m) -> tabulateDigits [natVal n, natVal m] $- toNatural (n `sMax` m) === (natVal n `max` natVal m)+ fromSNat (n `sMax` m) === (natVal n `max` natVal m) , $(testBinary "max" ''Max 'sMax) ]
@@ -68,7 +68,7 @@ instance Demote Nat where type Demoted Nat = Natural- demote = toNatural+ demote = fromSNat type instance Sing = SOrdering
type-natural.cabal view
@@ -1,13 +1,13 @@ cabal-version: >=1.10 name: type-natural-version: 1.2.0.1+version: 1.3.0.0 license: BSD3 license-file: LICENSE-copyright: (C) Hiromi ISHII 2013-2022+copyright: (C) Hiromi ISHII 2013-2023 maintainer: konn.jinro_at_gmail.com author: Hiromi ISHII tested-with:- GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.1 || ==9.2.4 || ==9.4.3+ GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.2 || ==9.2.7 || ==9.4.4 || ==9.6.1 homepage: https://github.com/konn/type-natural synopsis: Type-level natural and proofs of their properties.@@ -20,6 +20,8 @@ category: Math build-type: Simple+extra-source-files:+ Changelog.md source-repository head type: git@@ -56,7 +58,7 @@ TypeOperators UndecidableInstances - ghc-options: -Wall -O2 -fno-warn-orphans+ ghc-options: -Wall -fno-warn-orphans build-depends: base >=4 && <5 , constraints >=0.3@@ -67,11 +69,13 @@ , integer-logarithms , template-haskell >=2.8 - if impl(ghc >=9.4)- build-depends: ghc-typelits-presburger >=0.7.1-+ if impl(ghc >= 9.6)+ build-depends: ghc-typelits-presburger >=0.7.2 else- build-depends: ghc-typelits-presburger+ if impl(ghc >=9.4)+ build-depends: ghc-typelits-presburger >=0.7.1+ else+ build-depends: ghc-typelits-presburger if impl(ghc >=8.0.0) ghc-options: -Wno-redundant-constraints@@ -82,7 +86,7 @@ test-suite type-natural-test type: exitcode-stdio-1.0 main-is: test.hs- build-tools: tasty-discover -any+ build-tool-depends: tasty-discover:tasty-discover hs-source-dirs: tests default-language: Haskell2010 ghc-options: -Wall