Queue in Idris

queue.idr

module queue
import Data.Vect

-- Here's the port of the Liquid Haskell blog post on amortized
-- queues. The tricksy bit is that the "amortized" bit depends on
-- laziness. This means that while in the REPL (where Idris is lazy)
-- this is reasonably efficient. It compiles absolutely horribly
-- though because each time push or pop something we rotate the whole
-- damned thing.

-- If nothing else, it's a nice example of carrying a proof around and
-- using it computationally.

abstract
data Queue : Type -> Type where
  mkQueue :  LTE bsize fsize
          -> (front : Vect fsize a)
          -> (back : Vect bsize a)
          -> Queue a

public
empty : Queue a
empty = mkQueue LTEZero [] []

reassocLemma : Vect ((l + r) + S k) a -> Vect ((l + S r) + k) a
reassocLemma = ?reassocLemmaProof

mkBQueue : LTE m (S n) -> Vect n a -> Vect m a -> Queue a
mkBQueue LTEZero xs [] = mkQueue LTEZero xs []
mkBQueue (LTESucc prf) xs (y :: ys) = mkQueue LTEZero (rot prf xs ys [y]) []
         where rot : LTE i j
                   -> Vect j a
                   -> Vect i a
                   -> Vect k a
                   -> Vect (i + j + k) a
               rot LTEZero xs [] zs = xs ++ zs
               rot (LTESucc prf) (x :: xs) (z :: ys) zs =
                 x :: reassocLemma (rot prf xs ys (z :: zs))

public
head : Queue a -> Maybe (a, Queue a)
head (mkQueue LTEZero [] []) = Nothing
head (mkQueue LTEZero (x :: xs) []) = Just (x, mkQueue LTEZero xs [])
head (mkQueue (LTESucc prf) (x :: xs) (y :: ys)) =
  Just (x, mkBQueue (LTESucc prf) xs (y :: ys))

public
push : a -> Queue a -> Queue a
push x (mkQueue prf front back) = mkBQueue (LTESucc prf) front (x :: back)

---------- Proofs ----------

queue.reassocLemmaProof = proof
  intros
  rewrite plusSuccRightSucc l r
  compute
  rewrite sym (plusSuccRightSucc (plus l r) k)
  trivial