feat: cleanup def rendering and add reducible attribute

DocGen4/Process/Attributes.lean

@@ -62,34 +62,42 @@ open Compiler in
 instance : ToString InlineAttributeKind where
   toString kind :=
     match kind with
-    | InlineAttributeKind.inline => "inline"
+    | .inline => "inline"
-    | InlineAttributeKind.noinline => "noinline"
+    | .noinline => "noinline"
-    | InlineAttributeKind.macroInline => "macro_inline"
+    | .macroInline => "macro_inline"
-    | InlineAttributeKind.inlineIfReduce => "inline_if_reduce"
+    | .inlineIfReduce => "inline_if_reduce"
-    | InlineAttributeKind.alwaysInline => "always_inline"
+    | .alwaysInline => "always_inline"
 
 open Compiler in
 instance : ToString SpecializeAttributeKind where
   toString kind :=
     match kind with
-    | SpecializeAttributeKind.specialize => "specialize"
+    | .specialize => "specialize"
-    | SpecializeAttributeKind.nospecialize => "nospecialize"
+    | .nospecialize => "nospecialize"
+
+instance : ToString ReducibilityStatus where
+  toString kind :=
+    match kind with
+    | .reducible => "reducible"
+    | .semireducible => "semireducible"
+    | .irreducible => "irreducible"
 
 /--
 The list of all enum based attributes doc-gen knows about and can recover.
 -/
-def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩]
+@[reducible]
+def enumAttributes : Array EnumAttrWrapper := #[⟨Compiler.inlineAttrs⟩, ⟨reducibilityAttrs⟩]
 
 instance : ToString ExternEntry where
   toString entry :=
     match entry with
-    | ExternEntry.adhoc `all => ""
+    | .adhoc `all => ""
-    | ExternEntry.adhoc backend => s!"{backend} adhoc"
+    | .adhoc backend => s!"{backend} adhoc"
-    | ExternEntry.standard `all fn => fn
+    | .standard `all fn => fn
-    | ExternEntry.standard backend fn => s!"{backend} {fn}"
+    | .standard backend fn => s!"{backend} {fn}"
-    | ExternEntry.inline backend pattern => s!"{backend} inline {String.quote pattern}"
+    | .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}"
+    | .foreign backend fn  => s!"{backend} foreign {fn}"
 
 instance : ToString ExternAttrData where
   toString data := (data.arity?.map toString |>.getD "") ++ " " ++ String.intercalate " " (data.entries.map toString)

DocGen4/Process/DocInfo.lean

@@ -190,17 +190,19 @@ def getKindDescription : DocInfo → String
   | DefinitionSafety.unsafe => "unsafe opaque"
   | DefinitionSafety.partial => "partial def"
 | definitionInfo i => Id.run do
-  if i.hints.isAbbrev then
+  let mut modifiers := #[]
-    return "abbrev"
+  if i.isUnsafe then
-  else
+    modifiers := modifiers.push "unsafe"
-    let mut modifiers := #[]
+  if i.isNonComputable then
-    if i.isUnsafe then
+    modifiers := modifiers.push "noncomputable"
-      modifiers := modifiers.push "unsafe"
-    if i.isNonComputable then
-      modifiers := modifiers.push "noncomputable"
 
-    modifiers := modifiers.push "def"
+  let defKind :=
-    return String.intercalate " " modifiers.toList
+    if i.hints.isAbbrev then
+      "abbrev"
+    else
+      "def"
+  modifiers := modifiers.push defKind
+  return String.intercalate " " modifiers.toList
 | instanceInfo i => Id.run do
   let mut modifiers := #[]
   if i.isUnsafe then