# HG changeset patch
# User Markus Kaiser <markus.kaiser@in.tum.de>
# Date 1355955762 -3600
# Node ID f9386825bf71096ff8ab8d0c924ac2cec24c5cc7
# Parent  498aea38199b5feead88c96a822423295f97d7fa
week 10

diff -r 498aea38199b -r f9386825bf71 blatt10.pdf
Binary file blatt10.pdf has changed
diff -r 498aea38199b -r f9386825bf71 exercises/src/Exercise_10.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercises/src/Exercise_10.hs	Wed Dec 19 23:22:42 2012 +0100
@@ -0,0 +1,106 @@
+module Exercise_10 (module Join, module SafeMap) where
+
+{- Library DO NOT CHANGE -}
+import SafeMap (SafeMap, empty, update, lookup)
+import Join (Field, doJoin, doJoinFormat, parseFormat)
+{- End Library -}
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe G10.1 -}
+
+{-
+\alpha ist wie in den Folien definiert.
+
+
+Simulationseigenschaften:
+
+R_empty: \alpha empty = {}
+       : a      empty = {}
+
+
+R_insert: \alpha (insert x xs) = {x} \union \alpha xs
+        : a      (insert x xs) = {x}  union a      xs
+
+
+R_isin: isin x xs = x \in \alpha xs
+      : isin x xs = x  in a      xs
+
+
+R_size: size xs = |\alpha xs|
+      : size xs = |a      xs|
+
+
+
+Hilfslemmata:
+
+L_elem(xs): elem x xs = x in a xs
+Proof by structural induction on xs
+
+Base case: L_elem([])
+To show:
+
+Induction step: L_elem(ys) => Lemma(y : ys)
+IH:
+To show:
+
+
+L_length(xs): length (nub xs) = |a xs| 
+Proof by structural induction on xs
+
+Base case: L_elem([])
+To show:
+
+Induction step: L_elem(ys) => Lemma(y : ys)
+IH:
+To show:
+
+-}
+
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe G10.2 -}
+
+{- siehe SetPairList.hs -}
+
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe G10.3 -}
+
+{- siehe Queue.hs und SuperQueue.hs -}
+
+{-
+Definition von \alpha:
+
+        \alpha (Queue front kcab) = undefined
+
+
+Simulationseigenschaften: (5)
+
+
+
+Beweise:
+-}
+
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe H10.1 -}
+
+{- siehe SafeMap.hs -}
+
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe H10.2 -}
+
+{- siehe Join.hs -}
+
+
+
+{---------------------------------------------------------------------}
+{- Aufgabe H10.3 -}
+
+{- siehe Morsi.hs -}
\ No newline at end of file
diff -r 498aea38199b -r f9386825bf71 exercises/src/Join.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercises/src/Join.hs	Wed Dec 19 23:22:42 2012 +0100
@@ -0,0 +1,40 @@
+module Join where
+
+import Control.Monad
+import Data.List
+import System.Environment (getArgs)
+
+{-- nicht veraendern --}
+
+data Field = A Int | B Int
+
+readInt :: String -> Maybe Int
+readInt s =  case [x | (x,t) <- reads s, ("","") <- lex t] of
+               [x] -> Just x
+               _   -> Nothing
+
+{-- H10.2 --}
+
+doJoin :: [String] -> [String] -> [String]
+doJoin = undefined
+
+doJoinFormat :: [Field] -> [String] -> [String] -> [String]
+doJoinFormat = undefined
+
+parseFormat :: String -> Maybe [Field]
+parseFormat = undefined
+
+{-- Vorbereitetes Gerüst --}
+
+readLines :: String -> IO [String]
+readLines path = liftM lines $ readFile path
+
+main :: IO ()
+main = do
+    args <- getArgs
+    case args of
+      ["-f", fmtStr, file1, file2] | Just fmt <- parseFormat fmtStr ->
+        mapM_ putStrLn =<< liftM2 (doJoinFormat fmt) (readLines file1) (readLines file2)
+      [file1, file2] ->
+        mapM_ putStrLn =<< liftM2 doJoin (readLines file1) (readLines file2)
+      _ -> putStrLn "Syntax: Join [-f format] file1 file2"
diff -r 498aea38199b -r f9386825bf71 exercises/src/Queue.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercises/src/Queue.hs	Wed Dec 19 23:22:42 2012 +0100
@@ -0,0 +1,44 @@
+module Queue where
+import Test.QuickCheck
+import Test.QuickCheck.Poly (A)
+
+newtype Queue a = Queue [a]
+  deriving (Eq, Show)
+
+empty :: Queue a
+empty = undefined
+
+isEmpty :: Queue a -> Bool
+isEmpty (Queue xs) = undefined
+
+enqueue :: a -> Queue a -> Queue a
+enqueue x (Queue xs) = undefined
+
+dequeue :: Queue a -> (a, Queue a)
+dequeue (Queue (x : xs)) = undefined
+
+toList :: Queue a -> [a]
+toList (Queue xs) = undefined
+
+
+{- QuickCheck Tests -}
+
+instance Arbitrary a => Arbitrary (Queue a) where
+  arbitrary =
+    do
+      xs <- arbitrary
+      return $ Queue xs
+
+prop_isEmpty_empty = isEmpty empty
+
+prop_isEmpty_enqueue x q = not (isEmpty (enqueue (x :: A) q))
+
+prop_toList_enqueue x q = toList (enqueue x q) == toList q ++ [x :: A]
+
+prop_toList_dequeue x q =
+  not (isEmpty q) ==> (x :: A) : toList q' == toList q
+  where (x, q') = dequeue q
+
+prop_toList_ext q q' =
+  toList q == toList q' ==> (q :: Queue A) == q'
+
diff -r 498aea38199b -r f9386825bf71 exercises/src/SafeMap.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercises/src/SafeMap.hs	Wed Dec 19 23:22:42 2012 +0100
@@ -0,0 +1,17 @@
+{- Modul-Deklaration anpassen, wenn notwendig! -}
+module SafeMap where
+
+{- Diese Definition ist nur da, damit die Vorlage unveraendert kompiliert.
+ - Fuer eine richtige Loesung auf jeden Fall diese Definition ersetzen.
+ - Achten Sie darauf, keine Implementierungsdetails nach aussen dringen
+ - zu lassen -}
+type SafeMap k v = ()
+
+empty :: Eq k => SafeMap k v
+empty = undefined
+
+update :: Eq k => k -> v -> SafeMap k v -> SafeMap k v
+update = undefined
+
+lookup :: Eq k => k -> SafeMap k v -> Maybe v
+lookup = undefined
diff -r 498aea38199b -r f9386825bf71 exercises/src/SetPairList.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercises/src/SetPairList.hs	Wed Dec 19 23:22:42 2012 +0100
@@ -0,0 +1,85 @@
+module SetPairList where
+
+-- Abstraction function
+{-
+    alpha (S x) = undefined
+
+    To show: (10 things)
+-}
+
+-- Interface
+newtype Set a = S (...)
+
+invar :: Integral a => Set a -> Bool
+invar (S s) = undefined
+
+empty :: Set a
+empty = undefined
+
+insert :: Integral a => a -> Set a -> Set a
+insert n (S s) = undefined
+
+isin :: Integral a => a -> Set a -> Bool
+isin n (S s) = undefined
+
+size :: Integral a => Set a -> Integer
+size (S s) = undefined
+
+union :: Integral a => Set a -> Set a -> Set a
+union (S s1) (S s2) = undefined
+
+delete :: Integral a => a -> Set a -> Set a
+delete n (S s) = undefined
+
+-- 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
+
diff -r 498aea38199b -r f9386825bf71 exercises/src/SuperQueue.hs
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/exercises/src/SuperQueue.hs	Wed Dec 19 23:22:42 2012 +0100
@@ -0,0 +1,50 @@
+module SuperQueue where
+import Test.QuickCheck
+import Test.QuickCheck.Poly (A)
+
+data Queue a = Queue [a] [a]
+
+empty :: Queue a
+empty = undefined
+
+isEmpty :: Queue a -> Bool
+isEmpty (Queue front kcab) = undefined
+
+enqueue :: a -> Queue a -> Queue a
+enqueue x (Queue front kcab) = undefined
+
+dequeue :: Queue a -> (a, Queue a)
+dequeue (Queue front kcab) = undefined
+
+toList :: Queue a -> [a]
+toList (Queue front kcab) = undefined
+
+instance Eq a => Eq (Queue a) where
+  q == q' = undefined
+
+instance Show a => Show (Queue a) where
+  show = undefined
+
+
+{- QuickCheck Tests -}
+
+instance Arbitrary a => Arbitrary (Queue a) where
+  arbitrary =
+    do
+      front <- arbitrary
+      kcab <- arbitrary
+      return $ Queue front kcab
+
+prop_isEmpty_empty = isEmpty empty
+
+prop_isEmpty_enqueue x q = not (isEmpty (enqueue (x :: A) q))
+
+prop_toList_enqueue x q = toList (enqueue x q) == toList q ++ [x :: A]
+
+prop_toList_dequeue x q =
+  not (isEmpty q) ==> (x :: A) : toList q' == toList q
+  where (x, q') = dequeue q
+
+prop_toList_ext q q' =
+  toList q == toList q' ==> (q :: Queue A) == q'
+