From da69b1005699f7a32644435ea7fa06a32da191fb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Sep 2021 15:00:58 -0700
Subject: [PATCH] chore: cleanup

---
 src/Lean/Util/CollectFVars.lean       | 26 +++++++-------
 src/Lean/Util/CollectLevelParams.lean | 50 +++++++++++++++------------
 src/Lean/Util/CollectMVars.lean       | 28 ++++++++-------
 src/Lean/Util/FindLevelMVar.lean      | 47 ++++++++++++-------------
 src/Lean/Util/FindMVar.lean           | 25 +++++++-------
 5 files changed, 91 insertions(+), 85 deletions(-)

diff --git a/src/Lean/Util/CollectFVars.lean b/src/Lean/Util/CollectFVars.lean
index 296d1fd927..c59a0b276f 100644
--- a/src/Lean/Util/CollectFVars.lean
+++ b/src/Lean/Util/CollectFVars.lean
@@ -14,19 +14,21 @@ structure State where
 
 abbrev Visitor := State → State
 
-@[inline] def visit (f : Expr → Visitor) (e : Expr) : Visitor := fun s =>
-  if !e.hasFVar || s.visitedExpr.contains e then s
-  else f e { s with visitedExpr := s.visitedExpr.insert e }
+mutual
+  partial def visit (e : Expr) : Visitor := fun s =>
+    if !e.hasFVar || s.visitedExpr.contains e then s
+    else main e { s with visitedExpr := s.visitedExpr.insert e }
 
-partial def main : Expr → Visitor
-  | Expr.proj _ _ e _    => visit main e
-  | Expr.forallE _ d b _ => visit main b ∘ visit main d
-  | Expr.lam _ d b _     => visit main b ∘ visit main d
-  | Expr.letE _ t v b _  => visit main b ∘ visit main v ∘ visit main t
-  | Expr.app f a _       => visit main a ∘ visit main f
-  | Expr.mdata _ b _     => visit main b
-  | Expr.fvar fvarId _   => fun s => { s with fvarSet := s.fvarSet.insert fvarId }
-  | _                    => id
+  partial def main : Expr → Visitor
+    | Expr.proj _ _ e _    => visit e
+    | Expr.forallE _ d b _ => visit b ∘ visit d
+    | Expr.lam _ d b _     => visit b ∘ visit d
+    | Expr.letE _ t v b _  => visit b ∘ visit v ∘ visit t
+    | Expr.app f a _       => visit a ∘ visit f
+    | Expr.mdata _ b _     => visit b
+    | Expr.fvar fvarId _   => fun s => { s with fvarSet := s.fvarSet.insert fvarId }
+    | _                    => id
+end
 
 end CollectFVars
 
diff --git a/src/Lean/Util/CollectLevelParams.lean b/src/Lean/Util/CollectLevelParams.lean
index 667d80c920..590491592a 100644
--- a/src/Lean/Util/CollectLevelParams.lean
+++ b/src/Lean/Util/CollectLevelParams.lean
@@ -18,32 +18,36 @@ instance : Inhabited State := ⟨{}⟩
 
 abbrev Visitor := State → State
 
-@[inline] def visitLevel (f : Level → Visitor) (u : Level) : Visitor := fun s =>
-  if !u.hasParam || s.visitedLevel.contains u then s
-  else f u { s with visitedLevel := s.visitedLevel.insert u }
+mutual
+  partial def visitLevel (u : Level) : Visitor := fun s =>
+    if !u.hasParam || s.visitedLevel.contains u then s
+    else collect u { s with visitedLevel := s.visitedLevel.insert u }
 
-partial def collect : Level → Visitor
-  | Level.succ v _    => visitLevel collect v
-  | Level.max u v _   => visitLevel collect v ∘ visitLevel collect u
-  | Level.imax u v _  => visitLevel collect v ∘ visitLevel collect u
-  | Level.param n _   => fun s => { s with params := s.params.push n }
-  | _                 => id
+  partial def collect : Level → Visitor
+    | Level.succ v _    => visitLevel v
+    | Level.max u v _   => visitLevel v ∘ visitLevel u
+    | Level.imax u v _  => visitLevel v ∘ visitLevel u
+    | Level.param n _   => fun s => { s with params := s.params.push n }
+    | _                 => id
+end
 
-@[inline] def visitExpr (f : Expr → Visitor) (e : Expr) : Visitor := fun s =>
-  if !e.hasLevelParam then s
-  else if s.visitedExpr.contains e then s
-  else f e { s with visitedExpr := s.visitedExpr.insert e }
+mutual
+  partial def visitExpr (e : Expr) : Visitor := fun s =>
+    if !e.hasLevelParam then s
+    else if s.visitedExpr.contains e then s
+    else main e { s with visitedExpr := s.visitedExpr.insert e }
 
