aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

test: Option controlled mvar instantiation #44

Merged
aniva merged 2 commits from goal/diag into dev 2024-01-17 22:27:44 -08:00
Conversation 0 Commits 2 Files Changed 2 +9 -5
2 changed files with 9 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
Pantograph/Protocol.lean
View File

@ -250,6 +250,7 @@ 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

13
Pantograph/Serial.lean
View File

@ -276,9 +276,6 @@ 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 " "
@ -291,11 +288,17 @@ 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_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}" 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
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 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