Add json goal printing

This commit is contained in:
Leni Aniva 2023-05-27 23:10:39 -07:00
parent 3e05722d1e
commit 4613777607
5 changed files with 105 additions and 20 deletions

View File

@ -72,10 +72,10 @@ def execute (command: Command): Subroutine Lean.Json := do
errorIndex := errorI "index" errorIndex := errorI "index"
catalog (_: Catalog): Subroutine Lean.Json := do catalog (_: Catalog): Subroutine Lean.Json := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv
let names := env.constants.fold (init := []) (λ es name info => let names := env.constants.fold (init := #[]) (λ acc name info =>
match to_filtered_symbol name info with match to_filtered_symbol name info with
| .some x => x::es | .some x => acc.push x
| .none => es) | .none => acc)
return Lean.toJson <| ({ symbols := names }: CatalogResult) return Lean.toJson <| ({ symbols := names }: CatalogResult)
inspect (args: Inspect): Subroutine Lean.Json := do inspect (args: Inspect): Subroutine Lean.Json := do
let env ← Lean.MonadEnv.getEnv let env ← Lean.MonadEnv.getEnv

View File

@ -28,7 +28,7 @@ structure InteractionError where
structure Catalog where structure Catalog where
deriving Lean.FromJson deriving Lean.FromJson
structure CatalogResult where structure CatalogResult where
symbols: List String symbols: Array String
deriving Lean.ToJson deriving Lean.ToJson
-- Print the type of a symbol -- Print the type of a symbol
@ -72,7 +72,7 @@ structure ProofTactic where
tactic: String tactic: String
deriving Lean.FromJson deriving Lean.FromJson
structure ProofTacticResultSuccess where structure ProofTacticResultSuccess where
goals: Array String goals: Array Goal
nextId?: Option Nat -- Next proof state id nextId?: Option Nat -- Next proof state id
deriving Lean.ToJson deriving Lean.ToJson
structure ProofTacticResultFailure where structure ProofTacticResultFailure where

View File

@ -1,7 +1,7 @@
import Lean import Lean
import Pantograph.Symbols import Pantograph.Symbols
import Pantograph.Serial
/- /-
The proof state manipulation system The proof state manipulation system
@ -78,17 +78,12 @@ def execute_tactic (state: Elab.Tactic.SavedState) (goal: MVarId) (tactic: Strin
| Except.error err => return .error #[err] | Except.error err => return .error #[err]
| Except.ok stx => tacticM stx { elaborator := .anonymous } |>.run' state.tactic | Except.ok stx => tacticM stx { elaborator := .anonymous } |>.run' state.tactic
def goals_to_string (goals: List MVarId): M (Array String) := do
let goals ← goals.mapM fun g => do pure $ toString (← Meta.ppGoal g)
pure goals.toArray
/-- Response for executing a tactic -/ /-- Response for executing a tactic -/
inductive TacticResult where inductive TacticResult where
-- Invalid id -- Invalid id
| invalid (message: String): TacticResult | invalid (message: String): TacticResult
-- Goes to next state -- Goes to next state
| success (nextId?: Option Nat) (goals: Array String) | success (nextId?: Option Nat) (goals: Array Goal)
-- Fails with messages -- Fails with messages
| failure (messages: Array String) | failure (messages: Array String)
@ -116,6 +111,10 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT P
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) let goals ← nextGoals.mapM fun mvarId => do
match (← MonadMCtx.getMCtx).findDecl? mvarId with
| .some mvarDecl => serialize_goal mvarDecl
| .none => throwError mvarId
return .success (.some nextId) goals.toArray
end Pantograph end Pantograph

View File

