diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean
index 732e555..c4b28a9 100644
--- a/DocGen4/IncludeStr.lean
+++ b/DocGen4/IncludeStr.lean
@@ -34,21 +34,21 @@ don't have to carry them around as files.
-/
@[termElab includeStr] def includeStrImpl : TermElab := λ stx _ => do
let str := stx[1].isStrLit?.get!
- let srcPath := FilePath.mk $ ←getFileName
+ let srcPath := FilePath.mk <| ←getFileName
let currentDir ← IO.currentDir
-- HACK: Currently we cannot get current file path in VSCode, we have to traversely find the matched subdirectory in the current directory.
if let some path ← match srcPath.parent with
- | some p => pure $ some $ p / str
+ | some p => pure <| some <| p / str
| none => do
let foundDir ← traverseDir currentDir λ p => p / str |>.pathExists
- pure $ foundDir.map (· / str)
+ pure <| foundDir.map (· / str)
then
if ←path.pathExists then
if ←path.isDir then
throwError s!"{str} is a directory"
else
let content ← FS.readFile path
- pure $ mkStrLit content
+ pure <| mkStrLit content
else
throwError s!"{path} does not exist as a file"
else
diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean
index b534744..60d1d31 100644
--- a/DocGen4/LeanInk/Output.lean
+++ b/DocGen4/LeanInk/Output.lean
@@ -55,7 +55,7 @@ def Token.toHtml (t : Token) : AlectryonM Html := do
-- TODO: render docstring
let mut parts := #[]
if let some tyi := t.typeinfo then
- parts := parts.push $ ←tyi.toHtml
+ parts := parts.push <| ←tyi.toHtml
parts := parts.push t.processSemantic
@@ -218,6 +218,6 @@ def moduleToHtml (module : Process.Module) (inkPath : System.FilePath) (sourceFi
let baseCtx ← readThe SiteBaseContext
let (html, _) := render |>.run ctx baseCtx
pure html
- | .error err => throw $ IO.userError s!"Error while parsing LeanInk Output: {err}"
+ | .error err => throw <| IO.userError s!"Error while parsing LeanInk Output: {err}"
end DocGen4.Output.LeanInk
diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean
index 0f9661f..26ab8db 100644
--- a/DocGen4/LeanInk/Process.lean
+++ b/DocGen4/LeanInk/Process.lean
@@ -33,8 +33,8 @@ def runInk (inkPath : System.FilePath) (sourceFilePath : System.FilePath) : IO J
match Json.parse output with
| .ok out => pure out
| .error err =>
- throw $ IO.userError s!"LeanInk returned invalid JSON for file: {sourceFilePath}:\n{err}"
+ throw <| IO.userError s!"LeanInk returned invalid JSON for file: {sourceFilePath}:\n{err}"
| code =>
- throw $ IO.userError s!"LeanInk exited with code {code} for file: {sourceFilePath}:\n{←inkProcess.stderr.readToEnd}"
+ throw <| IO.userError s!"LeanInk exited with code {code} for file: {sourceFilePath}:\n{←inkProcess.stderr.readToEnd}"
end DocGen4.Output.LeanInk
diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean
index 10f1c48..e6e9db9 100644
--- a/DocGen4/Load.lean
+++ b/DocGen4/Load.lean
@@ -21,7 +21,7 @@ as well as all the dependencies.
-/
def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do
let (leanInstall?, lakeInstall?) ← Lake.findInstall?
- match ←(EIO.toIO' $ Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
+ match ←(EIO.toIO' <| Lake.mkLoadConfig {leanInstall?, lakeInstall?}) with
| .ok config =>
let ws : Lake.Workspace ← Lake.loadWorkspace config |>.run Lake.MonadLog.eio
let libraryLeanGitHash := ws.env.lean.githash
@@ -30,16 +30,16 @@ def lakeSetup (imports : List String) : IO (Except UInt32 Lake.Workspace) := do
let ctx ← Lake.mkBuildContext ws
(ws.root.buildImportsAndDeps imports *> pure ()) |>.run Lake.MonadLog.eio ctx
initSearchPath (←findSysroot) ws.leanPaths.oleanPath
- pure $ Except.ok ws
+ pure <| Except.ok ws
| .error err =>
- throw $ IO.userError err.toString
+ throw <| IO.userError err.toString
def envOfImports (imports : List Name) : IO Environment := do
importModules (imports.map (Import.mk · false)) Options.empty
def loadInit (imports : List Name) : IO Hierarchy := do
let env ← envOfImports imports
- pure $ Hierarchy.fromArray env.header.moduleNames
+ pure <| Hierarchy.fromArray env.header.moduleNames
/--
Load a list of modules from the current Lean search path into an `Environment`
diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index db1d156..5016b3b 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -90,7 +90,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
--let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath
let sourceSearchPath := ws.root.srcDir :: ws.leanSrcPath
- discard $ htmlOutputDeclarationDatas result |>.run config baseConfig
+ discard <| htmlOutputDeclarationDatas result |>.run config baseConfig
for (modName, module) in result.moduleInfo.toArray do
let fileDir := moduleNameToDirectory basePath modName
@@ -99,7 +99,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
-- The last component is the file name, so we drop it from the depth to root.
let baseConfig := { baseConfig with depthToRoot := modName.components.dropLast.length }
let moduleHtml := moduleToHtml module |>.run config baseConfig
- FS.createDirAll $ fileDir
+ FS.createDirAll fileDir
FS.writeFile filePath moduleHtml.toString
if let some inkPath := inkPath then
if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
@@ -127,6 +127,7 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
let mut allInstances : HashMap String (Array String) := .empty
let mut importedBy : HashMap String (Array String) := .empty
let mut allModules : List (String × Json) := []
+ let mut instancesFor : HashMap String (Array String) := .empty
for entry in ←System.FilePath.readDir declarationsBasePath do
if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
let fileContent ← FS.readFile entry.path
@@ -138,6 +139,10 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
let mut insts := allInstances.findD inst.className #[]
insts := insts.push inst.name
allInstances := allInstances.insert inst.className insts
+ for typeName in inst.typeNames do
+ let mut instsFor := instancesFor.findD typeName #[]
+ instsFor := instsFor.push inst.name
+ instancesFor := instancesFor.insert typeName instsFor
for imp in module.imports do
let mut impBy := importedBy.findD imp #[]
impBy := impBy.push module.name
@@ -145,11 +150,14 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
let postProcessInstances := allInstances.toList.map (λ(k, v) => (k, toJson v))
let postProcessImportedBy := importedBy.toList.map (λ(k, v) => (k, toJson v))
+ let postProcessInstancesFor := instancesFor.toList.map (λ(k, v) => (k, toJson v))
+
let finalJson := Json.mkObj [
("declarations", Json.mkObj allDecls),
("instances", Json.mkObj postProcessInstances),
("importedBy", Json.mkObj postProcessImportedBy),
- ("modules", Json.mkObj allModules)
+ ("modules", Json.mkObj allModules),
+ ("instancesFor", Json.mkObj postProcessInstancesFor)
]
-- The root JSON for find
FS.writeFile (declarationsBasePath / "declaration-data.bmp") finalJson.compress
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index c68d218..469b77c 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -75,7 +75,7 @@ def getRoot : BaseHtmlM String := do
def getHierarchy : BaseHtmlM Hierarchy := do pure (←read).hierarchy
def getCurrentName : BaseHtmlM (Option Name) := do pure (←read).currentName
def getResult : HtmlM AnalyzerResult := do pure (←read).result
-def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range
+def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure <| (←read).sourceLinker module range
def leanInkEnabled? : HtmlM Bool := do pure (←read).leanInkEnabled
/--
@@ -93,7 +93,7 @@ Returns the doc-gen4 link to a module name.
-/
def moduleNameToLink (n : Name) : BaseHtmlM String := do
let parts := n.components.map Name.toString
- pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+ pure <| (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
/--
Returns the HTML doc-gen4 link to a module name.
@@ -106,7 +106,7 @@ Returns the LeanInk link to a module name.
-/
def moduleNameToInkLink (n : Name) : BaseHtmlM String := do
let parts := "src" :: n.components.map Name.toString
- pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+ pure <| (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
/--
Returns the path to the HTML file that contains information about a module.
@@ -149,7 +149,7 @@ Returns the doc-gen4 link to a declaration name.
def declNameToLink (name : Name) : HtmlM String := do
let res ← getResult
let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
- pure $ (←moduleNameToLink module) ++ "#" ++ name.toString
+ pure <| (←moduleNameToLink module) ++ "#" ++ name.toString
/--
Returns the HTML doc-gen4 link to a declaration name.
@@ -163,7 +163,7 @@ Returns the LeanInk link to a declaration name.
def declNameToInkLink (name : Name) : HtmlM String := do
let res ← getResult
let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
- pure $ (←moduleNameToInkLink module) ++ "#" ++ name.toString
+ pure <| (←moduleNameToInkLink module) ++ "#" ++ name.toString
/--
Returns the HTML doc-gen4 link to a declaration name with "break_within"
@@ -185,7 +185,7 @@ only `+` should be linked, taking care of this is what this function is
responsible for.
-/
def splitWhitespaces (s : String) : (String × String × String) := Id.run do
- let front := "".pushn ' ' $ s.offsetOfPos (s.find (!Char.isWhitespace ·))
+ let front := "".pushn ' ' <| s.offsetOfPos (s.find (!Char.isWhitespace ·))
let mut s := s.trimLeft
let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
s := s.trimRight
@@ -199,7 +199,7 @@ 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.append tt => tt.foldlM (λ acc t => do pure <| acc ++ (←infoFormatToHtml t)) #[]
| TaggedText.tag a t =>
match a.info.val.info with
| Info.ofTermInfo i =>
@@ -207,7 +207,7 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
| Expr.const name _ =>
match t with
| TaggedText.text t =>
- let (front, t, back) := splitWhitespaces $ Html.escape t
+ let (front, t, back) := splitWhitespaces <| Html.escape t
let elem := {t}
pure #[Html.text front, elem, Html.text back]
| _ =>
diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean
index 3ce2225..521afc3 100644
--- a/DocGen4/Output/Class.lean
+++ b/DocGen4/Output/Class.lean
@@ -8,9 +8,6 @@ namespace Output
open scoped DocGen4.Jsx
open Lean
---def classInstanceToHtml (name : Name) : HtmlM Html := do
--- pure
{←declNameToHtmlLink name}
-
def classInstancesToHtml (className : Name) : HtmlM Html := do
pure
diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean
index d1506ab..971d066 100644
--- a/DocGen4/Output/DocString.lean
+++ b/DocGen4/Output/DocString.lean
@@ -44,7 +44,7 @@ partial def xmlGetHeadingId (el : Xml.Element) : String :=
elementToPlainText el |> replaceCharSeq unicodeToDrop "-"
where
elementToPlainText el := match el with
- | (Element.Element name attrs contents) =>
+ | (Element.Element _ _ contents) =>
"".intercalate (contents.toList.map contentToPlainText)
contentToPlainText c := match c with
| Content.Element el => elementToPlainText el
@@ -138,7 +138,6 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme
def extendAnchor (el : Element) : HtmlM Element := do
match el with
| Element.Element name attrs contents =>
- let root ← getRoot
let newAttrs ← match (attrs.find? "href").map extendLink with
| some href => href.map (attrs.insert "href")
| none => pure attrs
@@ -161,7 +160,7 @@ def autoLink (el : Element) : HtmlM Element := do
match link? with
| some link =>
let attributes := Std.RBMap.empty.insert "href" link
- pure [Content.Element $ Element.Element "a" attributes #[Content.Character s]]
+ pure [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
| none =>
let sHead := s.dropRightWhile (λ c => c ≠ '.')
let sTail := s.takeRightWhile (λ c => c ≠ '.')
@@ -171,7 +170,7 @@ def autoLink (el : Element) : HtmlM Element := do
let attributes := Std.RBMap.empty.insert "href" link'
pure [
Content.Character sHead,
- Content.Element $ Element.Element "a" attributes #[Content.Character sTail]
+ Content.Element <| Element.Element "a" attributes #[Content.Character sTail]
]
| none =>
pure [Content.Character s]
@@ -204,7 +203,7 @@ def docStringToHtml (s : String) : HtmlM (Array Html) := do
match manyDocument rendered.mkIterator with
| Parsec.ParseResult.success _ res =>
res.mapM λ x => do
- pure (Html.text $ toString (← modifyElement x))
+ pure (Html.text <| toString (← modifyElement x))
| _ => pure #[Html.text rendered]
end Output
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index 6132dc8..48fcd3d 100644
--- a/DocGen4/Output/Index.lean
+++ b/DocGen4/Output/Index.lean
@@ -11,12 +11,13 @@ namespace Output
open scoped DocGen4.Jsx
-def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") $ pure $
-
-
-
Welcome to the documentation page
- What is up?
-
+def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
+ pure <|
+
+
+
Welcome to the documentation page
+ What is up?
+
end Output
end DocGen4
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 47dbcaa..fdf5fdd 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -6,6 +6,14 @@ namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
+open Lean
+
+def instancesForToHtml (typeName : Name) : HtmlM Html := do
+ pure
+
+ Instances For
+