feat: Fetch declaration ranges for constants

main
Henrik Böving 2021-12-05 15:45:19 +01:00
parent 29a249e8fd
commit 7785c9f5bd
1 changed files with 15 additions and 7 deletions

View File

@ -17,6 +17,7 @@ def NameInfo.prettyPrint (i : NameInfo) : CoreM String := do
structure Info extends NameInfo where structure Info extends NameInfo where
doc : Option String doc : Option String
declarationRange : DeclarationRange
deriving Repr deriving Repr
structure AxiomInfo extends Info where structure AxiomInfo extends Info where
@ -90,7 +91,10 @@ def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let env ← getEnv let env ← getEnv
let type ← prettyPrintTerm v.type let type ← prettyPrintTerm v.type
let doc := findDocString? env v.name let doc := findDocString? env v.name
return Info.mk ⟨v.name, type⟩ doc match ←findDeclarationRanges? v.name with
-- TODO: Maybe selection range is more relevant? Figure this out in the future
| some range => return Info.mk ⟨v.name, type⟩ doc range.range
| none => panic! s!"{v.name} is a declaration without position"
def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
let info ← Info.ofConstantVal v.toConstantVal let info ← Info.ofConstantVal v.toConstantVal
@ -167,12 +171,16 @@ def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
namespace DocInfo namespace DocInfo
def isBlackListed (declName : Name) : MetaM Bool := do def isBlackListed (declName : Name) : MetaM Bool := do
let env ← getEnv match ←findDeclarationRanges? declName with
declName.isInternal | some _ =>
<||> isAuxRecursor env declName let env ← getEnv
<||> isNoConfusion env declName declName.isInternal
<||> isRec declName <||> isAuxRecursor env declName
<||> isMatcher declName <||> isNoConfusion env declName
<||> isRec declName
<||> isMatcher declName
-- TODO: Evaluate whether filtering out declarations without range is sensible
| none => true
-- TODO: Is this actually the best way? -- TODO: Is this actually the best way?
def isProjFn (declName : Name) : MetaM Bool := do def isProjFn (declName : Name) : MetaM Bool := do