From 56bd8c3ced007bf28d459aac089abcde53c9f567 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 20 May 2022 09:23:33 +0200
Subject: [PATCH] doc: Process.Base

---
 DocGen4/Process/Base.lean | 95 ++++++++++++++++++++++++++++++++++++---
 1 file changed, 89 insertions(+), 6 deletions(-)

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