@ -41,4 +41,71 @@ def type_expr_to_bound (expr: Expr): MetaM BoundExpression := do
return { binders, target := toString (← Meta.ppExpr body) } return { binders, target := toString (← Meta.ppExpr body) }
structure Variable where
name: String
/-- Does the name contain a dagger -/
isInaccessible: Bool := false
type: String
value?: Option String := .none
deriving ToJson
structure Goal where
/-- String case id -/
caseName?: Option String := .none
/-- Is the goal in conversion mode -/
isConversion: Bool := false
/-- target expression type -/
target: String
/-- Variables -/
vars: Array Variable := #[]
deriving ToJson
/-- Adapted from ppGoal -/
def serialize_goal (mvarDecl: MetavarDecl) : MetaM Goal := do
-- Options for printing; See Meta.ppGoal for details
let showLetValues := True
let ppAuxDecls := false
let ppImplDetailHyps := false
let lctx := mvarDecl.lctx
let lctx := lctx.sanitizeNames.run' { options := (← getOptions) }
Meta.withLCtx lctx mvarDecl.localInstances do
let rec ppVars (localDecl : LocalDecl) : MetaM Variable := do
match localDecl with
| .cdecl _ _ varName type _ _ =>
let varName := varName.simpMacroScopes
let type ← instantiateMVars type
return {
name := toString varName,
isInaccessible := varName.isInaccessibleUserName,
type := toString <| ← Meta.ppExpr type
}
| .ldecl _ _ varName type val _ _ => do
let varName := varName.simpMacroScopes
let type ← instantiateMVars type
let value? ← if showLetValues then
let val ← instantiateMVars val
pure $ .some <| toString <| (← Meta.ppExpr val)
else
pure $ .none
return {
name := toString varName,
isInaccessible := varName.isInaccessibleUserName,
type := toString <| ← Meta.ppExpr type
value? := value?
}
let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
let skip := !ppAuxDecls && localDecl.isAuxDecl || !ppImplDetailHyps && localDecl.isImplementationDetail
if skip then
return acc
else
let var ← ppVars localDecl
return var::acc
return {
caseName? := match mvarDecl.userName with
| Name.anonymous => .none
| name => .some <| toString name,
isConversion := "| " == (Meta.getGoalPrefix mvarDecl)
target := toString <| (← Meta.ppExpr (← instantiateMVars mvarDecl.type)),
vars := vars.reverse.toArray
}
end Pantograph end Pantograph

View File

@ -47,6 +47,8 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
(expr := expr) (expr := expr)
return (testSeq, Option.some state) return (testSeq, Option.some state)
deriving instance DecidableEq, Repr for Variable
deriving instance DecidableEq, Repr for Goal
deriving instance DecidableEq, Repr for TacticResult deriving instance DecidableEq, Repr for TacticResult
def proof_step (stateId: Nat) (goalId: Nat) (tactic: String) def proof_step (stateId: Nat) (goalId: Nat) (tactic: String)
@ -88,27 +90,35 @@ def proof_runner (env: Lean.Environment) (start: Start) (steps: List (TestM LSpe
return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "") return LSpec.test "Exception" (s!"internal exception #{← exception.toMessageData.toString}" = "")
| .ok a => return a | .ok a => return a
def build_goal (nameType: List (String × String)) (target: String): Goal :=
{
target := target,
vars := (nameType.map fun x => ({ name := x.fst, type := x.snd }: Variable)).toArray
}
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 (env: Lean.Environment): IO LSpec.TestSeq := def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do
let goal1 := "n m : Nat\n⊢ n + m = m + n" let goal1: Goal := {
target := "n + m = m + n",
vars := #[{ name := "n", type := "Nat" }, { name := "m", type := "Nat" }]
}
proof_runner env (.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"
(.failure #[s!"tactic 'assumption' failed\n{goal1}"]), (.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]),
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 (env: Lean.Environment): 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: Goal := build_goal [("n", "Nat"), ("m", "Nat")] "n + m = m + n"
proof_runner env (.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"
(.failure #[s!"tactic 'assumption' failed\n{goal1}"]), (.failure #[s!"tactic 'assumption' failed\nn m : Nat\n⊢ n + m = m + n"]),
proof_step 1 0 "rw [Nat.add_comm]" proof_step 1 0 "rw [Nat.add_comm]"
(.success .none #[]) (.success .none #[])
] ]
@ -129,11 +139,20 @@ example: ∀ (p q: Prop), p q → q p := by
. apply Or.inl . apply Or.inl
assumption assumption
def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do def proof_or_comm (env: Lean.Environment): IO LSpec.TestSeq := do
let branchGoal (caseName name: String): Goal := {
caseName? := .some caseName,
target := "q p",
vars := #[
{ name := "p", type := "Prop" },
{ name := "q", type := "Prop" },
{ name := "h✝", type := name, isInaccessible := true }
]
}
proof_runner env (.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) #[build_goal [("p", "Prop"), ("q", "Prop"), ("h", "p q")] "q p"]),
proof_step 1 0 "cases h" proof_step 1 0 "cases h"
(.success (.some 2) #[]), (.success (.some 2) #[branchGoal "inl" "p", branchGoal "inr" "q"]),
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) #[]),