Add tactic state manipulation

This commit is contained in:
Leni Ven 2023-05-17 21:58:03 -07:00
parent 2ec4efde55
commit 14a6eb1f59
6 changed files with 216 additions and 49 deletions

40
Examples/Proof.lean Normal file
View File

@ -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]

View File

@ -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 :=
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
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}"
unsafe def clear: Subroutine ClearResult := do
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

View File

@ -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

105
Pantograph/Proofs.lean Normal file
View File

@ -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

View File

@ -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"

View File

@ -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
}