chore: move ShareCommon to Std

src/Init.lean

@@ -13,4 +13,3 @@ import Init.System
 import Init.Util
 import Init.Fix
 import Init.LeanInit
-import Init.ShareCommon

src/Lean/Data/Name.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-
+import Init.Data.HashSet -- TODO
 namespace Lean
 
 instance stringToName : HasCoe String Name :=

src/Lean/Data/SMap.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Init.Data.PersistentHashMap
 universes u v w w'
 
 namespace Lean

src/Lean/Elab/Definition.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
+import Std.ShareCommon
 import Lean.Util.CollectLevelParams
 import Lean.Util.FoldConsts
 import Lean.Util.CollectFVars
@@ -99,9 +100,9 @@ else withUsedWhen ref vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun var
   val  ← Term.levelMVarToParam val;
   type ← Term.instantiateMVars ref type;
   val  ← Term.instantiateMVars view.val val;
-  let shareCommonTypeVal : ShareCommonM (Expr × Expr) := do {
-    type ← withShareCommon type;
-    val  ← withShareCommon val;
+  let shareCommonTypeVal : Std.ShareCommonM (Expr × Expr) := do {
+    type ← Std.withShareCommon type;
+    val  ← Std.withShareCommon val;
     pure (type, val)
   };
   let (type, val) := shareCommonTypeVal.run;

src/Lean/Level.lean

@@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Init.Data.PersistentHashMap -- TODO
+import Init.Data.PersistentHashSet -- TODO
 import Lean.Data.Name
 import Lean.Data.Format
 

src/Lean/Util/Closure.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Std.ShareCommon
 import Lean.MetavarContext
 import Lean.Environment
 import Lean.Util.FoldConsts
@@ -148,9 +149,9 @@ structure MkClosureResult :=
 (exprClosure  : Array Expr)
 
 def mkClosure (mctx : MetavarContext) (lctx : LocalContext) (type : Expr) (value : Expr) : Except String MkClosureResult :=
-let shareCommonTypeValue : ShareCommonM (Expr × Expr) := do {
-  type  ← withShareCommon type;
-  value ← withShareCommon value;
+let shareCommonTypeValue : Std.ShareCommonM (Expr × Expr) := do {
+  type  ← Std.withShareCommon type;
+  value ← Std.withShareCommon value;
   pure (type, value)
 };
 let (type, value) := shareCommonTypeValue.run;

src/Std.lean

@@ -4,3 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Std.Data
+import Std.ShareCommon

src/Std/ShareCommon.lean

@@ -3,14 +3,10 @@ Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-prelude
-import Init.Util
-import Init.Data.HashMap
 import Init.Data.HashSet
-import Init.Data.PersistentHashSet
 import Init.Data.PersistentHashMap
-import Init.Control.State
-
+import Init.Data.PersistentHashSet
+namespace Std
 universes u v
 
 namespace ShareCommon
@@ -118,7 +114,7 @@ end ShareCommon
 class MonadShareCommon (m : Type u → Type v) :=
 (withShareCommon {α : Type u} : α → m α)
 
-export MonadShareCommon (withShareCommon)
+abbrev withShareCommon := @MonadShareCommon.withShareCommon
 
 abbrev shareCommonM {α : Type u} {m : Type u → Type v} [MonadShareCommon m] (a : α) : m α :=
 withShareCommon a
@@ -148,3 +144,5 @@ x.run' ShareCommon.PersistentState.empty
 
 def shareCommon {α} (a : α) : α :=
 (withShareCommon a : ShareCommonM α).run
+
+end Std