From bb80875bb831670f1f0039ac1322ccf01710c03e Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Fri, 9 Aug 2024 10:44:32 +1000
Subject: [PATCH] chore: adaptations for nightly-2024-08-08 (#48)

---
 Qq/AssertInstancesCommute.lean |  2 +-
 Qq/Delab.lean                  |  2 +-
 Qq/Macro.lean                  | 20 ++++++++++----------
 lean-toolchain                 |  2 +-
 4 files changed, 13 insertions(+), 13 deletions(-)

diff --git a/Qq/AssertInstancesCommute.lean b/Qq/AssertInstancesCommute.lean
index a9b2ad8..b609849 100644
--- a/Qq/AssertInstancesCommute.lean
+++ b/Qq/AssertInstancesCommute.lean
@@ -17,7 +17,7 @@ def isRedundantLocalInst? (inst : FVarId) : MetaM (Option Expr) := do
 
 def findRedundantLocalInst? : QuoteM (Option (FVarId × Expr)) := do
   for {fvar, ..} in ← withUnquotedLCtx getLocalInstances do
-    if let some (.quoted (.fvar quotedFVar)) := (← read).exprBackSubst.find? fvar then
+    if let some (.quoted (.fvar quotedFVar)) := (← read).exprBackSubst[fvar]? then
       if (← quotedFVar.getDecl).hasValue then continue
       if let some result ← withUnquotedLCtx do isRedundantLocalInst? fvar.fvarId! then
         return (fvar.fvarId!, result)
diff --git a/Qq/Delab.lean b/Qq/Delab.lean
index 96e9c74..565abf0 100644
--- a/Qq/Delab.lean
+++ b/Qq/Delab.lean
@@ -51,7 +51,7 @@ def withDelabQuoted (k : StateT UnquoteState DelabM Term) : Delab :=
   let showNested := `pp.qq._nested
   if (← getOptions).get showNested true then
     for fv in (← get).abstractedFVars.reverse do
-      if let some (.quoted expr) := (← get).exprBackSubst.find? (.fvar fv) then
+      if let some (.quoted expr) := (← get).exprBackSubst[Expr.fvar fv]? then
       if let some decl := (← get).unquoted.find? fv then
       if (res.1.find? (·.getId == decl.userName)).isSome then
       if let some name := removeDollar decl.userName then
diff --git a/Qq/Macro.lean b/Qq/Macro.lean
index 070502a..cf33967 100644
--- a/Qq/Macro.lean
+++ b/Qq/Macro.lean
@@ -32,19 +32,19 @@ structure UnquoteState where
   mvars : List (Expr × MVarSynth) := []
 
   /-- Maps quoted expressions (of type Level) in the old context to level parameter names in the new context -/
-  levelSubst : HashMap Expr Level := {}
+  levelSubst : Std.HashMap Expr Level := {}
 
   /-- Maps quoted expressions (of type Expr) in the old context to expressions in the new context -/
-  exprSubst : HashMap Expr Expr := {}
+  exprSubst : Std.HashMap Expr Expr := {}
 
   /-- New unquoted local context -/
   unquoted := LocalContext.empty
 
   /-- Maps free variables in the new context to expressions in the old context (of type Expr) -/
-  exprBackSubst : HashMap Expr ExprBackSubstResult := {}
+  exprBackSubst : Std.HashMap Expr ExprBackSubstResult := {}
 
   /-- Maps free variables in the new context to levels in the old context (of type Level) -/
-  levelBackSubst : HashMap Level Expr := {}
+  levelBackSubst : Std.HashMap Level Expr := {}
 
   /-- New free variables in the new context that were newly introduced for irreducible expressions. -/
   abstractedFVars : Array FVarId := #[]
@@ -133,7 +133,7 @@ mutual
 
 partial def unquoteLevel (e : Expr) : UnquoteM Level := do
   let e ← whnf e
-  if let some l := (← get).levelSubst.find? e then
+  if let some l := (← get).levelSubst[e]? then
     return l
   if e.isAppOfArity ``Level.zero 0 then pure .zero
   else if e.isAppOfArity ``Level.succ 1 then return .succ (← unquoteLevel (e.getArg! 0))
@@ -236,7 +236,7 @@ partial def unquoteExpr (e : Expr) : UnquoteM Expr := do
   let e ← instantiateMVars (← whnf e)
   let eTy ← whnfR (← inferType e)
   if eTy.isAppOfArity ``Quoted 1 then
-    if let some e' := (← get).exprSubst.find? e then
+    if let some e' := (← get).exprSubst[e]? then
       return e'
     if ← isAssignablePattern e then
       return ← unquoteExprMVar e
@@ -359,13 +359,13 @@ def quoteLevel : Level → QuoteM Expr
   | .zero => return .const ``Level.zero []
   | .succ u => return mkApp (.const ``Level.succ []) (← quoteLevel u)
   | l@(.mvar ..) => do
-    if let some e := (← read).levelBackSubst.find? l then
+    if let some e := (← read).levelBackSubst[l]? then
       return e
     throwError "cannot quote level mvar {l}"
   | .max a b => return mkApp2 (.const ``Level.max []) (← quoteLevel a) (← quoteLevel b)
   | .imax a b => return mkApp2 (.const ``Level.imax []) (← quoteLevel a) (← quoteLevel b)
   | l@(.param n) => do
-    match (← read).levelBackSubst.find? l with
+    match (← read).levelBackSubst[l]? with
       | some e => return e
       | none =>
         match ← isLevelFVar n with
@@ -382,12 +382,12 @@ def quoteLevelList : List Level → QuoteM Expr
 partial def quoteExpr : Expr → QuoteM Expr
   | .bvar i => return mkApp (.const ``Expr.bvar []) (toExpr i)
   | e@(.fvar ..) => do
-    let some r := (← read).exprBackSubst.find? e | throwError "unknown free variable {e}"
+    let some r := (← read).exprBackSubst[e]? | throwError "unknown free variable {e}"
     match r with
     | .quoted r => return r
     | .unquoted r => quoteExpr r
   | e@(.mvar ..) => do
-    if let some (.quoted r) := (← read).exprBackSubst.find? e then return r
+    if let some (.quoted r) := (← read).exprBackSubst[e]? then return r
     throwError "resulting term contains metavariable {e}"
   | .sort u => return mkApp (.const ``Expr.sort []) (← quoteLevel u)
   | .const n ls => return mkApp2 (.const ``Expr.const []) (toExpr n) (← quoteLevelList ls)
diff --git a/lean-toolchain b/lean-toolchain
index 7f0ea50..9f6eaf7 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.10.0
+leanprover/lean4:nightly-2024-08-08