From ed4cee2eae884ad49f4a179dd0e353b4d8cbcf32 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 23 Jul 2022 13:01:25 +0200 Subject: [PATCH 1/4] chore: style, change $ to <| --- DocGen4/IncludeStr.lean | 8 ++++---- DocGen4/LeanInk/Output.lean | 4 ++-- DocGen4/LeanInk/Process.lean | 4 ++-- DocGen4/Load.lean | 8 ++++---- DocGen4/Output.lean | 4 ++-- DocGen4/Output/Base.lean | 16 ++++++++-------- DocGen4/Output/DocString.lean | 6 +++--- DocGen4/Output/Index.lean | 13 +++++++------ DocGen4/Output/Module.lean | 6 +++--- DocGen4/Output/Navbar.lean | 2 +- DocGen4/Output/NotFound.lean | 13 +++++++------ DocGen4/Output/SourceLinker.lean | 4 ++-- DocGen4/Output/ToHtmlFormat.lean | 4 ++-- DocGen4/Output/ToJson.lean | 2 +- DocGen4/Process/Analyze.lean | 17 ++++------------- DocGen4/Process/Attributes.lean | 12 ++++++------ DocGen4/Process/AxiomInfo.lean | 2 +- DocGen4/Process/Base.lean | 4 ++-- DocGen4/Process/DefinitionInfo.lean | 8 ++++---- DocGen4/Process/DocInfo.lean | 16 +++++++--------- DocGen4/Process/Hierarchy.lean | 14 +++++++------- DocGen4/Process/InductiveInfo.lean | 2 +- DocGen4/Process/InstanceInfo.lean | 4 ++-- DocGen4/Process/NameInfo.lean | 4 ++-- DocGen4/Process/OpaqueInfo.lean | 4 ++-- DocGen4/Process/StructureInfo.lean | 10 +++++----- DocGen4/Process/TheoremInfo.lean | 2 +- Main.lean | 8 ++++---- 28 files changed, 96 insertions(+), 105 deletions(-) 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..07b1229 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 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/DocString.lean b/DocGen4/Output/DocString.lean index d1506ab..a501e08 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -161,7 +161,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 +171,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 +204,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/Module.lean b/DocGen4/Output/Module.lean index 4aa50ee..278c929 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -65,7 +65,7 @@ and name. -/ def docInfoHeader (doc : DocInfo) : HtmlM Html := do let mut nodes := #[] - nodes := nodes.push $ Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription] + nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription] nodes := nodes.push @@ -168,7 +168,7 @@ Returns the list of all imports this module does. -/ def getImports (module : Name) : HtmlM (Array Name) := do let res ← getResult - pure $ res.moduleInfo.find! module |>.imports + pure <| res.moduleInfo.find! module |>.imports /-- Sort the list of all modules this one is importing, linkify it @@ -207,7 +207,7 @@ The main entry point to rendering the HTML for an entire module. def moduleToHtml (module : Process.Module) : HtmlM Html := withTheReader SiteBaseContext (setCurrentName module.name) do let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i) let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName - templateLiftExtends (baseHtmlGenerator module.name.toString) $ pure #[ + templateLiftExtends (baseHtmlGenerator module.name.toString) <| pure #[ ←internalNav memberNames module.name, Html.element "main" false #[] memberDocs ] diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 6f18a02..5952b6d 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -49,7 +49,7 @@ def moduleList : BaseHtmlM Html := do let hierarchy ← getHierarchy let mut list := Array.empty for (_, cs) in hierarchy.getChildren do - list := list.push $ ←moduleListDir cs + list := list.push <| ←moduleListDir cs pure
[list]
/-- diff --git a/DocGen4/Output/NotFound.lean b/DocGen4/Output/NotFound.lean index 2ed00a0..976ba06 100644 --- a/DocGen4/Output/NotFound.lean +++ b/DocGen4/Output/NotFound.lean @@ -14,12 +14,13 @@ open scoped DocGen4.Jsx /-- Render the 404 page. -/ -def notFound : BaseHtmlM Html := do templateExtends (baseHtml "404") $ pure $ -
-

404 Not Found

-

Unfortunately, the page you were looking for is no longer here.

-
-
+def notFound : BaseHtmlM Html := do templateExtends (baseHtml "404") <| + pure <| +
+

404 Not Found

+

Unfortunately, the page you were looking for is no longer here.

