chore: update to 2023-01-10 nightly

Aesop/Builder/Forward.lean

@@ -47,7 +47,7 @@ def getImmediatePremises (name : Name) (type : Expr) : Option (Array Name) →
     -- If immediate names are given, we check that corresponding arguments
     -- exists and record these arguments' positions.
     forallTelescopeReducing type λ args _ => do
-      let mut unseen := immediate.deduplicate (ord := ⟨Name.quickCmp⟩)
+      let mut unseen := immediate.sortAndDeduplicate (ord := ⟨Name.quickCmp⟩)
       let mut result := #[]
       for h : i in [:args.size] do
         have h : i < args.size := by simp_all [Membership.mem]

Aesop/Frontend/RuleExpr.lean

@@ -673,7 +673,7 @@ def toAdditionalRules (e : RuleExpr) (init : RuleConfig Option)
       | .ruleSets newRuleSets =>
         have _ : Ord RuleSetName := ⟨Name.quickCmp⟩
         let ruleSets :=
-          ⟨Array.mergeSortedFilteringDuplicates r.ruleSets.ruleSets $
+          ⟨Array.mergeSortedDeduplicating r.ruleSets.ruleSets $
             newRuleSets.ruleSets.qsortOrd⟩
         return { r with ruleSets }
 
@@ -775,7 +775,7 @@ def toRuleNameFilters (e : RuleExpr) :
       | .ruleSets newRuleSets =>
         have _ : Ord RuleSetName := ⟨Name.quickCmp⟩
         let ruleSets :=
-          ⟨Array.mergeSortedFilteringDuplicates r.ruleSets.ruleSets $
+          ⟨Array.mergeSortedDeduplicating r.ruleSets.ruleSets $
             newRuleSets.ruleSets.qsortOrd⟩
         return { r with ruleSets }
 

Aesop/Index.lean

@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.Index.Basic
+import Std.Lean.Meta.InstantiateMVars
 
 open Lean
 open Lean.Meta
@@ -37,8 +38,8 @@ instance : EmptyCollection (Index α) where
   }
 
 def merge (ri₁ ri₂ : Index α) : Index α where
-  byTarget := ri₁.byTarget.merge ri₂.byTarget
-  byHyp := ri₁.byHyp.merge ri₂.byHyp
+  byTarget := ri₁.byTarget.mergePreservingDuplicates ri₂.byTarget
+  byHyp := ri₁.byHyp.mergePreservingDuplicates ri₂.byHyp
   unindexed := ri₁.unindexed.merge ri₂.unindexed
 
 @[specialize]

Aesop/Profiling.lean

@@ -8,8 +8,7 @@ import Aesop.Nanos
 import Aesop.Tree.Data
 import Aesop.Tracing
 
-open Lean hiding HashMap
-open Std (HashMap)
+open Lean
 
 namespace Aesop
 
@@ -108,18 +107,18 @@ protected def toMessageData (p : Profile) : MessageData :=
           node (displayRuleApplications p.ruleApplicationTotals)
   ]]]
   where
-    compareTimings : (x y : RuleProfileName × Nanos × Nanos) → Ordering :=
-      compareOpposite $
-        compareLexicographic
-          (compareOn (λ (_, s, f) => s + f))
-          (compareOn (λ (n, _, _) => n))
+    compareTimings (x y : RuleProfileName × Nanos × Nanos) : Ordering :=
+      compareLex
+        (compareOn (λ (_, s, f) => s + f))
+        (compareOn (λ (n, _, _) => n))
+        x y
+      |>.swap
 
     displayRuleApplications (apps : HashMap RuleProfileName (Nanos × Nanos)) :
         Array MessageData := Id.run do
