Add json goal printing

This commit is contained in:
Leni Aniva 2023-05-27 23:10:39 -07:00
parent 9fe3f62371
commit 572548c1bd
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"
catalog (_: Catalog): Subroutine Lean.Json := do
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
| .some x => x::es
| .none => es)
| .some x => acc.push x
| .none => acc)
return Lean.toJson <| ({ symbols := names }: CatalogResult)
inspect (args: Inspect): Subroutine Lean.Json := do
let env ← Lean.MonadEnv.getEnv

View File

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

View File

@ -1,7 +1,7 @@
import Lean
import Pantograph.Symbols
import Pantograph.Serial
/-
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.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 -/
inductive TacticResult where
-- Invalid id
| invalid (message: String): TacticResult
-- Goes to next state
| success (nextId?: Option Nat) (goals: Array String)
| success (nextId?: Option Nat) (goals: Array Goal)
-- Fails with messages
| failure (messages: Array String)
@ -116,6 +111,10 @@ def ProofTree.execute (stateId: Nat) (goalId: Nat) (tactic: String): StateRefT P
parentGoalId := goalId
}
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

View File

@ -41,4 +41,71 @@ def type_expr_to_bound (expr: Expr): MetaM BoundExpression := do
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

View File

@ -47,6 +47,8 @@ def start_proof (start: Start): M (LSpec.TestSeq × Option ProofTree) := do
(expr := expr)
return (testSeq, Option.some state)
deriving instance DecidableEq, Repr for Variable
deriving instance DecidableEq, Repr for Goal
deriving instance DecidableEq, Repr for TacticResult
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}" = "")
| .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
intro n m
rw [Nat.add_comm]
def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq :=
let goal1 := "n m : Nat\n⊢ n + m = m + n"
def proof_nat_add_comm (env: Lean.Environment): IO LSpec.TestSeq := do
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_step 0 0 "intro n m"
(.success (.some 1) #[goal1]),
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]"
(.success .none #[])
]
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_step 0 0 "intro n m"
(.success (.some 1) #[goal1]),
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]"
(.success .none #[])
]
@ -129,11 +139,20 @@ example: ∀ (p q: Prop), p q → q p := by
. apply Or.inl
assumption
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_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"
(.success (.some 2) #[]),
(.success (.some 2) #[branchGoal "inl" "p", branchGoal "inr" "q"]),
proof_inspect #["", "0.0", "1.0"],
proof_step 2 0 "apply Or.inr"
(.success (.some 3) #[]),