refactor: change find syntax

DocGen4/Output.lean

@@ -10,6 +10,7 @@ import DocGen4.Output.Index
 import DocGen4.Output.Module
 import DocGen4.Output.NotFound
 import DocGen4.Output.Find
+import DocGen4.Output.Semantic
 
 namespace DocGen4
 
@@ -69,19 +70,24 @@ def htmlOutput (result : AnalyzerResult) (root : String) : IO Unit := do
   let notFoundHtml := ReaderT.run notFound config
   FS.createDirAll basePath
   FS.createDirAll (basePath / "find")
+  FS.createDirAll (basePath / "semantic")
 
   let mut declList := #[]
   for (_, mod) in result.moduleInfo.toArray do
     for decl in filterMapDocInfo mod.members do
       let name := decl.getName.toString
       let doc := decl.getDocString.getD ""
-      let link := Id.run <| ReaderT.run (declNameToLink decl.getName) config
+      let link := root ++ s!"semantic/{decl.getName.hash}.xml#"
-      let source := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config
+      let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config
-      let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("source", source)]
+      let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config
+      let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourcLink", sourceLink)]
       declList := declList.push obj
-
+      let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config 
+      FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml
   let json := Json.arr declList
 
+  FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config 
+
   FS.writeFile (basePath / "index.html") indexHtml.toString
   FS.writeFile (basePath / "404.html") notFoundHtml.toString
   FS.writeFile (basePath / "find" / "index.html") findHtml.toString

DocGen4/Output/Semantic.lean

@@ -0,0 +1,58 @@
+import DocGen4.Output.Template
+import DocGen4.Output.DocString
+import Lean.Data.Xml
+
+open Lean Xml
+
+namespace DocGen4
+namespace Output
+
+instance : ToString $ Array Element where
+  toString xs := xs.map toString |>.foldl String.append ""
+
+instance : Coe Element Content where
+  coe e := Content.Element e
+
+-- TODO: syntax metaprogramming and basic semantic data
+
+def semanticXml (i : DocInfo) : HtmlM $ Array Element := do
+  pure #[
+    Element.Element
+      "rdf:RDF"
+        (Std.RBMap.fromList [
+          ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"),
+          ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#")
+        ] _)
+        #[
+          Element.Element
+          "rdf:Description" 
+          (Std.RBMap.fromList [
+            ("rdf:about", s!"{←getRoot}semactic/{i.getName.hash}.xml#")
+          ] _)
+         #[]
+        ]
+  ]
+
+def schemaXml : HtmlM $ Array Element := do
+  pure #[
+    Element.Element
+      "rdf:RDF"
+        (Std.RBMap.fromList [
+          ("xmlns:rdf", "http://www.w3.org/1999/02/22-rdf-syntax-ns#"),
+          ("xmlns:docgen4", s!"{←getRoot}semactic/docgen4.xml#")
+        ] _)
+        #[
+          Element.Element
+          "docgen4:hasInstance" 
+          Std.RBMap.empty
+          #[
+            Element.Element
+            "rdfs:type" 
+            Std.RBMap.empty
+            #[Content.Character "rdf:Property"]
+          ]
+        ]
+  ]
+
+end Output
+end DocGen4

static/declaration-data.js

@@ -67,13 +67,14 @@ export class DeclarationDataCenter {
         const dataJson = await dataRes.json();
         // the data is a map of name (original case) to declaration data.
         const data = new Map(
-          dataJson.map(({ name, doc, link, source: sourceLink }) => [
+          dataJson.map(({ name, doc, link, docLink, sourceLink }) => [
             name,
             {
               name,
               lowerName: name.toLowerCase(),
               lowerDoc: doc.toLowerCase(),
               link,
+              docLink,
               sourceLink,
             },
           ])
@@ -91,7 +92,7 @@ export class DeclarationDataCenter {
    * Search for a declaration.
    * @returns {Array<any>}
    */
-  search(pattern, strict = false) {
+  search(pattern, strict = true) {
     if (!pattern) {
       return [];
     }
@@ -142,6 +143,7 @@ function getMatches(declarations, pattern, maxResults = 30) {
     lowerName,
     lowerDoc,
     link,
+    docLink,
     sourceLink,
   } of declarations.values()) {
     let err = matchCaseSensitive(name, lowerName, patNoSpaces);
@@ -154,7 +156,7 @@ function getMatches(declarations, pattern, maxResults = 30) {
       err = 3;
     }
     if (err !== undefined) {
-      results.push({ name, err, lowerName, lowerDoc, link, sourceLink });
+      results.push({ name, err, lowerName, lowerDoc, link, docLink, sourceLink });
     }
   }
   return results.sort(({ err: a }, { err: b }) => a - b).slice(0, maxResults);

static/find/find.js

@@ -1,26 +1,74 @@
 /**
  * This module is used for the `/find` endpoint.
+ *
+ * Two basic kinds of search syntax are supported:
+ *
+ * 1. Query-Fragment syntax: `/find?pattern=Nat.add#doc` for documentation and `/find?pattern=Nat.add#src` for source code.
+ * 2. Fragment-Only syntax:`/find/#doc/Nat.add` for documentation and `/find/#src/Nat.add` for source code.
+ *
+ * Though both of them are valid, the first one is highly recommended, and the second one is for compatibility and taste.
+ *
+ * There are some extended usage for the QF syntax. For example, appending `strict=false` to the query part
+ * (`/find?pattern=Nat.add&strict=false#doc`) will allow you to use the fuzzy search, rather than strict match.
+ * Also, the fragment is extensible as well. For now only `#doc` and `#src` are implement, and the plain query without
+ * hash (`/find?pattern=Nat.add`) is used for computer-friendly data (semantic web is great! :P), while all other fragments
+ * fallback to the `#doc` view.
  */
 
 import { SITE_ROOT } from "../site-root.js";
 import { DeclarationDataCenter } from "../declaration-data.js";
 
-async function findRedirect(pattern, isSource) {
+/**
+ * We don't use browser's default hash and searchParams in case Lean declaration name
+ * can be like `«#»`, rather we manually handle the `window.location.href` with regex.
+ */
+const LEAN_FRIENDLY_URL_REGEX = /^[^?#]+(?:\?((?:[^«#»]|«.*»)*))?(?:#(.*))?$/;
+const LEAN_FRIENDLY_AND_SEPARATOR = /(?<!«[^»]*)&/;
+const LEAN_FRIENDLY_EQUAL_SEPARATOR = /(?<!«[^»]*)=/;
+const LEAN_FRIENDLY_SLASH_SEPARATOR = /(?<!«[^»]*)\//;
+
+const [_, query, fragment] = LEAN_FRIENDLY_URL_REGEX.exec(window.location.href);
+const queryParams = new Map(
+  query
+    ?.split(LEAN_FRIENDLY_AND_SEPARATOR)
+    ?.map((p) => p.split(LEAN_FRIENDLY_EQUAL_SEPARATOR))
+    ?.filter((l) => l.length == 2 && l[0].length > 0)
+);
+const fragmentPaths = fragment?.split(LEAN_FRIENDLY_SLASH_SEPARATOR) ?? [];
+
+const pattern = queryParams.get("pattern") ?? fragmentPaths[1]; // if first fail then second, may be undefined
+const strict = (queryParams.get("strict") ?? "true") === "true"; // default to true
+const view = fragmentPaths[0];
+
+/**
+ * Find the result and redirect to the result page.
+ * @param {string} pattern the pattern to search for
+ * @param {string} view the view of the find result (`"doc"` or `"src"` for now)
+ */
+async function findAndRedirect(pattern, strict, view) {
+  // if no pattern provided, directly redirect to the 404 page
+  if (!pattern) {
+    window.location.replace(`${SITE_ROOT}404.html`);
+  }
+  // search for result
   const dataCenter = await DeclarationDataCenter.init();
-  let results = dataCenter.search(pattern, true);
+  let result = (dataCenter.search(pattern, strict) ?? [])[0]; // in case return non array
-  if (results.length == 0) {
+  // if no result found, redirect to the 404 page
-    // if there is no exact match, redirect to 404 page to use fuzzy match
+  if (!result) {
+    // TODO: better url semantic for 404, current implementation will lead to duplicate search for fuzzy match if not found.
     window.location.replace(`${SITE_ROOT}404.html#${pattern ?? ""}`);
   } else {
-    // redirect to doc or source page.
+    // success, redirect to doc or source page, or to the semantic rdf.
     window.location.replace(isSource ? results[0].sourceLink : results[0].link);
+    if (!view) {
+      window.location.replace(result.link);
+    } else if (view == "doc") {
+      window.location.replace(result.docLink);
+    } else if (view == "src") {
+      window.location.replace(result.sourceLink);
+    } else {
+      // fallback to doc page
+      window.location.replace(result.docLink);
+    }
   }
-}
+}
-
-let hash = window.location.hash.replace("#", "");
-
-if (hash.endsWith("/src")) {
-  findRedirect(hash.replace("/src", ""), true);
-} else {
-  findRedirect(hash, false);
-}

static/how-about.js

@@ -20,14 +20,14 @@ if (HOW_ABOUT) {
   if (pattern) {
     HOW_ABOUT.innerText = "Please wait a second. I'll try to help you.";
     DeclarationDataCenter.init().then((dataCenter) => {
-      let results = dataCenter.search(pattern);
+      let results = dataCenter.search(pattern, false);
       if (results.length > 0) {
         HOW_ABOUT.innerText = "How about one of these instead:";
         const ul = HOW_ABOUT.appendChild(document.createElement("ul"));
-        for (const { name, link } of results) {
+        for (const { name, docLink } of results) {
           const li = ul.appendChild(document.createElement("li"));
           const a = li.appendChild(document.createElement("a"));
-          a.href = link;
+          a.href = docLink;
           a.appendChild(document.createElement("code")).innerText = name;
         }
       } else {

static/search.js

@@ -87,18 +87,18 @@ SEARCH_INPUT.addEventListener("input", async (ev) => {
   // searching
   sr.setAttribute("state", "loading");
   const dataCenter = await DeclarationDataCenter.init();
-  const result = dataCenter.search(text);
+  const result = dataCenter.search(text, false);
 
   // in case user has updated the input.
   if (ev.target.value != text) return;
 
   // update search results
   removeAllChildren(sr);
-  for (const { name, link } of result) {
+  for (const { name, docLink } of result) {
     const d = sr.appendChild(document.createElement("a"));
     d.innerText = name;
     d.title = name;
-    d.href = link;
+    d.href = docLink;
   }
   sr.setAttribute("state", "done");
 });