finite 1.4.1.4 → 1.5.0.0
raw patch · 9 files changed
+344/−725 lines, 9 filesdep ~Cabaldep ~basedep ~containers
Dependency ranges changed: Cabal, base, containers, hashable, template-haskell
Files
- Readme.md +1/−1
- finite.cabal +9/−9
- src/lib/Finite.hs +10/−29
- src/lib/Finite/Class.hs +103/−232
- src/lib/Finite/Collection.hs +27/−79
- src/lib/Finite/PowerSet.hs +38/−66
- src/lib/Finite/TH.hs +32/−69
- src/lib/Finite/Type.hs +0/−93
- src/test/Test.hs +124/−147
Readme.md view
@@ -63,7 +63,7 @@ let ?bounds = fsm in -- show the data unlines $- [ "The FSM has " ++ show (elements ((#) :: T State)) ++ " states."+ [ "The FSM has " ++ show (elements (type State)) ++ " states." ] ++ [ "Labels:" ] ++
finite.cabal view
@@ -1,5 +1,5 @@ name: finite-version: 1.4.1.4+version: 1.5.0.0 synopsis: Finite ranges via types description: A framework for capturing finite ranges with types, where the sizes of the ranges are not@@ -20,6 +20,7 @@ build-type: Simple extra-source-files: Readme.md cabal-version: >=1.10+tested-with: GHC == 9.10.1, GHC == 9.12.1 source-repository head type: git@@ -34,11 +35,11 @@ -fignore-asserts build-depends:- base >=4.7 && <4.22+ base >=4.20 && <4.22 , array >=0.5 && <0.6- , containers >=0.5 && <0.8- , hashable >=1.2 && <1.6- , template-haskell >=2.11 && <2.24+ , containers >=0.7 && <0.8+ , hashable >=1.5 && <1.6+ , template-haskell >=2.22 && <2.24 , QuickCheck >=2.10 && <=2.16 exposed-modules:@@ -49,7 +50,6 @@ Finite.Class Finite.PowerSet Finite.Collection- Finite.Type hs-source-dirs: src/lib@@ -75,9 +75,9 @@ src/test build-depends:- base >=4.7 && <4.22- , hashable >=1.2 && <1.6- , Cabal >=2.4 && < 3.15+ base >=4.20 && <4.22+ , hashable >=1.5 && <1.6+ , Cabal >=3.12 && < 3.15 , QuickCheck >=2.10 && <=2.16 , finite
src/lib/Finite.hs view
@@ -13,16 +13,13 @@ -- The framework supports: -- -- * Easy access to the object's elements via types.--- * Efficient bidirectional mappings between indices and the--- elements.+-- * Efficient bidirectional mappings between indices and the elements. -- * Implicit total orderings on the elements. -- * Powerset Support.--- * Extension of a single context to a range of contexts via--- collections.+-- * Extension of a single context to a range of contexts via collections. -- * Easy passing of the context via implict parameters.--- * Generics Support: Finite range types can be easily constructed--- out of other finite range types using Haskell's `data`--- constructor.+-- * Generics Support: Finite range types can be easily constructed out+-- of other finite range types using Haskell's `data` constructor. -- * Template Haskell: Easy creation of basic finite instances using -- short Haskell templates, as well as the extension of existing -- types to more feature rich parameter spaces (requires the@@ -32,39 +29,23 @@ module Finite ( -- * The Finite Class- Finite(..)+ FiniteBounds+ , Finite(..) , GFinite(..)- , FiniteBounds+ , withBounds , -- * Powersets PowerSet , -- * Collections Collection(..)- , -- * Polymorphic Type Access- T- , (#)- , (\#)- , (<<#)- , (#<<)- , v2t- , t2v ) where ----------------------------------------------------------------------------- -import Finite.Type- ( T- , FiniteBounds- , (#)- , (\#)- , (<<#)- , (#<<)- , t2v- , v2t- )- import Finite.Class- ( Finite(..)+ ( FiniteBounds+ , Finite(..) , GFinite(..)+ , withBounds ) import Finite.PowerSet
src/lib/Finite/Class.hs view
@@ -9,21 +9,28 @@ {-# LANGUAGE - MultiWayIf- , TypeOperators+ ConstraintKinds , DefaultSignatures- , MultiParamTypeClasses , FlexibleContexts , FlexibleInstances+ , ImplicitParams+ , LambdaCase+ , MultiParamTypeClasses+ , TypeOperators+ , ScopedTypeVariables+ , RankNTypes+ , RequiredTypeArguments+ , ViewPatterns #-} ----------------------------------------------------------------------------- module Finite.Class- ( T+ ( FiniteBounds , Finite(..) , GFinite(..)+ , withBounds ) where -----------------------------------------------------------------------------@@ -32,16 +39,6 @@ ( assert ) -import Finite.Type- ( T- , FiniteBounds- , (#<<)- , (<<#)- , v2t- , (\#)- , (#)- )- import GHC.Generics ( Generic , Rep@@ -63,309 +60,183 @@ ----------------------------------------------------------------------------- --- | The 'Finite' class.+-- | A better looking constraint specifier.+type FiniteBounds b = (?bounds :: b) -class Finite b a where+----------------------------------------------------------------------------- +-- | A more ergonomic way to set the implicit parameter.+withBounds :: b -> (FiniteBounds b => c) -> c+withBounds b x = let ?bounds = b in x++-----------------------------------------------------------------------------++-- | The 'Finite' class.+class Finite b a where -- | Returns the number of elements associated with the given type.- elements- :: FiniteBounds b- => T a -> Int+ elements :: forall c -> (a ~ c, FiniteBounds b) => Int default elements- :: (Generic a, GFinite b (Rep a), FiniteBounds b)- => T a -> Int-- elements t = gelements #<< from <<# t+ :: (Generic a, GFinite b (Rep a)) =>+ forall c -> (a ~ c, FiniteBounds b) => Int+ elements _ = gelements (Rep a) -- | Turns the value in the associated range into an Int uniquely -- identifiying the value.- index- :: FiniteBounds b- => a -> Int-- default index- :: (Generic a, GFinite b (Rep a), FiniteBounds b)- => a -> Int+ index :: FiniteBounds b => a -> Int - index v = (+ (offset $ v2t v)) $ gindex $ from v+ default index ::+ (Generic a, GFinite b (Rep a), FiniteBounds b) =>+ a -> Int+ index v = (+ (offset a)) $ gindex $ from v -- | Turns an Int back to the value that is associated with it.- value- :: FiniteBounds b => Int -> a+ value :: FiniteBounds b => Int -> a - default value- :: (Generic a, GFinite b (Rep a), FiniteBounds b)- => Int -> a+ default value ::+ (Generic a, GFinite b (Rep a), FiniteBounds b) => Int -> a - value v =- let- o = offset $ v2t r- e = elements $ v2t r- r = to $ gvalue (v - o)- in- assert (v >= o && v < o + e) r+ value v = assert (v >= o && v < o + e) $ to $ gvalue (v - o)+ where+ o = offset a+ e = elements a -- | Allows to put an offset to the integer mapping. Per default the -- offset is zero.- offset- :: FiniteBounds b- => T a -> Int-+ offset :: forall c -> (a ~ c, FiniteBounds b) => Int offset _ = 0 -- | Returns a finite list of all elements of that type.- values- :: FiniteBounds b- => [a]-- values =- let- rs = map value xs- o = offset $ f rs- n = elements $ f rs- xs = [o, o + 1 .. o + n - 1]- in- rs-- where- f :: [a] -> T a- f _ = (#)+ values :: FiniteBounds b => [a]+ values = value <$> [o, o + 1 .. o + n - 1]+ where+ n = elements a+ o = offset a -- | Complements a given list of elements of that type- complement- :: FiniteBounds b- => [a] -> [a]-- complement xs =- let- o = offset $ f rs- n = elements $ f rs- s = S.fromList $ map index xs- a = S.fromAscList [o, o + 1 .. o + n - 1]- rs = map value $ S.toList $ S.difference a s- in- rs-- where- f :: [a] -> T a- f _ = (#)+ complement :: FiniteBounds b => [a] -> [a]+ complement xs = value <$> ys+ where+ o = offset a+ n = elements a+ s = S.fromList $ map index xs+ as = S.fromAscList [o, o + 1 .. o + n - 1]+ ys = S.toList $ S.difference as s -- | Less than operator according to the implicit total index order.- (|<|)- :: FiniteBounds b- => a -> a -> Bool-- (|<|) x y =- index x < index y-+ (|<|) :: FiniteBounds b => a -> a -> Bool+ x |<| y = index x < index y infixr |<| -- | Less or equal than operator according to the implicit total -- index order.- (|<=|)- :: FiniteBounds b- => a -> a -> Bool-- (|<=|) x y =- index x <= index y-+ (|<=|) :: FiniteBounds b => a -> a -> Bool+ x |<=| y = index x <= index y infixr |<=| -- | Greater or equal than operator according to the implicit total -- index order.- (|>=|)- :: FiniteBounds b- => a -> a -> Bool-- (|>=|) x y =- index x >= index y-+ (|>=|) :: FiniteBounds b => a -> a -> Bool+ x |>=| y = index x >= index y infixr |>=| - -- | Greater than operator according to the implicit total index- -- order.- (|>|)- :: FiniteBounds b- => a -> a -> Bool-- (|>|) x y =- index x > index y-+ -- | Greater than operator according to the implicit total index order.+ (|>|) :: FiniteBounds b => a -> a -> Bool+ x |>| y = index x > index y infixr |>| -- | Equal operator according to the implicit total index order.- (|==|)- :: FiniteBounds b- => a -> a -> Bool-- (|==|) x y =- index x == index y-+ (|==|) :: FiniteBounds b => a -> a -> Bool+ x |==| y = index x == index y infixr |==| -- | Unequal operator according to the implicit total index order.- (|/=|)- :: FiniteBounds b- => a -> a -> Bool-- (|/=|) x y =- index x /= index y-+ (|/=|) :: FiniteBounds b => a -> a -> Bool+ x |/=| y = index x /= index y infixr |/=| - -- | First element according to the total index order.- initial- :: FiniteBounds b- => T a -> a-- initial t =- value $ offset t+ initial :: forall c -> (a ~ c, FiniteBounds b) => a+ initial x = value $ offset x -- | Last element according to the total index order.- final- :: FiniteBounds b- => T a -> a-- final t =- value $ offset t + elements t - 1+ final :: forall c -> (a ~ c, FiniteBounds b) => a+ final x = value $ offset x + elements x - 1 -- | Next element according to the total index order (undefined for -- the last element).- next- :: FiniteBounds b- => a -> a-- next x =- let i = index x- in assert (i < offset (v2t x) + elements (v2t x) - 1)- $ value (i + 1)+ next :: FiniteBounds b => a -> a+ next (index -> i) = assert (i < offset a + elements a - 1) $ value (i + 1) -- | Previous element according to the total index order (undefined -- for the first element).- previous- :: FiniteBounds b- => a -> a-- previous x =- let i = index x- in assert (i > offset (v2t x))- $ value (i - 1)+ previous :: FiniteBounds b => a -> a+ previous (index -> i) = assert (i > offset a) $ value (i - 1) -- | The upper and lower bounds of the instance.- bounds- :: FiniteBounds b- => T a -> (a, a)-- bounds t =- (initial t, final t)+ bounds :: forall c -> (c ~ a, FiniteBounds b) => (a, a)+ bounds x = (initial x, final x) ----------------------------------------------------------------------------- -- | Generics implementation for the 'Finite' class. The -- realization is closely related to the one presented at -- https://wiki.haskell.org/GHC.Generics.- class GFinite b f where- gelements :: FiniteBounds b => T (f a) -> Int+ gelements :: forall c -> (c ~ f, FiniteBounds b) => Int gindex :: FiniteBounds b => f a -> Int gvalue :: FiniteBounds b => Int -> f a ----------------------------------------------------------------------------- -- | :*: instance.--instance- (GFinite b f, GFinite b g)- => GFinite b (f :*: g) where-- gelements x =- gelements (((\#) :: T ((f :*: g) a) -> T (f a)) x) *- gelements (((\#) :: T ((f :*: g) a) -> T (g a)) x)-- gindex (f :*: g) =- (gindex f * (gelements #<< g)) + gindex g-- gvalue n =- let- m = gelements #<< g- f = gvalue (n `div` m)- g = gvalue (n `mod` m)- in- (f :*: g)+instance (GFinite b f, GFinite b g) => GFinite b (f :*: g) where+ gelements _ = gelements f * gelements g+ gindex (f :*: g) = gindex f * gelements (type g) + gindex g+ gvalue n = f :*: g+ where+ m = gelements (type g)+ f = gvalue (n `div` m)+ g = gvalue (n `mod` m) ----------------------------------------------------------------------------- -- | :+: instance.--instance- (GFinite b f, GFinite b g)- => GFinite b (f :+: g) where-- gelements x =- gelements (((\#) :: T ((f :+: g) a) -> T (f a)) x) +- gelements (((\#) :: T ((f :+: g) a) -> T (g a)) x)-- gindex x = case x of- R1 y -> gindex y- L1 y -> gindex y + gelements (((\#) :: (f :+: g) a -> T (g a)) x)-- gvalue n =- let- m = gelements #<< g- g = gvalue (n `mod` m)- f = gvalue (n - m)- in if- | n < m -> R1 g- | otherwise -> L1 f+instance (GFinite b f, GFinite b g) => GFinite b (f :+: g) where+ gelements _ = gelements f + gelements g+ gindex = \case+ R1 x -> gindex x+ L1 x -> gindex x + gelements g+ gvalue n+ | n < m = R1 g+ | otherwise = L1 f+ where+ m = gelements (type g)+ g = gvalue (n `mod` m)+ f = gvalue (n - m) ----------------------------------------------------------------------------- -- | U1 instance.--instance- GFinite c U1 where-+instance GFinite c U1 where gelements _ = 1- gindex U1 = 0- gvalue _ = U1 ----------------------------------------------------------------------------- -- | M1 instance.--instance- (GFinite c f)- => GFinite c (M1 i v f) where-- gelements =- gelements . ((\#) :: T ((M1 i v f) p) -> T (f p))-+instance GFinite c f => GFinite c (M1 i v f) where+ gelements _ = gelements f gindex (M1 x) = gindex x- gvalue = M1 . gvalue ----------------------------------------------------------------------------- -- | K1 instance.--instance- (Finite b a)- => GFinite b (K1 i a) where-- gelements =- elements . ((\#) :: T ((K1 i a) c) -> T a)-- gindex (K1 x) = index x - (offset #<< x)-- gvalue n =- let- m = offset #<< x- x = value (n + m)- in- K1 x+instance Finite b a => GFinite b (K1 i a) where+ gelements _ = elements a+ gindex (K1 x) = index x - offset a+ gvalue n = K1 $ value (n + offset a) -----------------------------------------------------------------------------
src/lib/Finite/Collection.hs view
@@ -10,9 +10,10 @@ {-# LANGUAGE - MultiParamTypeClasses+ ImplicitParams , LambdaCase- , ImplicitParams+ , MultiParamTypeClasses+ , ScopedTypeVariables #-} @@ -22,19 +23,13 @@ ----------------------------------------------------------------------------- -import Finite.Type- ( T- , v2t- , (#<<)- , FiniteBounds- )- import Finite.Class ( Finite , elements , offset , value , index+ , withBounds ) import Data.Array.IArray@@ -55,9 +50,7 @@ -- | The 'Collection' type provides a set of items, each assigning an -- index of type @i@ to a value of type @a@.--data Collection i a =- Item i a+data Collection i a = Item i a deriving ( -- | Equality can be checked for collections, if the index type -- and the elements can be checked for equality.@@ -77,77 +70,32 @@ -- the bounds. Since the 'FiniteBounds' parameter always gives a -- finite sized array of bounding parameters, it is guaranteed that -- the connected collection has a finite bound as well.- instance (Ix i, Finite b a) => Finite (Array i b) (Collection i a) where-- elements t =- sum $ map (elms t) $ assocs ?bounds-- where- conv- :: T (Collection i a) -> T a-- conv = undefined--- elms- :: Finite b a => T (Collection i a) -> (i, b) -> Int-- elms t (_,b) =- let ?bounds = b- in elements $ conv t-- index (Item j v) =- let- -- array bounds- (l,u) = bounds ?bounds- -- list of indicies that appear before j- ys = assert (inRange (l,u) j) $ init $ range (l,j)- -- offset induces by these indices- o = sum $ map ((elms v .) (?bounds !)) ys- -- index of v with the bounds at position j- idx = let ?bounds = ?bounds ! j- in index v - offset #<< v- in- o + idx-- where- elms- :: Finite b a => a -> b -> Int+ elements _ = sum $ (`withBounds` elements a) . snd <$> assocs ?bounds - elms v b =- let ?bounds = b- in elements $ v2t v+ index (Item j v) = o + idx+ where+ -- array bounds+ (l, u) = bounds ?bounds+ -- list of indicies that appear before j+ ys = assert (inRange (l, u) j) $ init $ range (l, j)+ -- offset induces by these indices+ o = sum $ map ((`withBounds` elements a) . (?bounds !)) ys+ -- index of v with the bounds at position j+ idx = withBounds (?bounds ! j) $ index v - offset a value n =- let- -- elements of the whole collection- e = elements $ v2t r- -- array bounds- b = bounds ?bounds- -- target array index and reminder used as sub-index- (j,m) = position (conv r) n (range b)- -- result- r = let ?bounds = ?bounds ! j- in Item j $ value (m + offset (conv r))- in- assert (n >= 0 && n < e) r-- where- conv- :: Collection i a -> T a-- conv = undefined--- position- :: (Ix i, Finite b a, FiniteBounds (Array i b))- => T a -> Int -> [i] -> (i,Int)+ assert (n >= 0 && n < elements (Collection i a))+ $ withBounds (?bounds ! j) $ Item j $ value (m + offset a)+ where+ -- target array index and reminder used as sub-index+ (j, m) = position n $ range $ bounds ?bounds - position t n = \case- [] -> assert False undefined- x:xr ->- let m = let ?bounds = ?bounds ! x in elements t- in if m <= n then position t (n - m) xr else (x,n)+ position n = \case+ [] -> assert False undefined+ x : xr | m <= n -> position (n - m) xr+ | otherwise -> (x, n)+ where+ m = withBounds (?bounds ! x) $ elements a -----------------------------------------------------------------------------
src/lib/Finite/PowerSet.hs view
@@ -9,12 +9,10 @@ {-# LANGUAGE - MultiParamTypeClasses+ BangPatterns , FlexibleInstances- , FlexibleContexts- , LambdaCase- , MultiWayIf- , BangPatterns+ , MultiParamTypeClasses+ , ScopedTypeVariables #-} @@ -26,14 +24,6 @@ ----------------------------------------------------------------------------- -import Finite.Type- ( T- , (#)- , (\#)- , (#<<)- , v2t- )- import Finite.Class ( Finite(..) )@@ -47,51 +37,41 @@ -- | Powersets are just lists of the correpsonding elements. The type -- has only been added for clearification. Consider the corresponding -- instance of 'Finite' for possible applications.- type PowerSet a = [a] ----------------------------------------------------------------------------- -- | If the number of elements associated with a type is finite, then -- it also has finite number of powersets.- instance Finite b a => Finite b (PowerSet a) where-- elements =- pow2 2 . elements . ((\#) :: T (PowerSet a) -> T a)-- where- pow2 !a !n = case n of- 0 -> 1- 1 -> a- _ -> pow2 (2*a) (n-1)-- index = \case- [] -> 0- (y:yr) -> powsum (0,2,idx y,yr)-- where- idx x = index x - offset #<< x+ elements _ = pow2 2 $ elements a+ where+ pow2 !a !n = case n of+ 0 -> 1+ 1 -> a+ _ -> pow2 (2 * a) (n - 1) - powsum !p = case p of- (a,_,0,[]) ->- a + (1 - (a `mod` 2))- (a,p,1,[]) ->- a + ((1 - ((a `mod` (2*p)) `div` p)) * p)- (a,_,0,x:xr) ->- powsum (a + (1 - (a `mod` 2)),2,idx x,xr)- (a,p,1,x:xr) ->- powsum (a + ((1 - ((a `mod` (2*p)) `div` p)) * p), 2, idx x, xr)- (a,p,n,xs) ->- powsum (a,2*p,n-1,xs)+ index [] = 0+ index (y : yr) = powsum (0, 2, idx y, yr)+ where+ idx x = index x - offset a+ powsum !p = case p of+ (a, _, 0, []) ->+ a + (1 - (a `mod` 2))+ (a, p, 1, []) ->+ a + ((1 - ((a `mod` (2 * p)) `div` p)) * p)+ (a, _, 0, x : xr) ->+ powsum (a + (1 - (a `mod` 2)), 2, idx x, xr)+ (a, p, 1, x : xr) ->+ powsum (a + ((1 - ((a `mod` (2 * p)) `div` p)) * p), 2, idx x, xr)+ (a, p, n, xs) ->+ powsum (a, 2 * p, n - 1, xs) value n =- let ty :: T [a] -> T a- ty _ = (#)- bs = map (value . (+ (offset $ ty $ v2t bs))) $ bin n- in assert (n >= 0 && n < (elements #<< bs)) bs+ assert (n >= 0 && n < elements (PowerSet a))+ $ value . (+ offset a) <$> bin n - offset = offset . ((\#) :: T (PowerSet a) -> T a)+ offset _ = offset a values = powerset values @@ -99,30 +79,22 @@ -- | Converts an Int value to a list of Int values of logarithmic size -- encoding the original value.--bin- :: Int -> [Int]--bin x =- let- bin (a,!s,!n)- | n <= 0 = reverse a- | n `mod` 2 == 1 = bin (s:a, s+1, n `div` 2)- | otherwise = bin (a, s+1, n `div` 2)- in- bin ([],0,x)+bin :: Int -> [Int]+bin x = f ([], 0, x)+ where+ f (a, !s, !n)+ | n <= 0 = reverse a+ | n `mod` 2 == 1 = f (s : a, s + 1, n `div` 2)+ | otherwise = f ( a, s + 1, n `div` 2) ----------------------------------------------------------------------------- -- | Creates the powerset of a set, for sets represented as lists. If -- the given list is sorted, the created powerset will be sorted -- lexographically and the elements themselve will be sorted as well.--powerset- :: [a] -> [[a]]--powerset =- let f x a = [x] : foldr ((:) . (x:)) a a- in ([]:) . foldr f []+powerset :: [a] -> [[a]]+powerset = ([] :) . foldr f []+ where+ f x a = [x] : foldr ((:) . (x :)) a a -----------------------------------------------------------------------------
src/lib/Finite/TH.hs view
@@ -9,10 +9,14 @@ {-# LANGUAGE - LambdaCase+ CPP , ImplicitParams+ , ImpredicativeTypes+ , LambdaCase+ , RequiredTypeArguments , TemplateHaskell- , CPP+ , TypeOperators+ , ViewPatterns #-} @@ -46,13 +50,10 @@ , hashWithSalt ) -import Finite.Type- ( T- , FiniteBounds- )- import Finite.Class- ( Finite(..)+ ( FiniteBounds+ , Finite(..)+ , withBounds ) import Data.Char@@ -135,10 +136,7 @@ -- negate = Example . negage . example -- signum = Example . signum . example -- fromInteger = Example . fromInteger--newInstance- :: String -> Q [Dec]-+newInstance :: String -> Q [Dec] newInstance = \case [] -> assert False undefined (x:xr) -> assert (isUpper x) $ do@@ -415,10 +413,7 @@ -- elements _ = getBound ?bounds -- value = Example -- index = example--baseInstance- :: Q Type -> Q Exp -> String -> Q [Dec]-+baseInstance :: Q Type -> Q Exp -> String -> Q [Dec] baseInstance bounds f = \case [] -> assert False undefined (x:xr) -> assert (isUpper x) $ do@@ -479,10 +474,7 @@ ----------------------------------------------------------------------------- -- | Combined 'newInstance' with 'baseInstance'.--newBaseInstance- :: Q Type -> Q Exp -> String -> Q [Dec]-+newBaseInstance :: Q Type -> Q Exp -> String -> Q [Dec] newBaseInstance bounds f name = do xs <- newInstance name ys <- baseInstance bounds f name@@ -511,10 +503,7 @@ -- offset = let ?bounds = translate ?bounds in offset -- value = let ?bounds = translate ?bounds in value -- index = let ?bounds = translate ?bounds in index--extendInstance- :: Q Type -> Q Type -> Q Exp -> Q [Dec]-+extendInstance :: Q Type -> Q Type -> Q Exp -> Q [Dec] extendInstance rtype bounds access = do let tmpV = mkName "x" d_finite_instance <-@@ -588,69 +577,43 @@ -- >>> polyType [t|Maybe|] "a" -- <BLANKLINE> -- Maybe a--polyType- :: Q Type -> String -> Q Type--polyType con str = do+polyType :: Q Type -> String -> Q Type+polyType con (mkName -> name) = do t <- con- return $ t `AppT` (VarT $ mkName str)+ return $ t `AppT` VarT name ----------------------------------------------------------------------------- -appBounds- :: FiniteBounds b- => (b -> a) -> a--appBounds x =- x ?bounds+appBounds :: FiniteBounds b=> (b -> a) -> a+appBounds x = x ?bounds ----------------------------------------------------------------------------- -elementsSwitch- :: (Finite b' a, FiniteBounds b)- => (b -> b') -> T a -> Int--elementsSwitch f =- let ?bounds = f ?bounds- in elements+elementsSwitch ::+ (Finite b' a, FiniteBounds b) => (b -> b') ->+ Finite b a => forall c -> (c ~ a, FiniteBounds b) => Int+elementsSwitch f x = withBounds (f ?bounds) $ elements x ----------------------------------------------------------------------------- -offsetSwitch- :: (Finite b' a, FiniteBounds b)- => (b -> b') -> T a -> Int--offsetSwitch f =- let ?bounds = f ?bounds- in offset+offsetSwitch ::+ (Finite b' a, FiniteBounds b) => (b -> b') ->+ Finite b a => forall c -> (c ~ a, FiniteBounds b) => Int+offsetSwitch f x = withBounds (f ?bounds) $ offset x ----------------------------------------------------------------------------- -indexSwitch- :: (Finite b' a, FiniteBounds b)- => (b -> b') -> a -> Int--indexSwitch f =- let ?bounds = f ?bounds- in index+indexSwitch :: (Finite b' a, FiniteBounds b) => (b -> b') -> a -> Int+indexSwitch f = withBounds (f ?bounds) index ----------------------------------------------------------------------------- -valueSwitch- :: (Finite b' a, FiniteBounds b)- => (b -> b') -> Int -> a--valueSwitch f =- let ?bounds = f ?bounds- in value+valueSwitch :: (Finite b' a, FiniteBounds b) => (b -> b') -> Int -> a+valueSwitch f = withBounds (f ?bounds) value ----------------------------------------------------------------------------- -inRange- :: Int -> Int -> Bool--inRange x y =- x >= 0 && x < y+inRange :: Int -> Int -> Bool+inRange x y = x >= 0 && x < y -----------------------------------------------------------------------------
− src/lib/Finite/Type.hs
@@ -1,93 +0,0 @@--------------------------------------------------------------------------------- |--- Module : Finite.Type--- Maintainer : Felix Klein------ Type association to pass types via functions.-----------------------------------------------------------------------------------{-# LANGUAGE-- ImplicitParams- , ConstraintKinds-- #-}---------------------------------------------------------------------------------module Finite.Type- ( T- , FiniteBounds- , (#)- , (\#)- , (<<#)- , (#<<)- , t2v- , v2t- ) where----------------------------------------------------------------------------------- | A better looking constraint specifier.--type FiniteBounds b = (?bounds :: b)----------------------------------------------------------------------------------- | A type dummy.--newtype T a = T ()----------------------------------------------------------------------------------- | The type dummy instance.--(#) :: T a-(#) = T ()----------------------------------------------------------------------------------- | A type dummy returning function. Intended to use the type engine--- for accessing the type of the argument. Note that "@(\\#) :: a -> T--- a@" is just a special instance.--(\#) :: b -> T a-(\#) _ = (#)----------------------------------------------------------------------------------- | Get some undefined value of the given type. Intended to be used--- for extracting type information of polymorph types only.--t2v :: T a -> a-t2v _ = undefined----------------------------------------------------------------------------------- | Replace a function's argument by its type dummy. Intended to be used--- for extracting type information of polymorph types only.--infixr <<#--(<<#) :: (a -> b) -> T a -> b-(<<#) f _ = f undefined----------------------------------------------------------------------------------- | Get the type of a given value.--v2t :: a -> T a-v2t = (\#)----------------------------------------------------------------------------------- | Replace a function's dummy type argument with its value taking--- equivalent.--infixr #<<--(#<<) :: (T a -> b) -> a -> b-(#<<) f _ = f $ T ()-------------------------------------------------------------------------------
src/test/Test.hs view
@@ -9,12 +9,14 @@ {-# LANGUAGE - LambdaCase+ DeriveGeneric+ , ExplicitNamespaces , ImplicitParams+ , LambdaCase+ , MultiParamTypeClasses+ , RankNTypes , RecordWildCards- , DeriveGeneric , TemplateHaskell- , MultiParamTypeClasses #-} @@ -140,36 +142,33 @@ { run = (Finished . allPass) <$> sequence (map quickCheckResult- [ \x -> let ?bounds = Bounds $ abs x + 1 in- elements ((#) :: T AInst) == abs x + 1- , \x -> let ?bounds = Bounds $ abs x + 1 in- offset ((#) :: T AInst) == 0- , \x -> let ?bounds = Bounds $ abs x + 1 in- map index (values :: [AInst]) == [0,1..abs x]- , \x -> let ?bounds = Bounds $ abs x + 1 in- map value [0,1..abs x] == (values :: [AInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- all (\x -> x == value (index x)) (values :: [AInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- complement (filter (odd . index) (values :: [AInst]))- == filter (even . index) (values :: [AInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- initial ((#) :: T AInst) |<=| final ((#) :: T AInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else next (initial ((#) :: T AInst))- |>=| initial ((#) :: T AInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else previous (final ((#) :: T AInst))- |/=| final ((#) :: T AInst)+ [ \x -> sb x $ elements (type AInst) == abs x + 1+ , \x -> sb x $ offset (type AInst) == 0+ , \x -> sb x $ map index vs == [0,1..abs x]+ , \x -> sb x $ map value [0,1..abs x] == vs+ , \x -> sb x $ all (\x -> x == value (index x)) vs+ , \x -> sb x $ complement (filter (odd . index) vs)+ == filter (even . index) vs+ , \x -> sb x $ initial (type AInst) |<=| final (type AInst)+ , \x -> sb x $ abs x < 1 ||+ next (initial (type AInst))+ |>=| initial (type AInst)+ , \x -> sb x $ abs x < 1 ||+ previous (final (type AInst))+ |/=| final (type AInst) ]) , name = "TH: baseInstance" , tags = [] , options = [] , setOption = \_ _ -> Right t02 }+ where+ vs :: FiniteBounds Bounds => [AInst]+ vs = values + sb :: Int -> (FiniteBounds Bounds => c) -> c+ sb x = withBounds $ Bounds $ abs x + 1+ t03 = TestInstance { run = (Finished . allPass) <$> sequence@@ -182,29 +181,20 @@ , \x -> hash (BInst x) == hash (BInst x) , \x -> not $ null $ range (BInst 0, BInst $ abs x) , \x -> (BInst x) + (BInst 1) == (BInst 1) + (BInst x)- , \x -> let ?bounds = Bounds $ abs x + 1 in- elements ((#) :: T BInst) == abs x + 1- , \x -> let ?bounds = Bounds $ abs x + 1 in- offset ((#) :: T BInst) == 0- , \x -> let ?bounds = Bounds $ abs x + 1 in- map index (values :: [BInst]) == [0,1..abs x]- , \x -> let ?bounds = Bounds $ abs x + 1 in- map value [0,1..abs x] == (values :: [BInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- all (\x -> x == value (index x)) (values :: [BInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- complement (filter (odd . index) (values :: [BInst]))- == filter (even . index) (values :: [BInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- initial ((#) :: T BInst) |<=| final ((#) :: T BInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else next (initial ((#) :: T BInst))- |>=| initial ((#) :: T BInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else previous (final ((#) :: T BInst))- |/=| final ((#) :: T BInst)+ , \x -> sb x $ elements (type BInst) == abs x + 1+ , \x -> sb x $ offset (type BInst) == 0+ , \x -> sb x $ map index vs == [0,1..abs x]+ , \x -> sb x $ map value [0,1..abs x] == vs+ , \x -> sb x $ all (\x -> x == value (index x)) vs+ , \x -> sb x $ complement (filter (odd . index) vs)+ == filter (even . index) vs+ , \x -> sb x $ initial (type BInst) |<=| final (type BInst)+ , \x -> sb x $ abs x < 1 ||+ next (initial (type BInst))+ |>=| initial (type BInst)+ , \x -> sb x $ abs x < 1 ||+ previous (final (type BInst))+ |/=| final (type BInst) ] ++ [ quickCheckResult $ \x -> bInst x == bInst x ])@@ -213,137 +203,124 @@ , options = [] , setOption = \_ _ -> Right t03 }+ where+ vs :: FiniteBounds Bounds => [BInst]+ vs = values + sb :: Int -> (FiniteBounds Bounds => c) -> c+ sb x = withBounds $ Bounds $ abs x + 1+ t04 = TestInstance { run = (Finished . allPass) <$> sequence (map quickCheckResult- [ \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- elements ((#) :: T AInst) == abs x + 1- , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- offset ((#) :: T AInst) == 0- , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- map index (values :: [AInst]) == [0,1..abs x]- , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- map value [0,1..abs x] == (values :: [AInst])- , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- all (\x -> x == value (index x)) (values :: [AInst])- , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- complement (filter (odd . index) (values :: [AInst]))- == filter (even . index) (values :: [AInst])- , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- initial ((#) :: T AInst) |<=| final ((#) :: T AInst)- , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- if abs x < 1 then True- else next (initial ((#) :: T AInst))- |>=| initial ((#) :: T AInst)- , \x -> let ?bounds = BBounds $ Bounds $ abs x + 1 in- if abs x < 1 then True- else previous (final ((#) :: T AInst))- |/=| final ((#) :: T AInst)+ [ \x -> sb x $ elements (type AInst) == abs x + 1+ , \x -> sb x $ offset (type AInst) == 0+ , \x -> sb x $ map index vs == [0,1..abs x]+ , \x -> sb x $ map value [0,1..abs x] == vs+ , \x -> sb x $ all (\x -> x == value (index x)) vs+ , \x -> sb x $ complement (filter (odd . index) vs)+ == filter (even . index) vs+ , \x -> sb x $ initial (type AInst) |<=| final (type AInst)+ , \x -> sb x $ abs x < 1 ||+ next (initial (type AInst))+ |>=| initial (type AInst)+ , \x -> sb x $ abs x < 1 ||+ previous (final (type AInst))+ |/=| final (type AInst) ]) , name = "TH: extendInstance" , tags = [] , options = [] , setOption = \_ _ -> Right t04 }+ where+ vs :: FiniteBounds BBounds => [AInst]+ vs = values + sb :: Int -> (FiniteBounds BBounds => c) -> c+ sb x = withBounds $ BBounds $ Bounds $ abs x + 1+ t05 = TestInstance { run = (Finished . allPass) <$> sequence (map quickCheckResult- [ \x -> let ?bounds = Bounds $ abs x + 1 in- elements ((#) :: T GInst)- == 1 + (abs x + 1) + (abs x + 1) * (abs x + 1)- , \x -> let ?bounds = Bounds $ abs x + 1 in- offset ((#) :: T GInst) == 0- , \x -> let ?bounds = Bounds $ abs x + 1 in- map index (values :: [GInst])- == [0,1..elements ((#) :: T GInst) - 1]- , \x -> let ?bounds = Bounds $ abs x + 1 in- map value [0,1..elements ((#) :: T GInst) - 1]- == (values :: [GInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- all (\x -> x == value (index x)) (values :: [GInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- complement (filter (odd . index) (values :: [GInst]))- == filter (even . index) (values :: [GInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- initial ((#) :: T GInst) |<=| final ((#) :: T GInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else next (initial ((#) :: T GInst))- |>=| initial ((#) :: T GInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else previous (final ((#) :: T GInst))- |/=| final ((#) :: T GInst)+ [ \x -> sb x $ elements (type GInst)+ == 1 + (abs x + 1) + (abs x + 1) * (abs x + 1)+ , \x -> sb x $ offset (type GInst) == 0+ , \x -> sb x $ map index vs == [0,1..elements (type GInst) - 1]+ , \x -> sb x $ map value [0,1..elements (type GInst) - 1] == vs+ , \x -> sb x $ all (\x -> x == value (index x)) vs+ , \x -> sb x $ complement (filter (odd . index) vs)+ == filter (even . index) vs+ , \x -> sb x $ initial (type GInst) |<=| final (type GInst)+ , \x -> sb x $ abs x < 1 ||+ next (initial (type GInst))+ |>=| initial (type GInst)+ , \x -> sb x $ abs x < 1 ||+ previous (final (type GInst))+ |/=| final (type GInst) ]) , name = "Generics" , tags = [] , options = [] , setOption = \_ _ -> Right t05 }+ where+ vs :: FiniteBounds Bounds => [GInst]+ vs = values + sb :: Int -> (FiniteBounds Bounds => c) -> c+ sb x = withBounds $ Bounds $ abs x + 1+ t06 = TestInstance { run = (Finished . allPass) <$> sequence (map quickCheckResult- [ \x -> let ?bounds = Bounds $ abs x + 1 in- elements ((#) :: T OInst) == abs x + 1- , \x -> let ?bounds = Bounds $ abs x + 1 in- offset ((#) :: T OInst) == 3- , \x -> let ?bounds = Bounds $ abs x + 1 in- map index (values :: [OInst]) == [3,4..abs x + 3]- , \x -> let ?bounds = Bounds $ abs x + 1 in- map value [3,4..abs x + 3] == (values :: [OInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- all (\x -> x == value (index x)) (values :: [OInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- complement (filter (odd . index) (values :: [OInst]))- == filter (even . index) (values :: [OInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- initial ((#) :: T OInst) |<=| final ((#) :: T OInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else next (initial ((#) :: T OInst))- |>=| initial ((#) :: T OInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else previous (final ((#) :: T OInst))- |/=| final ((#) :: T OInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- elements ((#) :: T TInst)- == 1 + (abs x + 1) + (abs x + 1) * (abs x + 1)- , \x -> let ?bounds = Bounds $ abs x + 1 in- offset ((#) :: T TInst) == 0- , \x -> let ?bounds = Bounds $ abs x + 1 in- map index (values :: [TInst])- == [0,1..elements ((#) :: T TInst) - 1]- , \x -> let ?bounds = Bounds $ abs x + 1 in- map value [0,1..elements ((#) :: T TInst) - 1]- == (values :: [TInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- all (\x -> x == value (index x)) (values :: [TInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- complement (filter (odd . index) (values :: [TInst]))- == filter (even . index) (values :: [TInst])- , \x -> let ?bounds = Bounds $ abs x + 1 in- initial ((#) :: T TInst) |<=| final ((#) :: T TInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else next (initial ((#) :: T TInst))- |>=| initial ((#) :: T TInst)- , \x -> let ?bounds = Bounds $ abs x + 1 in- if abs x < 1 then True- else previous (final ((#) :: T TInst))- |/=| final ((#) :: T TInst)+ [ \x -> sb x $ elements (type OInst) == abs x + 1+ , \x -> sb x $ offset (type OInst) == 3+ , \x -> sb x $ map index ovs == [3,4..abs x + 3]+ , \x -> sb x $ map value [3,4..abs x + 3] == ovs+ , \x -> sb x $ all (\x -> x == value (index x)) ovs+ , \x -> sb x $ complement (filter (odd . index) ovs)+ == filter (even . index) ovs+ , \x -> sb x $ initial (type OInst) |<=| final (type OInst)+ , \x -> sb x $ abs x < 1 ||+ next (initial (type OInst))+ |>=| initial (type OInst)+ , \x -> sb x $ abs x < 1 ||+ previous (final (type OInst))+ |/=| final (type OInst)+ , \x -> sb x $ elements (type TInst)+ == 1 + (abs x + 1) + (abs x + 1) * (abs x + 1)+ , \x -> sb x $ offset (type TInst) == 0+ , \x -> sb x $ map index tvs == [0,1..elements (type TInst) - 1]+ , \x -> sb x $ map value [0,1..elements (type TInst) - 1] == tvs+ , \x -> sb x $ all (\x -> x == value (index x)) tvs+ , \x -> sb x $ complement (filter (odd . index) tvs)+ == filter (even . index) tvs+ , \x -> sb x $ initial (type TInst) |<=| final (type TInst)+ , \x -> sb x $ abs x < 1 ||+ next (initial (type TInst))+ |>=| initial (type TInst)+ , \x -> sb x $ abs x < 1 ||+ previous (final (type TInst))+ |/=| final (type TInst) ]) , name = "Offset" , tags = [] , options = [] , setOption = \_ _ -> Right t06 }+ where+ ovs :: FiniteBounds Bounds => [OInst]+ ovs = values++ tvs :: FiniteBounds Bounds => [TInst]+ tvs = values++ sb :: Int -> (FiniteBounds Bounds => c) -> c+ sb x = withBounds $ Bounds $ abs x + 1 allPass xs = case dropWhile (isSuccess) xs of [] -> Pass