Merge pull request #28 from leanprover/modifiers

Remaining modifiers for declarations

DocGen4.lean

@@ -9,3 +9,4 @@ import DocGen4.Load
 import DocGen4.ToHtmlFormat
 import DocGen4.IncludeStr
 import DocGen4.Output
+import DocGen4.Attributes

DocGen4/Attributes.lean

@@ -0,0 +1,110 @@
+import Lean
+
+namespace DocGen4
+
+open Lean Meta
+
+-- The following is probably completely overengineered but I love it
+class ValueAttr (attrKind : Type → Type) where
+  getValue {α : Type} [Inhabited α] [ToString α] : attrKind α → Environment → Name → Option String
+
+structure ValueAttrWrapper (attrKind : Type → Type) [ValueAttr attrKind] where
+  {α : Type}
+  attr : attrKind α
+  [str : ToString α]
+  [inhab : Inhabited α]
+
+def enumGetValue {α : Type} [Inhabited α] [ToString α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option String := OptionM.run do
+  let val ← EnumAttributes.getValue attr env decl
+  some (toString val)
+
+instance : ValueAttr EnumAttributes where
+  getValue := enumGetValue
+
+def parametricGetValue {α : Type} [Inhabited α] [ToString α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option String := OptionM.run do
+  let val ← ParametricAttribute.getParam attr env decl
+  some (attr.attr.name.toString ++ " " ++ toString val)
+
+instance : ValueAttr ParametricAttribute where
+  getValue := parametricGetValue
+
+abbrev EnumAttrWrapper := ValueAttrWrapper EnumAttributes
+abbrev ParametricAttrWrapper := ValueAttrWrapper ParametricAttribute
+
+def tagAttributes : Array TagAttribute := #[IR.UnboxResult.unboxAttr, neverExtractAttr, Elab.Term.elabWithoutExpectedTypeAttr, SynthInstance.inferTCGoalsRLAttr, matchPatternAttr]
+
+deriving instance Repr for Compiler.InlineAttributeKind
+deriving instance Repr for Compiler.SpecializeAttributeKind
+
+open Compiler in
+instance : ToString InlineAttributeKind where
+  toString kind :=
+    match kind with
+    | InlineAttributeKind.inline => "inline"
+    | InlineAttributeKind.noinline => "noinline"
+    | InlineAttributeKind.macroInline => "macroInline"
+    | InlineAttributeKind.inlineIfReduce => "inlineIfReduce"
+
+open Compiler in
+instance : ToString SpecializeAttributeKind where
+  toString kind :=
+    match kind with
+    | SpecializeAttributeKind.specialize => "specialize"
+    | SpecializeAttributeKind.nospecialize => "nospecialize"
+
+def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨Compiler.specializeAttrs⟩]
+
+instance : ToString ExternEntry where
+  toString entry :=
+    match entry with
+    | ExternEntry.adhoc `all => ""
+    | ExternEntry.adhoc backend => s!"{backend} adhoc"
+    | ExternEntry.standard `all fn => fn
+    | ExternEntry.standard backend fn => s!"{backend} {fn}"
+    | ExternEntry.inline backend pattern => s!"{backend} inline {String.quote pattern}"
+    -- TODO: The docs in the module dont specific how to render this
+    | ExternEntry.foreign backend fn  => s!"{backend} foreign {fn}"
+
+instance : ToString ExternAttrData where
+  toString data := (data.arity?.map toString |>.getD "") ++ String.intercalate " " (data.entries.map toString)
+
+def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, ⟨Compiler.implementedByAttr⟩]
+
+def getTags (decl : Name) : MetaM (Array String) := do
+  let env ← getEnv
+  pure $ tagAttributes.filter (TagAttribute.hasTag · env decl) |>.map (λ t => t.attr.name.toString)
+
+def getValuesAux {α : Type} {attrKind : Type → Type} [va : ValueAttr attrKind] [Inhabited α] [ToString α] (decl : Name) (attr : attrKind α) : MetaM (Option String) := do
+  let env ← getEnv
+  pure $ va.getValue attr env decl
+
+def getValues {attrKind : Type → Type} [ValueAttr attrKind] (decl : Name) (attrs : Array (ValueAttrWrapper attrKind)) : MetaM (Array String) := do
+  let env ← getEnv
+  let mut res := #[]
+  for attr in attrs do
+    if let some val ← @getValuesAux attr.α attrKind _ attr.inhab attr.str decl attr.attr then
+      res := res.push val
+  pure res
+
+def getEnumValues (decl : Name) : MetaM (Array String) := getValues decl enumAttributes
+def getParametricValues (decl : Name) : MetaM (Array String) := getValues decl parametricAttributes
+
+def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) := do
+  let insts ← getDefaultInstances className
+  for (inst, prio) in insts do
+    if inst == decl then
+      return some $ s!"defaultInstance {prio}"
+  pure none
+
+def hasSimp (decl : Name) : MetaM (Bool) := do
+  let thms ← simpExtension.getTheorems
+  pure $ thms.isLemma decl
+
+def getAllAttributes (decl : Name) : MetaM (Array String) := do
+  let tags ← getTags decl
+  let enums ← getEnumValues decl
+  let parametric ← getParametricValues decl
+  let simp := if ←hasSimp decl then #["simp"] else #[]
+  pure $ simp ++ tags ++ enums ++ parametric
+
+end DocGen4

