/-
Copyright (c) 2022 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving, Xubai Wang
-/
import DocGen4.Output.Base
import DocGen4.Output.ToHtmlFormat
import Lean.Data.Json
import LeanInk.Annotation.Alectryon
namespace LeanInk.Annotation.Alectryon
open DocGen4 Output
open scoped DocGen4.Jsx
structure AlectryonContext where
counter : Nat
abbrev AlectryonT := StateT AlectryonContext
abbrev AlectryonM := AlectryonT HtmlM
def getNextButtonLabel : AlectryonM String := do
let val ← get
let newCounter := val.counter + 1
set { val with counter := newCounter }
return s!"plain-lean4-lean-chk{val.counter}"
def TypeInfo.toHtml (tyi : TypeInfo) : AlectryonM Html := do
pure
def Token.processSemantic (t : Token) : Html :=
match t.semanticType with
| some "Name.Attribute" => {t.raw}
| some "Name.Variable" => {t.raw}
| some "Keyword" => {t.raw}
| _ => Html.text t.raw
def Token.toHtml (t : Token) : AlectryonM Html := do
-- Right now t.link is always none from LeanInk, ignore it
-- TODO: render docstring
let mut parts := #[]
if let some tyi := t.typeinfo then
parts := parts.push <| ← tyi.toHtml
parts := parts.push t.processSemantic
pure
-- TODO: Show rest of token
[parts]
def Contents.toHtml : Contents → AlectryonM Html
| .string value =>
pure
{value}
| .experimentalTokens values => do
let values ← values.mapM Token.toHtml
pure
[values]
def Hypothesis.toHtml (h : Hypothesis) : AlectryonM Html := do
let mut hypParts := #[[h.names.intersperse ", " |>.map Html.text |>.toArray]]
if h.body.snd != "" then
hypParts := hypParts.push
:= [← infoFormatToHtml h.body.fst]
hypParts := hypParts.push
: [← infoFormatToHtml h.type.fst]
pure
[hypParts]
def Goal.toHtml (g : Goal) : AlectryonM Html := do
let mut hypotheses := #[]
for hyp in g.hypotheses do
let rendered ← hyp.toHtml
hypotheses := hypotheses.push rendered
hypotheses := hypotheses.push
let conclusionHtml ←
match g.conclusion with
| .typed info _ => infoFormatToHtml info
| .untyped str => pure #[Html.text str]
pure
[hypotheses]
{g.name}
[conclusionHtml]
def Message.toHtml (m : Message) : AlectryonM Html := do
pure
-- TODO: This might have to be done in a fancier way
{m.contents}
def Sentence.toHtml (s : Sentence) : AlectryonM Html := do
let messages :=
if s.messages.size > 0 then
#[
[← s.messages.mapM Message.toHtml]
]
else
#[]
let goals :=
if s.goals.size > 0 then
-- TODO: Alectryon has a "alectryon-extra-goals" here, implement it
#[
[← s.goals.mapM Goal.toHtml]
]
else
#[]
let buttonLabel ← getNextButtonLabel
pure
[messages]
[goals]
def Text.toHtml (t : Text) : AlectryonM Html := t.contents.toHtml
def Fragment.toHtml : Fragment → AlectryonM Html
| .text value => value.toHtml
| .sentence value => value.toHtml
def baseHtml (content : Array Html) : AlectryonM Html := do
let banner :=
Built with doc-gen4, running Lean4.
Bubbles () indicate interactive fragments: hover for details, tap to reveal contents.
Use Ctrl+↑Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
On Mac, use Cmd instead of Ctrl.
pure
{banner}
[content]
def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List Fragment) := do
let config ← read
annotateFileWithCompounds [] config.inputFileContents as
-- TODO: rework monad mess
def renderAnnotations (as : List Annotation.Annotation) : HtmlT AnalysisM Html := do
let fs ← annotationsToFragments as
let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 }
return html
end LeanInk.Annotation.Alectryon