finite (empty) → 1.4.1.1
raw patch · 10 files changed
+2022/−0 lines, 10 filesdep +Cabaldep +QuickCheckdep +array
Dependencies added: Cabal, QuickCheck, array, base, containers, finite, hashable, template-haskell
Files
- LICENSE +20/−0
- Readme.md +84/−0
- finite.cabal +85/−0
- src/lib/Finite.hs +78/−0
- src/lib/Finite/Class.hs +371/−0
- src/lib/Finite/Collection.hs +153/−0
- src/lib/Finite/PowerSet.hs +124/−0
- src/lib/Finite/TH.hs +656/−0
- src/lib/Finite/Type.hs +93/−0
- src/test/Test.hs +358/−0
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2021 Felix Klein++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Readme.md view
@@ -0,0 +1,84 @@+# Finite++The library provides the Haskell class `Finite`, which allows to+associate types with finite ranges of elements in the context of a+bounding environment. The purpose of the class is to simplify the+handling of objects of bounded size, e.g. finite-state machines, where+the number of elements can be defined in the context of the object,+e.g. the number of states.++## Main Features++* Easy access to the object's elements via types.++* 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.++* Easy passing of the context via [implict+parameters](https://www.haskell.org/hugs/pages/users_guide/implicit-parameters.html).++* [Generics](https://wiki.haskell.org/Generics) Support: Finite range+ types can be easily constructed out of other finite range types+ using Haskell's `data` constructor.++* [Template Haskell](https://wiki.haskell.org/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.++## Example: Finite-State Machines++```haskell+import Finite+import Finite.TH++-- create two new basic types for the states and labels of the FSM+newInstance "State"+newInstance "Label"++-- FSM data type+data FSM =+ FSM+ { states :: Int+ , labels :: Int+ , transition :: State -> Label -> State+ , accepting :: State -> Bool+ , labelName :: Label -> String+ }++-- connect the types with corresponding bounds, as defined by the FSM+baseInstance [t|FSM|] [|states|] "State"+baseInstance [t|FSM|] [|labels|] "Label"++-- FSM Show instance for demonstrating the features of 'Finite'+instance Show FSM where+ show fsm =+ -- set the context+ let ?bounds = fsm in+ -- show the data+ unlines $+ [ "The FSM has " ++ show (elements ((#) :: T State)) ++ " states."+ ] +++ [ "Labels:"+ ] +++ [ " (" ++ show (index l) ++ ") " ++ labelName fsm l+ | l <- values+ ] +++ [ "Transitions:"+ ] +++ [ " " ++ show (index s) ++ " -- " ++ labelName fsm l +++ " --> " ++ show (index (transition fsm s l))+ | s <- values+ , l <- values+ ] +++ [ "Accepting:"+ ] +++ [ " " ++ show (map index $ filter (accepting fsm) values)+ ]+```
+ finite.cabal view
@@ -0,0 +1,85 @@+name: finite+version: 1.4.1.1+synopsis: Finite ranges via types+description: A framework for capturing finite ranges with+ types, where the sizes of the ranges are not+ fixed statically at compile time, but instead+ are passed at run-time via implicit parameters.+ .+ This is especially useful for objects of bounded+ size, e.g. finite automata, where the number of+ elements being part of the object, e.g. the number+ of states, is well-defined in the context of the+ object.+license: MIT+license-file: LICENSE+category: Types+author: Felix Klein <klein@react.uni-saarland.de>+maintainer: Felix Klein <klein@react.uni-saarland.de>+stability: stable+build-type: Simple+extra-source-files: Readme.md+cabal-version: >=1.10++source-repository head+ type: git+ location: https://github.com/kleinreact/finite++library++ ghc-options:+ -Wall+ -Wno-name-shadowing+ -Wno-orphans+ -fignore-asserts++ build-depends:+ base >=4.7 && <4.13+ , array >=0.5 && <0.6+ , containers >=0.5 && <0.7+ , hashable >=1.2+ , template-haskell >=2.11+ , QuickCheck++ exposed-modules:+ Finite+ Finite.TH++ other-modules:+ Finite.Class+ Finite.PowerSet+ Finite.Collection+ Finite.Type++ hs-source-dirs:+ src/lib++ default-language:+ Haskell2010++test-suite default++ ghc-options:+ -Wall+ -Wno-name-shadowing+ -Wno-orphans+ -fno-ignore-asserts++ type:+ detailed-0.9++ test-module:+ Test++ hs-source-dirs:+ src/test++ build-depends:+ base >=4.7 && <4.13+ , hashable >=1.2+ , Cabal >= 2.4+ , QuickCheck+ , finite++ default-language:+ Haskell2010
+ src/lib/Finite.hs view
@@ -0,0 +1,78 @@+-----------------------------------------------------------------------------+-- |+-- Module : Finite+-- Maintainer : Felix Klein+--+-- A framework for capturing finite ranges with types, where the sizes+-- of the ranges are not fixed statically at compile time, but instead+-- are passed at run-time via implicit parameters. The purpose of the+-- framework is to simplify the handling of objects of bounded size,+-- e.g. finite-state machines, where the number of elements can be+-- defined in the context of the object, e.g. the number of states.+--+-- The framework supports:+--+-- * Easy access to the object's elements via types.+-- * 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.+-- * 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.+-- * 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+-- explicit import of @Finite.TH@).+--+-----------------------------------------------------------------------------++module Finite+ ( -- * The Finite Class+ Finite(..)+ , GFinite(..)+ , FiniteBounds+ , -- * Powersets+ PowerSet+ , -- * Collections+ Collection(..)+ , -- * Polymorphic Type Access+ T+ , (#)+ , (\#)+ , (<<#)+ , (#<<)+ , v2t+ , t2v+ ) where++-----------------------------------------------------------------------------++import Finite.Type+ ( T+ , FiniteBounds+ , (#)+ , (\#)+ , (<<#)+ , (#<<)+ , t2v+ , v2t+ )++import Finite.Class+ ( Finite(..)+ , GFinite(..)+ )++import Finite.PowerSet+ ( PowerSet+ )++import Finite.Collection+ ( Collection(..)+ )++-----------------------------------------------------------------------------
+ src/lib/Finite/Class.hs view
@@ -0,0 +1,371 @@+-----------------------------------------------------------------------------+-- |+-- Module : Finite.Class+-- Maintainer : Felix Klein+--+-- 'Finite' main class decleration including generics support.+--+-----------------------------------------------------------------------------++{-# LANGUAGE++ MultiWayIf+ , TypeOperators+ , DefaultSignatures+ , MultiParamTypeClasses+ , FlexibleContexts+ , FlexibleInstances++ #-}++-----------------------------------------------------------------------------++module Finite.Class+ ( T+ , Finite(..)+ , GFinite(..)+ ) where++-----------------------------------------------------------------------------++import Control.Exception+ ( assert+ )++import Finite.Type+ ( T+ , FiniteBounds+ , (#<<)+ , (<<#)+ , v2t+ , (\#)+ , (#)+ )++import GHC.Generics+ ( Generic+ , Rep+ , (:*:)(..)+ , (:+:)(..)+ , U1(..)+ , M1(..)+ , K1(..)+ , from+ , to+ )++import qualified Data.IntSet as S+ ( toList+ , fromList+ , fromAscList+ , difference+ )++-----------------------------------------------------------------------------++-- | The 'Finite' class.++class Finite b a where++ -- | Returns the number of elements associated with the given type.+ elements+ :: FiniteBounds b+ => T a -> Int++ default elements+ :: (Generic a, GFinite b (Rep a), FiniteBounds b)+ => T a -> Int++ elements t = gelements #<< from <<# t++ -- | 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 v = (+ (offset $ v2t v)) $ gindex $ from v++ -- | Turns an Int back to the value that is associated with it.+ value+ :: 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++ -- | Allows to put an offset to the integer mapping. Per default the+ -- offset is zero.+ offset+ :: FiniteBounds b+ => T a -> 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 _ = (#)++ -- | 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 _ = (#)++ -- | Less than operator according to the implicit total index order.+ (|<|)+ :: 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++ infixr |<=|++ -- | Greater or equal than operator according to the implicit total+ -- index order.+ (|>=|)+ :: 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++ infixr |>|++ -- | Equal operator according to the implicit total index order.+ (|==|)+ :: 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++ infixr |/=|+++ -- | First element according to the total index order.+ initial+ :: FiniteBounds b+ => T a -> a++ initial t =+ value $ offset t++ -- | Last element according to the total index order.+ final+ :: FiniteBounds b+ => T a -> a++ final t =+ value $ offset t + elements t - 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)++ -- | 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)++ -- | The upper and lower bounds of the instance.+ bounds+ :: FiniteBounds b+ => T a -> (a, a)++ bounds t =+ (initial t, final t)++-----------------------------------------------------------------------------++-- | 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+ 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.++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++-----------------------------------------------------------------------------++-- | U1 instance.++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))++ 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++-----------------------------------------------------------------------------
+ src/lib/Finite/Collection.hs view
@@ -0,0 +1,153 @@+-----------------------------------------------------------------------------+-- |+-- Module : Finite.Collection+-- Maintainer : Felix Klein+--+-- Allows to extend a finite instance from a single bound to a+-- collection of bounds, given as a finite ranged array.+--+-----------------------------------------------------------------------------++{-# LANGUAGE++ MultiParamTypeClasses+ , LambdaCase+ , ImplicitParams++ #-}++-----------------------------------------------------------------------------++module Finite.Collection where++-----------------------------------------------------------------------------++import Finite.Type+ ( T+ , v2t+ , (#<<)+ , FiniteBounds+ )++import Finite.Class+ ( Finite+ , elements+ , offset+ , value+ , index+ )++import Data.Array.IArray+ ( Array+ , Ix+ , (!)+ , inRange+ , assocs+ , range+ , bounds+ )++import Control.Exception+ ( assert+ )++-----------------------------------------------------------------------------++-- | 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+ deriving+ ( -- | Equality can be checked for collections, if the index type+ -- and the elements can be checked for equality.+ Eq+ , -- | Order can be checked for collections, if the index type and+ -- the elements can be oredered.+ Ord+ , -- | Show a collection through its default constructor.+ Show+ )++-----------------------------------------------------------------------------++-- | Collections are used to extend Finite-Type / Context-Bounds pairs+-- to an array of bounds. At the same time the finite type is extended+-- to a collection of items that range over the same set of indices as+-- 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++ elms v b =+ let ?bounds = b+ in elements $ v2t v++ 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)++ 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)++-----------------------------------------------------------------------------
+ src/lib/Finite/PowerSet.hs view
@@ -0,0 +1,124 @@+-----------------------------------------------------------------------------+-- |+-- Module : Finite.PowerSet+-- Maintainer : Felix Klein+--+-- Encodes the powerset of a finite range type.+--+-----------------------------------------------------------------------------++{-# LANGUAGE++ MultiParamTypeClasses+ , FlexibleInstances+ , FlexibleContexts+ , LambdaCase+ , MultiWayIf+ , BangPatterns++ #-}++-----------------------------------------------------------------------------++module Finite.PowerSet+ ( PowerSet+ ) where++-----------------------------------------------------------------------------++import Finite.Type+ ( T+ , (\#)+ , (#<<)+ )++import Finite.Class+ ( Finite(..)+ )++import Control.Exception+ ( assert+ )++-----------------------------------------------------------------------------++-- | 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++ 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 bs = map (value . (+ (offset #<< head bs))) $ bin n+ in assert (n >= 0 && n < (elements #<< bs)) bs++ offset = offset . ((\#) :: T (PowerSet a) -> T a)++ values = powerset values++-----------------------------------------------------------------------------++-- | 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)++-----------------------------------------------------------------------------++-- | 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 []++-----------------------------------------------------------------------------
+ src/lib/Finite/TH.hs view
@@ -0,0 +1,656 @@+-----------------------------------------------------------------------------+-- |+-- Module : Finite.TH+-- Maintainer : Felix Klein+--+-- Template haskell for easy instance generation using newtypes.+--+-----------------------------------------------------------------------------++{-# LANGUAGE++ LambdaCase+ , ImplicitParams+ , TemplateHaskell+ , CPP++ #-}++-----------------------------------------------------------------------------++module Finite.TH+ ( newInstance+ , baseInstance+ , newBaseInstance+ , extendInstance+ , polyType+ ) where++-----------------------------------------------------------------------------++import qualified Data.Ix+ ( Ix+ , index+ , range+ , inRange+ )++import Test.QuickCheck+ ( Arbitrary+ , arbitrary+ , shrink+ )++import Data.Hashable+ ( Hashable+ , hashWithSalt+ )++import Finite.Type+ ( T+ , FiniteBounds+ )++import Finite.Class+ ( Finite(..)+ )++import Data.Char+ ( toLower+ , isUpper+ )++import Control.Exception+ ( assert+ )++import Language.Haskell.TH+ ( Q+ , Dec+ , Exp+#if MIN_VERSION_template_haskell(2,12,0)+ , DerivClause(..)+#endif+ , Type(..)+ , mkName+ , conT+ , appT+ , conP+ , varP+ , tupP+ , wildP+ , varE+ , conE+ , tupE+ , appE+ , funD+ , newtypeD+ , instanceD+ , recC+ , normalB+ , cxt+ , clause+ , bangType+ , varBangType+ , bang+ , noSourceUnpackedness+ , noSourceStrictness+ )++-----------------------------------------------------------------------------++-- | Creates a new basic type using the name provided as a string. The+-- template defines the corresponding data type using the provided+-- name and a corresponding access function using the same name with+-- the first letter moved to lower case. Furthermore, it also+-- instanciates corresponding `Show`, `Hashable`, 'Ix', 'Arbitrary',+-- and 'Num' instances.+--+-- >>> newInstance "Example"+-- <BLANKLINE>+-- newtype Example =+-- Example { example :: Int }+-- deriving (Eq, Ord)+-- <BLANKLINE>+-- instance Show Example where+-- show (Example x) = show x+-- <BLANKLINE>+-- instance Hashable Example where+-- hashWithSalt s (Example x) = hashWithSalt s x+-- <BLANKLINE>+-- instance Ix Example where+-- range (l,u) = map Example $ range (example l, example u)+-- index (l,u) x = index (example l, example u) (example x)+-- inRange (l,u) x = inRange (example l, example u) (example x)+-- <BLANKLINE>+-- instance Arbitrary Example where+-- arbitrary = Example <$> arbitrary+-- shrink (Example x) = map Example $ shrink x+-- <BLANKLINE>+-- instance Num Example where+-- (Example x) + (Example y) = Example (a + b)+-- (Example x) - (Example y) = Example (a - b)+-- (Example x) * (Example y) = Example (a * b)+-- abs = Example . abs . example+-- negate = Example . negage . example+-- signum = Example . signum . example+-- fromInteger = Example . fromInteger++newInstance+ :: String -> Q [Dec]++newInstance = \case+ [] -> assert False undefined+ (x:xr) -> assert (isUpper x) $ do+ let+ tmpV = mkName "x"+ conC = mkName $ x : xr+ accV = mkName $ toLower x : xr+ emptyContext = cxt []+ intT = conT (''Int)++ d_newtype <-+ newtypeD+ -- no context+ emptyContext+ -- newtype name+ conC+ -- no type parameters+ []+ -- no kinds+ Nothing+ -- newtype constructor+ (recC -- normalC+ conC+ [varBangType+ accV+ (bangType+ (bang noSourceUnpackedness noSourceStrictness)+ intT)])+ -- derive 'Eq' and 'Ord'+#if MIN_VERSION_template_haskell(2,12,0)+ [ return (DerivClause+ Nothing+ [ ConT (''Eq)+ , ConT (''Ord)+ ])+ ]+#else+ (return [ConT (''Eq), ConT (''Ord)])+#endif++ d_show_instance <-+ instanceD+ -- no context+ emptyContext+ -- instance of 'Show'+ (appT (conT (''Show)) (conT conC))+ -- declare 'show'+ [ funD ('show)+ [ clause+ -- pattern match constructor+ [conP conC [varP tmpV]]+ -- show inner content+ (normalB (appE (varE ('show)) (varE tmpV)))+ --+ [] ] ]++ d_hashable_instance <-+ instanceD+ -- no context+ emptyContext+ -- instance of 'Hashable'+ (appT (conT (''Hashable)) (conT conC))+ -- declare 'hashWithSalt'+ [ funD ('hashWithSalt)+ [ clause+ -- pattern match constructor+ [varP (mkName "s"), conP conC [varP tmpV]]+ -- show inner content+ (normalB (appE (appE (varE ('hashWithSalt))+ (varE (mkName "s")))+ (varE tmpV)))+ [] ] ]++ d_ix_instance <-+ instanceD+ -- no context+ emptyContext+ -- instance of 'Ix'+ (appT (conT (''Data.Ix.Ix)) (conT conC))+ -- declare 'range'+ [ funD ('Data.Ix.range)+ [ clause+ -- pattern match constructor+ [tupP [ varP (mkName "l"), varP (mkName "s") ]]+ -- show inner content+ (normalB+ (appE+ (appE (varE ('map)) (conE conC))+ (appE+ (varE ('Data.Ix.range))+ (tupE [ appE (varE accV) (varE (mkName "l"))+ , appE (varE accV) (varE (mkName "s"))+ ] ))))+ [] ]++ , funD ('Data.Ix.index)+ [ clause+ -- pattern match constructor+ [tupP [ varP (mkName "l"), varP (mkName "s") ]+ ,conP conC [varP tmpV]+ ]+ -- show inner content+ (normalB+ (appE+ (appE+ (varE ('Data.Ix.index))+ (tupE [ appE (varE accV) (varE (mkName "l"))+ , appE (varE accV) (varE (mkName "s"))+ ] ))+ (varE tmpV) ))+ [] ]+ , funD ('Data.Ix.inRange)+ [ clause+ -- pattern match constructor+ [tupP [ varP (mkName "l"), varP (mkName "s") ]+ ,conP conC [varP tmpV]+ ]+ -- show inner content+ (normalB+ (appE+ (appE+ (varE ('Data.Ix.inRange))+ (tupE [ appE (varE accV) (varE (mkName "l"))+ , appE (varE accV) (varE (mkName "s"))+ ] ))+ (varE tmpV) ))+ [] ] ]++ d_num_instance <-+ instanceD+ -- no context+ emptyContext+ -- instance of 'Num'+ (appT (conT (''Num)) (conT conC))+ -- declare '(+)'+ [ funD ('(+))+ [ clause+ -- pattern match constructor+ [ conP conC [varP (mkName "x")]+ , conP conC [varP (mkName "y")]+ ]+ -- (+) inner content+ (normalB+ (appE+ (conE conC)+ (appE+ (appE+ (varE ('(+)))+ (varE (mkName "x")))+ (varE (mkName "y")))))+ [] ]+ , funD ('(-))+ [ clause+ -- pattern match constructor+ [ conP conC [varP (mkName "x")]+ , conP conC [varP (mkName "y")]+ ]+ -- (+) inner content+ (normalB+ (appE+ (conE conC)+ (appE+ (appE+ (varE ('(-)))+ (varE (mkName "x")))+ (varE (mkName "y")))))+ [] ]+ , funD ('(*))+ [ clause+ -- pattern match constructor+ [ conP conC [varP (mkName "x")]+ , conP conC [varP (mkName "y")]+ ]+ -- (+) inner content+ (normalB+ (appE+ (conE conC)+ (appE+ (appE+ (varE ('(*)))+ (varE (mkName "x")))+ (varE (mkName "y")))))+ [] ]+ , funD ('abs)+ [ clause+ -- pattern match constructor+ [conP conC [varP tmpV]]+ -- show inner content+ (normalB (appE (conE conC) (appE (varE ('abs)) (varE tmpV))))+ --+ [] ]+ , funD ('negate)+ [ clause+ -- pattern match constructor+ [conP conC [varP tmpV]]+ -- show inner content+ (normalB+ (appE+ (conE conC)+ (appE (varE ('negate)) (varE tmpV))))+ --+ [] ]+ , funD ('signum)+ [ clause+ -- pattern match constructor+ [conP conC [varP tmpV]]+ -- show inner content+ (normalB+ (appE+ (conE conC)+ (appE (varE ('signum)) (varE tmpV))))+ --+ [] ]+ , funD ('fromInteger)+ [ clause+ -- pattern match constructor+ [varP tmpV]+ -- show inner content+ (normalB+ (appE+ (conE conC)+ (appE (varE ('fromInteger)) (varE tmpV))))+ --+ [] ] ]++ d_arbitrary_instance <-+ instanceD+ -- no context+ emptyContext+ -- instance of 'Hashable'+ (appT (conT (''Arbitrary)) (conT conC))+ -- declare 'hashWithSalt'+ [ funD ('arbitrary)+ [ clause+ -- pattern match constructor+ []+ -- show inner content+ (normalB+ (appE+ (appE+ (varE ('(<$>)))+ (conE conC))+ (varE ('arbitrary))))+ [] ]+ , funD ('shrink)+ [ clause+ -- pattern match constructor+ [conP conC [varP tmpV]]+ -- show inner content+ (normalB+ (appE+ (appE (varE ('map)) (conE conC))+ (appE (varE ('shrink)) (varE tmpV))))+ [] ] ]++ return+ [ d_newtype+ , d_show_instance+ , d_hashable_instance+ , d_ix_instance+ , d_num_instance+ , d_arbitrary_instance+ ]++-----------------------------------------------------------------------------++-- | Creates a basic finite instance using the bounds provided via the+-- first argument, the access function provided by the second argument+-- and the name provided as a string.+--+-- >>> baseInstance [t|Bounds|] [|getBound|] "Example"+-- <BLANKLINE>+-- instance Finite Bounds Example where+-- elements _ = getBound ?bounds+-- value = Example+-- index = example++baseInstance+ :: Q Type -> Q Exp -> String -> Q [Dec]++baseInstance bounds f = \case+ [] -> assert False undefined+ (x:xr) -> assert (isUpper x) $ do+ let+ tmpV = mkName "x"+ conC = mkName $ x : xr+ emptyContext = cxt []++ d_finite_instance <-+ instanceD+ -- no context+ emptyContext+ -- instanc of 'Finite'+ (appT (appT (conT (''Finite)) bounds) (conT conC))+ -- declare+ [ funD ('elements)+ [ clause+ -- ignore the pattern+ [ wildP ]+ -- get the value from the configuartion+ (normalB (appE (varE 'appBounds) f))+ --+ [] ]+ , funD ('value)+ [ clause+ -- get the value+ [ varP tmpV ]+ -- apply the constructor+ (normalB+ (appE+ (appE+ (varE 'assert)+ (appE+ (appE (varE 'inRange) (varE tmpV))+ (appE (varE 'appBounds) f)))+ (appE (conE conC) (varE tmpV))))+ --+ [] ]+ , funD ('index)+ [ clause+ -- get the value+ [ conP conC [varP tmpV] ]+ -- apply the destructor+ (normalB+ (appE+ (appE+ (varE 'assert)+ (appE+ (appE (varE 'inRange) (varE tmpV))+ (appE (varE 'appBounds) f)))+ (varE tmpV)))+ --+ [] ]+ ]++ return [ d_finite_instance ]++-----------------------------------------------------------------------------++-- | Combined 'newInstance' with 'baseInstance'.++newBaseInstance+ :: Q Type -> Q Exp -> String -> Q [Dec]++newBaseInstance bounds f name = do+ xs <- newInstance name+ ys <- baseInstance bounds f name+ return $ xs ++ ys++-----------------------------------------------------------------------------++-- | Extends a Finite instance to an extended parameter space. The+-- first argument takes the type to be extended, the second argument+-- the type of the new parameter space and the third argument a+-- translator function that translates the old parameter space into+-- the new one.+--+-- >>> :i Bounds+-- <BLANKLINE>+-- instance Finite Bounds Example+-- <BLANKLINE>+-- >>> :t derive+-- <BLANKLINE>+-- derive :: NewBounds -> Bounds+-- <BLANKLINE>+-- >>> extendInstance [t|Example|] [t|NewBounds] [|translate|]+-- <BLANKLINE>+-- instance Finite NewBounds Example where+-- elements = let ?bounds = translate ?bounds in elements+-- 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 rtype bounds access = do+ let tmpV = mkName "x"+ d_finite_instance <-+ instanceD+ -- no context+ (cxt [])+ -- instanc of 'Finite'+ (appT (appT (conT (''Finite)) bounds) rtype)+ -- declare+ [ funD ('elements)+ [ clause+ -- ignore the pattern+ [ varP tmpV ]+ -- get the value from the configuartion+ (normalB+ (appE+ (appE+ (varE 'elementsSwitch)+ access)+ (varE tmpV)))+ --+ [] ]+ , funD ('offset)+ [ clause+ -- ignore the pattern+ [ varP tmpV ]+ -- get the value from the configuartion+ (normalB+ (appE+ (appE+ (varE 'offsetSwitch)+ access)+ (varE tmpV)))+ --+ [] ]+ , funD ('value)+ [ clause+ -- ignore the pattern+ [ varP tmpV ]+ -- get the value from the configuartion+ (normalB+ (appE+ (appE+ (varE 'valueSwitch)+ access)+ (varE tmpV)))+ --+ [] ]+ , funD ('index)+ [ clause+ -- ignore the pattern+ [ varP tmpV ]+ -- get the value from the configuartion+ (normalB+ (appE+ (appE+ (varE 'indexSwitch)+ access)+ (varE tmpV)))+ --+ [] ]+ ]+ return [d_finite_instance]++-----------------------------------------------------------------------------++-- | Constructs a polymorph type given a type constructor and a free+-- type variable. Such a construction cannot be expressed in quotation+-- syntax directly.+--+-- >>> polyType [t|Maybe|] "a"+-- <BLANKLINE>+-- Maybe a++polyType+ :: Q Type -> String -> Q Type++polyType con str = do+ t <- con+ return $ t `AppT` (VarT $ mkName str)++-----------------------------------------------------------------------------++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++-----------------------------------------------------------------------------++offsetSwitch+ :: (Finite b' a, FiniteBounds b)+ => (b -> b') -> T a -> Int++offsetSwitch f =+ let ?bounds = f ?bounds+ in offset++-----------------------------------------------------------------------------++indexSwitch+ :: (Finite b' a, FiniteBounds b)+ => (b -> b') -> a -> Int++indexSwitch f =+ let ?bounds = f ?bounds+ in index++-----------------------------------------------------------------------------++valueSwitch+ :: (Finite b' a, FiniteBounds b)+ => (b -> b') -> Int -> a++valueSwitch f =+ let ?bounds = f ?bounds+ in value++-----------------------------------------------------------------------------++inRange+ :: Int -> Int -> Bool++inRange x y =+ x >= 0 && x < y++-----------------------------------------------------------------------------
+ src/lib/Finite/Type.hs view
@@ -0,0 +1,93 @@+-----------------------------------------------------------------------------+-- |+-- 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
@@ -0,0 +1,358 @@+-----------------------------------------------------------------------------+-- |+-- Module : Test+-- Maintainer : Felix Klein+--+-- Simple TestSuite.+--+-----------------------------------------------------------------------------++{-# LANGUAGE++ LambdaCase+ , ImplicitParams+ , RecordWildCards+ , DeriveGeneric+ , TemplateHaskell+ , MultiParamTypeClasses++ #-}++-----------------------------------------------------------------------------++module Test+ ( tests+ ) where++-----------------------------------------------------------------------------++import Distribution.TestSuite+ ( TestInstance(..)+ , Progress(..)+ , Result(..)+ , Test(..)+ )++import Data.Hashable+ ( hash+ )++import Data.Ix+ ( range+ )++import Control.Exception+ ( assert+ )++import GHC.Generics+ ( Generic+ )++import Test.QuickCheck+ ( Result+ ( Success+ , Failure+ , reason+ )+ , quickCheckResult+ )++import Finite.TH++import Finite++-----------------------------------------------------------------------------++newInstance "AInst"++data Bounds = Bounds { size :: Int }++baseInstance [t|Bounds|] [|size|] "AInst"++newBaseInstance [t|Bounds|] [|size|] "BInst"++data BBounds = BBounds { bnds :: Bounds }++extendInstance [t|AInst|] [t|BBounds|] [|bnds|]++data GInst =+ AData+ | BData AInst+ | CData AInst BInst+ deriving (Eq, Ord, Generic)++instance Finite Bounds GInst++newtype OInst = OInst { oInst :: Int } deriving (Eq, Ord)++instance Finite Bounds OInst where+ elements _ = size ?bounds+ offset _ = 3+ value = OInst+ index = oInst++data TInst =+ DData+ | EData OInst+ | FData AInst BInst+ deriving (Eq, Ord, Generic)++instance Finite Bounds TInst++-----------------------------------------------------------------------------++tests+ :: IO [Test]++tests = return+ [ Test t01+ , Test t02+ , Test t03+ , Test t04+ , Test t05+ , Test t06+ ]++ where+ t01 = TestInstance+ { run =+ (Finished . allPass) <$> sequence+ (map quickCheckResult+ [ \x -> x == aInst (AInst x)+ , \x -> AInst x == AInst x+ , \x -> AInst x < AInst (x + 1)+ , \x -> show (AInst x) == show (AInst x)+ , \x -> show (AInst x) == show x+ , \x -> hash (AInst x) == hash (AInst x)+ , \x -> not $ null $ range (AInst 0, AInst $ abs x)+ , \x -> (AInst x) + (AInst 1) == (AInst 1) + (AInst x)+ ] +++ [ quickCheckResult $ \x -> aInst x == aInst x+ ])+ , name = "TH: newInstance"+ , tags = []+ , options = []+ , setOption = \_ _ -> Right t01+ }++ t02 = TestInstance+ { 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)+ ])+ , name = "TH: baseInstance"+ , tags = []+ , options = []+ , setOption = \_ _ -> Right t02+ }++ t03 = TestInstance+ { run =+ (Finished . allPass) <$> sequence+ (map quickCheckResult+ [ \x -> x == bInst (BInst x)+ , \x -> BInst x == BInst x+ , \x -> BInst x < BInst (x + 1)+ , \x -> show (BInst x) == show (BInst x)+ , \x -> show (BInst x) == show x+ , \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)+ ] +++ [ quickCheckResult $ \x -> bInst x == bInst x+ ])+ , name = "TH: newBaseInstance"+ , tags = []+ , options = []+ , setOption = \_ _ -> Right t03+ }++ 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)+ ])+ , name = "TH: extendInstance"+ , tags = []+ , options = []+ , setOption = \_ _ -> Right t04+ }++ 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)+ ])+ , name = "Generics"+ , tags = []+ , options = []+ , setOption = \_ _ -> Right t05+ }++ 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)+ ])+ , name = "Offset"+ , tags = []+ , options = []+ , setOption = \_ _ -> Right t06+ }++ allPass xs = case dropWhile (isSuccess) xs of+ [] -> Pass+ x:_ -> case x of+ Failure{..} -> Fail reason+ _ -> assert False undefined++ isSuccess = \case+ Success {} -> True+ _ -> False++-----------------------------------------------------------------------------