packages feed

type-natural 1.1.0.1 → 1.2.0.1

raw patch · 7 files changed

+230/−82 lines, 7 filesdep ~ghc-typelits-presburger

Dependency ranges changed: ghc-typelits-presburger

Files

src/Data/Type/Natural/Lemma/Arithmetic.hs view
@@ -16,6 +16,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE NoStarIsType #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}  module Data.Type.Natural.Lemma.Arithmetic
src/Data/Type/Natural/Lemma/Order.hs view
@@ -36,8 +36,12 @@     sMin,     Max,     sMax,+    OrdCond,+    sOrdCond,      -- * Lemmas+    ordCondDistrib,+    leqOrdCond,     sFlipOrdering,     coerceLeqL,     coerceLeqR,@@ -58,6 +62,7 @@     congFlipOrdering,     ltToSuccLeq,     cmpZero,+    cmpSuccZeroGT,     leqToGT,     cmpZero',     zeroNoLT,@@ -118,6 +123,8 @@     lneqSuccStepL,     lneqSuccStepR,     plusStrictMonotone,+    minCase,+    maxCase,     maxZeroL,     maxZeroR,     minZeroL,@@ -162,13 +169,44 @@     (=~=),   ) import Proof.Propositional (IsTrue (..), eliminate, withWitness)+#if MIN_VERSION_ghc(9,2,1)+import qualified Data.Type.Ord as DTO+import Data.Type.Ord (OrdCond)+#endif + --------------------------------------------------  -- ** Type-level predicate & judgements.  -------------------------------------------------- +#if !MIN_VERSION_ghc(9,2,1)+type family OrdCond (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) where+  OrdCond 'LT lt eq gt = lt+  OrdCond 'EQ lt eq gt = eq+  OrdCond 'GT lt eq gt = gt+#endif++sOrdCond :: SOrdering o -> f lt -> f eq -> f gt -> f (OrdCond o lt eq gt)+sOrdCond SLT lt _ _ = lt+sOrdCond SEQ _ eq _ = eq+sOrdCond SGT _ _ gt = gt++minCase :: SNat n -> SNat m -> Either (Min n m :~: n) (Min n m :~: m)+minCase n m =+  case sCmpNat n m of+    SLT -> Left Refl+    SEQ -> Left Refl+    SGT -> Right Refl++maxCase :: SNat n -> SNat m -> Either (Max n m :~: m) (Max n m :~: n)+maxCase n m =+  case sCmpNat n m of+    SLT -> Left Refl+    SEQ -> Left Refl+    SGT -> Right Refl+ -- | Comparison via GADTs. data Leq n m where   ZeroLeq :: SNat m -> Leq 0 m@@ -176,9 +214,10 @@  type LeqWitness n m = IsTrue (n <=? m) +-- | Since 1.2.0 (argument changed) data a :<: b where-  ZeroLtSucc :: 0 :<: (m + 1)-  SuccLtSucc :: n :<: m -> (n + 1) :<: (m + 1)+  ZeroLtSucc :: SNat m -> 0 :<: (m + 1)+  SuccLtSucc :: SNat n -> SNat m -> n :<: m -> (n + 1) :<: (m + 1)  deriving instance Show (a :<: b) @@ -206,16 +245,30 @@ leqLhs (SuccLeqSucc leq) = sSucc $ leqLhs leq  propToBoolLt :: n :<: m -> IsTrue (n <? m)-propToBoolLt ZeroLtSucc = Witness-propToBoolLt (SuccLtSucc lt) =+propToBoolLt (ZeroLtSucc (sm :: SNat m)) = +  gcastWith (cmpZero sm) Witness+propToBoolLt (SuccLtSucc sn sm lt) =+  gcastWith (cmpSucc sn sm) $   withWitness (propToBoolLt lt) Witness  boolToPropLt :: n < m => SNat n -> SNat m -> n :<: m-boolToPropLt Zero (Succ _) = ZeroLtSucc-boolToPropLt (Succ _) Zero = eliminate (Refl :: 0 :~: 1)-boolToPropLt (Succ n) (Succ m) = SuccLtSucc (boolToPropLt n m)+boolToPropLt Zero (Succ sn) = ZeroLtSucc sn+boolToPropLt (Succ n) Zero = eliminate $+  start STrue+  =~= (Succ n %<? Zero)+  =~= sOrdCond (sCmpNat (Succ n) Zero) STrue SFalse SFalse+  === sOrdCond SGT STrue SFalse SFalse+    `because` sOrdCondCong1 (cmpSuccZeroGT n) STrue SFalse SFalse+  =~= SFalse+boolToPropLt (Succ n) (Succ m) = +  gcastWith (cmpSucc n m) $+  SuccLtSucc n m (boolToPropLt n m) -type Min n m = MinAux (n <=? m) n m+#if MIN_VERSION_ghc(9,2,1)+type Min m n = DTO.Min @Nat m n+#else+type Min m n = OrdCond (CmpNat m n) m m n+#endif  sMin :: SNat n -> SNat m -> SNat (Min n m) sMin = coerce $ min @Natural@@ -223,41 +276,87 @@ sMax :: SNat n -> SNat m -> SNat (Max n m) sMax = coerce $ max @Natural -type family MinAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where-  MinAux 'True n _ = n-  MinAux 'False _ m = m--type Max n m = MaxAux (n >=? m) n m--type family MaxAux (p :: Bool) (n :: Nat) (m :: Nat) :: Nat where-  MaxAux 'True n _ = n-  MaxAux 'False _ m = m+#if MIN_VERSION_ghc(9,2,1)+type Max m n = DTO.Max @Nat m n+#else+type Max m n = OrdCond (CmpNat m n) n n m+#endif  infix 4 <?, <, >=?, >=, >, >? -type n <? m = n + 1 <=? m+#if MIN_VERSION_ghc(9,2,1)+type (n :: Nat) <? m = n DTO.<? m+#else+type n <? m = OrdCond (CmpNat n m) 'True 'False 'False+#endif  (%<?) :: SNat n -> SNat m -> SBool (n <? m)-(%<?) = (%<=?) . sSucc+n %<? m = sOrdCond (sCmpNat n m) STrue SFalse SFalse +#if MIN_VERSION_ghc(9,2,2)+type (n :: Nat) < m = n DTO.< m+#else type n < m = (n <? m) ~ 'True+#endif -type n >=? m = m <=? n+#if MIN_VERSION_ghc(9,2,1)+type n >=? m = (DTO.>=?) @Nat n m+#else+type n >=? m = OrdCond (CmpNat n m) 'False 'True 'True+#endif  (%>=?) :: SNat n -> SNat m -> SBool (n >=? m)-(%>=?) = flip (%<=?)+n %>=? m = sOrdCond (sCmpNat n m) SFalse STrue STrue +#if MIN_VERSION_ghc(9,2,1)+type (n :: Nat) >= m = n DTO.>= m+#else type n >= m = (n >=? m) ~ 'True+#endif -type n >? m = m <? n+#if MIN_VERSION_ghc(9,2,1)+type (n :: Nat) >? m = n DTO.>? m+#else+type n >? m = OrdCond (CmpNat n m) 'False 'False 'True+#endif  (%>?) :: SNat n -> SNat m -> SBool (n >? m)-(%>?) = flip (%<?)+n %>? m = sOrdCond (sCmpNat n m) SFalse SFalse STrue +#if MIN_VERSION_ghc(9,2,1)+type (n :: Nat) > m = n DTO.> m+#else type n > m = (n >? m) ~ 'True+#endif  infix 4 %>?, %<?, %>=? +ordCondDistrib :: proxy f -> SOrdering o -> p l -> p' e -> p'' g ->+  OrdCond o (f l) (f e) (f g) :~: f (OrdCond o l e g)+ordCondDistrib _ SLT _ _ _ = Refl+ordCondDistrib _ SEQ _ _ _ = Refl+ordCondDistrib _ SGT _ _ _ = Refl++leqOrdCond+  :: SNat n -> SNat m -> (n <=? m) :~: OrdCond (CmpNat n m) 'True 'True 'False+#if MIN_VERSION_ghc(9,2,1)+leqOrdCond _ _ = Refl+#else+leqOrdCond Zero n =+  case cmpZero' n of+    Left Refl -> Refl+    Right Refl -> Refl+leqOrdCond (Succ m) Zero = +  gcastWith (succLeqZeroAbsurd' m) $+  gcastWith (cmpSuccZeroGT m) $+  Refl+leqOrdCond (Succ m) (Succ n) =+  gcastWith (cmpSucc m n) $+  start (Succ m %<=? Succ n)+  === (m %<=? n) `because` sym (leqSucc' m n)+  === sOrdCond (sCmpNat m n) STrue STrue SFalse `because` leqOrdCond m n+#endif+ data LeqView n m where   LeqZero :: SNat n -> LeqView 0 n   LeqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView (Succ n) (Succ m)@@ -373,6 +472,9 @@ cmpZero :: SNat a -> CmpNat 0 (Succ a) :~: 'LT cmpZero _ = Refl +cmpSuccZeroGT :: SNat a -> CmpNat (Succ a) 0 :~: 'GT+cmpSuccZeroGT _ = Refl+ leqToGT ::   SNat a ->   SNat b ->@@ -480,7 +582,7 @@     step :: SNat x -> LeqWitPf x -> LeqWitPf (Succ x)     step (n :: SNat x) (LeqWitPf ih) = LeqWitPf $ \m snLEQm ->       case viewLeq (sSucc n) m snLEQm of-#if !MIN_VERSION_ghc(9,2,0)+#if !MIN_VERSION_ghc(9,2,0) || MIN_VERSION_ghc(9,4,0)         LeqZero _ -> absurd $ succNonCyclic n Refl #endif         LeqSucc (_ :: SNat n') pm nLEQpm ->@@ -595,13 +697,17 @@ leqSucc' _ _ = Refl  leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n-leqToMin _ _ Witness = Refl+leqToMin n m Witness =+  case leqToCmp n m Witness of+    Left Refl -> Refl+    Right Refl -> Refl  geqToMin :: SNat n -> SNat m -> IsTrue (m <=? n) -> Min n m :~: m geqToMin n m Witness =-  case n %<=? m of-    SFalse -> Refl-    STrue -> Refl+  case leqToCmp m n Witness of+    Left Refl -> Refl+    Right Refl -> +      gcastWith (flipCmpNat m n) Refl  minComm :: SNat n -> SNat m -> Min n m :~: Min m n minComm n m =@@ -642,25 +748,23 @@   IsTrue (l <=? n) ->   IsTrue (l <=? m) ->   IsTrue (l <=? Min n m)-minLargest l n m lLEQn lLEQm =-  withKnownNat l $-    withKnownNat n $-      withKnownNat m $-        withKnownNat (sMin n m) $-          case n %<=? m of-            STrue -> lLEQn-            SFalse -> lLEQm+minLargest _ n m lLEQn lLEQm =+  case minCase n m of+    Left Refl -> lLEQn+    Right Refl -> lLEQm  leqToMax :: SNat n -> SNat m -> IsTrue (n <=? m) -> Max n m :~: m-leqToMax n m Witness =-  case n %>=? m of-    STrue -> Refl-    SFalse -> Refl+leqToMax n m lLeqm =+  case leqToCmp n m lLeqm of+    Left Refl -> Refl+    Right Refl -> Refl  geqToMax :: SNat n -> SNat m -> IsTrue (m <=? n) -> Max n m :~: n geqToMax n m Witness =-  case n %>=? m of-    STrue -> Refl+  case sCmpNat n m of+    SLT -> Refl+    SEQ -> Refl+    SGT -> Refl  maxComm :: SNat n -> SNat m -> Max n m :~: Max m n maxComm n m =@@ -701,36 +805,57 @@   IsTrue (n <=? l) ->   IsTrue (m <=? l) ->   IsTrue (Max n m <=? l)-maxLeast l n m lLEQn lLEQm =-  withKnownNat l $-    withKnownNat n $-      withKnownNat m $-        withKnownNat (sMax n m) $-          case n %>=? m of-            STrue -> lLEQn-            SFalse -> lLEQm+maxLeast _ n m nLEQl mLEQl =+  case maxCase n m of+    Left Refl -> mLEQl+    Right Refl -> nLEQl -lneqSuccLeq :: SNat n -> SNat m -> (n < m) :~: (Succ n <= m)++-- | Since 1.2.0.0 (type changed)+lneqSuccLeq :: SNat n -> SNat m -> (n <? m) :~: (Succ n <=? m)+#if MIN_VERSION_ghc(9,2,1) lneqSuccLeq _ _ = Refl+#else+lneqSuccLeq n m = isTrueRefl (n %<? m) (Succ n %<=? m)+  (ltToSuccLeq n m . lneqToLT n m)+  (ltToLneq n m . succLeqToLT n m) -lneqReversed :: SNat n -> SNat m -> (n < m) :~: (m > n)+isTrueRefl :: SBool a -> SBool b +  -> (IsTrue a -> IsTrue b)+  -> (IsTrue b -> IsTrue a)+  -> a :~: b+isTrueRefl SFalse SFalse _ _ = Refl+isTrueRefl STrue _ f _ = withWitness (f Witness) Refl+isTrueRefl _ STrue _ g = withWitness (g Witness) Refl+#endif++-- | Since 1.2.0.0 (type changed)+lneqReversed :: SNat n -> SNat m -> (n <? m) :~: (m >? n)+#if MIN_VERSION_ghc(9,2,1) lneqReversed _ _ = Refl+#else+lneqReversed n m = +  case sCmpNat n m of+    SLT -> gcastWith (flipCmpNat n m) Refl+    SEQ -> gcastWith (flipCmpNat n m) Refl+    SGT -> gcastWith (flipCmpNat n m) Refl+#endif  lneqToLT ::   SNat n ->   SNat m ->   IsTrue (n <? m) ->   CmpNat n m :~: 'LT-lneqToLT n m nLNEm =-  succLeqToLT n m $ gcastWith (lneqSuccLeq n m) nLNEm+lneqToLT n m Witness =+  case sCmpNat n m of+    SLT -> Refl  ltToLneq ::   SNat n ->   SNat m ->   CmpNat n m :~: 'LT ->   IsTrue (n <? m)-ltToLneq n m nLTm =-  gcastWith (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm+ltToLneq _ _ Refl = Witness  lneqZero :: SNat a -> IsTrue (0 <? Succ a) lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n@@ -742,7 +867,17 @@   SNat n ->   SNat m ->   (n <? m) :~: (Succ n <? Succ m)-succLneqSucc _ _ = Refl+succLneqSucc n m = +  start (n %<? m)+  =~=+  sOrdCond (sCmpNat n m)  STrue SFalse SFalse+  === sOrdCond (sCmpNat (Succ n) (Succ m)) STrue SFalse SFalse +    `because` sOrdCondCong1 (cmpSucc n m) STrue SFalse SFalse+  =~= (Succ n %<? Succ m)++sOrdCondCong1 :: o :~: o' -> proxy a -> proxy' b -> proxy' c +  -> OrdCond o a b c :~: OrdCond o' a b c+sOrdCondCong1 Refl _ _ _ = Refl  lneqRightPredSucc ::   SNat n ->
src/Data/Type/Natural/Presburger/MinMaxSolver.hs view
@@ -48,14 +48,18 @@    singMin <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "Min")   singMax <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "Max")-  caseMinAux <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "MinAux")-  caseMaxAux <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "MaxAux")+#if !MIN_VERSION_ghc(9,2,1)+  ordCondTyCon <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "OrdCond")+#endif   return     mempty       { natGeqBool = [singNatGeq]       , natLtBool = [singNatLt]       , natGtBool = [singNatGt]       , natMin = [singMin]+#if !MIN_VERSION_ghc(9,2,1)+      , ordCond = [ordCondTyCon]+#endif       , natMax = [singMax]       , parsePred = \toE ty ->           case splitTyConApp_maybe ty of@@ -63,13 +67,5 @@               | con == singNatLtProp -> (:<) <$> toE l <*> toE r               | con == singNatGtProp -> (:>) <$> toE l <*> toE r               | con == singNatGeqProp -> (:>=) <$> toE l <*> toE r-            _ -> mzero-      , parseExpr = \toE ty ->-          case splitTyConApp_maybe ty of-            Just (con, [_, n, m])-              | con == caseMinAux ->-                Min <$> toE n <*> toE m-              | con == caseMaxAux ->-                Max <$> toE n <*> toE m             _ -> mzero       }
src/Data/Type/Ordinal.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE EmptyDataDecls #-}@@ -19,8 +20,8 @@ {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}-{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}+{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-}+{-# OPTIONS_GHC -fobject-code #-}  {- | Set-theoretic ordinals for built-in type-level naturals @@ -64,11 +65,13 @@ import Data.Proxy (Proxy (Proxy)) import Data.Type.Equality import Data.Type.Natural-import Data.Type.Natural.Core (SNat (..)) import Data.Typeable (Typeable) import Language.Haskell.TH.Quote-import Numeric.Natural+import Numeric.Natural ( Natural ) import Unsafe.Coerce+import Proof.Propositional (IsTrue (Witness))+import Data.Type.Natural.Lemma.Order (lneqZeroAbsurd)+import Data.Void (absurd)  {- | Set-theoretic (finite) ordinals: @@ -178,16 +181,15 @@ enumOrdinal :: SNat (n :: Nat) -> [Ordinal n] enumOrdinal sn = withKnownNat sn $ map (reallyUnsafeNaturalToOrd Proxy) [0 .. toNatural sn - 1] --- | Since 1.0.0.0(type changed)+-- | Since 1.0.0.0 (type changed) succOrd :: forall (n :: Nat). (KnownNat n) => Ordinal n -> Ordinal (Succ n)-succOrd (OLt n) =-  OLt (sSucc n)+succOrd (OLt k) = OLt (sSucc k) {-# INLINE succOrd #-}  instance (KnownNat n, 0 < n) => Bounded (Ordinal n) where   minBound = OLt sZero -  maxBound = OLt $ sNat @(n - 1)+  maxBound = withKnownNat (sNat @n %- sNat @1) $ OLt $ sNat @(n - 1)  {- | Converts @'Natural'@s into @'Ordinal n'@.    If the given natural is greater or equal to @n@, raises exception.@@ -303,7 +305,7 @@  Since 1.0.0.0 -} absurdOrd :: Ordinal 0 -> a-absurdOrd (OLt _) = case (Refl :: 0 :~: 1) of+absurdOrd (OLt sn) = absurd $ lneqZeroAbsurd sn Witness  {- | @'absurdOrd'@ for value in 'Functor'.
tests/Data/Type/Natural/Lemma/OrderSpec.hs view
@@ -29,7 +29,7 @@ someNat' = toSomeSNat . fromInteger . getNonNegative  data SomeLeqNat where-  MkSomeLeqNat :: n <= m => SNat n -> SNat m -> SomeLeqNat+  MkSomeLeqNat :: (n <=? m) ~ 'True => SNat n -> SNat m -> SomeLeqNat  data SomeLtNat where   MkSomeLtNat ::@@ -40,7 +40,7 @@  data SomeLneqNat where   MkSomeLneqNat ::-    n < m =>+    (n <? m) ~ 'True =>     SNat n ->     SNat m ->     SomeLneqNat@@ -461,6 +461,12 @@         "truncMinusLeq terminates"         $ \(SomeSNat n) (SomeSNat m) ->           totalWitness $ truncMinusLeq n m+    , testProperty @(SomeSNat -> SomeSNat -> Property)+      "leqOrdCond terminates"+      $ \(SomeSNat n) (SomeSNat m) -> totalRefl $ leqOrdCond n m+    , testProperty @(SomeSNat -> Property)+      "cmpSuccZeroGT terminates"+      $ \(SomeSNat n) -> totalRefl $ cmpSuccZeroGT n     ]  totalWitness :: IsTrue p -> Property
tests/Shared.hs view
@@ -8,6 +8,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-}  module Shared where
type-natural.cabal view
@@ -1,12 +1,14 @@ cabal-version: >=1.10 name:          type-natural-version:       1.1.0.1+version:       1.2.0.1 license:       BSD3 license-file:  LICENSE-copyright:     (C) Hiromi ISHII 2013-2014+copyright:     (C) Hiromi ISHII 2013-2022 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.1+tested-with:+  GHC ==8.6.5 || ==8.8.4 || ==8.10.7 || ==9.0.1 || ==9.2.4 || ==9.4.3+ homepage:      https://github.com/konn/type-natural synopsis:      Type-level natural and proofs of their properties. description:@@ -62,9 +64,14 @@     , ghc     , ghc-typelits-knownnat     , ghc-typelits-natnormalise  >=0.4-    , ghc-typelits-presburger    >=0.5.1     , integer-logarithms     , template-haskell           >=2.8++  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