Use TermElabM as the main monad stack instead of IO

This commit is contained in:
Leni Aniva 2023-05-23 05:12:46 -07:00
parent 94bc3355a2
commit 1fed222f56
6 changed files with 208 additions and 318 deletions

135
Main.lean
View File

@ -10,28 +10,14 @@ namespace Pantograph
structure Context where structure Context where
coreContext: Lean.Core.Context
/-- Stores state of the REPL -/ /-- Stores state of the REPL -/
structure State where structure State where
environments: Array Lean.Environment := #[] --environments: Array Lean.Environment := #[]
proofTrees: Array Meta.ProofTree := #[] proofTrees: Array Meta.ProofTree := #[]
-- State monad -- State monad
abbrev Subroutine := ReaderT Context (StateT State IO) abbrev Subroutine := ReaderT Context (StateT State Lean.Elab.TermElabM)
def State.getEnv (state: State) (id: Nat): Except String Lean.Environment :=
match state.environments.get? id with
| .some env => return env
| .none => throw s!"Invalid environment id {id}"
-- Utilities
def option_expect (o: Option α) (error: String): Except String α :=
match o with
| .some value => return value
| .none => throw error
open Commands open Commands
@ -52,20 +38,12 @@ def parse_command (s: String): Except String Command := do
unsafe def execute (command: Command): Subroutine Lean.Json := do def execute (command: Command): Subroutine Lean.Json := do
match command.cmd with match command.cmd with
| "create" =>
match Lean.fromJson? command.payload with
| .ok args => create args
| .error x => return errorJson x
| "catalog" => | "catalog" =>
match Lean.fromJson? command.payload with match Lean.fromJson? command.payload with
| .ok args => catalog args | .ok args => catalog args
| .error x => return errorJson x | .error x => return errorJson x
| "clear" =>
-- Delete all the environments
let ret ← clear
return Lean.toJson ret
| "inspect" => | "inspect" =>
match Lean.fromJson? command.payload with match Lean.fromJson? command.payload with
| .ok args => inspect args | .ok args => inspect args
@ -88,93 +66,49 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
where where
errorJson (s: String) := Lean.toJson ({ error := "json", desc := s }: InteractionError) errorJson (s: String) := Lean.toJson ({ error := "json", desc := s }: InteractionError)
errorIndex (s: String) := Lean.toJson ({ error := "index", desc := s }: InteractionError) errorIndex (s: String) := Lean.toJson ({ error := "index", desc := s }: InteractionError)
create (args: Create): Subroutine Lean.Json := do catalog (_: Catalog): Subroutine Lean.Json := do
let state ← get let env ← Lean.MonadEnv.getEnv
let envId := state.environments.size
let env ← Lean.importModules
(imports := args.imports.map (λ str => { module := str_to_name 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 Lean.toJson ({
envId := envId,
symbols := env.constants.size,
filtered_symbols := num_filtered_symbols }: CreateResult)
catalog (args: Catalog): Subroutine Lean.Json := do
let state ← get
match state.getEnv args.envId with
| .error error => return Lean.toJson <| errorIndex error
| .ok env =>
let names := env.constants.fold (init := []) (λ es name info => let names := env.constants.fold (init := []) (λ es name info =>
match to_filtered_symbol name info with match to_filtered_symbol name info with
| .some x => x::es | .some x => x::es
| .none => es) | .none => es)
return Lean.toJson <| ({ symbols := names }: CatalogResult) return Lean.toJson <| ({ symbols := names }: CatalogResult)
clear: Subroutine Lean.Json := do
let state ← get
let nEnv := state.environments.size
for env in state.environments do
env.freeRegions
set ({ }: State)
return Lean.toJson ({ nEnv := nEnv }: ClearResult)
inspect (args: Inspect): Subroutine Lean.Json := do inspect (args: Inspect): Subroutine Lean.Json := do
let context ← read let env ← Lean.MonadEnv.getEnv
let state ← get
match state.getEnv args.envId with
| .error error => return Lean.toJson <| errorIndex error
| .ok env =>
let name := str_to_name args.name let name := str_to_name args.name
let info? := env.find? name let info? := env.find? name
match info? with match info? with
| none => return Lean.toJson <| errorIndex s!"Symbol not found {args.name}" | none => return Lean.toJson <| errorIndex s!"Symbol not found {args.name}"
| some info => | some info =>
let format ← Serial.expr_to_str let format ← Lean.Meta.ppExpr info.toConstantVal.type
(env := env)
(coreContext := context.coreContext)
(expr := info.toConstantVal.type)
let module? := env.getModuleIdxFor? name >>= let module? := env.getModuleIdxFor? name >>=
(λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString (λ idx => env.allImportedModuleNames.get? idx.toNat) |>.map toString
return Lean.toJson ({ return Lean.toJson ({
type := format, type := toString format,
module? := module? module? := module?
}: InspectResult) }: InspectResult)
proof_start (args: ProofStart): Subroutine Lean.Json := do proof_start (args: ProofStart): Subroutine Lean.Json := do
let context ← read
let state ← get let state ← get
let ret?: Except Lean.Json Meta.ProofTree ← ExceptT.run <| (do let env ← Lean.MonadEnv.getEnv
let env ← match state.getEnv args.envId with let expr?: Except Lean.Json Lean.Expr ← (match args.expr, args.copyFrom with
| .error error => throw <| Lean.toJson <| errorIndex error
| .ok env => pure env
let tree := Meta.createProofTree
(name := args.name.getD "Untitled")
(env := env)
(coreContext := context.coreContext)
let expr: Lean.Expr ← match args.expr, args.copyFrom with
| .some expr, .none => | .some expr, .none =>
let syn ← match Serial.syntax_from_str env expr with (match Serial.syntax_from_str env expr with
| .error str => throw <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError) | .error str => return .error <| Lean.toJson ({ error := "parsing", desc := str }: InteractionError)
| .ok syn => pure syn | .ok syn => do
let expr: Lean.Expr ← match (← Meta.ProofM.syntax_to_expr syn |>.run' tree) with (match (← Meta.syntax_to_expr syn) with
| .error str => throw <| Lean.toJson ({ error := "elab", desc := str }: InteractionError) | .error str => return .error <| Lean.toJson ({ error := "elab", desc := str }: InteractionError)
| .ok expr => pure expr | .ok expr => return .ok expr))
pure expr
| .none, .some copyFrom => | .none, .some copyFrom =>
match Serial.expr_from_const env (name := str_to_name copyFrom) with (match env.find? <| str_to_name copyFrom with
| .error str => | .none => return .error <| errorIndex s!"Symbol not found: {copyFrom}"
IO.println "Symbol not found" | .some cInfo => return .ok cInfo.type)
throw <| errorIndex str
| .ok expr => pure expr
| .none, .none => | .none, .none =>
throw <| Lean.toJson ({ error := "arguments", desc := "At least one of {expr, copyFrom} must be supplied" }: InteractionError) return .error <| Lean.toJson ({ error := "arguments", desc := "At least one of {expr, copyFrom} must be supplied" }: InteractionError)
| _, _ => throw <| Lean.toJson ({ error := "arguments", desc := "Cannot populate both of {expr, copyFrom}" }: InteractionError) | _, _ => return .error <| Lean.toJson ({ error := "arguments", desc := "Cannot populate both of {expr, copyFrom}" }: InteractionError))
let (_, tree) := ← (Meta.ProofM.start expr |>.run tree) match expr? with
return tree
)
match ret? with
| .error error => return error | .error error => return error
| .ok tree => | .ok expr =>
let tree ← Meta.ProofTree.create (str_to_name <| args.name.getD "Untitled") expr
-- Put the new tree in the environment -- Put the new tree in the environment
let nextTreeId := state.proofTrees.size let nextTreeId := state.proofTrees.size
set { state with proofTrees := state.proofTrees.push tree } set { state with proofTrees := state.proofTrees.push tree }
@ -184,7 +118,7 @@ unsafe def execute (command: Command): Subroutine Lean.Json := do
match state.proofTrees.get? args.treeId with match state.proofTrees.get? args.treeId with
| .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}" | .none => return Lean.toJson <| errorIndex "Invalid tree index {args.treeId}"
| .some tree => | .some tree =>
let (result, nextTree) ← Meta.ProofM.execute let (result, nextTree) ← Meta.ProofTree.execute
(stateId := args.stateId) (stateId := args.stateId)
(goalId := args.goalId.getD 0) (goalId := args.goalId.getD 0)
(tactic := args.tactic) |>.run tree (tactic := args.tactic) |>.run tree
@ -221,19 +155,30 @@ unsafe def loop : Subroutine Unit := do
IO.println <| toString <| ret IO.println <| toString <| ret
loop loop
unsafe def main : IO Unit := do unsafe def main (args: List String): IO Unit := do
Lean.enableInitializersExecution Lean.enableInitializersExecution
Lean.initSearchPath (← Lean.findSysroot) Lean.initSearchPath (← Lean.findSysroot)
let env ← Lean.importModules
(imports := args.map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
let context: Context := { let context: Context := {
coreContext := { }
let coreContext: Lean.Core.Context := {
currNamespace := str_to_name "Aniva", currNamespace := str_to_name "Aniva",
openDecls := [], -- No 'open' directives needed openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>", fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] } fileMap := { source := "", positions := #[0], lines := #[1] }
} }
}
try try
loop.run context |>.run' {} let termElabM := loop.run context |>.run' {}
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run'
discard <| coreM.toIO coreContext { env := env }
catch ex => catch ex =>
IO.println "Uncaught IO exception" IO.println "Uncaught IO exception"
IO.println ex.toString IO.println ex.toString

View File

@ -16,32 +16,16 @@ structure InteractionError where
-- Individual command and return types -- Individual command and return types
-- Create a new environment using the given imports
structure Create where
imports : List String := []
deriving Lean.FromJson
structure CreateResult where
envId: Nat
symbols: Nat
filtered_symbols: Nat
deriving Lean.ToJson
-- Print all symbols in environment -- Print all symbols in environment
structure Catalog where structure Catalog where
envId: Nat
deriving Lean.FromJson deriving Lean.FromJson
structure CatalogResult where structure CatalogResult where
symbols: List String symbols: List String
deriving Lean.ToJson deriving Lean.ToJson
-- Reset the state of REPL
structure ClearResult where
nEnv: Nat -- Number of environments reset
deriving Lean.ToJson
-- Print the type of a symbol -- Print the type of a symbol
structure Inspect where structure Inspect where
envId: Nat -- Environment id
name: String name: String
deriving Lean.FromJson deriving Lean.FromJson
structure InspectResult where structure InspectResult where
@ -50,7 +34,6 @@ structure InspectResult where
deriving Lean.ToJson deriving Lean.ToJson
structure ProofStart where structure ProofStart where
envId: Nat -- Environment id
name: Option String -- Identifier of the proof name: Option String -- Identifier of the proof
-- Only one of the fields below may be populated. -- Only one of the fields below may be populated.
expr: Option String -- Proof expression expr: Option String -- Proof expression

View File

@ -22,133 +22,74 @@ def Lean.MessageLog.getErrorMessages (log : Lean.MessageLog) : Lean.MessageLog :
namespace Pantograph.Meta namespace Pantograph.Meta
structure ProofState where structure ProofState where
goals : List Lean.MVarId
savedState : Lean.Elab.Tactic.SavedState savedState : Lean.Elab.Tactic.SavedState
parent : Option Nat := none parent : Option Nat := none
parentGoalId : Nat := 0 parentGoalId : Nat := 0
structure ProofTree where structure ProofTree where
-- All parameters needed to run a `TermElabM` monad -- All parameters needed to run a `TermElabM` monad
name: Lean.Name name: Lean.Name
coreContext : Lean.Core.Context
elabContext : Lean.Elab.Term.Context
/-
This state must be saved so it preserves existing variable assignments. See
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Resume.20proof.20in.20IO.20monad/near/360429763
It is unknown what will happen to this in the case of backtracking. Since we
never delete any proof states, it should be fine to store this here for now. A
test case `Or.comm` illustrates branching which will fail if the core state is
replaced every time.
-/
coreState : Lean.Core.State
-- Set of proof states -- Set of proof states
states : Array ProofState := #[] states : Array ProofState := #[]
abbrev ProofM := StateRefT ProofTree IO abbrev M := Lean.Elab.TermElabM
def createProofTree (name: Lean.Name) (env: Lean.Environment) (coreContext: Lean.Core.Context): ProofTree := def ProofTree.create (name: Lean.Name) (expr: Lean.Expr): M ProofTree := do
{ let expr ← Lean.instantiateMVars expr
let goal := (← Lean.Meta.mkFreshExprMVar expr (kind := Lean.MetavarKind.synthetic))
let savedStateMonad: Lean.Elab.Tactic.TacticM Lean.Elab.Tactic.SavedState := Lean.MonadBacktrack.saveState
let savedState ← savedStateMonad { elaborator := .anonymous } |>.run' { goals := [goal.mvarId!]}
return {
name := name, name := name,
coreContext := coreContext, states := #[{
elabContext := { savedState := savedState,
declName? := some (name ++ "_pantograph"), goals := [goal.mvarId!]
errToSorry := false }]
}
coreState := {
env := env
}
} }
-- Tree structures -- Print the tree structures in readable form
def ProofTree.structure_array (tree: ProofTree): Array String := def ProofTree.structure_array (tree: ProofTree): Array String :=
tree.states.map λ state => match state.parent with tree.states.map λ state => match state.parent with
| .none => "" | .none => ""
| .some parent => s!"{parent}.{state.parentGoalId}" | .some parent => s!"{parent}.{state.parentGoalId}"
-- 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'
coreM.toIO context.coreContext context.coreState
def ProofM.runTermElabM' (termElabM: Lean.Elab.TermElabM α): ProofM α := do
let (ret, coreState) ← ProofM.runTermElabM termElabM
set { ← get with coreState := coreState }
return ret
-- Parsing syntax under the environment -- Parsing syntax under the environment
def ProofM.syntax_to_expr (syn: Lean.Syntax): ProofM (Except String Lean.Expr) := do def syntax_to_expr (syn: Lean.Syntax): Lean.Elab.TermElabM (Except String Lean.Expr) := do
let termElabM : Lean.Elab.TermElabM (Except String Lean.Expr) :=
try try
--let expr ← Lean.Elab.Term.elabTerm syn
-- (expectedType? := none)
-- (catchExPostpone := false)
-- (implicitLambda := true)
let expr ← Lean.Elab.Term.elabType syn let expr ← Lean.Elab.Term.elabType syn
-- Immediately synthesise all metavariables if we need to leave the elaboration context.
-- 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 -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing --Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing
let expr ← Lean.instantiateMVars expr let expr ← Lean.instantiateMVars expr
return .ok expr return .ok expr
catch ex => return .error (← ex.toMessageData.toString) 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 def execute_tactic (state: Lean.Elab.Tactic.SavedState) (goal: Lean.MVarId) (tactic: String) :
let mvar ← Lean.Meta.mkFreshExprMVar (some expr) (kind := Lean.MetavarKind.synthetic) M (Except (Array String) (Lean.Elab.Tactic.SavedState × List Lean.MVarId)):= do
let termState : Lean.Elab.Term.SavedState ← Lean.Elab.Term.saveState let tacticM (stx: Lean.Syntax): Lean.Elab.Tactic.TacticM (Except (Array String) (Lean.Elab.Tactic.SavedState × List Lean.MVarId)) := do
let tacticState : Lean.Elab.Tactic.SavedState := { term := termState, tactic := { goals := [mvar.mvarId!] }} state.restore
return tacticState Lean.Elab.Tactic.setGoals [goal]
/-- 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
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 =>
state.term.restore
try try
Lean.Elab.Term.synthesizeSyntheticMVarsNoPostponing Lean.Elab.Tactic.evalTactic stx
let unsolvedGoals ← Lean.Elab.Tactic.run mvarId tac
if (← getThe Lean.Core.State).messages.hasErrors then if (← getThe Lean.Core.State).messages.hasErrors then
let messages := (← getThe Lean.Core.State).messages.getErrorMessages |>.toList.toArray let messages := (← getThe Lean.Core.State).messages.getErrorMessages |>.toList.toArray
let errors ← (messages.map Lean.Message.data).mapM fun md => md.toString let errors ← (messages.map Lean.Message.data).mapM fun md => md.toString
return .error errors return .error errors
else else
unsolvedGoals.forM Lean.instantiateMVarDeclMVars return .ok (← Lean.MonadBacktrack.saveState, ← Lean.Elab.Tactic.getUnsolvedGoals)
let nextState : Lean.Elab.Tactic.SavedState := { catch exception =>
term := (← Lean.Elab.Term.saveState), return .error #[← exception.toMessageData.toString]
tactic := { goals := unsolvedGoals } match Lean.Parser.runParserCategory
} (env := ← Lean.MonadEnv.getEnv)
return .ok nextState (catName := `tactic)
catch ex => (input := tactic)
return .error #[← ex.toMessageData.toString] (fileName := "<stdin>") with
| Except.error err => return .error #[err]
| Except.ok stx => tacticM stx { elaborator := .anonymous } |>.run' state.tactic
def extract_goals (state: Lean.Elab.Tactic.SavedState): Lean.Elab.TermElabM (Array String) := do def goals_to_string (goals: List Lean.MVarId): M (Array String) := do
state.term.restore let goals ← goals.mapM fun g => do pure $ toString (← Lean.Meta.ppGoal g)
let goals ← state.tactic.goals.mapM fun g => do pure $ toString (← Lean.Meta.ppGoal g)
pure goals.toArray pure goals.toArray
@ -162,31 +103,29 @@ inductive TacticResult where
| failure (messages: Array String) | failure (messages: Array String)
/-- Execute tactic on given state -/ /-- Execute tactic on given state -/
def ProofM.execute (stateId: Nat) (goalId: Nat) (tactic: String): ProofM TacticResult := do def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT ProofTree M TacticResult := do
let context ← get let tree ← get
match context.states.get? stateId with match tree.states.get? stateId with
| .none => return .invalid s!"Invalid state id {stateId}" | .none => return .invalid s!"Invalid state id {stateId}"
| .some state => | .some state =>
match (← ProofM.runTermElabM' <| execute_tactic (env := context.coreState.env) (state := state.savedState) (goalId := goalId) (tactic := tactic)) with match state.goals.get? goalId with
| .none => return .invalid s!"Invalid goal id {goalId}"
| .some goal =>
match (← execute_tactic (state := state.savedState) (goal := goal) (tactic := tactic)) with
| .error errors => | .error errors =>
return .failure errors return .failure errors
| .ok nextState => | .ok (nextState, nextGoals) =>
let nextId := context.states.size let nextId := tree.states.size
-- Return goals if nextGoals.isEmpty then
let goals ← ProofM.runTermElabM' <| extract_goals nextState
if goals.size = 0 then
return .success .none #[] return .success .none #[]
else else
-- Create next proof state node
let proofState: ProofState := { let proofState: ProofState := {
savedState := nextState, savedState := nextState,
goals := nextGoals,
parent := stateId, parent := stateId,
parentGoalId := goalId parentGoalId := goalId
} }
modify fun s => { s with states := s.states.push proofState } modify fun s => { s with states := s.states.push proofState }
return .success (.some nextId) (← goals_to_string nextGoals)
return .success (.some nextId) goals
end Pantograph.Meta end Pantograph.Meta

View File

@ -20,12 +20,4 @@ def syntax_from_str (env: Lean.Environment) (s: String): Except String Lean.Synt
(input := s) (input := s)
(fileName := "<stdin>") (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 end Pantograph.Serial

View File

@ -31,24 +31,23 @@ command { ... }
The list of available commands can be found in `Pantograph/Commands.lean`. An The list of available commands can be found in `Pantograph/Commands.lean`. An
empty command aborts the REPL. empty command aborts the REPL.
The `Pantograph` executable must be run with a list of modules to import.
Example: (~5k symbols) Example: (~5k symbols)
``` ```
$ lake env build/bin/Pantograph $ lake env build/bin/Pantograph "Init"
create {"imports": ["Init"]} catalog
catalog {"envId": 0} inspect {"name": "Nat.le_add_left"}
inspect {"envId": 0, "name": "Nat.le_add_left"}
``` ```
Example with `mathlib` (~90k symbols) Example with `mathlib` (~90k symbols)
``` ```
$ lake env build/bin/Pantograph $ lake env build/bin/Pantograph "Mathlib.Analysis.Seminorm"
create {"imports": ["Mathlib.Analysis.Seminorm"]} catalog
catalog {"envId": 0}
``` ```
Example proving a theorem: (alternatively use `proof.start {"id": 0, "name": "aa", "copyFrom": "Nat.add_comm", "expr": ""}`) to prime the proof Example proving a theorem: (alternatively use `proof.start {"copyFrom": "Nat.add_comm"}`) to prime the proof
``` ```
$ lake env build/bin/Pantograph $ lake env build/bin/Pantograph "Init"
create {"imports": ["Init"]} proof.start {"expr": "∀ (n m : Nat), n + m = m + n"}
proof.start {"envId": 0, "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": 0, "goalId": 0, "tactic": "intro n m"}
proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"} proof.tactic {"treeId": 0, "stateId": 1, "goalId": 0, "tactic": "assumption"}
proof.printTree {"treeId": 0} proof.printTree {"treeId": 0}
@ -63,8 +62,6 @@ If lean encounters stack overflow problems when printing catalog, execute this b
```sh ```sh
ulimit -s unlimited 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).
## Testing ## Testing

View File

@ -9,28 +9,21 @@ inductive Start where
| copy (name: String) -- Start from some name in the environment | copy (name: String) -- Start from some name in the environment
| expr (expr: String) -- Start from some expression | expr (expr: String) -- Start from some expression
def start_proof (start: Start): IO (LSpec.TestSeq × Option Meta.ProofTree) := do abbrev M := Meta.M
let imports := ["Init"] abbrev TestM := StateRefT Meta.ProofTree M
let env: Lean.Environment ← Lean.importModules
(imports := imports.map (λ str => { module := str_to_name str, runtimeOnly := false })) def start_proof (start: Start): M (LSpec.TestSeq × Option Meta.ProofTree) := do
(opts := {}) let env ← Lean.MonadEnv.getEnv
(trustLevel := 1)
let state := Meta.createProofTree
(name := str_to_name "TestExample") env
(coreContext := {
currNamespace := str_to_name "Aniva",
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] }
})
let mut testSeq := LSpec.TestSeq.done let mut testSeq := LSpec.TestSeq.done
match start with match start with
| .copy name => | .copy name =>
let cInfo? := str_to_name name |> env.find? let cInfo? := str_to_name name |> env.find?
testSeq := testSeq ++ LSpec.check s!"Symbol exists {name}" cInfo?.isSome testSeq := testSeq ++ LSpec.check s!"Symbol exists {name}" cInfo?.isSome
match cInfo? with match cInfo? with
| .some cinfo => | .some cInfo =>
let (_, state) ← Meta.ProofM.start cinfo.type |>.run state let state ← Meta.ProofTree.create
(name := str_to_name "TestExample")
(expr := cInfo.type)
return (testSeq, Option.some state) return (testSeq, Option.some state)
| .none => | .none =>
return (testSeq, Option.none) return (testSeq, Option.none)
@ -42,21 +35,23 @@ def start_proof (start: Start): IO (LSpec.TestSeq × Option Meta.ProofTree) := d
IO.println error IO.println error
return (testSeq, Option.none) return (testSeq, Option.none)
| .ok syn => | .ok syn =>
let expr? := (← Meta.ProofM.syntax_to_expr syn |>.run' state) let expr? ← Meta.syntax_to_expr syn
testSeq := testSeq ++ LSpec.check s!"Elaborating" expr?.isOk testSeq := testSeq ++ LSpec.check s!"Elaborating" expr?.isOk
match expr? with match expr? with
| .error error => | .error error =>
IO.println error IO.println error
return (testSeq, Option.none) return (testSeq, Option.none)
| .ok expr => | .ok expr =>
let (_, state) ← Meta.ProofM.start expr |>.run state let state ← Meta.ProofTree.create
(name := str_to_name "TestExample")
(expr := expr)
return (testSeq, Option.some state) return (testSeq, Option.some state)
deriving instance DecidableEq, Repr for Meta.TacticResult deriving instance DecidableEq, Repr for Meta.TacticResult
def proof_step (stateId: Nat) (goalId: Nat) (tactic: String) def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
(expected: Meta.TacticResult) : Meta.ProofM LSpec.TestSeq := do (expected: Meta.TacticResult) : TestM LSpec.TestSeq := do
let result: Meta.TacticResult ← Meta.ProofM.execute stateId goalId tactic let result: Meta.TacticResult ← Meta.ProofTree.execute stateId goalId tactic
match expected, result with match expected, result with
| .success (.some i) #[], .success (.some _) goals => | .success (.some i) #[], .success (.some _) goals =>
-- If the goals are omitted but the next state is specified, we imply that -- If the goals are omitted but the next state is specified, we imply that
@ -65,22 +60,41 @@ def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected) return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected)
| _, _ => | _, _ =>
return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected) return LSpec.test s!"{stateId}.{goalId} {tactic}" (result = expected)
def proof_inspect (expected: Array String) : Meta.ProofM LSpec.TestSeq := do
let result := (← get).structure_array
return LSpec.test s!"Tree structure" (result = expected)
def proof_runner (start: Start) (steps: List (Meta.ProofM LSpec.TestSeq)): IO LSpec.TestSeq := do def proof_inspect (expected: Array String) : TestM LSpec.TestSeq := do
let result := (← get).structure_array
return LSpec.test s!"tree structure" (result = expected)
def proof_runner (env: Lean.Environment) (start: Start) (steps: List (TestM LSpec.TestSeq)): IO LSpec.TestSeq := do
let termElabM := do
let (testSeq, state?) ← start_proof start let (testSeq, state?) ← start_proof start
match state? with match state? with
| .none => return testSeq | .none => return testSeq
| .some state => steps.foldlM (fun tests m => do pure $ tests ++ (← m)) testSeq |>.run' state | .some state => steps.foldlM (fun tests m => do pure $ tests ++ (← m)) testSeq |>.run' state
let coreContext: Lean.Core.Context := {
currNamespace := str_to_name "Aniva",
openDecls := [], -- No 'open' directives needed
fileName := "<Pantograph>",
fileMap := { source := "", positions := #[0], lines := #[1] }
}
let metaM := termElabM.run' (ctx := {
declName? := some "_pantograph",
errToSorry := false
})
let coreM := metaM.run'
match ← (coreM.run' coreContext { env := env }).toBaseIO with
| .error exception =>
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok a => return a
example: ∀ (a b: Nat), a + b = b + a := by example: ∀ (a b: Nat), a + b = b + a := by
intro n m intro n m
rw [Nat.add_comm] rw [Nat.add_comm]
def proof_nat_add_comm: IO LSpec.TestSeq := def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq :=
let goal1 := "n m : Nat\n⊢ n + m = m + n" let goal1 := "n m : Nat\n⊢ n + m = m + n"
proof_runner (.copy "Nat.add_comm") [ proof_runner env (.copy "Nat.add_comm") [
proof_step 0 0 "intro n m" proof_step 0 0 "intro n m"
(.success (.some 1) #[goal1]), (.success (.some 1) #[goal1]),
proof_step 1 0 "assumption" proof_step 1 0 "assumption"
@ -88,9 +102,9 @@ def proof_nat_add_comm: IO LSpec.TestSeq :=
proof_step 1 0 "rw [Nat.add_comm]" proof_step 1 0 "rw [Nat.add_comm]"
(.success .none #[]) (.success .none #[])
] ]
def proof_nat_add_comm_manual: IO LSpec.TestSeq := do def proof_nat_add_comm_manual (env: Lean.Environment): IO LSpec.TestSeq := do
let goal1 := "n m : Nat\n⊢ n + m = m + n" let goal1 := "n m : Nat\n⊢ n + m = m + n"
proof_runner (.expr "∀ (a b: Nat), a + b = b + a") [ proof_runner env (.expr "∀ (a b: Nat), a + b = b + a") [
proof_step 0 0 "intro n m" proof_step 0 0 "intro n m"
(.success (.some 1) #[goal1]), (.success (.some 1) #[goal1]),
proof_step 1 0 "assumption" proof_step 1 0 "assumption"
@ -114,15 +128,15 @@ example: ∀ (p q: Prop), p q → q p := by
assumption assumption
. apply Or.inl . apply Or.inl
assumption assumption
def proof_or_comm: IO LSpec.TestSeq := do def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do
proof_runner (.expr "∀ (p q: Prop), p q → q p") [ proof_runner env (.expr "∀ (p q: Prop), p q → q p") [
proof_step 0 0 "intro p q h" proof_step 0 0 "intro p q h"
(.success (.some 1) #["p q : Prop\nh : p q\n⊢ q p"]), (.success (.some 1) #["p q : Prop\nh : p q\n⊢ q p"]),
proof_step 1 0 "cases h" proof_step 1 0 "cases h"
(.success (.some 2) #[]), (.success (.some 2) #[]),
proof_inspect #["", "0.0", "1.0"], proof_inspect #["", "0.0", "1.0"],
proof_step 2 0 "apply Or.inr" proof_step 2 0 "apply Or.inr"
(.success (.some 3) #[""]), (.success (.some 3) #[]),
proof_inspect #["", "0.0", "1.0", "2.0"], proof_inspect #["", "0.0", "1.0", "2.0"],
proof_step 3 0 "assumption" proof_step 3 0 "assumption"
(.success .none #[]), (.success .none #[]),
@ -130,14 +144,34 @@ def proof_or_comm: IO LSpec.TestSeq := do
(.success (.some 4) #[]), (.success (.some 4) #[]),
proof_step 4 0 "assumption" proof_step 4 0 "assumption"
(.success .none #[]), (.success .none #[]),
proof_inspect #["", "0.0", "1.0", "2.0", "1.1"] proof_inspect #["", "0.0", "1.0", "2.0", "2.1"]
]
example (w x y z : Nat) (p : Nat → Prop)
(h : p (x * y + z * w * x)) : p (x * w * z + y * x) := by
simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *
assumption
def proof_arith_1 (env: Lean.Environment): IO LSpec.TestSeq := do
proof_runner env (.expr "∀ (w x y z : Nat) (p : Nat → Prop) (h : p (x * y + z * w * x)), p (x * w * z + y * x)") [
proof_step 0 0 "intros"
(.success (.some 1) #[]),
proof_step 1 0 "simp [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, Nat.mul_comm, Nat.mul_assoc, Nat.mul_left_comm] at *"
(.success (.some 2) #[]),
proof_step 2 0 "assumption"
(.success .none #[])
] ]
def test_proofs : IO LSpec.TestSeq := do def test_proofs : IO LSpec.TestSeq := do
let env: Lean.Environment ← Lean.importModules
(imports := ["Init"].map (λ str => { module := str_to_name str, runtimeOnly := false }))
(opts := {})
(trustLevel := 1)
return LSpec.group "Proofs" $ return LSpec.group "Proofs" $
(LSpec.group "Nat.add_comm" $ (← proof_nat_add_comm)) ++ (LSpec.group "Nat.add_comm" $ (← proof_nat_add_comm env)) ++
(LSpec.group "Nat.add_comm manual" $ (← proof_nat_add_comm_manual)) ++ (LSpec.group "Nat.add_comm manual" $ (← proof_nat_add_comm_manual env)) ++
(LSpec.group "Or.comm" $ (← proof_or_comm)) (LSpec.group "Or.comm" $ (← proof_or_comm env)) ++
(LSpec.group "Arithmetic 1" $ (← proof_arith_1 env))
end Pantograph.Test end Pantograph.Test