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

chore: Version 0.3 #136

Open
aniva wants to merge 487 commits from dev into main
pull from: dev
merge into: aniva:main
Conversation 0 Commits 487 Files Changed 52 +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
Showing only changes of commit 6a81d83c1f - Show all commits

1
Pantograph/Protocol.lean
View File

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