content: {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--maxparams=3"    @-}
  
  module AmortizedQueue 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
  