diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 75966d0..d664866 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -66,10 +66,10 @@ def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : ReaderT.run x ctx |>.run baseCtx |>.run instance [Monad m] : MonadLift HtmlM (HtmlT m) where - monadLift x := do pure <| x.run (←readThe SiteContext) (←readThe SiteBaseContext) + monadLift x := do return x.run (← readThe SiteContext) (← readThe SiteBaseContext) instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where - monadLift x := do pure <| x.run (←readThe SiteBaseContext) + monadLift x := do return x.run (← readThe SiteBaseContext) /-- Obtains the root URL as a relative one to the current depth. @@ -81,11 +81,11 @@ def getRoot : BaseHtmlM String := do let d <- SiteBaseContext.depthToRoot <$> read return (go d) -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 leanInkEnabled? : HtmlM Bool := do pure (←read).leanInkEnabled +def getHierarchy : BaseHtmlM Hierarchy := do return (← read).hierarchy +def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName +def getResult : HtmlM AnalyzerResult := do return (← read).result +def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range +def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled /-- If a template is meant to be extended because it for example only provides the @@ -102,20 +102,20 @@ 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" + return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" /-- Returns the HTML doc-gen4 link to a module name. -/ def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do - pure {module.toString} + return {module.toString} /-- 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" + return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" /-- Returns the path to the HTML file that contains information about a module. @@ -158,13 +158,13 @@ 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 + return (← moduleNameToLink module) ++ "#" ++ name.toString /-- Returns the HTML doc-gen4 link to a declaration name. -/ def declNameToHtmlLink (name : Name) : HtmlM Html := do - pure {name.toString} + return {name.toString} /-- Returns the LeanInk link to a declaration name. @@ -172,14 +172,14 @@ 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 + return (← moduleNameToInkLink module) ++ "#" ++ name.toString /-- Returns the HTML doc-gen4 link to a declaration name with "break_within" set as class. -/ def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do - pure {name.toString} + return {name.toString} /-- In Lean syntax declarations the following pattern is quite common: @@ -207,8 +207,8 @@ to as much information as possible. -/ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do match i with - | .text t => pure #[Html.escape t] - | .append tt => tt.foldlM (λ acc t => do pure <| acc ++ (←infoFormatToHtml t)) #[] + | .text t => return #[Html.escape t] + | .append tt => tt.foldlM (fun acc t => do return acc ++ (← infoFormatToHtml t)) #[] | .tag a t => match a.info.val.info with | Info.ofTermInfo i => @@ -217,16 +217,16 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do | .const name _ => -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM -- find a better solution - if (←getResult).name2ModIdx.contains name then + if (← getResult).name2ModIdx.contains name then match t with | .text t => let (front, t, back) := splitWhitespaces <| Html.escape t - let elem := {t} - pure #[Html.text front, elem, Html.text back] + let elem := {t} + return #[Html.text front, elem, Html.text back] | _ => - pure #[[←infoFormatToHtml t]] + return #[[← infoFormatToHtml t]] else - pure #[[←infoFormatToHtml t]] + return #[[← infoFormatToHtml t]] | .sort _ => match t with | .text t => @@ -234,21 +234,21 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do let sortLink := {sortPrefix} if rest != [] then rest := " " :: rest - pure #[sortLink, Html.text <| String.join rest] + return #[sortLink, Html.text <| String.join rest] | _ => - pure #[[← infoFormatToHtml t]] + return #[[← infoFormatToHtml t]] | _ => - pure #[[←infoFormatToHtml t]] - | _ => pure #[[←infoFormatToHtml t]] + return #[[← infoFormatToHtml t]] + | _ => return #[[← infoFormatToHtml t]] def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do - pure #[ + return #[ , , - , - , - , - + , + , + , + ] end DocGen4.Output diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index 4b4e280..c468ceb 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -12,7 +12,7 @@ open Lean Widget def equationLimit : Nat := 200 def equationToHtml (c : CodeWithInfos) : HtmlM Html := do - pure
  • [←infoFormatToHtml c]
    • + return
  • [← infoFormatToHtml c]
    • /-- Attempt to render all `simp` equations for this definition. At a size @@ -23,9 +23,9 @@ defined in `equationLimit` we stop trying since they: def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do if let some eqs := i.equations then let equationsHtml ← eqs.mapM equationToHtml - let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit) + let filteredEquationsHtml := equationsHtml.filter (·.textLength < equationLimit) if equationsHtml.size ≠ filteredEquationsHtml.size then - pure #[ + return #[
    Equations
    ] else - pure #[ + return #[
    Equations
    ] else - pure #[] + return #[] end Output end DocGen4 diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index a4128bf..82ef367 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -23,7 +23,7 @@ namespace Output /-- Similar to `Stirng.split` in Lean core, but keeps the separater. - e.g. `splitAround "a,b,c" (λ c => c = ',') = ["a", ",", "b", ",", "c"]` + e.g. `splitAround "a,b,c" (fun c => c = ',') = ["a", ",", "b", ",", "c"]` -/ def splitAround (s : String) (p : Char → Bool) : List String := splitAroundAux s p 0 0 [] @@ -81,15 +81,15 @@ def nameToLink? (s : String) : HtmlM (Option String) := do match res.moduleInfo.find! currentName |>.members |> filterMapDocInfo |>.find? (sameEnd ·.getName name) with | some info => declNameToLink info.getName - | _ => pure none - | _ => pure none + | _ => return none + | _ => return none else - pure none + return none where -- check if two names have the same ending components sameEnd n1 n2 := List.zip n1.componentsRev n2.componentsRev - |>.all λ ⟨a, b⟩ => a == b + |>.all fun ⟨a, b⟩ => a == b /-- Extend links with following rules: @@ -103,16 +103,16 @@ def extendLink (s : String) : HtmlM String := do -- for intra doc links if s.startsWith "##" then if let some link ← nameToLink? (s.drop 2) then - pure link + return link else panic! s!"Cannot find {s.drop 2}, only full name and abbrev in current module is supported" -- for id else if s.startsWith "#" then - pure s + return s -- for absolute and relative urls else if s.startsWith "http" then - pure s - else pure ((←getRoot) ++ s) + return s + else return ((← getRoot) ++ s) /-- Add attributes for heading. -/ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Element) : HtmlM Element := do @@ -127,12 +127,12 @@ def addHeadingAttributes (el : Element) (modifyElement : Element → HtmlM Eleme |>.insert "id" id |>.insert "class" "markdown-heading" let newContents := (← - contents.mapM (λ c => match c with + contents.mapM (fun c => match c with | Content.Element e => return Content.Element (← modifyElement e) | _ => pure c)) |>.push (Content.Character " ") |>.push (Content.Element anchor) - pure ⟨ name, newAttrs, newContents⟩ + return ⟨ name, newAttrs, newContents⟩ /-- Extend anchor links. -/ def extendAnchor (el : Element) : HtmlM Element := do @@ -141,7 +141,7 @@ def extendAnchor (el : Element) : HtmlM Element := do let newAttrs ← match attrs.find? "href" with | some href => pure (attrs.insert "href" (← extendLink href)) | none => pure attrs - pure ⟨ name, newAttrs, contents⟩ + return ⟨ name, newAttrs, contents⟩ /-- Automatically add intra documentation link for inline code span. -/ def autoLink (el : Element) : HtmlM Element := do @@ -153,27 +153,27 @@ def autoLink (el : Element) : HtmlM Element := do | Content.Character s => newContents := newContents ++ (← splitAround s unicodeToSplit |>.mapM linkify).join | _ => newContents := newContents.push c - pure ⟨ name, attrs, newContents ⟩ + return ⟨ name, attrs, newContents ⟩ where linkify s := do let link? ← nameToLink? s match link? with | some link => let attributes := Lean.RBMap.empty.insert "href" link - pure [Content.Element <| Element.Element "a" attributes #[Content.Character s]] + return [Content.Element <| Element.Element "a" attributes #[Content.Character s]] | none => - let sHead := s.dropRightWhile (λ c => c ≠ '.') - let sTail := s.takeRightWhile (λ c => c ≠ '.') + let sHead := s.dropRightWhile (· != '.') + let sTail := s.takeRightWhile (· != '.') let link'? ← nameToLink? sTail match link'? with | some link' => let attributes := Lean.RBMap.empty.insert "href" link' - pure [ + return [ Content.Character sHead, Content.Element <| Element.Element "a" attributes #[Content.Character sTail] ] | none => - pure [Content.Character s] + return [Content.Character s] unicodeToSplit (c : Char) : Bool := charInGeneralCategory c GeneralCategory.separator || charInGeneralCategory c GeneralCategory.other @@ -192,19 +192,18 @@ partial def modifyElement (element : Element) : HtmlM Element := autoLink el -- recursively modify else - let newContents ← contents.mapM λ c => match c with + let newContents ← contents.mapM fun c => match c with | Content.Element e => return Content.Element (← modifyElement e) | _ => pure c - pure ⟨ name, attrs, newContents ⟩ + return ⟨ name, attrs, newContents ⟩ /-- Convert docstring to Html. -/ def docStringToHtml (s : String) : HtmlM (Array Html) := do let rendered := CMark.renderHtml s match manyDocument rendered.mkIterator with | Parsec.ParseResult.success _ res => - res.mapM λ x => do - pure (Html.text <| toString (← modifyElement x)) - | _ => pure #[Html.text rendered] + res.mapM fun x => do return Html.text <| toString (← modifyElement x) + | _ => return #[Html.text rendered] end Output end DocGen4 diff --git a/DocGen4/Output/Find.lean b/DocGen4/Output/Find.lean index d0f171c..aa81f15 100644 --- a/DocGen4/Output/Find.lean +++ b/DocGen4/Output/Find.lean @@ -10,8 +10,8 @@ def find : BaseHtmlM Html := do pure - - + + diff --git a/DocGen4/Output/FoundationalTypes.lean b/DocGen4/Output/FoundationalTypes.lean index 7ece5c7..2297570 100644 --- a/DocGen4/Output/FoundationalTypes.lean +++ b/DocGen4/Output/FoundationalTypes.lean @@ -28,7 +28,7 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat

    Prop is notation for Sort 0.

    {← instancesForToHtml `_builtin_prop} -

    Pi types, {"Π a : α, β a"}

    +

    Pi types, {"(a : α) → β a"}

    The type of dependent functions is known as a pi type. Non-dependent functions and implications are a special case.

    Note that these can also be written with the alternative notations:

    @@ -39,13 +39,12 @@ def foundationalTypes : BaseHtmlM Html := templateLiftExtends (baseHtml "Foundat

    Lean also permits ASCII-only spellings of the three variants:

    Note that despite not itself being a function, (→) is available as infix notation for - {"λ α β, α → β"}.

    + {"fun α β, α → β"}.

    -- TODO: instances for pi types diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index 7d27cc3..0afeaf6 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -23,17 +23,17 @@ def ctorToHtml (c : Process.NameInfo) : HtmlM Html := do pure
  • [renderedDoc]
    - {shortName} : [←infoFormatToHtml c.type] + {shortName} : [← infoFormatToHtml c.type]
    • else pure
  • - {shortName} : [←infoFormatToHtml c.type] + {shortName} : [← infoFormatToHtml c.type]
    • def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do let constructorsHtml := - pure #[constructorsHtml] + return #[constructorsHtml] end Output end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 85932cd..f7bf551 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -31,14 +31,14 @@ def argToHtml (arg : Arg) : HtmlM Html := do | BinderInfo.strictImplicit => ("⦃", "⦄", true) | BinderInfo.instImplicit => ("[", "]", true) let mut nodes := #[Html.text s!"{l}{arg.name.toString} : "] - nodes := nodes.append (←infoFormatToHtml arg.type) + nodes := nodes.append (← infoFormatToHtml arg.type) nodes := nodes.push r let inner := [nodes] let html := Html.element "span" false #[("class", "decl_args")] #[inner] if implicit then - pure {html} + return {html} else - pure html + return html /-- Render the structures this structure extends from as HTML so it can be @@ -55,7 +55,7 @@ def structureInfoHeader (s : Process.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 - pure nodes + return nodes /-- Render the general header of a declaration containing its declaration type @@ -66,22 +66,22 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do nodes := nodes.push <| Html.element "span" false #[("class", "decl_kind")] #[doc.getKindDescription] nodes := nodes.push - + -- TODO: HTMLify the name {doc.getName.toString} for arg in doc.getArgs do - nodes := nodes.push (←argToHtml arg) + nodes := nodes.push (← argToHtml arg) match doc with - | DocInfo.structureInfo i => nodes := nodes.append (←structureInfoHeader i) - | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i) + | DocInfo.structureInfo i => nodes := nodes.append (← structureInfoHeader i) + | DocInfo.classInfo i => nodes := nodes.append (← structureInfoHeader i) | _ => nodes := nodes nodes := nodes.push <| Html.element "span" true #[("class", "decl_args")] #[" :"] - nodes := nodes.push
    [←infoFormatToHtml doc.getType]
    - pure
    [nodes]
    + nodes := nodes.push
    [← infoFormatToHtml doc.getType]
    + return
    [nodes]
    /-- The main entry point for rendering a single declaration inside a given module. @@ -100,12 +100,12 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do | none => pure #[] -- extra information like equations and instances let extraInfoHtml ← match doc with - | DocInfo.classInfo i => pure #[←classInstancesToHtml i.name] + | DocInfo.classInfo i => pure #[← classInstancesToHtml i.name] | 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] + | 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 := @@ -115,10 +115,10 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do else #[] let leanInkHtml := - if ←leanInkEnabled? then + if ← leanInkEnabled? then #[
    - ink + ink
    ] else @@ -128,11 +128,11 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
    - source + source
    [leanInkHtml] [attrsHtml] - {←docInfoHeader doc} + {← docInfoHeader doc} [docInfoHtml] [docStringHtml] [extraInfoHtml] @@ -146,7 +146,7 @@ as HTML. def modDocToHtml (mdoc : ModuleDoc) : HtmlM Html := do pure
    - [←docStringToHtml mdoc.doc] + [← docStringToHtml mdoc.doc]
    /-- @@ -168,15 +168,15 @@ 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 + return res.moduleInfo.find! module |>.imports /-- Sort the list of all modules this one is importing, linkify it and return the HTML. -/ def importsHtml (moduleName : Name) : HtmlM (Array Html) := do - let imports := (←getImports moduleName) |>.qsort Name.lt - imports.mapM (λ i => do pure
  • {←moduleToHtmlLink i}
    • ) + let imports := (← getImports moduleName).qsort Name.lt + imports.mapM (fun i => do return
  • {← moduleToHtmlLink i}
    • ) /-- Render the internal nav bar (the thing on the right on all module pages). @@ -185,12 +185,12 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do pure