/-
Copyright (c) 2022 Arthur Paulino. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Arthur Paulino, Jannis Limperg
-/

import Mathlib.Lean.Expr.Basic

/-!
# Miscellaneous helper functions for tactics.

[TODO] Ideally we would find good homes for everything in this file, eventually removing it.
-/

namespace Mathlib.Tactic

open Lean Meta Elab Tactic

variable [Monad: (Type ?u.365 → Type ?u.364) → Type (max(?u.365+1)?u.364)
Monad m: ?m.5
m]

/--
`modifyMetavarDecl mvarId f` updates the `MetavarDecl` for `mvarId` with `f`.
Conditions on `f`:

- The target of `f mdecl` is defeq to the target of `mdecl`.
- The local context of `f mdecl` must contain the same fvars as the local
  context of `mdecl`. For each fvar in the local context of `f mdecl`, the type
  (and value, if any) of the fvar must be defeq to the corresponding fvar in
  the local context of `mdecl`.

If `mvarId` does not refer to a declared metavariable, nothing happens.
-/
def modifyMetavarDecl: {m : Type → Type} → [inst : MonadMCtx m] → MVarId → (MetavarDecl → MetavarDecl) → m Unit
modifyMetavarDecl [MonadMCtx: (Type → Type) → Type
MonadMCtx m: ?m.16
m] (mvarId: MVarId
mvarId : MVarId: Type
MVarId)
    (f: MetavarDecl → MetavarDecl
f : MetavarDecl: Type
MetavarDecl → MetavarDecl: Type
MetavarDecl) : m: ?m.16
m Unit: Type
Unit := do
  modifyMCtx: {m : Type → Type} → [self : MonadMCtx m] → (MetavarContext → MetavarContext) → m Unit
modifyMCtx λ mctx: ?m.63
mctx =>
    match mctx: ?m.63
mctx.decls: MetavarContext → PersistentHashMap MVarId MetavarDecl
decls.find?: {α : Type ?u.66} → {β : Type ?u.65} → {x : BEq α} → {x_1 : Hashable α} → PersistentHashMap α β → α → Option β
find? mvarId: MVarId
mvarId with
    | none: {α : Type ?u.85} → Option α
none => mctx: ?m.63
mctx
    | some: {α : Type ?u.94} → α → Option α
some mdecl: MetavarDecl
mdecl => { mctx: ?m.63
mctx with decls := mctx: ?m.63
mctx.decls: MetavarContext → PersistentHashMap MVarId MetavarDecl
decls.insert: {α : Type ?u.109} →
  {β : Type ?u.108} → {x : BEq α} → {x_1 : Hashable α} → PersistentHashMap α β → α → β → PersistentHashMap α β
insert mvarId: MVarId
mvarId (f: MetavarDecl → MetavarDecl
f mdecl: MetavarDecl
mdecl) }

/--
`modifyTarget mvarId f` updates the target of the metavariable `mvarId` with
`f`. For any `e`, `f e` must be defeq to `e`. If `mvarId` does not refer to
a declared metvariable, nothing happens.
-/
def modifyTarget: [inst : MonadMCtx m] → MVarId → (Expr → Expr) → m Unit
modifyTarget [MonadMCtx: (Type → Type) → Type
MonadMCtx m: ?m.361
m] (mvarId: MVarId
mvarId : MVarId: Type
MVarId) (f: Expr → Expr
f : Expr: Type
Expr → Expr: Type
Expr) : m: ?m.361
m Unit: Type
Unit :=
  modifyMetavarDecl: {m : Type → Type} → [inst : MonadMCtx m] → MVarId → (MetavarDecl → MetavarDecl) → m Unit
modifyMetavarDecl mvarId: MVarId
mvarId fun mdecl: ?m.389
mdecl ↦
    { mdecl: ?m.389
mdecl with type := f: Expr → Expr
f mdecl: ?m.389
mdecl.type: MetavarDecl → Expr
type }

/--
`modifyLocalContext mvarId f` updates the local context of the metavariable
`mvarId` with `f`. The new local context must contain the same fvars as the old
local context and the types (and values, if any) of the fvars in the new local
context must be defeq to their equivalents in the old local context.

If `mvarId` does not refer to a declared metavariable, nothing happens.
-/
def modifyLocalContext: {m : Type → Type} → [inst : MonadMCtx m] → MVarId → (LocalContext → LocalContext) → m Unit
modifyLocalContext [MonadMCtx: (Type → Type) → Type
MonadMCtx m: ?m.497
m] (mvarId: MVarId
mvarId : MVarId: Type
MVarId)
    (f: LocalContext → LocalContext
f : LocalContext: Type
LocalContext → LocalContext: Type
LocalContext) : m: ?m.497
m Unit: Type
Unit :=
  modifyMetavarDecl: {m : Type → Type} → [inst : MonadMCtx m] → MVarId → (MetavarDecl → MetavarDecl) → m Unit
modifyMetavarDecl mvarId: MVarId
mvarId fun mdecl: ?m.525
mdecl ↦
    { mdecl: ?m.525
mdecl with lctx := f: LocalContext → LocalContext
f mdecl: ?m.525
mdecl.lctx: MetavarDecl → LocalContext
lctx }

/--
`modifyLocalDecl mvarId fvarId f` updates the local decl `fvarId` in the local
context of `mvarId` with `f`. `f` must leave the `fvarId` and `index` of the
`LocalDecl` unchanged. The type of the new `LocalDecl` must be defeq to the type
of the old `LocalDecl` (and the same applies to the value of the `LocalDecl`, if
any).

If `mvarId` does not refer to a declared metavariable or if `fvarId` does not
exist in the local context of `mvarId`, nothing happens.
-/
def modifyLocalDecl: [inst : MonadMCtx m] → MVarId → FVarId → (LocalDecl → LocalDecl) → m Unit
modifyLocalDecl [MonadMCtx: (Type → Type) → Type
MonadMCtx m: ?m.625
m] (mvarId: MVarId
mvarId : MVarId: Type
MVarId) (fvarId: FVarId
fvarId : FVarId: Type
FVarId)
    (f: LocalDecl → LocalDecl
f : LocalDecl: Type
LocalDecl → LocalDecl: Type
LocalDecl) : m: ?m.625
m Unit: Type
Unit :=
  modifyLocalContext: {m : Type → Type} → [inst : MonadMCtx m] → MVarId → (LocalContext → LocalContext) → m Unit
modifyLocalContext mvarId: MVarId
mvarId fun lctx: ?m.656
lctx ↦ lctx: ?m.656
lctx.modifyLocalDecl: LocalContext → FVarId → (LocalDecl → LocalDecl) → LocalContext
modifyLocalDecl fvarId: FVarId
fvarId f: LocalDecl → LocalDecl
f