Heading support

src/SSG/Djot/Block.idr

@@ -5,6 +5,7 @@ import SSG.Djot.Inline
 import SSG.Djot.Lines
 
 import Control.Eff
+import Data.Nat
 import Data.Maybe
 import Data.String
 import Derive.Prelude
@@ -20,23 +21,31 @@ import System
 %hide Generics.Derive.Show
 %hide Generics.Derive.Eq
 
---* Data Structures *
+--******************************
+--*       Data Structures      *
+--******************************
 
 ||| Types of block level element
 public export
 data BlockType : Type where
   TParagraph : BlockType
+  THeading : BlockType
 
 %runElab derive "BlockType" [Generic, Show, Eq, DecEq]
 
 ||| A block element
 public export
 data Block : BlockType -> Type where
-  Paragraph : (content : List (Inline)) -> Block TParagraph
+  Paragraph : (content : List Inline) -> Block TParagraph
+  Heading : (level : Nat) -> (content : List Inline)
+    -> {auto non_zero : IsSucc level} -> {auto in_range : level `LTE` 6}
+    -> Block THeading
 
 %runElab derive "Block" [Show, Eq]
 
---* Parsing Utilities *
+--******************************
+--*      Parsing Utilities     *
+--******************************
 
 ||| Type alias for block parsing
 BParser : Type -> Type
@@ -79,19 +88,78 @@ runBParser : (input : String) -> BParser t -> Maybe t
 runBParser input x =
   map fst . extract . runFail . runLines input $ x
 
---* Syntax *
+||| Returns true if a character is horizontal whitespace
+isHoriz : Char -> Bool
+isHoriz ' ' = True
+isHoriz '\t' = True
+isHoriz _ = False
+
+--******************************
+--*           Syntax           *
+--******************************
 
 -- Forward declare for mutual recursion
 ||| Top level block parser
 pBlock : BParser (t : BlockType ** Block t)
 
+-- Paragraph
+
 paragraph : BParser (Block TParagraph)
 paragraph = do
   contents <- map (inline . joinBy "\n") $ slurp blankLine
   pure $ Paragraph contents
 
+-- Heading
+
+record HeadingLevel where
+  constructor MkHL
+  level : Nat
+  {auto non_zero : IsSucc level}
+  {auto in_range : level `LTE` 6}
+
+acceptHeadingPrefix : String -> Maybe (HeadingLevel, String)
+acceptHeadingPrefix str =
+  let (level, str) = acceptHeadingPrefix' 0 str
+  in case isItSucc level of
+    Yes non_zero =>
+      case level `isLTE` 6 of
+        Yes in_range => Just $ (MkHL level, str)
+        No _ => Nothing
+    No _ => Nothing
+  where
+    acceptHeadingPrefix' : (acc : Nat) -> String -> (Nat, String)
+    acceptHeadingPrefix' acc str with (asList str)
+      acceptHeadingPrefix' acc "" | [] = (acc, "")
+      acceptHeadingPrefix' acc (strCons '#' str) | ('#' :: x) =
+        acceptHeadingPrefix' (S acc) str | x
+      acceptHeadingPrefix' acc (strCons c str) | (c :: x) =
+        if isHoriz c
+          then acceptHeadingPrefix' acc str | x
+          else (acc, strCons c str)
+
+headingFirstLine : BParser (HeadingLevel, String)
+headingFirstLine = do
+  first <- take >>= fromJust
+  fromJust $ acceptHeadingPrefix first
+
+heading : BParser (Block THeading)
+heading = do
+  (MkHL level {non_zero} {in_range}, first) <- headingFirstLine
+  rest <- slurp blankLine
+  let contents = joinBy "\n" $ first :: map (stripPrefix level) rest
+  pure $ Heading level (inline contents)
+  where
+    stripPrefix : (l : Nat) -> String -> String
+    stripPrefix l str with (asList str)
+      stripPrefix 0 str | _ = str
+      stripPrefix (S k) "" | [] = ""
+      stripPrefix (S k) (strCons '#' str) | ('#' :: x) = stripPrefix k str | x
+      stripPrefix (S k) (strCons c str) | (c :: x) = strCons c str
+
 -- Definition for top level block parser
