diff --git a/Changelog.md b/Changelog.md new file mode 100644 --- /dev/null +++ b/Changelog.md @@ -0,0 +1,11 @@ +# Changelog + +## 1.3.0.1 + +* Supports GHC 9.8 +* Drops support for GHC <9 + +## 1.3.0.0 + +* Supports GHC 9.6 +* Adds compatibility layer for `SNat` singleton provided since base 4.18 diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs deleted file mode 100644 --- a/Data/Type/Natural.hs +++ /dev/null @@ -1,520 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} -{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-} -{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-} -{-# LANGUAGE TypeOperators, UndecidableInstances, EmptyCase, LambdaCase #-} --- | Type level peano natural number, some arithmetic functions and their singletons. -module Data.Type.Natural (-- * Re-exported modules. - module Data.Singletons, - -- * Natural Numbers - -- | Peano natural numbers. It will be promoted to the type-level natural number. - Nat(..), - SSym0, SSym1, ZSym0, - -- | Singleton type for 'Nat'. - SNat, Sing (SZ, SS), - -- ** Arithmetic functions and their singletons. - min, Min, sMin, max, Max, sMax, - MinSym0, MinSym1, MinSym2, - MaxSym0, MaxSym1, MaxSym2, - (:+:), (:+), - (:+$), (:+$$), (:+$$$), - (%+), (%:+), (:*), (:*:), - (:*$), (:*$$), (:*$$$), - (%:*), (%*), (:-:), (:-), - (:**:), (:**), (%:**), (%**), - (:-$), (:-$$), (:-$$$), - (%:-), (%-), - -- ** Type-level predicate & judgements - Leq(..), (:<=), (:<<=), - (:<<=$),(:<<=$$),(:<<=$$$), - (%:<<=), LeqInstance, - boolToPropLeq, boolToClassLeq, propToClassLeq, - LeqTrueInstance, propToBoolLeq, - -- * Conversion functions - natToInt, intToNat, sNatToInt, - -- * Quasi quotes for natural numbers - nat, snat, - -- * Properties of natural numbers - succCongEq, eqPreservesS, succCong, plusCongR, plusCongL, - succPlusL, plusSuccL, succPlusR, plusSuccR, - plusZR, plusZL, plusAssociative, plusAssoc, - multAssociative, multAssoc, multComm, multZL, multZR, multOneL, - multOneR, snEqZAbsurd, succInjective, succInj, - plusInjectiveL, plusInjectiveR, - plusMultDistr, plusMultDistrib, multPlusDistr, multPlusDistrib, - multCongL, multCongR, - sAndPlusOne, succAndPlusOneR, - plusComm, plusCommutative, minusCongEq, minusCongL, - minusNilpotent, - eqSuccMinus, plusMinusEqL, plusMinusEqR, - zAbsorbsMinR, zAbsorbsMinL, plusSR, plusNeutralR, plusNeutralL, - leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR, - -- * Properties of ordering 'Leq' - leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR, - minLeqL, minLeqR, leqAnitsymmetric, maxLeqL, maxLeqR, - leqSnZAbsurd, leqnZElim, leqSnLeq, leqPred, leqSnnAbsurd, - -- * Useful type synonyms and constructors - zero, one, two, three, four, five, six, seven, eight, nine, ten, eleven, - twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty, - Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten, - Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty, - ZeroSym0, OneSym0, TwoSym0, ThreeSym0, FourSym0, FiveSym0, SixSym0, - SevenSym0, EightSym0, NineSym0, TenSym0, ElevenSym0, TwelveSym0, - ThirteenSym0, FourteenSym0, FifteenSym0, SixteenSym0, SeventeenSym0, - EighteenSym0, NineteenSym0, TwentySym0, - sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven, - sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty, - n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20, - N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20, - - N0Sym0, N1Sym0, N2Sym0, N3Sym0, N4Sym0, N5Sym0, N6Sym0, N7Sym0, N8Sym0, N9Sym0, N10Sym0, N11Sym0, N12Sym0, N13Sym0, N14Sym0, N15Sym0, N16Sym0, N17Sym0, N18Sym0, N19Sym0, N20Sym0, - sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14, - sN15, sN16, sN17, sN18, sN19, sN20 - ) where -import Data.Type.Natural.Compat -import Data.Type.Natural.Core -import Data.Type.Natural.Definitions hiding ((:<=)) - -import Data.Singletons -import qualified Data.Singletons.Prelude as S -import Data.Type.Monomorphic -import Language.Haskell.TH -import Language.Haskell.TH.Quote -import Prelude (Bool (..), Eq (..), Int, - Integral (..), Ord ((<)), error, - otherwise, ($), (.)) -import Prelude (Ord (..)) -import qualified Prelude as P -import Proof.Equational -import Data.Constraint (Dict(..)) - --------------------------------------------------- --- * Conversion functions. --------------------------------------------------- - --- | Convert integral numbers into 'Nat' -intToNat :: (Integral a, Ord a) => a -> Nat -intToNat 0 = Z -intToNat n - | n < 0 = error "negative integer" - | otherwise = S $ intToNat (n P.- 1) - --- | Convert 'Nat' into normal integers. -natToInt :: Integral n => Nat -> n -natToInt Z = 0 -natToInt (S n) = natToInt n P.+ 1 - --- | Convert 'SNat n' into normal integers. -sNatToInt :: P.Num n => SNat x -> n -sNatToInt SZ = 0 -sNatToInt (SS n) = sNatToInt n P.+ 1 - -instance Monomorphicable (Sing :: Nat -> *) where - type MonomorphicRep (Sing :: Nat -> *) = Int - demote (Monomorphic sn) = sNatToInt sn - promote n - | n < 0 = error "negative integer!" - | n == 0 = Monomorphic SZ - | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ SS sn - --------------------------------------------------- --- * Properties --------------------------------------------------- -plusZR :: SNat n -> n :+: 'Z :=: n -plusZR SZ = Refl -plusZR (SS n) = - start (SS n %+ SZ) - =~= SS (n %+ SZ) - === SS n `because` cong' SS (plusZR n) - -plusZL :: SNat n -> 'Z :+: n :=: n -plusZL _ = Refl - -succCong, succCongEq, eqPreservesS :: n :=: m -> 'S n :=: 'S m -succCong Refl = Refl -succCongEq = succCong -{-# DEPRECATED succCongEq "Will be removed in @0.5.0.0@. Use @'succCong'@ instead." #-} -eqPreservesS = succCong -{-# DEPRECATED eqPreservesS "Will be removed in @0.5.0.0@. Use @'succCong'@ instead." #-} - -snEqZAbsurd :: 'S n :=: 'Z -> a -snEqZAbsurd _ = bugInGHC - -succInj, succInjective :: 'S n :=: 'S m -> n :=: m -succInj Refl = Refl -succInjective = succInj -{-# DEPRECATED succInjective "Will be removed in @0.5.0.0@. \ - Use @'succInj'@ instead." #-} - -plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :=: n :+ l -> m :=: l -plusInjectiveL SZ _ _ Refl = Refl -plusInjectiveL (SS n) m l eq = plusInjectiveL n m l $ succInjective eq - -plusInjectiveR :: SNat n -> SNat m -> SNat l -> n :+ l :=: m :+ l -> n :=: m -plusInjectiveR n m l eq = plusInjectiveL l n m $ - start (l %:+ n) - === n %:+ l `because` plusCommutative l n - === m %:+ l `because` eq - === l %:+ m `because` plusCommutative m l - -succAndPlusOneR, sAndPlusOne :: SNat n -> 'S n :=: n :+: One -succAndPlusOneR SZ = Refl -succAndPlusOneR (SS n) = - start (SS (SS n)) - === SS (n %+ sOne) `because` cong' SS (succAndPlusOneR n) - =~= SS n %+ sOne -sAndPlusOne = succAndPlusOneR -{-# DEPRECATED sAndPlusOne "Will be removed in @0.5.0.0@. Use @'succAndPlusOneR'@ instead." #-} - -plusAssoc, plusAssociative :: SNat n -> SNat m -> SNat l - -> n :+: (m :+: l) :=: (n :+: m) :+: l -plusAssoc SZ _ _ = Refl -plusAssoc (SS n) m l = - start (SS n %+ (m %+ l)) - =~= SS (n %+ (m %+ l)) - === SS ((n %+ m) %+ l) `because` cong' SS (plusAssoc n m l) - =~= SS (n %+ m) %+ l - =~= (SS n %+ m) %+ l -plusAssociative = plusAssoc -{-# DEPRECATED plusAssociative "Will be removed in @0.5.0.0@. Use @'plusAssoc'@ instead." #-} - -plusSR :: SNat n -> SNat m -> 'S (n :+: m) :=: n :+: 'S m -plusSR n m = - start (SS (n %+ m)) - === (n %+ m) %+ sOne `because` succAndPlusOneR (n %+ m) - === n %+ (m %+ sOne) `because` symmetry (plusAssoc n m sOne) - === n %+ SS m `because` plusCongL n (symmetry $ succAndPlusOneR m) - -{-# DEPRECATED plusSR "Will be removed in @0.5.0.0@. Use @'plusSuccR'@ instead." #-} - - -plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m' -plusCongL _ Refl = Refl - -plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n -plusCongR _ Refl = Refl - -plusSuccL, succPlusL :: SNat n -> SNat m -> 'S n :+ m :=: 'S (n :+ m) -plusSuccL _ _ = Refl -succPlusL = plusSuccL -{-# DEPRECATED succPlusL "Will be removed in @0.5.0.0@. Use @'plusSuccL'@ instead." #-} - -plusSuccR, succPlusR :: SNat n -> SNat m -> n :+ 'S m :=: 'S (n :+ m) -plusSuccR SZ _ = Refl -plusSuccR (SS n) m = - start (SS n %+ SS m) - =~= SS (n %+ SS m) - === SS (SS (n %+ m)) `because` succCong (plusSuccR n m) - =~= SS (SS n %+ m) - -succPlusR = plusSuccR - -{-# DEPRECATED succPlusR "Will be removed in @0.5.0.0@. Use @'plusSuccR'@ instead." #-} - - -minusCongEq, minusCongL :: n :=: m -> SNat l -> n :-: l :=: m :-: l -minusCongL Refl _ = Refl -minusCongEq = minusCongL -{-# DEPRECATED minusCongEq "Will be removed in @0.5.0.0@. Use @'minusCongL'@ instead." #-} - -minusNilpotent :: SNat n -> n :-: n :=: Zero -minusNilpotent SZ = Refl -minusNilpotent (SS n) = - start (SS n %:- SS n) - =~= n %:- n - === SZ `because` minusNilpotent n - - -plusComm, plusCommutative :: SNat n -> SNat m -> n :+: m :=: m :+: n -plusComm SZ SZ = Refl -plusComm SZ (SS m) = - start (SZ %+ SS m) - =~= SS m - === SS (m %+ SZ) `because` cong' SS (plusCommutative SZ m) - =~= SS m %+ SZ -plusComm (SS n) m = - start (SS n %+ m) - =~= SS (n %+ m) - === SS (m %+ n) `because` cong' SS (plusCommutative n m) - === (m %+ n) %+ sOne `because` succAndPlusOneR (m %+ n) - === m %+ (n %+ sOne) `because` symmetry (plusAssoc m n sOne) - === m %+ SS n `because` plusCongL m (symmetry $ succAndPlusOneR n) - -plusCommutative = plusComm -{-# DEPRECATED plusCommutative "Will be removed in @0.5.0.0@. Use @'plusComm'@ instead." #-} - -eqSuccMinus :: ((m S.:<= n) ~ 'True) - => SNat n -> SNat m -> ('S n :-: m) :=: ('S (n :-: m)) -eqSuccMinus _ SZ = Refl -eqSuccMinus (SS n) (SS m) = - start (SS (SS n) %:- SS m) - =~= SS n %:- m - === SS (n %:- m) `because` eqSuccMinus n m - =~= SS (SS n %:- SS m) -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -eqSuccMinus _ _ = bugInGHC -#endif - - -plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n -plusMinusEqL SZ m = minusNilpotent m -plusMinusEqL (SS n) m = - case propToBoolLeq (plusLeqR n m) of - Dict -> transitivity (eqSuccMinus (n %+ m) m) (succCong $ plusMinusEqL n m) - -plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n -plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m) - -zAbsorbsMinR :: SNat n -> Min n 'Z :=: 'Z -zAbsorbsMinR SZ = Refl -zAbsorbsMinR (SS n) = - case zAbsorbsMinR n of - Refl -> Refl - -zAbsorbsMinL :: SNat n -> Min 'Z n :=: 'Z -zAbsorbsMinL SZ = Refl -zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl - -minComm :: SNat n -> SNat m -> Min n m :=: Min m n -minComm SZ SZ = Refl -minComm SZ (SS _) = Refl -minComm (SS _) SZ = Refl -minComm (SS n) (SS m) = case minComm n m of Refl -> Refl - -maxZL :: SNat n -> Max 'Z n :=: n -maxZL SZ = Refl -maxZL (SS _) = Refl - -maxComm :: SNat n -> SNat m -> (Max n m) :=: (Max m n) -maxComm SZ SZ = Refl -maxComm SZ (SS _) = Refl -maxComm (SS _) SZ = Refl -maxComm (SS n) (SS m) = case maxComm n m of Refl -> Refl - -maxZR :: SNat n -> Max n 'Z :=: n -maxZR n = transitivity (maxComm n SZ) (maxZL n) - -multPlusDistr, multPlusDistrib :: forall n m l. SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: (n :* m) :+ (n :* l) -multPlusDistrib SZ _ _ = Refl -multPlusDistrib (SS (n :: SNat n')) m l = - start (SS n %* (m %+ l)) - =~= (n %* (m %+ l)) %+ (m %+ l) - === ((n %* m) %+ (n %* l)) %+ (m %+ l) - `because` plusCongR (m %+ l) (multPlusDistrib n m l :: n' :* (m :+ l) :=: (n' :* m) :+ (n' :* l)) - === (n %* m) %+ (n %* l) %+ (l %+ m) `because` plusCongL ((n %* m) %+ (n %* l)) (plusCommutative m l) - === n %* m %+ (n %*l %+ (l %+ m)) `because` symmetry (plusAssoc (n %* m) (n %* l) (l %+ m)) - === n %* l %+ (l %+ m) %+ n %* m `because` plusCommutative (n %* m) (n %*l %+ (l %+ m)) - === (n %* l %+ l) %+ m %+ n %* m `because` plusCongR (n %* m) (plusAssoc (n %* l) l m) - =~= (SS n %* l) %+ m %+ n %* m - === (SS n %* l) %+ (m %+ (n %* m)) `because` symmetry (plusAssoc (SS n %* l) m (n %* m)) - === (SS n %* l) %+ ((n %* m) %+ m) `because` plusCongL (SS n %* l) (plusCommutative m (n %* m)) - =~= (SS n %* l) %+ (SS n %* m) - === (SS n %* m) %+ (SS n %* l) `because` plusCommutative (SS n %* l) (SS n %* m) -multPlusDistr = multPlusDistrib -{-# DEPRECATED multPlusDistr "Will be removed in @0.5.0.0@. Use @'multPlusDistrib'@ instead." #-} - -plusMultDistr, plusMultDistrib :: SNat n -> SNat m -> SNat l -> (n :+ m) :* l :=: (n :* l) :+ (m :* l) -plusMultDistrib SZ _ _ = Refl -plusMultDistrib (SS n) m l = - start ((SS n %+ m) %* l) - =~= SS (n %+ m) %* l - =~= (n %+ m) %* l %+ l - === n %* l %+ m %* l %+ l `because` plusCongR l (plusMultDistrib n m l) - === m %* l %+ n %* l %+ l `because` plusCongR l (plusCommutative (n %* l) (m %* l)) - === m %* l %+ (n %* l %+ l) `because` symmetry (plusAssoc (m %* l) (n %*l) l) - =~= m %* l %+ (SS n %* l) - === (SS n %* l) %+ (m %* l) `because` plusCommutative (m %* l) (SS n %* l) - -plusMultDistr = plusMultDistrib -{-# DEPRECATED plusMultDistr "Will be removed in @0.5.0.0@. Use @'plusMultDistrib'@ instead." #-} - -multAssoc, multAssociative :: SNat n -> SNat m -> SNat l -> n :* (m :* l) :=: (n :* m) :* l -multAssoc SZ _ _ = Refl -multAssoc (SS n) m l = - start (SS n %* (m %* l)) - =~= n %* (m %* l) %+ (m %* l) - === (n %* m) %* l %+ (m %* l) `because` plusCongR (m %* l) (multAssoc n m l) - === (n %* m %+ m) %* l `because` symmetry (plusMultDistrib (n %* m) m l) - =~= (SS n %* m) %* l -multAssociative = multAssoc -{-# DEPRECATED multAssociative "Will be removed in @0.5.0.0@. Use @'multAssoc'@ instead." #-} -multZL :: SNat m -> Zero :* m :=: Zero -multZL _ = Refl - -multZR :: SNat m -> m :* Zero :=: Zero -multZR SZ = Refl -multZR (SS n) = - start (SS n %* SZ) - =~= n %* SZ %+ SZ - === SZ %+ SZ `because` plusCongR SZ (multZR n) - =~= SZ - -multOneL :: SNat n -> One :* n :=: n -multOneL n = - start (sOne %* n) - =~= sZero %* n %+ n - =~= sZero %:+ n - =~= n - -multOneR :: SNat n -> n :* One :=: n -multOneR SZ = Refl -multOneR (SS n) = - start (SS n %* sOne) - =~= n %* sOne %+ sOne - === n %+ sOne `because` plusCongR sOne (multOneR n) - === SS n `because` symmetry (succAndPlusOneR n) - -multCongL :: SNat n -> m :=: l -> n :* m :=: n :* l -multCongL _ Refl = Refl - -multCongR :: SNat n -> m :=: l -> m :* n :=: l :* n -multCongR _ Refl = Refl - -multComm :: SNat n -> SNat m -> n :* m :=: m :* n -multComm SZ m = - start (SZ %* m) - =~= SZ - === m %* SZ `because` symmetry (multZR m) -multComm (SS n) m = - start (SS n %* m) - =~= n %* m %+ m - === m %* n %+ m `because` plusCongR m (multComm n m) - === m %* n %+ m %* sOne `because` plusCongL (m %* n) (symmetry $ multOneR m) - === m %* (n %+ sOne) `because` symmetry (multPlusDistrib m n sOne) - === m %* SS n `because` multCongL m (symmetry $ succAndPlusOneR n) - -plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: 'Z -plusNeutralR SZ m eq = - start m - =~= SZ %:+ m - === SZ `because` eq -plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq - -plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: 'Z -plusNeutralL n m eq = plusNeutralR m n $ - start (m %:+ n) - === n %:+ m `because` plusCommutative m n - === m `because` eq - --------------------------------------------------- --- * Properties of 'Leq' --------------------------------------------------- - -leqRefl :: SNat n -> Leq n n -leqRefl SZ = ZeroLeq SZ -leqRefl (SS n) = SuccLeqSucc $ leqRefl n - -leqSucc :: SNat n -> Leq n ('S n) -leqSucc SZ = ZeroLeq sOne -leqSucc (SS n) = SuccLeqSucc $ leqSucc n - -leqTrans :: Leq n m -> Leq m l -> Leq n l -leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq -leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -leqTrans _ _ = error "impossible!" -#endif - -instance Preorder Leq where - reflexivity = leqRefl - transitivity = leqTrans - -plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k) -plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k) -plusMonotone (ZeroLeq m) (SuccLeqSucc leq) = - case sym $ plusSuccR m (leqRhs leq) of - Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq -plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq' - -plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m) -plusLeqL SZ m = ZeroLeq $ coerce (symmetry $ plusZL m) m -plusLeqL (SS n) m = - start (SS n) - =<= SS (n %+ m) `because` SuccLeqSucc (plusLeqL n m) - =~= SS n %+ m - -plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m) -plusLeqR n m = - case plusCommutative n m of - Refl -> plusLeqL m n - -minLeqL :: SNat n -> SNat m -> Leq (Min n m) n -minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq SZ -minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n -minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m) - -minLeqR :: SNat n -> SNat m -> Leq (Min n m) m -minLeqR n m = case minComm n m of Refl -> minLeqL m n - -leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m -leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl -leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = succCong $ leqAnitsymmetric leq1 leq2 -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -leqAnitsymmetric _ _ = error "impossible!" -#endif - -maxLeqL :: SNat n -> SNat m -> Leq n (Max n m) -maxLeqL SZ m = ZeroLeq (sMax SZ m) -maxLeqL n SZ = case maxZR n of - Refl -> leqRefl n -maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m - -maxLeqR :: SNat n -> SNat m -> Leq m (Max n m) -maxLeqR n m = case maxComm n m of - Refl -> maxLeqL m n - -leqSnZAbsurd :: Leq ('S n) 'Z -> a -leqSnZAbsurd = \case {} - -leqnZElim :: Leq n 'Z -> n :=: 'Z -leqnZElim (ZeroLeq SZ) = Refl - -leqSnLeq :: Leq ('S n) m -> Leq n m -leqSnLeq (SuccLeqSucc leq) = - let n = leqLhs leq - m = SS $ leqRhs leq - in start n - =<= SS n `because` leqSucc n - =<= m `because` SuccLeqSucc leq -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -leqSnLeq _ = bugInGHC -#endif - -leqPred :: Leq ('S n) ('S m) -> Leq n m -leqPred (SuccLeqSucc leq) = leq -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -leqPred _ = bugInGHC -#endif - -leqSnnAbsurd :: Leq ('S n) n -> a -leqSnnAbsurd (SuccLeqSucc leq) = - case leqLhs leq of - SS _ -> leqSnnAbsurd leq -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 - _ -> bugInGHC "cannot be occured" -leqSnnAbsurd _ = bugInGHC -#endif - --------------------------------------------------- --- * Quasi Quoter --------------------------------------------------- - --- | Quotesi-quoter for 'Nat'. This can be used for an expression, pattern and type. --- --- for example: @sing :: SNat ([nat| 2 |] :+ [nat| 5 |])@ -nat :: QuasiQuoter -nat = QuasiQuoter { quoteExp = P.foldr appE (conE 'Z) . P.flip P.replicate (conE 'S) . P.read - , quotePat = P.foldr (\a b -> conP a [b]) (conP 'Z []) . P.flip P.replicate 'S . P.read - , quoteType = P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read - , quoteDec = error "not implemented" - } - --- | Quotesi-quoter for 'SNat'. This can be used for an expression, pattern and type. --- --- For example: @[snat|12|] '%+' [snat| 5 |]@, @'sing' :: [snat| 12 |]@, @f [snat| 12 |] = \"hey\"@ -snat :: QuasiQuoter -snat = QuasiQuoter { quoteExp = P.foldr appE (conE 'SZ) . P.flip P.replicate (conE 'SS) . P.read - , quotePat = P.foldr (\a b -> conP a [b]) (conP 'SZ []) . P.flip P.replicate 'SS . P.read - , quoteType = appT (conT ''SNat) . P.foldr appT (conT 'Z) . P.flip P.replicate (conT 'S) . P.read - , quoteDec = error "not implemented" - } diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs deleted file mode 100644 --- a/Data/Type/Natural/Builtin.hs +++ /dev/null @@ -1,329 +0,0 @@ -{-# LANGUAGE ConstraintKinds, CPP, DataKinds, GADTs, PolyKinds, RankNTypes #-} -{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} -{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} --- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@ -module Data.Type.Natural.Builtin - ( -- * Sysnonym to avoid confusion - Peano, - -- * Coercion between builtin type-level natural and peano numerals - FromPeano, ToPeano, sFromPeano, sToPeano, - -- * Properties of @'FromPeano'@ and @'ToPeano'@. - fromPeanoInjective, toPeanoInjective, - -- ** Bijection - fromToPeano, toFromPeano, - -- ** Algebraic isomorphisms - fromPeanoZeroCong, toPeanoZeroCong, - fromPeanoOneCong, toPeanoOneCong, - fromPeanoSuccCong, toPeanoSuccCong, - fromPeanoPlusCong, toPeanoPlusCong, - fromPeanoMultCong, toPeanoMultCong, - fromPeanoMonotone, toPeanoMonotone, - -- * Peano and commutative ring axioms for built-in @'GHC.TypeLits.Nat'@ - plusZR, plusZL, plusSuccR, plusSuccL, - multZR, multZL, multSuccR, multSuccL, - inductionNat, - plusComm, multComm, plusAssoc, multAssoc, - plusMultDistr, multPlusDistr - ) - where -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -import Data.Type.Natural.Compat -#endif - -import Data.Promotion.Prelude.Enum (Succ) -import Data.Singletons (Sing, SingI, sing) -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)) -import Data.Type.Natural (plusCongR) -import qualified Data.Type.Natural as PN -import Data.Void (absurd) -import qualified GHC.TypeLits as TL -import Proof.Equational ((:=:), (:~:) (Refl), coerce) -import Proof.Equational (start, sym, (===), (=~=)) -import Proof.Equational (because) -import Unsafe.Coerce (unsafeCoerce) - --- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@. -type Peano = PN.Nat - -type family FromPeano (n :: PN.Nat) :: TL.Nat where - FromPeano 'Z = 0 - FromPeano ('S n) = Succ (FromPeano n) - -type family ToPeano (n :: TL.Nat) :: PN.Nat where - ToPeano 0 = 'Z - ToPeano n = 'S (ToPeano (Pred n)) - -data NatView (n :: TL.Nat) where - IsZero :: NatView 0 - IsSucc :: Sing n -> NatView (Succ n) - -viewNat :: Sing n -> NatView n -viewNat n = - case n %~ (sing :: Sing 0) of - Proved Refl -> IsZero - Disproved _ -> IsSucc (sPred n) - -sFromPeano :: Sing n -> Sing (FromPeano n) -sFromPeano SZ = sing -sFromPeano (SS sn) = sSucc (sFromPeano sn) - -toPeanoInjective :: ToPeano n :=: ToPeano m -> n :=: m -toPeanoInjective Refl = Refl - --- trustMe :: a :=: b --- trustMe = unsafeCoerce (Refl :: () :=: ()) --- {-# WARNING trustMe --- "Used unproven type-equalities; This may cause disastrous result..." #-} - -toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :=: 'S (ToPeano n) -toPeanoSuccCong _ = unsafeCoerce (Refl :: () :=: ()) - -- We cannot prove this lemma within Haskell, so we assume it a priori. - -sToPeano :: Sing n -> Sing (ToPeano n) -sToPeano sn = - case sn %~ (sing :: Sing 0) of - Proved Refl -> SZ - Disproved _pf -> coerce (sym (toPeanoSuccCong (sPred sn))) (SS (sToPeano (sPred sn))) - --- litSuccInjective :: forall (n :: TL.Nat) (m :: TL.Nat). --- Succ n :=: Succ m -> n :=: m --- litSuccInjective Refl = Refl - -toFromPeano :: Sing n -> ToPeano (FromPeano n) :=: n -toFromPeano SZ = Refl -toFromPeano (SS sn) = - start (sToPeano (sFromPeano (SS sn))) - =~= sToPeano (sSucc (sFromPeano sn)) - === SS (sToPeano (sFromPeano sn)) `because` toPeanoSuccCong (sFromPeano sn) - === SS sn `because` PN.succCong (toFromPeano sn) - -congFromPeano :: n :=: m -> FromPeano n :=: FromPeano m -congFromPeano Refl = Refl - -congToPeano :: n :=: m -> ToPeano n :=: ToPeano m -congToPeano Refl = Refl - -congSucc :: n :=: m -> Succ n :=: Succ m -congSucc Refl = Refl - -fromToPeano :: Sing n -> FromPeano (ToPeano n) :=: n -fromToPeano sn = - case viewNat sn of - IsZero -> Refl - IsSucc n1 -> - start (sFromPeano (sToPeano sn)) - =~= sFromPeano (sToPeano (sSucc n1)) - === sFromPeano (SS (sToPeano n1)) - `because` congFromPeano (toPeanoSuccCong n1) - =~= sSucc (sFromPeano (sToPeano n1)) - === sSucc n1 `because` congSucc (fromToPeano n1) - -fromPeanoInjective :: forall n m. (SingI n, SingI m) - => FromPeano n :=: FromPeano m -> n :=: m -fromPeanoInjective frEq = - let sn = sing :: Sing n - sm = sing :: Sing m - in start sn - === sToPeano (sFromPeano sn) `because` sym (toFromPeano sn) - === sToPeano (sFromPeano sm) `because` congToPeano frEq - === sm `because` toFromPeano sm - -fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :=: Succ (FromPeano n) -fromPeanoSuccCong _sn = Refl - -fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.:+ m) :=: FromPeano n TL.+ FromPeano m -fromPeanoPlusCong SZ _ = Refl -fromPeanoPlusCong (SS sn) sm = - start (sFromPeano (SS sn %:+ sm)) - =~= sFromPeano (SS (sn %:+ sm)) - === sSucc (sFromPeano (sn %:+ sm)) `because` fromPeanoSuccCong (sn %:+ sm) - === sSucc (sFromPeano sn %:+ sFromPeano sm) `because` congSucc (fromPeanoPlusCong sn sm) - =~= sSucc (sFromPeano sn) %:+ sFromPeano sm - =~= sFromPeano (SS sn) %:+ sFromPeano sm - -toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n TL.+ m) :=: ToPeano n PN.:+ ToPeano m -toPeanoPlusCong sn sm = - case viewNat sn of - IsZero -> Refl - IsSucc pn -> - start (sToPeano (sSucc pn %:+ sm)) - =~= sToPeano (sSucc (pn %:+ sm)) - === SS (sToPeano (pn %:+ sm)) - `because` toPeanoSuccCong (pn %:+ sm) - === SS (sToPeano pn %:+ sToPeano sm) - `because` PN.succCong (toPeanoPlusCong pn sm) - =~= SS (sToPeano pn) %:+ sToPeano sm - === (sToPeano (sSucc pn) %:+ sToPeano sm) - `because` plusCongR (sToPeano sm) (sym (toPeanoSuccCong pn)) - =~= sToPeano sn %:+ sToPeano sm - -fromPeanoZeroCong :: FromPeano 'Z :=: 0 -fromPeanoZeroCong = Refl - -toPeanoZeroCong :: ToPeano 0 :=: 'Z -toPeanoZeroCong = Refl - -fromPeanoOneCong :: FromPeano PN.One :=: 1 -fromPeanoOneCong = Refl - -toPeanoOneCong :: ToPeano 1 :=: PN.One -toPeanoOneCong = Refl - -natPlusCongR :: Sing r -> n :=: m -> n TL.+ r :=: m TL.+ r -natPlusCongR _ Refl = Refl - -fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.:* m) :=: FromPeano n TL.* FromPeano m -fromPeanoMultCong SZ _ = Refl -fromPeanoMultCong (SS psn) sm = - start (sFromPeano (SS psn %:* sm)) - =~= sFromPeano (psn %:* sm %:+ sm) - === sFromPeano (psn %:* sm) %:+ sFromPeano sm - `because` fromPeanoPlusCong (psn %:* sm) sm - === sFromPeano psn %:* sFromPeano sm %:+ sFromPeano sm - `because` natPlusCongR (sFromPeano sm) (fromPeanoMultCong psn sm) - =~= sSucc (sFromPeano psn) %:* sFromPeano sm - =~= sFromPeano (SS psn) %:* sFromPeano sm - - -toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n PN.:* m) :=: ToPeano n PN.:* ToPeano m -toPeanoMultCong sn sm = - case viewNat sn of - IsZero -> Refl - IsSucc psn -> - start (sToPeano (sSucc psn %:* sm)) - =~= sToPeano (psn %:* sm %:+ sm) - === sToPeano (psn %:* sm) %:+ sToPeano sm - `because` toPeanoPlusCong (psn %:* sm) sm - === sToPeano psn %:* sToPeano sm %:+ sToPeano sm - `because` plusCongR (sToPeano sm) (toPeanoMultCong psn sm) - =~= SS (sToPeano psn) %:* sToPeano sm - === sToPeano (sSucc psn) %:* sToPeano sm - `because` PN.multCongR (sToPeano sm) (sym (toPeanoSuccCong psn)) - -infix 4 %:<=? -(%:<=?) :: Sing n -> Sing m -> Sing (n TL.<=? m) -sn %:<=? sm = - case viewNat sn of - IsZero -> STrue - IsSucc pn -> case viewNat sm of - IsZero -> SFalse - IsSucc pm -> - case pn %:<=? pm of - STrue -> STrue - SFalse -> SFalse - -natLeqSuccEq :: Sing n -> Sing m -> ((n TL.+ 1) TL.<=? (m TL.+ 1)) :~: (n TL.<=? m) -natLeqSuccEq _ _ = Refl - -leqqCong :: n :=: m -> l :=: z -> (n TL.<=? l) :~: (m TL.<=? z) -leqqCong Refl Refl = Refl - -leqCong :: n :=: m -> l :=: z -> (n :<= l) :~: (m :<= z) -leqCong Refl Refl = Refl - -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)) - === (sSucc (sFromPeano n) %:<=? sSucc (sFromPeano m)) - `because` leqqCong (fromPeanoSuccCong n) (fromPeanoSuccCong m) - === (sFromPeano n %:<=? sFromPeano m) - `because` natLeqSuccEq (sFromPeano n) (sFromPeano m) - === STrue - `because` fromPeanoMonotone n m -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -fromPeanoMonotone _ _ = bugInGHC -#endif - -natLeqZero :: (n TL.<= 0) => Sing n -> n :~: 0 -natLeqZero _ = Refl - --- | Currently, ghc-typelits-natnormalise reduces @(0 - 1) + 1@ to @0@, --- which is contradictory to current GHC's behaviour. --- So our assumption @((n :~: 0) -> Void)@ is simply disregarded. -natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :=: n -natSuccPred _ = Refl - -myLeqPred :: Sing n -> Sing m -> ('S n :<= 'S m) :=: (n :<= m) -myLeqPred SZ _ = Refl -myLeqPred (SS _) (SS _) = Refl -myLeqPred (SS _) SZ = Refl - -toPeanoCong :: a :=: b -> ToPeano a :=: ToPeano b -toPeanoCong Refl = Refl - -toPeanoMonotone :: (n TL.<= m) - => Sing n -> Sing m -> ((ToPeano n) :<= (ToPeano m)) :~: 'True -toPeanoMonotone sn sm = - case sn %~ (sing :: Sing 0) of - Proved Refl -> Refl - Disproved nPos -> case sm %~ (sing :: Sing 0) of - Proved Refl -> absurd $ nPos $ natLeqZero sm - Disproved mPos -> - let pn = sPred sn - pm = sPred sm - 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) %:<= SS (sToPeano pm)) - `because` leqCong (toPeanoSuccCong pn) (toPeanoSuccCong pm) - === (sToPeano pn %:<= sToPeano pm) - `because` myLeqPred (sToPeano pn) (sToPeano pm) - === STrue `because` toPeanoMonotone pn pm - --- | Induction scheme for built-in @'TL.Nat'@. -inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m TL.+ 1)) -> Sing n -> p n -inductionNat base step snat = - case viewNat snat of - IsZero -> base - IsSucc sl -> step (inductionNat base step sl) - -plusZR :: Sing n -> n TL.+ 0 :~: n -plusZR _ = Refl - -plusZL :: Sing n -> 0 TL.+ n :~: n -plusZL _ = Refl - -plusSuccL :: Sing n -> Sing m -> (Succ n) TL.+ m :~: Succ (n TL.+ m) -plusSuccL _ _ = Refl - -plusSuccR :: Sing n -> Sing m -> n TL.+ (Succ m) :~: Succ (n TL.+ m) -plusSuccR _ _ = Refl - -multZL :: Sing n -> 0 TL.* n :~: 0 -multZL _ = Refl - -multZR :: Sing n -> n TL.* 0 :~: 0 -multZR _ = Refl - -multSuccL :: Sing n -> Sing m -> Succ n TL.* m :~: (n TL.* m) TL.+ m -multSuccL _ _ = Refl - -multSuccR :: Sing n -> Sing m -> n TL.* Succ m :~: (n TL.* m) TL.+ n -multSuccR _ _ = Refl - -plusComm :: Sing n -> Sing m -> (n TL.+ m) :~: (m TL.+ n) -plusComm _ _ = Refl - -multComm :: Sing n -> Sing m -> (n TL.* m) :~: (m TL.* n) -multComm _ _ = Refl - -plusAssoc :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.+ l :~: n TL.+ (m TL.+ l) -plusAssoc _ _ _ = Refl - -multAssoc :: Sing n -> Sing m -> Sing l -> (n TL.* m) TL.* l :~: n TL.* (m TL.* l) -multAssoc _ _ _ = Refl - -plusMultDistr :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.* l :~: n TL.* l TL.+ m TL.* l -plusMultDistr _ _ _ = Refl - -multPlusDistr :: Sing n -> Sing m -> Sing l -> n TL.* (m TL.+ l) :~: n TL.* m TL.+ n TL.* l -multPlusDistr _ _ _ = Refl diff --git a/Data/Type/Natural/Compat.hs b/Data/Type/Natural/Compat.hs deleted file mode 100644 --- a/Data/Type/Natural/Compat.hs +++ /dev/null @@ -1,8 +0,0 @@ -{-# LANGUAGE CPP #-} -module Data.Type.Natural.Compat (bugInGHC) where -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -import Data.Singletons.Prelude (bugInGHC) -#else -bugInGHC :: a -bugInGHC = error "GHC case-analysis error!" -#endif diff --git a/Data/Type/Natural/Core.hs b/Data/Type/Natural/Core.hs deleted file mode 100644 --- a/Data/Type/Natural/Core.hs +++ /dev/null @@ -1,97 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} -{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-} -{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-} -{-# LANGUAGE TypeOperators, UndecidableInstances #-} -module Data.Type.Natural.Core where -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -import Data.Type.Natural.Compat -#endif - -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. --------------------------------------------------- --- | Comparison via type-class. -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 S.:<= b) ~ 'True) - -(%-) :: (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 -_ %- _ = bugInGHC -#endif - -infixl 6 %- -deriving instance Show (SNat n) -deriving instance Eq (SNat n) - -data (a :: Nat) :<: (b :: Nat) where - ZeroLtSucc :: Zero :<: 'S m - SuccLtSucc :: n :<: m -> 'S n :<: 'S m - -deriving instance Show (a :<: b) - --------------------------------------------------- --- * Total orderings on natural numbers. --------------------------------------------------- -propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m -propToBoolLeq _ = unsafeCoerce (Dict :: Dict ()) -{-# INLINE propToBoolLeq #-} - -boolToClassLeq :: (n S.:<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m -boolToClassLeq _ = unsafeCoerce (Dict :: Dict ()) -{-# INLINE boolToClassLeq #-} - -propToClassLeq :: Leq n m -> LeqInstance n m -propToClassLeq _ = unsafeCoerce (Dict :: Dict ()) -{-# INLINE propToClassLeq #-} - -{- --- | Below is the "proof" of the correctness of above: -propToBoolLeq :: Leq n m -> LeqTrueInstance n m -propToBoolLeq (ZeroLeq _) = Dict -propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict - -boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m -boolToClassLeq SZ _ = Dict -boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict -boolToClassLeq _ _ = bugInGHC - -propToClassLeq :: Leq n m -> LeqInstance n m -propToClassLeq (ZeroLeq _) = Dict -propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict --} - -type LeqInstance n m = Dict (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 -boolToPropLeq _ _ = bugInGHC -#endif - -leqRhs :: Leq n m -> SNat m -leqRhs (ZeroLeq m) = m -leqRhs (SuccLeqSucc leq) = SS $ leqRhs leq - -leqLhs :: Leq n m -> SNat n -leqLhs (ZeroLeq _) = SZ -leqLhs (SuccLeqSucc leq) = SS $ leqLhs leq diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs deleted file mode 100644 --- a/Data/Type/Natural/Definitions.hs +++ /dev/null @@ -1,174 +0,0 @@ -{-# LANGUAGE DataKinds, DeriveDataTypeable, FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances, GADTs, InstanceSigs, KindSignatures #-} -{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude, PolyKinds #-} -{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} -module Data.Type.Natural.Definitions - (module Data.Type.Natural.Definitions, - module Data.Singletons.Prelude - ) where -import Data.Singletons.Prelude -import Data.Singletons.TH (singletons) -import Data.Typeable (Typeable) -import Prelude (Num (..), Ord (..)) -import Prelude (Bool (..), Eq (..), Show (..)) -import qualified Prelude as P - - - --------------------------------------------------- --- * Natural numbers and its singleton type --------------------------------------------------- -singletons [d| - data Nat = Z | S Nat - deriving (Show, Eq) - |] - -deriving instance Typeable 'S -deriving instance Typeable 'Z - --------------------------------------------------- --- ** Arithmetic functions. --------------------------------------------------- - -singletons [d| - instance P.Ord Nat where - Z <= _ = True - S _ <= Z = False - S n <= S m = n <= m - - min Z Z = Z - min Z (S _) = Z - min (S _) Z = Z - min (S m) (S n) = S (min m n) - - max Z Z = Z - max Z (S n) = S n - max (S n) Z = S n - max (S n) (S m) = S (max n m) - |] - -singletons [d| - instance P.Num Nat where - Z + n = n - S m + n = S (m + n) - - n - Z = n - S n - S m = n - m - Z - S _ = Z - - Z * _ = Z - S n * m = n * m + m - - abs n = n - - signum Z = Z - signum (S _) = S Z - - fromInteger n = if n == 0 then Z else S (fromInteger (n-1)) - |] - -type n :-: m = n :- m -type n :+: m = n :+ m - -infixl 6 :-:, :+: - -singletons [d| - (**) :: Nat -> Nat -> Nat - _ ** Z = S Z - n ** S m = (n ** m) * n - |] - - --- | Addition for singleton numbers. -(%+) :: SNat n -> SNat m -> SNat (n :+: m) -(%+) = (%:+) -infixl 6 %+ - --- | Type-level multiplication. -type n :*: m = n :* m -infixl 7 :*: - --- | Multiplication for singleton numbers. -(%*) :: SNat n -> SNat m -> SNat (n :*: m) -(%*) = (%:*) -infixl 7 %* - --- | Type-level exponentiation. -type n :**: m = n :** m - --- | Exponentiation for singleton numbers. -(%**) :: SNat n -> SNat m -> SNat (n :**: m) -(%**) = (%:**) - -singletons [d| - zero, one, two, three, four, five, six, seven, eight, nine, ten :: Nat - eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty :: Nat - zero = Z - one = S zero - two = S one - three = S two - four = S three - five = S four - six = S five - seven = S six - eight = S seven - nine = S eight - ten = S nine - eleven = S ten - twelve = S eleven - thirteen = S twelve - fourteen = S thirteen - fifteen = S fourteen - sixteen = S fifteen - seventeen = S sixteen - eighteen = S seventeen - nineteen = S eighteen - twenty = S nineteen - n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat - n10, n11, n12, n13, n14, n15, n16, n17 :: Nat - n18, n19, n20 :: Nat - n0 = zero - n1 = one - n2 = two - n3 = three - n4 = four - n5 = five - n6 = six - n7 = seven - n8 = eight - n9 = nine - n10 = ten - n11 = eleven - n12 = twelve - n13 = thirteen - n14 = fourteen - n15 = fifteen - n16 = sixteen - n17 = seventeen - n18 = eighteen - n19 = nineteen - n20 = twenty - |] - --- | Boolean-valued type-level comparison function. -{-# 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." #-} diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs deleted file mode 100644 --- a/Data/Type/Ordinal.hs +++ /dev/null @@ -1,195 +0,0 @@ -{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase, EmptyDataDecls #-} -{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} -{-# LANGUAGE LambdaCase, PolyKinds, ScopedTypeVariables, StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-} --- | Set-theoretic ordinal arithmetic -module Data.Type.Ordinal - ( -- * Data-types - Ordinal (..), - -- * Conversion from cardinals to ordinals. - sNatToOrd', sNatToOrd, ordToInt, ordToSNat, - ordToSNat', CastedOrdinal(..), - unsafeFromInt, inclusion, inclusion', - -- * Ordinal arithmetics - (@+), enumOrdinal, - -- * Elimination rules for @'Ordinal' 'Z'@. - absurdOrd, vacuousOrd, vacuousOrdM, - -- * Quasi Quoter - od - ) where -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 -import Data.Type.Natural.Compat -#endif - -import Control.Monad (liftM) -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: --- --- > n = {0, 1, ..., n-1} --- --- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. -data Ordinal n where - OZ :: Ordinal ('S n) - OS :: Ordinal n -> Ordinal ('S n) - --- | Since 0.2.3.0 -deriving instance Typeable Ordinal --- | Parsing always fails, because there are no inhabitant. -instance Read (Ordinal 'Z) where - readsPrec _ _ = [] - -instance SingI n => Num (Ordinal n) where - _ + _ = error "Finite ordinal is not closed under addition." - _ - _ = error "Ordinal subtraction is not defined" - negate OZ = OZ - negate _ = error "There are no negative oridnals!" - OZ * _ = OZ - _ * OZ = OZ - _ * _ = error "Finite ordinal is not closed under multiplication" - abs = id - signum = error "What does Ordinal sign mean?" - fromInteger = unsafeFromInt . fromInteger - -deriving instance Read (Ordinal n) => Read (Ordinal ('S n)) -deriving instance Show (Ordinal n) -deriving instance Eq (Ordinal n) -deriving instance Ord (Ordinal n) - -instance SingI n => Enum (Ordinal n) where - fromEnum = ordToInt - toEnum = unsafeFromInt - enumFrom = enumFromOrd - enumFromTo = enumFromToOrd - -enumFromToOrd :: forall n. SingI n => Ordinal n -> Ordinal n -> [Ordinal n] -enumFromToOrd ok ol = - let k = ordToInt ok - l = ordToInt ol - in take (l - k + 1) $ enumFromOrd ok - -enumFromOrd :: forall n. SingI n => Ordinal n -> [Ordinal n] -enumFromOrd ord = drop (ordToInt ord) $ enumOrdinal (sing :: SNat n) - -enumOrdinal :: SNat n -> [Ordinal n] -enumOrdinal SZ = [] -enumOrdinal (SS n) = OZ : map OS (enumOrdinal n) - -instance SingI n => Bounded (Ordinal ('S n)) where - minBound = OZ - maxBound = - case propToBoolLeq $ leqRefl (sing :: SNat n) of - Dict -> sNatToOrd (sing :: SNat n) - -unsafeFromInt :: forall n. SingI n => Int -> Ordinal n -unsafeFromInt n = - case (promote n :: Monomorphic (Sing :: Nat -> *)) of - Monomorphic sn -> - 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 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 -sNatToOrd' _ _ = bugInGHC -#endif - --- | 'sNatToOrd'' with @n@ inferred. -sNatToOrd :: (SingI n, ('S m S.:<= n) ~ 'True) => SNat m -> Ordinal n -sNatToOrd = sNatToOrd' sing - -data CastedOrdinal n where - 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 -ordToSNat' OZ = CastedOrdinal SZ -ordToSNat' (OS on) = - case ordToSNat' on of - CastedOrdinal m -> - CastedOrdinal (SS m) - --- | Convert @Ordinal n@ into monomorphic @SNat@ -ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *) -ordToSNat OZ = Monomorphic SZ -ordToSNat (OS n) = - case ordToSNat n of - Monomorphic sn -> - case singInstance sn of - SingInstance -> Monomorphic (SS sn) - --- | Convert ordinal into @Int@. -ordToInt :: Ordinal n -> Int -ordToInt OZ = 0 -ordToInt (OS n) = 1 + ordToInt n - --- | Inclusion function for ordinals. -inclusion' :: (n S.:<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m -inclusion' _ = unsafeCoerce -{-# INLINE inclusion' #-} -{- --- The "proof" of the correctness of the above -inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m -inclusion' (SS SZ) OZ = OZ -inclusion' (SS (SS _)) OZ = OZ -inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (SS n) m -inclusion' _ _ = bugInGHC --} - --- | Inclusion function for ordinals with codomain inferred. -inclusion :: ((n S.:<= m) ~ 'True) => Ordinal n -> Ordinal m -inclusion on = unsafeCoerce on -{-# INLINE inclusion #-} - --- | Ordinal addition. -(@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m) -OZ @+ n = - let sn = sing :: SNat n - sm = sing :: SNat m - in case propToBoolLeq (plusLeqR sn sm) of - Dict -> inclusion n -OS n @+ m = - case sing :: SNat n of - SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 - _ -> bugInGHC -#endif - --- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. --- --- Since 0.2.3.0 -absurdOrd :: Ordinal 'Z -> a -absurdOrd cs = case cs of {} - --- | 'absurdOrd' for the value in 'Functor'. --- --- Since 0.2.3.0 -vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a -vacuousOrd = fmap absurdOrd - --- | 'absurdOrd' for the value in 'Monad'. --- This function will become uneccesary once 'Applicative' (and hence 'Functor') --- become the superclass of 'Monad'. --- --- Since 0.2.3.0 -vacuousOrdM :: Monad m => m (Ordinal 'Z) -> m a -vacuousOrdM = liftM absurdOrd - --- | Quasiquoter for ordinals -od :: QuasiQuoter -od = QuasiQuoter { quoteExp = foldr appE (conE 'OZ) . flip replicate (conE 'OS) . read - , quoteType = error "No type quoter for Ordinals" - , quotePat = foldr (\a b -> conP a [b]) (conP 'OZ []) . flip replicate 'OS . read - , quoteDec = error "No declaration quoter for Ordinals" - } diff --git a/src/Data/Type/Natural.hs b/src/Data/Type/Natural.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural.hs @@ -0,0 +1,178 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +-- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@ +module Data.Type.Natural + ( -- * Type-level naturals + + -- ** @Nat@, singletons and KnownNat manipulation, + Nat, + KnownNat, + SNat (Succ, Zero), + sNat, + sNatP, + toNatural, + SomeSNat (..), + toSomeSNat, + withSNat, + withKnownNat, + fromSNat, + natVal, + natVal', + someNatVal, + SomeNat (..), + (%~), + Equality (..), + type (===), + + -- *** Pattens and Views + viewNat, + zeroOrSucc, + ZeroOrSucc (..), + + -- ** Promtoed and singletonised operations + + -- *** Arithmetic + Succ, + sSucc, + S, + Pred, + sPred, + sS, + Zero, + sZero, + One, + sOne, + type (+), + (%+), + type (-), + (%-), + type (*), + (%*), + Div, + sDiv, + Mod, + sMod, + type (^), + (%^), + type (-.), + (%-.), + Log2, + sLog2, + + -- *** Ordering + type (<=?), + type (<=), + (%<=?), + type (=?), + type (>=), + (%>=?), + type (>?), + type (>), + (%>?), + CmpNat, + sCmpNat, + sCompare, + Min, + sMin, + Max, + sMax, + induction, + + -- * QuasiQuotes + snat, + + -- * Singletons for auxiliary types + SBool (..), + SOrdering (..), + OrderingI(..), + fromOrderingI, + toOrderingI, + FlipOrdering, + sFlipOrdering, + ) +where + +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 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. + + For example: @[snat|12|] '%+' [snat| 5 |]@. +-} +snat :: QuasiQuoter +snat = + QuasiQuoter + { quoteExp = \str -> + case readMaybe str of + Just n -> [|sNat :: SNat $(litT $ numTyLit n)|] + Nothing -> error "Must be natural literal" + , quotePat = \str -> + case readMaybe str of + Just n -> [p|((%~ (sNat :: SNat $(litT $ numTyLit n))) -> Equal)|] + Nothing -> error "Must be natural literal" + , quoteType = \str -> + case readMaybe str of + Just n -> litT $ numTyLit n + Nothing -> error "Must be natural literal" + , quoteDec = error "No declaration Quotes for Nat" + } + +toNatural :: SNat n -> Natural +{-# DEPRECATED toNatural "Use fromSNat instead" #-} +toNatural = fromSNat + +data SomeSNat where + SomeSNat :: KnownNat n => SNat n -> SomeSNat + +deriving instance Show SomeSNat + +instance Eq SomeSNat where + (==) = (==) `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 + SomeNat pn -> withKnownNat sn $ SomeSNat sn + where + sn = sNatP pn + +withSNat :: Natural -> (forall n. KnownNat n => SNat n -> r) -> r +withSNat n act = case someNatVal n of + SomeNat (pn :: Proxy n) -> withKnownNat sn $ act sn + where + sn = sNatP pn + +sNatP :: KnownNat n => pxy n -> SNat n +sNatP = const sNat diff --git a/src/Data/Type/Natural/Builtin.hs b/src/Data/Type/Natural/Builtin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Builtin.hs @@ -0,0 +1,7 @@ +-- | Since 1.0.0.0 +module Data.Type.Natural.Builtin + {-# DEPRECATED "Use Data.Type.Natural instead" #-} + (module Data.Type.Natural) +where + +import Data.Type.Natural diff --git a/src/Data/Type/Natural/Core.hs b/src/Data/Type/Natural/Core.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Core.hs @@ -0,0 +1,314 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NoStarIsType #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +module Data.Type.Natural.Core + ( SNat (Zero, Succ), +#if !MIN_VERSION_base(4,18,0) + fromSNat, + withKnownNat, + withSomeSNat, +#endif + unsafeLiftSBin, + ZeroOrSucc (..), + viewNat, + sNat, + (%+), + (%-), + (%*), + (%^), + sDiv, + sMod, + sLog2, + (%<=?), + sCmpNat, + sCompare, + Succ, + S, + sSucc, + sS, + Pred, + sPred, + Zero, + One, + sZero, + sOne, + Equality (..), + equalAbsurdFromBool, + type (===), + (%~), + sFlipOrdering, + FlipOrdering, + SOrdering (..), + SBool (..), + Natural, + OrderingI(..), + fromOrderingI, + toOrderingI, + -- Re-exports + module GHC.TypeNats, + ) +where + +import Data.Type.Equality + ( type (:~:) (..), + type (==), + ) +import GHC.TypeNats +import Math.NumberTheory.Logarithms (naturalLog2) +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) = UnsafeSNat Natural + deriving newtype (Show, Eq, Ord) + +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) -> + 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) +{-# INLINE (%+) #-} +(%+) = unsafeLiftSBin (+) + +(%-) :: SNat n -> SNat m -> SNat (n - m) +(%-) = unsafeLiftSBin (-) + +(%*) :: SNat n -> SNat m -> SNat (n * m) +(%*) = unsafeLiftSBin (*) + +sDiv :: SNat n -> SNat m -> SNat (Div n m) +sDiv = unsafeLiftSBin quot + +sMod :: SNat n -> SNat m -> SNat (Mod n m) +sMod = unsafeLiftSBin rem + +(%^) :: SNat n -> SNat m -> SNat (n ^ m) +(%^) = unsafeLiftSBin (^) + +sLog2 :: SNat n -> SNat (Log2 n) +sLog2 = unsafeLiftSUnary $ fromIntegral . naturalLog2 + +sNat :: forall n. KnownNat n => SNat 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 (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 + NonEqual :: + ((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 + +infix 4 ===, %~ + +(%~) :: SNat l -> SNat r -> Equality l r +l %~ r = + if fromSNat l == fromSNat r + then unsafeCoerce (Equal @()) + else unsafeCoerce (NonEqual @0 @1) + +type Zero = 0 + +type One = 1 + +sZero :: SNat 0 +sZero = sNat + +sOne :: SNat 1 +sOne = sNat + +type Succ n = n + 1 + +type S n = Succ n + +sSucc, sS :: SNat n -> SNat (Succ n) +sS = (%+ sOne) +sSucc = sS + +sPred :: SNat n -> SNat (Pred n) +sPred = (%- sOne) + +type Pred n = n - 1 + +data ZeroOrSucc n where + IsZero :: ZeroOrSucc 0 + IsSucc :: + SNat n -> + ZeroOrSucc (n + 1) + +pattern Zero :: forall n. () => n ~ 0 => SNat n +pattern Zero <- + (viewNat -> IsZero) + where + Zero = sZero + +pattern Succ :: forall n. () => forall n1. n ~ Succ n1 => SNat n1 -> SNat n +pattern Succ n <- + (viewNat -> IsSucc n) + where + Succ n = sSucc n + +{-# COMPLETE Zero, Succ #-} + +viewNat :: forall n. SNat n -> ZeroOrSucc n +viewNat n = + case n %~ sNat @0 of + 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 + +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 + +deriving instance Show (SBool ord) + +deriving instance Eq (SBool ord) + +deriving instance Typeable SBool + +infix 4 %<=? + +(%<=?) :: SNat n -> SNat m -> SBool (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 n m = + case compare (fromSNat n) (fromSNat m) of + LT -> unsafeCoerce SLT + EQ -> unsafeCoerce SEQ + GT -> unsafeCoerce SGT + diff --git a/src/Data/Type/Natural/Lemma/Arithmetic.hs b/src/Data/Type/Natural/Lemma/Arithmetic.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Lemma/Arithmetic.hs @@ -0,0 +1,296 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE NoStarIsType #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} + +module Data.Type.Natural.Lemma.Arithmetic + ( Zero, + One, + S, + sZero, + sOne, + ZeroOrSucc (..), + plusCong, + plusCongR, + plusCongL, + predCong, + Succ, + sS, + sSucc, + Pred, + sPred, + sPred', + succCong, + multCong, + multCongL, + multCongR, + minusCong, + minusCongL, + minusCongR, + succOneCong, + succInj, + succInj', + succNonCyclic, + induction, + plusMinus, + plusMinus', + plusZeroL, + plusSuccL, + plusZeroR, + plusSuccR, + plusComm, + plusAssoc, + multZeroL, + multSuccL, + multSuccL', + multZeroR, + multSuccR, + multComm, + multOneR, + multOneL, + plusMultDistrib, + multPlusDistrib, + minusNilpotent, + multAssoc, + plusEqCancelL, + plusEqCancelR, + succAndPlusOneL, + succAndPlusOneR, + predSucc, + viewNat, + zeroOrSucc, + plusEqZeroL, + plusEqZeroR, + predUnique, + multEqSuccElimL, + multEqSuccElimR, + minusZero, + multEqCancelR, + succPred, + multEqCancelL, + pattern Zero, + pattern Succ, + ) +where + +import Data.Type.Equality + ( gcastWith, + (:~:) (..), + ) +import Data.Type.Natural.Core +import Data.Type.Natural.Lemma.Presburger + ( plusEqZeroL, + plusEqZeroR, + succNonCyclic, + ) +import Data.Void (Void, absurd) +import Proof.Equational (because, start, sym, trans, (===)) + +predCong :: n :~: m -> Pred n :~: Pred m +predCong Refl = Refl + +plusCong :: n :~: m -> n' :~: m' -> n + n' :~: m + m' +plusCong Refl Refl = Refl + +plusCongL :: n :~: m -> SNat k -> n + k :~: m + k +plusCongL Refl _ = Refl + +plusCongR :: SNat k -> n :~: m -> k + n :~: k + m +plusCongR _ Refl = Refl + +succCong :: n :~: m -> S n :~: S m +succCong Refl = Refl + +multCong :: n :~: m -> l :~: k -> n * l :~: m * k +multCong Refl Refl = Refl + +multCongL :: n :~: m -> SNat k -> n * k :~: m * k +multCongL Refl _ = Refl + +multCongR :: SNat k -> n :~: m -> k * n :~: k * m +multCongR _ Refl = Refl + +minusCong :: n :~: m -> l :~: k -> n - l :~: m - k +minusCong Refl Refl = Refl + +minusCongL :: n :~: m -> SNat k -> n - k :~: m - k +minusCongL Refl _ = Refl + +minusCongR :: SNat k -> n :~: m -> k - n :~: k - m +minusCongR _ Refl = Refl + +succOneCong :: Succ 0 :~: 1 +succOneCong = Refl + +succInj :: Succ n :~: Succ m -> n :~: m +succInj Refl = Refl + +succInj' :: proxy n -> proxy' m -> Succ n :~: Succ m -> n :~: m +succInj' _ _ = succInj + +induction :: forall p k. p 0 -> (forall n. SNat n -> p n -> p (S n)) -> SNat k -> p k +induction base step = go + where + go :: SNat m -> p m + go sn = case viewNat sn of + IsZero -> base + IsSucc n -> withKnownNat n $ step n (go n) + +plusMinus :: SNat n -> SNat m -> n + m - m :~: n +plusMinus _ _ = Refl + +plusMinus' :: SNat n -> SNat m -> n + m - n :~: m +plusMinus' n m = + start (n %+ m %- n) + === m %+ n %- n `because` minusCongL (plusComm n m) n + === m `because` plusMinus m n + +plusZeroL :: SNat n -> (0 + n) :~: n +plusZeroL _ = Refl + +plusSuccL :: SNat n -> SNat m -> S n + m :~: S (n + m) +plusSuccL _ _ = Refl + +plusZeroR :: SNat n -> (n + 0) :~: n +plusZeroR _ = Refl + +plusSuccR :: SNat n -> SNat m -> n + S m :~: S (n + m) +plusSuccR _ _ = Refl + +plusComm :: SNat n -> SNat m -> n + m :~: m + n +plusComm _ _ = Refl + +plusAssoc :: + forall n m l. + SNat n -> + SNat m -> + SNat l -> + (n + m) + l :~: n + (m + l) +plusAssoc _ _ _ = Refl + +multZeroL :: SNat n -> 0 * n :~: 0 +multZeroL _ = Refl + +multSuccL :: SNat n -> SNat m -> S n * m :~: n * m + m +multSuccL _ _ = Refl + +multSuccL' :: SNat n -> SNat m -> S n * m :~: n * m + 1 * m +multSuccL' _ _ = Refl + +multZeroR :: SNat n -> n * 0 :~: 0 +multZeroR _ = Refl + +multSuccR :: SNat n -> SNat m -> n * S m :~: n * m + n +multSuccR _ _ = Refl + +multComm :: SNat n -> SNat m -> n * m :~: m * n +multComm _ _ = Refl + +multOneR :: SNat n -> n * 1 :~: n +multOneR _ = Refl + +multOneL :: SNat n -> 1 * n :~: n +multOneL _ = Refl + +plusMultDistrib :: + SNat n -> + SNat m -> + SNat l -> + (n + m) * l :~: (n * l) + (m * l) +plusMultDistrib _ _ _ = Refl + +multPlusDistrib :: + SNat n -> + SNat m -> + SNat l -> + n * (m + l) :~: (n * m) + (n * l) +multPlusDistrib _ _ _ = Refl + +minusNilpotent :: SNat n -> n - n :~: 0 +minusNilpotent _ = Refl + +multAssoc :: + SNat n -> + SNat m -> + SNat l -> + (n * m) * l :~: n * (m * l) +multAssoc _ _ _ = Refl + +plusEqCancelL :: SNat n -> SNat m -> SNat l -> n + m :~: n + l -> m :~: l +plusEqCancelL _ _ _ Refl = Refl + +plusEqCancelR :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m + l -> n :~: m +plusEqCancelR n m l nlml = + plusEqCancelL l n m $ + start (l %+ n) + === (n %+ l) `because` plusComm l n + === (m %+ l) `because` nlml + === (l %+ m) `because` plusComm m l + +succAndPlusOneL :: SNat n -> Succ n :~: 1 + n +succAndPlusOneL _ = Refl + +succAndPlusOneR :: SNat n -> Succ n :~: n + 1 +succAndPlusOneR _ = Refl + +predSucc :: SNat n -> Pred (Succ n) :~: n +predSucc _ = Refl + +zeroOrSucc :: SNat n -> ZeroOrSucc n +zeroOrSucc = viewNat + +predUnique :: SNat n -> SNat m -> Succ n :~: m -> n :~: Pred m +predUnique _ _ Refl = Refl + +minusZero :: SNat n -> n - 0 :~: n +minusZero _ = Refl + +multEqCancelR :: forall n m l. SNat n -> SNat m -> SNat l -> n * Succ l :~: m * Succ l -> n :~: m +multEqCancelR _ _ = go + where + go :: forall k. SNat k -> n * Succ k :~: m * Succ k -> n :~: m + go Zero Refl = Refl + go (Succ n) Refl = gcastWith (go n Refl) Refl + +succPred :: SNat n -> (n :~: 0 -> Void) -> Succ (Pred n) :~: n +succPred n nonZero = + case zeroOrSucc n of + IsZero -> absurd $ nonZero Refl + IsSucc n' -> sym $ succCong $ predUnique n' n Refl + +multEqCancelL :: SNat n -> SNat m -> SNat l -> Succ n * m :~: Succ n * l -> m :~: l +multEqCancelL n m l snmEsnl = + multEqCancelR m l n $ + multComm m (sSucc n) `trans` snmEsnl `trans` multComm (sSucc n) l + +sPred' :: proxy n -> SNat (Succ n) -> SNat n +sPred' pxy sn = gcastWith (succInj $ succCong $ predSucc (sPred' pxy sn)) (sPred sn) + +multEqSuccElimL :: + SNat n -> + SNat m -> + SNat l -> + n * m :~: Succ l -> + n :~: Succ (Pred n) +multEqSuccElimL Zero _ l Refl = absurd $ succNonCyclic l Refl +multEqSuccElimL (Succ _) _ _ Refl = Refl + +multEqSuccElimR :: SNat n -> SNat m -> SNat l -> n * m :~: Succ l -> m :~: Succ (Pred m) +multEqSuccElimR _ Zero l Refl = absurd $ succNonCyclic l Refl +multEqSuccElimR _ (Succ _) _ Refl = Refl diff --git a/src/Data/Type/Natural/Lemma/Order.hs b/src/Data/Type/Natural/Lemma/Order.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Lemma/Order.hs @@ -0,0 +1,1004 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +module Data.Type.Natural.Lemma.Order + ( DiffNat (..), + LeqView (..), + type (<), + type (), + type (>?), + (%>?), + type (>=), + type (>=?), + (%>=?), + FlipOrdering, + Min, + sMin, + Max, + sMax, + OrdCond, + sOrdCond, + + -- * Lemmas + ordCondDistrib, + leqOrdCond, + sFlipOrdering, + coerceLeqL, + coerceLeqR, + sLeqCongL, + sLeqCongR, + sLeqCong, + succDiffNat, + compareCongR, + leqToCmp, + eqlCmpEQ, + eqToRefl, + flipCmpNat, + ltToNeq, + leqNeqToLT, + succLeqToLT, + ltToLeq, + gtToLeq, + congFlipOrdering, + ltToSuccLeq, + cmpZero, + cmpSuccZeroGT, + leqToGT, + cmpZero', + zeroNoLT, + ltRightPredSucc, + cmpSucc, + ltSucc, + cmpSuccStepR, + ltSuccLToLT, + leqToLT, + leqZero, + leqSucc, + fromLeqView, + leqViewRefl, + viewLeq, + leqWitness, + leqStep, + leqNeqToSuccLeq, + leqRefl, + leqSuccStepR, + leqSuccStepL, + leqReflexive, + leqTrans, + leqAntisymm, + plusMonotone, + leqZeroElim, + plusMonotoneL, + plusMonotoneR, + plusLeqL, + plusLeqR, + plusCancelLeqR, + plusCancelLeqL, + succLeqZeroAbsurd, + succLeqZeroAbsurd', + succLeqAbsurd, + succLeqAbsurd', + notLeqToLeq, + leqSucc', + leqToMin, + geqToMin, + minComm, + minLeqL, + minLeqR, + minLargest, + leqToMax, + geqToMax, + maxComm, + maxLeqR, + maxLeqL, + maxLeast, + lneqSuccLeq, + lneqReversed, + lneqToLT, + ltToLneq, + lneqZero, + lneqSucc, + succLneqSucc, + lneqRightPredSucc, + lneqSuccStepL, + lneqSuccStepR, + plusStrictMonotone, + minCase, + maxCase, + maxZeroL, + maxZeroR, + minZeroL, + minZeroR, + minusSucc, + lneqZeroAbsurd, + minusPlus, + minPlusTruncMinus, + truncMinusLeq, + type (-.), + (%-.), + + -- * Various witnesses for orderings + LeqWitness, + (:<:), + Leq (..), + leqRhs, + leqLhs, + + -- ** conversions between lax orders + propToBoolLeq, + boolToPropLeq, + + -- ** conversions between strict orders + propToBoolLt, + boolToPropLt, + ) +where + +import Data.Type.Equality (gcastWith, (:~:) (..)) +import Data.Type.Natural.Core +import Data.Type.Natural.Lemma.Arithmetic +import Data.Void (Void, absurd) +import Proof.Equational + ( because, + start, + sym, + trans, + (===), + (=~=), + ) +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 + SuccLeqSucc :: Leq n m -> Leq (n + 1) (m + 1) + +type LeqWitness n m = IsTrue (n <=? m) + +-- | Since 1.2.0 (argument changed) +data a :<: b where + ZeroLtSucc :: SNat m -> 0 :<: (m + 1) + SuccLtSucc :: SNat n -> SNat m -> n :<: m -> (n + 1) :<: (m + 1) + +deriving instance Show (a :<: b) + +-------------------------------------------------- + +-- * Total orderings on natural numbers. + +-------------------------------------------------- +propToBoolLeq :: forall n m. Leq n m -> LeqWitness n m +propToBoolLeq (ZeroLeq _) = Witness +propToBoolLeq (SuccLeqSucc leq) = withWitness (propToBoolLeq leq) Witness +{-# INLINE propToBoolLeq #-} + +boolToPropLeq :: (n <= m) => SNat n -> SNat m -> Leq n m +boolToPropLeq Zero m = ZeroLeq m +boolToPropLeq (Succ n) (Succ m) = SuccLeqSucc $ boolToPropLeq n m +boolToPropLeq (Succ n) Zero = absurd $ succLeqZeroAbsurd n Witness + +leqRhs :: Leq n m -> SNat m +leqRhs (ZeroLeq m) = m +leqRhs (SuccLeqSucc leq) = sSucc $ leqRhs leq + +leqLhs :: Leq n m -> SNat n +leqLhs (ZeroLeq _) = Zero +leqLhs (SuccLeqSucc leq) = sSucc $ leqLhs leq + +propToBoolLt :: n :<: m -> IsTrue (n SNat n -> SNat m -> n :<: m +boolToPropLt Zero (Succ sn) = ZeroLtSucc sn +boolToPropLt (Succ n) Zero = eliminate $ + start STrue + =~= (Succ n % SNat m -> SNat (Min n m) +{-# INLINE sMin #-} +sMin = unsafeLiftSBin min + +sMax :: SNat n -> SNat m -> SNat (Max n m) +{-# INLINE sMax #-} +sMax = unsafeLiftSBin max + +#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 =?, >=, >, >? + +#if MIN_VERSION_ghc(9,2,1) +type (n :: Nat) SNat m -> SBool (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) +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 + +#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) +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) + +data DiffNat n m where + DiffNat :: SNat n -> SNat m -> DiffNat n (n + m) + +newtype LeqWitPf n = LeqWitPf {leqWitPf :: forall m. SNat m -> IsTrue (n <=? m) -> DiffNat n m} + +succDiffNat :: SNat n -> SNat m -> DiffNat n m -> DiffNat (Succ n) (Succ m) +succDiffNat _ _ (DiffNat n m) = gcastWith (plusSuccL n m) $ DiffNat (sSucc n) m + +-- | Since 1.0.0.0 (type changed) +coerceLeqL :: + forall n m l. + n :~: m -> + SNat l -> + IsTrue (n <=? l) -> + IsTrue (m <=? l) +coerceLeqL Refl _ Witness = Witness + +-- | Since 1.0.0.0 (type changed) +coerceLeqR :: + forall n m l. + SNat l -> + n :~: m -> + IsTrue (l <=? n) -> + IsTrue (l <=? m) +coerceLeqR _ Refl Witness = Witness + +compareCongR :: SNat a -> b :~: c -> CmpNat a b :~: CmpNat a c +compareCongR _ Refl = Refl + +sLeqCong :: a :~: b -> c :~: d -> (a <= c) :~: (b <= d) +sLeqCong Refl Refl = Refl + +sLeqCongL :: a :~: b -> SNat c -> (a <= c) :~: (b <= c) +sLeqCongL Refl _ = Refl + +sLeqCongR :: SNat a -> b :~: c -> (a <= b) :~: (a <= c) +sLeqCongR _ Refl = Refl + +newtype LeqViewRefl n = LeqViewRefl {proofLeqViewRefl :: LeqView n n} + +leqToCmp :: + SNat a -> + SNat b -> + IsTrue (a <=? b) -> + Either (a :~: b) (CmpNat a b :~: 'LT) +leqToCmp n m Witness = + case n %~ m of + Equal -> Left Refl + NonEqual -> Right Refl + +eqlCmpEQ :: SNat a -> SNat b -> a :~: b -> CmpNat a b :~: 'EQ +eqlCmpEQ _ _ Refl = Refl + +eqToRefl :: SNat a -> SNat b -> CmpNat a b :~: 'EQ -> a :~: b +eqToRefl _ _ Refl = Refl + +flipCmpNat :: + SNat a -> + SNat b -> + FlipOrdering (CmpNat a b) :~: CmpNat b a +flipCmpNat n m = case sCmpNat n m of + SGT -> Refl + SLT -> Refl + SEQ -> Refl + +ltToNeq :: + SNat a -> + SNat b -> + CmpNat a b :~: 'LT -> + a :~: b -> + Void +ltToNeq a b aLTb aEQb = + eliminate $ + start SLT + === sCmpNat a b `because` sym aLTb + === SEQ `because` eqlCmpEQ a b aEQb + +leqNeqToLT :: SNat a -> SNat b -> IsTrue (a <=? b) -> (a :~: b -> Void) -> CmpNat a b :~: 'LT +leqNeqToLT a b aLEQb aNEQb = either (absurd . aNEQb) id $ leqToCmp a b aLEQb + +succLeqToLT :: SNat a -> SNat b -> IsTrue (S a <=? b) -> CmpNat a b :~: 'LT +succLeqToLT _ _ Witness = Refl + +ltToLeq :: + SNat a -> + SNat b -> + CmpNat a b :~: 'LT -> + IsTrue (a <=? b) +ltToLeq _ _ Refl = Witness + +gtToLeq :: + SNat a -> + SNat b -> + CmpNat a b :~: 'GT -> + IsTrue (b <=? a) +gtToLeq _ _ Refl = Witness + +congFlipOrdering :: + a :~: b -> FlipOrdering a :~: FlipOrdering b +congFlipOrdering Refl = Refl + +ltToSuccLeq :: + SNat a -> + SNat b -> + CmpNat a b :~: 'LT -> + IsTrue (Succ a <=? b) +ltToSuccLeq _ _ Refl = Witness + +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 -> + IsTrue (Succ b <=? a) -> + CmpNat a b :~: 'GT +leqToGT _ _ Witness = Refl + +cmpZero' :: SNat a -> Either (CmpNat 0 a :~: 'EQ) (CmpNat 0 a :~: 'LT) +cmpZero' n = + case zeroOrSucc n of + IsZero -> Left $ eqlCmpEQ sZero n Refl + IsSucc n' -> Right $ cmpZero n' + +zeroNoLT :: SNat a -> CmpNat a 0 :~: 'LT -> Void +zeroNoLT n eql = + case cmpZero' n of + Left cmp0nEQ -> + eliminate $ + start SGT + =~= sFlipOrdering SLT + === sFlipOrdering (sCmpNat n sZero) `because` congFlipOrdering (sym eql) + === sCmpNat sZero n `because` flipCmpNat n sZero + === SEQ `because` cmp0nEQ + Right cmp0nLT -> + eliminate $ + start SGT + =~= sFlipOrdering SLT + === sFlipOrdering (sCmpNat n sZero) `because` congFlipOrdering (sym eql) + === sCmpNat sZero n `because` flipCmpNat n sZero + === SLT `because` cmp0nLT + +ltRightPredSucc :: SNat a -> SNat b -> CmpNat a b :~: 'LT -> b :~: Succ (Pred b) +ltRightPredSucc _ _ Refl = Refl + +cmpSucc :: SNat n -> SNat m -> CmpNat n m :~: CmpNat (Succ n) (Succ m) +cmpSucc _ _ = Refl + +ltSucc :: SNat a -> CmpNat a (Succ a) :~: 'LT +ltSucc _ = Refl + +cmpSuccStepR :: + forall n m. + SNat n -> + SNat m -> + CmpNat n m :~: 'LT -> + CmpNat n (Succ m) :~: 'LT +cmpSuccStepR _ _ Refl = Refl + +ltSuccLToLT :: + SNat n -> + SNat m -> + CmpNat (Succ n) m :~: 'LT -> + CmpNat n m :~: 'LT +ltSuccLToLT n m snLTm = + case zeroOrSucc m of + IsZero -> absurd $ zeroNoLT (sSucc n) snLTm + IsSucc m' -> + let nLTm = cmpSucc n m' `trans` snLTm + in start (sCmpNat n (sSucc m')) + === SLT `because` cmpSuccStepR n m' nLTm + +leqToLT :: + SNat a -> + SNat b -> + IsTrue (Succ a <=? b) -> + CmpNat a b :~: 'LT +leqToLT _ _ Witness = Refl + +leqZero :: SNat n -> IsTrue (0 <=? n) +leqZero _ = Witness + +leqSucc :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (Succ n <=? Succ m) +leqSucc _ _ Witness = Witness + +fromLeqView :: LeqView n m -> IsTrue (n <=? m) +fromLeqView (LeqZero n) = leqZero n +fromLeqView (LeqSucc n m nLEQm) = leqSucc n m nLEQm + +leqViewRefl :: SNat n -> LeqView n n +leqViewRefl = proofLeqViewRefl . induction base step + where + base :: LeqViewRefl 0 + base = LeqViewRefl $ LeqZero sZero + step :: SNat n -> LeqViewRefl n -> LeqViewRefl (Succ n) + step n (LeqViewRefl nLEQn) = + LeqViewRefl $ LeqSucc n n (fromLeqView nLEQn) + +viewLeq :: forall n m. SNat n -> SNat m -> IsTrue (n <=? m) -> LeqView n m +viewLeq n m nLEQm = + case (zeroOrSucc n, leqToCmp n m nLEQm) of + (IsZero, _) -> LeqZero m + (_, Left Refl) -> leqViewRefl n + (IsSucc n', Right nLTm) -> + let sm'EQm = ltRightPredSucc n m nLTm + m' = sPred m + 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 :: 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 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) || MIN_VERSION_ghc(9,4,0) + LeqZero _ -> absurd $ succNonCyclic n Refl +#endif + LeqSucc (_ :: SNat n') pm nLEQpm -> + succDiffNat n pm $ ih pm $ coerceLeqL (succInj Refl :: n' :~: x) pm nLEQpm + +leqStep :: forall n m l. SNat n -> SNat m -> SNat l -> n + l :~: m -> IsTrue (n <=? m) +leqStep _ _ _ Refl = Witness + +leqNeqToSuccLeq :: SNat n -> SNat m -> IsTrue (n <=? m) -> (n :~: m -> Void) -> IsTrue (Succ n <=? m) +leqNeqToSuccLeq n m nLEQm nNEQm = + case leqWitness n m nLEQm of + DiffNat _ k -> + case zeroOrSucc k of + IsZero -> absurd $ nNEQm $ sym $ plusZeroR n + IsSucc k' -> + leqStep (sSucc n) m k' $ + start (sSucc n %+ k') + === sSucc (n %+ k') `because` plusSuccL n k' + === n %+ sSucc k' `because` sym (plusSuccR n k') + =~= m + +leqRefl :: SNat n -> IsTrue (n <=? n) +leqRefl _ = Witness + +leqSuccStepR :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (n <=? Succ m) +leqSuccStepR _ _ Witness = Witness + +leqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n <=? m) -> IsTrue (n <=? m) +leqSuccStepL _ _ Witness = Witness + +leqReflexive :: SNat n -> SNat m -> n :~: m -> IsTrue (n <=? m) +leqReflexive _ _ Refl = Witness + +leqTrans :: SNat n -> SNat m -> SNat l -> IsTrue (n <=? m) -> IsTrue (m <=? l) -> IsTrue (n <=? l) +leqTrans _ _ _ Witness Witness = Witness + +leqAntisymm :: SNat n -> SNat m -> IsTrue (n <=? m) -> IsTrue (m <=? n) -> n :~: m +leqAntisymm _ _ Witness Witness = Refl + +plusMonotone :: + SNat n -> + SNat m -> + SNat l -> + SNat k -> + IsTrue (n <=? m) -> + IsTrue (l <=? k) -> + IsTrue ((n + l) <=? (m + k)) +plusMonotone _ _ _ _ Witness Witness = Witness + +leqZeroElim :: SNat n -> IsTrue (n <=? 0) -> n :~: 0 +leqZeroElim _ Witness = Refl + +plusMonotoneL :: + SNat n -> + SNat m -> + SNat l -> + IsTrue (n <=? m) -> + IsTrue ((n + l) <=? (m + l)) +plusMonotoneL _ _ _ Witness = Witness + +plusMonotoneR :: + SNat n -> + SNat m -> + SNat l -> + IsTrue (m <=? l) -> + IsTrue ((n + m) <=? (n + l)) +plusMonotoneR _ _ _ Witness = Witness + +plusLeqL :: SNat n -> SNat m -> IsTrue (n <=? (n + m)) +plusLeqL _ _ = Witness + +plusLeqR :: SNat n -> SNat m -> IsTrue (m <=? (n + m)) +plusLeqR _ _ = Witness + +plusCancelLeqR :: + SNat n -> + SNat m -> + SNat l -> + IsTrue ((n + l) <=? (m + l)) -> + IsTrue (n <=? m) +plusCancelLeqR _ _ _ Witness = Witness + +plusCancelLeqL :: + SNat n -> + SNat m -> + SNat l -> + IsTrue ((n + m) <=? (n + l)) -> + IsTrue (m <=? l) +plusCancelLeqL _ _ _ Witness = Witness + +succLeqZeroAbsurd :: SNat n -> IsTrue (S n <=? 0) -> Void +succLeqZeroAbsurd n leq = + succNonCyclic n (leqZeroElim (sSucc n) leq) + +succLeqZeroAbsurd' :: SNat n -> (S n <=? 0) :~: 'False +succLeqZeroAbsurd' _ = Refl + +succLeqAbsurd :: SNat n -> IsTrue (S n <=? n) -> Void +succLeqAbsurd n snLEQn = + eliminate $ + start SLT + === sCmpNat n n `because` sym (succLeqToLT n n snLEQn) + === SEQ `because` eqlCmpEQ n n Refl + +succLeqAbsurd' :: SNat n -> (S n <=? n) :~: 'False +succLeqAbsurd' _ = Refl + +notLeqToLeq :: forall n m. ((n <=? m) ~ 'False) => SNat n -> SNat m -> IsTrue (m <=? n) +notLeqToLeq _ _ = Witness + +leqSucc' :: SNat n -> SNat m -> (n <=? m) :~: (Succ n <=? Succ m) +leqSucc' _ _ = Refl + +leqToMin :: SNat n -> SNat m -> IsTrue (n <=? m) -> Min n m :~: n +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 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 = + case n %<=? m of + STrue -> + start (sMin n m) === n `because` leqToMin n m Witness + === sMin m n `because` sym (geqToMin m n Witness) + SFalse -> + start (sMin n m) === m `because` geqToMin n m (notLeqToLeq n m) + === sMin m n `because` sym (leqToMin m n $ notLeqToLeq n m) + +minLeqL :: SNat n -> SNat m -> IsTrue (Min n m <=? n) +minLeqL n m = + case n %<=? m of + STrue -> leqReflexive (sMin n m) n $ leqToMin n m Witness + SFalse -> + let mLEQn = notLeqToLeq n m + in leqTrans + (sMin n m) + m + n + (leqReflexive (sMin n m) m (geqToMin n m mLEQn)) + $ mLEQn + +minLeqR :: SNat n -> SNat m -> IsTrue (Min n m <=? m) +minLeqR n m = + leqTrans + (sMin n m) + (sMin m n) + m + (leqReflexive (sMin n m) (sMin m n) $ minComm n m) + (minLeqL m n) + +minLargest :: + SNat l -> + SNat n -> + SNat m -> + IsTrue (l <=? n) -> + IsTrue (l <=? m) -> + IsTrue (l <=? Min n m) +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 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 sCmpNat n m of + SLT -> Refl + SEQ -> Refl + SGT -> Refl + +maxComm :: SNat n -> SNat m -> Max n m :~: Max m n +maxComm n m = + case n %<=? m of + STrue -> + start (sMax n m) === m `because` leqToMax n m Witness + === sMax m n `because` sym (geqToMax m n Witness) + SFalse -> + start (sMax n m) === n `because` geqToMax n m (notLeqToLeq n m) + === sMax m n `because` sym (leqToMax m n $ notLeqToLeq n m) + +maxLeqR :: SNat n -> SNat m -> IsTrue (m <=? Max n m) +maxLeqR n m = + case n %<=? m of + STrue -> leqReflexive m (sMax n m) $ sym $ leqToMax n m Witness + SFalse -> + let mLEQn = notLeqToLeq n m + in leqTrans + m + n + (sMax n m) + mLEQn + (leqReflexive n (sMax n m) (sym $ geqToMax n m mLEQn)) + +maxLeqL :: SNat n -> SNat m -> IsTrue (n <=? Max n m) +maxLeqL n m = + leqTrans + n + (sMax m n) + (sMax n m) + (maxLeqR m n) + (leqReflexive (sMax m n) (sMax n m) $ maxComm m n) + +maxLeast :: + SNat l -> + SNat n -> + SNat m -> + IsTrue (n <=? l) -> + IsTrue (m <=? l) -> + IsTrue (Max n m <=? l) +maxLeast _ n m nLEQl mLEQl = + case maxCase n m of + Left Refl -> mLEQl + Right Refl -> nLEQl + + +-- | Since 1.2.0.0 (type changed) +lneqSuccLeq :: SNat n -> SNat m -> (n 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 ? 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 + CmpNat n m :~: 'LT +lneqToLT n m Witness = + case sCmpNat n m of + SLT -> Refl + +ltToLneq :: + SNat n -> + SNat m -> + CmpNat n m :~: 'LT -> + IsTrue (n IsTrue (0 IsTrue (n + SNat m -> + (n proxy a -> proxy' b -> proxy' c + -> OrdCond o a b c :~: OrdCond o' a b c +sOrdCondCong1 Refl _ _ _ = Refl + +lneqRightPredSucc :: + SNat n -> + SNat m -> + IsTrue (n + m :~: Succ (Pred m) +lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm + +lneqSuccStepL :: SNat n -> SNat m -> IsTrue (Succ n IsTrue (n SNat m -> IsTrue (n IsTrue (n + SNat m -> + SNat l -> + SNat k -> + IsTrue (n + IsTrue (l + IsTrue ((n + l) Max 0 n :~: n +maxZeroL n = leqToMax sZero n (leqZero n) + +maxZeroR :: SNat n -> Max n 0 :~: n +maxZeroR n = geqToMax n sZero (leqZero n) + +minZeroL :: SNat n -> Min 0 n :~: 0 +minZeroL n = leqToMin sZero n (leqZero n) + +minZeroR :: SNat n -> Min n 0 :~: 0 +minZeroR n = geqToMin n sZero (leqZero n) + +minusSucc :: SNat n -> SNat m -> IsTrue (m <=? n) -> Succ n - m :~: Succ (n - m) +minusSucc n m mLEQn = + case leqWitness m n mLEQn of + DiffNat _ k -> + start (sSucc n %- m) + =~= sSucc (m %+ k) %- m + === (m %+ sSucc k) %- m `because` minusCongL (sym $ plusSuccR m k) m + === (sSucc k %+ m) %- m `because` minusCongL (plusComm m (sSucc k)) m + === sSucc k `because` plusMinus (sSucc k) m + === sSucc (k %+ m %- m) `because` succCong (sym $ plusMinus k m) + === sSucc (m %+ k %- m) `because` succCong (minusCongL (plusComm k m) m) + =~= sSucc (n %- m) + +lneqZeroAbsurd :: SNat n -> IsTrue (n Void +lneqZeroAbsurd n leq = + succLeqZeroAbsurd n (gcastWith (lneqSuccLeq n sZero) leq) + +minusPlus :: + forall n m. + SNat n -> + SNat m -> + IsTrue (m <=? n) -> + n - m + m :~: n +minusPlus n m mLEQn = + case leqWitness m n mLEQn of + DiffNat _ k -> + start (n %- m %+ m) + =~= m %+ k %- m %+ m + === k %+ m %- m %+ m `because` plusCongL (minusCongL (plusComm m k) m) m + === k %+ m `because` plusCongL (plusMinus k m) m + === m %+ k `because` plusComm k m + =~= n + +-- | Natural subtraction, truncated to zero if m > n. +type n -. m = Subt n m (m <=? n) + +type family Subt n m (b :: Bool) where + Subt n m 'True = n - m + Subt n m 'False = 0 + +infixl 6 -. + +(%-.) :: SNat n -> SNat m -> SNat (n -. m) +n %-. m = + case m %<=? n of + STrue -> n %- m + SFalse -> sZero + +minPlusTruncMinus :: + SNat n -> + SNat m -> + Min n m + (n -. m) :~: n +minPlusTruncMinus n m = + case m %<=? n of + STrue -> + start (sMin n m %+ (n %-. m)) + === m %+ (n %-. m) `because` plusCongL (geqToMin n m Witness) (n %-. m) + =~= m %+ (n %- m) + === (n %- m) %+ m `because` plusComm m (n %- m) + === n `because` minusPlus n m Witness + SFalse -> + start (sMin n m %+ (n %-. m)) + =~= sMin n m %+ sZero + === sMin n m `because` plusZeroR (sMin n m) + === n `because` leqToMin n m (notLeqToLeq m n) + +truncMinusLeq :: SNat n -> SNat m -> IsTrue ((n -. m) <=? n) +truncMinusLeq n m = + case m %<=? n of + STrue -> leqStep (n %-. m) n m $ minusPlus n m Witness + SFalse -> leqZero n diff --git a/src/Data/Type/Natural/Lemma/Presburger.hs b/src/Data/Type/Natural/Lemma/Presburger.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Lemma/Presburger.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitForAll #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} + +module Data.Type.Natural.Lemma.Presburger where + +import Data.Type.Equality +import Data.Type.Natural.Core +import Data.Void + +plusEqZeroL :: SNat n -> SNat m -> n + m :~: 0 -> n :~: 0 +plusEqZeroL _ _ Refl = Refl + +plusEqZeroR :: SNat n -> SNat m -> n + m :~: 0 -> m :~: 0 +plusEqZeroR _ _ Refl = Refl + +succNonCyclic :: SNat n -> Succ n :~: 0 -> Void +succNonCyclic Zero r = case r of +succNonCyclic (Succ n) Refl = succNonCyclic n Refl diff --git a/src/Data/Type/Natural/Presburger/MinMaxSolver.hs b/src/Data/Type/Natural/Presburger/MinMaxSolver.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Presburger/MinMaxSolver.hs @@ -0,0 +1,60 @@ +{-# 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 @>=@. +-} +module Data.Type.Natural.Presburger.MinMaxSolver (plugin) where + +import Control.Monad (mzero) +import GHC.TypeLits.Presburger.Compat +import GHC.TypeLits.Presburger.Types + +import GHC.Plugins + ( Plugin, + fsLit, + mkModuleName, + mkTcOcc, + splitTyConApp_maybe, + ) +import GHC.Tc.Plugin + +plugin :: Plugin +plugin = + pluginWith $ + (<>) <$> defaultTranslation <*> genTypeNatsTranslation + +genTypeNatsTranslation :: TcPluginM Translation +genTypeNatsTranslation = do + orderMod <- lookupModule (mkModuleName "Data.Type.Natural.Lemma.Order") (fsLit "type-natural") + singNatLt <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "=?") + singNatGt <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc ">?") + + singNatLtProp <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "<") + singNatGeqProp <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc ">=") + singNatGtProp <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc ">") + + singMin <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "Min") + singMax <- tcLookupTyCon =<< lookupOrig orderMod (mkTcOcc "Max") +#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 + Just (con, [l, r]) + | con == singNatLtProp -> (:<) <$> toE l <*> toE r + | con == singNatGtProp -> (:>) <$> toE l <*> toE r + | con == singNatGeqProp -> (:>=) <$> toE l <*> toE r + _ -> mzero + } diff --git a/src/Data/Type/Natural/Utils.hs b/src/Data/Type/Natural/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Natural/Utils.hs @@ -0,0 +1,10 @@ +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeApplications #-} + +module Data.Type.Natural.Utils where + +import Data.Type.Equality (type (:~:) (..)) +import Unsafe.Coerce (unsafeCoerce) + +trustMe :: x :~: y +trustMe = unsafeCoerce (Refl @()) diff --git a/src/Data/Type/Ordinal.hs b/src/Data/Type/Ordinal.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Ordinal.hs @@ -0,0 +1,340 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE EmptyDataDecls #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} +{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-} +{-# OPTIONS_GHC -fobject-code #-} + +{- | Set-theoretic ordinals for built-in type-level naturals + + Since 1.0.0.0 +-} +module Data.Type.Ordinal + ( -- * Data-types + Ordinal (..), + pattern OZ, + pattern OS, + + -- * Quasi Quoter + -- $quasiquotes + od, + + -- * Conversion from cardinals to ordinals. + sNatToOrd', + sNatToOrd, + ordToNatural, + unsafeNaturalToOrd', + unsafeNaturalToOrd, + reallyUnsafeNaturalToOrd, + naturalToOrd, + naturalToOrd', + ordToSNat, + inclusion, + inclusion', + + -- * Ordinal arithmetics + (@+), + enumOrdinal, + + -- * Elimination rules for @'Ordinal' 'Z'@. + absurdOrd, + vacuousOrd, + ) +where + +import Data.Maybe (fromMaybe) +import Data.Ord (comparing) +import Data.Proxy (Proxy (Proxy)) +import Data.Type.Equality +import Data.Type.Natural +import Data.Typeable (Typeable) +import Language.Haskell.TH.Quote +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: + + > n = {0, 1, ..., n-1} + + So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. + + Since 1.0.0.0 +-} +data Ordinal (n :: Nat) where + OLt :: (n < m) => SNat (n :: Nat) -> Ordinal m + +{-# COMPLETE OLt #-} + +fromOLt :: + forall n m. + ((Succ n < Succ m), KnownNat m) => + SNat (n :: Nat) -> + Ordinal m +fromOLt n = OLt n + +{- | Pattern synonym representing the 0-th ordinal. + + Since 1.0.0.0 +-} +pattern OZ :: forall (n :: Nat). (0 < n) => Ordinal n +pattern OZ <- OLt Zero where OZ = OLt sZero + +{- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal. + + Since 1.0.0.0 +-} +pattern OS :: forall (t :: Nat). (KnownNat t) => Ordinal t -> Ordinal (Succ t) +pattern OS n <- + OLt (Succ (fromOLt -> n)) + where + OS o = succOrd o + +-- | Since 1.0.0.0 +deriving instance Typeable Ordinal + +{- | Class synonym for Peano numerals with ordinals. + + Since 1.0.0.0 +-} +instance (KnownNat n) => Num (Ordinal n) where + _ + _ = error "Finite ordinal is not closed under addition." + _ - _ = error "Ordinal subtraction is not defined" + negate _ = error "There are no negative oridnals!" + _ * _ = error "Finite ordinal is not closed under multiplication" + abs = id + signum = error "What does Ordinal sign mean?" + fromInteger = unsafeFromNatural' . fromIntegral + +unsafeFromNatural' :: forall n. KnownNat n => Natural -> Ordinal n +unsafeFromNatural' k = withSNat k $ \sk -> + case sk % OLt sk + SFalse -> error $ "Index out of bounds: " ++ show (k, natVal @n Proxy) + +-- deriving instance Read (Ordinal n) => Read (Ordinal (Succ n)) +instance + (KnownNat n) => + Show (Ordinal (n :: Nat)) + where + 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' + +instance Ord (Ordinal (n :: Nat)) where + compare = comparing ordToNatural + +instance + (KnownNat n) => + Enum (Ordinal (n :: Nat)) + where + fromEnum = fromEnum . ordToNatural + toEnum = unsafeFromNatural' . fromIntegral + enumFrom = enumFromOrd + enumFromTo = enumFromToOrd + +-- | Since 1.0.0.0 (type changed) +enumFromToOrd :: + forall (n :: Nat). + (KnownNat n) => + Ordinal n -> + Ordinal n -> + [Ordinal n] +enumFromToOrd ok ol = + map + (reallyUnsafeNaturalToOrd $ sNat @n) + [ordToNatural ok .. ordToNatural ol] + +-- | Since 1.0.0.0 (type changed) +enumFromOrd :: + forall (n :: Nat). + (KnownNat n) => + Ordinal n -> + [Ordinal n] +enumFromOrd ord = + map + (reallyUnsafeNaturalToOrd Proxy) + [ordToNatural ord .. natVal @n Proxy - 1] + +-- | Enumerate all @'Ordinal'@s less than @n@. +enumOrdinal :: SNat (n :: Nat) -> [Ordinal n] +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) +succOrd (OLt k) = OLt (sSucc k) +{-# INLINE succOrd #-} + +instance (KnownNat n, 0 < n) => Bounded (Ordinal n) where + minBound = OLt sZero + + 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. + + Since 1.0.0.0 +-} +unsafeNaturalToOrd :: + forall (n :: Nat). + (KnownNat n) => + Natural -> + Ordinal n +unsafeNaturalToOrd k = + fromMaybe (error "unsafeNaturalToOrd Out of bound") $ + naturalToOrd k + +-- | Since 1.0.0.0 +unsafeNaturalToOrd' :: + forall proxy (n :: Nat). + (KnownNat n) => + proxy n -> + Natural -> + Ordinal n +unsafeNaturalToOrd' _ = unsafeNaturalToOrd + +{-# WARNING reallyUnsafeNaturalToOrd "This function may violate type safety. Use with care!" #-} + +{- | Converts @'Natural'@s into @'Ordinal' n@, WITHOUT any boundary check. + This function may easily violate type-safety. Use with care! +-} +reallyUnsafeNaturalToOrd :: + forall pxy (n :: Nat). + (KnownNat n) => + pxy -> + Natural -> + Ordinal n +reallyUnsafeNaturalToOrd _ k = + withSNat k $ \(sk :: SNat k) -> + gcastWith (unsafeCoerce (Refl :: () :~: ()) :: (k SNat (n :: Nat) -> SNat m -> Ordinal n +sNatToOrd' _ = OLt +{-# INLINE sNatToOrd' #-} + +-- | 'sNatToOrd'' with @n@ inferred. +sNatToOrd :: (KnownNat n, m < n) => SNat m -> Ordinal n +sNatToOrd = sNatToOrd' sNat + +-- | Since 1.0.0.0 +naturalToOrd :: + forall n. + (KnownNat n) => + Natural -> + Maybe (Ordinal (n :: Nat)) +naturalToOrd = naturalToOrd' (sNat :: SNat n) + +naturalToOrd' :: + SNat (n :: Nat) -> + Natural -> + Maybe (Ordinal n) +naturalToOrd' sn k = withSNat k $ \(sk :: SNat pk) -> + case sk % Just (OLt sk) + _ -> Nothing + +{- | Convert @Ordinal n@ into monomorphic @SNat@ + + Since 1.0.0.0 +-} +ordToSNat :: Ordinal (n :: Nat) -> SomeSNat +ordToSNat (OLt n) = withKnownNat n $ SomeSNat n +{-# INLINE ordToSNat #-} + +ordToNatural :: + Ordinal (n :: Nat) -> + Natural +ordToNatural (OLt n) = fromSNat n + +{- | Inclusion function for ordinals. + + Since 1.0.0.0(constraint was weakened since last released) +-} +inclusion' :: (n <= m) => SNat m -> Ordinal n -> Ordinal m +inclusion' _ = unsafeCoerce +{-# INLINE inclusion' #-} + +{- | Inclusion function for ordinals with codomain inferred. + + Since 1.0.0.0(constraint was weakened since last released) +-} +inclusion :: (n <= m) => Ordinal n -> Ordinal m +inclusion (OLt a) = OLt a +{-# INLINE inclusion #-} + +{- | Ordinal addition. + + Since 1.0.0.0(type changed) +-} +(@+) :: + forall (n :: Nat) m. + (KnownNat n, KnownNat m) => + Ordinal n -> + Ordinal m -> + Ordinal (n + m) +OLt k @+ OLt l = OLt $ k %+ l + +{- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. + + Since 1.0.0.0 +-} +absurdOrd :: Ordinal 0 -> a +absurdOrd (OLt sn) = absurd $ lneqZeroAbsurd sn Witness + +{- | @'absurdOrd'@ for value in 'Functor'. + + Since 1.0.0.0 +-} +vacuousOrd :: (Functor f) => f (Ordinal 0) -> f a +vacuousOrd = fmap absurdOrd + +{- $quasiquotes #quasiquoters# + + This section provides QuasiQuoter and general generator for ordinals. + Note that, @'Num'@ instance for @'Ordinal'@s DOES NOT + checks boundary; with @'od'@, we can use literal with + boundary check. + For example, with @-XQuasiQuotes@ language extension enabled, + @['od'| 12 |] :: Ordinal 1@ doesn't typechecks and causes compile-time error, + whilst @12 :: Ordinal 1@ compiles but raises run-time error. + So, to enforce correctness, we recommend to use these quoters + instead of bare @'Num'@ numerals. +-} + +-- | Quasiquoter for ordinal indexed by built-in numeral @'GHC.TypeLits.Nat'@. +od :: QuasiQuoter +od = + QuasiQuoter + { quoteExp = \s -> [|OLt $(quoteExp snat s)|] + , quoteType = error "No type quoter for Ordinals" + , quotePat = \s -> [p|OLt ((%~ $(quoteExp snat s)) -> Equal)|] + , quoteDec = error "No declaration quoter for Ordinals" + } + +-- >>> 42 diff --git a/src/Data/Type/Ordinal/Builtin.hs b/src/Data/Type/Ordinal/Builtin.hs new file mode 100644 --- /dev/null +++ b/src/Data/Type/Ordinal/Builtin.hs @@ -0,0 +1,7 @@ +module Data.Type.Ordinal.Builtin + {-# DEPRECATED "Use Data.Type.Ordinal instead" #-} + ( module Data.Type.Ordinal, + ) +where + +import Data.Type.Ordinal diff --git a/tests/Data/Type/Natural/Lemma/OrderSpec.hs b/tests/Data/Type/Natural/Lemma/OrderSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/Natural/Lemma/OrderSpec.hs @@ -0,0 +1,485 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Data.Type.Natural.Lemma.OrderSpec where + +import Control.Exception (SomeException (..), evaluate, try) +import Data.Functor ((<&>)) +import Data.List (isInfixOf, isPrefixOf) +import Data.Type.Natural +import Data.Type.Natural.Lemma.Order +import Data.Void (Void) +import Proof.Propositional (IsTrue (Witness)) +import Shared () +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.HUnit +import Test.Tasty.QuickCheck +import Type.Reflection +import Unsafe.Coerce (unsafeCoerce) + +someNat' :: NonNegative Integer -> SomeSNat +someNat' = toSomeSNat . fromInteger . getNonNegative + +data SomeLeqNat where + MkSomeLeqNat :: (n <=? m) ~ 'True => SNat n -> SNat m -> SomeLeqNat + +data SomeLtNat where + MkSomeLtNat :: + CmpNat n m ~ 'LT => + SNat n -> + SNat m -> + SomeLtNat + +data SomeLneqNat where + MkSomeLneqNat :: + (n + SNat n -> + SNat m -> + SomeLneqNat + +data SomeGtNat where + MkSomeGtNat :: + CmpNat n m ~ 'GT => + SNat n -> + SNat m -> + SomeGtNat + +deriving instance Show SomeLeqNat + +deriving instance Show SomeLtNat + +deriving instance Show SomeLneqNat + +deriving instance Show SomeGtNat + +instance Arbitrary SomeLeqNat where + arbitrary = do + SomeSNat n <- someNat' <$> arbitrary + SomeSNat m <- someNat' <$> arbitrary + case n %<=? m of + STrue -> pure $ MkSomeLeqNat n m + SFalse -> + case m %<=? n of + STrue -> pure $ MkSomeLeqNat m n + SFalse -> error "Impossible!" + +instance Arbitrary SomeLtNat where + arbitrary = do + MkSomeLeqNat (n :: SNat n) (m :: SNat m) <- arbitrary + let m' = Succ m + case sCmpNat n m' of + SLT -> pure $ MkSomeLtNat n m' + _ -> error "impossible" + +instance Arbitrary SomeLneqNat where + arbitrary = do + MkSomeLtNat (n :: SNat n) (m :: SNat m) <- arbitrary + let m' = Succ m + case n % pure $ MkSomeLneqNat n m' + _ -> error "impossible" + +instance Arbitrary SomeGtNat where + arbitrary = do + MkSomeLeqNat (n :: SNat n) (m :: SNat m) <- arbitrary + let m' = Succ m + case sCmpNat m' n of + SGT -> pure $ MkSomeGtNat m' n + _ -> error "impossible" + +data SomeLeqView where + MkSomeLeqView :: LeqView n m -> SomeLeqView + +instance Show SomeLeqView where + showsPrec d (MkSomeLeqView (LeqZero n)) = + showParen (d > 10) $ + showString "LeqZero " + . showsPrec 11 n + showsPrec d (MkSomeLeqView (LeqSucc n m w)) = + showParen (d > 10) $ + showString "LeqSucc " + . showsPrec 11 n + . showChar ' ' + . showsPrec 11 m + . showChar ' ' + . showsPrec 11 w + +instance Arbitrary SomeLeqView where + arbitrary = sized $ \n -> + if n <= 0 + then + arbitrary <&> \case + SomeSNat sn -> MkSomeLeqView (LeqZero sn) + else + arbitrary <&> \case + MkSomeLeqNat sn sm -> MkSomeLeqView $ LeqSucc sn sm Witness + +givesImpossibleVoid :: Void -> Property +givesImpossibleVoid contradiction = ioProperty $ do + eith <- try @SomeException $ evaluate contradiction + case eith of + Left someE -> do + pure $ counterexample (show someE) $ + property $ + "Impossible" `isPrefixOf` show someE + || "Non-exhaustive" `isInfixOf` show someE + || "missingAlt" `isInfixOf` show someE + Right v -> + pure $ counterexample "Value of void returned..." + $ property False + +test_Lemmas :: TestTree +test_Lemmas = + testGroup + "Lemmas" + [ testProperty @(SomeLeqNat -> Property) "coerceLeqL terminates" $ \(MkSomeLeqNat (_ :: SNat n) sm) -> totalWitness $ coerceLeqL (Refl :: n :~: n) sm Witness + , testProperty @(SomeLeqNat -> Property) "coerceLeqR terminates" $ \(MkSomeLeqNat sn (_ :: SNat m)) -> totalWitness $ coerceLeqR sn (Refl :: m :~: m) Witness + , testProperty @(SomeSNat -> SomeSNat -> Property) "sLeqCong terminates" $ + \(SomeSNat (_ :: SNat n)) (SomeSNat (_ :: SNat m)) -> + totalRefl $ sLeqCong (Refl @n) (Refl @m) + , testProperty @(SomeSNat -> SomeSNat -> Property) "succDiffNat terminates and gives the correct value" $ + \(SomeSNat sn) (SomeSNat sm) -> + case succDiffNat sn (sn %+ sm) (DiffNat sn sm) of + DiffNat sns sms -> + fromSNat (sns %+ sms) + === fromSNat sn + fromSNat sm + 1 + , testProperty @(SomeSNat -> SomeSNat -> Property) + "compareCongR terminates" + $ \(SomeSNat a) (SomeSNat (_ :: SNat b)) -> + totalRefl $ compareCongR a (Refl @b) + , testProperty @(SomeLeqNat -> Property) + "leqToCmp works properly" + $ \case + MkSomeLeqNat a b -> + case leqToCmp a b Witness of + Left Refl -> fromSNat a === fromSNat b + Right Refl -> + property $ fromSNat a < fromSNat b + , testProperty @(SomeSNat -> Property) + "eqlCmpEQ terminates" + $ \(SomeSNat n) -> + totalRefl $ eqlCmpEQ n n Refl + , testProperty @(SomeSNat -> Property) + "eqToRefl terminates" + $ \(SomeSNat n) -> + totalRefl $ eqToRefl n n Refl + , testProperty @(SomeSNat -> SomeSNat -> Property) + "flipCmpNat terminates" + $ \(SomeSNat n) (SomeSNat m) -> + totalRefl $ flipCmpNat n m + , testProperty @(SomeSNat -> Property) + "ltToNeq works as expected" + $ \(SomeSNat n) -> + givesImpossibleVoid $ + ltToNeq n n (unsafeCoerce $ Refl @()) Refl + , testProperty @(SomeLeqNat -> Property) + "leqNeqToLT terminates" + $ \(MkSomeLeqNat n m) -> + case n %~ m of + Equal -> discard + NonEqual -> + totalRefl $ leqNeqToLT n m Witness (\case {}) + , testProperty @(SomeLeqNat -> Property) + "succLeqToLT terminates" + $ \(MkSomeLeqNat n' m) -> + case n' of + Succ n -> + totalRefl $ succLeqToLT n m Witness + _ -> discard + , testProperty @(SomeLtNat -> Property) + "ltToLeq terminates" + $ \(MkSomeLtNat n m) -> + totalWitness $ ltToLeq n m Refl + , testProperty @(SomeGtNat -> Property) + "gtToLeq terminates" + $ \(MkSomeGtNat n m) -> + totalWitness $ gtToLeq n m Refl + , testCase "congFlipOrdering" $ do + Refl <- evaluate (congFlipOrdering (Refl @( 'LT))) + Refl <- evaluate (congFlipOrdering (Refl @( 'GT))) + Refl <- evaluate (congFlipOrdering (Refl @( 'EQ))) + pure () + , testProperty @(SomeLtNat -> Property) "ltToSuccLeq terminates" $ \(MkSomeLtNat n m) -> + totalWitness $ ltToSuccLeq n m Refl + , testProperty @(SomeSNat -> Property) "cmpZero terminates" $ \(SomeSNat n) -> + totalRefl $ cmpZero n + , testProperty @(SomeLeqNat -> Property) "leqToGT terminates" $ \(MkSomeLeqNat b0 a) -> + case b0 of + Succ b -> + totalRefl $ leqToGT a b Witness + Zero -> discard + , testProperty @(SomeSNat -> Property) "cmpZero' works as expected" $ \(SomeSNat n) -> + case n of + Zero -> cmpZero' n === Left Refl + Succ {} -> case cmpZero' n of + Right Refl -> property True + l -> counterexample ("Left Refl expected, but got: " <> show l) False + , testProperty @(SomeSNat -> Property) + "zeroNoLT works as expected" + $ \(SomeSNat n) -> + givesImpossibleVoid $ zeroNoLT n (unsafeCoerce $ Refl @()) + , testProperty @(SomeLtNat -> Property) "ltRightPredSucc terminates" $ \(MkSomeLtNat a b) -> + totalRefl $ ltRightPredSucc a b Refl + , testProperty @(SomeSNat -> SomeSNat -> Property) "cmpSucc terminates" $ \(SomeSNat a) (SomeSNat b) -> + totalRefl $ cmpSucc a b + , testProperty @(SomeSNat -> Property) "ltSucc terminates" $ \(SomeSNat a) -> + totalRefl $ ltSucc a + , testProperty @(SomeLtNat -> Property) "cmpSuccStepR terminates" $ \(MkSomeLtNat a b) -> + totalRefl $ cmpSuccStepR a b Refl + , testProperty @(SomeLtNat -> Property) "ltSuccLToLT terminates" $ \(MkSomeLtNat a0 b) -> + case a0 of + Succ a -> totalRefl $ ltSuccLToLT a b Refl + Zero -> discard + , testProperty @(SomeLeqNat -> Property) "leqToLT terminates" $ \(MkSomeLeqNat a0 b) -> + case a0 of + Succ a -> totalRefl $ leqToLT a b Witness + Zero -> discard + , testProperty @(SomeSNat -> Property) "leqZero terminates" $ \(SomeSNat n) -> + totalWitness $ leqZero n + , testProperty @(SomeLeqNat -> Property) "leqSucc terminates" $ \(MkSomeLeqNat n m) -> + totalWitness $ leqSucc n m Witness + , testProperty @(SomeLeqView -> Property) "fromLeqView terminates" $ \(MkSomeLeqView lview) -> + totalWitness $ fromLeqView lview + , testProperty @(SomeSNat -> Property) "leqViewRefl works properly" $ \(SomeSNat sn) -> + case leqViewRefl sn of + LeqZero sn' -> + fromSNat sn' === fromSNat sn .&&. fromSNat sn' === 0 + LeqSucc sn' sm' Witness -> + 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' -> + fromSNat sn === 0 .&&. fromSNat sm === fromSNat sm' + LeqSucc sn' sm' Witness -> + 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 -> + fromSNat sn === fromSNat sn' + .&&. fromSNat sn' + fromSNat delta === fromSNat sm + , testProperty @(SomeSNat -> SomeSNat -> Property) + "leqStep terminates" + $ \(SomeSNat n) (SomeSNat l) -> + let m = n %+ l + in totalWitness $ leqStep n m l Refl + , testProperty @(SomeLeqNat -> Property) "leqNeqToSuccLeq terminates" $ + \(MkSomeLeqNat n m) -> + case n %~ m of + Equal -> discard + NonEqual -> + totalWitness $ leqNeqToSuccLeq n m Witness (\case {}) + , testProperty @(SomeSNat -> Property) "leqRefl terminates" $ + \(SomeSNat n) -> + totalWitness $ leqRefl n + , testProperty @(SomeLeqNat -> Property) "leqSuccStepR and leqSuccStepL terminates" $ + \(MkSomeLeqNat n m) -> + totalWitness (leqSuccStepR n m Witness) + .&&. case n of + Succ n' -> + label "leqSuccStepL tested" $ + totalWitness (leqSuccStepL n' m Witness) + _ -> property True + , testProperty @(SomeSNat -> Property) "leqReflexive terminates" $ + \(SomeSNat n) -> + totalWitness $ leqReflexive n n Refl + , testProperty @(SomeLeqNat -> SomeSNat -> Property) "leqTrans terminates" $ + \(MkSomeLeqNat (n :: SNat n) (m :: SNat m)) (SomeSNat (l0 :: SNat lMinsM)) -> + let l = m %+ l0 + in case m %<=? l of + STrue -> + totalWitness $ + leqTrans n m l Witness (Witness :: IsTrue (m <=? (m + lMinsM))) + SFalse -> error "impossible" + , testProperty @(SomeSNat -> Property) "leqAntisymm terminates" $ + \(SomeSNat n) -> + totalRefl $ leqAntisymm n n Witness Witness + , testProperty @(SomeLeqNat -> SomeLeqNat -> Property) "plusMonotone terminates" $ + \(MkSomeLeqNat n m) (MkSomeLeqNat l k) -> + totalWitness $ plusMonotone n m l k Witness Witness + , testCase "leqZeroElim terminates" $ + leqZeroElim (sNat @0) Witness @?= Refl + , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusMonotoneL terminates" $ + \(MkSomeLeqNat n m) (SomeSNat l) -> + totalWitness $ plusMonotoneL n m l Witness + , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusMonotoneR terminates" $ + \(MkSomeLeqNat n m) (SomeSNat l) -> + totalWitness $ plusMonotoneR l n m Witness + , testProperty @(SomeSNat -> SomeSNat -> Property) "plusLeqL terminates" $ + \(SomeSNat n) (SomeSNat m) -> + totalWitness $ plusLeqL n m + , testProperty @(SomeSNat -> SomeSNat -> Property) "plusLeqR terminates" $ + \(SomeSNat n) (SomeSNat m) -> + totalWitness $ plusLeqR n m + , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusCancelLeqL terminates" $ + \(MkSomeLeqNat (m :: SNat m) (l :: SNat l)) (SomeSNat n) -> + totalWitness $ + plusCancelLeqR + n + m + l + (unsafeCoerce (Witness :: IsTrue (m <=? l))) + , testProperty @(SomeLeqNat -> SomeSNat -> Property) "plusCancelLeqR terminates" $ + \(MkSomeLeqNat (n :: SNat n) (m :: SNat m)) (SomeSNat l) -> + totalWitness $ + plusCancelLeqR + n + m + l + (unsafeCoerce (Witness :: IsTrue (n <=? m))) + , testProperty @(SomeSNat -> Property) "succLeqZeroAbsurd works properly" $ \(SomeSNat n) -> + givesImpossibleVoid $ succLeqZeroAbsurd n (unsafeCoerce Witness) + , testProperty @(SomeSNat -> Property) "succLeqZeroAbsurd' works properly" $ \(SomeSNat n) -> + totalRefl $ succLeqZeroAbsurd' n + , testProperty @(SomeSNat -> Property) "succLeqAbsurd works properly" $ \(SomeSNat n) -> + givesImpossibleVoid $ succLeqAbsurd n (unsafeCoerce Witness) + , testProperty @(SomeSNat -> Property) "succLeqAbsurd' works properly" $ \(SomeSNat n) -> + totalRefl $ succLeqAbsurd' n + , testProperty @(SomeGtNat -> Property) + "notLeqToLeq terminates" + $ \(MkSomeGtNat n m) -> + case n %<=? m of + STrue -> error "impossible!" + SFalse -> + totalWitness $ notLeqToLeq n m + , testProperty + @(SomeSNat -> SomeSNat -> Property) + "leqSucc' terminates" + $ \(SomeSNat n) (SomeSNat m) -> + totalRefl $ leqSucc' n m + , testProperty @(SomeLeqNat -> Property) "leqToMin terminates" $ + \(MkSomeLeqNat n m) -> + totalRefl $ leqToMin n m Witness + , testProperty @(SomeLeqNat -> Property) "geqToMin terminates" $ + \(MkSomeLeqNat n m) -> + totalRefl $ geqToMin m n Witness + , testProperty @(SomeSNat -> SomeSNat -> Property) "minComm terminates" $ + \(SomeSNat n) (SomeSNat m) -> + totalRefl $ minComm n m + , testProperty @(SomeSNat -> SomeSNat -> Property) "minLeqL terminates" $ + \(SomeSNat n) (SomeSNat m) -> + totalWitness $ minLeqL n m + , testProperty @(SomeSNat -> SomeSNat -> Property) "minLeqR terminates" $ + \(SomeSNat n) (SomeSNat m) -> + totalWitness $ minLeqR n m + , testProperty @(SomeLeqNat -> SomeSNat -> Property) "minLargest terminates" $ + \(MkSomeLeqNat l n) (SomeSNat lm) -> + let m = l %+ lm + in totalWitness $ + minLargest l n m Witness (unsafeCoerce Witness) + , testProperty @(SomeLeqNat -> Property) "leqToMax termaxates" $ + \(MkSomeLeqNat n m) -> + totalRefl $ leqToMax n m Witness + , testProperty @(SomeLeqNat -> Property) "geqToMax termaxates" $ + \(MkSomeLeqNat n m) -> + totalRefl $ geqToMax m n Witness + , testProperty @(SomeSNat -> SomeSNat -> Property) "maxComm termaxates" $ + \(SomeSNat n) (SomeSNat m) -> + totalRefl $ maxComm n m + , testProperty @(SomeSNat -> SomeSNat -> Property) "maxLeqL termaxates" $ + \(SomeSNat n) (SomeSNat m) -> + totalWitness $ maxLeqL n m + , testProperty @(SomeSNat -> SomeSNat -> Property) "maxLeqR termaxates" $ + \(SomeSNat n) (SomeSNat m) -> + totalWitness $ maxLeqR n m + , testProperty @(SomeLeqNat -> Property) "maxLeast termaxates" $ + \(MkSomeLeqNat n l) -> + forAll (elements [0 .. fromSNat l]) $ \m0 -> + case toSomeSNat m0 of + SomeSNat m -> + totalWitness $ + maxLeast l n m Witness (unsafeCoerce Witness) + , testProperty @(SomeSNat -> SomeSNat -> Property) "lneqSuccLeq terminates" $ + \(SomeSNat n) (SomeSNat m) -> + totalRefl $ lneqSuccLeq n m + , testProperty @(SomeSNat -> SomeSNat -> Property) "lneqReversed terminates" $ + \(SomeSNat n) (SomeSNat m) -> + totalRefl $ lneqReversed n m + , testProperty @(SomeLneqNat -> Property) "lneqToLT terminates" $ + \(MkSomeLneqNat n m) -> + totalRefl $ lneqToLT n m Witness + , testProperty @(SomeLtNat -> Property) "ltToLneq terminates" $ + \(MkSomeLtNat n m) -> + totalWitness $ ltToLneq n m Refl + , testProperty @(SomeSNat -> Property) "lneqZero terminates" $ + \(SomeSNat n) -> totalWitness $ lneqZero n + , testProperty @(SomeSNat -> Property) "lneqSucc terminates" $ + \(SomeSNat n) -> totalWitness $ lneqSucc n + , testProperty @(SomeSNat -> SomeSNat -> Property) "succLneqSucc terminates" $ + \(SomeSNat n) (SomeSNat m) -> totalRefl $ succLneqSucc n m + , testProperty @(SomeLneqNat -> Property) "lneqRightPredSucc terminates" $ + \(MkSomeLneqNat n m) -> + totalRefl $ lneqRightPredSucc n m Witness + , testProperty @(SomeLneqNat -> Property) "lneqSuccStepL and lneqSuccStepR works properly" $ + \(MkSomeLneqNat n m) -> + conjoin + [ totalWitness (lneqSuccStepR n m Witness) + , case n of + Succ n' -> + label "lneqSuccStepL checked" $ + totalWitness (lneqSuccStepL n' m Witness) + Zero -> property True + ] + , testProperty @(SomeLneqNat -> SomeLneqNat -> Property) + "plusStrictMonotone terminates" + $ \(MkSomeLneqNat n m) (MkSomeLneqNat l k) -> + totalWitness $ + plusStrictMonotone n m l k Witness Witness + , testProperty @(SomeSNat -> Property) "maxZeroL terminates" $ + \(SomeSNat n) -> totalRefl $ maxZeroL n + , testProperty @(SomeSNat -> Property) "maxZeroR terminates" $ + \(SomeSNat n) -> totalRefl $ maxZeroR n + , testProperty @(SomeSNat -> Property) "minZeroL terminates" $ + \(SomeSNat n) -> totalRefl $ minZeroL n + , testProperty @(SomeSNat -> Property) "minZeroR terminates" $ + \(SomeSNat n) -> totalRefl $ minZeroR n + , testProperty @(SomeLeqNat -> Property) "minusSucc terminates" $ + \(MkSomeLeqNat m n) -> + totalRefl $ minusSucc n m Witness + , testProperty @(SomeSNat -> Property) "lneqZeroAbsurd is absurd" $ + \(SomeSNat n) -> + givesImpossibleVoid $ + lneqZeroAbsurd n $ unsafeCoerce Witness + , testProperty @(SomeLeqNat -> Property) + "minusPlus terminates" + $ \(MkSomeLeqNat m n) -> + totalRefl $ + minusPlus n m Witness + , testProperty @(SomeSNat -> SomeSNat -> Property) + "minPlusTruncMinus terminates" + $ \(SomeSNat n) (SomeSNat m) -> + totalRefl $ minPlusTruncMinus n m + , testProperty @(SomeSNat -> SomeSNat -> Property) + "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 +totalWitness w = + counterexample "Witness is not totalRefl!" $ + within + 10000 + ( (case w of Witness -> True :: Bool) :: + Bool + ) + +totalRefl :: a :~: b -> Property +totalRefl = within 10000 . total diff --git a/tests/Data/Type/Natural/Presburger/Cases.hs b/tests/Data/Type/Natural/Presburger/Cases.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/Natural/Presburger/Cases.hs @@ -0,0 +1,27 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -fdefer-type-errors #-} +{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-} + +module Data.Type.Natural.Presburger.Cases where + +import Data.Proxy (Proxy (Proxy)) +import Data.Type.Equality +import Data.Type.Natural +import GHC.TypeNats + +minFlip :: n <= m => p n -> q m -> Min m n :~: n +minFlip _ _ = Refl + +maxFlip :: n <= m => p n -> q m -> Max m n :~: m +maxFlip _ _ = Refl + +minComm :: q m -> p n -> Min n m :~: Min m n +minComm _ _ = Refl + +maxComm :: q m -> p n -> Max n m :~: Max m n +maxComm _ _ = Refl + +falsity :: n <= m => p n -> q m -> Min n m :~: m +falsity _ _ = Refl diff --git a/tests/Data/Type/Natural/Presburger/MinMaxSolverSpec.hs b/tests/Data/Type/Natural/Presburger/MinMaxSolverSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/Natural/Presburger/MinMaxSolverSpec.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Data.Type.Natural.Presburger.MinMaxSolverSpec where + +import Control.Exception +import Control.Monad +import Data.Type.Equality +import Data.Type.Natural +import Data.Type.Natural.Presburger.Cases +import Shared +import Test.QuickCheck (ioProperty) +import Test.Tasty +import Test.Tasty.HUnit +import Test.Tasty.QuickCheck +import Unsafe.Coerce (unsafeCoerce) + +test_MinMaxSolver :: TestTree +test_MinMaxSolver = + testGroup + "Data.Type.Natural.Presburger.MinMaxSolver" + [ testProperty @(SomeLeq -> Property) "rejects errornousInputs" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ falsity n m + case eith of + Left {} -> pure True + Right {} -> pure False + , testProperty @(SomeLeq -> Property) "minFlip" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ minFlip n m + case eith of + Left {} -> pure False + Right {} -> pure True + , testProperty @(SomeLeq -> Property) "maxFlip" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ maxFlip n m + case eith of + Left {} -> pure False + Right {} -> pure True + , testProperty @(SomeLeq -> Property) "maxComm" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ maxComm n m + case eith of + Left {} -> pure False + Right {} -> pure True + , testProperty @(SomeLeq -> Property) "minComm" $ \case + (SomeLeq n m) -> ioProperty @Bool $ do + eith <- try @TypeError $ void $ evaluate $ minComm n m + case eith of + Left {} -> pure False + Right {} -> pure True + ] + +data SomeLeq where + SomeLeq :: n <= m => SNat n -> SNat m -> SomeLeq + +deriving instance Show SomeLeq + +instance Arbitrary SomeLeq where + arbitrary = do + n <- arbitrary + dn <- arbitrary + withSNat n $ + withSNat (n + dn) $ \(sn :: SNat n) (sm :: SNat m) -> + gcastWith (unsafeCoerce (Refl @()) :: (n <=? m) :~: 'True) $ + pure (SomeLeq sn sm) diff --git a/tests/Data/Type/NaturalSpec.hs b/tests/Data/Type/NaturalSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/NaturalSpec.hs @@ -0,0 +1,124 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} + +module Data.Type.NaturalSpec where + +import Data.Type.Natural +import Data.Type.NaturalSpec.TH +import Math.NumberTheory.Logarithms (naturalLog2, naturalLogBase) +import Numeric.Natural +import GHC.TypeNats +import Shared +import Test.Tasty +import Test.Tasty.QuickCheck +import Test.QuickCheck +import Control.Monad (join) + +test_arith :: TestTree +test_arith = + testGroup + "Arithmetic operations on singletons behaves correctly" + [ testProperty "(+), compared to demoted" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [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 .&&. 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] $ + 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) + .||. 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) + .||. 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] $ + 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] $ + 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) + .||. fromSNat (sLog2 n) === fromIntegral (naturalLog2 (natVal n)) + , $(testUnary False "Log2" ''Log2 'sLog2) + , testProperty "succ" $ \(SomeSNat n) -> + tabulateDigits [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) + .||. fromSNat (sPred n) === pred (natVal n) + , $(testUnary False "Pred" ''Pred 'sPred) + ] + +demoteBool :: SBool b -> Bool +demoteBool SFalse = False +demoteBool STrue = True + +demoteOrdering :: SOrdering sord -> Ordering +demoteOrdering SLT = LT +demoteOrdering SEQ = EQ +demoteOrdering SGT = GT + +test_order :: TestTree +test_order = + testGroup + "Order operations on singletons coincides with expression-leven ops" + [ testProperty "(<=?)" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + demoteBool (n %<=? m) === (natVal n <= natVal m) + , $(testBinary "(<=?)" ''(<=?) '(%<=?)) + , testProperty "( + tabulateDigits [natVal n, natVal m] $ + demoteBool (n %=?)" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + demoteBool (n %>=? m) === (natVal n >= natVal m) + , $(testBinary "(>=?)" ''(>=?) '(%>=?)) + , testProperty "(>?)" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + demoteBool (n %>? m) === (natVal n > natVal m) + , $(testBinary "(>?)" ''(>?) '(%>?)) + , testProperty "sCmpNat" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, natVal m] $ + demoteOrdering (n `sCmpNat` m) === compare (natVal n) (natVal m) + , $(testBinary "CmpNat" ''CmpNat 'sCmpNat) + , testProperty "min" $ \(SomeSNat n) (SomeSNat m) -> + tabulateDigits [natVal n, 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] $ + fromSNat (n `sMax` m) === (natVal n `max` natVal m) + , $(testBinary "max" ''Max 'sMax) + ] + +tabulateDigits :: Testable prop => [Natural] -> prop -> Property +tabulateDigits = +#if MIN_VERSION_QuickCheck(2,12,0) + tabulate + "# of input digits" + . map (show . succ . naturalLogBase 10 . (+ 1)) +#else + const property +#endif diff --git a/tests/Data/Type/NaturalSpec/TH.hs b/tests/Data/Type/NaturalSpec/TH.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/NaturalSpec/TH.hs @@ -0,0 +1,56 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} + +module Data.Type.NaturalSpec.TH where + +import Data.Type.Natural +import Language.Haskell.TH +import Numeric.Natural +import Shared +import Test.Tasty +import Test.Tasty.HUnit + +allCombs :: [(Integer, Integer)] +allCombs = [(n, m) | n <- range, m <- range] + +range :: [Integer] +range = [0] ++ [50] ++ [63 .. 65] ++ [98, 99, 100, 200] ++ [1024, 1023, 1025] + +testUnary :: Bool -> String -> Name -> Name -> ExpQ +testUnary allowZero label tyName singName = + [|testCase (label ++ ", compared to fixed type-level")|] + `appE` doE + [ noBindS + [| + demote ($(varE singName) (sNat @($tyN))) + @?= demote (sing @($(conT tyName) $tyN)) + |] + | nat <- range + , let tyN = litT $ numTyLit nat + , allowZero || nat /= 0 + ] + +testBinary :: String -> Name -> Name -> ExpQ +testBinary = testBinaryP (const $ const True) + +testBinaryP :: (Integer -> Integer -> Bool) -> String -> Name -> Name -> ExpQ +testBinaryP ok label tyName singName = + [|testCase (label ++ ", compared to fixed type-level")|] + `appE` doE + [ noBindS + [| + demote ($(varE singName) (sNat @($tyL)) (sNat @($tyR))) + @?= demote (sing @($(conT tyName) $tyL $tyR)) + |] + | l <- range + , let tyL = litT $ numTyLit l + , r <- range + , let tyR = litT $ numTyLit r + , ok l r + ] + +-- >>> length allCombs +-- 289 diff --git a/tests/Data/Type/OrdinalSpec.hs b/tests/Data/Type/OrdinalSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Type/OrdinalSpec.hs @@ -0,0 +1,1 @@ +module Data.Type.OrdinalSpec where diff --git a/tests/Shared.hs b/tests/Shared.hs new file mode 100644 --- /dev/null +++ b/tests/Shared.hs @@ -0,0 +1,84 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Shared where + +import Data.Kind (Type) +import Data.Type.Natural +import Data.Type.Ordinal +import GHC.TypeNats +import Numeric.Natural +import Test.QuickCheck +import Test.QuickCheck.Instances () + +instance (KnownNat n, 0 < n) => Arbitrary (Ordinal n) where + arbitrary = elements $ enumOrdinal sNat + shrink 0 = [] + shrink n = [0 .. pred n] + +instance Arbitrary SomeNat where + arbitrary = sized $ \n -> someNatVal <$> resize n arbitrary + shrink (SomeNat pn) = + someNatVal <$> shrink (natVal pn) + +instance Arbitrary SomeSNat where + arbitrary = sized $ \n -> toSomeSNat <$> resize n arbitrary + shrink (SomeSNat pn) = + toSomeSNat <$> shrink (natVal pn) + +type family Sing = (r :: k -> Type) + +class Demote k where + type Demoted k + type Demoted k = k + demote :: Sing (a :: k) -> Demoted k + +class Known a where + sing :: Sing a + +instance KnownNat n => Known n where + sing = sNat + +instance Known 'True where + sing = STrue + +instance Known 'False where + sing = SFalse + +instance Known 'LT where + sing = SLT + +instance Known 'GT where + sing = SGT + +instance Known 'EQ where + sing = SEQ + +type instance Sing = SNat + +instance Demote Nat where + type Demoted Nat = Natural + demote = fromSNat + +type instance Sing = SOrdering + +instance Demote Ordering where + demote SLT = LT + demote SEQ = EQ + demote SGT = GT + +type instance Sing = SBool + +instance Demote Bool where + demote STrue = True + demote SFalse = False diff --git a/tests/test.hs b/tests/test.hs new file mode 100644 --- /dev/null +++ b/tests/test.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-} diff --git a/type-natural.cabal b/type-natural.cabal --- a/type-natural.cabal +++ b/type-natural.cabal @@ -1,55 +1,114 @@ --- Initial type-natural.cabal generated by cabal init. For further --- documentation, see http://haskell.org/cabal/users-guide/ +cabal-version: 3.0 +name: type-natural +version: 1.3.0.2 +license: BSD-3-Clause +license-file: LICENSE +copyright: (C) Hiromi ISHII 2013-2024 +maintainer: konn.jinro_at_gmail.com +author: Hiromi ISHII +tested-with: ghc ==9.2.8 || ==9.4.8 || ==9.6.5 || ==9.8.4 || ==9.10.1 +homepage: https://github.com/konn/type-natural +synopsis: Type-level natural and proofs of their properties. +description: + Type-level natural numbers and proofs of their properties. -name: type-natural -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 -license: BSD3 -license-file: LICENSE -author: Hiromi ISHII -maintainer: konn.jinro_at_gmail.com -copyright: (C) Hiromi ISHII 2013-2014 -category: Math -build-type: Simple -cabal-version: >= 1.10 -tested-with: GHC == 7.10.3, GHC == 8.0.1 +category: Math +build-type: Simple +extra-source-files: Changelog.md source-repository head - Type: git - Location: git://github.com/konn/type-natural.git - + type: git + location: git://github.com/konn/type-natural.git library - ghc-options: -Wall -O2 -fno-warn-orphans - if impl(ghc >= 8.0.0) - ghc-options: -Wno-redundant-constraints - exposed-modules: Data.Type.Natural - , Data.Type.Ordinal - , Data.Type.Natural.Builtin - other-modules: Data.Type.Natural.Definitions - , Data.Type.Natural.Core - , Data.Type.Natural.Compat - build-depends: base >= 4 && < 5 - , equational-reasoning == 0.4.* - , monomorphic >= 0.0.3 - , template-haskell >= 2.8 && < 3 - , constraints >= 0.3 && < 0.9 - , ghc-typelits-natnormalise == 0.4.* - , ghc-typelits-presburger == 0.1.* - , singletons >= 2.0 && < 2.3 + -- cabal-gild: discover src --exclude src/**/Core.hs --exclude src/**/Utils.hs --exclude src/Data/Type/Natural/Lemma/Presburger.hs + exposed-modules: + Data.Type.Natural + Data.Type.Natural.Builtin + Data.Type.Natural.Lemma.Arithmetic + Data.Type.Natural.Lemma.Order + Data.Type.Natural.Presburger.MinMaxSolver + Data.Type.Ordinal + Data.Type.Ordinal.Builtin - default-language: Haskell2010 - default-extensions: DataKinds - PolyKinds - ConstraintKinds - GADTs - ScopedTypeVariables - TemplateHaskell - TypeFamilies - TypeOperators - MultiParamTypeClasses - UndecidableInstances - FlexibleContexts - FlexibleInstances + hs-source-dirs: src + other-modules: + Data.Type.Natural.Core + Data.Type.Natural.Lemma.Presburger + Data.Type.Natural.Utils + + default-language: Haskell2010 + default-extensions: + ConstraintKinds + DataKinds + FlexibleContexts + FlexibleInstances + GADTs + MultiParamTypeClasses + PolyKinds + ScopedTypeVariables + TemplateHaskell + TypeFamilies + TypeOperators + UndecidableInstances + + default-extensions: NoStarIsType + ghc-options: + -Wall + -Wno-orphans + -Wno-redundant-constraints + + build-depends: + base >=4 && <5, + constraints >=0.3, + equational-reasoning >=0.4.1.1, + ghc, + ghc-typelits-knownnat, + ghc-typelits-natnormalise >=0.4, + integer-logarithms, + template-haskell >=2.8, + + if impl(ghc >=9.8.4) + build-depends: ghc-typelits-presburger >=0.7.4.1 + else + if impl(ghc >=9.8) + build-depends: ghc-typelits-presburger >=0.7.3 + else + if impl(ghc >=9.6) + build-depends: ghc-typelits-presburger >=0.7.2 + else + if impl(ghc >=9.4) + build-depends: ghc-typelits-presburger >=0.7.1 + else + build-depends: ghc-typelits-presburger + +test-suite type-natural-test + type: exitcode-stdio-1.0 + main-is: test.hs + build-tool-depends: tasty-discover:tasty-discover + hs-source-dirs: tests + default-language: Haskell2010 + ghc-options: -Wall + other-modules: + Data.Type.Natural.Lemma.OrderSpec + Data.Type.Natural.Presburger.Cases + Data.Type.Natural.Presburger.MinMaxSolverSpec + Data.Type.NaturalSpec + Data.Type.NaturalSpec.TH + Data.Type.OrdinalSpec + Shared + + build-depends: + QuickCheck, + base, + equational-reasoning, + integer-logarithms, + quickcheck-instances, + tasty, + tasty-discover, + tasty-hunit, + tasty-quickcheck, + template-haskell, + type-natural, + + default-extensions: NoStarIsType