bookshelf-doc/DocGen4/Process/StructureInfo.lean

59 lines
1.9 KiB
Plaintext
Raw Blame History

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
import DocGen4.Process.Base
import DocGen4.Process.NameInfo
namespace DocGen4.Process
open Lean Meta
/--
Execute `k` with an array containing pairs `(fieldName, fieldType)`.
`k` is executed in an updated local context which contains local declarations for the `structName` parameters.
-/
def withFields (info : InductiveVal) (k : Array (Name × Expr) → MetaM α) (includeSubobjectFields : Bool := false) : MetaM α := do
let structName := info.name
let us := info.levelParams.map mkLevelParam
forallTelescopeReducing info.type fun params _ =>
withLocalDeclD `s (mkAppN (mkConst structName us) params) fun s => do
let mut info := #[]
for fieldName in getStructureFieldsFlattened (← getEnv) structName includeSubobjectFields do
let proj ← mkProjection s fieldName
info := info.push (fieldName, (← inferType proj))
k info
def getFieldTypes (v : InductiveVal) : MetaM (Array NameInfo) := do
withFields v fun fields =>
fields.foldlM (init := #[]) (fun acc (name, type) => do return acc.push (← NameInfo.ofTypedName (v.name.append name) type))
def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let env ← getEnv
let parents := getParentStructures env v.name
let ctorVal := getStructureCtor env v.name
let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type
match getStructureInfo? env v.name with
| some i =>
if i.fieldNames.size - parents.size > 0 then
return {
toInfo := info,
fieldInfo := ← getFieldTypes v,
parents,
ctor
}
else
return {
toInfo := info,
fieldInfo := #[],
parents,
ctor
}
| none => panic! s!"{v.name} is not a structure"
end DocGen4.Process