From 41241bfa40465d313e03959202668fc88bdfb7f9 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sun, 21 May 2023 17:41:39 -0700 Subject: [PATCH] Add REPL tactics --- Examples/ExprIO.lean | 25 ------ Examples/Proof.lean | 68 ++++++++++------ Main.lean | 108 +++++++++++++++++++------ Pantograph/Commands.lean | 33 +++++++- Pantograph/IO.lean | 19 ----- Pantograph/Meta.lean | 169 +++++++++++++++++++++++++++++++++++++++ Pantograph/Proofs.lean | 105 ------------------------ Pantograph/Serial.lean | 31 +++++++ Pantograph/Symbols.lean | 2 +- README.md | 21 ++++- lakefile.lean | 7 -- 11 files changed, 378 insertions(+), 210 deletions(-) delete mode 100644 Examples/ExprIO.lean delete mode 100644 Pantograph/IO.lean create mode 100644 Pantograph/Meta.lean delete mode 100644 Pantograph/Proofs.lean create mode 100644 Pantograph/Serial.lean diff --git a/Examples/ExprIO.lean b/Examples/ExprIO.lean deleted file mode 100644 index efc8522..0000000 --- a/Examples/ExprIO.lean +++ /dev/null @@ -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 := "") with - | Except.error error => IO.println s!"{error}" - | Except.ok (syn: Lean.Syntax) => - let reprint := Lean.Syntax.reprint syn |>.get! - IO.println reprint diff --git a/Examples/Proof.lean b/Examples/Proof.lean index 51530d0..bafe406 100644 --- a/Examples/Proof.lean +++ b/Examples/Proof.lean @@ -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 - 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 +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 := "", + 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 (result, state) ← Meta.ProofM.execute 0 tactic |>.run state + IO.println s! "Executed {tactic}, Response: [{serialise result}]" + let tactic := "assumption" -- should fail + 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 (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 diff --git a/Main.lean b/Main.lean index 24b802a..5fbb411 100644 --- a/Main.lean +++ b/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 := "", fileMap := { source := "", positions := #[0], lines := #[1] } } } - loop.run context |>.run' {} + try + loop.run context |>.run' {} + catch ex => + IO.println "Uncaught IO exception" + IO.println ex.toString diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 1563d3d..358b937 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -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 diff --git a/Pantograph/IO.lean b/Pantograph/IO.lean deleted file mode 100644 index 6391b77..0000000 --- a/Pantograph/IO.lean +++ /dev/null @@ -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 diff --git a/Pantograph/Meta.lean b/Pantograph/Meta.lean new file mode 100644 index 0000000..ccda3d6 --- /dev/null +++ b/Pantograph/Meta.lean @@ -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 := "") 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 diff --git a/Pantograph/Proofs.lean b/Pantograph/Proofs.lean deleted file mode 100644 index b79f890..0000000 --- a/Pantograph/Proofs.lean +++ /dev/null @@ -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 := "", - 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 := "") 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 diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean new file mode 100644 index 0000000..8616381 --- /dev/null +++ b/Pantograph/Serial.lean @@ -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 := "") + +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 diff --git a/Pantograph/Symbols.lean b/Pantograph/Symbols.lean index 3f8ad58..641a276 100644 --- a/Pantograph/Symbols.lean +++ b/Pantograph/Symbols.lean @@ -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 := diff --git a/README.md b/README.md index eb66b9a..3a11a34 100644 --- a/README.md +++ b/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). diff --git a/lakefile.lean b/lakefile.lean index a49f77a..62ca33c 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -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 -}