-pBlock = selectParser paragraph []
+pBlock = selectParser paragraph
+  [ (isJust . acceptHeadingPrefix, heading)
+  ]
 
 
 --******************************
@@ -106,7 +174,9 @@ block input =
     Nothing => (_ ** [])
     Just x => fromList x
 
---* Unit Tests *
+--******************************
+--*         Unit Tests         *
+--******************************
 
 [myshow] Show (t : BlockType ** Block t) where
   show (_ ** block) = show block
@@ -138,3 +208,24 @@ smokeTwoParagraph =
   golden
     "Hello World!\n\nHello Alice!"
     [Paragraph [Text "Hello World!"], Paragraph [Text "Hello Alice!"]]
+
+-- @@test Heading Smoke
+smokeHeading : IO Bool
+smokeHeading =
+  golden
+    "# Level 1 Heading"
+    [Heading 1 [Text "Level 1 Heading"]]
+
+-- @@test Multiline Prefixed Heading Smoke
+smokeHeadingMultilinePrefixed : IO Bool
+smokeHeadingMultilinePrefixed =
+  golden
+    "# Level 1\n# Heading"
+    [Heading 1 [Text "Level 1", SoftLineBreak, Text "Heading"]]
+
+-- @@test Multiline Nonprefixed Heading Smoke
+smokeHeadingMultilineNonprefixed : IO Bool
+smokeHeadingMultilineNonprefixed =
+  golden
+    "# Level 1\nHeading"
+    [Heading 1 [Text "Level 1", SoftLineBreak, Text "Heading"]]

src/SSG/Djot/Lines.idr

@@ -57,6 +57,13 @@ slurp predicate = do
         | _ => pure []
       map (x ::) (slurp predicate)
 
+||| Pop the next line and ignore its value
+export
+drop : Has Lines fs => Eff fs ()
+drop = do
+  _ <- take
+  pure ()
+
 --************************
 --*    Effect Handlers   *
 --************************

src/SSG/Djot/Render.idr

@@ -6,6 +6,7 @@ import SSG.Djot.Inline
 import SSG.Djot.Block
 
 import Data.List
+import Data.Nat
 
 ||| Render a single inline element as HTML
 export
@@ -30,6 +31,20 @@ renderBlocks : {types: _} -> DList _ Block types -> (types' ** DList _ Html type
 
 renderBlock (Paragraph content) =
   (_ ** Normal "p" []  (snd (renderInlines content)))
+renderBlock (Heading 1 content {non_zero = ItIsSucc} {in_range}) =
+  (_ ** Normal "h1" [] (snd (renderInlines content)))
+renderBlock (Heading 2 content {non_zero = ItIsSucc} {in_range}) =
+  (_ ** Normal "h2" [] (snd (renderInlines content)))
+renderBlock (Heading 3 content {non_zero = ItIsSucc} {in_range}) =
+  (_ ** Normal "h3" [] (snd (renderInlines content)))
+renderBlock (Heading 4 content {non_zero = ItIsSucc} {in_range}) =
+  (_ ** Normal "h4" [] (snd (renderInlines content)))
+renderBlock (Heading 5 content {non_zero = ItIsSucc} {in_range}) =
+  (_ ** Normal "h5" [] (snd (renderInlines content)))
+renderBlock (Heading 6 content {non_zero = ItIsSucc} {in_range}) =
+  (_ ** Normal "h6" [] (snd (renderInlines content)))
+renderBlock (Heading (6 + (S n)) content {non_zero = ItIsSucc} {in_range}) =
+  absurd in_range
 
 renderBlocks xs = dMap' (\_, x => renderBlock x) xs