Add tactic state manipulation

Examples/Proof.lean

@@ -0,0 +1,40 @@
+import Lean
+import Pantograph.Proofs
+import Pantograph.Symbols
+
+open Pantograph
+
+/-
+Example of using the internal API to execute tactics!
+-/
+
+def execute_proof (env: Lean.Environment): IO Unit := do
+  let name := strToName "Nat.add_comm"
+  let context := createContext name env
+  (do
+    let state ← start_proof_state
+    IO.println "Proof state started!"
+    let tactic := "intro n m"
+    let (state, response) ← execute_tactic state tactic
+    IO.println s! "Executed {tactic}  Errors: {response.errors}  Goals: {response.goals}"
+    --let tactic := "assumption" -- should fail
+    --let (_, response) ← execute_tactic state tactic
+    --IO.println s! "Executed {tactic}  Errors: {response.errors}  Goals: {response.goals}"
+    let tactic := "rw [Nat.add_comm]"
+    let (state, response) ← execute_tactic state tactic
+    IO.println s! "Executed {tactic}  Errors: {response.errors}  Goals: {response.goals}"
+  ) |>.run context
+
+unsafe def main : IO Unit := do
+  Lean.enableInitializersExecution
+  Lean.initSearchPath (← Lean.findSysroot)
+  let imports := ["Init"]
+  let env: Lean.Environment ← Lean.importModules
+    (imports := imports.map (λ str => { module := strToName str, runtimeOnly := false }))
+    (opts := {})
+    (trustLevel := 1)
+  execute_proof env
+
+example : ∀ (n m : Nat), n + m = m + n := by
+  intros n m
+  rw [Nat.add_comm]

Main.lean

@@ -12,6 +12,7 @@ def option_expect (o: Option α) (error: String): Except String α :=
   | .some value => return value
   | .none => throw error
 
+
 structure State where
   environments: Array Lean.Environment
 
@@ -26,13 +27,35 @@ structure Command where
   payload: Lean.Json
   deriving Lean.FromJson
 
-namespace Commands
+open Commands
 
-def create (args: Create): Subroutine CreateResult := do
+unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do
+  let obj ← Lean.Json.parse command
+  let command: Command ← Lean.fromJson? obj
+  match command.cmd with
+  | "create" =>
+    let args: Commands.Create ← Lean.fromJson? command.payload
+    let ret ← create args
+    return Lean.toJson ret
+  | "catalog" =>
+    let args: Commands.Catalog ← Lean.fromJson? command.payload
+    let ret ← catalog args
+    return Lean.toJson ret
+  | "clear" =>
+    -- Delete all the environments
+    let ret ← clear
+    return Lean.toJson ret
+  | "proof.trace" =>
+    let args: Commands.ProofTrace ← Lean.fromJson? command.payload
+    let ret ← proof_trace args
+    return Lean.toJson ret
+  | cmd => throw s!"Unknown verb: {cmd}"
+  where
+  create (args: Create): Subroutine CreateResult := do
     let state ← get
     let id := nextId state
     let env ← Lean.importModules
-    (imports := args.imports.map strTransform)
+      (imports := args.imports.map (λ str => { module := strToName str, runtimeOnly := false }))
       (opts := {})
       (trustLevel := 1)
     modify fun s => { environments := s.environments.push env }
@@ -42,12 +65,7 @@ def create (args: Create): Subroutine CreateResult := do
       id := id,
       symbols := env.constants.size,
       filtered_symbols := num_filtered_symbols }
-  where strTransform (s: String): Lean.Import :=
+  catalog (args: Catalog): Subroutine CatalogResult := do
-      let li := s.split (λ c => c == '.')
-      let name := li.foldl (λ pre segment => Lean.Name.str pre segment) Lean.Name.anonymous
-      { module := name, runtimeOnly := false }
-
-def catalog (args: Catalog): Subroutine CatalogResult := do
     let state ← get
     match state.environments.get? args.id with
     | .some env =>
@@ -57,35 +75,22 @@ def catalog (args: Catalog): Subroutine CatalogResult := do
         | .none => es)
       return { theorems := names }
     | .none => throw s!"Invalid environment id {args.id}"
-
+  clear: Subroutine ClearResult := do
-unsafe def clear: Subroutine ClearResult := do
     let state ← get
     for env in state.environments do
       env.freeRegions
     return { n := state.environments.size }
+  proof_trace (args: ProofTrace): Subroutine ProofTraceResult := do
+    -- Step 1: Create tactic state
+    -- Step 2: Execute tactic
+    -- Step 3: ??
+    return { expr := "test" }
+
 
-end Commands
 end Pantograph
 
 open Pantograph
 
-unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do
-  let obj ← Lean.Json.parse command
-  let command: Command ← Lean.fromJson? obj
-  match command.cmd with
-  | "create" =>
-    let args: Commands.Create ← Lean.fromJson? command.payload
-    let ret ← Commands.create args
-    return Lean.toJson ret
-  | "catalog" =>
-    let args: Commands.Catalog ← Lean.fromJson? command.payload
-    let ret ← Commands.catalog args
-    return Lean.toJson ret
-  | "clear" =>
-    -- Delete all the environments
-    let ret ← Commands.clear
-    return Lean.toJson ret
-  | cmd => throw s!"Unknown verb: {cmd}"
 
 
 -- Main IO functions

Pantograph/Commands.lean

@@ -6,20 +6,28 @@ namespace Pantograph.Commands
 structure Create where
   imports : List String
   deriving Lean.FromJson
