From 72034b08318bf5503b782e270ecdf376745212d6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 20 Nov 2022 13:10:05 +0100
Subject: [PATCH] feat: linkify builtin types

---
 DocGen4/Output/Base.lean              | 23 +++++++++++++++++------
 DocGen4/Output/FoundationalTypes.lean |  6 +++---
 DocGen4/Process/Hierarchy.lean        |  1 +
 3 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 53ef5bc..75966d0 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -207,18 +207,19 @@ to as much information as possible.
 -/
 partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
   match i with
-  | TaggedText.text t => pure #[Html.escape t]
-  | TaggedText.append tt => tt.foldlM (λ acc t => do pure <| acc ++ (←infoFormatToHtml t)) #[]
-  | TaggedText.tag a t =>
+  | .text t => pure #[Html.escape t]
+  | .append tt => tt.foldlM (λ acc t => do pure <| acc ++ (←infoFormatToHtml t)) #[]
+  | .tag a t =>
     match a.info.val.info with
     | Info.ofTermInfo i =>
       let cleanExpr :=  i.expr.consumeMData
-      if let Expr.const name _ := cleanExpr then
+      match cleanExpr with
+      | .const name _ =>
         -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
         -- find a better solution
         if (←getResult).name2ModIdx.contains name then
           match t with
-          | TaggedText.text t =>
+          | .text t =>
             let (front, t, back) := splitWhitespaces <| Html.escape t
             let elem := <a href={←declNameToLink name}>{t}</a>
             pure #[Html.text front, elem, Html.text back]
@@ -226,7 +227,17 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
             pure #[<a href={←declNameToLink name}>[←infoFormatToHtml t]</a>]
         else
          pure #[<span class="fn">[←infoFormatToHtml t]</span>]
-      else
+      | .sort _ =>
+        match t with
+        | .text t =>
+          let mut sortPrefix :: rest := t.splitOn " " | unreachable!
+          let sortLink := <a href={s!"{← getRoot}foundational_types.html"}>{sortPrefix}</a>
+          if rest != [] then
+            rest := " " :: rest
+          pure #[sortLink, Html.text <| String.join rest]
+        | _ =>
+          pure #[<a href={s!"{← getRoot}foundational_types.html"}>[← infoFormatToHtml t]</a>]
+      | _ =>
          pure #[<span class="fn">[←infoFormatToHtml t]</span>]
     | _ => pure #[<span class="fn">[←infoFormatToHtml t]</span>]
 
diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean
index 6112832..b1e00a7 100644
--- a/DocGen4/Output/FoundationalTypes.lean
+++ b/DocGen4/Output/FoundationalTypes.lean
@@ -5,9 +5,9 @@ namespace DocGen4.Output
 
 open scoped DocGen4.Jsx
 
-def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundational Type") do
+def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundational Types") do
   pure <|
-    <div class="docfile">
+    <main>
       <a id="top"></a>
       <h1>Foundational Types</h1>
 
@@ -45,6 +45,6 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat
       <p>Note that despite not itself being a function, <code>(→)</code> is available as infix notation for
       <code>{"λ α β, α → β"}</code>.</p>    
       -- TODO: instnaces for pi types 
-    </div>
+    </main>
 
 end DocGen4.Output
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean
index 02ba920..5a52d6f 100644
--- a/DocGen4/Process/Hierarchy.lean
+++ b/DocGen4/Process/Hierarchy.lean
@@ -89,6 +89,7 @@ def baseDirBlackList : HashSet String :=
     "find",
     "how-about.js",
     "index.html",
+    "foundational_types.html",
     "mathjax-config.js",
     "navbar.html",
     "nav.js",