Mercurial > 12ws.info2
view exercises/src/SetPairList.hs @ 26:ce9610f08925
Merge
author | Markus Kaiser <markus.kaiser@in.tum.de> |
---|---|
date | Wed, 09 Jan 2013 19:45:47 +0100 |
parents | 34fea195e238 ea3fba2381bc |
children |
line wrap: on
line source
module SetPairList(Set, empty, insert, isin, size, union, delete) where -- Abstraction function {- alpha :: Set a -> {a} alpha (S []) = {} alpha (S ((a, b):xs)) = {a..b} union (alpha xs) To show: (10 things) alpha empty = {} invar s ==> alpha (insert x s) = {x} union alpha s invar s ==> alpha (delete x s) = alpha s \ {x} invar s ==> isin x s = x \in alpha s invar s ==> size s = |alpha s| invar s1, invar s2 ==> alpha (union s1 s2) = (alpha s1) union (alpha s2) invar empty invar s ==> invar (insert x s) invar s ==> invar(delete x s) invar s1, invar s2 ==> invar (union s1 s2) -} -- Interface newtype Set a = S (PairList a) invar :: Integral a => Set a -> Bool invar (S s) = invarPL s empty :: Set a empty = S emptyPL insert :: Integral a => a -> Set a -> Set a insert n (S s) = S (insertPL n s) isin :: Integral a => a -> Set a -> Bool isin n (S s) = isinPL n s size :: Integral a => Set a -> Integer size (S s) = sizePL s union :: Integral a => Set a -> Set a -> Set a union (S s1) (S s2) = S (unionPL s1 s2) delete :: Integral a => a -> Set a -> Set a delete n (S s) = S (deletePL n s) -- Implementation type PairList a = [(a, a)] invarPL :: Integral a => PairList a -> Bool invarPL [] = True invarPL [(m,n)] = m <= n invarPL ((m1,n1):(m2,n2):ms) = m1 <= n1 && n1 + 1 < m2 && invarPL ((m2,n2):ms) emptyPL :: PairList a emptyPL = [] insertPL :: Integral a => a -> PairList a -> PairList a insertPL n [] = [(n,n)] insertPL n ((k1,l1) : (k2,l2) : ks) | l1 + 1 == n && n + 1 == k2 = (k1,l2) : ks insertPL n ((k,l) : ks) | n + 1 == k = (n,l) : ks | n < k = (n,n) : (k,l) : ks | k <= n && n <= l = (k,l) : ks | l + 1 == n = (k,n) : ks | otherwise = (k,l) : insertPL n ks isinPL :: Ord a => a -> PairList a -> Bool isinPL n = any (\(k,l) -> k <= n && n <= l) sizePL :: Integral a => PairList a -> Integer sizePL [] = 0 sizePL ((k,l) : s) = toInteger (l - k + 1) + sizePL s unionPL :: Integral a => PairList a -> PairList a -> PairList a unionPL [] ls = ls unionPL ks [] = ks unionPL ((k1,l1):ks) ((k2,l2):ls) = if k1 <= k2 then if l1 + 1 < k2 then (k1,l1) : unionPL ks ((k2, l2):ls) else if l1 <= l2 then unionPL ks ((k1,l2):ls) else {- l1 > l2 -} unionPL ((k1,l1):ks) ls else if k1 <= l2 + 1 then if l1 <= l2 then unionPL ks ((k2,l2):ls) else {- l1 > l2 -} unionPL ((k2,l1):ks) ls else (k2,l2) : unionPL ((k1,l1):ks) ls deletePL :: Integral a => a -> PairList a -> PairList a deletePL n [] = [] deletePL n ((k,l) : ks) | n < k = (k,l) : ks | n == k = if k < l then (k+1,l) : ks else ks | k < n && n < l = (k,n-1) : (n+1,l) : ks | n == l = if k < l then (k,l-1) : ks else ks | otherwise = (k,l) : deletePL n ks