Compare commits
No commits in common. "a811decf84ae09b5e3356e6923d7d831bbd71e7a" and "42c3da4a67de1fcff5fa1a25944b462ad91d007c" have entirely different histories.
a811decf84
...
42c3da4a67
|
@ -250,7 +250,6 @@ structure GoalDiag where
|
||||||
printNewMVars: Bool := false
|
printNewMVars: Bool := false
|
||||||
-- Print all mvars
|
-- Print all mvars
|
||||||
printAll: Bool := false
|
printAll: Bool := false
|
||||||
instantiate: Bool := true
|
|
||||||
|
|
||||||
|
|
||||||
end Pantograph.Protocol
|
end Pantograph.Protocol
|
||||||
|
|
|
@ -276,6 +276,9 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
|
||||||
mctx.decls.forM (fun mvarId decl => do
|
mctx.decls.forM (fun mvarId decl => do
|
||||||
if goals.contains mvarId || mvarId == root then
|
if goals.contains mvarId || mvarId == root then
|
||||||
pure ()
|
pure ()
|
||||||
|
-- Always print the root goal
|
||||||
|
else if mvarId == goalState.root then
|
||||||
|
printMVar (pref := ">") mvarId decl
|
||||||
-- Print the remainig ones that users don't see in Lean
|
-- Print the remainig ones that users don't see in Lean
|
||||||
else if options.printAll then
|
else if options.printAll then
|
||||||
let pref := if goalState.newMVars.contains mvarId then "~" else " "
|
let pref := if goalState.newMVars.contains mvarId then "~" else " "
|
||||||
|
@ -288,17 +291,11 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
|
||||||
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
|
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
|
||||||
if options.printContext then
|
if options.printContext then
|
||||||
decl.lctx.fvarIdToDecl.forM printFVar
|
decl.lctx.fvarIdToDecl.forM printFVar
|
||||||
let type ← if options.instantiate
|
let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
|
||||||
then instantiateMVars decl.type
|
|
||||||
else pure $ decl.type
|
|
||||||
let type_sexp ← serialize_expression_ast type (sanitize := false)
|
|
||||||
IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
|
IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
|
||||||
if options.printValue then
|
if options.printValue then
|
||||||
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
|
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
|
||||||
let value ← if options.instantiate
|
IO.println s!" = {← Meta.ppExpr value}"
|
||||||
then instantiateMVars value
|
|
||||||
else pure $ value
|
|
||||||
IO.println s!" := {← Meta.ppExpr value}"
|
|
||||||
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
|
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
|
||||||
IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
|
||||||
userNameToString : Name → String
|
userNameToString : Name → String
|
||||||
|
|
Loading…
Reference in New Issue