feat: Prograde tactics #83
|
@ -289,29 +289,31 @@ protected def GoalState.serializeGoals
|
||||||
|
|
||||||
/-- Print the metavariables in a readable format -/
|
/-- Print the metavariables in a readable format -/
|
||||||
@[export pantograph_goal_state_diag_m]
|
@[export pantograph_goal_state_diag_m]
|
||||||
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do
|
protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): CoreM String := do
|
||||||
goalState.restoreMetaM
|
let metaM: MetaM String := do
|
||||||
let savedState := goalState.savedState
|
goalState.restoreMetaM
|
||||||
let goals := savedState.tactic.goals
|
let savedState := goalState.savedState
|
||||||
let mctx ← getMCtx
|
let goals := savedState.tactic.goals
|
||||||
let root := goalState.root
|
let mctx ← getMCtx
|
||||||
-- Print the root
|
let root := goalState.root
|
||||||
let result: String ← match mctx.decls.find? root with
|
-- Print the root
|
||||||
| .some decl => printMVar ">" root decl
|
let result: String ← match mctx.decls.find? root with
|
||||||
| .none => pure s!">{root.name}: ??"
|
| .some decl => printMVar ">" root decl
|
||||||
let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
|
| .none => pure s!">{root.name}: ??"
|
||||||
match mctx.decls.find? mvarId with
|
let resultGoals ← goals.filter (· != root) |>.mapM (fun mvarId =>
|
||||||
| .some decl => printMVar "⊢" mvarId decl
|
match mctx.decls.find? mvarId with
|
||||||
| .none => pure s!"⊢{mvarId.name}: ??"
|
| .some decl => printMVar "⊢" mvarId decl
|
||||||
)
|
| .none => pure s!"⊢{mvarId.name}: ??"
|
||||||
let goals := goals.toSSet
|
)
|
||||||
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
|
let goals := goals.toSSet
|
||||||
!(goals.contains mvarId || mvarId == root) && options.printAll)
|
let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
|
||||||
|>.mapM (fun (mvarId, decl) => do
|
!(goals.contains mvarId || mvarId == root) && options.printAll)
|
||||||
let pref := if parentHasMVar mvarId then " " else "~"
|
|>.mapM (fun (mvarId, decl) => do
|
||||||
printMVar pref mvarId decl
|
let pref := if parentHasMVar mvarId then " " else "~"
|
||||||
)
|
printMVar pref mvarId decl
|
||||||
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
|
)
|
||||||
|
pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
|
||||||
|
metaM.run' {}
|
||||||
where
|
where
|
||||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
|
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM String := mvarId.withContext do
|
||||||
let resultFVars: List String ←
|
let resultFVars: List String ←
|
||||||
|
|
Loading…
Reference in New Issue