Evaluate iteratee: drop head

Let's perform the evaluation on head and drop.

drop :: Int -> IterV el ()
drop 0 = Done () Empty
drop n = Cont step
  where
    step (El _) = drop (n-1)
    step Empty = Cont step
    step EOF = Done () EOF

head :: IterV el (Maybe el)
head = Cont step
  where
    step (El el) = Done (Just el) Empty
    step Empty = Cont step
    step EOF = Done Nothing EOF

This is goal

*Main> run $ enum (drop 1 >> head) "abc"
Just (Just 'b')

The following steps are to generate the goal above.

run $ enum (drop 1 >> head) "abc"

run $ enum (drop 1 >>= (\x -> head)) "abc"

run $ enum (case (drop 1) of 
                       Done x e -> case ((\x -> head) x) of 
                            Done x' _ -> Done x' e
                            Cont k     -> k e
                       Cont k -> Cont (\str ->((k str) >>= (\x -> head)))
                    ) "abc"

-- Using drop rule. The step is bound to "drop 1"
run $ enum (case (Cont step) of 
                       Done x e -> case ((\x -> head) x) of 
                            Done x' _ -> Done x' e
                            Cont k     -> k e
                       Cont k -> Cont (\str ->((k str) >>= (\x -> head)))
                    ) "abc"

run $ enum (Cont (\e ->((step e) >>= (\x -> head)))
                    ) "abc"

-- enum feeds element to the iteratee, when it is Cont
run $ enum ((step (El 'a')) >>= (\x -> head)))
                    ) "bc"

-- As the step is from "drop 1", it is evaluated to "drop 1-1)"
run $ enum (drop (1-1) >>= (\x -> head)))
                    ) "bc"

run $ enum (drop 0 >>= (\x -> head)))
                    ) "bc"

run $ enum (Done () Empty >>= (\x -> head)))
                    ) "bc"

run $ enum (case ((\x -> head) () of 
                        Done x' _ -> Done x' Empty
                        Cont k     -> k Empty))
                    ) "bc"

run $ enum (case head of 
                        Done x' _ -> Done x' Empty
                        Cont k     -> k Empty))
                    ) "bc"

-- step is bound to head
run $ enum (case (Cont step) of 
                        Done x' _ -> Done x' Empty
                        Cont k     -> k Empty))
                    ) "bc"

run $ enum (step Empty) "bc"

-- This step is bound to head
run $ enum (Cont step) "bc"

run $ enum (Cont step) "bc"

run $ enum (step (El 'b')) "c"

-- Enum returns the iteratee if it is Done
run $ enum (Done (Just 'b') Empty) "c"

run $ (Done (Just 'b') Empty)

Just (Just 'b')