diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Readme.md b/Readme.md new file mode 100644 --- /dev/null +++ b/Readme.md @@ -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) + ] +``` diff --git a/finite.cabal b/finite.cabal new file mode 100644 --- /dev/null +++ b/finite.cabal @@ -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 +maintainer: Felix Klein +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 diff --git a/src/lib/Finite.hs b/src/lib/Finite.hs new file mode 100644 --- /dev/null +++ b/src/lib/Finite.hs @@ -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(..) + ) + +----------------------------------------------------------------------------- diff --git a/src/lib/Finite/Class.hs b/src/lib/Finite/Class.hs new file mode 100644 --- /dev/null +++ b/src/lib/Finite/Class.hs @@ -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 + +----------------------------------------------------------------------------- diff --git a/src/lib/Finite/Collection.hs b/src/lib/Finite/Collection.hs new file mode 100644 --- /dev/null +++ b/src/lib/Finite/Collection.hs @@ -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) + +----------------------------------------------------------------------------- diff --git a/src/lib/Finite/PowerSet.hs b/src/lib/Finite/PowerSet.hs new file mode 100644 --- /dev/null +++ b/src/lib/Finite/PowerSet.hs @@ -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 [] + +----------------------------------------------------------------------------- diff --git a/src/lib/Finite/TH.hs b/src/lib/Finite/TH.hs new file mode 100644 --- /dev/null +++ b/src/lib/Finite/TH.hs @@ -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" +-- +-- newtype Example = +-- Example { example :: Int } +-- deriving (Eq, Ord) +-- +-- instance Show Example where +-- show (Example x) = show x +-- +-- instance Hashable Example where +-- hashWithSalt s (Example x) = hashWithSalt s x +-- +-- 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) +-- +-- instance Arbitrary Example where +-- arbitrary = Example <$> arbitrary +-- shrink (Example x) = map Example $ shrink x +-- +-- 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" +-- +-- 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 +-- +-- instance Finite Bounds Example +-- +-- >>> :t derive +-- +-- derive :: NewBounds -> Bounds +-- +-- >>> extendInstance [t|Example|] [t|NewBounds] [|translate|] +-- +-- 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" +-- +-- 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 + +----------------------------------------------------------------------------- diff --git a/src/lib/Finite/Type.hs b/src/lib/Finite/Type.hs new file mode 100644 --- /dev/null +++ b/src/lib/Finite/Type.hs @@ -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 () + +----------------------------------------------------------------------------- diff --git a/src/test/Test.hs b/src/test/Test.hs new file mode 100644 --- /dev/null +++ b/src/test/Test.hs @@ -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 + +-----------------------------------------------------------------------------