fix: First miss-handling of free variables

main
Henrik Böving 2023-10-17 20:21:14 +02:00
parent f15d561411
commit bc9cba13b1
1 changed files with 35 additions and 31 deletions

View File

@ -15,38 +15,42 @@ def NameInfo.ofTypedName (n : Name) (t : Expr) : MetaM NameInfo := do
let env ← getEnv let env ← getEnv
return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n} return { name := n, type := ← prettyPrintTerm t, doc := ← findDocString? env n}
partial def typeToArgsType (e : Expr) : (Array ((Option Name) × Expr × BinderInfo) × Expr) := partial def argTypeTelescope {α : Type} (e : Expr) (k : Array ((Option Name) × Expr × BinderInfo) → Expr → MetaM α) : MetaM α :=
let helper := fun name type body data => go e #[]
-- Once we hit a name with a macro scope we stop traversing the expression where
-- and print what is left after the : instead. The only exception go (e : Expr) (args : Array ((Option Name) × Expr × BinderInfo)) : MetaM α := do
-- to this is instances since these almost never have a name let helper := fun name type body bi =>
-- but should still be printed as arguments instead of after the :. -- Once we hit a name with a macro scope we stop traversing the expression
if data.isInstImplicit && name.hasMacroScopes then -- and print what is left after the : instead. The only exception
let arg := (none, type, data) -- to this is instances since these almost never have a name
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩)) -- but should still be printed as arguments instead of after the :.
(#[arg] ++ args, final) if bi.isInstImplicit && name.hasMacroScopes then
else if name.hasMacroScopes then let arg := (none, type, bi)
(#[], e) Meta.withLocalDecl name bi type fun fvar => do
else go (Expr.instantiate1 body fvar) (args.push arg)
let arg := (some name, type, data) else if name.hasMacroScopes then
let (args, final) := typeToArgsType (Expr.instantiate1 body (mkFVar ⟨name⟩)) k args e
(#[arg] ++ args, final) else
match e.consumeMData with let arg := (some name, type, bi)
| Expr.forallE name type body binderInfo => helper name type body binderInfo Meta.withLocalDecl name bi type fun fvar => do
| _ => (#[], e) go (Expr.instantiate1 body fvar) (args.push arg)
match e.consumeMData with
| Expr.forallE name type body binderInfo => helper name type body binderInfo
| _ => k args e
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let (args, type) := typeToArgsType v.type argTypeTelescope v.type fun args type => do
let args ← args.mapM (fun (n, e, b) => do return Arg.mk n (← prettyPrintTerm e) b) let args ← args.mapM (fun (n, e, b) => do return Arg.mk n (← prettyPrintTerm e) b)
let nameInfo ← NameInfo.ofTypedName v.name type let nameInfo ← NameInfo.ofTypedName v.name type
match ← findDeclarationRanges? v.name with match ← findDeclarationRanges? v.name with
-- TODO: Maybe selection range is more relevant? Figure this out in the future -- TODO: Maybe selection range is more relevant? Figure this out in the future
| some range => return { | some range =>
toNameInfo := nameInfo, return {
args, toNameInfo := nameInfo,
declarationRange := range.range, args,
attrs := ← getAllAttributes v.name declarationRange := range.range,
} attrs := ← getAllAttributes v.name
| none => panic! s!"{v.name} is a declaration without position" }
| none => panic! s!"{v.name} is a declaration without position"
end DocGen4.Process end DocGen4.Process