+
+
end Output end DocGen4 diff --git a/DocGen4/Output/SourceLinker.lean b/DocGen4/Output/SourceLinker.lean index 1080b76..e403c5e 100644 --- a/DocGen4/Output/SourceLinker.lean +++ b/DocGen4/Output/SourceLinker.lean @@ -27,7 +27,7 @@ def getGithubBaseUrl (gitUrl : String) : String := Id.run do url := url.dropRight 4 pure s!"https://github.com/{url}" else if url.endsWith ".git" then - pure $ url.dropRight 4 + pure <| url.dropRight 4 else pure url @@ -70,7 +70,7 @@ def sourceLinker (ws : Lake.Workspace) : IO (Name → Option DeclarationRange | _ => ("https://example.com", "master") gitMap := gitMap.insert dep.name value - pure $ λ module range => + pure λ module range => let parts := module.components.map Name.toString let path := (parts.intersperse "/").foldl (· ++ ·) "" let root := module.getRoot diff --git a/DocGen4/Output/ToHtmlFormat.lean b/DocGen4/Output/ToHtmlFormat.lean index b93d400..2558794 100644 --- a/DocGen4/Output/ToHtmlFormat.lean +++ b/DocGen4/Output/ToHtmlFormat.lean @@ -104,7 +104,7 @@ def translateAttrs (attrs : Array (TSyntax `DocGen4.Jsx.jsxAttr)) : MacroM (TSyn | `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) => let n ← match n with | `(jsxAttrName| $n:str) => pure n - | `(jsxAttrName| $n:ident) => pure $ quote (toString n.getId) + | `(jsxAttrName| $n:ident) => pure <| quote (toString n.getId) | _ => Macro.throwUnsupported let v ← match v with | `(jsxAttrVal| {$v}) => pure v @@ -128,7 +128,7 @@ private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : Mac | `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html)) | _ => Macro.throwUnsupported let tag := toString n.getId - pure $ (tag, cs) + pure <| (tag, cs) macro_rules | `(<$n $attrs* />) => do diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index 7d0a06c..954560b 100644 --- a/DocGen4/Output/ToJson.lean +++ b/DocGen4/Output/ToJson.lean @@ -47,6 +47,6 @@ def Process.Module.toJson (module : Process.Module) : HtmlM Json := do instances := instances imports := module.imports.map Name.toString } - pure $ ToJson.toJson jsonMod + pure <| ToJson.toJson jsonMod end DocGen4.Output diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean index 35c4563..d076131 100644 --- a/DocGen4/Process/Analyze.lean +++ b/DocGen4/Process/Analyze.lean @@ -79,15 +79,6 @@ def getDocString : ModuleMember → Option String end ModuleMember -def getRelevantModules (imports : List Name) : MetaM (HashSet Name) := do - let env ← getEnv - let mut relevant := .empty - for module in env.header.moduleNames do - for import in imports do - if import == module then - relevant := relevant.insert module - pure relevant - inductive AnalyzeTask where | loadAll (load : List Name) : AnalyzeTask | loadAllLimitAnalysis (analyze : List Name) : AnalyzeTask @@ -104,7 +95,7 @@ def getAllModuleDocs (relevantModules : Array Name) : MetaM (HashMap Name Module let some modIdx := env.getModuleIdx? module | unreachable! let moduleData := env.header.moduleData.get! modIdx let imports := moduleData.imports.map Import.module - res := res.insert module $ Module.mk module modDocs imports + res := res.insert module <| Module.mk module modDocs imports pure res /-- @@ -113,9 +104,9 @@ of this `MetaM` run and mentioned by the `AnalyzeTask`. -/ def process (task : AnalyzeTask) : MetaM (AnalyzerResult × Hierarchy) := do let env ← getEnv - let relevantModules ← match task with - | .loadAll _ => pure $ HashSet.fromArray env.header.moduleNames - | .loadAllLimitAnalysis analysis => getRelevantModules analysis + let relevantModules := match task with + | .loadAll _ => HashSet.fromArray env.header.moduleNames + | .loadAllLimitAnalysis analysis => HashSet.fromArray analysis.toArray let allModules := env.header.moduleNames let mut res ← getAllModuleDocs relevantModules.toArray diff --git a/DocGen4/Process/Attributes.lean b/DocGen4/Process/Attributes.lean index 02dc67d..a7b1317 100644 --- a/DocGen4/Process/Attributes.lean +++ b/DocGen4/Process/Attributes.lean @@ -101,11 +101,11 @@ def parametricAttributes : Array ParametricAttrWrapper := #[⟨externAttr⟩, def getTags (decl : Name) : MetaM (Array String) := do let env ← getEnv - pure $ tagAttributes.filter (TagAttribute.hasTag · env decl) |>.map (λ t => t.attr.name.toString) + 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 + 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 @@ -122,12 +122,12 @@ def getDefaultInstance (decl : Name) (className : Name) : MetaM (Option String) let insts ← getDefaultInstances className for (inst, prio) in insts do if inst == decl then - return some $ s!"defaultInstance {prio}" + return some s!"defaultInstance {prio}" pure none def hasSimp (decl : Name) : MetaM (Option String) := do let thms ← simpExtension.getTheorems - pure $ + pure <| if thms.isLemma decl then some "simp" else @@ -135,7 +135,7 @@ def hasSimp (decl : Name) : MetaM (Option String) := do def hasCsimp (decl : Name) : MetaM (Option String) := do let env ← getEnv - pure $ + pure <| if Compiler.hasCSimpAttribute env decl then some "csimp" else @@ -163,6 +163,6 @@ def getAllAttributes (decl : Name) : MetaM (Array String) := do let enums ← getEnumValues decl let parametric ← getParametricValues decl let customs ← getCustomAttrs decl - pure $ customs ++ tags ++ enums ++ parametric + pure <| customs ++ tags ++ enums ++ parametric end DocGen4 diff --git a/DocGen4/Process/AxiomInfo.lean b/DocGen4/Process/AxiomInfo.lean index c4eb78c..817af6f 100644 --- a/DocGen4/Process/AxiomInfo.lean +++ b/DocGen4/Process/AxiomInfo.lean @@ -14,6 +14,6 @@ open Lean Meta def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do let info ← Info.ofConstantVal v.toConstantVal - pure $ AxiomInfo.mk info v.isUnsafe + pure <| AxiomInfo.mk info v.isUnsafe end DocGen4.Process diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean index 6a6b550..8bc9d98 100644 --- a/DocGen4/Process/Base.lean +++ b/DocGen4/Process/Base.lean @@ -176,9 +176,9 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do fileMap := default, ngen := ← getNGen } - pure $ tagExprInfos ctx infos tt + pure <| tagExprInfos ctx infos tt def isInstance (declName : Name) : MetaM Bool := do - pure $ (instanceExtension.getState (←getEnv)).instanceNames.contains declName + pure <| (instanceExtension.getState (←getEnv)).instanceNames.contains declName end DocGen4.Process diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean index 24df630..8a1805a 100644 --- a/DocGen4/Process/DefinitionInfo.lean +++ b/DocGen4/Process/DefinitionInfo.lean @@ -45,13 +45,13 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := match eqs? with | some eqs => let prettyEqs ← eqs.mapM processEq - pure $ DefinitionInfo.mk info isUnsafe v.hints prettyEqs isNonComput + pure <| DefinitionInfo.mk info isUnsafe v.hints prettyEqs isNonComput | none => - let eq ← prettyPrintTerm $ stripArgs (←valueToEq v) - pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isNonComput + let eq ← prettyPrintTerm <| stripArgs (←valueToEq v) + pure <| DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isNonComput catch err => IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}" - pure $ DefinitionInfo.mk info isUnsafe v.hints none isNonComput + pure <| DefinitionInfo.mk info isUnsafe v.hints none isNonComput end DocGen4.Process diff --git a/DocGen4/Process/DocInfo.lean b/DocGen4/Process/DocInfo.lean index ad382ec..898f589 100644 --- a/DocGen4/Process/DocInfo.lean +++ b/DocGen4/Process/DocInfo.lean @@ -103,8 +103,8 @@ def isBlackListed (declName : Name) : MetaM Bool := do | some _ => let env ← getEnv pure (declName.isInternal) - <||> (pure $ isAuxRecursor env declName) - <||> (pure $ isNoConfusion env declName) + <||> (pure <| isAuxRecursor env declName) + <||> (pure <| isNoConfusion env declName) <||> isRec declName <||> isMatcher declName -- TODO: Evaluate whether filtering out declarations without range is sensible @@ -134,10 +134,10 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, | ConstantInfo.thmInfo i => pure <| some <| theoremInfo (←TheoremInfo.ofTheoremVal i) | ConstantInfo.opaqueInfo i => pure <| some <| opaqueInfo (←OpaqueInfo.ofOpaqueVal i) | ConstantInfo.defnInfo i => - if ← (isProjFn i.name) then + if ←isProjFn i.name then pure none else - if (←isInstance i.name) then + if ←isInstance i.name then let info ← InstanceInfo.ofDefinitionVal i pure <| some <| instanceInfo info else @@ -156,9 +156,7 @@ def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, else pure <| some <| inductiveInfo (←InductiveInfo.ofInductiveVal i) -- we ignore these for now - | ConstantInfo.ctorInfo i => pure none - | ConstantInfo.recInfo i => pure none - | ConstantInfo.quotInfo i => pure none + | ConstantInfo.ctorInfo _ | ConstantInfo.recInfo _ | ConstantInfo.quotInfo _ => pure none def getKindDescription : DocInfo → String | axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom" @@ -179,7 +177,7 @@ def getKindDescription : DocInfo → String modifiers := modifiers.push "noncomputable" modifiers := modifiers.push "def" - pure $ String.intercalate " " modifiers.toList + pure <| String.intercalate " " modifiers.toList | instanceInfo i => Id.run do let mut modifiers := #[] if i.isUnsafe then @@ -188,7 +186,7 @@ def getKindDescription : DocInfo → String modifiers := modifiers.push "noncomputable" modifiers := modifiers.push "instance" - pure $ String.intercalate " " modifiers.toList + pure <| String.intercalate " " modifiers.toList | inductiveInfo i => if i.isUnsafe then "unsafe inductive" else "inductive" | structureInfo _ => "structure" | classInfo _ => "class" diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean index 7727e15..4831c9e 100644 --- a/DocGen4/Process/Hierarchy.lean +++ b/DocGen4/Process/Hierarchy.lean @@ -57,28 +57,28 @@ def getChildren : Hierarchy → HierarchyMap def isFile : Hierarchy → Bool | node _ f _ => f -partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do +partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run do let hn := h.getName let mut cs := h.getChildren if getNumParts hn + 1 == getNumParts n then match cs.find Name.cmp n with | none => - node hn h.isFile (cs.insert Name.cmp n $ empty n true) + node hn h.isFile (cs.insert Name.cmp n <| empty n true) | some (node _ true _) => h | some (node _ false ccs) => cs := cs.erase Name.cmp n - node hn h.isFile (cs.insert Name.cmp n $ node n true ccs) + node hn h.isFile (cs.insert Name.cmp n <| node n true ccs) else let leveledName := getNLevels n (getNumParts hn + 1) match cs.find Name.cmp leveledName with | some nextLevel => cs := cs.erase Name.cmp leveledName -- BUG? - node hn h.isFile $ cs.insert Name.cmp leveledName (nextLevel.insert! n) + node hn h.isFile <| cs.insert Name.cmp leveledName (nextLevel.insert! n) | none => let child := (insert! (empty leveledName false) n) - node hn h.isFile $ cs.insert Name.cmp leveledName child + node hn h.isFile <| cs.insert Name.cmp leveledName child partial def fromArray (names : Array Name) : Hierarchy := names.foldl insert! (empty anonymous false) @@ -106,7 +106,7 @@ partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Arr if (←entry.path.isDir) then children := children ++ (←fromDirectoryAux entry.path (.str previous entry.fileName)) else - children := children.push $ .str previous (entry.fileName.dropRight ".html".length) + children := children.push <| .str previous (entry.fileName.dropRight ".html".length) pure children def fromDirectory (dir : System.FilePath) : IO Hierarchy := do @@ -114,7 +114,7 @@ def fromDirectory (dir : System.FilePath) : IO Hierarchy := do for entry in ←System.FilePath.readDir dir do if !baseDirBlackList.contains entry.fileName && (←entry.path.isDir) then children := children ++ (←fromDirectoryAux entry.path (.mkSimple entry.fileName)) - pure $ Hierarchy.fromArray children + pure <| Hierarchy.fromArray children end Hierarchy end DocGen4 diff --git a/DocGen4/Process/InductiveInfo.lean b/DocGen4/Process/InductiveInfo.lean index 0302b1e..77c33e5 100644 --- a/DocGen4/Process/InductiveInfo.lean +++ b/DocGen4/Process/InductiveInfo.lean @@ -22,6 +22,6 @@ 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.ofTypedName name (←getConstructorType name)) - pure $ InductiveInfo.mk info ctors v.isUnsafe + pure <| InductiveInfo.mk info ctors v.isUnsafe end DocGen4.Process diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean index c4c4a07..7ce5e7e 100644 --- a/DocGen4/Process/InstanceInfo.lean +++ b/DocGen4/Process/InstanceInfo.lean @@ -17,8 +17,8 @@ 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 $ InstanceInfo.mk { info with attrs := info.attrs.push instAttr } className + pure <| InstanceInfo.mk { info with attrs := info.attrs.push instAttr } className else - pure $ InstanceInfo.mk info className + pure <| InstanceInfo.mk info className end DocGen4.Process diff --git a/DocGen4/Process/NameInfo.lean b/DocGen4/Process/NameInfo.lean index 4fd39e6..edda363 100644 --- a/DocGen4/Process/NameInfo.lean +++ b/DocGen4/Process/NameInfo.lean @@ -35,11 +35,11 @@ partial def typeToArgsType (e : Expr) : (Array (Name × Expr × BinderInfo) × E def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let (args, type) := typeToArgsType v.type - let args ← args.mapM (λ (n, e, b) => do pure $ Arg.mk n (←prettyPrintTerm e) b) + let args ← args.mapM (λ (n, e, b) => do pure <| Arg.mk n (←prettyPrintTerm e) b) let nameInfo ← NameInfo.ofTypedName v.name type match ←findDeclarationRanges? v.name with -- TODO: Maybe selection range is more relevant? Figure this out in the future - | some range => pure $ Info.mk nameInfo args range.range (←getAllAttributes v.name) + | some range => pure <| Info.mk nameInfo args range.range (←getAllAttributes v.name) | none => panic! s!"{v.name} is a declaration without position" end DocGen4.Process diff --git a/DocGen4/Process/OpaqueInfo.lean b/DocGen4/Process/OpaqueInfo.lean index 9fad69b..6a46778 100644 --- a/DocGen4/Process/OpaqueInfo.lean +++ b/DocGen4/Process/OpaqueInfo.lean @@ -18,9 +18,9 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do let env ← getEnv let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome if isPartial then - pure $ OpaqueInfo.mk info t DefinitionSafety.partial + 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 + pure <| OpaqueInfo.mk info t safety end DocGen4.Process diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean index 0cf8326..256b9b8 100644 --- a/DocGen4/Process/StructureInfo.lean +++ b/DocGen4/Process/StructureInfo.lean @@ -17,7 +17,7 @@ def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) := match type, n with | e, 0 => (e, []) | Expr.forallE name type body _, x + 1 => - let body := body.instantiate1 $ mkFVar ⟨name⟩ + let body := body.instantiate1 <| mkFVar ⟨name⟩ let next := dropArgs body x { next with snd := (name, type) :: next.snd} | e, x + 1 => panic! s!"No forallE left" @@ -28,8 +28,8 @@ def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : Meta let (_, fields) := dropArgs fieldFunction (ctor.numFields - parents) let mut fieldInfos := #[] for (name, type) in fields do - fieldInfos := fieldInfos.push $ ←NameInfo.ofTypedName (struct.append name) type - pure $ fieldInfos + fieldInfos := fieldInfos.push <| ←NameInfo.ofTypedName (struct.append name) type + pure <| fieldInfos def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do let info ← Info.ofConstantVal v.toConstantVal @@ -39,9 +39,9 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do match getStructureInfo? env v.name with | some i => if i.fieldNames.size - parents.size > 0 then - pure $ StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents (←NameInfo.ofTypedName ctor.name ctor.type) + pure <| StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents (←NameInfo.ofTypedName ctor.name ctor.type) else - pure $ StructureInfo.mk info #[] parents (←NameInfo.ofTypedName ctor.name ctor.type) + pure <| StructureInfo.mk info #[] parents (←NameInfo.ofTypedName ctor.name ctor.type) | none => panic! s!"{v.name} is not a structure" end DocGen4.Process diff --git a/DocGen4/Process/TheoremInfo.lean b/DocGen4/Process/TheoremInfo.lean index 37c6a91..b779b0a 100644 --- a/DocGen4/Process/TheoremInfo.lean +++ b/DocGen4/Process/TheoremInfo.lean @@ -14,6 +14,6 @@ open Lean Meta def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do let info ← Info.ofConstantVal v.toConstantVal - pure $ TheoremInfo.mk info + pure <| TheoremInfo.mk info end DocGen4.Process diff --git a/Main.lean b/Main.lean index f514be6..803b444 100644 --- a/Main.lean +++ b/Main.lean @@ -9,15 +9,15 @@ def findLeanInk? (p : Parsed) : IO (Option System.FilePath) := do | some ink => let inkPath := System.FilePath.mk ink.value if ←inkPath.pathExists then - pure $ some inkPath + pure <| some inkPath else - throw $ IO.userError "Invalid path to LeanInk binary provided" + throw <| IO.userError "Invalid path to LeanInk binary provided" | none => pure none def getTopLevelModules (p : Parsed) : IO (List String) := do let topLevelModules := p.variableArgsAs! String |>.toList if topLevelModules.length == 0 then - throw $ IO.userError "No topLevelModules provided." + throw <| IO.userError "No topLevelModules provided." pure topLevelModules def runSingleCmd (p : Parsed) : IO UInt32 := do @@ -42,7 +42,7 @@ def runIndexCmd (p : Parsed) : IO UInt32 := do def runDocGenCmd (p : Parsed) : IO UInt32 := do let modules : List String := p.variableArgsAs! String |>.toList if modules.length == 0 then - throw $ IO.userError "No modules provided." + throw <| IO.userError "No modules provided." let res ← lakeSetup modules match res with From 04387711deeac00969017bb20dfd8b42a5ac8ec0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 23 Jul 2022 13:04:36 +0200 Subject: [PATCH 2/4] chore: remove unused variables --- DocGen4/Output/DocString.lean | 3 +-- DocGen4/Process/DefinitionInfo.lean | 5 ++--- DocGen4/Process/InductiveInfo.lean | 1 - DocGen4/Process/StructureInfo.lean | 4 ++-- Main.lean | 2 +- 5 files changed, 6 insertions(+), 9 deletions(-) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index a501e08..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 diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean index 8a1805a..eb990a5 100644 --- a/DocGen4/Process/DefinitionInfo.lean +++ b/DocGen4/Process/DefinitionInfo.lean @@ -14,10 +14,10 @@ open Lean Meta Widget partial def stripArgs (e : Expr) : Expr := match e.consumeMData with - | Expr.lam name type body data => + | Expr.lam name _ body _ => let name := name.eraseMacroScopes stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩)) - | Expr.forallE name type body data => + | Expr.forallE name _ body _ => let name := name.eraseMacroScopes stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩)) | _ => e @@ -28,7 +28,6 @@ def processEq (eq : Name) : MetaM CodeWithInfos := do prettyPrintTerm final def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do - let env ← getEnv withOptions (tactic.hygienic.set . false) do lambdaTelescope v.value fun xs body => do let us := v.levelParams.map mkLevelParam diff --git a/DocGen4/Process/InductiveInfo.lean b/DocGen4/Process/InductiveInfo.lean index 77c33e5..e2a4db9 100644 --- a/DocGen4/Process/InductiveInfo.lean +++ b/DocGen4/Process/InductiveInfo.lean @@ -20,7 +20,6 @@ def getConstructorType (ctor : Name) : MetaM Expr := do 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.ofTypedName name (←getConstructorType name)) pure <| InductiveInfo.mk info ctors v.isUnsafe diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean index 256b9b8..ba92593 100644 --- a/DocGen4/Process/StructureInfo.lean +++ b/DocGen4/Process/StructureInfo.lean @@ -20,11 +20,11 @@ def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) := let body := body.instantiate1 <| mkFVar ⟨name⟩ let next := dropArgs body x { next with snd := (name, type) :: next.snd} - | e, x + 1 => panic! s!"No forallE left" + | _e, _x + 1 => panic! s!"No forallE left" def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : MetaM (Array NameInfo) := do let type := ctor.type - let (fieldFunction, params) := dropArgs type (ctor.numParams + parents) + let (fieldFunction, _) := dropArgs type (ctor.numParams + parents) let (_, fields) := dropArgs fieldFunction (ctor.numFields - parents) let mut fieldInfos := #[] for (name, type) in fields do diff --git a/Main.lean b/Main.lean index 803b444..00606b7 100644 --- a/Main.lean +++ b/Main.lean @@ -33,7 +33,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do pure 0 | Except.error rc => pure rc -def runIndexCmd (p : Parsed) : IO UInt32 := do +def runIndexCmd (_p : Parsed) : IO UInt32 := do let hierarchy ← Hierarchy.fromDirectory basePath let baseConfig := getSimpleBaseContext hierarchy htmlOutputIndex baseConfig From 3aae640f69bf33c77f0b07b78930942f9c934874 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 23 Jul 2022 13:37:17 +0200 Subject: [PATCH 3/4] chore: structure ctor style --- DocGen4/Output/ToJson.lean | 2 +- DocGen4/Process/AxiomInfo.lean | 5 ++++- DocGen4/Process/Base.lean | 4 ++-- DocGen4/Process/DefinitionInfo.lean | 31 +++++++++++++++++++++++------ DocGen4/Process/DocInfo.lean | 2 +- DocGen4/Process/InductiveInfo.lean | 6 +++++- DocGen4/Process/InstanceInfo.lean | 12 +++++++---- DocGen4/Process/NameInfo.lean | 7 ++++++- DocGen4/Process/OpaqueInfo.lean | 19 ++++++++++++------ DocGen4/Process/StructureInfo.lean | 17 +++++++++++++--- DocGen4/Process/TheoremInfo.lean | 2 +- 11 files changed, 80 insertions(+), 27 deletions(-) diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index 954560b..67a37c7 100644 --- a/DocGen4/Output/ToJson.lean +++ b/DocGen4/Output/ToJson.lean @@ -40,7 +40,7 @@ def Process.Module.toJson (module : Process.Module) : HtmlM Json := do for decl in declInfo do jsonDecls := (←DocInfo.toJson module.name decl) :: jsonDecls if let .instanceInfo i := decl then - instances := instances.push { name := i.name.toString, className := i.instClass.toString} + instances := instances.push { name := i.name.toString, className := i.className.toString} let jsonMod : JsonModule := { name := module.name.toString, declarations := jsonDecls, diff --git a/DocGen4/Process/AxiomInfo.lean b/DocGen4/Process/AxiomInfo.lean index 817af6f..df0cb48 100644 --- a/DocGen4/Process/AxiomInfo.lean +++ b/DocGen4/Process/AxiomInfo.lean @@ -14,6 +14,9 @@ open Lean Meta def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do let info ← Info.ofConstantVal v.toConstantVal - pure <| AxiomInfo.mk info v.isUnsafe + pure { + toInfo := info, + isUnsafe := v.isUnsafe + } end DocGen4.Process diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean index 8bc9d98..487f687 100644 --- a/DocGen4/Process/Base.lean +++ b/DocGen4/Process/Base.lean @@ -87,7 +87,7 @@ structure OpaqueInfo extends Info where A value of partial is interpreted as this opaque being part of a partial def since the actual definition for a partial def is hidden behind an inaccessible value. -/ - unsafeInformation : DefinitionSafety + definitionSafety : DefinitionSafety deriving Inhabited /-- @@ -104,7 +104,7 @@ structure DefinitionInfo extends Info where Information about an `instance` declaration. -/ structure InstanceInfo extends DefinitionInfo where - instClass : Name + className : Name deriving Inhabited /-- diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean index eb990a5..769d050 100644 --- a/DocGen4/Process/DefinitionInfo.lean +++ b/DocGen4/Process/DefinitionInfo.lean @@ -38,19 +38,38 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do let info ← Info.ofConstantVal v.toConstantVal let isUnsafe := v.safety == DefinitionSafety.unsafe - let isNonComput := isNoncomputable (←getEnv) v.name + let isNonComputable := isNoncomputable (←getEnv) v.name try let eqs? ← getEqnsFor? v.name match eqs? with | some eqs => - let prettyEqs ← eqs.mapM processEq - pure <| DefinitionInfo.mk info isUnsafe v.hints prettyEqs isNonComput + let equations ← eqs.mapM processEq + pure { + toInfo := info, + isUnsafe, + hints := v.hints, + equations, + isNonComputable + } | none => - let eq ← prettyPrintTerm <| stripArgs (←valueToEq v) - pure <| DefinitionInfo.mk info isUnsafe v.hints (some #[eq]) isNonComput + let equations := #[←prettyPrintTerm <| stripArgs (←valueToEq v)] + pure { + toInfo := info, + isUnsafe, + hints := v.hints, + equations, + isNonComputable + } catch err => IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}" - pure <| DefinitionInfo.mk info isUnsafe v.hints none isNonComput + pure { + toInfo := info, + isUnsafe, + hints := v.hints, + equations := none, + isNonComputable + } + end DocGen4.Process diff --git a/DocGen4/Process/DocInfo.lean b/DocGen4/Process/DocInfo.lean index 898f589..4407f0f 100644 --- a/DocGen4/Process/DocInfo.lean +++ b/DocGen4/Process/DocInfo.lean @@ -162,7 +162,7 @@ def getKindDescription : DocInfo → String | axiomInfo i => if i.isUnsafe then "unsafe axiom" else "axiom" | theoremInfo _ => "theorem" | opaqueInfo i => - match i.unsafeInformation with + match i.definitionSafety with | DefinitionSafety.safe => "opaque" | DefinitionSafety.unsafe => "unsafe opaque" | DefinitionSafety.partial => "partial def" diff --git a/DocGen4/Process/InductiveInfo.lean b/DocGen4/Process/InductiveInfo.lean index e2a4db9..c4f911b 100644 --- a/DocGen4/Process/InductiveInfo.lean +++ b/DocGen4/Process/InductiveInfo.lean @@ -21,6 +21,10 @@ def getConstructorType (ctor : Name) : MetaM Expr := do def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do let info ← Info.ofConstantVal v.toConstantVal let ctors ← v.ctors.mapM (λ name => do NameInfo.ofTypedName name (←getConstructorType name)) - pure <| InductiveInfo.mk info ctors v.isUnsafe + pure { + toInfo := info, + ctors, + isUnsafe := v.isUnsafe + } end DocGen4.Process diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean index 7ce5e7e..ac4e275 100644 --- a/DocGen4/Process/InstanceInfo.lean +++ b/DocGen4/Process/InstanceInfo.lean @@ -14,11 +14,15 @@ namespace DocGen4.Process open Lean Meta def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do - let info ← DefinitionInfo.ofDefinitionVal v + let mut info ← DefinitionInfo.ofDefinitionVal v let some className := getClassName (←getEnv) v.type | unreachable! + if let some instAttr ← getDefaultInstance v.name className then - pure <| InstanceInfo.mk { info with attrs := info.attrs.push instAttr } className - else - pure <| InstanceInfo.mk info className + info := { info with attrs := info.attrs.push instAttr } + + pure { + toDefinitionInfo := info, + className + } end DocGen4.Process diff --git a/DocGen4/Process/NameInfo.lean b/DocGen4/Process/NameInfo.lean index edda363..af52073 100644 --- a/DocGen4/Process/NameInfo.lean +++ b/DocGen4/Process/NameInfo.lean @@ -39,7 +39,12 @@ def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do let nameInfo ← NameInfo.ofTypedName v.name type match ←findDeclarationRanges? v.name with -- TODO: Maybe selection range is more relevant? Figure this out in the future - | some range => pure <| Info.mk nameInfo args range.range (←getAllAttributes v.name) + | some range => pure { + toNameInfo := nameInfo, + args, + declarationRange := range.range, + attrs := (←getAllAttributes v.name) + } | none => panic! s!"{v.name} is a declaration without position" end DocGen4.Process diff --git a/DocGen4/Process/OpaqueInfo.lean b/DocGen4/Process/OpaqueInfo.lean index 6a46778..f3ca217 100644 --- a/DocGen4/Process/OpaqueInfo.lean +++ b/DocGen4/Process/OpaqueInfo.lean @@ -14,13 +14,20 @@ open Lean Meta def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do let info ← Info.ofConstantVal v.toConstantVal - let t ← prettyPrintTerm v.value + let value ← prettyPrintTerm v.value 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 + let definitionSafety := + if isPartial then + DefinitionSafety.partial + else if v.isUnsafe then + DefinitionSafety.unsafe + else + DefinitionSafety.safe + pure { + toInfo := info, + value, + definitionSafety + } end DocGen4.Process diff --git a/DocGen4/Process/StructureInfo.lean b/DocGen4/Process/StructureInfo.lean index ba92593..3fec571 100644 --- a/DocGen4/Process/StructureInfo.lean +++ b/DocGen4/Process/StructureInfo.lean @@ -35,13 +35,24 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do let info ← Info.ofConstantVal v.toConstantVal let env ← getEnv let parents := getParentStructures env v.name - let ctor := getStructureCtor env v.name + let ctorVal := getStructureCtor env v.name + let ctor ← NameInfo.ofTypedName ctorVal.name ctorVal.type match getStructureInfo? env v.name with | some i => if i.fieldNames.size - parents.size > 0 then - pure <| StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents (←NameInfo.ofTypedName ctor.name ctor.type) + pure { + toInfo := info, + fieldInfo := (←getFieldTypes v.name ctorVal parents.size), + parents, + ctor + } else - pure <| StructureInfo.mk info #[] parents (←NameInfo.ofTypedName ctor.name ctor.type) + pure { + toInfo := info, + fieldInfo := #[], + parents, + ctor + } | none => panic! s!"{v.name} is not a structure" end DocGen4.Process diff --git a/DocGen4/Process/TheoremInfo.lean b/DocGen4/Process/TheoremInfo.lean index b779b0a..3375bc7 100644 --- a/DocGen4/Process/TheoremInfo.lean +++ b/DocGen4/Process/TheoremInfo.lean @@ -14,6 +14,6 @@ open Lean Meta def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do let info ← Info.ofConstantVal v.toConstantVal - pure <| TheoremInfo.mk info + pure { toInfo := info } end DocGen4.Process From 247b930364d317cb3ad21899b3dcc44b3c8f1213 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sat, 23 Jul 2022 15:40:08 +0200 Subject: [PATCH 4/4] feat: instances for --- DocGen4/Output.lean | 10 +++++++++- DocGen4/Output/Class.lean | 3 --- DocGen4/Output/Inductive.lean | 8 ++++++++ DocGen4/Output/Module.lean | 2 ++ DocGen4/Output/ToJson.lean | 9 +++++++-- DocGen4/Process/Base.lean | 1 + DocGen4/Process/InstanceInfo.lean | 16 ++++++++++++++-- static/declaration-data.js | 13 +++++++++++++ static/instances.js | 25 +++++++++++++++++++++---- 9 files changed, 75 insertions(+), 12 deletions(-) diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 07b1229..5016b3b 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -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/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/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 +
      +
      def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do let shortName := c.name.components'.head!.toString diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 278c929..97414d5 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -106,6 +106,8 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do | DocInfo.definitionInfo i => equationsToHtml i | DocInfo.instanceInfo i => equationsToHtml i.toDefinitionInfo | DocInfo.classInductiveInfo i => pure #[←classInstancesToHtml i.name] + | DocInfo.inductiveInfo i => pure #[←instancesForToHtml i.name] + | DocInfo.structureInfo i => pure #[←instancesForToHtml i.name] | _ => pure #[] let attrs := doc.getAttrs let attrsHtml := diff --git a/DocGen4/Output/ToJson.lean b/DocGen4/Output/ToJson.lean index 67a37c7..25e8b9c 100644 --- a/DocGen4/Output/ToJson.lean +++ b/DocGen4/Output/ToJson.lean @@ -17,6 +17,7 @@ structure JsonDeclaration where structure JsonInstance where name : String className : String + typeNames : Array String deriving FromJson, ToJson structure JsonModule where @@ -40,11 +41,15 @@ def Process.Module.toJson (module : Process.Module) : HtmlM Json := do for decl in declInfo do jsonDecls := (←DocInfo.toJson module.name decl) :: jsonDecls if let .instanceInfo i := decl then - instances := instances.push { name := i.name.toString, className := i.className.toString} + instances := instances.push { + name := i.name.toString, + className := i.className.toString + typeNames := i.typeNames.map Name.toString + } let jsonMod : JsonModule := { name := module.name.toString, declarations := jsonDecls, - instances := instances + instances, imports := module.imports.map Name.toString } pure <| ToJson.toJson jsonMod diff --git a/DocGen4/Process/Base.lean b/DocGen4/Process/Base.lean index 487f687..d7bcb1b 100644 --- a/DocGen4/Process/Base.lean +++ b/DocGen4/Process/Base.lean @@ -105,6 +105,7 @@ Information about an `instance` declaration. -/ structure InstanceInfo extends DefinitionInfo where className : Name + typeNames : Array Name deriving Inhabited /-- diff --git a/DocGen4/Process/InstanceInfo.lean b/DocGen4/Process/InstanceInfo.lean index ac4e275..dbccd67 100644 --- a/DocGen4/Process/InstanceInfo.lean +++ b/DocGen4/Process/InstanceInfo.lean @@ -11,7 +11,17 @@ import DocGen4.Process.DefinitionInfo namespace DocGen4.Process -open Lean Meta +open Lean Meta + +def getInstanceTypes (typ : Expr) : MetaM (Array Name) := do + let (_, _, tail) ← forallMetaTelescopeReducing typ + let args := tail.getAppArgs + let (_, bar) ← args.mapM (Expr.forEach · findName) |>.run .empty + pure bar +where + findName : Expr → StateRefT (Array Name) MetaM Unit + | .const name _ => do set <| (←get).push name + | _ => pure () def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do let mut info ← DefinitionInfo.ofDefinitionVal v @@ -19,10 +29,12 @@ def InstanceInfo.ofDefinitionVal (v : DefinitionVal) : MetaM InstanceInfo := do if let some instAttr ← getDefaultInstance v.name className then info := { info with attrs := info.attrs.push instAttr } + let typeNames ← getInstanceTypes v.type pure { toDefinitionInfo := info, - className + className, + typeNames } end DocGen4.Process diff --git a/static/declaration-data.js b/static/declaration-data.js index a12d4f1..953edf2 100644 --- a/static/declaration-data.js +++ b/static/declaration-data.js @@ -92,6 +92,19 @@ export class DeclarationDataCenter { } } + /** + * Search for all instances that involve a certain type + * @returns {Array} + */ + instancesForType(typeName) { + const instances = this.declarationData.instancesFor[typeName]; + if (!instances) { + return []; + } else { + return instances; + } + } + /** * Analogous to Lean declNameToLink * @returns {String} diff --git a/static/instances.js b/static/instances.js index cc7d113..fa73c5c 100644 --- a/static/instances.js +++ b/static/instances.js @@ -1,19 +1,36 @@ import { DeclarationDataCenter } from "./declaration-data.js"; annotateInstances(); +annotateInstancesFor() async function annotateInstances() { const dataCenter = await DeclarationDataCenter.init(); - const instanceLists = [...(document.querySelectorAll(".instances-list"))]; + const instanceForLists = [...(document.querySelectorAll(".instances-list"))]; - for (const instanceList of instanceLists) { - const className = instanceList.id.slice("instances-list-".length); + for (const instanceForList of instanceForLists) { + const className = instanceForList.id.slice("instances-list-".length); const instances = dataCenter.instancesForClass(className); var innerHTML = ""; for(var instance of instances) { const instanceLink = dataCenter.declNameToLink(instance); innerHTML += `
    • ${instance}
      • ` } - instanceList.innerHTML = innerHTML; + instanceForList.innerHTML = innerHTML; + } +} + +async function annotateInstancesFor() { + const dataCenter = await DeclarationDataCenter.init(); + const instanceForLists = [...(document.querySelectorAll(".instances-for-list"))]; + + for (const instanceForList of instanceForLists) { + const typeName = instanceForList.id.slice("instances-for-list-".length); + const instances = dataCenter.instancesForType(typeName); + var innerHTML = ""; + for(var instance of instances) { + const instanceLink = dataCenter.declNameToLink(instance); + innerHTML += `
    • ${instance}
      • ` + } + instanceForList.innerHTML = innerHTML; } }