chore: Update Lean to v4.19.0 #205

import Lean
open Lean

def fileName := "<example>"

structure Context where
  env: Environment
  coreContext : Core.Context := {
    currNamespace := Name.anonymous,
    openDecls := [],
    fileName,
    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 Expr := do
  let syn? := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := s)
    (fileName := fileName)
  let .ok syn := syn? | throwError "Parser not defined"
  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[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.mapM (·.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[goalId]!

  let expr := Parser.runParserCategory
    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := expr)
    (fileName := fileName) |>.toOption |>.get!
  let goalType ← mvarId.getType

  let expr ← mvarId.withContext (Elab.Term.elabTerm (stx := expr) (expectedType? := .some goalType))

  mvarId.checkNotAssigned `try_assign
  mvarId.assign expr

  if (← getThe Core.State).messages.hasErrors then
    let messages := (← getThe Core.State).messages |>.toList.toArray
    let errors ← messages.mapM (·.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 : Elab.Tactic.SavedState := {
    term := (← Elab.Term.saveState),
    tactic := { goals := nextGoals }
  }
  return nextState

def execute_term_elab (termElabM: Elab.TermElabM α): M IO (α × Core.State) := do
  let context ← read
  let metaM : MetaM α := termElabM.run' (ctx := context.elabContext)
  let coreM : CoreM α := metaM.run'
  let coreState : 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: Environment ← importModules
    (imports := #[`Init])
    (opts := {})
    (trustLevel := 1)
  proof |>.run { env := env }

Seems like the parser is not defined.

Tactic execution pipeline in a nutshell: ```lean import Lean open Lean def fileName := "<example>" structure Context where env: Environment coreContext : Core.Context := { currNamespace := Name.anonymous, openDecls := [], fileName, 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 Expr := do let syn? := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := s) (fileName := fileName) let .ok syn := syn? | throwError "Parser not defined" 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[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.mapM (·.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[goalId]! let expr := Parser.runParserCategory (env := ← MonadEnv.getEnv) (catName := `term) (input := expr) (fileName := fileName) |>.toOption |>.get! let goalType ← mvarId.getType let expr ← mvarId.withContext (Elab.Term.elabTerm (stx := expr) (expectedType? := .some goalType)) mvarId.checkNotAssigned `try_assign mvarId.assign expr if (← getThe Core.State).messages.hasErrors then let messages := (← getThe Core.State).messages |>.toList.toArray let errors ← messages.mapM (·.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 : Elab.Tactic.SavedState := { term := (← Elab.Term.saveState), tactic := { goals := nextGoals } } return nextState def execute_term_elab (termElabM: Elab.TermElabM α): M IO (α × Core.State) := do let context ← read let metaM : MetaM α := termElabM.run' (ctx := context.elabContext) let coreM : CoreM α := metaM.run' let coreState : 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: Environment ← importModules (imports := #[`Init]) (opts := {}) (trustLevel := 1) proof |>.run { env := env } ``` Seems like the parser is not defined.

This pull request can be merged automatically.

You are not authorized to merge this pull request.

Sign in to join this conversation.

No reviewers