chore: cleanup

src/Lean/Meta/LevelDefEq.lean

@@ -9,28 +9,28 @@ import Lean.Meta.InferType
 namespace Lean.Meta
 
 private partial def decAux? : Level → MetaM (Option Level)
-  | Level.zero _        => pure none
-  | Level.param _ _     => pure none
+  | Level.zero _        => return none
+  | Level.param _ _     => return none
   | Level.mvar mvarId _ => do
     let mctx ← getMCtx
     match mctx.getLevelAssignment? mvarId with
     | some u => decAux? u
     | none   =>
       if (← isReadOnlyLevelMVar mvarId) then
-        pure none
+        return none
       else
         let u ← mkFreshLevelMVar
         assignLevelMVar mvarId (mkLevelSucc u)
-        pure u
-  | Level.succ u _  => pure u
+        return u
+  | Level.succ u _  => return u
   | u =>
     let process (u v : Level) : MetaM (Option Level) := do
       match (← decAux? u) with
-      | none   => pure none
+      | none   => return none
       | some u => do
         match (← decAux? v) with
-        | none   => pure none
-        | some v => pure $ mkLevelMax' u v
+        | none   => return none
+        | some v => return mkLevelMax' u v
     match u with
     | Level.max u v _  => process u v
     /- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`. -/
@@ -40,22 +40,21 @@ private partial def decAux? : Level → MetaM (Option Level)
 def decLevel? (u : Level) : MetaM (Option Level) := do
   let mctx ← getMCtx
   match (← decAux? u) with
-  | some v => pure $ some v
+  | some v => return some v
   | none   => do
     modify fun s => { s with mctx := mctx }
-    pure none
+    return none
 
 def decLevel (u : Level) : MetaM Level := do
   match (← decLevel? u) with
-  | some u => pure u
+  | some u => return u
   | none   => throwError! "invalid universe level, {u} is not greater than 0"
 
 /- This method is useful for inferring universe level parameters for function that take arguments such as `{α : Type u}`.
    Recall that `Type u` is `Sort (u+1)` in Lean. Thus, given `α`, we must infer its universe level,
    and then decrement 1 to obtain `u`. -/
 def getDecLevel (type : Expr) : MetaM Level := do
-  let u ← getLevel type
-  decLevel u
+  decLevel (← getLevel type)
 
 private def strictOccursMaxAux (lvl : Level) : Level → Bool
   | Level.max u v _ => strictOccursMaxAux lvl u || strictOccursMaxAux lvl v
@@ -70,7 +69,7 @@ private def strictOccursMax (lvl : Level) : Level → Bool
 
 /-- `mkMaxArgsDiff mvarId (max u_1 ... (mvar mvarId) ... u_n) v` => `max v u_1 ... u_n` -/
 private def mkMaxArgsDiff (mvarId : MVarId) : Level → Level → Level
-  | Level.max u v _,     acc => mkMaxArgsDiff mvarId v $ mkMaxArgsDiff mvarId u acc
+  | Level.max u v _,     acc => mkMaxArgsDiff mvarId v <| mkMaxArgsDiff mvarId u acc
   | l@(Level.mvar id _), acc => if id != mvarId then mkLevelMax' acc l else acc
   | l,                   acc => mkLevelMax' acc l
 
@@ -79,84 +78,86 @@ private def mkMaxArgsDiff (mvarId : MVarId) : Level → Level → Level
   and assigning `?m := max ?n v` -/
 private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit := do
   let n ← mkFreshLevelMVar
-  assignLevelMVar mvarId $ mkMaxArgsDiff mvarId v n
+  assignLevelMVar mvarId <| mkMaxArgsDiff mvarId v n
 
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit :=
   modifyPostponed fun postponed => postponed.push { lhs := lhs, rhs := rhs }
 
 mutual
-private partial def solve (u v : Level) : MetaM LBool := do
-  match u, v with
-  | Level.mvar mvarId _, _ =>
-    if (← isReadOnlyLevelMVar mvarId) then
-      pure LBool.undef
-    else if !u.occurs v then
-      assignLevelMVar u.mvarId! v
-      pure LBool.true
-    else if !strictOccursMax u v then
-      solveSelfMax u.mvarId! v
-      pure LBool.true
-    else
-      pure LBool.undef
-  | Level.zero _, Level.max v₁ v₂ _ =>
-    Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂)
-  | Level.zero _, Level.imax _ v₂ _ =>
-    Bool.toLBool <$> isLevelDefEqAux levelZero v₂
-  | Level.zero _, Level.succ .. => pure LBool.false
-  | Level.succ u _, v =>
-    match (← Meta.decLevel? v) with
-    | some v => Bool.toLBool <$> isLevelDefEqAux u v
-    | none   => pure LBool.undef
-  | _, _ => pure LBool.undef
 
-partial def isLevelDefEqAux : Level → Level → MetaM Bool
-  | Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs
-  | lhs, rhs => do
-    if lhs == rhs then
-      pure true
-    else
-      trace[Meta.isLevelDefEq.step]! "{lhs} =?= {rhs}"
-      let lhs' ← instantiateLevelMVars lhs
-      let lhs' := lhs'.normalize
-      let rhs' ← instantiateLevelMVars rhs
-      let rhs' := rhs'.normalize
-      if lhs != lhs' || rhs != rhs' then
-        isLevelDefEqAux lhs' rhs'
+  private partial def solve (u v : Level) : MetaM LBool := do
+    match u, v with
+    | Level.mvar mvarId _, _ =>
+      if (← isReadOnlyLevelMVar mvarId) then
+        return LBool.undef
+      else if !u.occurs v then
+        assignLevelMVar u.mvarId! v
+        return LBool.true
+      else if !strictOccursMax u v then
+        solveSelfMax u.mvarId! v
+        return LBool.true
       else
-        let r ← solve lhs rhs;
-        if r != LBool.undef then
-          pure $ r == LBool.true
+        return LBool.undef
+    | Level.zero _, Level.max v₁ v₂ _ =>
+      Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂)
+    | Level.zero _, Level.imax _ v₂ _ =>
+      Bool.toLBool <$> isLevelDefEqAux levelZero v₂
+    | Level.zero _, Level.succ .. => return LBool.false
+    | Level.succ u _, v =>
+      match (← Meta.decLevel? v) with
+      | some v => Bool.toLBool <$> isLevelDefEqAux u v
+      | none   => return LBool.undef
+    | _, _ => return LBool.undef
+
+  partial def isLevelDefEqAux : Level → Level → MetaM Bool
+    | Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs
+    | lhs, rhs => do
+      if lhs == rhs then
+        return true
+      else
+        trace[Meta.isLevelDefEq.step]! "{lhs} =?= {rhs}"
+        let lhs' ← instantiateLevelMVars lhs
+        let lhs' := lhs'.normalize
+        let rhs' ← instantiateLevelMVars rhs
+        let rhs' := rhs'.normalize
+        if lhs != lhs' || rhs != rhs' then
+          isLevelDefEqAux lhs' rhs'
         else
-          let r ← solve rhs lhs;
+          let r ← solve lhs rhs;
           if r != LBool.undef then
-            pure $ r == LBool.true
-          else do
-            let mctx ← getMCtx
-            if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then
-              let ctx ← read
-              if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
-                trace[Meta.isLevelDefEq.stuck]! "{lhs} =?= {rhs}"
-                Meta.throwIsDefEqStuck
+            return r == LBool.true
+          else
+            let r ← solve rhs lhs;
+            if r != LBool.undef then
+              return r == LBool.true
+            else do
+              let mctx ← getMCtx
+              if !mctx.hasAssignableLevelMVar lhs && !mctx.hasAssignableLevelMVar rhs then
+                let ctx ← read
+                if ctx.config.isDefEqStuckEx && (lhs.isMVar || rhs.isMVar) then do
+                  trace[Meta.isLevelDefEq.stuck]! "{lhs} =?= {rhs}"
+                  Meta.throwIsDefEqStuck
+                else
+                  return false
               else
-                pure false
-            else
-              postponeIsLevelDefEq lhs rhs; pure true
+                postponeIsLevelDefEq lhs rhs
+                return true
 end
 
 def isListLevelDefEqAux : List Level → List Level → MetaM Bool
-  | [],    []    => pure true
+  | [],    []    => return true
   | u::us, v::vs => isLevelDefEqAux u v <&&> isListLevelDefEqAux us vs
-  | _,     _     => pure false
+  | _,     _     => return false
 
 private def getNumPostponed : MetaM Nat := do
-  pure (← getPostponed).size
+  return (← getPostponed).size
 
 open Std (PersistentArray)
 
 private def getResetPostponed : MetaM (PersistentArray PostponedEntry) := do
   let ps ← getPostponed
   setPostponed {}
-  pure ps
+  return ps
 
 private def processPostponedStep : MetaM Bool :=
   traceCtx `Meta.isLevelDefEq.postponed.step do