-      let mut timings : Array (RuleProfileName × Nanos × Nanos) := #[]
-      for (n, (successful, failed)) in apps do
-        timings := timings.push (n, successful, failed)
-      timings := timings.qsortOrd (ord := ⟨compareTimings⟩)
+      let timings := apps.fold (init := Array.mkEmpty apps.size)
+        λ timings n (successful, failed) => timings.push (n, successful, failed)
+      let timings := timings.qsortOrd (ord := ⟨compareTimings⟩)
       let result := timings.map λ (n, s, f) =>
         m!"[{(s + f).printAsMillis} / {s.printAsMillis} / {f.printAsMillis}] {n}"
       return result

Aesop/Rule/Name.lean

@@ -109,9 +109,9 @@ instance : BEq RuleName where
     n₁.scope == n₂.scope && n₁.name == n₂.name
 
 protected def compare : (_ _ : RuleName) → Ordering :=
-  compareLexicographic (compareOn (·.builder)) $
-  compareLexicographic (compareOn (·.phase)) $
-  compareLexicographic (compareOn (·.scope)) $
+  compareLex (compareOn (·.builder)) $
+  compareLex (compareOn (·.phase)) $
+  compareLex (compareOn (·.scope)) $
   (λ n₁ n₂ => n₁.name.cmp n₂.name)
 
 protected def quickCompare (n₁ n₂ : RuleName) : Ordering :=

Aesop/RuleSet.lean

@@ -115,12 +115,12 @@ def merge (rs₁ rs₂ : RuleSet) : RuleSet where
   unsafeRules := rs₁.unsafeRules.merge rs₂.unsafeRules
   safeRules := rs₁.safeRules.merge rs₂.safeRules
   normSimpLemmaDescrs :=
-    rs₁.normSimpLemmaDescrs.merge rs₂.normSimpLemmaDescrs λ _ nsd₁ _ => nsd₁
+    rs₁.normSimpLemmaDescrs.mergeWith rs₂.normSimpLemmaDescrs λ _ nsd₁ _ => nsd₁
     -- We can merge left-biased here because `nsd₁` and `nsd₂` should be equal
     -- anyway.
   localNormSimpLemmas := rs₁.localNormSimpLemmas ++ rs₂.localNormSimpLemmas
   ruleNames :=
-    rs₁.ruleNames.merge rs₂.ruleNames λ _ ns₁ ns₂ =>
+    rs₁.ruleNames.mergeWith rs₂.ruleNames λ _ ns₁ ns₂ =>
       ns₁ ++ ns₂
   erased :=
     -- Add the erased rules from `rs₁` to `init`, except those rules which are

Aesop/Script.lean

@@ -7,6 +7,7 @@ Authors: Jannis Limperg
 import Aesop.Util
 import Std.Lean.Meta.Clear
 import Std.Lean.Meta.Inaccessible
+import Std.Lean.HashSet
 
 open Lean
 open Lean.Elab.Tactic

Aesop/Tree/UnsafeQueue.lean

@@ -6,6 +6,7 @@ Authors: Jannis Limperg
 
 import Aesop.Constants
 import Aesop.Rule
+import Std.Data.Array.Merge
 
 open Lean
 
@@ -45,8 +46,8 @@ def name : UnsafeQueueEntry → RuleName
   | postponedSafeRule r => r.rule.name
 
 instance : Ord UnsafeQueueEntry :=
-  ⟨ compareLexicographic
-      (compareOpposite $ compareOn successProbability)
+  ⟨ compareLex
+      (λ x y => compareOn successProbability x y |>.swap)
       (compareOn name) ⟩
 
 end UnsafeQueueEntry
@@ -70,7 +71,7 @@ def initial (postponedSafeRules : Array PostponedSafeRule)
   let postponedSafeRules :=
     postponedSafeRules.map .postponedSafeRule
       |>.qsort (λ x y => compare x y |>.isLT)
-  postponedSafeRules.mergeSortedFilteringDuplicates unsafeRules |>.toSubarray
+  postponedSafeRules.mergeSortedDeduplicating unsafeRules |>.toSubarray
 
 def entriesToMessageData (q : UnsafeQueue) : Array MessageData :=
   q.toArray.map toMessageData