DocGen4/IncludeStr.lean

@@ -19,7 +19,7 @@ syntax (name := includeStr) "include_str" str : term
         throwError s!"{str} is a directory"
       else
         let content ← FS.readFile path
-        return mkStrLit content
+        pure $ mkStrLit content
     else
       throwError s!"\"{str}\" does not exist as a file"
 

DocGen4/Load.lean

@@ -14,10 +14,10 @@ open Lean System Std IO
 
 def getLakePath : IO FilePath := do
   match (← IO.getEnv "LAKE") with
-  | some path => System.FilePath.mk path
+  | some path => pure $ System.FilePath.mk path
   | none =>
     let lakePath := (←findSysroot?) / "bin" / "lake"
-    lakePath.withExtension System.FilePath.exeExtension
+    pure $ lakePath.withExtension System.FilePath.exeExtension
 
 -- Modified from the LSP Server
 def lakeSetupSearchPath (lakePath : System.FilePath) (imports : Array String) : IO Lean.SearchPath := do

DocGen4/Output.lean

@@ -32,22 +32,22 @@ def getGithubBaseUrl : IO String := do
   if url.startsWith "git@" then
     url := url.drop 15
     url := url.dropRight 4
-    s!"https://github.com/{url}"
+    pure s!"https://github.com/{url}"
   else if url.endsWith ".git" then
-    url.dropRight 4
+    pure $ url.dropRight 4
   else