@@ -168,26 +169,26 @@ private def processPostponedStep : MetaM Bool :=
 
 private partial def processPostponed (mayPostpone : Bool := true) : MetaM Bool := do
 if (← getNumPostponed) == 0 then
-  pure true
+  return true
 else
   traceCtx `Meta.isLevelDefEq.postponed do
     let rec loop : MetaM Bool := do
       let numPostponed ← getNumPostponed
       if numPostponed == 0 then
-        pure true
+        return true
       else
         trace[Meta.isLevelDefEq.postponed]! "processing #{numPostponed} postponed is-def-eq level constraints"
         if !(← processPostponedStep) then
-          pure false
+          return false
         else
           let numPostponed' ← getNumPostponed
           if numPostponed' == 0 then
-            pure true
+            return true
           else if numPostponed' < numPostponed then
             loop
           else
             trace[Meta.isLevelDefEq.postponed]! "no progress solving pending is-def-eq level constraints"
-            pure mayPostpone
+            return mayPostpone
     loop
 
 private def restore (env : Environment) (mctx : MetavarContext) (postponed : PersistentArray PostponedEntry) : MetaM Unit := do
@@ -208,13 +209,13 @@ private def restore (env : Environment) (mctx : MetavarContext) (postponed : Per
   try
     if (← x) then
       if (← processPostponed mayPostpone) then
-        pure true
+        return true
       else
         restore env mctx postponed
-        pure false
+        return false
     else
       restore env mctx postponed
-      pure false
+      return false
   catch ex =>
     restore env mctx postponed
     throw ex
@@ -223,7 +224,7 @@ private def postponedToMessageData (ps : PersistentArray PostponedEntry) : Messa
   let mut r := MessageData.nil
   for p in ps do
     r := m!"{r}\n{p.lhs} =?= {p.rhs}"
-  pure r
+  return r
 
 @[specialize] def withoutPostponingUniverseConstraintsImp {α} (x : MetaM α) : MetaM α := do
   let postponed ← getResetPostponed
@@ -232,31 +233,31 @@ private def postponedToMessageData (ps : PersistentArray PostponedEntry) : Messa
     unless (← processPostponed (mayPostpone := false)) do
       throwError! "stuck at solving universe constraints{MessageData.nestD (postponedToMessageData (← getPostponed))}"
     setPostponed postponed
-    pure a
+    return a
   catch ex =>
     setPostponed postponed
     throw ex
 
 @[inline] def withoutPostponingUniverseConstraints {α m} [MonadControlT MetaM m] [Monad m] : m α → m α :=
-  mapMetaM $ withoutPostponingUniverseConstraintsImp
+  mapMetaM <| withoutPostponingUniverseConstraintsImp
 
 def isLevelDefEq (u v : Level) : MetaM Bool :=
   traceCtx `Meta.isLevelDefEq do
-    let b ← commitWhen (mayPostpone := true) $ Meta.isLevelDefEqAux u v
+    let b ← commitWhen (mayPostpone := true) <| Meta.isLevelDefEqAux u v
     trace[Meta.isLevelDefEq]! "{u} =?= {v} ... {if b then "success" else "failure"}"
-    pure b
+    return b
 
 def isExprDefEq (t s : Expr) : MetaM Bool :=
   traceCtx `Meta.isDefEq do
-    let b ← commitWhen (mayPostpone := true) $ Meta.isExprDefEqAux t s
+    let b ← commitWhen (mayPostpone := true) <| Meta.isExprDefEqAux t s
     trace[Meta.isDefEq]! "{t} =?= {s} ... {if b then "success" else "failure"}"
-    pure b
+    return b
 
 abbrev isDefEq (t s : Expr) : MetaM Bool :=
   isExprDefEq t s
 
 def isExprDefEqGuarded (a b : Expr) : MetaM Bool := do
-  try isExprDefEq a b catch _ => pure false
+  try isExprDefEq a b catch _ => return false
 
 abbrev isDefEqGuarded (t s : Expr) : MetaM Bool :=
   isExprDefEqGuarded t s