{-@ LIQUID "--no-termination" @-}
{-@ LIQUID "--maxparams=3"    @-}

module LazyQueue where

-- Source: Okasaki, JFP 1995
-- http://www.westpoint.edu/eecs/SiteAssets/SitePages/Faculty%20Publication%20Documents/Okasaki/jfp95queue.pdf

--------------------------------------------------------------------------------
-- | Sized Lists
--------------------------------------------------------------------------------

data SList a = SL { size  :: Int
                  , elems :: [a]
                  }

{-@ type SListN a N = {v:SList a | size v = N} @-}

-- | Invariant: `size` is really the size:

{-@ data SList a = SL { size  :: Nat
                      , elems :: {v:[a] | len v = size}
                      }
  @-}

-- | Size function actually returns the size: (Duh!)

{-@ size :: q:SList a -> {v:Nat | v = size q} @-}

-- | Non-Empty Lists:

{-@ type NEList a = {v:SList a | size v > 0} @-}


{-@ nil          :: SListN a 0  @-}
nil              = SL 0 []

{-@ cons         :: a -> xs:SList a -> SListN a {size xs + 1}   @-}
cons x (SL n xs) = SL (n+1) (x:xs)

{-@ tl           :: xs:NEList a -> SListN a {size xs - 1}  @-}
tl (SL n (_:xs)) = SL (n-1) xs
tl _             = die "never"

{-@ hd           :: xs:NEList a -> a @-}
hd (SL _ (x:_))  = x 
hd _             = die "never"


--------------------------------------------------------------------------------
-- | Sized Lists
--------------------------------------------------------------------------------

data Queue a = Q  { left   :: SList a
                  , right  :: SList a
                  }

-- | Invariant: `|right|` <= `|left|`

{-@ data Queue a = Q { left  :: SList a 
                     , right :: {v:SList a | size v <= size left}
                     }
  @-}



emp = Q nil nil

qsize         :: Queue a -> Int
qsize (Q l r) = size l + size r

insert e (Q l r) = makeq l (e `cons` r)

{-@ makeq :: l:_ -> r:{ _ | size r <= size l + 1} -> _  @-}
makeq l r
  | size r <= size l = Q l r
  | otherwise        = Q (rot l r nil) nil

{-@ rot :: l:_ -> r:SListN _ {1 + size l} -> a:_ -> {v:_ | size v = size l + size r + size a} @-}
rot l r a
  | size l == 0      = (hd r) `cons` a
  | otherwise        = (hd l) `cons` (rot (tl l) (tl r) ((hd r) `cons` a))

{-@ die :: {v:_ | false} -> a @-}
die x = error x