Basic html representation

2025-02-18 22:34:14 -05:00 · 2025-02-18 22:34:14 -05:00 · 33a4ad6dc8
commit 33a4ad6dc8
parent 544a526f54
4 changed files with 176 additions and 1 deletions
--- 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
--- 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
--- a/src/SSG/HTML/ElementTypes.idr
+++ 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"
--- a/todo.org
+++ 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=