-structure Catalog where
-  id: Nat
-  deriving Lean.FromJson
-
 structure CreateResult where
   id: Nat
   symbols: Nat
   filtered_symbols: Nat
   deriving Lean.ToJson
+
+structure Catalog where
+  id: Nat
+  deriving Lean.FromJson
 structure CatalogResult where
   theorems: List String
   deriving Lean.ToJson
+
 structure ClearResult where
   n: Nat -- Number of environments reset
   deriving Lean.ToJson
 
+structure ProofTrace where
+  id: Nat -- Environment id
+  deriving Lean.FromJson
+structure ProofTraceResult where
+  expr: String
+  deriving Lean.ToJson
+
 end Pantograph.Commands

Pantograph/Proofs.lean

@@ -0,0 +1,105 @@
+import Lean
+import Pantograph.Symbols
+
+
+/-
+The proof state manipulation system
+
+A proof state is launched by providing
+1. Environment: `Lean.Environment`
+2. Expression: `Lean.Expr`
+The expression becomes the first meta variable in the saved tactic state
+`Lean.Elab.Tactic.SavedState`.
+From this point on, any proof which extends
+`Lean.Elab.Term.Context` and
+-/
+
+def Lean.MessageLog.getErrorMessages (log : Lean.MessageLog) : Lean.MessageLog :=
+{ msgs := log.msgs.filter fun m => match m.severity with | Lean.MessageSeverity.error => true | _ => false }
+
+namespace Pantograph
+
+
+
+-- All parameters needed to run a `TermElabM` monad
+structure Context where
+  env: Lean.Environment
+  name: Lean.Name
+  coreContext : Lean.Core.Context
+  elabContext: Lean.Elab.Term.Context
+
+-- Tactic execution response
+structure Response : Type where
+  goals    : Array String := #[]
+  errors   : Array String := #[]
+
+
+def createContext (name: Lean.Name) (env: Lean.Environment): Context :=
+  {
+    env := env,
+    name := name,
+    coreContext := {
+      currNamespace := strToName "Aniva",
+      openDecls := [],     -- No 'open' directives needed
+      fileName := "<Gym>",
+      fileMap := { source := "", positions := #[0], lines := #[1] }
+    },
+    elabContext := {
+      declName? := some (name ++ "_pantograph"),
+      errToSorry := false
+    }
+  }
+
+def Context.runTermElabM (termElabM: Lean.Elab.TermElabM α): ReaderT Context 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 Context.runTermElabM' (termElabM: Lean.Elab.TermElabM α): ReaderT Context IO α := do
+  let context ← read
+  let (result, _) ← context.runTermElabM termElabM
+  return result
+
+
+def start_proof_state: ReaderT Context IO Lean.Elab.Tactic.SavedState := do
+  let context ← read
+  let name := context.name
+  let termElabM : Lean.Elab.TermElabM Lean.Elab.Tactic.SavedState := do
+    match context.env.find? name with
+    | none       => throwError "decl {name} not found"
+    | some cInfo =>
+      if ¬ (← Lean.Meta.isProp cInfo.type) then throwError "decl {name} not a theorem"
+      let mvar ← Lean.Meta.mkFreshExprMVar (some cInfo.type) (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!] }}
+      return tacticState
+  Context.runTermElabM' termElabM
+
+def execute_tactic (state: Lean.Elab.Tactic.SavedState) (tacticString : String) : ReaderT Context IO (Lean.Elab.Tactic.SavedState × Response) := do
+  let context ← read
+  match Lean.Parser.runParserCategory
+    (env := context.env)
+    (catName := `tactic)
+    (input := tacticString)
+    (fileName := "<stdin>") with
+  | Except.error err => pure (state, { errors := #[err] })
+  | Except.ok stx    => Context.runTermElabM' <| do
+    state.term.restore
+    let tac : Lean.Elab.Tactic.TacticM Unit := set state.tactic *> Lean.Elab.Tactic.evalTactic stx
+    let mvarId : Lean.MVarId := state.tactic.goals.head!
+    try
+      let unsolvedGoals ← Lean.Elab.Tactic.run mvarId tac
+      if (← getThe Lean.Core.State).messages.hasErrors then
+        let messages := (← getThe Lean.Core.State).messages.getErrorMessages |>.toList.toArray
+        pure (state, { errors := ← (messages.map Lean.Message.data).mapM fun md => md.toString })
+      else
+        let nextState : Lean.Elab.Tactic.SavedState := { term := (← Lean.Elab.Term.saveState), tactic := { goals := unsolvedGoals}}
+        let goals ← nextState.tactic.goals.mapM fun g => do pure $ toString (← Lean.Meta.ppGoal g)
+        pure (nextState, { goals := goals.toArray })
+    catch ex =>
+      pure (state, { errors := #[← ex.toMessageData.toString] })
+
+
+
+end Pantograph

Pantograph/Symbols.lean

@@ -5,6 +5,9 @@ import Lean.Declaration
 
 namespace Pantograph
 
+def strToName (s: String): Lean.Name :=
+  (s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous
+
 def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
   let nameDeduce: Bool := match n.getRoot with
   | .str _ name => name.startsWith "_" ∨ name == "Lean"

lakefile.lean

@@ -17,3 +17,9 @@ lean_exe pantograph {
   -- Somehow solves the native symbol not found problem
   supportInterpreter := true
 }
+
+lean_exe examples_proof {
+  root := `Examples.Proof
+  -- Somehow solves the native symbol not found problem
+  supportInterpreter := true
+}