[WIP] implement a PriorityQueue

base/PriorityQueue.kind

@@ -0,0 +1,3 @@
+type PriorityQueue<A: Type> {
+  new(priority: A -> Nat, tree: PriorityQueue.Tree<A>)
+}

base/PriorityQueue/In.kind

@@ -0,0 +1,3 @@
+PriorityQueue.In<A: Type>(queue: PriorityQueue<A>, a: A): Type
+  open queue
+  PriorityQueue.Tree.In!(queue.tree, a)

base/PriorityQueue/Tree.kind

@@ -0,0 +1,4 @@
+type PriorityQueue.Tree <A: Type> {
+    empty
+    node(rank: Nat, element: A, left: PriorityQueue.Tree<A>, right: PriorityQueue.Tree<A>)
+}

base/PriorityQueue/Tree/Either.kind

@@ -0,0 +1,5 @@
+type PriorityQueue.Tree.Either<A: Type, B: Type, C:Type> {
+  left(value: A)
+  here(value: B)
+  right(value: C)
+}

base/PriorityQueue/Tree/In.kind

@@ -0,0 +1,6 @@
+PriorityQueue.Tree.In<A: Type>(tree: PriorityQueue.Tree<A>, a: A): Type
+  case tree {
+    empty: Empty
+    node:
+      PriorityQueue.Tree.Either<PriorityQueue.Tree.In!(tree.left, a), tree.element == a, PriorityQueue.Tree.In!(tree.right, a)>
+  }

base/PriorityQueue/Tree/empty_tree_is_empty.kind

@@ -0,0 +1,2 @@
+PriorityQueue.Tree.empty_tree_is_empty<A: Type>: PriorityQueue.Tree.is_empty(A, PriorityQueue.Tree.empty(A)) == true
+  refl

base/PriorityQueue/Tree/is_empty.kind

@@ -0,0 +1,5 @@
+PriorityQueue.Tree.is_empty<A: Type>(tree: PriorityQueue.Tree<A>): Bool
+  case tree {
+      empty: true
+      node: false
+  }

base/PriorityQueue/Tree/make.kind

@@ -0,0 +1,7 @@
+PriorityQueue.Tree.make<A: Type>(element: A, a: PriorityQueue.Tree<A>, b: PriorityQueue.Tree<A>): PriorityQueue.Tree<A>
+  let rank_a = PriorityQueue.Tree.rank!(a)
+  let rank_b = PriorityQueue.Tree.rank!(b)
+  if Nat.gte(rank_a, rank_b) then
+    PriorityQueue.Tree.node!(Nat.succ(rank_b), element, a b)    
+  else
+    PriorityQueue.Tree.node!(Nat.succ(rank_a), element, b a)

base/PriorityQueue/Tree/merge.kind

@@ -0,0 +1,13 @@
+PriorityQueue.Tree.merge<A: Type>(priority: A -> Nat, a: PriorityQueue.Tree<A>, b: PriorityQueue.Tree<A>): PriorityQueue.Tree<A>
+  case a {
+    empty: b
+    node:
+      case b {
+          empty: a
+          node:
+            if Nat.lte(priority(a.element), priority(b.element)) then
+              PriorityQueue.Tree.make!(a.element, a.left, PriorityQueue.Tree.merge!(priority, a.right, b))
+            else
+              PriorityQueue.Tree.make!(b.element, b.left, PriorityQueue.Tree.merge!(priority, a, b.right))
+      }
+  }

base/PriorityQueue/Tree/peek.kind

@@ -0,0 +1,9 @@
+PriorityQueue.Tree.peek<A: Type>(tree: PriorityQueue.Tree<A>)<Hyp: PriorityQueue.Tree.is_empty!(tree) == false>: A
+  case tree with Hyp {
+      empty:
+        let hypothesis = Hyp :: rewrite x in (x == false) with PriorityQueue.Tree.empty_tree_is_empty<A>
+        let impossible = Bool.true_neq_false(hypothesis)
+        Empty.absurd!(impossible)
+      node: tree.element
+  }!
+

