Add REPL tactics
This commit is contained in:
parent
15aab3d31f
commit
083ec8beec
|
|
@ -1,25 +0,0 @@
|
|||
import Lean
|
||||
|
||||
def strToName (s: String): Lean.Name :=
|
||||
(s.splitOn ".").foldl Lean.Name.str Lean.Name.anonymous
|
||||
|
||||
unsafe def main (args: List String): 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)
|
||||
|
||||
let expr := args.head?.getD "a + b"
|
||||
|
||||
match Lean.Parser.runParserCategory
|
||||
(env := env)
|
||||
(catName := `term)
|
||||
(input := expr)
|
||||
(fileName := "<stdin>") with
|
||||
| Except.error error => IO.println s!"{error}"
|
||||
| Except.ok (syn: Lean.Syntax) =>
|
||||
let reprint := Lean.Syntax.reprint syn |>.get!
|
||||
IO.println reprint
|
||||
|
|
@ -1,5 +1,6 @@
|
|||
import Lean
|
||||
import Pantograph.Proofs
|
||||
import Pantograph.Meta
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Symbols
|
||||
|
||||
open Pantograph
|
||||
|
|
@ -8,29 +9,50 @@ 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
|
||||
def serialise (result: Meta.TacticResult): String := match result with
|
||||
| .invalid message => s!"Invalid: {message}"
|
||||
| .success 0 _ => s!"Completed!"
|
||||
| .success nextId _ => s!"Success: {nextId}"
|
||||
| .failure messages => s!"Failures: {messages}"
|
||||
|
||||
def start_proof: IO Meta.ProofTree := do
|
||||
let imports := ["Init"]
|
||||
let env: Lean.Environment ← Lean.importModules
|
||||
(imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
let name := str_to_name "Nat.add_comm"
|
||||
let state := Meta.createProofTree
|
||||
(name := str_to_name "aa") env
|
||||
(coreContext := {
|
||||
currNamespace := str_to_name "Aniva",
|
||||
openDecls := [], -- No 'open' directives needed
|
||||
fileName := "<Pantograph>",
|
||||
fileMap := { source := "", positions := #[0], lines := #[1] }
|
||||
})
|
||||
let s := "∀ (n m : Nat), n + m = m + n"
|
||||
let syn: Lean.Syntax := Serial.syntax_from_str env s |>.toOption |>.get!
|
||||
IO.println "Created syntax"
|
||||
let expr: Lean.Expr := (← Meta.ProofM.syntax_to_expr syn |>.run' state) |>.toOption |>.get!
|
||||
IO.println "Created expr"
|
||||
--let expr := env.find? name |>.get! |>.type
|
||||
let (_, state) ← Meta.ProofM.start expr |>.run state
|
||||
return state
|
||||
|
||||
def execute_proof: IO Unit := do
|
||||
let state ← start_proof
|
||||
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 (result, state) ← Meta.ProofM.execute 0 tactic |>.run state
|
||||
IO.println s! "Executed {tactic}, Response: [{serialise result}]"
|
||||
let tactic := "assumption" -- should fail
|
||||
let (_, response) ← execute_tactic state tactic
|
||||
IO.println s! "Executed {tactic} Errors: {response.errors} Goals: {response.goals}"
|
||||
let (result, state) ← Meta.ProofM.execute 1 tactic |>.run state
|
||||
IO.println s! "Executed {tactic}, Response: [{serialise result}]"
|
||||
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
|
||||
let (result, state) ← Meta.ProofM.execute 1 tactic |>.run state
|
||||
IO.println s! "Executed {tactic}, Response: [{serialise result}]"
|
||||
|
||||
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
|
||||
execute_proof
|
||||
|
|
|
|||
106
Main.lean
106
Main.lean
|
|
@ -2,7 +2,8 @@ import Lean.Data.Json
|
|||
import Lean.Environment
|
||||
|
||||
import Pantograph.Commands
|
||||
import Pantograph.IO
|
||||
import Pantograph.Serial
|
||||
import Pantograph.Meta
|
||||
import Pantograph.Symbols
|
||||
|
||||
namespace Pantograph
|
||||
|
|
@ -14,6 +15,7 @@ structure Context where
|
|||
/-- Stores state of the REPL -/
|
||||
structure State where
|
||||
environments: Array Lean.Environment := #[]
|
||||
proofTrees: Array Meta.ProofTree := #[]
|
||||
|
||||
-- State monad
|
||||
abbrev Subroutine := ReaderT Context (StateT State IO)
|
||||
|
|
@ -70,9 +72,17 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
|
|||
match Lean.fromJson? command.payload with
|
||||
| .ok args => inspect args
|
||||
| .error x => return errorJson x
|
||||
| "proof.trace" =>
|
||||
| "proof.start" =>
|
||||
match Lean.fromJson? command.payload with
|
||||
| .ok args => proof_trace args
|
||||
| .ok args => proof_start args
|
||||
| .error x => return errorJson x
|
||||
| "proof.tactic" =>
|
||||
match Lean.fromJson? command.payload with
|
||||
| .ok args => proof_tactic args
|
||||
| .error x => return errorJson x
|
||||
| "proof.printTree" =>
|
||||
match Lean.fromJson? command.payload with
|
||||
| .ok args => proof_print_tree args
|
||||
| .error x => return errorJson x
|
||||
| cmd =>
|
||||
let error: InteractionError := { error := "unknown", desc := s!"Unknown command {cmd}" }
|
||||
|
|
@ -84,7 +94,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
|
|||
let state ← get
|
||||
let id := nextId state
|
||||
let env ← Lean.importModules
|
||||
(imports := args.imports.map (λ str => { module := strToName str, runtimeOnly := false }))
|
||||
(imports := args.imports.map (λ str => { module := str_to_name str, runtimeOnly := false }))
|
||||
(opts := {})
|
||||
(trustLevel := 1)
|
||||
modify fun s => { environments := s.environments.push env }
|
||||
|
|
@ -109,7 +119,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
|
|||
let nEnv := state.environments.size
|
||||
for env in state.environments do
|
||||
env.freeRegions
|
||||
set { state with environments := #[] }
|
||||
set ({ }: State)
|
||||
return Lean.toJson ({ nEnv := nEnv }: ClearResult)
|
||||
inspect (args: Inspect): Subroutine Lean.Json := do
|
||||
let context ← read
|
||||
|
|
@ -117,35 +127,83 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
|
|||
match state.getEnv args.id with
|
||||
| .error error => return Lean.toJson <| errorIndex error
|
||||
| .ok env =>
|
||||
let info? := env.find? <| strToName args.symbol
|
||||
let info? := env.find? <| str_to_name args.symbol
|
||||
match info? with
|
||||
| none => return Lean.toJson <| errorIndex s!"Symbol not found {args.symbol}"
|
||||
| some info =>
|
||||
let format ← IO.exprToStr
|
||||
let format ← Serial.expr_to_str
|
||||
(env := env)
|
||||
(coreContext := context.coreContext)
|
||||
(expr := info.toConstantVal.type)
|
||||
return Lean.toJson ({ type := format }: InspectResult)
|
||||
proof_trace (args: ProofTrace): Subroutine Lean.Json := do
|
||||
-- Step 1: Create tactic state
|
||||
-- Step 2: Execute tactic
|
||||
-- Step 3: ??
|
||||
return Lean.toJson ({ expr := "test" }: ProofTraceResult)
|
||||
proof_start (args: ProofStart): Subroutine Lean.Json := do
|
||||
let context ← read
|
||||
let state ← get
|
||||
let ret?: Except Lean.Json Meta.ProofTree ← ExceptT.run <| (do
|
||||
let env ← match state.getEnv args.id with
|
||||
| .error error => throw <| Lean.toJson <| errorIndex error
|
||||
| .ok env => pure env
|
||||
let tree := Meta.createProofTree
|
||||
(name := args.name)
|
||||
(env := env)
|
||||
(coreContext := context.coreContext)
|
||||
let expr: Lean.Expr ← match args.expr, args.copyFrom with
|
||||
| "", "" =>
|
||||
throw <| Lean.toJson ({ error := "arguments", desc := "At least one of {expr, copyFrom} must be supplied" }: InteractionError)
|
||||
| expr, "" =>
|
||||
let syn ← match Serial.syntax_from_str env expr with
|
||||
| .error str => throw <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError)
|
||||
| .ok syn => pure syn
|
||||
let expr: Lean.Expr ← match (← Meta.ProofM.syntax_to_expr syn |>.run' tree) with
|
||||
| .error str => throw <| Lean.toJson ({ error := "elab", desc := str }: InteractionError)
|
||||
| .ok expr => pure expr
|
||||
pure expr
|
||||
| "", copyFrom =>
|
||||
match Serial.expr_from_const env (name := str_to_name copyFrom) with
|
||||
| .error str =>
|
||||
IO.println "Symbol not found"
|
||||
throw <| errorIndex str
|
||||
| .ok expr => pure expr
|
||||
| _, _ => throw <| Lean.toJson ({ error := "arguments", desc := "Cannot populate both of {expr, copyFrom}" }: InteractionError)
|
||||
let (_, tree) := ← (Meta.ProofM.start expr |>.run tree)
|
||||
return tree
|
||||
)
|
||||
match ret? with
|
||||
| .error error => return error
|
||||
| .ok tree =>
|
||||
-- Put the new tree in the environment
|
||||
let nextId := state.proofTrees.size
|
||||
set { state with proofTrees := state.proofTrees.push tree }
|
||||
return Lean.toJson ({ treeId := nextId }: ProofStartResult)
|
||||
proof_tactic (args: ProofTactic): Subroutine Lean.Json := do
|
||||
let state ← get
|
||||
match state.proofTrees.get? args.treeId with
|
||||
| .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}"
|
||||
| .some tree =>
|
||||
let (result, nextTree) ← Meta.ProofM.execute args.stateId args.goalId args.tactic |>.run tree
|
||||
match result with
|
||||
| .invalid message => return Lean.toJson <| errorIndex message
|
||||
| .success nextId goals =>
|
||||
set { state with proofTrees := state.proofTrees.set! args.treeId nextTree }
|
||||
return Lean.toJson ({ nextId := nextId, goals := goals }: ProofTacticResultSuccess)
|
||||
| .failure messages =>
|
||||
return Lean.toJson ({ errorMessages := messages }: ProofTacticResultFailure)
|
||||
proof_print_tree (args: ProofPrintTree): Subroutine Lean.Json := do
|
||||
let state ← get
|
||||
match state.proofTrees.get? args.treeId with
|
||||
| .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}"
|
||||
| .some tree =>
|
||||
let parents := tree.states.map λ state => match state.parent with
|
||||
| .none => ""
|
||||
| .some parent => s!"{parent}.{state.parentGoalId}"
|
||||
return Lean.toJson ({parents := parents}: ProofPrintTreeResult)
|
||||
|
||||
|
||||
end Pantograph
|
||||
|
||||
open Pantograph
|
||||
|
||||
|
||||
|
||||
-- Main IO functions
|
||||
|
||||
unsafe def getLines : IO String := do
|
||||
match (← (← IO.getStdin).getLine) with
|
||||
| "" => pure ""
|
||||
| "\n" => pure "\n"
|
||||
| line => pure <| line ++ (← getLines)
|
||||
open Pantograph
|
||||
|
||||
unsafe def loop : Subroutine Unit := do
|
||||
let command ← (← IO.getStdin).getLine
|
||||
|
|
@ -163,10 +221,14 @@ unsafe def main : IO Unit := do
|
|||
Lean.initSearchPath (← Lean.findSysroot)
|
||||
let context: Context := {
|
||||
coreContext := {
|
||||
currNamespace := strToName "Aniva",
|
||||
currNamespace := str_to_name "Aniva",
|
||||
openDecls := [], -- No 'open' directives needed
|
||||
fileName := "<Pantograph>",
|
||||
fileMap := { source := "", positions := #[0], lines := #[1] }
|
||||
}
|
||||
}
|
||||
try
|
||||
loop.run context |>.run' {}
|
||||
catch ex =>
|
||||
IO.println "Uncaught IO exception"
|
||||
IO.println ex.toString
|
||||
|
|
|
|||
|
|
@ -48,11 +48,38 @@ structure InspectResult where
|
|||
type: String := ""
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure ProofTrace where
|
||||
structure ProofStart where
|
||||
id: Nat -- Environment id
|
||||
name: String := "Untitled" -- Identifier of the proof
|
||||
-- Only one of the fields below may be populated.
|
||||
expr: String := "" -- Proof expression
|
||||
copyFrom: String := "" -- Theorem name
|
||||
deriving Lean.FromJson
|
||||
structure ProofTraceResult where
|
||||
expr: String
|
||||
structure ProofStartResult where
|
||||
error: String := ""
|
||||
treeId: Nat := 0 -- Proof tree id
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure ProofTactic where
|
||||
treeId: Nat
|
||||
stateId: Nat
|
||||
goalId: Nat := 0
|
||||
tactic: String
|
||||
deriving Lean.FromJson
|
||||
structure ProofTacticResultSuccess where
|
||||
goals: Array String
|
||||
nextId: Nat
|
||||
deriving Lean.ToJson
|
||||
structure ProofTacticResultFailure where
|
||||
errorMessages: Array String -- Error messages generated by tactic
|
||||
deriving Lean.ToJson
|
||||
|
||||
structure ProofPrintTree where
|
||||
treeId: Nat
|
||||
deriving Lean.FromJson
|
||||
structure ProofPrintTreeResult where
|
||||
-- "" if no parents, otherwise "parentId.goalId"
|
||||
parents: Array String
|
||||
deriving Lean.ToJson
|
||||
|
||||
end Pantograph.Commands
|
||||
|
|
|
|||
|
|
@ -1,19 +0,0 @@
|
|||
import Lean
|
||||
|
||||
/-
|
||||
Expression IO
|
||||
-/
|
||||
|
||||
|
||||
namespace Pantograph.IO
|
||||
|
||||
|
||||
def exprToStr (env: Lean.Environment) (coreContext: Lean.Core.Context) (expr: Lean.Expr): IO String := do
|
||||
let metaM := Lean.Meta.ppExpr expr
|
||||
let coreM : Lean.CoreM Lean.Format := metaM.run'
|
||||
let coreState : Lean.Core.State := { env := env }
|
||||
let (format, _) ← coreM.toIO coreContext coreState
|
||||
return format.pretty
|
||||
|
||||
|
||||
end Pantograph.IO
|
||||
|
|
@ -0,0 +1,169 @@
|
|||
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.Meta
|
||||
|
||||
structure ProofState where
|
||||
savedState : Lean.Elab.Tactic.SavedState
|
||||
parent : Option Nat := none
|
||||
parentGoalId : Nat := 0
|
||||
structure ProofTree where
|
||||
-- All parameters needed to run a `TermElabM` monad
|
||||
env: Lean.Environment
|
||||
name: Lean.Name
|
||||
coreContext : Lean.Core.Context
|
||||
elabContext : Lean.Elab.Term.Context
|
||||
|
||||
-- Set of proof states
|
||||
states : Array ProofState := #[]
|
||||
|
||||
abbrev ProofM := StateRefT ProofTree IO
|
||||
|
||||
def createProofTree (name: Lean.Name) (env: Lean.Environment) (coreContext: Lean.Core.Context): ProofTree :=
|
||||
{
|
||||
env := env,
|
||||
name := name,
|
||||
coreContext := coreContext,
|
||||
elabContext := {
|
||||
declName? := some (name ++ "_pantograph"),
|
||||
errToSorry := false
|
||||
}
|
||||
}
|
||||
|
||||
-- Executing a `TermElabM`
|
||||
def ProofM.runTermElabM (termElabM: Lean.Elab.TermElabM α): ProofM (α × Lean.Core.State) := do
|
||||
let context ← get
|
||||
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 ProofM.runTermElabM' (termElabM: Lean.Elab.TermElabM α): ProofM α := do
|
||||
return Prod.fst <| ← ProofM.runTermElabM termElabM
|
||||
|
||||
-- Parsing syntax under the environment
|
||||
def ProofM.syntax_to_expr (syn: Lean.Syntax): ProofM (Except String Lean.Expr) := do
|
||||
let termElabM : Lean.Elab.TermElabM (Except String Lean.Expr) :=
|
||||
try
|
||||
--let expr ← Lean.Elab.Term.elabTerm syn
|
||||
-- (expectedType? := none)
|
||||
-- (catchExPostpone := false)
|
||||
-- (implicitLambda := true)
|
||||
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 .ok expr
|
||||
|
||||
catch ex => return .error (← ex.toMessageData.toString)
|
||||
ProofM.runTermElabM' <| termElabM
|
||||
|
||||
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!] }}
|
||||
return tacticState
|
||||
/-- Create the initial proof state of the proof tree -/
|
||||
def ProofM.start (expr: Lean.Expr): ProofM Unit := do
|
||||
let state: ProofState := {
|
||||
savedState := (← ProofM.runTermElabM' <| start_tactic_state expr),
|
||||
parent := none
|
||||
}
|
||||
let tree ← get
|
||||
set { tree with states := #[state] }
|
||||
|
||||
|
||||
def execute_tactic (env: Lean.Environment) (state: Lean.Elab.Tactic.SavedState) (goalId: Nat) (tactic: String) :
|
||||
Lean.Elab.TermElabM (Except (Array String) Lean.Elab.Tactic.SavedState):= do
|
||||
-- Factor this one out to allow for direct syntactic communication
|
||||
match Lean.Parser.runParserCategory
|
||||
(env := env)
|
||||
(catName := `tactic)
|
||||
(input := tactic)
|
||||
(fileName := "<stdin>") with
|
||||
| Except.error err => return .error #[err]
|
||||
| Except.ok stx => do
|
||||
state.term.restore
|
||||
let tac : Lean.Elab.Tactic.TacticM Unit := set state.tactic *> Lean.Elab.Tactic.evalTactic stx
|
||||
match state.tactic.goals.get? goalId with
|
||||
| .none => return .error #[s!"Invalid goalId {goalId}"]
|
||||
| .some mvarId =>
|
||||
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
|
||||
let errors ← (messages.map Lean.Message.data).mapM fun md => md.toString
|
||||
return .error errors
|
||||
else
|
||||
let nextState : Lean.Elab.Tactic.SavedState := {
|
||||
term := (← Lean.Elab.Term.saveState),
|
||||
tactic := { goals := unsolvedGoals}
|
||||
}
|
||||
return .ok nextState
|
||||
catch ex =>
|
||||
return .error #[← ex.toMessageData.toString]
|
||||
|
||||
def extract_goals (state: Lean.Elab.Tactic.SavedState): Lean.Elab.TermElabM (Array String) := do
|
||||
state.term.restore
|
||||
let goals ← state.tactic.goals.mapM fun g => do pure $ toString (← Lean.Meta.ppGoal g)
|
||||
pure goals.toArray
|
||||
|
||||
|
||||
/-- Response for executing a tactic -/
|
||||
inductive TacticResult where
|
||||
-- Invalid id
|
||||
| invalid (message: String): TacticResult
|
||||
-- Goes to next state
|
||||
| success (nextId: Nat) (goals: Array String)
|
||||
-- Fails with messages
|
||||
| failure (messages: Array String)
|
||||
|
||||
/-- Execute tactic on given state -/
|
||||
def ProofM.execute (stateId: Nat) (goalId: Nat) (tactic: String): ProofM TacticResult := do
|
||||
let context ← get
|
||||
match context.states.get? stateId with
|
||||
| .none => return .invalid s!"Invalid state id {stateId}"
|
||||
| .some state =>
|
||||
match (← ProofM.runTermElabM' <| execute_tactic (env := context.env) (state := state.savedState) (goalId := goalId) (tactic := tactic)) with
|
||||
| .error errors =>
|
||||
return .failure errors
|
||||
| .ok nextState =>
|
||||
let nextId := context.states.size
|
||||
-- Return goals
|
||||
let goals ← ProofM.runTermElabM' <| extract_goals nextState
|
||||
|
||||
if goals.size = 0 then
|
||||
return .success 0 #[]
|
||||
else
|
||||
-- Create next proof state node
|
||||
let proofState: ProofState := {
|
||||
savedState := nextState,
|
||||
parent := stateId,
|
||||
parentGoalId := goalId
|
||||
}
|
||||
modify fun s => { s with states := s.states.push proofState }
|
||||
|
||||
return .success nextId goals
|
||||
|
||||
|
||||
end Pantograph.Meta
|
||||
|
|
@ -1,105 +0,0 @@
|
|||
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
|
||||
|
|
@ -0,0 +1,31 @@
|
|||
import Lean
|
||||
|
||||
/-
|
||||
Expression IO
|
||||
-/
|
||||
|
||||
|
||||
namespace Pantograph.Serial
|
||||
|
||||
|
||||
/-- Read a theorem from the environment -/
|
||||
def expr_from_const (env: Lean.Environment) (name: Lean.Name): Except String Lean.Expr :=
|
||||
match env.find? name with
|
||||
| none => throw s!"Symbol not found: {name}"
|
||||
| some cInfo => return cInfo.type
|
||||
def syntax_from_str (env: Lean.Environment) (s: String): Except String Lean.Syntax :=
|
||||
Lean.Parser.runParserCategory
|
||||
(env := env)
|
||||
(catName := `term)
|
||||
(input := s)
|
||||
(fileName := "<stdin>")
|
||||
|
||||
def expr_to_str (env: Lean.Environment) (coreContext: Lean.Core.Context) (expr: Lean.Expr): IO String := do
|
||||
let metaM := Lean.Meta.ppExpr expr
|
||||
let coreM : Lean.CoreM Lean.Format := metaM.run'
|
||||
let coreState : Lean.Core.State := { env := env }
|
||||
let (format, _) ← coreM.toIO coreContext coreState
|
||||
return format.pretty
|
||||
|
||||
|
||||
end Pantograph.Serial
|
||||
|
|
@ -5,7 +5,7 @@ import Lean.Declaration
|
|||
|
||||
namespace Pantograph
|
||||
|
||||
def strToName (s: String): Lean.Name :=
|
||||
def str_to_name (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 :=
|
||||
|
|
|
|||
21
README.md
21
README.md
|
|
@ -20,9 +20,10 @@ lake build mathlib
|
|||
## Usage
|
||||
|
||||
The binary must be run inside a `lake env` environment. i.e. `lake env
|
||||
build/bin/pantograph`. The REPL loop accepts commands and outputs either an
|
||||
`Error:` (indicating malformed command) or a json return value indicating the
|
||||
result of a command execution. The command can be passed in one of two formats
|
||||
build/bin/pantograph`. The REPL loop accepts commands as single-line JSON inputs
|
||||
and outputs either an `Error:` (indicating malformed command) or a json return
|
||||
value indicating the result of a command execution. The command can be passed in
|
||||
one of two formats
|
||||
```
|
||||
command { ... }
|
||||
{ "cmd": command, "payload": ... }
|
||||
|
|
@ -43,7 +44,18 @@ $ lake env build/bin/Pantograph
|
|||
create {"imports": ["Mathlib.Analysis.Seminorm"]}
|
||||
catalog {"id": 0}
|
||||
```
|
||||
|
||||
Example proving a theorem: (alternatively use `proof.start {"id": 0, "name": "aa", "copyFrom": "Nat.add_comm", "expr": ""}`) to prime the proof
|
||||
```
|
||||
$ lake env build/bin/Pantograph
|
||||
create {"imports": ["Init"]}
|
||||
proof.start {"id": 0, "name": "aa", "copyFrom": "", "expr": "∀ (n m : Nat), n + m = m + n"}
|
||||
proof.tactic {"treeId": 0, "stateId": 0, "goalId": 0, "tactic": "intro n m"}
|
||||
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"}
|
||||
proof.printTree {"treeId": 0}
|
||||
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "rw [Nat.add_comm]"}
|
||||
proof.printTree {"treeId": 0}
|
||||
```
|
||||
where the application of `assumption` should lead to a failure.
|
||||
|
||||
## Troubleshooting
|
||||
|
||||
|
|
@ -51,3 +63,4 @@ If lean encounters stack overflow problems when printing catalog, execute this b
|
|||
```sh
|
||||
ulimit -s unlimited
|
||||
```
|
||||
Due to a current bug in Lean (which existed in Lean 3), [the default value of structures are not honoured when parsing Json's](https://github.com/leanprover/lean4/issues/2225).
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
import Lake
|
||||
open Lake DSL
|
||||
|
||||
|
||||
package pantograph
|
||||
|
||||
require mathlib from git
|
||||
|
|
@ -23,9 +22,3 @@ lean_exe examples_proof {
|
|||
-- Somehow solves the native symbol not found problem
|
||||
supportInterpreter := true
|
||||
}
|
||||
|
||||
lean_exe examples_expr_io {
|
||||
root := `Examples.ExprIO
|
||||
-- Somehow solves the native symbol not found problem
|
||||
supportInterpreter := true
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue