0 | module HoodMelvilleQueue
6 | data RotationState a =
8 | | Reversing Int (List a) (List a) (List a) (List a)
9 | | Appending Int (List a) (List a)
13 | data HoodMelvilleQueue a = HM Int (List a) (RotationState a) Int (List a)
15 | exec : RotationState a -> RotationState a
16 | exec (Reversing ok (x :: f) f' (y :: r) r') = Reversing (ok + 1) f (x :: f') r (y :: r')
17 | exec (Reversing ok [] f' [y] r') = Appending ok f' (y :: r')
18 | exec (Appending 0 f' r') = Done r'
19 | exec (Appending ok (x :: f') r') = Appending (ok - 1) f' (x :: r')
22 | invalidate : RotationState a -> RotationState a
23 | invalidate (Reversing ok f f' r r') = Reversing (ok - 1) f f' r r'
24 | invalidate (Appending 0 f' (x :: r')) = Done r'
25 | invalidate (Appending ok f' r' ) = Appending (ok - 1) f' r'
26 | invalidate state = state
28 | exec2 : Int -> List a -> RotationState a -> Int -> List a -> HoodMelvilleQueue a
29 | exec2 lenf f state lenr r =
30 | case exec (exec state) of
31 | (Done newf) => HM lenf newf Idle lenr r
32 | newstate => HM lenf f newstate lenr r
34 | check : Int -> List a -> RotationState a -> Int -> List a -> HoodMelvilleQueue a
35 | check lenf f state lenr r =
36 | if lenr <= lenf then exec2 lenf f state lenr r
37 | else let newstate = Reversing 0 f [] r []
38 | in exec2 (lenf + lenr) f newstate 0 []
42 | Queue HoodMelvilleQueue where
43 | empty = HM 0 [] Idle 0 []
44 | isEmpty (HM lenf f state lenr r) = lenf == 0
46 | snoc (HM lenf f state lenr r) x = check lenf f state (lenr + 1) (x :: r)
48 | head (HM _ [] _ _ _) = idris_crash "empty queue"
49 | head (HM _ (x :: f') _ _ _) = x
51 | tail (HM lenf [] state lenr r) = idris_crash "empty queue"
52 | tail (HM lenf (x :: f') state lenr r) =
53 | check (lenf - 1) f' (invalidate state) lenr r