From 33a4ad6dc8a290c747d7f2b4d2c5a9a43a429f55 Mon Sep 17 00:00:00 2001
From: Nathan McCarty <thatonelutenist@stranger.systems>
Date: Tue, 18 Feb 2025 22:34:14 -0500
Subject: [PATCH] Basic html representation
---
SSG.ipkg | 4 +-
src/SSG/HTML.idr | 70 +++++++++++++++++++++++++
src/SSG/HTML/ElementTypes.idr | 98 +++++++++++++++++++++++++++++++++++
todo.org | 5 ++
4 files changed, 176 insertions(+), 1 deletion(-)
create mode 100644 src/SSG/HTML/ElementTypes.idr
create mode 100644 todo.org
diff --git a/SSG.ipkg b/SSG.ipkg
index 3e8c0b2..0033da9 100644
--- a/SSG.ipkg
+++ b/SSG.ipkg
@@ -13,12 +13,14 @@ authors = "Nathan McCarty"
-- langversion
-- packages to add to search path
-depends = eff
+depends = structures
+ , eff
-- modules to install
modules = SSG.Parser.Core
, SSG.Parser.Markdown
, SSG.HTML
+ , SSG.HTML.ElementTypes
-- main file (i.e. file to load at REPL)
main = Main
diff --git a/src/SSG/HTML.idr b/src/SSG/HTML.idr
index 7ca024f..17f3322 100644
--- a/src/SSG/HTML.idr
+++ b/src/SSG/HTML.idr
@@ -1 +1,71 @@
module SSG.HTML
+
+import public SSG.HTML.ElementTypes
+
+import Data.String
+
+import Structures.Dependent.DList
+
+export infix 8 =$
+
+public export
+data Attribute : Type where
+ -- TODO: Add some structure here, maybe make `=$` a smart constructor
+ (=$) : (attribute, value : String) -> Attribute
+
+namespace Attribute
+ export
+ toString : Attribute -> String
+ toString (attribute =$ value) =
+ let value_cs = unpack value
+ in if any (== '\'') value_cs
+ then "\"\{value}\""
+ else if any (== '"') value_cs || any (== ' ') value_cs
+ then "'\{value}'"
+ else value
+
+public export
+data Tag : String -> Type where
+ -- TODO: Find a way to move this out of tag
+ ||| Raw text, represented as a tag for compatibility
+ Raw : (content : String)
+ -> Tag ""
+ ||| A void type tag, has attributes, no contents
+ Void : (type : String) -> {auto void_prf : IsVoid type}
+ -> (attributes : List Attribute)
+ -> Tag type
+ ||| A normal type tag, has attributes, and contents
+ Normal : (type : String) -> {auto normal_prf : IsNormal type}
+ -> (attributes : List Attribute)
+ -- TODO: Erase content_types
+ -> {content_types : _} -> (contents : DList _ Tag content_types)
+ -> Tag type
+ ||| A raw text or an escapable raw text element
+ RawText : (type : String)
+ -> {auto raw_prf : Either (IsRawText type) (IsEscapableRawText type)}
+ -> (attributes : List Attribute)
+ -> (content : String)
+ -> Tag type
+
+namespace Tag
+ viewIndented : (indent_level : Nat) -> Tag type -> String
+ viewIndented indent_level (Raw content) =
+ replicate (indent_level * 2) ' ' ++ content
+ viewIndented indent_level (Void type attributes) =
+ let indent = replicate (indent_level * 2) ' '
+ in if length attributes > 0
+ then
+ let attrs = joinBy " " $ map toString attributes
+ in "<\{type} \{attrs} />"
+ else "<\{type} />"
+ viewIndented indent_level (Normal type attributes contents) =
+ ?viewIndented_rhs_2
+ viewIndented indent_level (RawText type attributes content) =
+ ?viewIndented_rhs_3
+
+ view : Tag type -> String
+ view = viewIndented 0
+
+ render : Tag "html" -> String
+ render x =
+ "<!DOCTYPE HTML>\n" ++ viewIndented 0 x
diff --git a/src/SSG/HTML/ElementTypes.idr b/src/SSG/HTML/ElementTypes.idr
new file mode 100644
index 0000000..e767ea5
--- /dev/null
+++ b/src/SSG/HTML/ElementTypes.idr
@@ -0,0 +1,98 @@
+module SSG.HTML.ElementTypes
+
+||| Proof that the element type identified by the given string is a void element
+public export
+data IsVoid : String -> Type where
+ IsArea : IsVoid "area"
+ IsBase : IsVoid "base"
+ IsBr : IsVoid "br"
+ IsCol : IsVoid "col"
+ IsImg : IsVoid "img"
+ IsInput : IsVoid "input"
+ IsLink : IsVoid "link"
+ IsMeta : IsVoid "meta"
+ IsParam : IsVoid "param"
+ IsSource : IsVoid "source"
+ IsTrack : IsVoid "track"
+ IsWbr : IsVoid "wbr"
+
+||| Proof that the element type identified by the given string is a raw text
+||| element
+public export
+data IsRawText : String -> Type where
+ IsScript : IsRawText "script"
+ IsStyle : IsRawText "style"
+||| Proof that the element type identified by the given string is an escapable
+||| raw text element
+public export
+data IsEscapableRawText : String -> Type where
+ IsTextarea : IsEscapableRawText "textarea"
+ IsTitle : IsEscapableRawText "title"
+
+||| Proof that the element type idenitified by the given string is a normal
+||| element
+public export
+data IsNormal : String -> Type where
+ -- Document element
+ IsHtml : IsNormal "html"
+ -- Sections
+ IsBody : IsNormal "body"
+ IsArticle : IsNormal "article"
+ IsSection : IsNormal "section"
+ IsNav : IsNormal "nav"
+ IsAside : IsNormal "aside"
+ IsH1 : IsNormal "h1"
+ IsH2 : IsNormal "h2"
+ IsH3 : IsNormal "h3"
+ IsH4 : IsNormal "h4"
+ IsH5 : IsNormal "h5"
+ IsH6 : IsNormal "h6"
+ IsHgroup : IsNormal "hgroup"
+ IsHeader : IsNormal "header"
+ IsFooter : IsNormal "footer"
+ IsAddress : IsNormal "address"
+ -- Grouping content
+ IsP : IsNormal "p"
+ IsHr : IsNormal "hr"
+ IsPre : IsNormal "pre"
+ IsBlockquote : IsNormal "blockquote"
+ IsOl : IsNormal "ol"
+ IsUl : IsNormal "ul"
+ IsMenu : IsNormal "menu"
+ IsLi : IsNormal "li"
+ IsDl : IsNormal "dl"
+ IsDt : IsNormal "dt"
+ IsDd : IsNormal "dd"
+ IsFigure : IsNormal "figure"
+ IsFigcaption : IsNormal "figcaption"
+ IsMain : IsNormal "main"
+ IsSearch : IsNormal "search"
+ IsDiv : IsNormal "div"
+ -- Text level semantics
+ IsA : IsNormal "a"
+ IsEm : IsNormal "em"
+ IsStrong : IsNormal "strong"
+ IsSmall : IsNormal "small"
+ IsS : IsNormal "s"
+ IsCite : IsNormal "cite"
+ IsQ : IsNormal "q"
+ IsDfn : IsNormal "dfn"
+ IsAbbr : IsNormal "abbr"
+ IsRuby : IsNormal "ruby"
+ IsRt : IsNormal "rt"
+ IsRp : IsNormal "rp"
+ IsData : IsNormal "data"
+ IsTime : IsNormal "time"
+ IsCode : IsNormal "code"
+ IsVar : IsNormal "var"
+ IsSamp : IsNormal "samp"
+ IsKbd : IsNormal "kbd"
+ IsSub : IsNormal "sub"
+ IsSup : IsNormal "sup"
+ IsI : IsNormal "i"
+ IsB : IsNormal "b"
+ IsU : IsNormal "u"
+ IsMark : IsNormal "mark"
+ IsBdi : IsNormal "bdi"
+ IsBdo : IsNormal "bdo"
+ IsSpan : IsNormal "span"
diff --git a/todo.org b/todo.org
new file mode 100644
index 0000000..f9056b9
--- /dev/null
+++ b/todo.org
@@ -0,0 +1,5 @@
+* HTML Handling
+** TODO Special handling for =pre= in =view=
+** TODO Smart spec compliance for =attribute=
+Probably want to refine the attribute and value strings, and be smarter about how we choose to quote the value string.
+** TODO Move =Raw= out of =Tag=