From e246fd961fbf7c41798bcace4f33952f00f4581e Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 17 May 2023 21:58:03 -0700 Subject: [PATCH] Add tactic state manipulation --- Examples/Proof.lean | 40 +++++++++++++++ Main.lean | 95 ++++++++++++++++++----------------- Pantograph/Commands.lean | 16 ++++-- Pantograph/Proofs.lean | 105 +++++++++++++++++++++++++++++++++++++++ Pantograph/Symbols.lean | 3 ++ lakefile.lean | 6 +++ 6 files changed, 216 insertions(+), 49 deletions(-) create mode 100644 Examples/Proof.lean create mode 100644 Pantograph/Proofs.lean diff --git a/Examples/Proof.lean b/Examples/Proof.lean new file mode 100644 index 0000000..c4e18f1 --- /dev/null +++ b/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] diff --git a/Main.lean b/Main.lean index 7c159a3..9daf2f5 100644 --- a/Main.lean +++ b/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,48 +27,7 @@ structure Command where payload: Lean.Json deriving Lean.FromJson -namespace Commands - -def create (args: Create): Subroutine CreateResult := do - let state ← get - let id := nextId state - let env ← Lean.importModules - (imports := args.imports.map strTransform) - (opts := {}) - (trustLevel := 1) - modify fun s => { environments := s.environments.push env } - let num_filtered_symbols := env.constants.fold (init := 0) (λ acc name info => - acc + if is_symbol_unsafe_or_internal name info then 0 else 1) - return { - 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 - let state ← get - match state.environments.get? args.id with - | .some env => - let names := env.constants.fold (init := []) (λ es name info => - match to_filtered_symbol name info with - | .some x => x::es - | .none => es) - return { theorems := names } - | .none => throw s!"Invalid environment id {args.id}" - -unsafe def clear: Subroutine ClearResult := do - let state ← get - for env in state.environments do - env.freeRegions - return { n := state.environments.size } - -end Commands -end Pantograph - -open Pantograph +open Commands unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do let obj ← Lean.Json.parse command @@ -75,17 +35,62 @@ unsafe def execute (command: String): ExceptT String (T IO) Lean.Json := do match command.cmd with | "create" => let args: Commands.Create ← Lean.fromJson? command.payload - let ret ← Commands.create args + let ret ← create args return Lean.toJson ret | "catalog" => let args: Commands.Catalog ← Lean.fromJson? command.payload - let ret ← Commands.catalog args + let ret ← catalog args return Lean.toJson ret | "clear" => -- Delete all the environments - let ret ← Commands.clear + 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 (λ str => { module := strToName str, runtimeOnly := false })) + (opts := {}) + (trustLevel := 1) + modify fun s => { environments := s.environments.push env } + let num_filtered_symbols := env.constants.fold (init := 0) (λ acc name info => + acc + if is_symbol_unsafe_or_internal name info then 0 else 1) + return { + id := id, + symbols := env.constants.size, + filtered_symbols := num_filtered_symbols } + catalog (args: Catalog): Subroutine CatalogResult := do + let state ← get + match state.environments.get? args.id with + | .some env => + let names := env.constants.fold (init := []) (λ es name info => + match to_filtered_symbol name info with + | .some x => x::es + | .none => es) + return { theorems := names } + | .none => throw s!"Invalid environment id {args.id}" + 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 Pantograph + +open Pantograph + -- Main IO functions diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 675a2cf..d6b62f3 100644 --- a/Pantograph/Commands.lean +++ b/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 diff --git a/Pantograph/Proofs.lean b/Pantograph/Proofs.lean new file mode 100644 index 0000000..b79f890 --- /dev/null +++ b/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 := "", + 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/Symbols.lean b/Pantograph/Symbols.lean index 97dafc7..3f8ad58 100644 --- a/Pantograph/Symbols.lean +++ b/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" diff --git a/lakefile.lean b/lakefile.lean index d3acec1..a642187 100644 --- a/lakefile.lean +++ b/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 +}