Last active
August 29, 2015 14:14
-
-
Save jozefg/cb2d1280e06f26dbf2e9 to your computer and use it in GitHub Desktop.
Queue in Idris
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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