chore: upstream Std.Lean.LocalContext

src/Init/Data/Array/Basic.lean

@@ -21,21 +21,6 @@ def mkArray {α : Type u} (n : Nat) (v : α) : Array α := {
   data := List.replicate n v
 }
 
-/--
-`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
-```
-ofFn f = #[f 0, f 1, ... , f(n - 1)]
-``` -/
-def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
-  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
-  go (i : Nat) (acc : Array α) : Array α :=
-    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by n - i
-
-/-- The array `#[0, 1, ..., n - 1]`. -/
-def range (n : Nat) : Array Nat :=
-  n.fold (flip Array.push) (mkEmpty n)
-
 @[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
   List.length_replicate ..
 
@@ -428,10 +413,6 @@ def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :
 def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
   Id.run <| as.mapIdxM f
 
-/-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
-def zipWithIndex (arr : Array α) : Array (α × Nat) :=
-  arr.mapIdx fun i a => (a, i)
-
 @[inline]
 def find? {α : Type} (as : Array α) (p : α → Bool) : Option α :=
   Id.run <| as.findM? p
@@ -506,11 +487,6 @@ def elem [BEq α] (a : α) (as : Array α) : Bool :=
 def toList (as : Array α) : List α :=
   as.foldr List.cons []
 
-/-- Prepends an `Array α` onto the front of a list.  Equivalent to `as.toList ++ l`. -/
-@[inline]
-def toListAppend (as : Array α) (l : List α) : List α :=
-  as.foldr List.cons l
-
 instance {α : Type u} [Repr α] : Repr (Array α) where
   reprPrec a _ :=
     let _ : Std.ToFormat α := ⟨repr⟩
@@ -540,13 +516,6 @@ def concatMapM [Monad m] (f : α → m (Array β)) (as : Array α) : m (Array β
 def concatMap (f : α → Array β) (as : Array α) : Array β :=
   as.foldl (init := empty) fun bs a => bs ++ f a
 
-/-- Joins array of array into a single array.
-
-`flatten #[#[a₁, a₂, ⋯], #[b₁, b₂, ⋯], ⋯]` = `#[a₁, a₂, ⋯, b₁, b₂, ⋯]`
--/
-def flatten (as : Array (Array α)) : Array α :=
-  as.foldl (init := empty) fun r a => r ++ a
-
 end Array
 
 export Array (mkArray)

src/Lean/Data/Json.lean

@@ -8,4 +8,3 @@ import Lean.Data.Json.Stream
 import Lean.Data.Json.Printer
 import Lean.Data.Json.Parser
 import Lean.Data.Json.FromToJson
-import Lean.Data.Json.Elab

src/Lean/Data/Json/Elab.lean

@@ -1,79 +0,0 @@
-/-
- Copyright (c) 2022 E.W.Ayers. All rights reserved.
- Released under Apache 2.0 license as described in the file LICENSE.
- Authors: E.W.Ayers, Wojciech Nawrocki
--/
-import Lean.Data.Json.FromToJson
-import Lean.Syntax
-
-/-!
-# JSON-like syntax for Lean.
-
-Now you can write
-
-```lean
-open Lean.Json
-
-#eval json% {
-  hello : "world",
-  cheese : ["edam", "cheddar", {kind : "spicy", rank : 100.2}],
-  lemonCount : 100e30,
-  isCool : true,
-  isBug : null,
-  lookACalc: $(23 + 54 * 2)
-}
-```
--/
-
-namespace Lean.Json
-
-/-- Json syntactic category -/
-declare_syntax_cat json (behavior := symbol)
-/-- Json null value syntax. -/
-syntax "null" : json
-/-- Json true value syntax. -/
-syntax "true" : json
-/-- Json false value syntax. -/
-syntax "false" : json
-/-- Json string syntax. -/
-syntax str : json
-/-- Json number negation syntax for ordinary numbers. -/
-syntax "-"? num : json
-/-- Json number negation syntax for scientific numbers. -/
-syntax "-"? scientific : json
-/-- Json array syntax. -/
-syntax "[" json,* "]" : json
-/-- Json identifier syntax. -/
-syntax jsonIdent := ident <|> str
-/-- Json key/value syntax. -/
-syntax jsonField := jsonIdent ": " json
-/-- Json object syntax. -/
-syntax "{" jsonField,* "}" : json
-/-- Allows to use Json syntax in a Lean file. -/
-syntax "json% " json : term
-
-
-macro_rules
-  | `(json% null)           => `(Lean.Json.null)
-  | `(json% true)           => `(Lean.Json.bool Bool.true)
-  | `(json% false)          => `(Lean.Json.bool Bool.false)
-  | `(json% $n:str)         => `(Lean.Json.str $n)
-  | `(json% $n:num)         => `(Lean.Json.num $n)
-  | `(json% $n:scientific)  => `(Lean.Json.num $n)
-  | `(json% -$n:num)        => `(Lean.Json.num (-$n))
-  | `(json% -$n:scientific) => `(Lean.Json.num (-$n))
-  | `(json% [$[$xs],*])     => `(Lean.Json.arr #[$[json% $xs],*])
-  | `(json% {$[$ks:jsonIdent : $vs:json],*}) => do
-    let ks : Array (TSyntax `term) ← ks.mapM fun
-      | `(jsonIdent| $k:ident) => pure (k.getId |> toString |> quote)
-      | `(jsonIdent| $k:str)   => pure k
-      | _                     => Macro.throwUnsupported
-    `(Lean.Json.mkObj [$[($ks, json% $vs)],*])
-  | `(json% $stx)           =>
-    if stx.raw.isAntiquot then
-      let stx := ⟨stx.raw.getAntiquotTerm⟩
-      `(Lean.toJson $stx)
-    else
-      Macro.throwUnsupported
-
-end Lean.Json

src/Lean/LocalContext.lean

@@ -141,6 +141,15 @@ def hasExprMVar : LocalDecl → Bool
   | cdecl (type := t) ..              => t.hasExprMVar
   | ldecl (type := t) (value := v) .. => t.hasExprMVar || v.hasExprMVar
 
+/--
+Set the kind of a `LocalDecl`.
+-/
+def 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
+
 end LocalDecl
 
 /-- A LocalContext is an ordered set of local variable declarations.
@@ -311,6 +320,13 @@ def renameUserName (lctx : LocalContext) (fromName : Name) (toName : Name) : Loc
       { fvarIdToDecl := map.insert decl.fvarId decl
         decls        := decls.set decl.index decl }
 
+/--
+Set the kind of the given fvar.
+-/
+def setKind (lctx : LocalContext) (fvarId : FVarId)
+    (kind : LocalDeclKind) : LocalContext :=
+  lctx.modifyLocalDecl fvarId (·.setKind kind)
+
 def setBinderInfo (lctx : LocalContext) (fvarId : FVarId) (bi : BinderInfo) : LocalContext :=
   modifyLocalDecl lctx fvarId fun decl => decl.setBinderInfo bi
 
@@ -451,6 +467,27 @@ def sanitizeNames (lctx : LocalContext) : StateM NameSanitizerState LocalContext
             modify fun s => s.insert decl.userName
             pure lctx
 
+/--
+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
+
+/--
+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 fun fvarId =>
+    match lctx.fvarIdToDecl.find? fvarId with
+    | none => (0, fvarId)
+    | some ldecl => (ldecl.index, fvarId)
+  hyps.qsort (fun h i => h.fst < i.fst) |>.map (·.snd)
+
 end LocalContext
 
 /-- Class used to denote that `m` has a local context. -/

tests/lean/run/toFromJson.lean

@@ -2,13 +2,13 @@ import Lean
 
 open Lean
 
-declare_syntax_cat mjson
-syntax str : mjson
-syntax num : mjson
-syntax "{" (ident ": " mjson),* "}" : mjson
-syntax "[" mjson,* "]" : mjson
+declare_syntax_cat json
+syntax str : json
+syntax num : json
+syntax "{" (ident ": " json),* "}" : json
+syntax "[" json,* "]" : json
 
-syntax "json " mjson : term
+syntax "json " json : term
 
 /- declare a micro json parser, so we can write our tests in a more legible way. -/
 open Json in macro_rules