HTML.Generate

module HTML.Generate where

open import Agda.Builtin.List using ([]; _∷_)
open import Agda.Builtin.Nat using (zero; suc)
open import Agda.Builtin.Reflection
  using (TC; Term; bindTC; quoteTC; returnTC; strErr; typeError; unify)
open import Agda.Builtin.Reflection.External using (execTC)
open import Agda.Builtin.Sigma using (_,_)
open import Agda.Builtin.String using (String; primStringAppend)
open import Agda.Builtin.Unit using (⊤; tt)
open import Agda.Primitive using () renaming (Set to Type)

open import FF.HTML.Render using (render)
open import FF.HTML.Spec.Safe using (HtmlT; renderer)
open import HTML.Showcase

infixr 5 _++_
infixl 1 _>>=_

_++_ : String -> String -> String
_++_ = primStringAppend

_>>=_ : ∀ {A B : Type} -> TC A -> (A -> TC B) -> TC B
_>>=_ = bindTC

nodeExecutable : String
nodeExecutable = "node"

writerScript : String
writerScript = "/Users/marcin/agdaLibs/ff-html/scripts/write-html.js"

dashboardOutput : String
dashboardOutput = "/Users/marcin/agdaLibs/ff-html/generated/safe-dashboard.html"

componentGalleryOutput : String
componentGalleryOutput = "/Users/marcin/agdaLibs/ff-html/generated/component-gallery.html"

introOutput : String
introOutput = "/Users/marcin/agdaLibs/ff-html/generated/01-intro.html"

semanticArticleOutput : String
semanticArticleOutput = "/Users/marcin/agdaLibs/ff-html/generated/02-semantic-article.html"

selectorStyleSheetOutput : String
selectorStyleSheetOutput = "/Users/marcin/agdaLibs/ff-html/generated/03-selector-stylesheet.html"

renderDocument : HtmlT -> String
renderDocument html = "<!doctype html>\n" ++ render renderer html

writeError : String -> String -> String -> String -> String
writeError outputPath stdout stderr html =
  "failed to write rendered HTML\n\n"
  ++ "Path:\n"
  ++ outputPath
  ++ "\n\nStdout:\n"
  ++ stdout
  ++ "\n\nStderr:\n"
  ++ stderr
  ++ "\n\nRendered input:\n"
  ++ html

writeHtmlFileTC : String -> HtmlT -> TC ⊤
writeHtmlFileTC outputPath html =
  let rendered = renderDocument html in
  execTC nodeExecutable (writerScript ∷ outputPath ∷ []) rendered >>= λ where
    (zero , _) -> returnTC tt
    (suc _ , (stdout , stderr)) ->
      typeError (strErr (writeError outputPath stdout stderr rendered) ∷ [])

macro
  writeHtmlFile : String -> HtmlT -> Term -> TC ⊤
  writeHtmlFile outputPath html hole =
    writeHtmlFileTC outputPath html >>= λ _ ->
    quoteTC tt >>= unify hole

generatedDashboard : ⊤
generatedDashboard =
  writeHtmlFile dashboardOutput dashboardPage

generatedComponentGallery : ⊤
generatedComponentGallery =
  writeHtmlFile componentGalleryOutput componentGalleryPage

generatedIntro : ⊤
generatedIntro =
  writeHtmlFile introOutput introPage

generatedSemanticArticle : ⊤
generatedSemanticArticle =
  writeHtmlFile semanticArticleOutput semanticArticlePage

generatedSelectorStyleSheet : ⊤
generatedSelectorStyleSheet =
  writeHtmlFile selectorStyleSheetOutput selectorStyleSheetPage