Merge pull request 'test: Option controlled mvar instantiation' (#44) from goal/diag into dev

Reviewed-on: #44
This commit is contained in:
Leni Aniva 2024-01-17 22:27:44 -08:00
commit a811decf84
2 changed files with 9 additions and 5 deletions

View File

@ -250,6 +250,7 @@ structure GoalDiag where
printNewMVars: Bool := false
-- Print all mvars
printAll: Bool := false
instantiate: Bool := true
end Pantograph.Protocol

View File

@ -276,9 +276,6 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
mctx.decls.forM (fun mvarId decl => do
if goals.contains mvarId || mvarId == root then
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
else if options.printAll then
let pref := if goalState.newMVars.contains mvarId then "~" else " "
@ -291,11 +288,17 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
printMVar (pref: String) (mvarId: MVarId) (decl: MetavarDecl): MetaM Unit := do
if options.printContext then
decl.lctx.fvarIdToDecl.forM printFVar
let type_sexp ← serialize_expression_ast (← instantiateMVars decl.type) (sanitize := false)
let type ← if options.instantiate
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}"
if options.printValue then
if let Option.some value := (← getMCtx).eAssignment.find? mvarId then
IO.println s!" = {← Meta.ppExpr value}"
let value ← if options.instantiate
then instantiateMVars value
else pure $ value
IO.println s!" := {← Meta.ppExpr value}"
printFVar (fvarId: FVarId) (decl: LocalDecl): MetaM Unit := do
IO.println s!" | {fvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type}"
userNameToString : Name → String