base/PriorityQueue/Tree/rank.kind

@@ -0,0 +1,6 @@
+PriorityQueue.Tree.rank<A: Type>(tree: PriorityQueue.Tree<A>): Nat
+  case tree {
+      empty: 0
+      node: tree.rank
+  }
+

base/PriorityQueue/Tree/singleton.kind

@@ -0,0 +1,2 @@
+PriorityQueue.Tree.singleton<A: Type>(a: A): PriorityQueue.Tree<A>
+  PriorityQueue.Tree.node!(1, a, PriorityQueue.Tree.empty!, PriorityQueue.Tree.empty!)

base/PriorityQueue/empty.kind

@@ -0,0 +1,2 @@
+PriorityQueue.empty<A: Type>(priority: A -> Nat): PriorityQueue<A>
+  PriorityQueue.new!(priority, PriorityQueue.Tree.empty!)

base/PriorityQueue/head.kind

@@ -0,0 +1,6 @@
+PriorityQueue.head<A: Type>(queue: PriorityQueue<A>): Maybe<A>
+  open queue
+  case queue.tree {
+      empty: Maybe.none!
+      node: Maybe.some!(queue.tree.element) 
+  }

base/PriorityQueue/insert.kind

@@ -0,0 +1,5 @@
+PriorityQueue.insert<A: Type>(a: A, queue: PriorityQueue<A>): PriorityQueue<A>
+  open queue
+  let singleton = PriorityQueue.Tree.singleton!(a)
+  let merged = PriorityQueue.Tree.merge!(queue.priority, singleton queue.tree)
+  PriorityQueue.new!(queue.priority, merged)

base/PriorityQueue/is_empty.kind

@@ -0,0 +1,3 @@
+PriorityQueue.is_empty<A: Type>(queue: PriorityQueue<A>): Bool
+  open queue
+  PriorityQueue.Tree.is_empty!(queue.tree)

base/PriorityQueue/is_empty_queue_implies_is_empty_tree.kind

@@ -0,0 +1,4 @@
+PriorityQueue.is_empty_queue_implies_is_empty_tree<A: Type>(queue: PriorityQueue<A>): PriorityQueue.is_empty!(queue) == PriorityQueue.Tree.is_empty!(PriorityQueue.tree_of!(queue))
+  case queue {
+      new: refl
+  }!

base/PriorityQueue/priority.kind

@@ -0,0 +1,3 @@
+PriorityQueue.priority<A: Type>(queue: PriorityQueue<A>, a: A): Nat
+  open queue
+  queue.priority(a)

base/PriorityQueue/safe_head.kind

@@ -0,0 +1,3 @@
+PriorityQueue.safe_head<A: Type>(queue: PriorityQueue<A>)<Hyp: PriorityQueue.is_empty!(queue) == false>: A
+  let hypothesis = Hyp :: rewrite x in (x == false) with PriorityQueue.is_empty_queue_implies_is_empty_tree!(queue)
+  PriorityQueue.Tree.peek!(PriorityQueue.tree_of!(queue), hypothesis)

base/PriorityQueue/tail.kind

@@ -0,0 +1,9 @@
+PriorityQueue.tail<A: Type>(queue: PriorityQueue<A>): PriorityQueue<A>
+  open queue
+  case queue.tree {
+      empty: queue
+      node:
+        let priority = queue.priority
+        let merged = PriorityQueue.Tree.merge!(priority, queue.tree.left, queue.tree.right)
+        PriorityQueue.new!(queue.priority, merged)
+  }

base/PriorityQueue/tree_of.kind

@@ -0,0 +1,3 @@
+PriorityQueue.tree_of<A: Type>(queue: PriorityQueue<A>): PriorityQueue.Tree<A>
+  open queue
+  queue.tree