Could not reference local context variables #61

New Issue

aniva · 2024-04-06T17:52:26-07:00

aniva commented

2024-04-06 17:52:26 -07:00

This test currently fails:

def test_have: TestM Unit := do
  let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))")
  let state0 ← match state? with
    | .some state => pure state
    | .none => do
      addTest $ assertUnreachable "Goal could not parse"
      return ()
  let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "intro p q h" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"])

  let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "Or.inl (Or.inl h)") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
    #[buildGoal [] ""])

MWE:

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.elabTermAndSynthesize (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 }

This test currently fails: ```lean def test_have: TestM Unit := do let state? ← startProof (.expr "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))") let state0 ← match state? with | .some state => pure state | .none => do addTest $ assertUnreachable "Goal could not parse" return () let state1 ← match ← state0.tryTactic (goalId := 0) (tactic := "intro p q h") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "intro p q h" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p")] "(p ∨ q) ∨ p ∨ q"]) let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "Or.inl (Or.inl h)") with | .success state => pure state | other => do addTest $ assertUnreachable $ other.toString return () addTest $ LSpec.check "have" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) = #[buildGoal [] ""]) ``` MWE: ```lean 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.elabTermAndSynthesize (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 } ```

aniva added the

labels 2024-04-06 17:52:26 -07:00

aniva self-assigned this 2024-04-06 17:52:26 -07:00

aniva added reference goal/have-conv-calc

2024-04-06 21:55:07 -07:00

aniva commented

2024-04-06 21:55:20 -07:00