max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: annotate syntheticness in info format

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-20 18:40:25 +01:00
parent 21a826ee51
commit b94c5c181c
1 changed files with 12 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/Elab/InfoTree.lean
View file

@ -108,17 +108,23 @@ def ContextInfo.toPPContext (info : ContextInfo) (lctx : LocalContext) : PPConte
def ContextInfo.ppSyntax (info : ContextInfo) (lctx : LocalContext) (stx : Syntax) : IO Format := do
ppTerm (info.toPPContext lctx) stx
private def formatStxRange (cinfo : ContextInfo) (stx : Syntax) : Format := do
let pos := stx.getPos?.getD 0
let endPos := stx.getTailPos?.getD pos
return f!"{fmtPos pos stx.getHeadInfo}-{fmtPos endPos stx.getTailInfo}"
where fmtPos pos info :=
let pos := format <| cinfo.fileMap.toPosition pos
match info with
| SourceInfo.original .. => pos
| _ => f!"{pos}†"
def TermInfo.format (cinfo : ContextInfo) (info : TermInfo) : IO Format := do
cinfo.runMetaM info.lctx do
let pos := info.stx.getPos?.getD 0
let endPos := info.stx.getTailPos?.getD pos
return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {cinfo.fileMap.toPosition pos}-{cinfo.fileMap.toPosition endPos}"
return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange cinfo info.stx}"
def FieldInfo.format (cinfo : ContextInfo) (info : FieldInfo) : IO Format := do
cinfo.runMetaM info.lctx do
let pos := info.stx.getPos?.getD 0
let endPos := info.stx.getTailPos?.getD pos
return f!"{info.name} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {cinfo.fileMap.toPosition pos}-{cinfo.fileMap.toPosition endPos}"
return f!"{info.name} : {← Meta.ppExpr (← Meta.inferType info.val)} := {← Meta.ppExpr info.val} @ {formatStxRange cinfo info.stx}"
def ContextInfo.ppGoals (cinfo : ContextInfo) (goals : List MVarId) : IO Format :=
if goals.isEmpty then