import Lean

structure Context where
  env: Lean.Environment
  coreContext : Lean.Core.Context := {
      currNamespace := Lean.Name.anonymous,
      openDecls := [],     -- No 'open' directives needed
      fileName := "<onion>",
      fileMap := { source := "", positions := #[0], lines := #[1] }
    }
  elabContext : Lean.Elab.Term.Context := {
      declName? := some "Onion",
      errToSorry := false
    }

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

def parse_expr (env: Lean.Environment) (s: String): Lean.Elab.TermElabM Lean.Expr := do
  let syn := Lean.Parser.runParserCategory
    (env := env)
    (catName := `term)
    (input := s)
    (fileName := "<stdin>") |>.toOption |>.get!
  let expr ← Lean.Elab.Term.elabType syn
  -- Immediately synthesise all metavariables since we need to leave the elaboration context.
  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
  Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let expr ← Lean.instantiateMVars expr
  return expr

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

def execute_tactic (env: Lean.Environment) (state: Lean.Elab.Tactic.SavedState) (tactic: String): Lean.Elab.TermElabM Lean.Elab.Tactic.SavedState := do
  let stx := Lean.Parser.runParserCategory
    (env := env)
    (catName := `tactic)
    (input := tactic)
    (fileName := "<stdin>") |>.toOption |>.get!
  state.term.restore
  let tac : Lean.Elab.Tactic.TacticM Unit := set state.tactic *> Lean.Elab.Tactic.evalTactic stx
  let mvarId := state.tactic.goals.get! 0
  Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
  let unsolvedGoals ← Lean.Elab.Tactic.run mvarId tac
  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
  else
    unsolvedGoals.forM Lean.instantiateMVarDeclMVars
    let nextState : Lean.Elab.Tactic.SavedState := {
      term := (← Lean.Elab.Term.saveState),
      tactic := { goals := unsolvedGoals }
    }
    let goals ← unsolvedGoals.mapM fun g => do pure $ toString (← Lean.Meta.ppGoal g)
    IO.println s!"Tactic succeeded with goals {goals}"
    return nextState

def term_elab_layer (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 meta_layer (metaM: Lean.MetaM α): M IO (α × Lean.Core.State) := do
  let context ← read
  let coreM : Lean.CoreM α := metaM.run'
  let coreState : Lean.Core.State := { env := context.env }
  coreM.toIO context.coreContext coreState
def core_layer_2 (coreM: Lean.CoreM α): M IO (α × Lean.Core.State) := do
  let context ← read
  let coreState : Lean.Core.State := { env := context.env }
  let core := coreM.run context.coreContext coreState
  match (← core.toIO') with
  | .ok result => return result
  | .error e =>
    IO.println s!"Oh no {← e.toMessageData.toString}"
    sorry

def core_layer (coreM: Lean.CoreM α): M IO (α × Lean.Core.State) := do
  let context ← read
  let coreState : Lean.Core.State := { env := context.env }
  coreM.toIO context.coreContext coreState

def Context.to_meta (context: Context) (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
  termElabM.run' (ctx := context.elabContext)
def Context.to_core (context: Context) (termElabM: Lean.Elab.TermElabM α): Lean.CoreM α :=
  context.to_meta termElabM |>.run'
def Context.to_io_2 (context: Context) (termElabM: Lean.Elab.TermElabM α): IO α := do
  let coreState : Lean.Core.State := { env := context.env }
  let core := context.to_core termElabM |>.run context.coreContext coreState
  match (← core.toIO') with
  | .ok result => return result.fst
  | .error e =>
    IO.println s!"Oh no {← e.toMessageData.toString}"
    sorry
def Context.to_io (context: Context) (termElabM: Lean.Elab.TermElabM α): IO α := do
  let coreState : Lean.Core.State := { env := context.env }
  let (ret, _) ← context.to_core termElabM |>.toIO context.coreContext coreState
  return ret


def proof_term_elab: M IO Unit := do
  let context ← read
  let env := context.env
  let (_, _) ← term_elab_layer <| do
    let expr ← parse_expr env "∀ (p q: Prop), p ∨ q → q ∨ p"
    let state ← start_tactic_state expr
    let state ← execute_tactic env state "intro p q h"
    let state ← execute_tactic env state "cases h"
    let _ ← execute_tactic env state "apply Or.inr"
  IO.println "Completed"
def proof_core: M IO Unit := do
  let context ← read
  let env := context.env
  let (_, _) ← core_layer <| do
    let expr ← context.to_core <| parse_expr env "∀ (p q: Prop), p ∨ q → q ∨ p"
    let state ← context.to_core <| start_tactic_state expr
    let state ← context.to_core <| execute_tactic env state "intro p q h"
    let state ← context.to_core <| execute_tactic env state "cases h"
    let _ ← context.to_core <| execute_tactic env state "apply Or.inr"
  IO.println "Completed"
def proof_core_2: M IO Unit := do
  let context ← read
  let env := context.env
  let (_, _) ← core_layer_2 <| do
    let expr ← context.to_core <| parse_expr env "∀ (p q: Prop), p ∨ q → q ∨ p"
    let state ← context.to_core <| start_tactic_state expr
    let state ← context.to_core <| execute_tactic env state "intro p q h"
    let state ← context.to_core <| execute_tactic env state "cases h"
    let _ ← context.to_core <| execute_tactic env state "apply Or.inr"
  IO.println "Completed"
def proof_io_2: M IO Unit := do
  let context ← read
  let env := context.env
  let expr ← context.to_io_2 <| parse_expr env "∀ (p q: Prop), p ∨ q → q ∨ p"
  let state ← context.to_io_2 <| start_tactic_state expr
  let state ← context.to_io_2 <| execute_tactic env state "intro p q h"
  let state ← context.to_io_2 <| execute_tactic env state "cases h"
  let _ ← context.to_io_2 <| execute_tactic env state "apply Or.inr"
  IO.println "Completed"
def proof_io: M IO Unit := do
  let context ← read
  let env := context.env
  let expr ← context.to_io <| parse_expr env "∀ (p q: Prop), p ∨ q → q ∨ p"
  let state ← context.to_io <| start_tactic_state expr
  let state ← context.to_io <| execute_tactic env state "intro p q h"
  let state ← context.to_io <| execute_tactic env state "cases h"
  let _ ← context.to_io <| execute_tactic env state "apply Or.inr"
  IO.println "Completed"


def main := do
  let env ← Lean.importModules
    (imports := [{ module := Lean.Name.str .anonymous "Init", runtimeOnly := false }])
    (opts := {})
    (trustLevel := 1)
  proof_term_elab |>.run { env := env }