chore: Consolidate local context extensions. (#403)

Std.lean

@@ -84,14 +84,14 @@ import Std.Lean.HashMap
 import Std.Lean.HashSet
 import Std.Lean.InfoTree
 import Std.Lean.Json
+import Std.Lean.LocalContext
 import Std.Lean.Meta.AssertHypotheses
 import Std.Lean.Meta.Basic
 import Std.Lean.Meta.Clear
 import Std.Lean.Meta.DiscrTree
 import Std.Lean.Meta.Expr
 import Std.Lean.Meta.Inaccessible
 import Std.Lean.Meta.InstantiateMVars
-import Std.Lean.Meta.LCtx
 import Std.Lean.Meta.SavedState
 import Std.Lean.Meta.Simp
 import Std.Lean.Meta.UnusedNames

Std/Lean/LocalContext.lean

@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2022 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro, Jannis Limperg
+-/
+import Lean.LocalContext
+
+namespace Lean
+
+/--
+Set the kind of a `LocalDecl`.
+-/
+def LocalDecl.setKind : LocalDecl → LocalDeclKind → LocalDecl
+  | cdecl index fvarId userName type bi _, kind =>
+      cdecl index fvarId userName type bi kind
+  | ldecl index fvarId userName type value nonDep _, kind =>
+      ldecl index fvarId userName type value nonDep kind
+
+namespace LocalContext
+
+/--
+Given an `FVarId`, this function returns the corresponding user name,
+but only if the name can be used to recover the original FVarId.
+-/
+def getRoundtrippingUserName? (lctx : LocalContext) (fvarId : FVarId) : Option Name := do
+  let ldecl₁ ← lctx.find? fvarId
+  let ldecl₂ ← lctx.findFromUserName? ldecl₁.userName
+  guard <| ldecl₁.fvarId == ldecl₂.fvarId
+  some ldecl₁.userName
+
+/--
+Set the kind of the given fvar.
+-/
+def setKind (lctx : LocalContext) (fvarId : FVarId)
+    (kind : LocalDeclKind) : LocalContext :=
+  lctx.modifyLocalDecl fvarId (·.setKind kind)
+
+/--
+Sort the given `FVarId`s by the order in which they appear in `lctx`. If any of
+the `FVarId`s do not appear in `lctx`, the result is unspecified.
+-/
+def sortFVarsByContextOrder (lctx : LocalContext) (hyps : Array FVarId) : Array FVarId :=
+  let hyps := hyps.map λ fvarId =>
+    match lctx.fvarIdToDecl.find? fvarId with
+    | none => (0, fvarId)
+    | some ldecl => (ldecl.index, fvarId)
+  hyps.qsort (λ h i => h.fst < i.fst) |>.map (·.snd)
+
+end LocalContext

Std/Lean/Meta/Basic.lean

@@ -4,45 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Jannis Limperg
 -/
 import Lean.Meta
+import Std.Lean.LocalContext
 
 open Lean Lean.Meta
 
 namespace Lean
 
-/--
-Set the kind of a `LocalDecl`.
--/
-def LocalDecl.setKind : LocalDecl → LocalDeclKind → LocalDecl
-  | cdecl index fvarId userName type bi _, kind =>
-      cdecl index fvarId userName type bi kind
-  | ldecl index fvarId userName type value nonDep _, kind =>
-      ldecl index fvarId userName type value nonDep kind
-
-
-namespace LocalContext
-
-/--
-Set the kind of the given fvar.
--/
-def setKind (lctx : LocalContext) (fvarId : FVarId)
-    (kind : LocalDeclKind) : LocalContext :=
-  lctx.modifyLocalDecl fvarId (·.setKind kind)
-
-/--
-Sort the given `FVarId`s by the order in which they appear in `lctx`. If any of
-the `FVarId`s do not appear in `lctx`, the result is unspecified.
--/
-def sortFVarsByContextOrder (lctx : LocalContext) (hyps : Array FVarId) :
-    Array FVarId :=
-  let hyps := hyps.map λ fvarId =>
-    match lctx.fvarIdToDecl.find? fvarId with
-    | none => (0, fvarId)
-    | some ldecl => (ldecl.index, fvarId)
-  hyps.qsort (λ h i => h.fst < i.fst) |>.map (·.snd)
-
-end LocalContext
-
-
 /--
 Sort the given `FVarId`s by the order in which they appear in the current local
 context. If any of the `FVarId`s do not appear in the current local context, the

Std/Tactic/Simpa.lean

@@ -6,7 +6,7 @@ Authors: Arthur Paulino, Gabriel Ebner, Mario Carneiro
 import Lean.Meta.Tactic.Assumption
 import Lean.Elab.Tactic.Simp
 import Lean.Linter.Util
-import Std.Lean.Meta.LCtx
+import Std.Lean.LocalContext
 import Std.Lean.Parser
 import Std.Tactic.OpenPrivate
 import Std.Tactic.TryThis