-- | Abstraction on a "zipped" list. Use these instances to have a list cursored on a position, also -- called double linked list. module Engine where import Test.QuickCheck import Control.Monad import Data.Maybe import Data.List -- | represent an action, which can fail with Nothing , an index error type Change a = a -> Maybe a -- | Pos represent the position addressed in the engine data Pos -- | the engine addresses a real line = Line { nth :: Int -- ^ The index of the line starting from 1 } -- | the engine addresses before first line , if ever present | Begin -- | the engine addresses after last line | End { lns :: Int -- ^ The number of lines in the engine } deriving Show -- | relative distance between two positions distance (Line n) (Line m) = m - n +1 distance Begin (Line m) = m distance (Line n) (End m) = m - n distance Begin (End m) = m distance _ _ = 0 -- | the class to implement for holding a list of elements with a cursor on them class Eq a => Engine a where -- | An empty engine empty :: a empty = listIn [] -- | An engine is isomorphic to a list listIn :: [String] -> a -- | Extract the list from the engine listOut :: a -> Maybe [String] -- | Extract n lines from the position addressed linen :: Int -> a -> Maybe [String] -- | Extract the addressed line line :: a -> Maybe String line w = head `fmap` linen 1 w -- | Possibly set the addressed line to the nth line jump :: Int -> Change a -- | Insert some lines before the addressed line ins :: [String] -> Change a -- | Insert some lines after the addressed line add :: [String] -> Change a -- | Delete the addressed line , address the next one del :: Change a -- | Delete n lines from the addressed position deln :: Int -> Change a -- | Address an append position end :: Change a -- | Address before the first line start :: Change a -- | The number of the addressed line pos :: a -> Pos -- | Address the next line next :: Change a -- | Address the prev line prev :: Change a -- | Jump back n lines prevn :: Int -> Change a prevn 0 w = Just w prevn n w = prev w >>= prevn (n-1) -- | Jump ahead n lines nextn :: Int -> Change a nextn 0 w = Just w nextn n w = next w >>= nextn (n-1) -- | Jump n lines relative to the addredded line rjump :: Int -> Change a rjump n = iterateM n (if n > 0 then next else prev) where iterateM n f w | n > 0 = f w >>= iterateM (n - 1) f | True = Just w -- | Create all the engines from the addressed one to the last one tillend :: a -> [a] -- | all the next engines from the addressed next to itself , wrapping around fwdcycle :: a -> [a] -- | Create all the engines from the start to the addressed one included fromstart :: a -> [a] -- | all the prev engines from the addressed prev to itself , wrapping around bwdcycle :: a -> [a] -- | last element if present last :: Engine w => Change w last t = end t >>= prev -- | first element if present first :: Engine w => Change w first t = start t >>= next newtype W w = W w deriving Show instance (Eq w,Engine w) => Arbitrary (W w) where arbitrary = do n <- choose (0,10) ws <- replicateM n $ replicateM 15 $ choose ('a','z') return $ W $ listIn ws coarbitrary = undefined instance Arbitrary Char where arbitrary = choose ('a','z') coarbitrary = undefined prop_E1 :: (Engine w) => W w -> String -> Bool prop_E1 (W y) = \x -> (add [x] y >>= listOut) == Just (x:fromJust (listOut y)) propInOut f xs = Just $ listIn xs >>= f >>= listOut prop_Empty (W y) = (y == empty) ==> prev y == Nothing && next y == Nothing prop_toEnd (W y) = (y /= empty) ==> let Just ls = length `fmap` listOut y in collect ls $ nextn (ls +1) y == end y && nextn ls y == (end y >>= prev) prop_toEndAndBack (W y) = (y /= empty) ==> let Just ls = length `fmap` listOut y in collect ls $ (end y >>= start) == Just y prop_add (W y) xs = (add xs y >>= listOut) == Just xs --prop_ins (W y) xs = (listIn xs >>= end >>= ins xs >>= listOut) == Just (head xs:head -- -- data Prop w = forall p . (Engine w) => Prop w (\w -> \p -> Property)