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