From 8b31db8e20ef5e31877615b1142160ba811b89a5 Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Thu, 28 Mar 2024 17:17:24 +0100
Subject: [PATCH] FVarIdSubst: eliminate Std.HashMap

... to reduce dependency on Std.
---
 Aesop/RuleTac/FVarIdSubst.lean | 11 ++++++-----
 Aesop/RuleTac/GoalDiff.lean    | 11 +----------
 Aesop/Util/Basic.lean          | 13 ++++++++++++-
 3 files changed, 19 insertions(+), 16 deletions(-)

diff --git a/Aesop/RuleTac/FVarIdSubst.lean b/Aesop/RuleTac/FVarIdSubst.lean
index afda8638..f79c8d28 100644
--- a/Aesop/RuleTac/FVarIdSubst.lean
+++ b/Aesop/RuleTac/FVarIdSubst.lean
@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg
 -/
 
-import Batteries.Data.HashMap
+import Lean
 
 open Lean Lean.Meta
 
 namespace Aesop
 
 structure FVarIdSubst where
-  map : Batteries.HashMap FVarId FVarId
+  map : HashMap FVarId FVarId
   deriving Inhabited
 
 namespace FVarIdSubst
@@ -53,15 +53,16 @@ instance : EmptyCollection FVarIdSubst :=
   ⟨.empty⟩
 
 def insert (s : FVarIdSubst) (old new : FVarId) : FVarIdSubst :=
-  let map : Batteries.HashMap _ _ := s.map.mapVal λ _ v =>
-    if v == old then new else v
+  let map : HashMap _ _ := s.map.fold (init := ∅) λ map k v =>
+    map.insert k $ if v == old then new else v
   ⟨map.insert old new⟩
 
 def erase (s : FVarIdSubst) (fvarId : FVarId) : FVarIdSubst :=
   ⟨s.map.erase fvarId⟩
 
 def append (s t : FVarIdSubst) : FVarIdSubst :=
-  let map := s.map.mapVal λ _ v => t.get v
+  let map : HashMap _ _ := s.map.fold (init := ∅) λ map k v =>
+    map.insert k $ t.get v
   ⟨t.map.fold (init := map) λ s k v => s.insert k v⟩
 
 def ofFVarSubstIgnoringNonFVarIds (s : FVarSubst) : FVarIdSubst := .mk $
diff --git a/Aesop/RuleTac/GoalDiff.lean b/Aesop/RuleTac/GoalDiff.lean
index d7d470d0..7e076f44 100644
--- a/Aesop/RuleTac/GoalDiff.lean
+++ b/Aesop/RuleTac/GoalDiff.lean
@@ -5,6 +5,7 @@ Authors: Jannis Limperg
 -/
 
 import Aesop.RuleTac.FVarIdSubst
+import Aesop.Util.Basic
 
 open Lean Lean.Meta
 
@@ -88,16 +89,6 @@ def diffGoals (old new : MVarId) (fvarSubst : FVarIdSubst) :
     fvarSubst
   }
 
--- TODO upstream
-local instance [BEq α] [Hashable α] [Monad m] :
-    ForM m (Batteries.HashMap α β) (α × β) where
-  forM | m, f => m.forM λ a b => f (a, b)
-
--- TODO upstream
-local instance [BEq α] [Hashable α] [Monad m] :
-    ForIn m (Batteries.HashMap α β) (α × β) where
-  forIn := ForM.forIn
-
 namespace GoalDiff
 
 /--
diff --git a/Aesop/Util/Basic.lean b/Aesop/Util/Basic.lean
index 77e6ef5d..95b78702 100644
--- a/Aesop/Util/Basic.lean
+++ b/Aesop/Util/Basic.lean
@@ -11,7 +11,7 @@ import Batteries.Data.String
 import Batteries.Lean.Expr
 import Batteries.Lean.Meta.DiscrTree
 import Batteries.Lean.PersistentHashSet
-import Lean.Meta.Tactic.TryThis
+import Lean
 
 open Lean
 open Lean.Meta Lean.Elab.Tactic
@@ -64,6 +64,17 @@ def toArray [BEq α] [Hashable α] (s : PersistentHashSet α) :
 
 end PersistentHashSet
 
+-- TODO upstream; generalise to {m : Type u → Type v}.
+-- Need to generalise `HashMap.forM` first.
+scoped instance {m : Type u → Type u} [BEq α] [Hashable α] [Monad m] :
+    ForM m (HashMap α β) (α × β) where
+  forM | m, f => m.forM λ a b => f (a, b)
+
+-- TODO upstream; generalise to {m : Type u → Type v}.
+scoped instance {m : Type u → Type u} [BEq α] [Hashable α] [Monad m] :
+    ForIn m (HashMap α β) (α × β) where
+  forIn := ForM.forIn
+
 section DiscrTree
 
 open DiscrTree