From 5bae061b544f25d89655330e954eeb351fbbc9cf Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Wed, 27 Jul 2022 20:11:41 +0200
Subject: [PATCH] fix: mess of monad transformers in LeanInk adapter

---
 DocGen4/LeanInk/Output.lean  | 2 +-
 DocGen4/LeanInk/Process.lean | 8 ++++----
 DocGen4/Output/Base.lean     | 6 ++++++
 3 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/DocGen4/LeanInk/Output.lean b/DocGen4/LeanInk/Output.lean
index 5c719b1..60f7a86 100644
--- a/DocGen4/LeanInk/Output.lean
+++ b/DocGen4/LeanInk/Output.lean
@@ -209,7 +209,7 @@ def annotationsToFragments (as : List Annotation.Annotation) : AnalysisM (List F
 -- 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 } |>.run (←readThe SiteContext) (←readThe SiteBaseContext)
+  let (html, _) ← fs.mapM Fragment.toHtml >>= (baseHtml ∘ List.toArray) |>.run { counter := 0 }
   pure html
 
 end LeanInk.Annotation.Alectryon
diff --git a/DocGen4/LeanInk/Process.lean b/DocGen4/LeanInk/Process.lean
index 8c327e8..dcd31aa 100644
--- a/DocGen4/LeanInk/Process.lean
+++ b/DocGen4/LeanInk/Process.lean
@@ -13,10 +13,10 @@ namespace DocGen4.Process.LeanInk
 
 open Lean
 open DocGen4.Output
--- TODO: rework monad mess
+
 def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do
-  let some modName := getCurrentName |>.run (←readThe SiteBaseContext) | unreachable!
-  let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as |>.run (←readThe SiteContext) (←readThe SiteBaseContext)
+  let some modName ← getCurrentName | unreachable!
+  let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as
   let srcDir := moduleNameToDirectory srcBasePath modName
   let srcPath := moduleNameToFile srcBasePath modName
   IO.FS.createDirAll srcDir
@@ -26,7 +26,7 @@ def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.Analy
 def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
   let ctx ← readThe SiteContext
   let baseCtx ← readThe SiteBaseContext
-  let outputFn := (λ as => docGenOutput as |>.run ctx baseCtx)
+  let outputFn := (docGenOutput · |>.run ctx baseCtx)
   return ← LeanInk.Analysis.runAnalysis { 
     name := "doc-gen4"
     genOutput := outputFn
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index c2292d1..331fe58 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -66,6 +66,12 @@ def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) :
 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)
+
+instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
+  monadLift x := do pure <| x.run (←readThe SiteBaseContext)
+
 /--
 Obtains the root URL as a relative one to the current depth.
 -/