Base.lean

/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import DocGen4.Process
import DocGen4.Output.ToHtmlFormat

namespace DocGen4.Output

open scoped DocGen4.Jsx
open Lean System Widget Elab Process

def basePath (buildDir : System.FilePath) := buildDir / "doc"
def srcBasePath (buildDir : System.FilePath) := basePath buildDir / "src"
def declarationsBasePath (buildDir : System.FilePath) := buildDir / "doc-data"

/-- The structure representing a processed bibitem. -/
structure BibItem where
  /-- The cite key as in the bib file. -/
  citekey : String
  /-- The tag generated by bib processor, e.g. `[Doe12]`.
  Should be plain text and should not be escaped. -/
  tag : String
  /-- The HTML generated by bib processor, e.g.
  `John Doe. <i>Test</i>. 2012.`-/
  html : String
  /-- The plain text form of `html` field. Should not be escaped. -/
  plaintext : String
  deriving FromJson, ToJson

/-- The structure representing a backref item. -/
structure BackrefItem where
  /-- The cite key as in the bib file. -/
  citekey : String
  /-- The name of the module. -/
  modName : Name
  /-- The name of the function, as a string. It is empty if the backref is in modstring. -/
  funName : String
  /-- The index of the backref in that module, starting from zero. -/
  index : Nat
  deriving FromJson, ToJson, Inhabited

/--
The context used in the `BaseHtmlM` monad for HTML templating.
-/
structure SiteBaseContext where

  /--
  The build directory (provided by lake).
  -/
  buildDir : System.FilePath

  /--
  The module hierarchy as a tree structure.
  -/
  hierarchy : Hierarchy
  /--
  How far away we are from the page root, used for relative links to the root.
  -/
  depthToRoot: Nat
  /--
  The name of the current module if there is one, there exist a few
  pages that don't have a module name.
  -/
  currentName : Option Name
  /--
  The list of references, as an array.
  -/
  refs : Array BibItem

/--
The read-only context used in the `HtmlM` monad for HTML templating.
-/
structure SiteContext where
  /--
  The full analysis result from the Process module.
  -/
  result : AnalyzerResult
  /--
  A function to link declaration names to their source URLs, usually Github ones.
  -/
  sourceLinker : Name → Option DeclarationRange → String
  /--
  The references as a map.
  -/
  refsMap : Std.HashMap String BibItem

/--
The writable state used in the `HtmlM` monad for HTML templating.
-/
structure SiteState where
  /--
  The list of back references, as an array.
  -/
  backrefs : Array BackrefItem := #[]
  /--
  The errors occurred during the process.
  -/
  errors : String := ""

def setCurrentName (name : Name) (ctx : SiteBaseContext) := {ctx with currentName := some name}

abbrev BaseHtmlT := ReaderT SiteBaseContext
abbrev BaseHtmlM := BaseHtmlT Id

abbrev HtmlT (m) := StateT SiteState <| ReaderT SiteContext <| BaseHtmlT m
abbrev HtmlM := HtmlT Id

def HtmlT.run (x : HtmlT m α) (state : SiteState) (ctx : SiteContext)
    (baseCtx : SiteBaseContext) : m (α × SiteState) :=
  StateT.run x state |>.run ctx |>.run baseCtx

def HtmlM.run (x : HtmlM α) (state : SiteState) (ctx : SiteContext)
    (baseCtx : SiteBaseContext) : α × SiteState :=
  StateT.run x state |>.run ctx |>.run baseCtx |>.run

instance [Monad m] : MonadLift HtmlM (HtmlT m) where
  monadLift x := do return (x.run (← getThe SiteState) (← readThe SiteContext) (← readThe SiteBaseContext)).1

instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
  monadLift x := do return x.run (← readThe SiteBaseContext)

/-- Add a backref of the given `citekey` and `funName` to current document, and returns it. -/
def addBackref (citekey funName : String) : HtmlM BackrefItem := do
  let newBackref : BackrefItem := {
    citekey := citekey
    modName := (← readThe SiteBaseContext).currentName.get!
    funName := funName
    index := (← get).backrefs.size
  }
  modify fun cfg => { cfg with backrefs := cfg.backrefs.push newBackref }
  pure newBackref

/-- Add an error message to errors of current document. -/
def addError (err : String) : HtmlM Unit := do
  modify fun cfg => { cfg with errors := cfg.errors ++ err ++ "\n" }

/--
Obtains the root URL as a relative one to the current depth.
-/
def getRoot : BaseHtmlM String := do
  let rec go: Nat -> String
  | 0 => "./"
  | Nat.succ n' => "../" ++ go n'
  let d <- SiteBaseContext.depthToRoot <$> read
  return (go d)

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

/--
If a template is meant to be extended because it for example only provides the
header but no real content this is the way to fill the template with content.
This is untyped so HtmlM and BaseHtmlM can be mixed.
-/
def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m β :=
  new >>= base

def templateLiftExtends {α β} {m n} [Bind m] [MonadLiftT n m] (base : α → n β) (new : m α) : m β :=
  new >>= (monadLift ∘ base)
