
  0 | module BankersDeque
  1 | 
  2 | import Data.List
  3 | 
  4 | import Deque
  5 | 
  6 | %default total
  7 | 
  8 | export
  9 | data BankersDeque a = BD Int (List a) Int (List a)
 10 | 
 11 | c : Int
 12 | c = 3
 13 | 
 14 | check : Int -> List a -> Int -> List a -> BankersDeque a
 15 | check lenf f lenr r =
 16 |   if lenf > c * lenr + 1 then
 17 |      let i = (lenf + lenr) `div` 2
 18 |          j = lenf + lenr - i
 19 |          f' = take (cast i) f
 20 |          r' = r ++ reverse (drop (cast i) f)
 21 |      in BD i f' j r'
 22 |   else if lenr > c * lenf + 1 then
 23 |     let j = (lenf + lenr) `div` 2
 24 |         i = lenf + lenr - j
 25 |         r' = take (cast j) r
 26 |         f' = f ++ reverse (drop (cast j) r)
 27 |     in BD i f' j r'
 28 |   else BD lenf f lenr r
 29 | 
 30 | export
 31 | partial
 32 | Deque BankersDeque where
 33 |   empty = BD 0 [] 0 []
 34 |   isEmpty (BD lenf f lenr r) = lenf + lenr == 0
 35 | 
 36 |   cons x (BD lenf f lenr r) = check (lenf + 1) (x :: f) lenr r
 37 | 
 38 |   head (BD lenf []        lenr [x]) = x -- Missing in Haskell original
 39 |   head (BD lenf []        lenr r)   = idris_crash "empty deque"
 40 |   head (BD lenf (x :: f') lenr r)   = x
 41 | 
 42 |   tail (BD lenf []        lenr [x]) = empty -- Missing in Haskell original
 43 |   tail (BD lenf []        lenr r)   = idris_crash "empty deque"
 44 |   tail (BD lenf (x :: f') lenr r)   = check (lenf - 1) f' lenr r
 45 | 
 46 |   snoc (BD lenf f lenr r) x = check lenf f (lenr + 1) (x :: r)
 47 | 
 48 |   last (BD lenf [x] lenr [])        = x -- Missing in Haskell original
 49 |   last (BD lenf f   lenr [])        = idris_crash "empty deque"
 50 |   last (BD lenf f   lenr (x :: r')) = x
 51 | 
 52 |   init (BD lenf [x] lenr [])        = empty -- Missing in Haskell original
 53 |   init (BD lenf f   lenr [])        = idris_crash "empty deque"
 54 |   init (BD lenf f   lenr (x :: r')) = check lenf f (lenr - 1) r'
 55 |