type-natural 0.8.3.0 → 0.8.3.1
raw patch · 5 files changed
+50/−10 lines, 5 filesdep +singletons-presburgerdep ~singletons
Dependencies added: singletons-presburger
Dependency ranges changed: singletons
Files
- Data/Type/Natural.hs +8/−3
- Data/Type/Natural/Builtin.hs +10/−1
- Data/Type/Natural/Class/Order.hs +17/−3
- Data/Type/Natural/Singleton/Compat.hs +11/−2
- type-natural.cabal +4/−1
Data/Type/Natural.hs view
@@ -11,7 +11,12 @@ Nat(..), SSym0, SSym1, ZSym0, -- | Singleton type for 'Nat'.- SNat, Sing (SZ, SS),+ SNat,+#if MIN_VERSION_singletons(2,6,0)+ SNat (SZ, SS),+#else+ Sing(SZ,SS),+#endif -- ** Arithmetic functions and their singletons. min, Min, sMin, max, Max, sMax, MinSym0, MinSym1, MinSym2,@@ -23,7 +28,7 @@ (%*), type (-), type (**), (%**), type (-@#@$), type (-@#@$$), type (-@#@$$$),- (%-), + (%-), -- ** Type-level predicate & judgements Leq(..), type (<=), LeqInstance, boolToPropLeq, boolToClassLeq, propToClassLeq,@@ -69,8 +74,8 @@ import Data.Type.Natural.Core import Data.Type.Natural.Definitions hiding (type (<=)) import Data.Void+import Language.Haskell.TH (appE, appT, conE, conP, conT) import Language.Haskell.TH.Quote-import Language.Haskell.TH (conT, appT, conP, conE, appE) import Proof.Equational import Proof.Propositional hiding (Not)
Data/Type/Natural/Builtin.hs view
@@ -2,7 +2,11 @@ {-# LANGUAGE FlexibleContexts, GADTs, InstanceSigs, PolyKinds, RankNTypes #-} {-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+#if MIN_VERSION_singletons(2,6,0)+{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-}+#else {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}+#endif {-# 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@@ -35,14 +39,19 @@ import Data.Singletons.Decide (SDecide (..)) import Data.Singletons.Decide (Decision (..))-import Data.Singletons.Prelude (Sing (..), SingKind(..))+import Data.Singletons.Prelude (Sing (..), SingKind(..), SBool(..)) import Data.Singletons.Prelude (SingI (..)) import Data.Singletons.Prelude.Enum (PEnum (..), SEnum (..)) import Data.Singletons.Prelude.Ord (POrd (..), SOrd (..)) import Data.Singletons.TH (sCases) import Data.Singletons.TypeLits (withKnownNat) import Data.Type.Equality ((:~:) (..))+#if MIN_VERSION_singletons(2,6,0)+import Data.Type.Natural (Nat (S, Z), SNat (SS, SZ))+#else import Data.Type.Natural (Nat (S, Z), Sing (SS, SZ))+#endif+ import qualified Data.Type.Natural as PN import Data.Void (absurd) import Data.Void (Void)
Data/Type/Natural/Class/Order.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces #-}+{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces #-} {-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-}@@ -21,11 +21,25 @@ type MinSym0, type MinSym1, type MinSym2, type MaxSym0, type MaxSym1, type MaxSym2, type CompareSym0, type CompareSym1, type CompareSym2,- Sing (SLT, SEQ, SGT), SOrd(..), POrd(..),+#if MIN_VERSION_singletons(2,6,0)+ SOrdering (SLT, SEQ, SGT),+#else+ Sing (SLT, SEQ, SGT),+#endif++ SOrd(..), POrd(..), LTSym0, GTSym0, EQSym0, (%<), (%<=), (%>), (%>=)) -import Data.Singletons.Prelude (Sing (SFalse, STrue), sing, withSingI)+import Data.Singletons.Prelude+ (Sing,+#if MIN_VERSION_singletons(2,6,0)+ SBool (SFalse, STrue),+#else+ Sing (SFalse, STrue),+#endif+ sing, withSingI+ ) import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ) import Data.Singletons.TH (singletonsOnly) import Data.Type.Equality ((:~:) (..))
Data/Type/Natural/Singleton/Compat.hs view
@@ -4,15 +4,24 @@ ( module Data.Singletons.Prelude.Eq, module Data.Singletons.Prelude.Num,- module Data.Singletons.Prelude.Ord,+ module Data.Singletons.Prelude.Ord+#if MIN_VERSION_singletons(2,6,0)+ ,SOrdering(..)+#endif #if !MIN_VERSION_singletons(2,4,0)- module Data.Type.Natural.Singleton.Compat+ ,module Data.Type.Natural.Singleton.Compat #endif ) where #if !MIN_VERSION_singletons(2,4,0) import Data.Type.Natural.Singleton.Compat.TH+#endif++#if MIN_VERSION_singletons(2,6,0)+import Data.Singletons.Prelude (SOrdering (SEQ, SGT, SLT))+#else+ #endif import Data.Singletons.Prelude.Eq
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.8.3.0+version: 0.8.3.1 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. .@@ -64,6 +64,9 @@ FlexibleInstances if impl(ghc >= 8.6) default-extensions: NoStarIsType+ if impl(ghc >= 8.8)+ default-extensions: NoStarIsType, TypeApplications+ build-depends: singletons-presburger >= 0.3 && <0.4 if impl(ghc >= 8.4) build-depends: ghc-typelits-presburger >= 0.3 && <0.4 else