/--
Returns the doc-gen4 link to a module name.
-/
def moduleNameToLink (n : Name) : BaseHtmlM String := do
  let parts := n.components.map Name.toString
  return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"

/--
Returns the HTML doc-gen4 link to a module name.
-/
def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
  return <a href={← moduleNameToLink module}>{module.toString}</a>

/--
Returns the path to the HTML file that contains information about a module.
-/
def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
  let parts := n.components.map Name.toString
  FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"

/--
Returns the directory of the HTML file that contains information about a module.
-/
def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
  let parts := n.components.dropLast.map Name.toString
  basePath / parts.foldl (· / ·) (FilePath.mk ".")

section Static
/-!
The following section contains all the statically included files that
are used in documentation generation, notably JS and CSS ones.
-/
  def styleCss : String := include_str "../../static/style.css"
  def faviconSvg : String := include_str "../../static/favicon.svg"
  def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
  def colorSchemeJs : String := include_str "../../static/color-scheme.js"
  def jumpSrcJs : String := include_str "../../static/jump-src.js"
  def navJs : String := include_str "../../static/nav.js"
  def expandNavJs : String := include_str "../../static/expand-nav.js"
  def howAboutJs : String := include_str "../../static/how-about.js"
  def searchJs : String := include_str "../../static/search.js"
  def instancesJs : String := include_str "../../static/instances.js"
  def importedByJs : String := include_str "../../static/importedBy.js"
  def findJs : String := include_str "../../static/find/find.js"
  def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"

end Static

/--
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[name]!.toNat]!
  return (← moduleNameToLink module) ++ "#" ++ name.toString

/--
Returns the HTML doc-gen4 link to a declaration name.
-/
def declNameToHtmlLink (name : Name) : HtmlM Html := do
  return <a href={← declNameToLink name}>{name.toString}</a>

/--
Returns a name splitted into parts.
Together with "break_within" CSS class this helps browser to break a name
nicely.
-/
def breakWithin (name: String) : (Array Html) :=
  name.splitOn "."
    |> .map (fun (s: String) => <span class="name">{s}</span>)
    |> .intersperse "."
    |> List.toArray

/--
Returns the HTML doc-gen4 link to a declaration name with "break_within"
set as class.
-/
def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
  return <a class="break_within" href={← declNameToLink name}>
      [breakWithin name.toString]
    </a>

/--
In Lean syntax declarations the following pattern is quite common:
```
syntax term " + " term : term
```
that is, we place spaces around the operator in the middle. When the
`InfoTree` framework provides us with information about what source token
corresponds to which identifier it will thus say that `" + "` corresponds to
`HAdd.hadd`. This is however not the way we want this to be linked, in the HTML
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 mut length := s.length
  let mut s := s.trimLeft
  let front := "".pushn ' ' (length - s.length)
  length := s.length
  s := s.trimRight
  let back := "".pushn ' ' (length - s.length)
  (front, s, back)

/--
Turns a `CodeWithInfos` object, that is basically a Lean syntax tree with
information about what the identifiers mean, into an HTML object that links
to as much information as possible.
-/
partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
  match i with
  | .text t => return #[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 =>
      let cleanExpr :=  i.expr.consumeMData
      match cleanExpr with
      | .const name _ =>
        -- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
        -- find a better solution
        if (← getResult).name2ModIdx.contains name then
          match t with
          | .text t =>
            let (front, t, back) := splitWhitespaces t
            let elem := <a href={← declNameToLink name}>{t}</a>
            return #[Html.text front, elem, Html.text back]
          | _ =>
            return #[<a href={← declNameToLink name}>[← infoFormatToHtml t]</a>]
        else
         return #[<span class="fn">[← infoFormatToHtml t]</span>]
      | .sort _ =>
        match t with
        | .text t =>
          let sortPrefix :: rest := t.splitOn " " | unreachable!
          let sortLink := <a href={s!"{← getRoot}foundational_types.html"}>{sortPrefix}</a>
          let mut restStr := String.intercalate " " rest
          if restStr.length != 0 then
            restStr := " " ++ restStr
          return #[sortLink, Html.text restStr]
        | _ =>
          return #[<a href={s!"{← getRoot}foundational_types.html"}>[← infoFormatToHtml t]</a>]
      | _ =>
         return #[<span class="fn">[← infoFormatToHtml t]</span>]
    | _ => return #[<span class="fn">[← infoFormatToHtml t]</span>]

def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
  return #[
    <meta charset="UTF-8"/>,
    <meta name="viewport" content="width=device-width, initial-scale=1"/>,
    <link rel="stylesheet" href={s!"{← getRoot}style.css"}/>,
    <link rel="icon" href={s!"{← getRoot}favicon.svg"}/>,
    <link rel="mask-icon" href={s!"{← getRoot}favicon.svg"} color="#000000"/>,
    <link rel="prefetch" href={s!"{← getRoot}/declarations/declaration-data.bmp"} as="image"/>
  ]

end DocGen4.Output