doc: Process.Base

main
Henrik Böving 2022-05-20 09:23:33 +02:00
parent d519ef6b58
commit 56bd8c3ced
1 changed files with 89 additions and 6 deletions

View File

@ -9,66 +9,148 @@ import Lean
namespace DocGen4.Process namespace DocGen4.Process
open Lean Widget Meta open Lean Widget Meta
/--
Stores information about a typed name.
-/
structure NameInfo where structure NameInfo where
/--
The name that has this info attached.
-/
name : Name name : Name
/--
The pretty printed type of this name.
-/
type : CodeWithInfos type : CodeWithInfos
/--
The doc string of the name if it exists.
-/
doc : Option String doc : Option String
deriving Inhabited deriving Inhabited
/--
An argument to a declaration, e.g. the `(x : Nat)` in `def foo (x : Nat) := x`.
-/
structure Arg where structure Arg where
/--
The name of the argument.
-/
name : Name name : Name
/--
The pretty printed type of the argument.
-/
type : CodeWithInfos type : CodeWithInfos
/--
What kind of binder was used for the argument.
-/
binderInfo : BinderInfo binderInfo : BinderInfo
/--
A base structure for information about a declaration.
-/
structure Info extends NameInfo where structure Info extends NameInfo where
/--
The list of arguments to the declaration.
-/
args : Array Arg args : Array Arg
/--
In which lines the declaration was created.
-/
declarationRange : DeclarationRange declarationRange : DeclarationRange
/--
A list of (known) attributes that are attached to the declaration.
-/
attrs : Array String attrs : Array String
deriving Inhabited deriving Inhabited
/--
Information about an `axiom` declaration.
-/
structure AxiomInfo extends Info where structure AxiomInfo extends Info where
isUnsafe : Bool isUnsafe : Bool
deriving Inhabited deriving Inhabited
/--
Information about a `theorem` declaration.
-/
structure TheoremInfo extends Info structure TheoremInfo extends Info
deriving Inhabited deriving Inhabited
/--
Information about a `constant` declaration.
-/
structure OpaqueInfo extends Info where structure OpaqueInfo extends Info where
/--
The pretty printed value of the declaration.
-/
value : CodeWithInfos value : CodeWithInfos
-- A value of partial is interpreted as this constant being part of a partial def /--
-- since the actual definition for a partial def is hidden behind an inaccessible value A value of partial is interpreted as this constant being part of a partial def
since the actual definition for a partial def is hidden behind an inaccessible value.
-/
unsafeInformation : DefinitionSafety unsafeInformation : DefinitionSafety
deriving Inhabited deriving Inhabited
/--
Information about a `def` declaration, note that partial defs are handled by `OpaqueInfo`.
-/
structure DefinitionInfo extends Info where structure DefinitionInfo extends Info where
-- partial defs are handled by OpaqueInfo
isUnsafe : Bool isUnsafe : Bool
hints : ReducibilityHints hints : ReducibilityHints
equations : Option (Array CodeWithInfos) equations : Option (Array CodeWithInfos)
isNonComputable : Bool isNonComputable : Bool
deriving Inhabited deriving Inhabited
/--
Information about an `instance` declaration.
-/
abbrev InstanceInfo := DefinitionInfo abbrev InstanceInfo := DefinitionInfo
/--
Information about an `inductive` declaration
-/
structure InductiveInfo extends Info where structure InductiveInfo extends Info where
ctors : List NameInfo -- List of all constructors and their type for this inductive datatype /--
List of all constructors of this inductive type.
-/
ctors : List NameInfo
isUnsafe : Bool isUnsafe : Bool
deriving Inhabited deriving Inhabited
/--
Information about a `structure` declaration.
-/
structure StructureInfo extends Info where structure StructureInfo extends Info where
/--
Information about all the fields of the structure.
-/
fieldInfo : Array NameInfo fieldInfo : Array NameInfo
/--
All the structures this one inherited from.
-/
parents : Array Name parents : Array Name
/--
The constructor of the structure.
-/
ctor : NameInfo ctor : NameInfo
deriving Inhabited deriving Inhabited
/--
Information about a `class` declaration.
-/
structure ClassInfo extends StructureInfo where structure ClassInfo extends StructureInfo where
instances : Array Name instances : Array Name
deriving Inhabited deriving Inhabited
/--
Information about a `class inductive` declaration.
-/
structure ClassInductiveInfo extends InductiveInfo where structure ClassInductiveInfo extends InductiveInfo where
instances : Array Name instances : Array Name
deriving Inhabited deriving Inhabited
/--
A general type for informations about declarations.
-/
inductive DocInfo where inductive DocInfo where
| axiomInfo (info : AxiomInfo) : DocInfo | axiomInfo (info : AxiomInfo) : DocInfo
| theoremInfo (info : TheoremInfo) : DocInfo | theoremInfo (info : TheoremInfo) : DocInfo
@ -81,8 +163,9 @@ inductive DocInfo where
| classInductiveInfo (info : ClassInductiveInfo) : DocInfo | classInductiveInfo (info : ClassInductiveInfo) : DocInfo
deriving Inhabited deriving Inhabited
deriving instance Inhabited for ModuleDoc /--
Turns an `Expr` into a pretty printed `CodeWithInfos`.
-/
def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
let (fmt, infos) ← formatInfos expr let (fmt, infos) ← formatInfos expr
let tt := TaggedText.prettyTagged fmt let tt := TaggedText.prettyTagged fmt