Commit ceb3fffd authored by Michael Hanus 's avatar Michael Hanus

Synched with current lib-trunk

parent d8ef9ec6
------------------------------------------------------------------------------
--- Library for formatted output on terminals
---
--- Information on ANSI Codes can be found at
--- http://en.wikipedia.org/wiki/ANSI_escape_code
---
--- @author Sebastian Fischer, Bjoern Peemoeller
--- @version March 2015
--- @category general
------------------------------------------------------------------------------
module AnsiCodes
( -- cursor movement
cursorPos
, cursorHome
, cursorUp
, cursorDown
, cursorFwd
, cursorBack
, saveCursor
, restoreCursor
-- graphics control
, clear
, eraseLine
-- formatting output
, normal
, bold
, faint
, italic
, underline
, blinkSlow
, blinkRapid
, inverse
, concealed
, crossedout
-- foreground color
, black
, red
, green
, yellow
, blue
, cyan
, magenta
, white
, fgDefault
-- background color
, bgBlack
, bgRed
, bgGreen
, bgYellow
, bgBlue
, bgCyan
, bgMagenta
, bgWhite
, bgDefault
) where
import List (isSuffixOf)
-- -----------------------------------------------------------------------------
-- Cursor movement
-- -----------------------------------------------------------------------------
--- move cursor to position
cursorPos :: Int -> Int -> String
cursorPos r c = cmd (show r ++ ";" ++ show c ++ "H")
--- move cursor to home position
cursorHome :: String
cursorHome = cmd "H"
--- move cursor n lines up
cursorUp :: Int -> String
cursorUp = moveCursor "A"
--- move cursor n lines down
cursorDown :: Int -> String
cursorDown = moveCursor "B"
--- move cursor n columns forward
cursorFwd :: Int -> String
cursorFwd = moveCursor "C"
--- move cursor n columns backward
cursorBack :: Int -> String
cursorBack = moveCursor "D"
--- save cursor position
saveCursor :: String
saveCursor = cmd "s"
--- restore saved cursor position
restoreCursor :: String
restoreCursor = cmd "u"
-- -----------------------------------------------------------------------------
-- Graphics control
-- -----------------------------------------------------------------------------
--- clear screen
clear :: String
clear = cmd "2J"
--- erase line
eraseLine :: String
eraseLine = cmd "K"
-- -----------------------------------------------------------------------------
-- Text formatting
-- -----------------------------------------------------------------------------
--- Reset formatting to normal formatting
normal :: String -> String
normal = mode 0
--- Bold text
bold :: String -> String
bold = mode 1
--- Faint text
faint :: String -> String
faint = mode 2
--- Italic text
italic :: String -> String
italic = mode 3
--- Underlined text
underline :: String -> String
underline = mode 4
--- Slowly blinking text
blinkSlow :: String -> String
blinkSlow = mode 5
--- rapidly blinking text
blinkRapid :: String -> String
blinkRapid = mode 6
--- Inverse colors
inverse :: String -> String
inverse = mode 7
--- Concealed (invisible) text
concealed :: String -> String
concealed = mode 8
--- Crossed out text
crossedout :: String -> String
crossedout = mode 9
-- -----------------------------------------------------------------------------
-- Foreground color
-- -----------------------------------------------------------------------------
--- Black foreground color
black :: String -> String
black = mode 30
--- Red foreground color
red :: String -> String
red = mode 31
--- Green foreground color
green :: String -> String
green = mode 32
--- Yellow foreground color
yellow :: String -> String
yellow = mode 33
--- Blue foreground color
blue :: String -> String
blue = mode 34
--- Magenta foreground color
magenta :: String -> String
magenta = mode 35
--- Cyan foreground color
cyan :: String -> String
cyan = mode 36
--- White foreground color
white :: String -> String
white = mode 37
--- Default foreground color
fgDefault :: String -> String
fgDefault = mode 39
-- -----------------------------------------------------------------------------
-- Background color
-- -----------------------------------------------------------------------------
--- Black background color
bgBlack :: String -> String
bgBlack = mode 40
--- Red background color
bgRed :: String -> String
bgRed = mode 41
--- Green background color
bgGreen :: String -> String
bgGreen = mode 42
--- Yellow background color
bgYellow :: String -> String
bgYellow = mode 43
--- Blue background color
bgBlue :: String -> String
bgBlue = mode 44
--- Magenta background color
bgMagenta :: String -> String
bgMagenta = mode 45
--- Cyan background color
bgCyan :: String -> String
bgCyan = mode 46
--- White background color
bgWhite :: String -> String
bgWhite = mode 47
--- Default background color
bgDefault :: String -> String
bgDefault = mode 49
-- -----------------------------------------------------------------------------
-- Helper functions
-- -----------------------------------------------------------------------------
--- Cursor movements
moveCursor :: String -> Int -> String
moveCursor s n = cmd (show n ++ s)
--- Text mode
mode :: Int -> String -> String
mode n s = cmd (show n ++ "m") ++ s ++ if end `isSuffixOf` s then "" else end
where end = cmd "0m"
--- Create a command using the CSI (control sequence introducer) "\ESC["
cmd :: String -> String
cmd s = '\ESC' : '[' : s
------------------------------------------------------------------------------
--- An implementation of double-ended queues supporting access at both
--- ends in constant amortized time.
---
--- @author Bernd Brassel, Olaf Chitil, Michael Hanus, Sebastian Fischer,
--- Bjoern Peemoeller
--- @version January 2015
--- @category algorithm
------------------------------------------------------------------------------
module Dequeue
( -- Abstract data type, constructors and queries
Queue, empty, cons, snoc, isEmpty, deqLength
-- Selectors
, deqHead, deqTail, deqLast, deqInit, deqReverse, rotate, matchHead, matchLast
-- conversion from and to lists
, listToDeq, deqToList
) where
--- The datatype of a queue.
data Queue a = S Int [a] Int [a]
--- The empty queue.
empty :: Queue _
empty = S 0 [] 0 []
--- Inserts an element at the front of the queue.
cons :: a -> Queue a -> Queue a
cons x (S lenf f lenr r) = check (lenf + 1) (x : f) lenr r
--- Inserts an element at the end of the queue.
snoc :: a -> Queue a -> Queue a
snoc x (S lenf f lenr r) = deqReverse (check (lenr + 1) (x : r) lenf f)
--- Is the queue empty?
isEmpty :: Queue _ -> Bool
isEmpty (S lenf _ lenr _) = lenf + lenr == 0
--- Returns the number of elements in the queue.
deqLength :: Queue _ -> Int
deqLength (S lenf _ lenr _) = lenf + lenr
--- The first element of the queue.
deqHead :: Queue a -> a
deqHead (S lenf f _ r) = head (if lenf == 0 then r else f)
--- Removes an element at the front of the queue.
deqTail :: Queue a -> Queue a
deqTail (S _ [] _ _) = empty
deqTail (S lenf (_:fs) lenr r) = deqReverse (check lenr r (lenf - 1) fs)
--- The last element of the queue.
deqLast :: Queue a -> a
deqLast (S _ f lenr r) = head (if lenr == 0 then f else r)
--- Removes an element at the end of the queue.
deqInit :: Queue a -> Queue a
deqInit (S _ _ _ [] ) = empty
deqInit (S lenf f lenr (_:rs)) = check lenf f (lenr - 1) rs
--- Reverses a double ended queue.
deqReverse :: Queue a -> Queue a
deqReverse (S lenf f lenr r) = S lenr r lenf f
--- Moves the first element to the end of the queue.
rotate :: Queue a -> Queue a
rotate q = snoc (deqHead q) (deqTail q)
--- Matches the front of a queue.
--- `matchHead q` is equivalent to
--- `if isEmpty q then Nothing else Just (deqHead q, deqTail q)`
--- but more efficient.
matchHead :: Queue a -> Maybe (a, Queue a)
matchHead (S _ [] _ [] ) = Nothing
matchHead (S _ [] _ [x] ) = Just (x, empty)
matchHead (S _ [] _ (_:_:_))
= error $ "Dequeue.matchHead: illegal queue"
matchHead (S lenf (x:xs) lenr r )
= Just (x, deqReverse (check lenr r (lenf - 1) xs))
--- Matches the end of a queue.
--- `matchLast q` is equivalent to
--- `if isEmpty q then Nothing else Just (deqLast q,deqInit q)`
--- but more efficient.
matchLast :: Queue a -> Maybe (a,Queue a)
matchLast (S _ [] _ [] ) = Nothing
matchLast (S _ [x] _ [] ) = Just (x, empty)
matchLast (S _ (_:_:_) _ [] )
= error $ "Dequeue.matchLast: illegal queue"
matchLast (S lenf f lenr (x:xs)) = Just (x, check lenf f (lenr - 1) xs)
--- Transforms a list to a double ended queue.
listToDeq :: [a] -> Queue a
listToDeq xs = check (length xs) xs 0 []
--- Transforms a double ended queue to a list.
deqToList :: Queue a -> [a]
deqToList (S _ xs _ ys) = xs ++ reverse ys
--- Check for invariant: The length of the first list is smaller than
--- three times the length of the second plus 1.
check :: Int -> [a] -> Int -> [a] -> Queue a
check lenf f lenr r
| lenf <= 3 * lenr + 1 = S lenf f lenr r
| otherwise = S lenf' f' lenr' r'
where
len = lenf + lenr
lenf' = len `div` 2
lenr' = len - lenf'
(f', rf') = splitAt lenf' f
r' = r ++ reverse rf'
......@@ -16,7 +16,7 @@ module Distribution
) where
import Directory ( getHomeDirectory )
import FilePath ( (</>) )
import FilePath ( FilePath, (</>) )
-----------------------------------------------------------------
-- Compiler and run-time environment name and version
......
---------------------------------------------------------------------------
--- Library with an implementation of red-black trees:
--- <P>
--- Serves as the base for both TableRBT and SetRBT
--- All the operations on trees are generic, i.e., one has to provide
--- two explicit order predicates ("<CODE>lessThan</CODE>" and "<CODE>eq</CODE>"below)
--- on elements.
---
--- @author Johannes Koj, Michael Hanus, Bernd Brassel
--- @version March 2005
--- @category algorithm
----------------------------------------------------------------------------
module RedBlackTree
( RedBlackTree, empty, isEmpty, lookup, update
, tree2list, sortBy, newTreeLike, setInsertEquivalence, delete
) where
----------------------------------------------------------------------------
-- the main interface:
--- A red-black tree consists of a tree structure and three order predicates.
--- These predicates generalize the red black tree. They define
--- 1) equality when inserting into the tree<br>
--- eg for a set eqInsert is (==),
--- for a multiset it is (\ _ _ -> False)
--- for a lookUp-table it is ((==) . fst)
--- 2) equality for looking up values
--- eg for a set eqLookUp is (==),
--- for a multiset it is (==)
--- for a lookUp-table it is ((==) . fst)
--- 3) the (less than) relation for the binary search tree
data RedBlackTree a
= RedBlackTree
(a -> a -> Bool) -- equality for insertion
(a -> a -> Bool) -- equality for lookup
(a -> a -> Bool) -- lessThan for search
(Tree a) -- contents
--- The three relations are inserted into the structure by function empty.
--- Returns an empty tree, i.e., an empty red-black tree
--- augmented with the order predicates.
empty :: (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool)
-> RedBlackTree a
empty eqInsert eqLookUp lessThan = RedBlackTree eqInsert eqLookUp lessThan Empty
--- Test on emptyness
isEmpty :: RedBlackTree _ -> Bool
isEmpty (RedBlackTree _ _ _ Empty) = True
isEmpty (RedBlackTree _ _ _ (Tree _ _ _ _)) = False
--- Creates a new empty red black tree from with the same ordering as a give one.
newTreeLike :: RedBlackTree a -> RedBlackTree a
newTreeLike (RedBlackTree eqIns eqLk lt _) = RedBlackTree eqIns eqLk lt Empty
--- Returns an element if it is contained in a red-black tree.
--- @param p - a pattern for an element to look up in the tree
--- @param t - a red-black tree
--- @return the contained True if p matches in t
lookup :: a -> RedBlackTree a -> Maybe a
lookup p (RedBlackTree _ eqLk lt t) = lookupTree eqLk lt p t
lookupTree :: (a -> a -> Bool) -> (a -> a -> Bool) -> a -> Tree a -> Maybe a
lookupTree _ _ _ Empty = Nothing
lookupTree eq lt p (Tree _ e l r)
| eq p e = Just e
| lt p e = lookupTree eq lt p l
| otherwise = lookupTree eq lt p r
--- Updates/inserts an element into a RedBlackTree.
update :: a -> RedBlackTree a -> RedBlackTree a
update e (RedBlackTree eqIns eqLk lt t) =
RedBlackTree eqIns eqLk lt (updateTree eqIns lt e t)
updateTree :: (a -> a -> Bool) -> (a -> a -> Bool) -> a -> Tree a -> Tree a
updateTree eq lt e t = let (Tree _ e2 l r) = upd t
in Tree Black e2 l r
where
upd Empty = Tree Red e Empty Empty
upd (Tree c e2 l r) | eq e e2 = Tree c e l r
| lt e e2 = balanceL (Tree c e2 (upd l) r)
| otherwise = balanceR (Tree c e2 l (upd r))
--- Deletes entry from red black tree.
delete :: a -> RedBlackTree a -> RedBlackTree a
delete e (RedBlackTree eqIns eqLk lt t) =
RedBlackTree eqIns eqLk lt (blackenRoot (deleteTree eqLk lt e t))
where
blackenRoot Empty = Empty
blackenRoot (Tree _ x l r) = Tree Black x l r
deleteTree :: (a -> a -> Prelude.Bool)
-> (a -> a -> Prelude.Bool) -> a -> Tree a -> Tree a
deleteTree _ _ _ Empty = Empty -- no error for non existence
deleteTree eq lt e (Tree c e2 l r)
| eq e e2 = if isEmptyTree l then addColor c r else
if isEmptyTree r
then addColor c l
else let el = rightMost l
in delBalanceL (Tree c el (deleteTree eq lt el l) r)
| lt e e2 = delBalanceL (Tree c e2 (deleteTree eq lt e l) r)
| otherwise = delBalanceR (Tree c e2 l (deleteTree eq lt e r))
where
addColor DoublyBlack tree = tree -- should not occur
addColor Red tree = tree
addColor Black Empty = Empty
addColor Black (Tree Red x lx rx) = Tree Black x lx rx
addColor Black (Tree Black x lx rx) = Tree DoublyBlack x lx rx
addColor Black (Tree DoublyBlack x lx rx) = Tree DoublyBlack x lx rx
rightMost Empty = error "RedBlackTree.rightMost"
rightMost (Tree _ x _ rx) = if isEmptyTree rx then x else rightMost rx
--- Transforms a red-black tree into an ordered list of its elements.
tree2list :: RedBlackTree a -> [a]
tree2list (RedBlackTree _ _ _ t) = tree2listTree t
tree2listTree :: Tree a -> [a]
tree2listTree tree = t2l tree []
where
t2l Empty es = es
t2l (Tree _ e l r) es = t2l l (e : t2l r es)
--- Generic sort based on insertion into red-black trees.
--- The first argument is the order for the elements.
sortBy :: Eq a => (a -> a -> Bool) -> [a] -> [a]
sortBy cmp xs = tree2list (foldr update (empty (\_ _->False) (==) cmp) xs)
--- For compatibility with old version only
setInsertEquivalence :: (a -> a -> Bool) -> RedBlackTree a -> RedBlackTree a
setInsertEquivalence eqIns (RedBlackTree _ eqLk lt t) = RedBlackTree eqIns eqLk lt t
----------------------------------------------------------------------------
-- implementation of red-black trees:
rbt :: RedBlackTree a -> Tree a
rbt (RedBlackTree _ _ _ t) = t
--- The colors of a node in a red-black tree.
data Color = Red | Black | DoublyBlack
deriving Eq
--- The structure of red-black trees.
data Tree a = Tree Color a (Tree a) (Tree a)
| Empty
isEmptyTree :: Tree _ -> Bool
isEmptyTree Empty = True
isEmptyTree (Tree _ _ _ _) = False
isBlack :: Tree _ -> Bool
isBlack Empty = True
isBlack (Tree c _ _ _) = c == Black
isRed :: Tree _ -> Bool
isRed Empty = False
isRed (Tree c _ _ _) = c == Red
isDoublyBlack :: Tree _ -> Bool
isDoublyBlack Empty = True
isDoublyBlack (Tree c _ _ _) = c == DoublyBlack
left :: Tree a -> Tree a
left Empty = error "RedBlackTree.left"
left (Tree _ _ l _) = l
right :: Tree a -> Tree a
right Empty = error "RedBlackTree.right"
right (Tree _ _ _ r) = r
singleBlack :: Tree a -> Tree a
singleBlack Empty = Empty
singleBlack (Tree Red x l r) = Tree Red x l r
singleBlack (Tree Black x l r) = Tree Black x l r
singleBlack (Tree DoublyBlack x l r) = Tree Black x l r
--- for the implementation of balanceL and balanceR refer to picture 3.5, page 27,
--- Okasaki "Purely Functional Data Structures"
balanceL :: Tree a -> Tree a
balanceL tree
| isRed leftTree && isRed (left leftTree)
= let Tree _ z (Tree _ y (Tree _ x a b) c) d = tree
in Tree Red y (Tree Black x a b) (Tree Black z c d)
| isRed leftTree && isRed (right leftTree)
= let Tree _ z (Tree _ x a (Tree _ y b c)) d = tree
in Tree Red y (Tree Black x a b) (Tree Black z c d)
| otherwise = tree
where
leftTree = left tree
balanceR :: Tree a -> Tree a
balanceR tree
| isRed rightTree && isRed (right rightTree)
= let Tree _ x a (Tree _ y b (Tree _ z c d)) = tree
in Tree Red y (Tree Black x a b) (Tree Black z c d)
| isRed rightTree && isRed (left rightTree)
= let Tree _ x a (Tree _ z (Tree _ y b c) d) = tree
in Tree Red y (Tree Black x a b) (Tree Black z c d)
| otherwise = tree
where
rightTree = right tree
--- balancing after deletion
delBalanceL :: Tree a -> Tree a
delBalanceL tree = if isDoublyBlack (left tree) then reviseLeft tree else tree
reviseLeft :: Tree a -> Tree a
reviseLeft tree
| isEmptyTree r = tree
| blackr && isRed (left r)
= let Tree col x a (Tree _ z (Tree _ y b c) d) = tree
in Tree col y (Tree Black x (singleBlack a) b) (Tree Black z c d)
| blackr && isRed (right r)
= let Tree col x a (Tree _ y b (Tree _ z c d)) = tree
in Tree col y (Tree Black x (singleBlack a) b) (Tree Black z c d)
| blackr
= let Tree col x a (Tree _ y b c) = tree
in Tree (if col==Red then Black else DoublyBlack) x (singleBlack a)
(Tree Red y b c)
| otherwise
= let Tree _ x a (Tree _ y b c) = tree
in Tree Black y (reviseLeft (Tree Red x a b)) c
where
r = right tree
blackr = isBlack r
delBalanceR :: Tree a -> Tree a
delBalanceR tree = if isDoublyBlack (right tree) then reviseRight tree
else tree
reviseRight :: Tree a -> Tree a
reviseRight tree
| isEmptyTree l = tree
| blackl && isRed (left l)
= let Tree col x (Tree _ y (Tree _ z d c) b) a = tree
in Tree col y (Tree Black z d c) (Tree Black x b (singleBlack a))
| blackl && isRed (right l)
= let Tree col x (Tree _ z d (Tree _ y c b)) a = tree
in Tree col y (Tree Black z d c) (Tree Black x b (singleBlack a))
| blackl
= let Tree col x (Tree _ y c b) a = tree
in Tree (if col==Red then Black
else DoublyBlack) x (Tree Red y c b) (singleBlack a)
| otherwise
= let Tree _ x (Tree _ y c b) a = tree
in Tree Black y c (reviseRight (Tree Red x b a))
where
l = left tree
blackl = isBlack l
----------------------------------------------------------------------------
--- Library with an implementation of sets as red-black trees.
---
--- All the operations on sets are generic, i.e., one has to provide
--- an explicit order predicate `(<)` (less-than) on elements.
---
--- @author Johannes Koj, Michael Hanus, Bernd Brassel
--- @version March 2013
--- @category algorithm
----------------------------------------------------------------------------
module SetRBT where
import qualified RedBlackTree as RBT
import Maybe (isJust)
type SetRBT a = RBT.RedBlackTree a
--- Returns an empty set, i.e., an empty red-black tree
--- augmented with an order predicate.
emptySetRBT :: Eq a => (a -> a -> Bool) -> SetRBT a
emptySetRBT = RBT.empty (==) (==)