-partial def main : Expr → Visitor
-  | Expr.proj _ _ s _    => visitExpr main s
-  | Expr.forallE _ d b _ => visitExpr main b ∘ visitExpr main d
-  | Expr.lam _ d b _     => visitExpr main b ∘ visitExpr main d
-  | Expr.letE _ t v b _  => visitExpr main b ∘ visitExpr main v ∘ visitExpr main t
-  | Expr.app f a _       => visitExpr main a ∘ visitExpr main f
-  | Expr.mdata _ b _     => visitExpr main b
-  | Expr.const _ us _    => fun s => us.foldl (fun s u => visitLevel collect u s) s
-  | Expr.sort u _        => visitLevel collect u
-  | _                    => id
+  partial def main : Expr → Visitor
+    | Expr.proj _ _ s _    => visitExpr s
+    | Expr.forallE _ d b _ => visitExpr b ∘ visitExpr d
+    | Expr.lam _ d b _     => visitExpr b ∘ visitExpr d
+    | Expr.letE _ t v b _  => visitExpr b ∘ visitExpr v ∘ visitExpr t
+    | Expr.app f a _       => visitExpr a ∘ visitExpr f
+    | Expr.mdata _ b _     => visitExpr b
+    | Expr.const _ us _    => fun s => us.foldl (fun s u => visitLevel u s) s
+    | Expr.sort u _        => visitLevel u
+    | _                    => id
+end
 
 partial def State.getUnusedLevelParam (s : CollectLevelParams.State) (pre : Name := `v) : Level :=
   let v := mkLevelParam pre;
diff --git a/src/Lean/Util/CollectMVars.lean b/src/Lean/Util/CollectMVars.lean
index 250ef65112..58b1e10788 100644
--- a/src/Lean/Util/CollectMVars.lean
+++ b/src/Lean/Util/CollectMVars.lean
@@ -17,23 +17,25 @@ instance : Inhabited State := ⟨{}⟩
 
 abbrev Visitor := State → State
 
-@[inline] def visit (f : Expr → Visitor) (e : Expr) : Visitor := fun s =>
-  if !e.hasMVar || s.visitedExpr.contains e then s
-  else f e { s with visitedExpr := s.visitedExpr.insert e }
+mutual
+  partial def visit (e : Expr) : Visitor := fun s =>
+    if !e.hasMVar || s.visitedExpr.contains e then s
+    else main e { s with visitedExpr := s.visitedExpr.insert e }
 
-partial def main : Expr → Visitor
-  | Expr.proj _ _ e _    => visit main e
-  | Expr.forallE _ d b _ => visit main b ∘ visit main d
-  | Expr.lam _ d b _     => visit main b ∘ visit main d
-  | Expr.letE _ t v b _  => visit main b ∘ visit main v ∘ visit main t
-  | Expr.app f a _       => visit main a ∘ visit main f
-  | Expr.mdata _ b _     => visit main b
-  | Expr.mvar mvarId _   => fun s => { s with result := s.result.push mvarId }
-  | _                    => id
+  partial def main : Expr → Visitor
+    | Expr.proj _ _ e _    => visit e
+    | Expr.forallE _ d b _ => visit b ∘ visit d
+    | Expr.lam _ d b _     => visit b ∘ visit d
+    | Expr.letE _ t v b _  => visit b ∘ visit v ∘ visit t
+    | Expr.app f a _       => visit a ∘ visit f
+    | Expr.mdata _ b _     => visit b
+    | Expr.mvar mvarId _   => fun s => { s with result := s.result.push mvarId }
+    | _                    => id
+end
 
 end CollectMVars
 
 def Expr.collectMVars (s : CollectMVars.State) (e : Expr) : CollectMVars.State :=
-  CollectMVars.visit CollectMVars.main e s
+  CollectMVars.visit e s
 
 end Lean
diff --git a/src/Lean/Util/FindLevelMVar.lean b/src/Lean/Util/FindLevelMVar.lean
index e84186b7d3..291e8d2766 100644
--- a/src/Lean/Util/FindLevelMVar.lean
+++ b/src/Lean/Util/FindLevelMVar.lean
@@ -12,33 +12,32 @@ namespace FindLevelMVar
 abbrev Visitor := Option MVarId → Option MVarId
 
 mutual
-partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
-  if s.isSome || !e.hasLevelMVar then s else main p e s
+  partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
+    if s.isSome || !e.hasLevelMVar then s else main p e s
 
-@[specialize]
-partial def main (p : MVarId → Bool) : Expr → Visitor
-  | Expr.sort l _        => visitLevel p l
-  | Expr.const _ ls _    => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc
-  | Expr.forallE _ d b _ => visit p b ∘ visit p d
-  | Expr.lam _ d b _     => visit p b ∘ visit p d
-  | Expr.letE _ t v b _  => visit p b ∘ visit p v ∘ visit p t
-  | Expr.app f a _       => visit p a ∘ visit p f
-  | Expr.mdata _ b _     => visit p b
-  | Expr.proj _ _ e _    => visit p e
-  | _                    => id
+  @[specialize]
+  partial def main (p : MVarId → Bool) : Expr → Visitor
+    | Expr.sort l _        => visitLevel p l
+    | Expr.const _ ls _    => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc
+    | Expr.forallE _ d b _ => visit p b ∘ visit p d
+    | Expr.lam _ d b _     => visit p b ∘ visit p d
+    | Expr.letE _ t v b _  => visit p b ∘ visit p v ∘ visit p t
+    | Expr.app f a _       => visit p a ∘ visit p f
+    | Expr.mdata _ b _     => visit p b
+    | Expr.proj _ _ e _    => visit p e
+    | _                    => id
 
-partial def visitLevel (p : MVarId → Bool) (l : Level) : Visitor := fun s =>
-  if s.isSome || !l.hasMVar then s else mainLevel p l s
-
-@[specialize]
-partial def mainLevel (p : MVarId → Bool) : Level → Visitor
-  | Level.zero _        => id
-  | Level.succ l _      => visitLevel p l
-  | Level.max l₁ l₂ _   => visitLevel p l₁ ∘ visitLevel p l₂
-  | Level.imax l₁ l₂ _  => visitLevel p l₁ ∘ visitLevel p l₂
-  | Level.param n _     => id
-  | Level.mvar mvarId _ => fun s => if p mvarId then some mvarId else s
+  partial def visitLevel (p : MVarId → Bool) (l : Level) : Visitor := fun s =>
+    if s.isSome || !l.hasMVar then s else mainLevel p l s
 
+  @[specialize]
+  partial def mainLevel (p : MVarId → Bool) : Level → Visitor
+    | Level.zero _        => id
+    | Level.succ l _      => visitLevel p l
+    | Level.max l₁ l₂ _   => visitLevel p l₁ ∘ visitLevel p l₂
+    | Level.imax l₁ l₂ _  => visitLevel p l₁ ∘ visitLevel p l₂
+    | Level.param n _     => id
+    | Level.mvar mvarId _ => fun s => if p mvarId then some mvarId else s
 end
 
 end FindLevelMVar
diff --git a/src/Lean/Util/FindMVar.lean b/src/Lean/Util/FindMVar.lean
index 620e1cb735..4d18130a1f 100644
--- a/src/Lean/Util/FindMVar.lean
+++ b/src/Lean/Util/FindMVar.lean
@@ -12,20 +12,19 @@ namespace FindMVar
 abbrev Visitor := Option MVarId → Option MVarId
 
 mutual
-partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
-  if s.isSome || !e.hasMVar then s else main p e s
-
-@[specialize]
-partial def main (p : MVarId → Bool) : Expr → Visitor
-  | Expr.proj _ _ e _    => visit p e
-  | Expr.forallE _ d b _ => visit p b ∘ visit p d
-  | Expr.lam _ d b _     => visit p b ∘ visit p d
-  | Expr.letE _ t v b _  => visit p b ∘ visit p v ∘ visit p t
-  | Expr.app f a _       => visit p a ∘ visit p f
-  | Expr.mdata _ b _     => visit p b
-  | Expr.mvar mvarId _   => fun s => if s.isNone && p mvarId then some mvarId else s
-  | _                    => id
+  partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
+    if s.isSome || !e.hasMVar then s else main p e s
 
+  @[specialize]
+  partial def main (p : MVarId → Bool) : Expr → Visitor
+    | Expr.proj _ _ e _    => visit p e
+    | Expr.forallE _ d b _ => visit p b ∘ visit p d
+    | Expr.lam _ d b _     => visit p b ∘ visit p d
+    | Expr.letE _ t v b _  => visit p b ∘ visit p v ∘ visit p t
+    | Expr.app f a _       => visit p a ∘ visit p f
+    | Expr.mdata _ b _     => visit p b
+    | Expr.mvar mvarId _   => fun s => if s.isNone && p mvarId then some mvarId else s
+    | _                    => id
 end
 
 end FindMVar