Heading support

.gitignore

@@ -1,2 +1,4 @@
 build/
 *.*~
+test/failures
+test/*/*/output

SSG.ipkg

@@ -13,14 +13,23 @@ authors = "Nathan McCarty"
 -- langversion
 
 -- packages to add to search path
-depends = structures
+depends = contrib
+        , structures
+        , tailrec
         , eff
+        , elab-util
+        , elab-pretty
+        , sop
+        , prettier
 
 -- modules to install
-modules = SSG.Parser.Core
-        , SSG.Parser.Markdown
-        , SSG.HTML
+modules = SSG.HTML
         , SSG.HTML.ElementTypes
+        , SSG.Djot
+        , SSG.Djot.Lines
+        , SSG.Djot.Block
+        , SSG.Djot.Inline
+        , SSG.Djot.Render
 
 -- main file (i.e. file to load at REPL)
 main = Main

examples/src/HelloWorld.idr

@@ -5,15 +5,15 @@ import SSG.HTML
 import Structures.Dependent.DList
 
 helloWorld : Html "html"
-helloWorld =
-  tag "html" ["lang" =$ "en"] [
-    tag "head" [] [
-      tag "title" [] "Example"
-    ],
-    tag "body" [] [
-      tag "p" [] [Text "Hello World!"]
-    ]
-  ]
+-- helloWorld =
+--   tag "html" ["lang" =$ "en"] [] [
+--     tag "head" [] [
+--       tag "title" [] "Example"
+--     ],
+--     tag "body" [] [
+--       tag "p" [] [Text "Hello World!"]
+--     ]
+--   ]
 
 main : IO ()
 main = putStr $ render helloWorld

pack.toml

@@ -4,6 +4,11 @@ path = "."
 ipkg = "SSG.ipkg"
 test = "test/test.ipkg"
 
+[custom.all.Djot]
+type = "local"
+path = "."
+ipkg = "Djot.ipkg"
+
 [custom.all.SSG-test]
 type = "local"
 path = "test"

src/SSG/Djot.idr

@@ -0,0 +1,5 @@
+module SSG.Djot
+
+import public SSG.Djot.Inline
+import public SSG.Djot.Block
+import public SSG.Djot.Render

src/SSG/Djot/Block.idr

@@ -0,0 +1,231 @@
+||| DJot Block formatting parser
+module SSG.Djot.Block
+
+import SSG.Djot.Inline
+import SSG.Djot.Lines
+
+import Control.Eff
+import Data.Nat
+import Data.Maybe
+import Data.String
+import Derive.Prelude
+import Derive.Pretty
+import Generics.Derive
+import Structures.Dependent.DList
+
+-- Just for iutils unit tests
+import System
+
+%language ElabReflection
+%hide Generics.SOP.values
+%hide Generics.Derive.Show
+%hide Generics.Derive.Eq
+
+--******************************
+--*       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
+  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     *
+--******************************
+
+||| Type alias for block parsing
+BParser : Type -> Type
+BParser t = Eff [Lines, Fail] t
+
+-- FIXME: Proper whitespace handling
+||| Detect if a line is blank
+blankLine : String -> Bool
+blankLine = null . trim
+
+||| Select and apply the first matching parser from a list, with a fallback parser
+selectParser :
+  {fallback_type : BlockType} -> {values : _}
+  -> (fallback : BParser (Block fallback_type))
+  -> DList BlockType (\t => (String -> Bool, BParser (Block t))) values
+  -> BParser (t : BlockType ** Block t)
+selectParser fallback [] = do
+  x <- fallback
+  pure (_ ** x)
+selectParser fallback ((pred, parser) :: rest) = do
+  Just line <- peek
+    | _ => fail
+  if pred line
+    then do
+      x <- parser
+      pure (_ ** x)
+    else selectParser fallback rest
+
+||| Repeat a parser until failure or if we are out of lines
+repeat : BParser t -> BParser (List t)
+repeat x = do
+  Just _ <- peek
+    | _ => pure []
+  Just res <- lift . runFail $ x
+    | _ => pure []
+  map (res ::) (repeat x)
+
+||| Run a parser
+runBParser : (input : String) -> BParser t -> Maybe t
+runBParser input x =
+  map fst . extract . runFail . runLines input $ x
+
+||| 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
+  [ (isJust . acceptHeadingPrefix, heading)
+  ]
+
+
+--******************************
+--* Top Level Parsing Function *
+--******************************
+
+||| Parse a string as a sequences of blocks
+export
+block : (input : String) -> (values ** DList BlockType Block values)
+block input =
+  case runBParser input (repeat pBlock) of
+    Nothing => (_ ** [])
+    Just x => fromList x
+
+--******************************
+--*         Unit Tests         *
+--******************************
+
+[myshow] Show (t : BlockType ** Block t) where
+  show (_ ** block) = show block
+
+{values : _} -> Show (DList BlockType Block values) where
+  show xs =
+    let xs = map (show @{myshow}) $ toList xs
+    in "[\{joinBy ", " xs}]"
+
+golden : {values : _}
+  -> (input : String) -> (ref : DList BlockType Block values) -> IO Bool
+golden input ref = do
+  putStrLn "Input: \{show input}"
+  putStrLn "Reference:\n  \{show ref}"
+  let (types ** output) = block input
+  putStrLn "Output:\n  \{show output}"
+  pure $ ref $== output
+
+-- @@test Paragraph Smoke
+smokeParagraph : IO Bool
+smokeParagraph =
+  golden
+    "Hello World!"
+    [Paragraph [Text "Hello World!"]]
+
+-- @@test Two Paragraph Smoke
+smokeTwoParagraph : IO Bool
+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/Inline.idr

