type-natural 0.4.1.1 → 0.4.2.0

raw patch · 6 files changed

+51/−32 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Data/Type/Natural.hs +3/−2
• Data/Type/Natural/Builtin.hs +9/−8
• Data/Type/Natural/Core.hs +11/−8
• Data/Type/Natural/Definitions.hs +19/−6
• Data/Type/Ordinal.hs +8/−7
• type-natural.cabal +1/−1

@@ -75,8 +75,8 @@ import Data.Type.Natural.Core import Data.Type.Natural.Definitions hiding ((:<=)) -import           Data.Constraint           hiding ((:-)) import           Data.Singletons+import qualified Data.Singletons.Prelude as S import           Data.Type.Monomorphic import           Language.Haskell.TH import           Language.Haskell.TH.Quote@@ -86,6 +86,7 @@ import           Prelude                   (Ord (..)) import qualified Prelude                   as P import           Proof.Equational+import Data.Constraint (Dict(..))  -------------------------------------------------- -- * Conversion functions.@@ -242,7 +243,7 @@ plusCommutative = plusComm {-# DEPRECATED plusCommutative "Will be removed in @0.5.0.0@. Use @'plusComm'@ instead." #-} -eqSuccMinus :: ((m :<<= n) ~ 'True)+eqSuccMinus :: ((m S.:<= n) ~ 'True)             => SNat n -> SNat m -> ('S n :-: m) :=: ('S (n :-: m)) eqSuccMinus _      SZ     = Refl eqSuccMinus (SS n) (SS m) =

@@ -36,6 +36,7 @@ import           Data.Singletons.Decide       (Decision (..), (%~)) import           Data.Singletons.Decide       (Void) import           Data.Singletons.Prelude.Bool (Sing (..))+import           Data.Singletons.Prelude.Ord  (POrd(..), SOrd ((%:<=))) import           Data.Singletons.Prelude.Enum (Pred, sPred, sSucc) import           Data.Singletons.Prelude.Num  (SNum (..)) import           Data.Type.Natural            (Nat (S, Z), Sing (SS, SZ))@@ -224,10 +225,10 @@ leqqCong :: n :=: m -> l :=: z -> (n TL.<=? l) :~: (m TL.<=? z) leqqCong Refl Refl = Refl -leqCong :: n :=: m -> l :=: z -> (n PN.:<<= l) :~: (m PN.:<<= z)+leqCong :: n :=: m -> l :=: z -> (n :<= l) :~: (m :<= z) leqCong Refl Refl = Refl -fromPeanoMonotone :: ((n PN.:<<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n TL.<=? FromPeano m) :=: 'True+fromPeanoMonotone :: ((n :<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n TL.<=? FromPeano m) :=: 'True fromPeanoMonotone SZ _ = Refl fromPeanoMonotone (SS n) (SS m) =    start (sFromPeano (SS n) %:<=? sFromPeano (SS m))@@ -250,7 +251,7 @@ natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :=: n natSuccPred _ = Refl -myLeqPred :: Sing n -> Sing m -> ('S n PN.:<<= 'S m) :=: (n PN.:<<= m)+myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :=: (n :<= m) myLeqPred SZ _ = Refl myLeqPred (SS _) (SS _) = Refl myLeqPred (SS _) SZ = Refl@@ -259,7 +260,7 @@ toPeanoCong Refl = Refl  toPeanoMonotone :: (n TL.<= m)-                => Sing n -> Sing m -> ((ToPeano n) PN.:<<= (ToPeano m)) :~: 'True+                => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True toPeanoMonotone sn sm =   case sn %~ (sing :: Sing 0) of     Proved Refl -> Refl@@ -268,13 +269,13 @@       Disproved mPos ->         let pn = sPred sn             pm = sPred sm-        in start (sToPeano sn PN.%:<<= sToPeano sm)-             === (sToPeano (sSucc pn) PN.%:<<= sToPeano (sSucc pm))+        in start (sToPeano sn %:<= sToPeano sm)+             === (sToPeano (sSucc pn) %:<= sToPeano (sSucc pm))                  `because` leqCong (toPeanoCong $ sym $ natSuccPred nPos)                                    (toPeanoCong $ sym $ natSuccPred mPos)-             === (SS (sToPeano pn) PN.%:<<= SS (sToPeano pm))+             === (SS (sToPeano pn) %:<= SS (sToPeano pm))                  `because` leqCong (toPeanoSuccCong pn) (toPeanoSuccCong pm)-             === (sToPeano pn PN.%:<<= sToPeano pm)+             === (sToPeano pn %:<= sToPeano pm)                  `because` myLeqPred (sToPeano pn) (sToPeano pm)              === STrue `because` toPeanoMonotone pn pm 

@@ -8,10 +8,12 @@ import Data.Type.Natural.Compat #endif -import Data.Constraint               hiding ((:-))-import Data.Type.Natural.Definitions hiding ((:<=))-import Prelude                       (Bool (..), Eq (..), Show (..), ($))-import Unsafe.Coerce+import           Data.Constraint               hiding ((:-))+import qualified Data.Singletons.Prelude       as S+import           Data.Type.Natural.Definitions hiding ((:<=))+import           Prelude                       (Bool (..), Eq (..), Show (..),+                                                ($))+import           Unsafe.Coerce  -------------------------------------------------- -- ** Type-level predicate & judgements.@@ -20,15 +22,16 @@ class (n :: Nat) :<= (m :: Nat) instance 'Z :<= n instance (n :<= m) => 'S n :<= 'S m+{-# DEPRECATED (:<=) "This class will be removed in 0.5.0.0. Use @(n 'Data.Singletons.Prelude.Ord.:<=' m) ~ 'True@ instead" #-}  -- | Comparison via GADTs. data Leq (n :: Nat) (m :: Nat) where   ZeroLeq     :: SNat m -> Leq Zero m   SuccLeqSucc :: Leq n m -> Leq ('S n) ('S m) -type LeqTrueInstance a b = Dict ((a :<<= b) ~ 'True)+type LeqTrueInstance a b = Dict ((a S.:<= b) ~ 'True) -(%-) :: (m :<<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m)+(%-) :: (m S.:<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m) n   %- SZ    = n SS n %- SS m = n %- m #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800@@ -52,7 +55,7 @@ propToBoolLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE propToBoolLeq #-} -boolToClassLeq :: (n :<<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq :: (n S.:<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m boolToClassLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE boolToClassLeq #-} @@ -78,7 +81,7 @@  type LeqInstance n m = Dict (n :<= m) -boolToPropLeq :: (n :<<= m) ~ 'True => SNat n -> SNat m -> Leq n m+boolToPropLeq :: (n S.:<= m) ~ 'True => SNat n -> SNat m -> Leq n m boolToPropLeq SZ     m      = ZeroLeq m boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800

@@ -153,9 +153,22 @@  |]  -- | Boolean-valued type-level comparison function.-singletons [d|- (<<=) :: Nat -> Nat -> Bool- Z   <<= _   = True- S _ <<= Z   = False- S n <<= S m = n <<= m- |]+{-# DEPRECATED (<<=) "Use @'Ord'@ instance instead." #-}+(<<=) :: Nat -> Nat -> Bool+(<<=) = (<=)++{-# DEPRECATED (:<<=) "Use @'(:<=)'@ from @'POrd'@ instead." #-}+type n :<<= m = n :<= m++{-# DEPRECATED (%:<<=) "Use @'(%:<=)'@ from @'POrd'@ instead." #-}+(%:<<=) :: SNat n -> SNat m -> SBool (n :<<= m)+(%:<<=) = (%:<=)++type (:<<=$) = (:<=$)+{-# DEPRECATED (:<<=$) "Use @(':<=$')@ instead." #-}++type (:<<=$$) = (:<=$$)+{-# DEPRECATED (:<<=$$) "Use @(':<=$$')@ instead." #-}++type (:<<=$$$) n m = (:<=$$$) n m+{-# DEPRECATED (:<<=$$$) "Use @(':<=$$$')@ instead." #-}

@@ -22,14 +22,15 @@ #endif  import Control.Monad             (liftM)-import Data.Constraint import Data.Singletons.Prelude import Data.Type.Monomorphic import Data.Type.Natural+import Data.Constraint(Dict(..)) import Data.Typeable             (Typeable) import Language.Haskell.TH import Language.Haskell.TH.Quote import Unsafe.Coerce+import qualified Data.Singletons.Prelude as S  -- | Set-theoretic (finite) ordinals: --@@ -92,12 +93,12 @@ unsafeFromInt n =     case (promote n :: Monomorphic (Sing :: Nat -> *)) of       Monomorphic sn ->-           case SS sn %:<<= (sing :: SNat n) of+           case SS sn %:<= (sing :: SNat n) of              STrue -> sNatToOrd' (sing :: SNat n) sn              SFalse -> error "Bound over!"  -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@.-sNatToOrd' :: ('S m :<<= n) ~ 'True => SNat n -> SNat m -> Ordinal n+sNatToOrd' :: ('S m S.:<= n) ~ 'True => SNat n -> SNat m -> Ordinal n sNatToOrd' (SS _) SZ = OZ sNatToOrd' (SS n) (SS m) = OS $ sNatToOrd' n m #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800@@ -105,11 +106,11 @@ #endif  -- | 'sNatToOrd'' with @n@ inferred.-sNatToOrd :: (SingI n, ('S m :<<= n) ~ 'True) => SNat m -> Ordinal n+sNatToOrd :: (SingI n, ('S m S.:<= n) ~ 'True) => SNat m -> Ordinal n sNatToOrd = sNatToOrd' sing  data CastedOrdinal n where-  CastedOrdinal :: ('S m :<<= n) ~ 'True => SNat m -> CastedOrdinal n+  CastedOrdinal :: ('S m S.:<= n) ~ 'True => SNat m -> CastedOrdinal n  -- | Convert @Ordinal n@ into @SNat m@ with the proof of @'S m :<<= n@. ordToSNat' :: Ordinal n -> CastedOrdinal n@@ -134,7 +135,7 @@ ordToInt (OS n) = 1 + ordToInt n  -- | Inclusion function for ordinals.-inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m+inclusion' :: (n S.:<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m inclusion' _ = unsafeCoerce {-# INLINE inclusion' #-} {-@@ -147,7 +148,7 @@ -}  -- | Inclusion function for ordinals with codomain inferred.-inclusion :: ((n :<<= m) ~ 'True) => Ordinal n -> Ordinal m+inclusion :: ((n S.:<= m) ~ 'True) => Ordinal n -> Ordinal m inclusion on = unsafeCoerce on {-# INLINE inclusion #-} 

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                type-natural-version:             0.4.1.1+version:             0.4.2.0 synopsis:            Type-level natural and proofs of their properties. description:         Type-level natural numbers and proofs of their properties. homepage:            https://github.com/konn/type-natural