From 572548c1bddc97eb4bd60b3898481b0f92aa2435 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 27 May 2023 23:10:39 -0700 Subject: [PATCH] Add json goal printing --- Main.lean | 6 ++-- Pantograph/Commands.lean | 4 +-- Pantograph/Meta.lean | 15 +++++---- Pantograph/Serial.lean | 67 ++++++++++++++++++++++++++++++++++++++++ Test/Proofs.lean | 33 +++++++++++++++----- 5 files changed, 105 insertions(+), 20 deletions(-) diff --git a/Main.lean b/Main.lean index 9481f2b..28b8126 100644 --- a/Main.lean +++ b/Main.lean @@ -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 diff --git a/Pantograph/Commands.lean b/Pantograph/Commands.lean index 7d0cb8f..b6442c4 100644 --- a/Pantograph/Commands.lean +++ b/Pantograph/Commands.lean @@ -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 diff --git a/Pantograph/Meta.lean b/Pantograph/Meta.lean index 9072195..3426628 100644 --- a/Pantograph/Meta.lean +++ b/Pantograph/Meta.lean @@ -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 diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 8304665..4b1c620 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -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 diff --git a/Test/Proofs.lean b/Test/Proofs.lean index 46c8c6a..52854d4 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -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) #[]),