tfp 0.6 → 0.7
raw patch · 7 files changed
+113/−26 lines, 7 filesnew-uploader
Files
- LICENSE +1/−0
- Test.hs +9/−0
- Types/Data/Num.hs +5/−0
- Types/Data/Num/Decimal/Ops.hs +16/−0
- Types/Data/Num/Ops.hs +33/−2
- Types/Data/Ord.hs +17/−0
- tfp.cabal +32/−24
LICENSE view
@@ -1,3 +1,4 @@+Copyright (c) 2013 Henning Thielemann Copyright (c) 2008 Peter Gavin All rights reserved.
Test.hs view
@@ -220,6 +220,15 @@ testMax3 :: Max D6 D1 -> D6 testMax3 = Prelude.id +testLog1 :: Log2Ceil D8 -> D3+testLog1 = Prelude.id+testLog2 :: Log2Ceil D9 -> D4+testLog2 = Prelude.id+testLog3 :: Log2Ceil D2 -> D1+testLog3 = Prelude.id+testLog4 :: Log2Ceil D1 -> D0+testLog4 = Prelude.id+ class TestIter n zero where testIter :: n -> zero -> Prelude.String
Types/Data/Num.hs view
@@ -20,6 +20,7 @@ , reifyIntegralD , reifyPositiveD , reifyNegativeD+ , reifyNaturalD #endif ) where @@ -47,4 +48,8 @@ reifyNegativeD :: Integer -> (forall s. (NegativeT s, Repr s ~ Decimal) => s -> a) -> Maybe a #endif reifyNegativeD = reifyNegative decimal+#if __GLASGOW_HASKELL__ >= 704+reifyNaturalD :: Integer -> (forall s. (NaturalT s, Repr s ~ Decimal) => s -> a) -> Maybe a+#endif+reifyNaturalD = reifyNatural decimal #endif
Types/Data/Num/Decimal/Ops.hs view
@@ -135,6 +135,13 @@ type instance IsNegative' DecN = False type instance IsNegative' (xh :. xl) = False +-- type family IsNatural x+type instance IsNatural (Dec x) = IsNatural' x+type family IsNatural' x+type instance IsNatural' (Neg' x) = False+type instance IsNatural' DecN = True+type instance IsNatural' (xh :. xl) = True+ -- type family Neg x type instance Neg (Dec DecN) = Dec DecN type instance Neg (Dec (Neg' x)) = Dec x@@ -761,6 +768,15 @@ type instance Pow2' (Neg' x) y = DecN type instance Pow2' DecN y = y type instance Pow2' (xh :. xl) y = Pow2' (Pred' (xh :. xl)) (Mul2' y)++---------------+-- Logarithm+type instance Log2Ceil (Dec x) = Dec (Log2C' (Pred' x) DecN)++type family Log2C' x y+type instance Log2C' (Neg' x) y = DecN+type instance Log2C' DecN y = y+type instance Log2C' (xh :. xl) y = Log2C' (Div2' (xh :. xl)) (Succ' y) --------------- -- Compare
Types/Data/Num/Ops.hs view
@@ -22,6 +22,8 @@ , isZeroT , IsNegative , isNegativeT+ , IsNatural+ , isNaturalT , Succ , succT , Pred@@ -40,6 +42,8 @@ , mul2T , Pow2 , pow2T+ , Log2Ceil+ , log2CeilT , DivMod , divModT , Div@@ -57,6 +61,7 @@ , NegativeT , reifyPositive , reifyNegative+ , reifyNatural ) where import Types.Data.Bool@@ -82,6 +87,10 @@ isNegativeT :: x -> IsNegative x isNegativeT _ = undefined +type family IsNatural x+isNaturalT :: x -> IsNatural x+isNaturalT _ = undefined+ type family Succ x succT :: x -> Succ x succT _ = undefined@@ -139,9 +148,12 @@ pow2T :: x -> Pow2 x pow2T _ = undefined -class IntegerT x => NaturalT x-instance (IntegerT x, IsNegative x ~ False) => NaturalT x+type family Log2Ceil x+log2CeilT :: x -> Log2Ceil x+log2CeilT _ = undefined +class IntegerT x => NaturalT x+instance (IntegerT x, IsNatural x ~ True) => NaturalT x class IntegerT x => PositiveT x instance (IntegerT x, IsPositive x ~ True) => PositiveT x class IntegerT x => NegativeT x@@ -158,6 +170,7 @@ --- positive and negative assertions: unsafe, in a trusted kernel data AssertPos x data AssertNeg x+data AssertNat x assertPos :: x -> AssertPos x assertPos _ = undefined@@ -165,9 +178,20 @@ assertNeg :: x -> AssertNeg x assertNeg _ = undefined +assertNat :: x -> AssertNat x+assertNat _ = undefined+ type instance IsPositive (AssertPos x) = True+type instance IsPositive (AssertNeg x) = False++type instance IsNegative (AssertPos x) = False type instance IsNegative (AssertNeg x) = True+type instance IsNegative (AssertNat x) = False +type instance IsNatural (AssertPos x) = True+type instance IsNatural (AssertNeg x) = False+type instance IsNatural (AssertNat x) = True+ instance IntegerT x => IntegerT (AssertPos x) where fromIntegerT _ = fromIntegerT (undefined :: x) type Repr (AssertPos x) = Repr x@@ -176,10 +200,17 @@ fromIntegerT _ = fromIntegerT (undefined :: x) type Repr (AssertNeg x) = Repr x +instance IntegerT x => IntegerT (AssertNat x) where+ fromIntegerT _ = fromIntegerT (undefined :: x)+ type Repr (AssertNat x) = Repr x+ reifyPositive :: IntegerR r => r -> Integer -> (forall s. (PositiveT s, Repr s ~ r) => s -> a) -> Maybe a reifyPositive r n k | n > 0 = Just (reifyIntegral r n (k . assertPos)) | otherwise = Nothing reifyNegative :: IntegerR r => r -> Integer -> (forall s. (NegativeT s, Repr s ~ r) => s -> a) -> Maybe a reifyNegative r n k | n < 0 = Just (reifyIntegral r n (k . assertNeg))+ | otherwise = Nothing+reifyNatural :: IntegerR r => r -> Integer -> (forall s. (NaturalT s, Repr s ~ r) => s -> a) -> Maybe a+reifyNatural r n k | n >= 0 = Just (reifyIntegral r n (k . assertNat)) | otherwise = Nothing
Types/Data/Ord.hs view
@@ -26,14 +26,19 @@ , isGTT , (:<:) , ltT+ , LTT , (:<=:) , leT+ , LET , (:==:) , eqT+ , EQT , (:>=:) , geT+ , GET , (:>:) , gtT+ , GTT , Min , minT , Max@@ -86,31 +91,43 @@ type instance x :<: y = IsLT (Compare x y) ltT :: x -> y -> x :<: y ltT _ _ = Prelude.undefined+class LTT x y+instance ((x :<: y) ~ True) => LTT x y type family x :<=: y type instance x :<=: y = Not (x :>: y) leT :: x -> y -> x :<=: y leT _ _ = Prelude.undefined+class LET x y+instance ((x :<=: y) ~ True) => LET x y type family x :==: y type instance x :==: y = IsEQ (Compare x y) eqT :: x -> y -> x :==: y eqT _ _ = Prelude.undefined+class EQT x y+instance ((x :==: y) ~ True) => EQT x y type family x :/=: y type instance x :/=: y = Not (x :==: y) neT :: x -> y -> x :/=: y neT _ _ = Prelude.undefined+class NET x y+instance ((x :/=: y) ~ True) => NET x y type family x :>=: y type instance x :>=: y = Not (x :<: y) geT :: x -> y -> x :>=: y geT _ _ = Prelude.undefined+class GET x y+instance ((x :>=: y) ~ True) => GET x y type family x :>: y type instance x :>: y = IsGT (Compare x y) gtT :: x -> y -> x :>: y gtT _ _ = Prelude.undefined+class GTT x y+instance ((x :>: y) ~ True) => GTT x y type family Min x y type instance Min x y = If (x :<=: y) x y
tfp.cabal view
@@ -1,27 +1,35 @@ name: tfp-version: 0.6-cabal-version: >= 1.6+version: 0.7 build-type: Simple license: BSD3 license-file: LICENSE-copyright: Copyright (c) 2008 Peter Gavin-author: Peter Gavin-maintainer: pgavin@gmail.com-homepage: http://github.com/pgavin/tfp+copyright: Copyright (c) 2013 Henning Thielemann, 2008 Peter Gavin+author: Peter Gavin, Henning Thielemann+maintainer: haskell@henning-thielemann.de+homepage: http://www.haskell.org/haskellwiki/Type_arithmetic stability: alpha-package-url: http://github.com/pgavin/tfp-synopsis: Type-level programming library using type families-description: TFP (short for Type Family Programming) provides implementations of type-level integers and booleans,- and (eventually) simple type-level data structures. It uses type families as functions to produce new types,- which provides an intuitive way to parameterize data types and functions on numerical values at compile time.-category: Data-tested-with: GHC == 6.9.0+synopsis: Type-level integers, booleans, lists using type families+description:+ TFP is an abbreviation for Type Family Programming.+ It provides implementations of type-level integers and booleans,+ and (eventually) simple type-level data structures.+ It uses type families as functions to produce new types,+ which provides an intuitive way to parameterize data types+ and functions on numerical values at compile time.+category: Type System+tested-with: GHC == 7.4.2+cabal-version: >= 1.6 -source-repository head {- type: git- location: git@github.com:pgavin/tfp.git-}+source-repository head+ type: darcs+ location: http://code.haskell.org/~thielema/tfp/ +source-repository this+ tag: 0.7+ type: darcs+ location: http://code.haskell.org/~thielema/tfp/++ flag build-test description: Build the tfp-test test program default: False@@ -34,18 +42,18 @@ Rank2Types, FlexibleContexts build-depends: base >= 3.0 && < 5, template-haskell >= 2.0 exposed-modules:- Data.SizedInt,- Data.SizedWord,- Types,- Types.Base,- Types.Data.Bool,+ Data.SizedInt+ Data.SizedWord+ Types+ Types.Base+ Types.Data.Bool Types.Data.Num Types.Data.Num.Ops- Types.Data.Num.Decimal,+ Types.Data.Num.Decimal Types.Data.Num.Decimal.Literals Types.Data.Num.Decimal.Literals.TH Types.Data.Num.Decimal.Digits- Types.Data.List,+ Types.Data.List Types.Data.Ord other-modules: Types.Data.Num.Decimal.Ops