@@ -0,0 +1,240 @@
+||| Djot inline formatting parser
+module SSG.Djot.Inline
+
+import Control.Eff
+import Data.List1
+import Data.Maybe
+import Data.String
+import Derive.Prelude
+import Derive.Pretty
+
+-- Just for iutils unit tests
+import System
+
+%language ElabReflection
+
+--******************************
+--*       Data Structures      *
+--******************************
+
+||| Types of inline styling
+public export
+data Inline : Type where
+  Text : (text : String) -> Inline
+  SoftLineBreak : Inline
+  HardLineBreak : Inline
+
+%runElab derive "Inline" [Eq, Show, Pretty]
+
+--******************************
+--*      Parsing Utilities     *
+--******************************
+
+||| Type alias for inline parsing
+IParser : Type -> Type
+IParser t = Eff [State (List Char), Fail] t
+
+||| Get the next char, modifiying the state
+popChar : IParser Char
+popChar = do
+  x :: xs <- get
+    | [] => fail
+  put xs
+  pure x
+
+||| Get the next char, without modifying the state
+peekChar : IParser Char
+peekChar = do
+  x :: xs <- get
+    | [] => fail
+  pure x
+
+||| Attempt to parse something without propagating the failure
+try : IParser t -> IParser (Maybe t)
+try x = do
+  state <- get
+  x <- lift . runFail $ x
+  case x of
+    Nothing => do
+      put state
+      pure Nothing
+    Just y => pure $ Just y
+
+
+||| Choose a parser
+oneOf : List (IParser t) -> IParser t
+oneOf [] = fail
+oneOf (x :: xs) = do
+  state <- get
+  x <- lift . runFail $ x
+  case x of
+    Nothing => do
+      put state
+      oneOf xs
+    Just y => pure y
+
+||| Parse 0+ of something
+many : IParser t -> IParser (List t)
+many x = do
+  Just y <- try x
+    | _ => pure []
+  map (y ::) $ many x
+
+||| Parse 1+ of something
+atLeastOne : IParser t -> IParser (List1 t)
+atLeastOne x = do
+  Just y <- try x
+    | _ => fail
+  map (y :::) (many x)
+
+||| Match exactly the given string
+exactly : String -> IParser (List Char)
+exactly str = exactly' (unpack str)
+  where
+    exactly' : List Char -> IParser (List Char)
+    exactly' [] = pure []
+    exactly' (x :: xs) = do
+      y <- popChar
+      if x == y
+        then map (x ::) (exactly' xs)
+        else fail
+
+||| Match vertical whitespace
+vert : IParser (List Char)
+vert = oneOf
+  [ exactly "\n"
+  , exactly "\r\n"
+  , exactly "\r"
+  ]
+
+||| Match horizontal whitespace
+horiz : IParser (List Char)
+horiz = oneOf
+  [ exactly " "
+  , exactly "\t"
+  ]
+
+||| Run a parser
+runIParser : (str : String) -> IParser t -> Maybe t
+runIParser str x = 
+  fst . extract . runState (unpack str) . runFail $ x
+
+--******************************
+--*           Syntax           *
+--******************************
+
+-- Forward declare so we can get mutually recursive
+||| Top level parser function for Inline Content
+pInline : IParser Inline
+
+||| Parse a character as plain text
+text : IParser Inline
+text = do
+  c <- popChar
+  pure $ Text (singleton c)
+
+||| Parse a soft linebreak
+softLineBreak : IParser Inline
+softLineBreak = do
+  _ <- atLeastOne singleBreak
+  pure SoftLineBreak
+  where
+    singleBreak : IParser ()
+    singleBreak = do
+      _ <- many horiz
+      _ <- vert
+      _ <- many horiz
+      pure ()
+
+hardLineBreak : IParser Inline
+hardLineBreak = do
+  _ <- exactly "\\"
+  _ <- many horiz
+  _ <- vert
+  _ <- many horiz
+  pure HardLineBreak
+
+-- Definition of pInline
+pInline = oneOf
+  [ hardLineBreak
+  , softLineBreak
+  , text
+  ]
+
+--******************************
+--*       Post Processing      *
+--******************************
+
+||| Combine adjacent Text entries
+combineTexts : List Inline -> List Inline
+combineTexts [] = []
+combineTexts (Text a :: (Text b :: xs)) =
+  combineTexts (Text (a ++ b) :: xs)
+combineTexts (x :: xs) = x :: combineTexts xs
+
+||| Remove trailing soft line breaks
+removeTrailingSoftbreak : List Inline -> List Inline
+removeTrailingSoftbreak xs = reverse (removeTrailingSoftbreak' (reverse xs))
+  where
+    removeTrailingSoftbreak' : List Inline -> List Inline
+    removeTrailingSoftbreak' (SoftLineBreak :: xs) = removeTrailingSoftbreak' xs
+    removeTrailingSoftbreak' xs = xs
+
+||| Top level post processor
+postProcess : List Inline -> List Inline
+postProcess xs = removeTrailingSoftbreak . combineTexts $ xs
+
+--******************************
+--* Top Level Parsing Function *
+--******************************
+
+||| Parse a string as inline content
+export
+inline : (input : String) -> List Inline
+inline input =
+  postProcess . fromMaybe [] . runIParser input $ many pInline
+
+--******************************
+--*         Unit Tests         *
+--******************************
+
+golden : (input : String) -> (reference : List Inline) -> IO Bool
+golden input reference = do
+  putStrLn "Input: \{show input}"
+  let opts = Opts 78
+  let ref_pretty = Doc.render opts $ pretty reference
+  putStrLn "Reference:\n\{unlines . map ("  " ++) . lines $ ref_pretty}"
+  let output = inline input
+  let out_pretty = Doc.render opts $ pretty output
+  putStrLn "Output:\n\{unlines . map ("  " ++) . lines $ out_pretty}"
+  pure $ reference == output
+
+-- @@test Just text parses as text
+testTextAsText : IO Bool
+testTextAsText =
+  golden "Hello World!" [Text "Hello World!"]
+
+-- @@test Soft line break smoke
+smokeSoftLineBreak : IO Bool
+smokeSoftLineBreak =
+  golden "Hello\nWorld!" [Text "Hello", SoftLineBreak, Text "World!"]
+
+-- @@test Soft line break double line break
+testDoubleSoftLineBreak : IO Bool
+testDoubleSoftLineBreak =
+  golden "Hello\n\nWorld!" [Text "Hello", SoftLineBreak, Text "World!"]
+
+-- @@test Soft line break trailing line break
+testTrailingSoftLineBreak : IO Bool
+testTrailingSoftLineBreak =
+  golden "Hello\n\nWorld!\n" [Text "Hello", SoftLineBreak, Text "World!"]
+
+-- @@test Soft line break multiple trailing line breaks
+testTrailingSoftLineBreaks : IO Bool
+testTrailingSoftLineBreaks =
+  golden "Hello\n\nWorld!\n\n\n" [Text "Hello", SoftLineBreak, Text "World!"]
+
+-- @@test Hard line break smoke
+smokeHardLineBreak : IO Bool
+smokeHardLineBreak =
+  golden "Hello\\\nWorld!" [Text "Hello", HardLineBreak, Text "World!"]

src/SSG/Djot/Lines.idr

@@ -0,0 +1,135 @@
+||| An effect for reading an input as a list of lines
+module SSG.Djot.Lines
+
+import Data.String
+
+import Control.Eff
+
+-- Only for iutils unit tests
+import System
+
+--************************
+--*   Effect Definition  *
+--************************
+
+export
+data Lines : Type -> Type where
+  ||| Peek the next line
+  Peek : Lines (Maybe String)
+  ||| Take the next line
+  Take : Lines (Maybe String)
+
+--************************
+--*    Effect Actions    *
+--************************
+
+export
+peek : Has Lines fs => Eff fs (Maybe String)
+peek = send Peek
+
+export
+take : Has Lines fs => Eff fs (Maybe String)
+take = send Take
+
+--************************
+--* Extra Effect Actions *
+--************************
+
+||| Take lines until a line matching the given predicate is encountered, dropping the
+||| all of the matching lines until the first non matching one
+|||
+||| Intended to be used to slurp up to the next blank line, discarding the blanks
+export
+slurp : Has Lines fs => (predicate : String -> Bool) -> Eff fs (List String)
+slurp predicate = do
+  Just line <- peek
+    | _ => pure []
+  if predicate line
+    then do
+      _ <- take
+      Just next <- peek
+        | _ => pure []
+      if predicate next
+        then slurp predicate
+        else pure []
+    else do
+      Just x <- take
+        | _ => 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   *
+--************************
+
+||| Split the next line from a string
+nextLine : String -> Maybe (String, String)
+nextLine str =
+  if null str
+    then Nothing
+    else
+      let 
+        (before, after) = break (\c => any (== c) ['\r', '\n']) str
+      in Just (before, removeNewline after)
+  where
+    -- If `after` is empty, we have hit the end of the string, and there is no newline
+    -- character to remove. If it has contents, then we need to remove the newline
+    removeNewline : String -> String
+    removeNewline str with (strM str)
+      removeNewline "" | StrNil = ""
+      removeNewline (strCons '\n' xs) | (StrCons '\n' xs) = xs
+      -- Handle either a \r or a \r\n
+      removeNewline (strCons '\r' xs) | (StrCons '\r' xs) with (strM xs)
+        removeNewline (strCons '\r' "") | (StrCons '\r' "") | StrNil = ""
+        removeNewline (strCons '\r' _) | (StrCons '\r' _) | (StrCons '\n' xs1) = xs1
+        removeNewline (strCons '\r' _) | (StrCons '\r' _) | (StrCons x xs1) = strCons x xs1
+      -- We shouldn't ever hit this case, as we would have to have contents after the
+      -- break, but no newline character, but we fill it in for the sake of totality
+      removeNewline (strCons x xs) | (StrCons x xs) = str
+
+unLines : String -> Lines s -> (s, String)
+unLines str Peek =
+  case nextLine str of
+    Nothing => (Nothing, str)
+    Just (before, after) => (Just before, str)
+unLines str Take =
+  case nextLine str of
+    Nothing => (Nothing, str)
+    Just (before, after) => (Just before, after)
+
+||| Feed a `Lines` from a provided input string
+export
+runLines : Has Lines fs =>
+  (input : String) -> Eff fs t -> Eff (fs - Lines) (t, String)
+runLines input =
+  handleRelayS input (\x, y => pure (y, x)) $ \input2, lns, f =>
+    let (vv, input3) = unLines input2 lns
+    in f input3 vv
+
+--************************
+--*      Unit Tests      *
+--************************
+
+-- @@test runLines Smoke Test
+runLinesSmoke : IO Bool
+runLinesSmoke = do
+  let input = "Hello\nWorld\n\n"
+  putStrLn "Input: \{show input}"
+  let reference = lines input
+  putStrLn "Reference: \{show reference}"
+  let (output, rest) = extract $ runLines input lines'
+  putStrLn "Output: \{show output}"
+  putStrLn "Rest: \{show rest}"
+  pure $ output == reference && null rest
+  where
+    lines' : Eff [Lines] (List String)
+    lines' = do
+      Just next <- take
+        | _ => pure []
+      map (next ::) lines'

src/SSG/Djot/Render.idr

@@ -0,0 +1,57 @@
+||| Render Djot to HTML
+module SSG.Djot.Render
+
+import SSG.HTML
+import SSG.Djot.Inline
+import SSG.Djot.Block
+
+import Data.List
+import Data.Nat
+
+||| Render a single inline element as HTML
+export
+renderInline : Inline -> Maybe (t ** Html t)
+-- FIXME: escape text
+renderInline (Text text) = Just (_ ** Text text)
+renderInline SoftLineBreak = Nothing
+renderInline HardLineBreak = Just (_ ** Void "br" [])
+
+||| Render a list of inline elments to html
+export
+renderInlines : List Inline -> (types ** DList _ Html types)
+renderInlines xs = fromList . catMaybes $ map renderInline xs
+
+||| Render a single block element as HTML
+export
+renderBlock : Block t -> (t ** Html t)
+
+||| Render a list of block level elements to html
+export
+renderBlocks : {types: _} -> DList _ Block types -> (types' ** DList _ Html types')
+
+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
+
+||| Render a complete html document from a list of block level elements
+export
+renderDocument : {types : _} -> DList _ Block types -> Html "html"
+renderDocument xs =
+  Normal "html" ["lang" =$ "en"] [
+    Normal "body" [] (snd (renderBlocks xs))
+  ]

src/SSG/HTML.idr

@@ -63,8 +63,8 @@ namespace Html
     if length attributes > 0
       then
         let attrs = joinBy " " $ map toString attributes
-        in "<\{type} \{attrs} />"
-      else "<\{type} />"
+        in "\{indent}<\{type} \{attrs}>"
+      else "\{indent}<\{type}>"
   viewIndented indent_level (Normal type attributes {content_types} contents) =
     let indent = replicate (indent_level * 2) ' ' in
     -- Special handling if the tag contains exactly one `Text` element, we won't
@@ -123,10 +123,10 @@ namespace Html
   TagType' : (type : String) -> {auto prf : IsValidTag type} -> Type
   TagType' type {prf} = TagType prf
 
-  ||| Smart constructor for tags
-  public export
-  tag : (type : String) -> {auto prf : IsValidTag type} -> TagType prf
-  tag type {prf = (PVoid type)} = Void type
-  tag type {prf = (PRawText type)} = RawText type
-  tag type {prf = (PEscapableRawText type)} = RawText type
-  tag type {prf = (PNormal type)} = Normal type
+  -- ||| Smart constructor for tags
+  -- public export
+  -- tag : (type : String) -> {auto prf : IsValidTag type} -> TagType prf
+  -- tag type {prf = (PVoid type)} = Void type
+  -- tag type {prf = (PRawText type)} = RawText type
+  -- tag type {prf = (PEscapableRawText type)} = RawText type
+  -- tag type {prf = (PNormal type)} = Normal type

src/SSG/Parser/Core.idr

@@ -1 +0,0 @@
-module SSG.Parser.Core

src/SSG/Parser/Markdown.idr

@@ -1 +0,0 @@
-module SSG.Parser.Markdown

test/Main.idr

@@ -0,0 +1,9 @@
+module Main
+
+import Test.Golden.RunnerHelper
+
+main : IO ()
+main = goldenRunner
+  [ "Hedgehog Tests" `atDir` "hedgehog"
+  , "Djot -> HTML Tests" `atDir` "djotToHtml"
+  ]

test/djotToHtml/001-paragraph/Main.idr

@@ -0,0 +1,18 @@
+module Main
+
+import SSG.Djot
+import SSG.HTML
+
+import System
+import System.File
+
+main : IO ()
+main = do
+  Right contents <- readFile "./test.dj"
+    | Left err => do
+      printLn err
+      exitFailure
+  let (_ ** blocks) = block contents
+  let html = renderDocument blocks
+  let output = render html
+  putStrLn output

test/djotToHtml/001-paragraph/expected

@@ -0,0 +1,33 @@
+<!DOCTYPE HTML>
+<html lang=en>
+  <body>
+    <p>Hello World!</p>
+    <p>Hello Alice!</p>
+    <p>
+      A Multi-line
+      Paragraph
+    </p>
+    <p>Two line breaks</p>
+    <p>
+      A multiline paragraph
+      with some indentation
+    </p>
+    <p>
+      This is a hard
+      <br>
+      line break
+    </p>
+    <p>
+      And again
+      <br>
+      with some spaces afterwards
+    </p>
+    <p>
+      And now we
+      mix soft
+      <br>
+      and hard
+      linebreaks
+    </p>
+  </body>
+</html>

test/djotToHtml/001-paragraph/pack.toml

@@ -0,0 +1,5 @@
+[custom.all.SSG]
+type = "local"
+path = "../../.."
+ipkg = "SSG.ipkg"
+test = "test/test.ipkg"

test/djotToHtml/001-paragraph/run

@@ -0,0 +1,6 @@
+rm -rf build/
+
+flock "$1" pack -q install-deps test.ipkg
+pack -q run test.ipkg
+
+rm -rf build/

test/djotToHtml/001-paragraph/test.dj

@@ -0,0 +1,23 @@
+Hello World!
+
+Hello Alice!
+
+A Multi-line
+Paragraph
+
+
+Two line breaks
+
+A multiline paragraph
+  with some indentation
+
+This is a hard\
+line break
+
+And again\   
+with some spaces afterwards
+
+And now we
+mix soft\ 
+and hard
+linebreaks

test/djotToHtml/001-paragraph/test.ipkg

@@ -0,0 +1,9 @@
+package a-test
+
+depends = SSG
+        , hedgehog
+        , eff
+
+main = Main
+
+executable = test

test/djotToHtml/002-headings/Main.idr

@@ -0,0 +1,18 @@
+module Main
+
+import SSG.Djot
+import SSG.HTML
+
+import System
+import System.File
+
+main : IO ()
+main = do
+  Right contents <- readFile "./test.dj"
+    | Left err => do
+      printLn err
+      exitFailure
+  let (_ ** blocks) = block contents
+  let html = renderDocument blocks
+  let output = render html
+  putStrLn output

test/djotToHtml/002-headings/expected

@@ -0,0 +1,44 @@
+<!DOCTYPE HTML>
+<html lang=en>
+  <body>
+    <h1>Level 1 Heading</h1>
+    <h2>Level 2 Heading</h2>
+    <h3>Level 3 Heading</h3>
+    <h4>Level 4 Heading</h4>
+    <h5>Level 5 Heading</h5>
+    <h6>Level 6 Heading</h6>
+    <p>####### Level 7 Not a heading</p>
+    <h1>
+      Multiline heading
+      with prefix
+    </h1>
+    <h1>
+      Multiline heading
+      with prefix and some extra whitespace
+    </h1>
+    <h2>
+      Level 2 multiline heading
+      with prefix
+    </h2>
+    <h1>
+      Multiline heading
+      with no prefix
+    </h1>
+    <h2>
+      Level 2 multiline heading
+      with no prefix
+    </h2>
+    <h1>
+      Unprefixed multiline heading
+      with some indentation
+    </h1>
+    <h1>
+      Heading level 1
+      # With a level 2 right after it (this line shouldn't be a heading)
+    </h1>
+    <h2>
+      Heading level 2
+      With a level 1 right after it (this line shouldn't be a heading)
+    </h2>
+  </body>
+</html>

test/djotToHtml/002-headings/pack.toml

@@ -0,0 +1,5 @@
+[custom.all.SSG]
+type = "local"
+path = "../../.."
+ipkg = "SSG.ipkg"
+test = "test/test.ipkg"

test/djotToHtml/002-headings/run

@@ -0,0 +1,6 @@
+rm -rf build/
+
+flock "$1" pack -q install-deps test.ipkg
+pack -q run test.ipkg
+
+rm -rf build/

test/djotToHtml/002-headings/test.dj

@@ -0,0 +1,38 @@
+# Level 1 Heading
+
+## Level 2 Heading
+
+### Level 3 Heading
+
+#### Level 4 Heading
+
+##### Level 5 Heading
+
+###### Level 6 Heading
+
+####### Level 7 Not a heading
+
+# Multiline heading
+# with prefix
+
+# Multiline heading
+#     with prefix and some extra whitespace
+
+## Level 2 multiline heading
+## with prefix
+
+
+# Multiline heading
+with no prefix
+
+## Level 2 multiline heading
+with no prefix
+
+# Unprefixed multiline heading
+  with some indentation
+
+# Heading level 1
+## With a level 2 right after it (this line shouldn't be a heading)
+
+## Heading level 2
+# With a level 1 right after it (this line shouldn't be a heading)

test/djotToHtml/002-headings/test.ipkg

@@ -0,0 +1,9 @@
+package a-test
+
+depends = SSG
+        , hedgehog
+        , eff
+
+main = Main
+
+executable = test

test/hedgehog/001-lines/Main.idr

@@ -0,0 +1,28 @@
+module Main
+
+import SSG.Djot.Lines
+
+import Control.Eff
+import Data.String
+import Hedgehog
+
+lines' : Eff [Lines] (List String)
+lines' = do
+  Just next <- take
+    | _ => pure []
+  map (next ::) lines'
+
+propLinesEquiv : Property
+propLinesEquiv = property $ do
+  str <- forAll $ string (linear 0 256) ascii
+  let std_lines = lines str
+  let (our_lines, rest) = extract $ runLines str lines'
+  our_lines === std_lines
+
+main : IO ()
+main = test $
+  [ MkGroup
+      "Lines effect"
+      [ ("Lines effect equivalent to lines", propLinesEquiv)
+      ]
+  ]

test/hedgehog/001-lines/expected

@@ -0,0 +1,3 @@
+━━━ Lines effect ━━━
+  ✓ Lines effect equivalent to lines passed 1000 tests.
+  ✓ 1 succeeded.

test/hedgehog/001-lines/pack.toml

@@ -0,0 +1,5 @@
+[custom.all.SSG]
+type = "local"
+path = "../../.."
+ipkg = "SSG.ipkg"
+test = "test/test.ipkg"

test/hedgehog/001-lines/run

@@ -0,0 +1,6 @@
+rm -rf build/
+
+flock "$1" pack -q install-deps test.ipkg
+HEDGEHOG_COLOR=0 pack -q run test.ipkg -n 1000
+
+rm -rf build/

test/hedgehog/001-lines/test.ipkg

@@ -0,0 +1,9 @@
+package a-test
+
+depends = SSG
+        , hedgehog
+        , eff
+
+main = Main
+
+executable = test

test/src/Main.idr

@@ -1,4 +0,0 @@
-module Main
-
-main : IO ()
-main = putStrLn "Test successful!"

test/test.ipkg

@@ -14,6 +14,7 @@ authors = "Nathan McCarty"
 
 -- packages to add to search path
 depends = SSG
+        , golden-runner-helper
 
 -- modules to install
 -- modules =
@@ -24,7 +25,7 @@ main = Main
 -- name of executable
 executable = "SSG-test"
 -- opts =
-sourcedir = "src"
+-- sourcedir = "."
 -- builddir =
 -- outputdir =
 

todo.org

@@ -2,5 +2,67 @@
 ** 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 Don't generate any further indent once we are already inside a =p=
+** TODO Text escaping function
 ** NO Move =Raw= out of =Tag=
 Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make sense
+* Parser Core
+** TODO Refine =location= in =ParserLocation=
+** TODO Error messages
+** TODO Combinators for predictive parsing
+* Djot [4/40]
+:PROPERTIES:
+:COOKIE_DATA: recursive
+:END:
+** Parsing [4/34]
+*** Block Level
+**** TODO Block Quote
+**** TODO List Item
+**** TODO List
+**** TODO Code Block
+**** TODO Thematic Break
+**** TODO Raw Block
+**** TODO Div
+**** TODO Pipe Table
+**** TODO Reference Link Definition
+**** TODO Footnote
+**** TODO Block Attributes
+**** TODO Heading Links
+**** DONE Paragraph
+**** DONE Heading
+*** Inline
+**** TODO Escaped Text
+**** TODO Link
+**** TODO Image
+**** TODO Autolink
+**** TODO Verbatim
+**** TODO Emphasis/Strong
+**** TODO Highlighted
+**** TODO Super/subscript
+**** TODO Insert/delete
+**** TODO Smart Punctuation
+**** TODO Math
+**** TODO Footnote Reference
+**** TODO Comment
+**** TODO Symbols
+**** TODO Raw Inline
+**** TODO Inline Attributes
+**** DONE Ordinary Text
+**** DONE Linebreak
+*** Lines effect
+**** TODO =IO= Backed implementation
+*** Known Inaccuracies
+**** TODO Stripping of prefixes from multiline headings isn't entirely accurate
+Currently, it strips at least =level= ~#~'s from the start of the line, but doesn't check to see if its the correct number of them.
+I need to see how other implementations handle this
+** Extensions
+*** TODO GFM-style alerts
+*** TODO Emoji extension
+**** TODO Unicode Emoji
+**** TODO Icon font emoji
+**** TODO Autolink for source forges
+** Misc
+*** TODO Add =fromString= for =Inline=
+* Features
+** TODO Preview rendered post in terminal
+Centered headings, text styling, and syntax highlighted code blocks