From 0efbc0bc03e8bc3f31f996482110492383dcface Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Mon, 29 Aug 2022 03:50:25 -0400 Subject: [PATCH] chore: remove BinomialHeap, DList, Stack, Queue These are moving to std4. --- src/Bootstrap/Data.lean | 4 - src/Bootstrap/Data/BinomialHeap.lean | 236 ---------------------- src/Bootstrap/Data/DList.lean | 64 ------ src/Bootstrap/Data/Queue.lean | 38 ---- src/Bootstrap/Data/Stack.lean | 36 ---- tests/compiler/binomial.lean | 28 --- tests/compiler/binomial.lean.expected.out | 1 - tests/lean/629.lean | 9 - tests/lean/629.lean.expected.out | 2 - tests/lean/binomialHeap.lean | 20 -- tests/lean/binomialHeap.lean.expected.out | 12 -- tests/lean/run/PPTopDownAnalyze.lean | 8 +- tests/lean/run/forInElabBug.lean | 25 ++- 13 files changed, 19 insertions(+), 464 deletions(-) delete mode 100644 src/Bootstrap/Data/BinomialHeap.lean delete mode 100644 src/Bootstrap/Data/DList.lean delete mode 100644 src/Bootstrap/Data/Queue.lean delete mode 100644 src/Bootstrap/Data/Stack.lean delete mode 100644 tests/compiler/binomial.lean delete mode 100644 tests/compiler/binomial.lean.expected.out delete mode 100644 tests/lean/629.lean delete mode 100644 tests/lean/629.lean.expected.out delete mode 100644 tests/lean/binomialHeap.lean delete mode 100644 tests/lean/binomialHeap.lean.expected.out diff --git a/src/Bootstrap/Data.lean b/src/Bootstrap/Data.lean index 3dc761b815..2a24d7935b 100644 --- a/src/Bootstrap/Data.lean +++ b/src/Bootstrap/Data.lean @@ -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 diff --git a/src/Bootstrap/Data/BinomialHeap.lean b/src/Bootstrap/Data/BinomialHeap.lean deleted file mode 100644 index d99d696db7..0000000000 --- a/src/Bootstrap/Data/BinomialHeap.lean +++ /dev/null @@ -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 diff --git a/src/Bootstrap/Data/DList.lean b/src/Bootstrap/Data/DList.lean deleted file mode 100644 index 4c1d7a121e..0000000000 --- a/src/Bootstrap/Data/DList.lean +++ /dev/null @@ -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⟩ diff --git a/src/Bootstrap/Data/Queue.lean b/src/Bootstrap/Data/Queue.lean deleted file mode 100644 index b7610fe9ea..0000000000 --- a/src/Bootstrap/Data/Queue.lean +++ /dev/null @@ -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 }) diff --git a/src/Bootstrap/Data/Stack.lean b/src/Bootstrap/Data/Stack.lean deleted file mode 100644 index 5fd76f7b17..0000000000 --- a/src/Bootstrap/Data/Stack.lean +++ /dev/null @@ -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 } diff --git a/tests/compiler/binomial.lean b/tests/compiler/binomial.lean deleted file mode 100644 index 72ad89a806..0000000000 --- a/tests/compiler/binomial.lean +++ /dev/null @@ -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 diff --git a/tests/compiler/binomial.lean.expected.out b/tests/compiler/binomial.lean.expected.out deleted file mode 100644 index d411bb7c1a..0000000000 --- a/tests/compiler/binomial.lean.expected.out +++ /dev/null @@ -1 +0,0 @@ -400 diff --git a/tests/lean/629.lean b/tests/lean/629.lean deleted file mode 100644 index 3e9f861271..0000000000 --- a/tests/lean/629.lean +++ /dev/null @@ -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 diff --git a/tests/lean/629.lean.expected.out b/tests/lean/629.lean.expected.out deleted file mode 100644 index abded944c0..0000000000 --- a/tests/lean/629.lean.expected.out +++ /dev/null @@ -1,2 +0,0 @@ -(0, 2) -[(0, 3), (0, 1)] diff --git a/tests/lean/binomialHeap.lean b/tests/lean/binomialHeap.lean deleted file mode 100644 index 88bd8bd321..0000000000 --- a/tests/lean/binomialHeap.lean +++ /dev/null @@ -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 diff --git a/tests/lean/binomialHeap.lean.expected.out b/tests/lean/binomialHeap.lean.expected.out deleted file mode 100644 index b095d8a041..0000000000 --- a/tests/lean/binomialHeap.lean.expected.out +++ /dev/null @@ -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] diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 86328186c4..e67ceddad7 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -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 diff --git a/tests/lean/run/forInElabBug.lean b/tests/lean/run/forInElabBug.lean index e03cb8ee6a..8e88cc7a88 100644 --- a/tests/lean/run/forInElabBug.lean +++ b/tests/lean/run/forInElabBug.lean @@ -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