Parsing expression in the context of a goal

Stream: lean4

[Leni Aniva]

Programatically, how can I parse an expression that refers to variables in the local context? For example, suppose the goal (with a TermElabM context and MVarId looks like this:

p q : Prop
h : p
⊢ (p ∨ q) ∨ p ∨ q

and I want to type the expression Or.inl h. It seems like its not sufficient to restore the TermElabM context and then run Lean.Elab.Term.elabTerm:

state.term.restore
let expr <- Elab.Term.elabTerm stx
...

Below is a MWE showing what I want to do. The program crashes when the expression Or.inl h is elaborated.

import Lean

open Lean

def filename := "<example>"

structure Context where
  env: Environment
  coreContext : Core.Context := {
    currNamespace := Name.anonymous,
    openDecls := [],
    fileName := "<stdin>",
    fileMap := { source := "", positions := #[0] }
  }
  elabContext : Elab.Term.Context := {
    declName? := .none,
    errToSorry := false
  }

abbrev M (m: Type → Type) := ReaderT Context m

def parse_expr (s: String): Elab.TermElabM Lean.Expr := do
  let syn := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := s)
    (fileName := filename) |>.toOption |>.get!
  let expr ← Elab.Term.elabType syn
  Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let expr ← instantiateMVars expr
  return expr

def start_tactic_state (expr: Expr): Elab.TermElabM Elab.Tactic.SavedState := do
  let mvar ← Meta.mkFreshExprMVar (some expr) (kind := .synthetic)
  let termState : Elab.Term.SavedState ← Elab.Term.saveState
  let tacticState : Elab.Tactic.SavedState := { term := termState, tactic := { goals := [mvar.mvarId!] }}
  IO.println "Tactic state started"
  return tacticState

def execute_tactic (state: Elab.Tactic.SavedState) (goalId: Nat) (tactic: String):
  Elab.TermElabM Elab.Tactic.SavedState := do
  let stx := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `tactic)
    (input := tactic)
    (fileName := filename) |>.toOption |>.get!
  state.term.restore
  let tac : Elab.Tactic.TacticM Unit := set state.tactic *> Elab.Tactic.evalTactic stx
  let mvarId := state.tactic.goals.get! goalId
  Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let unsolvedGoals ← Elab.Tactic.run mvarId tac
  if (← getThe Core.State).messages.hasErrors then
    let messages := (← getThe Core.State).messages |>.toList.toArray
    let errors ← (messages.map Message.data).mapM fun md => md.toString
    IO.println s!"{errors}"
    return state
  else
    unsolvedGoals.forM instantiateMVarDeclMVars
    let nextState : Elab.Tactic.SavedState := {
      term := (← Elab.Term.saveState),
      tactic := { goals := unsolvedGoals }
    }
    let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
    IO.println s!"Tactic '{tactic}' succeeded."
    IO.println s!"{goals}"
    return nextState
def try_assign (state: Elab.Tactic.SavedState) (goalId: Nat) (expr: String):
  Elab.TermElabM Elab.Tactic.SavedState := do
  state.term.restore
  let mvarId := state.tactic.goals.get! goalId

  let expr := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := expr)
    (fileName := filename) |>.toOption |>.get!
  let goalType ← mvarId.getType
  let expr ← Elab.Term.elabTerm (stx := expr) (expectedType? := .some goalType)

  mvarId.checkNotAssigned `try_assign
  mvarId.assign expr

  if (← getThe Lean.Core.State).messages.hasErrors then
    let messages := (← getThe Lean.Core.State).messages |>.toList.toArray
    let errors ← (messages.map Lean.Message.data).mapM fun md => md.toString
    IO.println s!"{errors}"
    return state

  let prevMCtx := state.term.meta.meta.mctx
  let nextMCtx ← getMCtx
  -- Generate a list of mvarIds that exist in the parent state; Also test the
  -- assertion that the types have not changed on any mvars.
  let newMVars ← nextMCtx.decls.foldlM (fun acc mvarId mvarDecl => do
    if let .some prevMVarDecl := prevMCtx.decls.find? mvarId then
      assert! prevMVarDecl.type == mvarDecl.type
      return acc
    else
      return mvarId :: acc
    ) []
  let nextGoals ← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned))
  let nextState : Lean.Elab.Tactic.SavedState := {
    term := (← Lean.Elab.Term.saveState),
    tactic := { goals := nextGoals }
  }
  return nextState

def execute_term_elab (termElabM: Lean.Elab.TermElabM α): M IO (α × Lean.Core.State) := do
  let context ← read
  let metaM : Lean.MetaM α := termElabM.run' (ctx := context.elabContext)
  let coreM : Lean.CoreM α := metaM.run'
  let coreState : Lean.Core.State := { env := context.env }
  coreM.toIO context.coreContext coreState

def proof: M IO Unit := do
  let context ← read
  let (_, _) ← execute_term_elab <| do
    let expr ← parse_expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
    let state ← start_tactic_state expr
    let state ← execute_tactic state 0 "intro p q h"
    let branch ← try_assign state 0 "Or.inl (Or.inl h)"
  IO.println "Completed"


def main := do
  let env: Lean.Environment ← Lean.importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
  proof |>.run { env := env }

The error is

unknown identifier 'h'

[Leni Aniva]

I found the solution: Lean.Meta.withLCtx