-    url
+    pure url
 
 def getCommit : IO String := do
   let out ← IO.Process.output {cmd := "git", args := #["rev-parse", "HEAD"]}
   if out.exitCode != 0 then
     throw <| IO.userError <| "git exited with code " ++ toString out.exitCode
-  out.stdout.trimRight
+  pure out.stdout.trimRight
 
 def sourceLinker : IO (Name → Option DeclarationRange → String) := do
   let baseUrl ← getGithubBaseUrl
   let commit ← getCommit
-  return λ name range =>
+  pure λ name range =>
     let parts := name.components.map Name.toString
     let path := (parts.intersperse "/").foldl (· ++ ·) ""
     let r := name.getRoot

DocGen4/Output/Base.lean

@@ -25,17 +25,17 @@ def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName :=
 abbrev HtmlT := ReaderT SiteContext
 abbrev HtmlM := HtmlT Id
 
-def getRoot : HtmlM String := do (←read).root
+def getRoot : HtmlM String := do pure (←read).root
-def getResult : HtmlM AnalyzerResult := do (←read).result
+def getResult : HtmlM AnalyzerResult := do pure (←read).result
-def getCurrentName : HtmlM (Option Name) := do (←read).currentName
+def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName
-def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do (←read).sourceLinker module range
+def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range
 
 def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
   new >>= base
 
 def moduleNameToLink (n : Name) : HtmlM String := do
   let parts := n.components.map Name.toString
-  (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+  pure $ (←getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
 
 def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
   let parts := n.components.map Name.toString
@@ -53,7 +53,7 @@ end Static
 def declNameToLink (name : Name) : HtmlM String := do
   let res ← getResult
   let module := res.moduleNames[res.name2ModIdx.find! name]
-  (←moduleNameToLink module) ++ "#" ++ name.toString
+  pure $ (←moduleNameToLink module) ++ "#" ++ name.toString
 
 def splitWhitespaces (s : String) : (String × String × String) := Id.run do
   let front := "".pushn ' ' (s.find (!Char.isWhitespace ·))
@@ -64,8 +64,8 @@ def splitWhitespaces (s : String) : (String × String × String) := Id.run do
 
 partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
   match i with
-  | TaggedText.text t => return #[t]
+  | TaggedText.text t => pure #[t]
-  | TaggedText.append tt => tt.foldlM (λ acc t => do acc ++ (←infoFormatToHtml t)) #[]
+  | TaggedText.append tt => tt.foldlM (λ acc t => do pure $ acc ++ (←infoFormatToHtml t)) #[]
   | TaggedText.tag a t =>
     match a.info.val.info with
     | Info.ofTermInfo i =>
@@ -75,13 +75,13 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
          | TaggedText.text t =>
            let (front, t, back) := splitWhitespaces t
            let elem := Html.element "a" true #[("href", ←declNameToLink name)] #[t]
-           #[Html.text front, elem, Html.text back]
+           pure #[Html.text front, elem, Html.text back]
          | _ =>
            -- TODO: Is this ever reachable?
-           #[Html.element "a" true #[("href", ←declNameToLink name)] (←infoFormatToHtml t)]
+           pure #[Html.element "a" true #[("href", ←declNameToLink name)] (←infoFormatToHtml t)]
       | _ =>
-         #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+         pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
-    | _ => #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
+    | _ => pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
 
 end Output
 end DocGen4

DocGen4/Output/Class.lean

@@ -8,11 +8,12 @@ open scoped DocGen4.Jsx
 open Lean
 
 def classInstanceToHtml (name : Name) : HtmlM Html := do
-  <li><a href={←declNameToLink name}>{name.toString}</a></li>
+  pure <li><a href={←declNameToLink name}>{name.toString}</a></li>
 
-def classInstancesToHtml (i : ClassInfo) : HtmlM Html := do
+def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
-  let instancesHtml ← i.instances.mapM classInstanceToHtml
+  let instancesHtml ← instances.mapM classInstanceToHtml
-  return <details «class»="instances">
+  pure
+    <details «class»="instances">
         <summary>Instances</summary>
         <ul>
           [instancesHtml]
@@ -20,7 +21,7 @@ def classInstancesToHtml (i : ClassInfo) : HtmlM Html := do
     </details>
 
 def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
-  (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i)
+  pure $ (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
 
 end Output
 end DocGen4

DocGen4/Output/ClassInductive.lean

@@ -0,0 +1,13 @@
+import DocGen4.Output.Template
+import DocGen4.Output.Class
+import DocGen4.Output.Inductive
+
+
+namespace DocGen4
+namespace Output
+
+def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do
+  pure $ (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
+
+end Output
+end DocGen4

DocGen4/Output/Definition.lean

@@ -7,26 +7,27 @@ open scoped DocGen4.Jsx
 open Lean Widget
 
 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
-  <li «class»="equation">[←infoFormatToHtml c]</li>
+  pure <li «class»="equation">[←infoFormatToHtml c]</li>
 
 def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do
-  if let some eqs ← i.equations then
+  if let some eqs := i.equations then
     let equationsHtml ← eqs.mapM equationToHtml
-    return <details>
+    pure
+      <details>
         <summary>Equations</summary>
         <ul «class»="equations">
           [equationsHtml]
         </ul>
       </details>
   else
-    return none
+    pure none
 
 def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
   let equationsHtml ← equationsToHtml i
-  if let some equationsHtml ← equationsHtml then
+  if let some equationsHtml := equationsHtml then
-    #[equationsHtml]
+    pure #[equationsHtml]
   else
-    #[]
+    pure #[]
 
 end Output
 end DocGen4

DocGen4/Output/Index.lean

@@ -11,7 +11,7 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
-def index : HtmlM Html := do templateExtends (baseHtml "Index") $
+def index : HtmlM Html := do templateExtends (baseHtml "Index") $ pure $
   <main>
     <a id="top"></a>
     <h1> Welcome to the documentation page </h1>

DocGen4/Output/Inductive.lean

@@ -8,10 +8,10 @@ open scoped DocGen4.Jsx
 def ctorToHtml (i : NameInfo) : HtmlM Html := do
   let shortName := i.name.components'.head!.toString
   let name := i.name.toString
-  return <li «class»="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
+  pure <li «class»="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
 
-def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) :=
+def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
-  return #[<ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>]
+  pure #[<ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>]
 
 end Output
 end DocGen4

DocGen4/Output/Module.lean

@@ -9,6 +9,7 @@ import DocGen4.Output.Structure
 import DocGen4.Output.Class
 import DocGen4.Output.Definition
 import DocGen4.Output.Instance
+import DocGen4.Output.ClassInductive
 
 namespace DocGen4
 namespace Output
@@ -30,9 +31,9 @@ def argToHtml (arg : Arg) : HtmlM Html := do
   let inner := Html.element "span" true #[("class", "fn")] nodes
   let html := Html.element "span" false #[("class", "decl_args")] #[inner]
   if implicit then
-    <span «class»="impl_arg">{html}</span>
+    pure <span «class»="impl_arg">{html}</span>
   else
-    html
+    pure html
 
 def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
   let mut nodes := #[]
@@ -45,13 +46,11 @@ def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
       let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
       parents := parents.push html
     nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
-  nodes
+  pure nodes
 
 def docInfoHeader (doc : DocInfo) : HtmlM Html := do
   let mut nodes := #[]
-  -- TODO: noncomputable, partial
+  nodes := nodes.push <span «class»="decl_kind">{doc.getKindDescription}</span>
-  -- TODO: Support all the kinds in CSS
-  nodes := nodes.push <span «class»="decl_kind">{doc.getKind}</span>
   nodes := nodes.push
     <span «class»="decl_name">
       <a «class»="break_within" href={←declNameToLink doc.getName}>
@@ -70,26 +69,35 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
 
   nodes := nodes.push <span «class»="decl_args">:</span>
   nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
-  return <div «class»="decl_header"> [nodes] </div>
+  pure <div «class»="decl_header"> [nodes] </div>
 
 def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
-  let doc_html ← match doc with
+  let docHtml ← match doc with
   | DocInfo.inductiveInfo i => inductiveToHtml i
   | DocInfo.structureInfo i => structureToHtml i
   | DocInfo.classInfo i => classToHtml i
   | DocInfo.definitionInfo i => definitionToHtml i
   | DocInfo.instanceInfo i => instanceToHtml i
-  | _ => #[]
+  | DocInfo.classInductiveInfo i => classInductiveToHtml i
+  | _ => pure #[]
 
-  return <div «class»="decl" id={doc.getName.toString}>
+  let attrs := doc.getAttrs
+  let attrsHtml :=
+    if attrs.size > 0 then
+      let attrStr := "@[" ++ String.intercalate ", " doc.getAttrs.toList ++ "]"
+      #[Html.element "div" false #[("class", "attributes")] #[attrStr]]
+    else
+      #[]
+
+  pure
+    <div «class»="decl" id={doc.getName.toString}>
       <div «class»={doc.getKind}>
         <div «class»="gh_link">
-        -- TODO: Put the proper source link
           <a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
         </div>
-      -- TODO: Attributes
+        [attrsHtml]
         {←docInfoHeader doc}
-      [←doc_html]
+        [docHtml]
       </div>
     </div>
 
@@ -100,41 +108,41 @@ def declarationToNavLink (module : Name) : Html :=
 
 -- TODO: Similar functions are used all over the place, we should dedup them
 def moduleToNavLink (module : Name) : HtmlM Html := do
-  <a href={←moduleNameToLink module}>{module.toString}</a>
+  pure <a href={←moduleNameToLink module}>{module.toString}</a>
 
 def getImports (module : Name) : HtmlM (Array Name) := do
   let res ← getResult
-  let some idx ← res.moduleNames.findIdx? (. == module) | unreachable!
+  let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
   let adj := res.importAdj.get! idx
   let mut imports := #[]
   for i in [:adj.size] do
     if adj.get! i then
       imports := imports.push (res.moduleNames.get! i)
-  imports
+  pure imports
 
 def getImportedBy (module : Name) : HtmlM (Array Name) := do
   let res ← getResult
-  let some idx ← res.moduleNames.findIdx? (. == module) | unreachable!
+  let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
   let adj := res.importAdj
   let mut impBy := #[]
   for i in [:adj.size] do
     if adj.get! i |>.get! idx then
       impBy := impBy.push (res.moduleNames.get! i)
-  impBy
+  pure impBy
 
 def importedByHtml (moduleName : Name) : HtmlM (Array Html) := do
   let imports := (←getImportedBy moduleName) |>.qsort Name.lt
-  imports.mapM (λ i => do <li>{←moduleToNavLink i}</li>)
+  imports.mapM (λ i => do pure <li>{←moduleToNavLink i}</li>)
 
 
 def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
   let imports := (←getImports moduleName) |>.qsort Name.lt
-  imports.mapM (λ i => do <li>{←moduleToNavLink i}</li>)
+  imports.mapM (λ i => do pure <li>{←moduleToNavLink i}</li>)
 
 def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
+  pure
     <nav «class»="internal_nav">
       <h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
-    -- TODO: Proper source links
       <p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
       <div «class»="imports">
         <details>
@@ -155,7 +163,7 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
 
 def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
   let docInfos ← module.members.mapM (λ i => docInfoToHtml module.name i)
-  templateExtends (baseHtmlArray module.name.toString) $ #[
+  templateExtends (baseHtmlArray module.name.toString) $ pure #[
     ←internalNav (module.members.map DocInfo.getName) module.name,
     Html.element "main" false #[] docInfos
   ]

DocGen4/Output/Navbar.lean

@@ -13,8 +13,8 @@ namespace Output
 open Lean
 open scoped DocGen4.Jsx
 
-def moduleListFile (file : Name) : HtmlM Html :=
+def moduleListFile (file : Name) : HtmlM Html := do
-  return <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
+  pure <div "class"="nav_link" [if (← getCurrentName) == file then #[("visible", "")] else #[]]>
     <a href={← moduleNameToLink file}>{file.toString}</a>
   </div>
 
@@ -25,7 +25,8 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
   let dirNodes ← (dirs.mapM moduleListDir)
   let fileNodes ← (files.mapM moduleListFile)
   let moduleLink ← moduleNameToLink h.getName
-  return <details "class"="nav_sect" "data-path"={moduleLink}
+  pure
+    <details "class"="nav_sect" "data-path"={moduleLink}
       [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
       <summary>{h.getName.toString}</summary>
       [dirNodes]
@@ -37,9 +38,10 @@ def moduleList : HtmlM Html := do
   let mut list := Array.empty
   for (n, cs) in hierarchy.getChildren do
     list := list.push $ ←moduleListDir cs
-  return <div "class"="module_list">[list]</div>
+  pure <div "class"="module_list">[list]</div>
 
 def navbar : HtmlM Html := do
+  pure
     <nav «class»="nav">
       <h3>General documentation</h3>
       <div «class»="nav_link"><a href={s!"{←getRoot}"}>index</a></div>

DocGen4/Output/NotFound.lean

@@ -11,7 +11,7 @@ namespace Output
 
 open scoped DocGen4.Jsx
 
-def notFound : HtmlM Html := do templateExtends (baseHtml "404") $
+def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ pure $
   <main>
     <h1>404 Not Found</h1>
     <p> Unfortunately, the page you were looking for is no longer here. </p>

DocGen4/Output/Structure.lean

@@ -9,16 +9,18 @@ open Lean
 def fieldToHtml (f : NameInfo) : HtmlM Html := do
   let shortName := f.name.components'.head!.toString
   let name := f.name.toString
-  return <li «class»="structure_field" id={name}>{s!"{shortName} "} : [←infoFormatToHtml f.type]</li>
+  pure <li «class»="structure_field" id={name}>{s!"{shortName} "} : [←infoFormatToHtml f.type]</li>
 
 def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
   if Name.isSuffixOf `mk i.ctor.name then
-    #[<ul «class»="structure_fields" id={i.ctor.name.toString}>
+    pure #[
+      <ul «class»="structure_fields" id={i.ctor.name.toString}>
         [←i.fieldInfo.mapM fieldToHtml]
       </ul>]
   else
     let ctorShortName := i.ctor.name.components'.head!.toString
-    #[<ul «class»="structure_ext">
+    pure #[
+      <ul «class»="structure_ext">
         <li id={i.ctor.name.toString} «class»="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
         <ul «class»="structure_ext_fields">
           [←i.fieldInfo.mapM fieldToHtml]

DocGen4/Output/Template.lean

@@ -12,6 +12,7 @@ namespace Output
 open scoped DocGen4.Jsx
 
 def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
+  pure
     <html lang="en">
       <head>
         <link rel="stylesheet" href={s!"{←getRoot}style.css"}/>

DocGen4/Process.lean

@@ -10,6 +10,7 @@ import Std.Data.HashMap
 import Lean.Meta.SynthInstance
 
 import DocGen4.Hierarchy
+import DocGen4.Attributes
 
 namespace DocGen4
 
@@ -29,6 +30,7 @@ structure Info extends NameInfo where
   args : Array Arg
   doc : Option String
   declarationRange : DeclarationRange
+  attrs : Array String
   deriving Inhabited
 
 structure AxiomInfo extends Info where
@@ -40,14 +42,17 @@ structure TheoremInfo extends Info
 
 structure OpaqueInfo extends Info where
   value : CodeWithInfos
-  isUnsafe : Bool
+  -- 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
 
 structure DefinitionInfo extends Info where
-  --value : CodeWithInfos
+  -- partial defs are handled by OpaqueInfo
-  unsafeInformation : DefinitionSafety
+  isUnsafe : Bool
   hints : ReducibilityHints
   equations : Option (Array CodeWithInfos)
+  isComputable : Bool
   deriving Inhabited
 
 abbrev InstanceInfo := DefinitionInfo
@@ -67,6 +72,10 @@ structure ClassInfo extends StructureInfo where
   instances : Array Name
   deriving Inhabited
 
+structure ClassInductiveInfo extends InductiveInfo where
+  instances : Array Name
+  deriving Inhabited
+
 inductive DocInfo where
 | axiomInfo (info : AxiomInfo) : DocInfo
 | theoremInfo (info : TheoremInfo) : DocInfo
@@ -76,6 +85,7 @@ inductive DocInfo where
 | inductiveInfo (info : InductiveInfo) : DocInfo
 | structureInfo (info : StructureInfo) : DocInfo
 | classInfo (info : ClassInfo) : DocInfo
+| classInductiveInfo (info : ClassInductiveInfo) : DocInfo
   deriving Inhabited
 
 namespace DocInfo
@@ -89,6 +99,7 @@ def getDeclarationRange : DocInfo → DeclarationRange
 | inductiveInfo i => i.declarationRange
 | structureInfo i => i.declarationRange
 | classInfo i => i.declarationRange
+| classInductiveInfo i => i.declarationRange
 
 def lineOrder (l r : DocInfo) : Bool :=
   l.getDeclarationRange.pos.line < r.getDeclarationRange.pos.line
@@ -132,35 +143,40 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
     openDecls := ← getOpenDecls
     fileMap := default
   }
-  tagExprInfos ctx infos tt
+  pure $ tagExprInfos ctx infos tt
 
 def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
   let env ← getEnv
   let (args, type) := typeToArgsType v.type
   let type ← prettyPrintTerm type
-  let args ← args.mapM (λ (n, e, b) => do Arg.mk n (←prettyPrintTerm e) b)
+  let args ← args.mapM (λ (n, e, b) => do pure $ Arg.mk n (←prettyPrintTerm e) b)
   let doc ← findDocString? env v.name
   match ←findDeclarationRanges? v.name with
   -- TODO: Maybe selection range is more relevant? Figure this out in the future
-  | some range => return Info.mk ⟨v.name, type⟩ args doc range.range
+  | some range => pure $ Info.mk ⟨v.name, type⟩ args doc range.range (←getAllAttributes v.name)
   | none => panic! s!"{v.name} is a declaration without position"
 
 def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
-  return AxiomInfo.mk info v.isUnsafe
+  pure $ AxiomInfo.mk info v.isUnsafe
 
 def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
-  return TheoremInfo.mk info
+  pure $ TheoremInfo.mk info
 
 def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let t ← prettyPrintTerm v.value
-  return OpaqueInfo.mk info t v.isUnsafe
+  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
 
 def isInstance (declName : Name) : MetaM Bool := do
-  (instanceExtension.getState (←getEnv)).instanceNames.contains declName
+  pure $ (instanceExtension.getState (←getEnv)).instanceNames.contains declName
-
 
 partial def stripArgs (e : Expr) : Expr :=
   match e.consumeMData with
@@ -184,34 +200,50 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
       let us := v.levelParams.map mkLevelParam
       let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
       let type ← mkForallFVars xs type
-      type
+      pure type
+
+-- The following code is translated from ll_infer_type.cpp
+def computable? (defn : Name) : MetaM Bool := do
+  let cstage2Name := defn.append `_cstage2
+  let env ← getEnv
+  pure $ env.find? cstage2Name |>.isSome
 
 def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
+  let isUnsafe := v.safety == DefinitionSafety.unsafe
+  let isComputable ← computable? v.name
   try
     let eqs? ← getEqnsFor? v.name
     match eqs? with
     | some eqs =>
       let prettyEqs ← eqs.mapM processEq
-      DefinitionInfo.mk info v.safety v.hints prettyEqs
+      pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isComputable
     | none =>
       let eq ← prettyPrintTerm $ stripArgs (←valueToEq v)
-      DefinitionInfo.mk info v.safety v.hints (some #[eq])
+      pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isComputable
   catch err =>
     IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
-    return DefinitionInfo.mk info v.safety v.hints none
+    pure $ DefinitionInfo.mk info isUnsafe v.hints none isComputable
+
+def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do
+  let info ← DefinitionInfo.ofDefinitionVal v
+  let some className := getClassName (←getEnv) v.type | unreachable!
+  if let some instAttr ← getDefaultInstance v.name className then
+    pure { info with attrs := info.attrs.push instAttr }
+  else
+    pure info
 
 def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
   let env ← getEnv
   match env.find? ctor with
-  | some (ConstantInfo.ctorInfo i) => ←prettyPrintTerm i.type
+  | some (ConstantInfo.ctorInfo i) => prettyPrintTerm i.type
   | _ => panic! s!"Constructor {ctor} was requested but does not exist"
 
 def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
   let env ← getEnv
-  let ctors ← v.ctors.mapM (λ name => do NameInfo.mk name (←getConstructorType name))
+  let ctors ← v.ctors.mapM (λ name => do pure $ NameInfo.mk name (←getConstructorType name))
-  return InductiveInfo.mk info ctors v.isUnsafe
+  pure $ InductiveInfo.mk info ctors v.isUnsafe
 
 def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
   match type, n with
@@ -229,7 +261,7 @@ def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : Meta
   let mut field_infos := #[]
   for (name, type) in fields do
     field_infos := field_infos.push { name := struct.append name, type := ←prettyPrintTerm type}
-  field_infos
+  pure $ field_infos
 
 def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   let info ← Info.ofConstantVal v.toConstantVal
@@ -240,17 +272,24 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
   match getStructureInfo? env v.name with
   | some i =>
     if i.fieldNames.size - parents.size > 0 then
-      return StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
+      pure $ StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
     else
-      return StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
+      pure $ StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
   | none => panic! s!"{v.name} is not a structure"
 
+def getInstances (className : Name) : MetaM (Array Name) := do
+  let fn ← mkConstWithFreshMVarLevels className
+  let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
+  let insts ← SynthInstance.getInstances (mkAppN fn xs)
+  pure $ insts.map Expr.constName!
+
 def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
   let sinfo ← StructureInfo.ofInductiveVal v
-  let fn ← mkConstWithFreshMVarLevels v.name
+  pure $ ClassInfo.mk sinfo (←getInstances v.name)
-  let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
+
-  let insts ← SynthInstance.getInstances (mkAppN fn xs)
+def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
-  return ClassInfo.mk sinfo (insts.map Expr.constName!)
+  let info ← InductiveInfo.ofInductiveVal v
+  pure $ ClassInductiveInfo.mk info (←getInstances v.name)
 
 namespace DocInfo
 
@@ -258,13 +297,13 @@ def isBlackListed (declName : Name) : MetaM Bool := do
   match ←findDeclarationRanges? declName with
   | some _ =>
     let env ← getEnv
-    declName.isInternal
+    pure (declName.isInternal)
-    <||> isAuxRecursor env declName
+    <||> (pure $ isAuxRecursor env declName)
-    <||> isNoConfusion env declName
+    <||> (pure $ isNoConfusion env declName)
     <||> isRec declName
     <||> isMatcher declName
   -- TODO: Evaluate whether filtering out declarations without range is sensible
-  | none => true
+  | none => pure true
 
 -- TODO: Is this actually the best way?
 def isProjFn (declName : Name) : MetaM Bool := do
@@ -275,42 +314,46 @@ def isProjFn (declName : Name) : MetaM Bool := do
       match getStructureInfo? env parent with
       | some i =>
         match i.fieldNames.find? (· == name) with
-        | some _ => true
+        | some _ => pure true
-        | none => false
+        | none => pure false
       | none => panic! s!"{parent} is not a structure"
     else
-      false
+      pure false
-  | _ => false
+  | _ => pure false
 
 def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do
   if (←isBlackListed name) then
     return none
   match info with
-  | ConstantInfo.axiomInfo i => some $ axiomInfo (←AxiomInfo.ofAxiomVal i)
+  | ConstantInfo.axiomInfo i => pure <| some <| axiomInfo (←AxiomInfo.ofAxiomVal i)
-  | ConstantInfo.thmInfo i => some $ theoremInfo (←TheoremInfo.ofTheoremVal i)
+  | ConstantInfo.thmInfo i => pure <| some <| theoremInfo (←TheoremInfo.ofTheoremVal i)
-  | ConstantInfo.opaqueInfo i => some $ opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
+  | ConstantInfo.opaqueInfo i => pure <| some <| opaqueInfo (←OpaqueInfo.ofOpaqueVal i)
   | ConstantInfo.defnInfo i =>
     if ← (isProjFn i.name) then
-      none
+      pure none
+    else
+      if (←isInstance i.name) then
+        let info ← InstanceInfo.ofDefinitionVal i
+        pure <| some <| instanceInfo info
       else
         let info ← DefinitionInfo.ofDefinitionVal i
-      if (←isInstance i.name) then
+        pure <| some <| definitionInfo  info
-        some $ instanceInfo info
-      else
-        some $ definitionInfo info
   | ConstantInfo.inductInfo i =>
     let env ← getEnv
     if isStructure env i.name then
       if isClass env i.name then
-        some $ classInfo (←ClassInfo.ofInductiveVal i)
+        pure <| some <| classInfo (←ClassInfo.ofInductiveVal i)
       else
-        some $ structureInfo (←StructureInfo.ofInductiveVal i)
+        pure <| some <| structureInfo (←StructureInfo.ofInductiveVal i)
     else
-      some $ inductiveInfo (←InductiveInfo.ofInductiveVal i)
+      if isClass env i.name then
+        pure <| some <| classInductiveInfo (←ClassInductiveInfo.ofInductiveVal i)
+      else
+        pure <| some <| inductiveInfo (←InductiveInfo.ofInductiveVal i)
   -- we ignore these for now
-  | ConstantInfo.ctorInfo i => none
+  | ConstantInfo.ctorInfo i => pure none
-  | ConstantInfo.recInfo i => none
+  | ConstantInfo.recInfo i => pure none
-  | ConstantInfo.quotInfo i => none
+  | ConstantInfo.quotInfo i => pure none
 
 def getName : DocInfo → Name
 | axiomInfo i => i.name
@@ -321,16 +364,52 @@ def getName : DocInfo → Name
 | inductiveInfo i => i.name
 | structureInfo i => i.name
 | classInfo i => i.name
+| classInductiveInfo i => i.name
 
 def getKind : DocInfo → String
 | axiomInfo _ => "axiom"
 | theoremInfo _ => "theorem"
 | opaqueInfo _ => "constant"
 | definitionInfo _ => "def"
-| instanceInfo _ => "instance" -- TODO: This doesnt exist in CSS yet
+| instanceInfo _ => "instance"
 | inductiveInfo _ => "inductive"
 | structureInfo _ => "structure"
-| classInfo _ => "class" -- TODO: This is handled as structure right now
+| classInfo _ => "class"
+| classInductiveInfo _ => "class"
+
+def getKindDescription : DocInfo → String
+| axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom"
+| theoremInfo _ => "theorem"
+| opaqueInfo i =>
+  match i.unsafeInformation with
+  | DefinitionSafety.safe => "constant"
+  | DefinitionSafety.unsafe => "unsafe constant"
+  | DefinitionSafety.partial => "partial def"
+| definitionInfo i => Id.run do
+  if i.hints.isAbbrev then
+    pure "abbrev"
+  else
+    let mut modifiers := #[]
+    if i.isUnsafe then
+      modifiers := modifiers.push "unsafe"
+    if ¬i.isComputable then
+      modifiers := modifiers.push "noncomputable"
+
+    modifiers := modifiers.push "def"
+    pure $ String.intercalate " " modifiers.toList
+| instanceInfo i => Id.run do
+  let mut modifiers := #[]
+  if i.isUnsafe then
+    modifiers := modifiers.push "unsafe"
+  if ¬i.isComputable then
+    modifiers := modifiers.push "noncomputable"
+
+  modifiers := modifiers.push "instance"
+  pure $ String.intercalate " " modifiers.toList
+| inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive"
+| structureInfo _ => "structure"
+| classInfo _ => "class"
+| classInductiveInfo _ => "class inductive"
 
 def getType : DocInfo → CodeWithInfos
 | axiomInfo i => i.type
@@ -341,6 +420,7 @@ def getType : DocInfo → CodeWithInfos
 | inductiveInfo i => i.type
 | structureInfo i => i.type
 | classInfo i => i.type
+| classInductiveInfo i => i.type
 
 def getArgs : DocInfo → Array Arg
 | axiomInfo i => i.args
@@ -351,6 +431,18 @@ def getArgs : DocInfo → Array Arg
 | inductiveInfo i => i.args
 | structureInfo i => i.args
 | classInfo i => i.args
+| classInductiveInfo i => i.args
+
+def getAttrs : DocInfo → Array String
+| axiomInfo i => i.attrs
+| theoremInfo i => i.attrs
+| opaqueInfo i => i.attrs
+| definitionInfo i => i.attrs
+| instanceInfo i => i.attrs
+| inductiveInfo i => i.attrs
+| structureInfo i => i.attrs
+| classInfo i => i.attrs
+| classInductiveInfo i => i.attrs
 
 end DocInfo
 
@@ -379,7 +471,7 @@ def process : MetaM AnalyzerResult := do
     try
       let analysis := Prod.fst <$> Meta.MetaM.toIO (DocInfo.ofConstant cinfo) { maxHeartbeats := 5000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {}
       if let some dinfo ← analysis then
-        let some modidx ← env.getModuleIdxFor? dinfo.getName | unreachable!
+        let some modidx := env.getModuleIdxFor? dinfo.getName | unreachable!
         let moduleName := env.allImportedModuleNames.get! modidx
         let module := res.find! moduleName
         res := res.insert moduleName {module with members := module.members.push dinfo}
@@ -391,13 +483,13 @@ def process : MetaM AnalyzerResult := do
   -- TODO: This could probably be faster if we did an insertion sort above instead
   for (moduleName, module) in res.toArray do
     res := res.insert moduleName {module with members := module.members.qsort DocInfo.lineOrder}
-    let some modIdx ← env.getModuleIdx? moduleName | unreachable!
+    let some modIdx := env.getModuleIdx? moduleName | unreachable!
     let moduleData := env.header.moduleData.get! modIdx
     for imp in moduleData.imports do
-      let some importIdx ← env.getModuleIdx? imp.module | unreachable!
+      let some importIdx := env.getModuleIdx? imp.module | unreachable!
       adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
 
-  return {
+  pure {
     name2ModIdx := env.const2ModIdx,
     moduleNames := env.header.moduleNames,
     moduleInfo := res,
@@ -405,6 +497,4 @@ def process : MetaM AnalyzerResult := do
     importAdj := adj
   }
 
-
-
 end DocGen4

DocGen4/ToHtmlFormat.lean

@@ -86,12 +86,12 @@ def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
     as ← match attr with
     | `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
       let n ← match n with
-        | `(jsxAttrName| $n:strLit) => n
+        | `(jsxAttrName| $n:strLit) => pure n
-        | `(jsxAttrName| $n:ident) => quote (toString n.getId)
+        | `(jsxAttrName| $n:ident) => pure $ quote (toString n.getId)
         | _ => Macro.throwUnsupported
       let v ← match v with
-        | `(jsxAttrVal| {$v}) => v
+        | `(jsxAttrVal| {$v}) => pure v
-        | `(jsxAttrVal| $v:strLit) => v
+        | `(jsxAttrVal| $v:strLit) => pure v
         | _ => Macro.throwUnsupported
       `(($as).push ($n, ($v : String)))
     | `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-04
+leanprover/lean4:nightly-2022-02-11