2 posts from January 2009

<pre> search3 :: !Bool !(u:a -> .(v:([u:a] -> w:[.b]) -> x:[.b])) u:a -> y:[.b], [v <= u,x v <= w,x v <= y] search3 kind explorer root | kind = do_all_depth [root] [] = do_all_breadth [root] [] where do_all_depth [] t = t do_all_depth [v:vs] t = explorer v \ vs` = do_all_depth vs` (do_all_depth vs t) do_all_breadth [] t = t do_all_breadth [v:vs] t = explorer v \ vs` = do_all_breadth vs (do_all_breadth vs` t) </pre>

<pre> :: Queue a = Queue !Int !.[a] !Int !.[.[a]] /* enqLen enqList deqLen deqList */ adjust :: !u:(Queue .a) -> v:(Queue .a), [u <= v] adjust q=:(Queue enqLen enqList deqLen deqList) | enqLen > 3 && enqLen >= deqLen = Queue 0 [] (enqLen + deqLen) (deqList ++ [reverse enqList]) | otherwise = q enq :: .a !u:(Queue .a) -> v:(Queue .a), [u <= v] enq a (Queue enqLen enqList deqLen deqList) = adjust (Queue (enqLen + 1) [a:enqList] deqLen deqList) deq :: !u:(Queue .a) -> (.a, !v:(Queue .a)), [u <= v] deq (Queue enqLen enqList deqLen [[]:deqList]) = deq (Queue enqLen enqList deqLen deqList) deq (Queue enqLen enqList deqLen [[a:as]:deqList]) = (a, adjust (Queue enqLen enqList (deqLen - 1) [as:deqList])) deq (Queue enqLen enqList 0 deqList) = deq (Queue 0 [] enqLen [reverse enqList]) newq :: .(Queue .a) newq = Queue 0 [] 0 [] emptyq :: !.(Queue .a) -> .Bool emptyq (Queue 0 _ 0 _) = True emptyq _ = False </pre>