Merge pull request #73 from leanprover/refactor

A little refactoring + instances for feature
main
Henrik Böving 2022-07-23 15:45:41 +02:00 committed by GitHub
commit 3924034385
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
32 changed files with 241 additions and 137 deletions

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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`

View File

@ -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

View File

@ -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 := <a href={←declNameToLink name}>{t}</a>
pure #[Html.text front, elem, Html.text back]
| _ =>

View File

@ -8,9 +8,6 @@ namespace Output
open scoped DocGen4.Jsx
open Lean
--def classInstanceToHtml (name : Name) : HtmlM Html := do
-- pure <li>{←declNameToHtmlLink name}</li>
def classInstancesToHtml (className : Name) : HtmlM Html := do
pure
<details «class»="instances">

View File

@ -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

View File

@ -11,7 +11,8 @@ namespace Output
open scoped DocGen4.Jsx
def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") $ pure $
def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
pure <|
<main>
<a id="top"></a>
<h1> Welcome to the documentation page </h1>

View File

@ -6,6 +6,14 @@ namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
open Lean
def instancesForToHtml (typeName : Name) : HtmlM Html := do
pure
<details «class»="instances">
<summary>Instances For</summary>
<ul id={s!"instances-for-list-{typeName}"} class="instances-for-list"></ul>
</details>
def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do
let shortName := c.name.components'.head!.toString

View File

@ -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
<span class="decl_name">
<a class="break_within" href={←declNameToLink doc.getName}>
@ -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 :=
@ -168,7 +170,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 +209,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
]

View File

@ -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 <div class="module_list">[list]</div>
/--

View File

@ -14,7 +14,8 @@ open scoped DocGen4.Jsx
/--
Render the 404 page.
-/
def notFound : BaseHtmlM Html := do templateExtends (baseHtml "404") $ pure $
def notFound : BaseHtmlM Html := do templateExtends (baseHtml "404") <|
pure <|
<main>
<h1>404 Not Found</h1>
<p> Unfortunately, the page you were looking for is no longer here. </p>

View File

@ -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

View File

@ -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

View File

@ -17,6 +17,7 @@ structure JsonDeclaration where
structure JsonInstance where
name : String
className : String
typeNames : Array String
deriving FromJson, ToJson
structure JsonModule where
@ -40,13 +41,17 @@ 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
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
pure <| ToJson.toJson jsonMod
end DocGen4.Output

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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,8 @@ structure DefinitionInfo extends Info where
Information about an `instance` declaration.
-/
structure InstanceInfo extends DefinitionInfo where
instClass : Name
className : Name
typeNames : Array Name
deriving Inhabited
/--
@ -176,9 +177,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

View File

@ -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
@ -39,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

View File

@ -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,15 +156,13 @@ 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"
| theoremInfo _ => "theorem"
| opaqueInfo i =>
match i.unsafeInformation with
match i.definitionSafety with
| DefinitionSafety.safe => "opaque"
| DefinitionSafety.unsafe => "unsafe opaque"
| DefinitionSafety.partial => "partial def"
@ -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"

View File

@ -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

View File

@ -20,8 +20,11 @@ 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
pure {
toInfo := info,
ctors,
isUnsafe := v.isUnsafe
}
end DocGen4.Process

View File

@ -13,12 +13,28 @@ namespace DocGen4.Process
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 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 }
let typeNames ← getInstanceTypes v.type
pure {
toDefinitionInfo := info,
className,
typeNames
}
end DocGen4.Process

View File

@ -35,11 +35,16 @@ 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 {
toNameInfo := nameInfo,
args,
declarationRange := range.range,
attrs := (←getAllAttributes v.name)
}
| none => panic! s!"{v.name} is a declaration without position"
end DocGen4.Process

View File

@ -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
let definitionSafety :=
if isPartial then
pure $ OpaqueInfo.mk info t DefinitionSafety.partial
DefinitionSafety.partial
else if v.isUnsafe then
DefinitionSafety.unsafe
else
let safety := if v.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
pure $ OpaqueInfo.mk info t safety
DefinitionSafety.safe
pure {
toInfo := info,
value,
definitionSafety
}
end DocGen4.Process

View File

@ -17,31 +17,42 @@ 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"
| _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
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
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

View File

@ -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

View File

@ -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
@ -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
@ -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

View File

@ -92,6 +92,19 @@ export class DeclarationDataCenter {
}
}
/**
* Search for all instances that involve a certain type
* @returns {Array<String>}
*/
instancesForType(typeName) {
const instances = this.declarationData.instancesFor[typeName];
if (!instances) {
return [];
} else {
return instances;
}
}
/**
* Analogous to Lean declNameToLink
* @returns {String}

View File

@ -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 += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
}
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 += `<li><a href="${SITE_ROOT}${instanceLink}">${instance}</a></li>`
}
instanceForList.innerHTML = innerHTML;
}
}