chore: remove BinomialHeap, DList, Stack, Queue
These are moving to std4.
This commit is contained in:
Mario Carneiro
Leonardo de Moura
parent
bf89c5a0f5
commit
0efbc0bc03
13 changed files with 19 additions and 464 deletions
|
|
@ -3,10 +3,6 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
|||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
import Bootstrap.Data.BinomialHeap
|
||||
import Bootstrap.Data.DList
|
||||
import Bootstrap.Data.Stack
|
||||
import Bootstrap.Data.Queue
|
||||
import Bootstrap.Data.HashMap
|
||||
import Bootstrap.Data.HashSet
|
||||
import Bootstrap.Data.PersistentArray
|
||||
|
|
|
|||
|
|
@ -1,236 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura, Jannis Limperg
|
||||
-/
|
||||
namespace Std
|
||||
universe u
|
||||
namespace BinomialHeapImp
|
||||
|
||||
structure HeapNodeAux (α : Type u) (h : Type u) where
|
||||
val : α
|
||||
rank : Nat
|
||||
children : List h
|
||||
|
||||
-- A `Heap` is a forest of binomial trees.
|
||||
inductive Heap (α : Type u) : Type u where
|
||||
| heap (ns : List (HeapNodeAux α (Heap α))) : Heap α
|
||||
deriving Inhabited
|
||||
|
||||
open Heap
|
||||
|
||||
-- A `HeapNode` is a binomial tree. If a `HeapNode` has rank `k`, its children
|
||||
-- have ranks between `0` and `k - 1`. They are ordered by rank. Additionally,
|
||||
-- the value of each child must be less than or equal to the value of its
|
||||
-- parent node.
|
||||
abbrev HeapNode α := HeapNodeAux α (Heap α)
|
||||
|
||||
variable {α : Type u}
|
||||
|
||||
def hRank : List (HeapNode α) → Nat
|
||||
| [] => 0
|
||||
| h::_ => h.rank
|
||||
|
||||
def isEmpty : Heap α → Bool
|
||||
| heap [] => true
|
||||
| _ => false
|
||||
|
||||
def empty : Heap α :=
|
||||
heap []
|
||||
|
||||
def singleton (a : α) : Heap α :=
|
||||
heap [{ val := a, rank := 1, children := [] }]
|
||||
|
||||
-- Combine two binomial trees of rank `r`, creating a binomial tree of rank
|
||||
-- `r + 1`.
|
||||
@[specialize] def combine (le : α → α → Bool) (n₁ n₂ : HeapNode α) : HeapNode α :=
|
||||
if le n₂.val n₁.val then
|
||||
{ n₂ with rank := n₂.rank + 1, children := n₂.children ++ [heap [n₁]] }
|
||||
else
|
||||
{ n₁ with rank := n₁.rank + 1, children := n₁.children ++ [heap [n₂]] }
|
||||
|
||||
-- Merge two forests of binomial trees. The forests are assumed to be ordered
|
||||
-- by rank and `mergeNodes` maintains this invariant.
|
||||
@[specialize] def mergeNodes (le : α → α → Bool) : List (HeapNode α) → List (HeapNode α) → List (HeapNode α)
|
||||
| [], h => h
|
||||
| h, [] => h
|
||||
| f@(h₁ :: t₁), s@(h₂ :: t₂) =>
|
||||
if h₁.rank < h₂.rank then h₁ :: mergeNodes le t₁ s
|
||||
else if h₂.rank < h₁.rank then h₂ :: mergeNodes le t₂ f
|
||||
else
|
||||
let merged := combine le h₁ h₂
|
||||
let r := merged.rank
|
||||
if r != hRank t₁ then
|
||||
if r != hRank t₂ then merged :: mergeNodes le t₁ t₂ else mergeNodes le (merged :: t₁) t₂
|
||||
else
|
||||
if r != hRank t₂ then mergeNodes le t₁ (merged :: t₂) else merged :: mergeNodes le t₁ t₂
|
||||
termination_by _ h₁ h₂ => h₁.length + h₂.length
|
||||
decreasing_by simp_wf; simp_arith [*]
|
||||
|
||||
@[specialize] def merge (le : α → α → Bool) : Heap α → Heap α → Heap α
|
||||
| heap h₁, heap h₂ => heap (mergeNodes le h₁ h₂)
|
||||
|
||||
@[specialize] def head? (le : α → α → Bool) : Heap α → Option α
|
||||
| heap [] => none
|
||||
| heap (h::hs) => some $
|
||||
hs.foldl (init := h.val) fun r n => if le r n.val then r else n.val
|
||||
|
||||
@[inline] def head [Inhabited α] (le : α → α → Bool) (h : Heap α) : α :=
|
||||
head? le h |>.getD default
|
||||
|
||||
@[specialize] def findMin (le : α → α → Bool) : List (HeapNode α) → Nat → HeapNode α × Nat → HeapNode α × Nat
|
||||
| [], _, r => r
|
||||
| h::hs, idx, (h', idx') => if le h'.val h.val then findMin le hs (idx+1) (h', idx') else findMin le hs (idx+1) (h, idx)
|
||||
-- It is important that we check `le h'.val h.val` here, not the other way
|
||||
-- around. This ensures that head? and findMin find the same element even
|
||||
-- when we have `le h'.val h.val` and `le h.val h'.val` (i.e. le is not
|
||||
-- irreflexive).
|
||||
|
||||
def deleteMin (le : α → α → Bool) : Heap α → Option (α × Heap α)
|
||||
| heap [] => none
|
||||
| heap [h] =>
|
||||
let tail :=
|
||||
match h.children with
|
||||
| [] => empty
|
||||
| (h::hs) => hs.foldl (merge le) h
|
||||
some (h.val, tail)
|
||||
| heap hhs@(h::hs) =>
|
||||
let (min, minIdx) := findMin le hs 1 (h, 0)
|
||||
let rest := hhs.eraseIdx minIdx
|
||||
let tail := min.children.foldl (merge le) (heap rest)
|
||||
some (min.val, tail)
|
||||
|
||||
@[inline] def tail? (le : α → α → Bool) (h : Heap α) : Option (Heap α) :=
|
||||
deleteMin le h |>.map (·.snd)
|
||||
|
||||
@[inline] def tail (le : α → α → Bool) (h : Heap α) : Heap α :=
|
||||
tail? le h |>.getD empty
|
||||
|
||||
partial def toList (le : α → α → Bool) (h : Heap α) : List α :=
|
||||
match deleteMin le h with
|
||||
| none => []
|
||||
| some (hd, tl) => hd :: toList le tl
|
||||
|
||||
partial def toArray (le : α → α → Bool) (h : Heap α) : Array α :=
|
||||
go #[] h
|
||||
where
|
||||
go (acc : Array α) (h : Heap α) : Array α :=
|
||||
match deleteMin le h with
|
||||
| none => acc
|
||||
| some (hd, tl) => go (acc.push hd) tl
|
||||
|
||||
partial def toListUnordered : Heap α → List α
|
||||
| heap ns => ns.bind fun n => n.val :: n.children.bind toListUnordered
|
||||
|
||||
partial def toArrayUnordered (h : Heap α) : Array α :=
|
||||
go #[] h
|
||||
where
|
||||
go (acc : Array α) : Heap α → Array α
|
||||
| heap ns => Id.run do
|
||||
let mut acc := acc
|
||||
for n in ns do
|
||||
acc := acc.push n.val
|
||||
for h in n.children do
|
||||
acc := go acc h
|
||||
return acc
|
||||
|
||||
inductive WellFormed (le : α → α → Bool) : Heap α → Prop where
|
||||
| empty : WellFormed le empty
|
||||
| singleton (a) : WellFormed le (singleton a)
|
||||
| merge (h₁ h₂) : WellFormed le h₁ → WellFormed le h₂ → WellFormed le (merge le h₁ h₂)
|
||||
| deleteMin (a) (h tl) : WellFormed le h → deleteMin le h = some (a, tl) → WellFormed le tl
|
||||
|
||||
theorem WellFormed.tail? {le} (h tl : Heap α) (hwf : WellFormed le h) (eq : tail? le h = some tl) : WellFormed le tl := by
|
||||
simp only [BinomialHeapImp.tail?] at eq
|
||||
match eq₂: BinomialHeapImp.deleteMin le h with
|
||||
| none =>
|
||||
rw [eq₂] at eq; cases eq
|
||||
| some (a, tl) =>
|
||||
rw [eq₂] at eq; cases eq
|
||||
exact deleteMin _ _ _ hwf eq₂
|
||||
|
||||
theorem WellFormed.tail {le} (h : Heap α) (hwf : WellFormed le h) : WellFormed le (tail le h) := by
|
||||
simp only [BinomialHeapImp.tail]
|
||||
match eq: BinomialHeapImp.tail? le h with
|
||||
| none => exact empty
|
||||
| some tl => exact tail? _ _ hwf eq
|
||||
|
||||
end BinomialHeapImp
|
||||
|
||||
open BinomialHeapImp
|
||||
|
||||
def BinomialHeap (α : Type u) (le : α → α → Bool) := { h : Heap α // WellFormed le h }
|
||||
|
||||
@[inline] def mkBinomialHeap (α : Type u) (le : α → α → Bool) : BinomialHeap α le :=
|
||||
⟨empty, WellFormed.empty⟩
|
||||
|
||||
namespace BinomialHeap
|
||||
variable {α : Type u} {le : α → α → Bool}
|
||||
|
||||
@[inline] def empty : BinomialHeap α le :=
|
||||
mkBinomialHeap α le
|
||||
|
||||
@[inline] def isEmpty : BinomialHeap α le → Bool
|
||||
| ⟨b, _⟩ => BinomialHeapImp.isEmpty b
|
||||
|
||||
/-- O(1) -/
|
||||
@[inline] def singleton (a : α) : BinomialHeap α le :=
|
||||
⟨BinomialHeapImp.singleton a, WellFormed.singleton a⟩
|
||||
|
||||
/-- O(log n) -/
|
||||
@[inline] def merge : BinomialHeap α le → BinomialHeap α le → BinomialHeap α le
|
||||
| ⟨b₁, h₁⟩, ⟨b₂, h₂⟩ => ⟨BinomialHeapImp.merge le b₁ b₂, WellFormed.merge b₁ b₂ h₁ h₂⟩
|
||||
|
||||
/-- O(log n) -/
|
||||
@[inline] def insert (a : α) (h : BinomialHeap α le) : BinomialHeap α le :=
|
||||
merge (singleton a) h
|
||||
|
||||
/-- O(n log n) -/
|
||||
def ofList (le : α → α → Bool) (as : List α) : BinomialHeap α le :=
|
||||
as.foldl (flip insert) empty
|
||||
|
||||
/-- O(n log n) -/
|
||||
def ofArray (le : α → α → Bool) (as : Array α) : BinomialHeap α le :=
|
||||
as.foldl (flip insert) empty
|
||||
|
||||
/-- O(log n) -/
|
||||
@[inline] def deleteMin : BinomialHeap α le → Option (α × BinomialHeap α le)
|
||||
| ⟨b, h⟩ =>
|
||||
match eq: BinomialHeapImp.deleteMin le b with
|
||||
| none => none
|
||||
| some (a, tl) => some (a, ⟨tl, WellFormed.deleteMin a b tl h eq⟩)
|
||||
|
||||
/-- O(log n) -/
|
||||
@[inline] def head [Inhabited α] : BinomialHeap α le → α
|
||||
| ⟨b, _⟩ => BinomialHeapImp.head le b
|
||||
|
||||
/-- O(log n) -/
|
||||
@[inline] def head? : BinomialHeap α le → Option α
|
||||
| ⟨b, _⟩ => BinomialHeapImp.head? le b
|
||||
|
||||
/-- O(log n) -/
|
||||
@[inline] def tail? : BinomialHeap α le → Option (BinomialHeap α le)
|
||||
| ⟨b, h⟩ =>
|
||||
match eq: BinomialHeapImp.tail? le b with
|
||||
| none => none
|
||||
| some tl => some ⟨tl, WellFormed.tail? b tl h eq⟩
|
||||
|
||||
/-- O(log n) -/
|
||||
@[inline] def tail : BinomialHeap α le → BinomialHeap α le
|
||||
| ⟨b, h⟩ => ⟨BinomialHeapImp.tail le b, WellFormed.tail b h⟩
|
||||
|
||||
/-- O(n log n) -/
|
||||
@[inline] def toList : BinomialHeap α le → List α
|
||||
| ⟨b, _⟩ => BinomialHeapImp.toList le b
|
||||
|
||||
/-- O(n log n) -/
|
||||
@[inline] def toArray : BinomialHeap α le → Array α
|
||||
| ⟨b, _⟩ => BinomialHeapImp.toArray le b
|
||||
|
||||
/-- O(n) -/
|
||||
@[inline] def toListUnordered : BinomialHeap α le → List α
|
||||
| ⟨b, _⟩ => BinomialHeapImp.toListUnordered b
|
||||
|
||||
/-- O(n) -/
|
||||
@[inline] def toArrayUnordered : BinomialHeap α le → Array α
|
||||
| ⟨b, _⟩ => BinomialHeapImp.toArrayUnordered b
|
||||
|
|
@ -1,64 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Leonardo de Moura
|
||||
-/
|
||||
namespace Std
|
||||
universe u
|
||||
/--
|
||||
A difference List is a Function that, given a List, returns the original
|
||||
contents of the difference List prepended to the given List.
|
||||
This structure supports `O(1)` `append` and `concat` operations on lists, making it
|
||||
useful for append-heavy uses such as logging and pretty printing.
|
||||
-/
|
||||
structure DList (α : Type u) where
|
||||
apply : List α → List α
|
||||
invariant : ∀ l, apply l = apply [] ++ l
|
||||
|
||||
namespace DList
|
||||
variable {α : Type u}
|
||||
open List
|
||||
|
||||
def ofList (l : List α) : DList α :=
|
||||
⟨(l ++ ·), fun t => by simp⟩
|
||||
|
||||
def empty : DList α :=
|
||||
⟨id, fun _ => rfl⟩
|
||||
|
||||
instance : EmptyCollection (DList α) :=
|
||||
⟨DList.empty⟩
|
||||
|
||||
def toList : DList α → List α
|
||||
| ⟨f, _⟩ => f []
|
||||
|
||||
def singleton (a : α) : DList α := {
|
||||
apply := fun t => a :: t,
|
||||
invariant := fun _ => rfl
|
||||
}
|
||||
|
||||
def cons : α → DList α → DList α
|
||||
| a, ⟨f, h⟩ => {
|
||||
apply := fun t => a :: f t,
|
||||
invariant := by intro t; simp; rw [h]
|
||||
}
|
||||
|
||||
def append : DList α → DList α → DList α
|
||||
| ⟨f, h₁⟩, ⟨g, h₂⟩ => {
|
||||
apply := f ∘ g,
|
||||
invariant := by
|
||||
intro t
|
||||
show f (g t) = (f (g [])) ++ t
|
||||
rw [h₁ (g t), h₂ t, ← append_assoc (f []) (g []) t, ← h₁ (g [])]
|
||||
}
|
||||
|
||||
def push : DList α → α → DList α
|
||||
| ⟨f, h⟩, a => {
|
||||
apply := fun t => f (a :: t),
|
||||
invariant := by
|
||||
intro t
|
||||
show f (a :: t) = f (a :: nil) ++ t
|
||||
rw [h [a], h (a::t), append_assoc (f []) [a] t]
|
||||
rfl
|
||||
}
|
||||
|
||||
instance : Append (DList α) := ⟨DList.append⟩
|
||||
|
|
@ -1,38 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Daniel Selsam
|
||||
|
||||
Simple queue implemented using two lists.
|
||||
Note: this is only a temporary placeholder.
|
||||
-/
|
||||
namespace Std
|
||||
universe u v w
|
||||
|
||||
structure Queue (α : Type u) where
|
||||
eList : List α := []
|
||||
dList : List α := []
|
||||
|
||||
namespace Queue
|
||||
|
||||
variable {α : Type u}
|
||||
|
||||
def empty : Queue α :=
|
||||
{ eList := [], dList := [] }
|
||||
|
||||
def isEmpty (q : Queue α) : Bool :=
|
||||
q.dList.isEmpty && q.eList.isEmpty
|
||||
|
||||
def enqueue (v : α) (q : Queue α) : Queue α :=
|
||||
{ q with eList := v::q.eList }
|
||||
|
||||
def enqueueAll (vs : List α) (q : Queue α) : Queue α :=
|
||||
{ q with eList := vs ++ q.eList }
|
||||
|
||||
def dequeue? (q : Queue α) : Option (α × Queue α) :=
|
||||
match q.dList with
|
||||
| d::ds => some (d, { q with dList := ds })
|
||||
| [] =>
|
||||
match q.eList.reverse with
|
||||
| [] => none
|
||||
| d::ds => some (d, { eList := [], dList := ds })
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Daniel Selsam
|
||||
|
||||
Simple stack API implemented using an array.
|
||||
-/
|
||||
namespace Std
|
||||
universe u v w
|
||||
|
||||
structure Stack (α : Type u) where
|
||||
vals : Array α := #[]
|
||||
|
||||
namespace Stack
|
||||
|
||||
variable {α : Type u}
|
||||
|
||||
def empty : Stack α := {}
|
||||
|
||||
def isEmpty (s : Stack α) : Bool :=
|
||||
s.vals.isEmpty
|
||||
|
||||
def push (v : α) (s : Stack α) : Stack α :=
|
||||
{ s with vals := s.vals.push v }
|
||||
|
||||
def peek? (s : Stack α) : Option α :=
|
||||
if s.vals.isEmpty then none else s.vals.get? (s.vals.size-1)
|
||||
|
||||
def peek! [Inhabited α] (s : Stack α) : α :=
|
||||
s.vals.back
|
||||
|
||||
def pop [Inhabited α] (s : Stack α) : Stack α :=
|
||||
{ s with vals := s.vals.pop }
|
||||
|
||||
def modify [Inhabited α] (s : Stack α) (f : α → α) : Stack α :=
|
||||
{ s with vals := s.vals.modify (s.vals.size-1) f }
|
||||
|
|
@ -1,28 +0,0 @@
|
|||
import Bootstrap.Data.BinomialHeap
|
||||
|
||||
open Std
|
||||
|
||||
abbrev Heap := BinomialHeap Nat (fun a b => a < b)
|
||||
|
||||
def mkHeap (n m : Nat) : Heap :=
|
||||
let hs : List Heap := n.fold (fun i hs =>
|
||||
let h : Heap := BinomialHeap.empty
|
||||
let h : Heap := m.fold (fun j h =>
|
||||
let v := n*m - j*n - i
|
||||
h.insert v) h
|
||||
h :: hs)
|
||||
[]
|
||||
hs.foldl (fun h₁ h₂ => h₁.merge h₂) BinomialHeap.empty
|
||||
|
||||
partial def display : Nat → Heap → IO Unit
|
||||
| prev, h => do
|
||||
if h.isEmpty then pure ()
|
||||
else
|
||||
let m := h.head
|
||||
unless prev < m do IO.println s!"failed {prev} {m}"
|
||||
display m h.tail
|
||||
|
||||
def main : IO Unit := do
|
||||
let h := mkHeap 20 20
|
||||
display 0 h
|
||||
IO.println h.toList.length
|
||||
|
|
@ -1 +0,0 @@
|
|||
400
|
||||
|
|
@ -1,9 +0,0 @@
|
|||
import Bootstrap.Data.BinomialHeap
|
||||
|
||||
open Std
|
||||
|
||||
def test : BinomialHeap (Nat × Nat) (λ (x, _) (y, _) => x < y) :=
|
||||
BinomialHeap.empty.insert (0, 1) |>.insert (0, 2) |>.insert (0, 3)
|
||||
|
||||
#eval test.head
|
||||
#eval test.tail.toList
|
||||
|
|
@ -1,2 +0,0 @@
|
|||
(0, 2)
|
||||
[(0, 3), (0, 1)]
|
||||
|
|
@ -1,20 +0,0 @@
|
|||
import Bootstrap
|
||||
|
||||
open Std
|
||||
open BinomialHeap
|
||||
|
||||
def h₁ : BinomialHeap Nat (· < ·) := BinomialHeap.ofList _ [2, 1, 3, 5, 4]
|
||||
def h₂ : BinomialHeap Nat (· < ·) := BinomialHeap.ofList _ [0, 1, 6]
|
||||
|
||||
#eval h₁.head
|
||||
#eval h₁.tail.toList
|
||||
#eval h₁.deleteMin.map (·.fst)
|
||||
#eval h₁.deleteMin.map (·.snd.toList)
|
||||
#eval h₁.toList
|
||||
#eval h₁.toArray
|
||||
#eval h₁.toArrayUnordered.qsort (· < ·)
|
||||
#eval h₁.toListUnordered.toArray.qsort (· < ·)
|
||||
#eval h₁.insert 7 |>.toList
|
||||
#eval h₁.insert 0 |>.toList
|
||||
#eval h₁.insert 4 |>.toList
|
||||
#eval h₁.merge h₂ |>.toList
|
||||
|
|
@ -1,12 +0,0 @@
|
|||
1
|
||||
[2, 3, 4, 5]
|
||||
some 1
|
||||
some [2, 3, 4, 5]
|
||||
[1, 2, 3, 4, 5]
|
||||
#[1, 2, 3, 4, 5]
|
||||
#[1, 2, 3, 4, 5]
|
||||
#[1, 2, 3, 4, 5]
|
||||
[1, 2, 3, 4, 5, 7]
|
||||
[0, 1, 2, 3, 4, 5]
|
||||
[1, 2, 3, 4, 4, 5]
|
||||
[0, 1, 1, 2, 3, 4, 5, 6]
|
||||
|
|
@ -308,10 +308,10 @@ def takesStrictMotive ⦃motive : Nat → Type⦄ {n : Nat} (x : motive n) : mot
|
|||
#testDelab @takesStrictMotive (fun x => Unit) 0 expecting takesStrictMotive (motive := fun x => Unit) (n := 0)
|
||||
#testDelab @takesStrictMotive (fun x => Unit) 0 () expecting takesStrictMotive (motive := fun x => Unit) (n := 0) ()
|
||||
|
||||
def stackMkInjEqSnippet :=
|
||||
fun {α : Type} (xs : Array α) => Eq.ndrec (motive := fun _ => (Std.Stack.mk xs = Std.Stack.mk xs)) (Eq.refl (Std.Stack.mk xs)) (rfl : xs = xs)
|
||||
def arrayMkInjEqSnippet :=
|
||||
fun {α : Type} (xs : List α) => Eq.ndrec (motive := fun _ => (Array.mk xs = Array.mk xs)) (Eq.refl (Array.mk xs)) (rfl : xs = xs)
|
||||
|
||||
#testDelabN stackMkInjEqSnippet
|
||||
#testDelabN arrayMkInjEqSnippet
|
||||
|
||||
def typeAs (α : Type u) (a : α) := ()
|
||||
|
||||
|
|
@ -346,7 +346,7 @@ set_option pp.analyze.trustSubtypeMk true in
|
|||
#testDelabN Lean.Elab.InfoTree.goalsAt?.match_1
|
||||
#testDelabN Std.ShareCommon.ObjectMap.find?
|
||||
#testDelabN Std.ShareCommon.ObjectMap.insert
|
||||
#testDelabN Std.Stack.mk.injEq
|
||||
#testDelabN Array.mk.injEq
|
||||
#testDelabN Lean.PrefixTree.empty
|
||||
#testDelabN Std.PersistentHashMap.getCollisionNodeSize.match_1
|
||||
#testDelabN Std.HashMap.size.match_1
|
||||
|
|
|
|||
|
|
@ -1,17 +1,22 @@
|
|||
import Bootstrap
|
||||
structure HeapNodeAux (α : Type u) (h : Type u) where
|
||||
val : α
|
||||
children : List h
|
||||
|
||||
namespace Std.BinomialHeapImp
|
||||
-- A `Heap` is a forest of binomial trees.
|
||||
inductive Heap (α : Type u) : Type u where
|
||||
| heap (ns : List (HeapNodeAux α (Heap α))) : Heap α
|
||||
deriving Inhabited
|
||||
|
||||
open Heap
|
||||
|
||||
partial def toArrayUnordered' (h : Heap α) : Array α :=
|
||||
go #[] h
|
||||
where
|
||||
go (acc : Array α) : Heap α → Array α
|
||||
| heap ns => Id.run do
|
||||
let mut acc := acc
|
||||
for h₁ : n in ns do
|
||||
acc := acc.push n.val
|
||||
for h₂ : h in n.children do
|
||||
acc := go acc h
|
||||
return acc
|
||||
go (acc : Array α) : Heap α → Array α
|
||||
| heap ns => Id.run do
|
||||
let mut acc := acc
|
||||
for h₁ : n in ns do
|
||||
acc := acc.push n.val
|
||||
for h₂ : h in n.children do
|
||||
acc := go acc h
|
||||
return acc
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue