Merge pull request 'feat: Print parent expression assignment' (#45) from goal/relation into dev
Reviewed-on: #45
This commit is contained in:
commit
3292b34070
|
@ -206,8 +206,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
|
|||
| .some goalState => runMetaM <| do
|
||||
goalState.restoreMetaM
|
||||
let root? ← goalState.rootExpr?.mapM (λ expr => serialize_expression state.options expr)
|
||||
let parent? ← goalState.parentExpr?.mapM (λ expr => serialize_expression state.options expr)
|
||||
return .ok {
|
||||
root?,
|
||||
parent?,
|
||||
}
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -7,8 +7,6 @@ open Pantograph
|
|||
|
||||
namespace Pantograph.Environment
|
||||
|
||||
abbrev CR α := Except Protocol.InteractionError α
|
||||
|
||||
def is_symbol_unsafe_or_internal (n: Lean.Name) (info: Lean.ConstantInfo): Bool :=
|
||||
isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ info.isUnsafe
|
||||
where
|
||||
|
@ -32,14 +30,14 @@ def to_filtered_symbol (n: Lean.Name) (info: Lean.ConstantInfo): Option String :
|
|||
if is_symbol_unsafe_or_internal n info
|
||||
then Option.none
|
||||
else Option.some <| to_compact_symbol_name n info
|
||||
def catalog (_: Protocol.EnvCatalog): CoreM (CR Protocol.EnvCatalogResult) := do
|
||||
def catalog (_: Protocol.EnvCatalog): CoreM (Protocol.CR Protocol.EnvCatalogResult) := do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let names := env.constants.fold (init := #[]) (λ acc name info =>
|
||||
match to_filtered_symbol name info with
|
||||
| .some x => acc.push x
|
||||
| .none => acc)
|
||||
return .ok { symbols := names }
|
||||
def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR Protocol.EnvInspectResult) := do
|
||||
def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (Protocol.CR Protocol.EnvInspectResult) := do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let name := args.name.toName
|
||||
let info? := env.find? name
|
||||
|
@ -90,7 +88,7 @@ def inspect (args: Protocol.EnvInspect) (options: Protocol.Options): CoreM (CR P
|
|||
} }
|
||||
| _ => core
|
||||
return .ok result
|
||||
def addDecl (args: Protocol.EnvAdd): CoreM (CR Protocol.EnvAddResult) := do
|
||||
def addDecl (args: Protocol.EnvAdd): CoreM (Protocol.CR Protocol.EnvAddResult) := do
|
||||
let env ← Lean.MonadEnv.getEnv
|
||||
let tvM: Elab.TermElabM (Except String (Expr × Expr)) := do
|
||||
let type ← match syntax_from_str env args.type with
|
||||
|
|
|
@ -1,3 +1,4 @@
|
|||
import Pantograph.Protocol
|
||||
import Lean
|
||||
|
||||
def Lean.MessageLog.getErrorMessages (log : MessageLog) : MessageLog :=
|
||||
|
@ -20,6 +21,9 @@ structure GoalState where
|
|||
-- The id of the goal in the parent
|
||||
parentGoalId: Nat := 0
|
||||
|
||||
-- Parent state metavariable source
|
||||
parentMVar: Option MVarId
|
||||
|
||||
abbrev M := Elab.TermElabM
|
||||
|
||||
protected def GoalState.create (expr: Expr): M GoalState := do
|
||||
|
@ -36,6 +40,7 @@ protected def GoalState.create (expr: Expr): M GoalState := do
|
|||
savedState,
|
||||
root,
|
||||
newMVars := SSet.insert .empty root,
|
||||
parentMVar := .none,
|
||||
}
|
||||
protected def GoalState.goals (state: GoalState): List MVarId := state.savedState.tactic.goals
|
||||
|
||||
|
@ -114,10 +119,11 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tactic: String
|
|||
return acc.insert mvarId
|
||||
) SSet.empty
|
||||
return .success {
|
||||
state with
|
||||
root := state.root,
|
||||
savedState := nextSavedState
|
||||
newMVars,
|
||||
parentGoalId := goalId,
|
||||
parentMVar := .some goal,
|
||||
}
|
||||
|
||||
protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String): M TacticResult := do
|
||||
|
@ -164,10 +170,11 @@ protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String
|
|||
Elab.Tactic.setGoals (← newMVars.filterM (λ mvar => do pure !(← mvar.isAssigned)))
|
||||
let nextSavedState ← MonadBacktrack.saveState
|
||||
return .success {
|
||||
state with
|
||||
root := state.root,
|
||||
savedState := nextSavedState,
|
||||
newMVars := newMVars.toSSet,
|
||||
parentGoalId := goalId,
|
||||
parentMVar := .some goal,
|
||||
}
|
||||
catch exception =>
|
||||
return .failure #[← exception.toMessageData.toString]
|
||||
|
@ -203,8 +210,8 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
|
|||
else
|
||||
target.resume (goals := branch.goals)
|
||||
|
||||
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
|
||||
let expr := goalState.mctx.eAssignment.find! goalState.root
|
||||
protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
|
||||
let expr ← goalState.mctx.eAssignment.find? goalState.root
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
if expr.hasMVar then
|
||||
-- Must not assert that the goal state is empty here. We could be in a branch goal.
|
||||
|
@ -212,6 +219,12 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr :=
|
|||
.none
|
||||
else
|
||||
assert! goalState.goals.isEmpty
|
||||
.some expr
|
||||
return expr
|
||||
protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
|
||||
let parent ← goalState.parentMVar
|
||||
let expr := goalState.mctx.eAssignment.find! parent
|
||||
let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
|
||||
return expr
|
||||
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -240,7 +240,9 @@ structure GoalPrint where
|
|||
deriving Lean.FromJson
|
||||
structure GoalPrintResult where
|
||||
-- The root expression
|
||||
root?: Option Expression
|
||||
root?: Option Expression := .none
|
||||
-- The filling expression of the parent goal
|
||||
parent?: Option Expression := .none
|
||||
deriving Lean.ToJson
|
||||
|
||||
-- Diagnostic Options, not available in REPL
|
||||
|
@ -252,5 +254,6 @@ structure GoalDiag where
|
|||
printAll: Bool := false
|
||||
instantiate: Bool := true
|
||||
|
||||
abbrev CR α := Except InteractionError α
|
||||
|
||||
end Pantograph.Protocol
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
namespace Pantograph
|
||||
|
||||
def version := "0.2.10-alpha"
|
||||
def version := "0.2.12-alpha"
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -210,6 +210,8 @@ def proof_or_comm: TestM Unit := do
|
|||
| .none => do
|
||||
addTest $ assertUnreachable "Goal could not parse"
|
||||
return ()
|
||||
addTest $ LSpec.check "(0 parent)" state0.parentExpr?.isNone
|
||||
addTest $ LSpec.check "(0 root)" state0.rootExpr?.isNone
|
||||
|
||||
let state1 ← match ← state0.execute (goalId := 0) (tactic := "intro p q h") with
|
||||
| .success state => pure state
|
||||
|
@ -218,6 +220,8 @@ def proof_or_comm: TestM Unit := do
|
|||
return ()
|
||||
addTest $ LSpec.check "intro n m" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[buildGoal [("p", "Prop"), ("q", "Prop"), ("h", "p ∨ q")] "q ∨ p"])
|
||||
addTest $ LSpec.check "(1 parent)" state1.parentExpr?.isSome
|
||||
addTest $ LSpec.check "(1 root)" state1.rootExpr?.isNone
|
||||
let state2 ← match ← state1.execute (goalId := 0) (tactic := "cases h") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
|
@ -225,12 +229,21 @@ def proof_or_comm: TestM Unit := do
|
|||
return ()
|
||||
addTest $ LSpec.check "cases h" ((← state2.serializeGoals (options := ← read)).map (·.devolatilize) =
|
||||
#[branchGoal "inl" "p", branchGoal "inr" "q"])
|
||||
addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
|
||||
addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
|
||||
|
||||
let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false)
|
||||
-- This is due to delayed assignment
|
||||
addTest $ LSpec.test "(2 parent)" (state2parent ==
|
||||
"((:mv _uniq.45) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
|
||||
|
||||
let state3_1 ← match ← state2.execute (goalId := 0) (tactic := "apply Or.inr") with
|
||||
| .success state => pure state
|
||||
| other => do
|
||||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false)
|
||||
addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.83))")
|
||||
addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
|
||||
let state4_1 ← match ← state3_1.execute (goalId := 0) (tactic := "assumption") with
|
||||
| .success state => pure state
|
||||
|
@ -238,6 +251,8 @@ def proof_or_comm: TestM Unit := do
|
|||
addTest $ assertUnreachable $ other.toString
|
||||
return ()
|
||||
addTest $ LSpec.check " assumption" state4_1.goals.isEmpty
|
||||
let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false)
|
||||
addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.49)")
|
||||
addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
|
||||
let state3_2 ← match ← state2.execute (goalId := 1) (tactic := "apply Or.inl") with
|
||||
| .success state => pure state
|
||||
|
|
Loading…
Reference in New Issue