From e9a9e17439f92c974bd9688ba99a1ba2a18bbb77 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Fri, 10 Dec 2021 15:24:38 +0100
Subject: [PATCH] feat: Basic Html to String converter

It works okay-ish for basic HTML which should be good enough for now
---
 DocGen4/ToHtmlFormat.lean | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean
index 778edf7..2b617d2 100644
--- a/DocGen4/ToHtmlFormat.lean
+++ b/DocGen4/ToHtmlFormat.lean
@@ -26,6 +26,27 @@ inductive Html where
 instance : Coe String Html :=
   ⟨Html.text⟩
 
+namespace Html
+
+def attributesToString (attrs : Array (String × String)) :String :=
+  attrs.foldl (λ acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ v ++ "\"") ""
+
+-- TODO: Termination proof
+partial def toStringAux : Html → String
+| element tag attrs #[] => s!"<{tag}{attributesToString attrs}/>\n"
+| element tag attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
+| element tag attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
+| element tag attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"
+| text s => s
+
+def toString (html : Html) : String :=
+  html.toStringAux.trimRight
+
+instance : ToString Html :=
+  ⟨toString⟩
+
+end Html
+
 namespace Jsx
 open Parser PrettyPrinter