chore: structure ctor style

main
Henrik Böving 2022-07-23 13:37:17 +02:00
parent 04387711de
commit 3aae640f69
11 changed files with 80 additions and 27 deletions

View File

@ -40,7 +40,7 @@ def Process.Module.toJson (module : Process.Module) : HtmlM Json := do
for decl in declInfo do
jsonDecls := (←DocInfo.toJson module.name decl) :: jsonDecls
if let .instanceInfo i := decl then
instances := instances.push { name := i.name.toString, className := i.instClass.toString}
instances := instances.push { name := i.name.toString, className := i.className.toString}
let jsonMod : JsonModule := {
name := module.name.toString,
declarations := jsonDecls,

View File

@ -14,6 +14,9 @@ open Lean Meta
def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
let info ← Info.ofConstantVal v.toConstantVal
pure <| AxiomInfo.mk info v.isUnsafe
pure {
toInfo := info,
isUnsafe := v.isUnsafe
}
end DocGen4.Process

View File

@ -87,7 +87,7 @@ structure OpaqueInfo extends Info where
A value of partial is interpreted as this opaque being part of a partial def
since the actual definition for a partial def is hidden behind an inaccessible value.
-/
unsafeInformation : DefinitionSafety
definitionSafety : DefinitionSafety
deriving Inhabited
/--
@ -104,7 +104,7 @@ structure DefinitionInfo extends Info where
Information about an `instance` declaration.
-/
structure InstanceInfo extends DefinitionInfo where
instClass : Name
className : Name
deriving Inhabited
/--

View File

@ -38,19 +38,38 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let isUnsafe := v.safety == DefinitionSafety.unsafe
let isNonComput := isNoncomputable (←getEnv) v.name
let isNonComputable := isNoncomputable (←getEnv) v.name
try
let eqs? ← getEqnsFor? v.name
match eqs? with
| some eqs =>
let prettyEqs ← eqs.mapM processEq
pure <| DefinitionInfo.mk info isUnsafe v.hints prettyEqs isNonComput
let equations ← eqs.mapM processEq
pure {
toInfo := info,
isUnsafe,
hints := v.hints,
equations,
isNonComputable
}
| none =>
let eq ← prettyPrintTerm <| stripArgs (←valueToEq v)
pure <| DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isNonComput
let equations := #[←prettyPrintTerm <| stripArgs (←valueToEq v)]
pure {
toInfo := info,
isUnsafe,
hints := v.hints,
equations,
isNonComputable
}
catch err =>
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
pure <| DefinitionInfo.mk info isUnsafe v.hints none isNonComput
pure {
toInfo := info,
isUnsafe,
hints := v.hints,
equations := none,
isNonComputable
}
end DocGen4.Process

View File

@ -162,7 +162,7 @@ def getKindDescription : DocInfo → String
| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
| theoremInfo _ => "theorem"
| opaqueInfo i =>
match i.unsafeInformation with
match i.definitionSafety with
| DefinitionSafety.safe => "opaque"
| DefinitionSafety.unsafe => "unsafe opaque"
| DefinitionSafety.partial => "partial def"

View File

@ -21,6 +21,10 @@ def getConstructorType (ctor : Name) : MetaM Expr := do
def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let ctors ← v.ctors.mapM (λ name => do NameInfo.ofTypedName name (←getConstructorType name))
pure <| InductiveInfo.mk info ctors v.isUnsafe
pure {
toInfo := info,
ctors,
isUnsafe := v.isUnsafe
}
end DocGen4.Process

View File

@ -14,11 +14,15 @@ namespace DocGen4.Process
open Lean Meta
def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
let info ← DefinitionInfo.ofDefinitionVal v
let mut info ← DefinitionInfo.ofDefinitionVal v
let some className := getClassName (←getEnv) v.type | unreachable!
if let some instAttr ← getDefaultInstance v.name className then
pure <| InstanceInfo.mk { info with attrs := info.attrs.push instAttr } className
else
pure <| InstanceInfo.mk info className
info := { info with attrs := info.attrs.push instAttr }
pure {
toDefinitionInfo := info,
className
}
end DocGen4.Process

View File

@ -39,7 +39,12 @@ def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let nameInfo ← NameInfo.ofTypedName v.name type
match ←findDeclarationRanges? v.name with
-- TODO: Maybe selection range is more relevant? Figure this out in the future
| some range => pure <| Info.mk nameInfo args range.range (←getAllAttributes v.name)
| some range => pure {
toNameInfo := nameInfo,
args,
declarationRange := range.range,
attrs := (←getAllAttributes v.name)
}
| none => panic! s!"{v.name} is a declaration without position"
end DocGen4.Process

View File

@ -14,13 +14,20 @@ open Lean Meta
def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let t ← prettyPrintTerm v.value
let value ← prettyPrintTerm v.value
let env ← getEnv
let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
if isPartial then
pure <| OpaqueInfo.mk info t DefinitionSafety.partial
else
let safety := if v.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
pure <| OpaqueInfo.mk info t safety
let definitionSafety :=
if isPartial then
DefinitionSafety.partial
else if v.isUnsafe then
DefinitionSafety.unsafe
else
DefinitionSafety.safe
pure {
toInfo := info,
value,
definitionSafety
}
end DocGen4.Process

View File

@ -35,13 +35,24 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let env ← getEnv
let parents := getParentStructures env v.name
let ctor := getStructureCtor 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
pure <| StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents (←NameInfo.ofTypedName ctor.name ctor.type)
pure {
toInfo := info,
fieldInfo := (←getFieldTypes v.name ctorVal parents.size),
parents,
ctor
}
else
pure <| StructureInfo.mk info #[] parents (←NameInfo.ofTypedName ctor.name ctor.type)
pure {
toInfo := info,
fieldInfo := #[],
parents,
ctor
}
| none => panic! s!"{v.name} is not a structure"
end DocGen4.Process

View File

@ -14,6 +14,6 @@ open Lean Meta
def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
let info ← Info.ofConstantVal v.toConstantVal
pure <| TheoremInfo.mk info
pure { toInfo := info }
end DocGen4.Process