01.01.08

Exercise 11.1

Posted in Uncategorized at 12:35 pm by admin

1) Prove that (∀cs | cs is finite) putCharList cs = map putChar cs

where

 putCharList [] = [] putCharList (c:cs) = putChar c : putCharList cs   map f [] = [] map f (x:xs) = f x : map f xs

Base case:

 putCharList [] => [] => map putChar []

Inductive Step:

assume that purCharList cs = map putChar cs

then

 putCharList (c:cs) => putChar c : putCharList cs => putChar c : map putChar cs => map putChar (c:cs)

QED.

2) Prove that (∀xs | xs is finite) listProd xs = fold (*) 1 xs

where

 listProd [] = 1 listProd (x:xs) = x * listProd xs   fold op init [] = init fold op init (x:xs) = x `op` fold op init xs

Base case:

 listProd [] => 1 => fold (*) 1 []

Inductive Step:

assume that listProd xs = fold (*) 1 xs

then

 listProd (x:xs) => x * listProd xs => x * fold (*) 1 xs => fold (*) 1 (x:xs)

QED.

Exercise 10.4

Posted in Uncategorized at 12:18 am by admin

A quick look at Graphics.SOE reveals that getWindowEvent is the right function to trap mouse down, up, and move events separately.

 {- maybeClear is useful for avoiding flicker when not dragging objects. A real flicker-free solution should use double-buffering of course - this code still flickers terribly while dragging. -}   maybeClear :: Bool -> Window -> IO () maybeClear b w = if b then do clearWindow w else return ()   {- The program is in two halves: either we're waiting for a click (not dragging), or we're waiting for a release (dragging). Waiting for a click is almost identical to the previous definition of loop, except for the event function. -}   waitForClick :: Window -> [(Color, Region)] -> Bool -> IO () waitForClick w regs b = do maybeClear b w sequence_ [drawRegionInWindow w c r | (c,r) <- reverse regs] event <- getWindowEvent w case event of (Button (x,y) True True) -> let aux (_,r) = r `containsR` (pixelToInch (x - xWin2), pixelToInch (yWin2 - y)) in case (break aux regs) of (_, []) -> closeWindow w (top, hit:bot) -> waitForRelease (x,y) (x,y) w (hit : (top++bot)) True _ -> waitForClick w regs False   {- While dragging, we keep track of the initial click coordinates and translate the Region at the head of the list by the offset of the current mouse coordinates. When the mouse button is released, we go back to waiting for a click, leaving the head Region where it is. -}   waitForRelease :: Point -> Point -> Window -> [(Color, Region)] -> Bool -> IO () waitForRelease (origx, origy) (x,y) w regs b = do maybeClear b w sequence_ [drawRegionInWindow w c r | (c,r) <- reverse \$ tail regs] let (c,r) = head regs newHeadReg = (Translate (pixelToInch (x - origx), pixelToInch(origy - y)) r) drawRegionInWindow w c newHeadReg event <- getWindowEvent w case event of (Button (x,y) True False) -> waitForClick w ((c,newHeadReg) : (tail regs)) True (MouseMove pt) -> waitForRelease (origx,origy) pt w regs True _ -> waitForRelease (origx,origy) (x,y) w regs False   {- All that remains is to drive the drag and drop functionality with some boilerplate draw and main functions. -}   draw3 :: String -> Picture -> IO () draw3 s p = runGraphics \$ do w <- openWindow s (xWin, yWin) waitForClick w (pictToList p) True   main = draw3 "Drag and Drop" pic