type-natural 0.8.2.0 → 0.8.3.0
raw patch · 7 files changed
+45/−29 lines, 7 filesdep ~ghc-typelits-presburgerdep ~singletons
Dependency ranges changed: ghc-typelits-presburger, singletons
Files
- Data/Type/Natural/Builtin.hs +11/−8
- Data/Type/Natural/Class/Arithmetic.hs +20/−16
- Data/Type/Natural/Definitions.hs +0/−1
- Data/Type/Ordinal.hs +2/−0
- Data/Type/Ordinal/Builtin.hs +1/−0
- Data/Type/Ordinal/Peano.hs +1/−0
- type-natural.cabal +10/−4
Data/Type/Natural/Builtin.hs view
@@ -376,13 +376,16 @@ {-# SPECIALISE instance PeanoOrder TL.Nat #-} eqlCmpEQ _ _ Refl = Refl ltToLeq _ _ Refl = Witness- succLeqToLT m n Witness =- case sCompare (sSucc m) n of- SLT -> Refl- SEQ -> Refl-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800- _ -> bugInGHC-#endif+ succLeqToLT n m w = case sCompare n m of+ SEQ -> eliminate $+ start SLT === sCompare n m `because` sym (leqToLT n m w)+ === sFlipOrdering (sCompare n m) `because` sym (flipCompare n m)+ =~= SEQ+ SGT -> eliminate $+ start SLT === sCompare n m `because` sym (leqToLT n m w)+ =~= SGT+ SLT -> Refl+ cmpZero _ = Refl leqRefl _ = Witness eqToRefl _ _ Refl = Refl@@ -397,7 +400,7 @@ leqToMin _ _ Witness = Refl leqToMax _ _ Witness = Refl- geqToMax n m mLEQn =+ geqToMax n m mLEQn@Witness = case leqToCmp m n mLEQn of Left eql -> withRefl eql Refl Right mLTn ->
Data/Type/Natural/Class/Arithmetic.hs view
@@ -1,8 +1,8 @@-{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-}+{-# LANGUAGE CPP, DataKinds, EmptyCase, ExplicitForAll, ExplicitNamespaces #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies #-}-{-# LANGUAGE TypeInType, ViewPatterns , ExplicitNamespaces #-}+{-# LANGUAGE TypeInType, ViewPatterns #-} module Data.Type.Natural.Class.Arithmetic (Zero, One, S, sZero, sOne, ZeroOrSucc(..), plusCong, plusCongR, plusCongL, succCong,@@ -11,22 +11,25 @@ IsPeano(..), pattern Zero, pattern Succ, module Data.Type.Natural.Singleton.Compat ) where-import Data.Type.Natural.Singleton.Compat- (type (/=), type (==), type (+), type (*), type (-)- ,type (/=@#@$) ,type (/=@#@$$), type (/=@#@$$$)- ,type (==@#@$) ,type (==@#@$$), type (==@#@$$$)- ,type (+@#@$) ,type (+@#@$$), type (+@#@$$$)- ,type (*@#@$) ,type (*@#@$$), type (*@#@$$$)- ,type (-@#@$) ,type (-@#@$$), type (-@#@$$$)- ,(%==), (%/=), (%+), (%*), (%-)- , FromInteger, FromIntegerSym0, FromIntegerSym1- ,SNum(..), PNum(..)- )+import Data.Type.Natural.Singleton.Compat (type (*), type (*@#@$),+ type (*@#@$$), type (*@#@$$$),+ type (+), type (+@#@$),+ type (+@#@$$), type (+@#@$$$),+ type (-), type (-@#@$),+ type (-@#@$$), type (-@#@$$$),+ type (/=), type (/=@#@$),+ type (/=@#@$$), type (/=@#@$$$),+ type (==), type (==@#@$),+ type (==@#@$$), type (==@#@$$$),+ FromInteger, FromIntegerSym0,+ FromIntegerSym1, PNum (..),+ SNum (..), (%*), (%+), (%-), (%/=),+ (%==)) import Data.Functor.Const (Const (..)) import Data.Singletons.Decide (SDecide (..))-import Data.Singletons.Prelude (Apply, SingI (..), SingKind (..),- SomeSing (..), Sing)+import Data.Singletons.Prelude (Apply, Sing, SingI (..), SingKind (..),+ SomeSing (..)) import Data.Singletons.Prelude.Enum (Pred, SEnum (..), Succ, sPred, sSucc) import Data.Type.Equality ((:~:) (..)) import Data.Void (Void, absurd)@@ -570,3 +573,4 @@ pattern Succ n <- (zeroOrSucc -> IsSucc n) where Succ n = sSucc n +{-# COMPLETE Zero, Succ #-}
Data/Type/Natural/Definitions.hs view
@@ -10,7 +10,6 @@ ) where import Data.Type.Natural.Singleton.Compat -import Data.Promotion.Prelude.Enum import Data.Singletons.Prelude import Data.Singletons.Prelude.Enum import Data.Singletons.TH
Data/Type/Ordinal.hs view
@@ -56,6 +56,8 @@ data Ordinal (n :: nat) where OLt :: (IsPeano nat, (n < m) ~ 'True) => Sing (n :: nat) -> Ordinal m +{-# COMPLETE OLt #-}+ fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n < Succ m) ~ 'True, SingI m) => Sing (n :: nat) -> Ordinal m fromOLt n =
Data/Type/Ordinal/Builtin.hs view
@@ -50,6 +50,7 @@ pattern OLt :: () => forall (n1 :: Nat). ((n1 SC.< t) ~ 'True) => Sing n1 -> O.Ordinal t pattern OLt n = O.OLt n+{-# COMPLETE OLt #-} -- | Pattern synonym representing the 0-th ordinal. --
Data/Type/Ordinal/Peano.hs view
@@ -49,6 +49,7 @@ pattern OLt :: () => forall (n1 :: Nat). ((n1 < t) ~ 'True) => Sing n1 -> O.Ordinal t pattern OLt n = O.OLt n+{-# COMPLETE OLt #-} -- | Pattern synonym representing the 0-th ordinal. --
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.8.2.0+version: 0.8.3.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. .@@ -18,7 +18,7 @@ category: Math build-type: Simple cabal-version: >= 1.10-tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3+tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.3, GHC == 8.6.3, GHC == 8.8.2 source-repository head Type: git@@ -29,6 +29,7 @@ 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.Ordinal.Builtin@@ -46,8 +47,7 @@ , template-haskell >= 2.8 , constraints >= 0.3 , ghc-typelits-natnormalise >= 0.4- , ghc-typelits-presburger >= 0.2.0.0- , singletons >= 2.2 && < 2.5+ , singletons >= 2.2 && < 2.6 default-language: Haskell2010 default-extensions: DataKinds@@ -62,3 +62,9 @@ UndecidableInstances FlexibleContexts FlexibleInstances+ if impl(ghc >= 8.6)+ default-extensions: NoStarIsType+ if impl(ghc >= 8.4)+ build-depends: ghc-typelits-presburger >= 0.3 && <0.4+ else+ build-depends: ghc-typelits-presburger >= 0.2 && <0.3