Skip to content

Instantly share code, notes, and snippets.

@bananu7
Forked from jozefg/queue.idr
Last active August 29, 2015 14:14
Show Gist options
  • Save bananu7/a08ed48e57e5770006d4 to your computer and use it in GitHub Desktop.
Save bananu7/a08ed48e57e5770006d4 to your computer and use it in GitHub Desktop.
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment