From d75c4e2101e09fdbe0ab52ee4ccfbf97dabc47b5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 6 Mar 2021 10:54:40 -0800
Subject: [PATCH] chore: cleanup

---
 src/Lean/CoreM.lean               | 10 ++++------
 src/Lean/Elab/SyntheticMVars.lean | 32 +++++++++++--------------------
 src/Lean/ResolveName.lean         |  7 ++++---
 3 files changed, 19 insertions(+), 30 deletions(-)

diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index b892e0f09c..eaa4c1827a 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -74,8 +74,7 @@ instance : MonadResolveName CoreM where
   getOpenDecls := return (← read).openDecls
 
 @[inline] def liftIOCore (x : IO α) : CoreM α := do
-  let ref ← getRef
-  IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x
+  IO.toEIO (fun (err : IO.Error) => Exception.error (← getRef) (toString err)) x
 
 instance : MonadLift IO CoreM where
   monadLift := liftIOCore
@@ -86,8 +85,7 @@ instance : MonadTrace CoreM where
 
 private def mkFreshNameImp (n : Name) : CoreM Name := do
   let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
-  let env ← getEnv
-  pure $ addMacroScope env.mainModule n fresh
+  return addMacroScope (← getEnv).mainModule n fresh
 
 def mkFreshUserName (n : Name) : CoreM Name :=
   mkFreshNameImp n
@@ -101,8 +99,8 @@ def mkFreshUserName (n : Name) : CoreM Name :=
 @[inline] def CoreM.toIO (x : CoreM α) (ctx : Context) (s : State) : IO (α × State) := do
   match (← (x.run { ctx with initHeartbeats := (← IO.getNumHeartbeats) } s).toIO') with
   | Except.error (Exception.error _ msg)   => do let e ← msg.toString; throw $ IO.userError e
-  | Except.error (Exception.internal id _) => throw $ IO.userError $ "internal exception #" ++ toString id.idx
-  | Except.ok a => pure a
+  | Except.error (Exception.internal id _) => throw <| IO.userError <| "internal exception #" ++ toString id.idx
+  | Except.ok a                            => return a
 
 instance [MetaEval α] : MetaEval (CoreM α) where
   eval env opts x _ := do
diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean
index be4c7bb0ce..e3ce64f753 100644
--- a/src/Lean/Elab/SyntheticMVars.lean
+++ b/src/Lean/Elab/SyntheticMVars.lean
@@ -90,10 +90,7 @@ private def synthesizePendingCoeInstMVar
         if (← occursCheck auxMVarId eNew) then
           assignExprMVar auxMVarId eNew
           return true
-        else
-          return false
-      else
-        return false
+      return false
     catch
       | Exception.error _ msg => throwTypeMismatchError errorMsgHeader? expectedType eType e f? msg
       | _                     => unreachable!
@@ -188,13 +185,11 @@ private def getSomeSynthethicMVarsRef : TermElabM Syntax := do
   | some mvarDecl => return mvarDecl.stx
   | none          => return Syntax.missing
 
-
 mutual
 
   partial def liftTacticElabM {α} (mvarId : MVarId) (x : TacticM α) : TermElabM α :=
     withMVarContext mvarId do
-      let s ← get
-      let savedSyntheticMVars := s.syntheticMVars
+      let savedSyntheticMVars := (← get).syntheticMVars
       modify fun s => { s with syntheticMVars := [] }
       try
         let a ← x.run' { main := mvarId } { goals := [mvarId] }
@@ -233,8 +228,7 @@ mutual
     let ctx ← read
     traceAtCmdPos `Elab.resuming fun _ =>
       m!"resuming synthetic metavariables, mayPostpone: {ctx.mayPostpone}, postponeOnError: {postponeOnError}"
-    let s ← get
-    let syntheticMVars    := s.syntheticMVars
+    let syntheticMVars    := (← get).syntheticMVars
     let numSyntheticMVars := syntheticMVars.length
     -- We reset `syntheticMVars` because new synthetic metavariables may be created by `synthesizeSyntheticMVar`.
     modify fun s => { s with syntheticMVars := [] }
@@ -262,11 +256,9 @@ mutual
     a "best option". If, after that, we still haven't made progress, we report "stuck" errors. -/
   partial def synthesizeSyntheticMVars (mayPostpone := true) : TermElabM Unit :=
     let rec loop (u : Unit) : TermElabM Unit := do
-      let ref ← getSomeSynthethicMVarsRef
-      withRef ref <| withIncRecDepth do
-        let s ← get
-        unless s.syntheticMVars.isEmpty do
-          if ← synthesizeSyntheticMVarsStep false false then
+      withRef (← getSomeSynthethicMVarsRef) <| withIncRecDepth do
+        unless (← get).syntheticMVars.isEmpty do
+          if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then
             loop ()
           else if !mayPostpone then
             /- Resume pending metavariables with "elaboration postponement" disabled.
@@ -285,13 +277,13 @@ mutual
                We the type of `x` may learn later its type and it may contain implicit and/or auto arguments.
                By disabling postponement, we are essentially giving up the opportunity of learning `x`s type
                and assume it does not have implict and/or auto arguments. -/
-            if ← withoutPostponing (synthesizeSyntheticMVarsStep true  false) then
+            if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := true) (runTactics := false) then
               loop ()
             else if ← synthesizeUsingDefault then
               loop ()
-            else if ← withoutPostponing (synthesizeSyntheticMVarsStep false false) then
+            else if ← withoutPostponing <| synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := false) then
               loop ()
-            else if ← synthesizeSyntheticMVarsStep false true then
+            else if ← synthesizeSyntheticMVarsStep (postponeOnError := false) (runTactics := true) then
               loop ()
             else
               reportStuckSyntheticMVars
@@ -312,8 +304,7 @@ def synthesizeSyntheticMVarsUsingDefault : TermElabM Unit := do
   synthesizeUsingDefaultLoop
 
 private partial def withSynthesizeImp {α} (k : TermElabM α) (mayPostpone : Bool) : TermElabM α := do
-  let s ← get
-  let syntheticMVarsSaved := s.syntheticMVars
+  let syntheticMVarsSaved := (← get).syntheticMVars
   modify fun s => { s with syntheticMVars := [] }
   try
     let a ← k
@@ -334,7 +325,6 @@ private partial def withSynthesizeImp {α} (k : TermElabM α) (mayPostpone : Boo
 /-- Elaborate `stx`, and make sure all pending synthetic metavariables created while elaborating `stx` are solved. -/
 def elabTermAndSynthesize (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr :=
   withRef stx do
-    let v ← withSynthesize <| elabTerm stx expectedType?
-    instantiateMVars v
+    instantiateMVars (← withSynthesize <| elabTerm stx expectedType?)
 
 end Lean.Elab.Term
diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean
index 9528d53b9e..5a5c40a16d 100644
--- a/src/Lean/ResolveName.lean
+++ b/src/Lean/ResolveName.lean
@@ -93,8 +93,9 @@ private def resolveOpenDecls (env : Environment) (id : Name) : List OpenDecl →
 def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl) (id : Name) : List (Name × List String) :=
   -- decode macro scopes from name before recursion
   let extractionResult := extractMacroScopes id
-  let rec loop : Name → List String → List (Name × List String)
-    | id@(Name.str p s _), projs =>
+  let rec loop (id : Name) (projs : List String) : List (Name × List String) :=
+    match id with
+    | Name.str p s _ =>
       -- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
       let id := { extractionResult with name := id }.review
       match resolveUsingNamespace env id ns with
@@ -111,7 +112,7 @@ def resolveGlobalName (env : Environment) (ns : Name) (openDecls : List OpenDecl
           match resolvedIds with
           | _ :: _ => resolvedIds.eraseDups.map fun id => (id, projs)
           | []     => loop p (s::projs)
-    | _, _ => []
+    | _ => []
   loop extractionResult.name []
 
 /- Namespace resolution -/