def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
let instancesHtml ← instances.mapM classInstanceToHtml
- return
+ pure
+ Instances
[instancesHtml]
@@ -20,7 +21,7 @@ def classInstancesToHtml (instances : Array Name) : HtmlM Html := do
def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
- (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
+ pure $ (←structureToHtml i.toStructureInfo).push (←classInstancesToHtml i.instances)
end Output
end DocGen4
diff --git a/DocGen4/Output/ClassInductive.lean b/DocGen4/Output/ClassInductive.lean
index 0e07f72..6113e73 100644
--- a/DocGen4/Output/ClassInductive.lean
+++ b/DocGen4/Output/ClassInductive.lean
@@ -7,7 +7,7 @@ namespace DocGen4
namespace Output
def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do
- (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
+ pure $ (←inductiveToHtml i.toInductiveInfo).push (←classInstancesToHtml i.instances)
end Output
end DocGen4
diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean
index f92627c..64813d4 100644
--- a/DocGen4/Output/Definition.lean
+++ b/DocGen4/Output/Definition.lean
@@ -7,26 +7,27 @@ open scoped DocGen4.Jsx
open Lean Widget
def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
-
[←infoFormatToHtml c]
+ pure
[←infoFormatToHtml c]
def equationsToHtml (i : DefinitionInfo) : HtmlM (Option Html) := do
- if let some eqs ← i.equations then
+ if let some eqs := i.equations then
let equationsHtml ← eqs.mapM equationToHtml
- return
- Equations
-
- [equationsHtml]
-
-
+ pure
+
+ Equations
+
+ [equationsHtml]
+
+
else
- return none
+ pure none
def definitionToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
let equationsHtml ← equationsToHtml i
- if let some equationsHtml ← equationsHtml then
- #[equationsHtml]
+ if let some equationsHtml := equationsHtml then
+ pure #[equationsHtml]
else
- #[]
+ pure #[]
end Output
end DocGen4
diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean
index b09ac47..e0342b6 100644
--- a/DocGen4/Output/Index.lean
+++ b/DocGen4/Output/Index.lean
@@ -11,7 +11,7 @@ namespace Output
open scoped DocGen4.Jsx
-def index : HtmlM Html := do templateExtends (baseHtml "Index") $
+def index : HtmlM Html := do templateExtends (baseHtml "Index") $ pure $
Welcome to the documentation page
diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean
index 0aa9444..d8f84df 100644
--- a/DocGen4/Output/Inductive.lean
+++ b/DocGen4/Output/Inductive.lean
@@ -8,10 +8,10 @@ open scoped DocGen4.Jsx
def ctorToHtml (i : NameInfo) : HtmlM Html := do
let shortName := i.name.components'.head!.toString
let name := i.name.toString
- return
]
+def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
+ pure #[
[← i.ctors.toArray.mapM ctorToHtml]
]
end Output
end DocGen4
diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean
index 6e50374..94d7827 100644
--- a/DocGen4/Output/Module.lean
+++ b/DocGen4/Output/Module.lean
@@ -31,9 +31,9 @@ def argToHtml (arg : Arg) : HtmlM Html := do
let inner := Html.element "span" true #[("class", "fn")] nodes
let html := Html.element "span" false #[("class", "decl_args")] #[inner]
if implicit then
- {html}
+ pure {html}
else
- html
+ pure html
def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
let mut nodes := #[]
@@ -46,7 +46,7 @@ def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
parents := parents.push html
nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray
- nodes
+ pure nodes
def docInfoHeader (doc : DocInfo) : HtmlM Html := do
let mut nodes := #[]
@@ -69,7 +69,7 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
nodes := nodes.push :
nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
- return
[nodes]
+ pure
[nodes]
def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
let doc_html ← match doc with
@@ -79,18 +79,19 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
| DocInfo.definitionInfo i => definitionToHtml i
| DocInfo.instanceInfo i => instanceToHtml i
| DocInfo.classInductiveInfo i => classInductiveToHtml i
- | _ => #[]
+ | _ => pure #[]
- return
def declarationToNavLink (module : Name) : Html :=
@@ -99,61 +100,62 @@ def declarationToNavLink (module : Name) : Html :=
-- TODO: Similar functions are used all over the place, we should dedup them
def moduleToNavLink (module : Name) : HtmlM Html := do
- {module.toString}
+ pure {module.toString}
def getImports (module : Name) : HtmlM (Array Name) := do
let res ← getResult
- let some idx ← res.moduleNames.findIdx? (. == module) | unreachable!
+ let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
let adj := res.importAdj.get! idx
let mut imports := #[]
for i in [:adj.size] do
if adj.get! i then
imports := imports.push (res.moduleNames.get! i)
- imports
+ pure imports
def getImportedBy (module : Name) : HtmlM (Array Name) := do
let res ← getResult
- let some idx ← res.moduleNames.findIdx? (. == module) | unreachable!
+ let some idx := res.moduleNames.findIdx? (. == module) | unreachable!
let adj := res.importAdj
let mut impBy := #[]
for i in [:adj.size] do
if adj.get! i |>.get! idx then
impBy := impBy.push (res.moduleNames.get! i)
- impBy
+ pure impBy
def importedByHtml (moduleName : Name) : HtmlM (Array Html) := do
let imports := (←getImportedBy moduleName) |>.qsort Name.lt
- imports.mapM (λ i => do
{←moduleToNavLink i}
)
+ imports.mapM (λ i => do pure
{←moduleToNavLink i}
)
def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
let imports := (←getImports moduleName) |>.qsort Name.lt
- imports.mapM (λ i => do
{←moduleToNavLink i}
)
+ imports.mapM (λ i => do pure
{←moduleToNavLink i}
)
def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
-
+ pure
+
def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
let docInfos ← module.members.mapM (λ i => docInfoToHtml module.name i)
- templateExtends (baseHtmlArray module.name.toString) $ #[
+ templateExtends (baseHtmlArray module.name.toString) $ pure #[
←internalNav (module.members.map DocInfo.getName) module.name,
Html.element "main" false #[] docInfos
]
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index fee4598..d2d4792 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -13,8 +13,8 @@ namespace Output
open Lean
open scoped DocGen4.Jsx
-def moduleListFile (file : Name) : HtmlM Html :=
- return
+def moduleListFile (file : Name) : HtmlM Html := do
+ pure
@@ -25,36 +25,38 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
let dirNodes ← (dirs.mapM moduleListDir)
let fileNodes ← (files.mapM moduleListFile)
let moduleLink ← moduleNameToLink h.getName
- return
- {h.getName.toString}
- [dirNodes]
- [fileNodes]
-
+ pure
+
+ {h.getName.toString}
+ [dirNodes]
+ [fileNodes]
+
def moduleList : HtmlM Html := do
let hierarchy := (←getResult).hierarchy
let mut list := Array.empty
for (n, cs) in hierarchy.getChildren do
list := list.push $ ←moduleListDir cs
- return
[list]
+ pure
[list]
def navbar : HtmlM Html := do
-
+ pure
+
end Output
end DocGen4
diff --git a/DocGen4/Output/NotFound.lean b/DocGen4/Output/NotFound.lean
index ed5d547..a700963 100644
--- a/DocGen4/Output/NotFound.lean
+++ b/DocGen4/Output/NotFound.lean
@@ -11,7 +11,7 @@ namespace Output
open scoped DocGen4.Jsx
-def notFound : HtmlM Html := do templateExtends (baseHtml "404") $
+def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ pure $
404 Not Found
Unfortunately, the page you were looking for is no longer here.
diff --git a/DocGen4/Output/Structure.lean b/DocGen4/Output/Structure.lean
index 688324f..23212ae 100644
--- a/DocGen4/Output/Structure.lean
+++ b/DocGen4/Output/Structure.lean
@@ -9,16 +9,18 @@ open Lean
def fieldToHtml (f : NameInfo) : HtmlM Html := do
let shortName := f.name.components'.head!.toString
let name := f.name.toString
- return
{s!"{shortName} "} : [←infoFormatToHtml f.type]
+ pure
{s!"{shortName} "} : [←infoFormatToHtml f.type]
def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
if Name.isSuffixOf `mk i.ctor.name then
- #[
- [←i.fieldInfo.mapM fieldToHtml]
-
]
+ pure #[
+
+ [←i.fieldInfo.mapM fieldToHtml]
+
]
else
let ctorShortName := i.ctor.name.components'.head!.toString
- #[
- -- TODO: Replace this form with our own search
-
-
+
+
Documentation
+
{title}
+ -- TODO: Replace this form with our own search
+
+
- [site]
-
- {←navbar}
+ [site]
+
+ {←navbar}
- -- Lean in JS in HTML in Lean...very meta
-
+ -- Lean in JS in HTML in Lean...very meta
+
- -- TODO Add more js stuff
-
-
-
+ -- TODO Add more js stuff
+
+
+
def baseHtml (title : String) (site : Html) : HtmlM Html := baseHtmlArray title #[site]
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index c4b0e46..363863d 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -140,7 +140,7 @@ def prettyPrintTerm (expr : Expr) : MetaM CodeWithInfos := do
openDecls := ← getOpenDecls
fileMap := default
}
- return tagExprInfos ctx infos tt
+ pure $ tagExprInfos ctx infos tt
def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let env ← getEnv
@@ -150,16 +150,16 @@ def Info.ofConstantVal (v : ConstantVal) : MetaM Info := do
let doc ← findDocString? env v.name
match ←findDeclarationRanges? v.name with
-- TODO: Maybe selection range is more relevant? Figure this out in the future
- | some range => return Info.mk ⟨v.name, type⟩ args doc range.range
+ | some range => pure $ Info.mk ⟨v.name, type⟩ args doc range.range
| none => panic! s!"{v.name} is a declaration without position"
def AxiomInfo.ofAxiomVal (v : AxiomVal) : MetaM AxiomInfo := do
let info ← Info.ofConstantVal v.toConstantVal
- return AxiomInfo.mk info v.isUnsafe
+ pure $ AxiomInfo.mk info v.isUnsafe
def TheoremInfo.ofTheoremVal (v : TheoremVal) : MetaM TheoremInfo := do
let info ← Info.ofConstantVal v.toConstantVal
- return TheoremInfo.mk info
+ pure $ TheoremInfo.mk info
def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
let info ← Info.ofConstantVal v.toConstantVal
@@ -167,13 +167,13 @@ def OpaqueInfo.ofOpaqueVal (v : OpaqueVal) : MetaM OpaqueInfo := do
let env ← getEnv
let isPartial := env.find? (Compiler.mkUnsafeRecName v.name) |>.isSome
if isPartial then
- return 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
- return OpaqueInfo.mk info t safety
+ pure $ OpaqueInfo.mk info t safety
def isInstance (declName : Name) : MetaM Bool := do
- return (instanceExtension.getState (←getEnv)).instanceNames.contains declName
+ pure $ (instanceExtension.getState (←getEnv)).instanceNames.contains declName
partial def stripArgs (e : Expr) : Expr :=
match e.consumeMData with
@@ -213,7 +213,7 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
pure $ DefinitionInfo.mk info isUnsafe v.hints (some #[eq])
catch err =>
IO.println s!"WARNING: Failed to calculate equational lemmata for {v.name}: {←err.toMessageData.toString}"
- return DefinitionInfo.mk info isUnsafe v.hints none
+ pure $ DefinitionInfo.mk info isUnsafe v.hints none
def getConstructorType (ctor : Name) : MetaM CodeWithInfos := do
let env ← getEnv
@@ -225,7 +225,7 @@ def InductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM InductiveInfo := do
let info ← Info.ofConstantVal v.toConstantVal
let env ← getEnv
let ctors ← v.ctors.mapM (λ name => do pure $ NameInfo.mk name (←getConstructorType name))
- return InductiveInfo.mk info ctors v.isUnsafe
+ pure $ InductiveInfo.mk info ctors v.isUnsafe
def dropArgs (type : Expr) (n : Nat) : (Expr × List (Name × Expr)) :=
match type, n with
@@ -243,7 +243,7 @@ def getFieldTypes (struct : Name) (ctor : ConstructorVal) (parents : Nat) : Meta
let mut field_infos := #[]
for (name, type) in fields do
field_infos := field_infos.push { name := struct.append name, type := ←prettyPrintTerm type}
- return field_infos
+ pure $ field_infos
def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
let info ← Info.ofConstantVal v.toConstantVal
@@ -254,24 +254,24 @@ def StructureInfo.ofInductiveVal (v : InductiveVal) : MetaM StructureInfo := do
match getStructureInfo? env v.name with
| some i =>
if i.fieldNames.size - parents.size > 0 then
- return StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
+ pure $ StructureInfo.mk info (←getFieldTypes v.name ctor parents.size) parents ⟨ctor.name, ctorType⟩
else
- return StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
+ pure $ StructureInfo.mk info #[] parents ⟨ctor.name, ctorType⟩
| none => panic! s!"{v.name} is not a structure"
def getInstances (className : Name) : MetaM (Array Name) := do
let fn ← mkConstWithFreshMVarLevels className
let (xs, _, _) ← forallMetaTelescopeReducing (← inferType fn)
let insts ← SynthInstance.getInstances (mkAppN fn xs)
- return insts.map Expr.constName!
+ pure $ insts.map Expr.constName!
def ClassInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInfo := do
let sinfo ← StructureInfo.ofInductiveVal v
- return ClassInfo.mk sinfo (←getInstances v.name)
+ pure $ ClassInfo.mk sinfo (←getInstances v.name)
def ClassInductiveInfo.ofInductiveVal (v : InductiveVal) : MetaM ClassInductiveInfo := do
let info ← InductiveInfo.ofInductiveVal v
- return ClassInductiveInfo.mk info (←getInstances v.name)
+ pure $ ClassInductiveInfo.mk info (←getInstances v.name)
namespace DocInfo
@@ -290,18 +290,18 @@ def isBlackListed (declName : Name) : MetaM Bool := do
-- TODO: Is this actually the best way?
def isProjFn (declName : Name) : MetaM Bool := do
let env ← getEnv
- return match declName with
+ match declName with
| Name.str parent name _ =>
if isStructure env parent then
match getStructureInfo? env parent with
| some i =>
match i.fieldNames.find? (· == name) with
- | some _ => true
- | none => false
+ | some _ => pure true
+ | none => pure false
| none => panic! s!"{parent} is not a structure"
else
- false
- | _ => false
+ pure false
+ | _ => pure false
def ofConstant : (Name × ConstantInfo) → MetaM (Option DocInfo) := λ (name, info) => do
if (←isBlackListed name) then
@@ -446,7 +446,7 @@ def process : MetaM AnalyzerResult := do
let some importIdx := env.getModuleIdx? imp.module | unreachable!
adj := adj.set! modIdx (adj.get! modIdx |>.set! importIdx true)
- return {
+ pure {
name2ModIdx := env.const2ModIdx,
moduleNames := env.header.moduleNames,
moduleInfo := res,
diff --git a/lean-toolchain b/lean-toolchain
index a68e3bc..4b598af 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-02-08
\ No newline at end of file
+leanprover/lean4:nightly-2022-02-11