tfp 0.1 → 0.2
raw patch · 8 files changed
+207/−17 lines, 8 filesdep +QuickCheckdep ~base
Dependencies added: QuickCheck
Dependency ranges changed: base
Files
- Test.hs +96/−8
- Types/Data/Num.hs +7/−0
- Types/Data/Num/Decimal/Digits.hs +4/−0
- Types/Data/Num/Decimal/Literals/TH.hs +20/−4
- Types/Data/Num/Decimal/Ops.hs +22/−0
- Types/Data/Num/Ops.hs +38/−1
- Types/Data/Ord.hs +14/−0
- tfp.cabal +6/−4
Test.hs view
@@ -1,12 +1,13 @@ module Main where +import qualified Test.QuickCheck as Q+ import qualified Prelude+import Data.Char (intToDigit)+import Control.Monad (when) -import Types.Data.Ord-import Types.Data.Num+import Types import Types.Data.Num.Decimal.Literals.TH-import Types.Data.Bool-import Data.SizedWord testIsPositive1 :: IsPositive D1 -> True testIsPositive1 = Prelude.id@@ -55,6 +56,14 @@ testSucc6 = Prelude.id testSucc7 :: Succ DN101 -> DN100 testSucc7 = Prelude.id+testSucc8 :: Succ D0 -> D1 :+: D0+testSucc8 = Prelude.id+testSucc9 :: Succ D0 -> D0 :+: D1+testSucc9 = Prelude.id+testSucc10 :: Succ D9 -> D1 :+: D9+testSucc10 = Prelude.id+testSucc11 :: Succ D9 -> D9 :+: D1+testSucc11 = Prelude.id testPred1 :: Pred D1 -> D0 testPred1 = Prelude.id@@ -70,6 +79,28 @@ testPred6 = Prelude.id testPred7 :: Pred D100 -> D99 testPred7 = Prelude.id+testPred8 :: Pred D0 -> D0 :-: D1+testPred8 = Prelude.id+testPred9 :: Pred D10 -> D10 :-: D1+testPred9 = Prelude.id+testPred10 :: Pred D9 -> D8+testPred10 = Prelude.id+testPred11 :: Pred D8 -> D7+testPred11 = Prelude.id+testPred12 :: Pred D7 -> D6+testPred12 = Prelude.id+testPred13 :: Pred D6 -> D5+testPred13 = Prelude.id+testPred14 :: Pred D5 -> D4+testPred14 = Prelude.id+testPred15 :: Pred D4 -> D3+testPred15 = Prelude.id+testPred16 :: Pred D3 -> D2+testPred16 = Prelude.id+testPred17 :: Pred D2 -> D1+testPred17 = Prelude.id+testPred18 :: Pred D1 -> D0+testPred18 = Prelude.id testAdd1 :: D0 :+: D0 -> D0 testAdd1 = Prelude.id@@ -148,8 +179,65 @@ testFac4 :: Fac D10 -> D3628800 testFac4 = Prelude.id -f :: n -> (n :+: D5)-f _ = Prelude.undefined+testEQ1 :: D0 :==: D0 -> True+testEQ1 = Prelude.id+testEQ2 :: D0 :==: Pred D1 -> True+testEQ2 = Prelude.id+testEQ3 :: (D1 :+: D9) :==: D10 -> True+testEQ3 = Prelude.id+testEQ4 :: (D1 :+: D9) :==: D11 -> False+testEQ4 = Prelude.id+testEQ5 :: D9 :==: D0 -> False+testEQ5 = Prelude.id+testEQ6 :: D8 :==: D0 -> False+testEQ6 = Prelude.id+testEQ7 :: D7 :==: D0 -> False+testEQ7 = Prelude.id+testEQ8 :: D6 :==: D0 -> False+testEQ8 = Prelude.id+testEQ9 :: D5 :==: D0 -> False+testEQ9 = Prelude.id+testEQ10 :: D4 :==: D0 -> False+testEQ10 = Prelude.id+testEQ11 :: D3 :==: D0 -> False+testEQ11 = Prelude.id+testEQ12 :: D2 :==: D0 -> False+testEQ12 = Prelude.id+testEQ13 :: D1 :==: D0 -> False+testEQ13 = Prelude.id -main :: Prelude.IO ()-main = Prelude.return ()+testMin1 :: Min D0 D5 -> D0+testMin1 = Prelude.id+testMin2 :: Min D5 D0 -> D0+testMin2 = Prelude.id+testMin3 :: Min DN5 D5 -> DN5+testMin3 = Prelude.id++testMax1 :: Max D1 D6 -> D6+testMax1 = Prelude.id+testMax2 :: Max DN6 D6 -> D6+testMax2 = Prelude.id+testMax3 :: Max D6 D1 -> D6+testMax3 = Prelude.id++class TestIter n zero where+ testIter :: n -> zero -> Prelude.String++instance ( NaturalT n+ , (n :==: D0) ~ True )+ => TestIter n True where+ testIter _ _ = ""++instance ( NaturalT n+ , (n :==: D0) ~ False+ , TestIter (Pred n) ((Pred n) :==: D0) )+ => TestIter n False where+ testIter n _ =+ intToDigit (fromIntegerT n) : testIter (_T :: (Pred n)) (_T :: ((Pred n) :==: D0))++main = do+ let testIterResult = testIter d9 (_T :: False)+ when (testIterResult Prelude./= "987654321") (Prelude.putStrLn ("testIter failed, got: " Prelude.++ testIterResult))+ Q.quickCheck prop_reifyIntegral++prop_reifyIntegral i = reifyIntegral (Prelude.undefined :: Decimal) i fromIntegerT Prelude.== i
Types/Data/Num.hs view
@@ -15,7 +15,14 @@ module Types.Data.Num ( module Types.Data.Num.Ops , module Types.Data.Num.Decimal+ , reifyIntegralD+ , reifyPositiveD+ , reifyNegativeD ) where import Types.Data.Num.Ops import Types.Data.Num.Decimal++reifyIntegralD = reifyIntegral decimal+reifyPositiveD = reifyPositive decimal+reifyNegativeD = reifyNegative decimal
Types/Data/Num/Decimal/Digits.hs view
@@ -20,6 +20,10 @@ import Types.Data.List import Types.Data.Num.Ops +-- | Representation name for decimal type level numbers.+data Decimal+decimal = undefined :: Decimal+ -- | The wrapper type for decimal type level numbers. data Dec x data Neg' x
Types/Data/Num/Decimal/Literals/TH.hs view
@@ -2,11 +2,27 @@ import Language.Haskell.TH +import qualified Types.Data.Num.Decimal.Digits as D+import qualified Types.Data.Num.Ops as O+ decLiteralT :: Integer -> Q Type-decLiteralT n = appT (conT (mkName "Dec")) (decLiteralT' n)- where decLiteralT' n | n < 0 = appT (conT (mkName "Neg'")) (decLiteralT' (-n))- | n == 0 = conT (mkName "DecN")- | otherwise = appT (appT (conT (mkName ":.")) (decLiteralT' (n `div` 10))) (conT (mkName ("Dec" ++ show (n `mod` 10))))+decLiteralT n = appT (conT (''D.Dec)) (decLiteralT' n)+ where decLiteralT' n | n < 0 = appT (conT ''D.Neg') (decLiteralT' (-n))+ | n == 0 = conT ''D.DecN+ | otherwise = appT (appT (conT ''(O.:.)) (decLiteralT' (n `div` 10))) (conT (case n `mod` 10 of+ 0 -> ''D.Dec0 + 1 -> ''D.Dec1+ 2 -> ''D.Dec2+ 3 -> ''D.Dec3+ 4 -> ''D.Dec4+ 5 -> ''D.Dec5+ 6 -> ''D.Dec6+ 7 -> ''D.Dec7+ 8 -> ''D.Dec8+ 9 -> ''D.Dec9))++decLiteralV :: Integer -> Q Exp+decLiteralV n = sigE [| undefined |] (decLiteralT n) decLiteralD :: String -> String
Types/Data/Num/Decimal/Ops.hs view
@@ -22,8 +22,30 @@ import Types.Data.Num.Decimal.Literals import Types.Data.Num.Decimal.Digits +instance IntegerR Decimal where+ reifyIntegral _ i k = reifyIntegral' i (\(_ :: s) -> k (undefined :: Dec s))++reifyIntegral' :: Integer -> (forall s. IntegerT' s => s -> w) -> w+reifyIntegral' i k | i < 0 = go (negate i) (\(_ :: s) -> k (undefined :: Neg' s)) + | otherwise = go i k+ where+ go :: Integer -> (forall s. IntegerT' s => s -> w) -> w+ go 0 k = k (undefined :: DecN)+ go i k = let (j, d) = quotRem i 10 in case d of+ 0 -> go j (\(_ :: s) -> k (undefined :: s :. Dec0))+ 1 -> go j (\(_ :: s) -> k (undefined :: s :. Dec1))+ 2 -> go j (\(_ :: s) -> k (undefined :: s :. Dec2))+ 3 -> go j (\(_ :: s) -> k (undefined :: s :. Dec3))+ 4 -> go j (\(_ :: s) -> k (undefined :: s :. Dec4))+ 5 -> go j (\(_ :: s) -> k (undefined :: s :. Dec5))+ 6 -> go j (\(_ :: s) -> k (undefined :: s :. Dec6))+ 7 -> go j (\(_ :: s) -> k (undefined :: s :. Dec7))+ 8 -> go j (\(_ :: s) -> k (undefined :: s :. Dec8))+ 9 -> go j (\(_ :: s) -> k (undefined :: s :. Dec9))+ instance IntegerT' x => IntegerT (Dec x) where fromIntegerT _ = fromIntegerT' (undefined :: x)+ type Repr (Dec x) = Decimal class IntegerT' x where fromIntegerT' :: Num y => x -> y
Types/Data/Num/Ops.hs view
@@ -50,10 +50,13 @@ , div2T , Fac , facT+ , IntegerR (..) , IntegerT (..) , NaturalT , PositiveT , NegativeT+ , reifyPositive+ , reifyNegative ) where import Types.Data.Bool@@ -144,5 +147,39 @@ class IntegerT x => NegativeT x instance (IntegerT x, IsNegative x ~ True) => NegativeT x -class IntegerT x where+class (IntegerR (Repr x)) => IntegerT x where fromIntegerT :: Num y => x -> y+ type Repr x++class IntegerR r where+ reifyIntegral :: r -> Integer -> (forall s. (IntegerT s, Repr s ~ r) => s -> a) -> a+++--- positive and negative assertions: unsafe, in a trusted kernel+data AssertPos x+data AssertNeg x++assertPos :: x -> AssertPos x+assertPos _ = undefined++assertNeg :: x -> AssertNeg x+assertNeg _ = undefined++type instance IsPositive (AssertPos x) = True+type instance IsNegative (AssertNeg x) = True++instance IntegerT x => IntegerT (AssertPos x) where + fromIntegerT _ = fromIntegerT (undefined :: x)+ type Repr (AssertPos x) = Repr x++instance IntegerT x => IntegerT (AssertNeg x) where+ fromIntegerT _ = fromIntegerT (undefined :: x)+ type Repr (AssertNeg 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
Types/Data/Ord.hs view
@@ -34,6 +34,10 @@ , geT , (:>:) , gtT+ , Min+ , minT+ , Max+ , maxT ) where import qualified Prelude@@ -107,6 +111,16 @@ type instance x :>: y = IsGT (Compare x y) gtT :: x -> y -> x :>: y gtT _ _ = Prelude.undefined++type family Min x y+type instance Min x y = If (x :<=: y) x y+minT :: x -> y -> Min x y+minT _ _ = Prelude.undefined++type family Max x y+type instance Max x y = If (x :>=: y) x y+maxT :: x -> y -> Max x y+maxT _ _ = Prelude.undefined type instance Compare False False = EQ type instance Compare False True = LT
tfp.cabal view
@@ -1,5 +1,5 @@ name: tfp-version: 0.1+version: 0.2 cabal-version: >= 1.2 build-type: Simple license: BSD3@@ -25,7 +25,8 @@ extensions: TypeFamilies, UndecidableInstances, TypeOperators, EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables, FlexibleInstances, TemplateHaskell, TypeSynonymInstances,- MultiParamTypeClasses, GeneralizedNewtypeDeriving+ MultiParamTypeClasses, GeneralizedNewtypeDeriving,+ Rank2Types, FlexibleContexts build-depends: base >= 3.0, template-haskell >= 2.0 exposed-modules: Data.SizedInt,@@ -55,7 +56,8 @@ extensions: TypeFamilies, UndecidableInstances, TypeOperators, EmptyDataDecls, DeriveDataTypeable, ScopedTypeVariables, FlexibleInstances, TemplateHaskell, TypeSynonymInstances,- MultiParamTypeClasses, GeneralizedNewtypeDeriving+ MultiParamTypeClasses, GeneralizedNewtypeDeriving,+ FunctionalDependencies, Rank2Types, FlexibleContexts main-is: Test.hs- build-depends: base >= 3.0, template-haskell >= 2.0+ build-depends: base >= 3.0, template-haskell >= 2.0, QuickCheck >= 1.2.0.0 }