From 7f4bcf5f5168bdd7f6f7722016f18698d97867b7 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Wed, 19 Feb 2025 05:00:28 -0500 Subject: [PATCH 01/33] Disable smart constructor for now --- examples/src/HelloWorld.idr | 18 +++++++++--------- src/SSG/HTML.idr | 14 +++++++------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/examples/src/HelloWorld.idr b/examples/src/HelloWorld.idr index bd272ba..3dc71fa 100644 --- a/examples/src/HelloWorld.idr +++ b/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 diff --git a/src/SSG/HTML.idr b/src/SSG/HTML.idr index 91c07f3..4262e4e 100644 --- a/src/SSG/HTML.idr +++ b/src/SSG/HTML.idr @@ -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 From 045fab1b4bb1cba0d84c7eb744ab7a2ddcc5c185 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Wed, 19 Feb 2025 10:02:05 -0500 Subject: [PATCH 02/33] Core parser effect --- SSG.ipkg | 1 + src/SSG/Parser/Core.idr | 170 ++++++++++++++++++++++++++++++++++++++++ todo.org | 2 + 3 files changed, 173 insertions(+) diff --git a/SSG.ipkg b/SSG.ipkg index 0033da9..dadbfdb 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -15,6 +15,7 @@ authors = "Nathan McCarty" -- packages to add to search path depends = structures , eff + , refined -- modules to install modules = SSG.Parser.Core diff --git a/src/SSG/Parser/Core.idr b/src/SSG/Parser/Core.idr index e070a95..17c7725 100644 --- a/src/SSG/Parser/Core.idr +++ b/src/SSG/Parser/Core.idr @@ -1 +1,171 @@ module SSG.Parser.Core + +import Data.Vect +import Data.String + +import Control.Eff + +--------------------------- +-- Internal parser state -- +--------------------------- + +||| The location of a parser within a string +public export +data ParserLocation : Type where + AtPoint : (length : Int) -> (location : Int) -> ParserLocation + EndOfInput : (length : Int) -> ParserLocation + +namespace ParserLocation + export + fromString : String -> ParserLocation + fromString str = + if strLength str > 0 + then AtPoint 0 (strLength str) + else EndOfInput 0 + +||| The state of a parser +public export +record ParserState where + constructor MkPS + input : String + location : ParserLocation + +namespace ParserState + export + fromString : String -> ParserState + fromString str = MkPS str (fromString str) + + export + toString : ParserState -> String + toString (MkPS input (AtPoint length location)) = strSubstr location length input + toString (MkPS input (EndOfInput length)) = "" + + +||| Three way result of parsing +public export +data ParseResult : Type -> Type where + Got : t -> ParseResult t + Failed : t -> ParseResult t + EoF : ParseResult t + +----------------- +-- Effect Type -- +----------------- + +||| The parser effect +export +data Parser : Type -> Type where + -- Save and load the state + Save : Parser ParserState + Load : ParserState -> Parser () + -- Peek the next `n` characters, if there are enough, without altering the parser state + Peek : (n : Nat) -> Parser (Maybe (Vect n Char)) + -- Parse a single char, if it satisfies a predicate + ParseChar : (predicate : Char -> Bool) -> Parser (ParseResult Char) + -- Parse an exact string match + ParseExact : (str : String) -> Parser (ParseResult String) + -- Skip a run of 0 or more chars all satisfying a predicate + SkipChars : (predicate : Char -> Bool) -> Parser () + -- Detect the end of input + ParseEoF : Parser Bool + +----------------------- +-- Effectful Actions -- +----------------------- + +||| Aquire a copy of the current parser state +||| +||| Intended to be used for backtracking +export +save : Has Parser fs => Eff fs ParserState +save = send Save + +||| Restore the parser state to a previousy persisted copy +export +load : Has Parser fs => ParserState -> Eff fs () +load x = send $ Load x + +||| Look ahead exactly `n` characters +export +peek : Has Parser fs => (n : Nat) -> Eff fs (Maybe (Vect n Char)) +peek n = send $ Peek n + +||| Attempt to parse a single char satisfying the given predicate, leaving the parser +||| state unchanged on failure +export +parseChar : Has Parser fs => (predicate : Char -> Bool) -> Eff fs (ParseResult Char) +parseChar predicate = send $ ParseChar predicate + +||| Parse an exact match of the given string +export +parseExact : Has Parser fs => (str : String) -> Eff fs (ParseResult String) +parseExact str = send $ ParseExact str + +||| Skip a run of any number of characters satisfying the given predicate +export +skipChars : Has Parser fs => (predicate : Char -> Bool) -> Eff fs () +skipChars predicate = send $ SkipChars predicate + +-------------------- +-- Effect handler -- +-------------------- + +export +unParser : ParserState -> Parser a -> (a, ParserState) +-- Save the parser state +unParser s Save = + (s, s) +-- Load a provided parser state +unParser s (Load x) = + ((), x) +-- Look ahead exactly `n` characters +unParser s@(MkPS input (AtPoint length location)) (Peek n) = + let cs = unpack . strSubstr location (cast n) $ input + in (toVect n cs, s) +unParser s@(MkPS input (EndOfInput length)) (Peek n) = + (Nothing, s) +-- Attempt to parse a single character matching a given predicate, bail out without +-- affecting the parser state otherwise +unParser s@(MkPS input (AtPoint length location)) (ParseChar predicate) = + -- Saftey: We maintain location < length as a type invariant + let c = assert_total $ strIndex input location + in if predicate c + then if location + 1 < length + then (Got c, MkPS input (AtPoint length location)) + else (Got c, MkPS input (EndOfInput length)) + else (Failed c, s) +unParser s@(MkPS input (EndOfInput length)) (ParseChar predicate) = + (EoF, s) +-- Parse an exact string match +unParser s@(MkPS input (AtPoint length location)) (ParseExact str) = + let substr = strSubstr location (strLength str) input + in if substr == str + then if location + (strLength str) < length + then (Got substr, MkPS input (AtPoint length (location + strLength str))) + else (Got substr, MkPS input (EndOfInput length)) + else (Failed substr, s) +unParser s@(MkPS input (EndOfInput length)) (ParseExact str) = (EoF, s) +-- Skip any number of chars satisfying a given predicate +unParser s@(MkPS input (AtPoint length location)) (SkipChars predicate) = + case unParser s (ParseChar predicate) of + (Got _, s) => unParser s (SkipChars predicate) + (_, s) => ((), s) +unParser s@(MkPS input (EndOfInput length)) (SkipChars predicate) = + ((), s) +-- "Parse" the end of input +unParser s@(MkPS input (AtPoint length location)) ParseEoF = (False, s) +unParser s@(MkPS input (EndOfInput length)) ParseEoF = (True, s) + +export +runParser' : Has Parser fs => + (s : ParserState) -> Eff fs t -> Eff (fs - Parser) (t, ParserState) +runParser' s = + handleRelayS s (\state, t => pure (t, state)) $ \s2, ps, f => + let (a, st) = unParser s2 ps + in f st a + +export +runParser : Has Parser fs => + (s : String) -> Eff fs t -> Eff (fs - Parser) (t, String) +runParser s x = + map (\(x,y) => (x, toString y)) $ runParser' (fromString s) x diff --git a/todo.org b/todo.org index cda0ed9..a8cb81f 100644 --- a/todo.org +++ b/todo.org @@ -4,3 +4,5 @@ Probably want to refine the attribute and value strings, and be smarter about how we choose to quote the value string. ** 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= From 2033a48c3e079372d2ce73d04da87f86c812dc28 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Wed, 19 Feb 2025 11:22:25 -0500 Subject: [PATCH 03/33] Add Utility file --- SSG.ipkg | 1 + src/SSG/Parser/Core.idr | 5 ++ src/SSG/Parser/Markdown.idr | 9 ++++ src/SSG/Parser/Util.idr | 101 ++++++++++++++++++++++++++++++++++++ todo.org | 1 + 5 files changed, 117 insertions(+) create mode 100644 src/SSG/Parser/Util.idr diff --git a/SSG.ipkg b/SSG.ipkg index dadbfdb..5775c67 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -19,6 +19,7 @@ depends = structures -- modules to install modules = SSG.Parser.Core + , SSG.Parser.Util , SSG.Parser.Markdown , SSG.HTML , SSG.HTML.ElementTypes diff --git a/src/SSG/Parser/Core.idr b/src/SSG/Parser/Core.idr index 17c7725..ab8cc92 100644 --- a/src/SSG/Parser/Core.idr +++ b/src/SSG/Parser/Core.idr @@ -106,6 +106,11 @@ export skipChars : Has Parser fs => (predicate : Char -> Bool) -> Eff fs () skipChars predicate = send $ SkipChars predicate +||| Detect EoF +export +parseEoF : Has Parser fs => Eff fs Bool +parseEoF = send ParseEoF + -------------------- -- Effect handler -- -------------------- diff --git a/src/SSG/Parser/Markdown.idr b/src/SSG/Parser/Markdown.idr index e760e1b..4f4ade3 100644 --- a/src/SSG/Parser/Markdown.idr +++ b/src/SSG/Parser/Markdown.idr @@ -1 +1,10 @@ module SSG.Parser.Markdown + +import SSG.Parser.Core +import SSG.Parser.Util + +import Data.List1 +import Data.Vect +import Data.Nat +import Control.Eff + diff --git a/src/SSG/Parser/Util.idr b/src/SSG/Parser/Util.idr new file mode 100644 index 0000000..22aeeeb --- /dev/null +++ b/src/SSG/Parser/Util.idr @@ -0,0 +1,101 @@ +module SSG.Parser.Util + +import SSG.Parser.Core + +import Data.List1 +import Data.Vect +import Control.Eff + +||| Type alias for parsing errors +public export +ParseError : Type +ParseError = String + +||| Type alias for a parser equipped with exception handling +public export +PS : Type -> Type +PS a = Eff [Parser, Except ParseError] a + +||| Attempt to run a fallible parser, backtracking on failure +export +try : (f : PS a) -> (err : ParseError -> PS a) -> PS a +try f err = do + state <- save + result <- lift . runExcept $ f + case result of + Left e => do + load state + err e + Right result => pure result + +||| Variant of `try` that wraps the result in a `Maybe` +export +tryMaybe : (f : PS a) -> PS (Maybe a) +tryMaybe f = try (map Just f) (\_ => pure Nothing) + +||| Variant of `try` that wraps the result in an `Either` +export +tryEither : (f : PS a) -> PS (Either ParseError a) +tryEither f = try (map Right f) (\e => pure $ Left e) + +||| Attempt to parse each of a list of parsers, returning the first that +||| succeeds +export +oneOfE : (err : ParseError) -> List (PS a) -> PS a +oneOfE err [] = throw err +oneOfE err (x :: xs) = do + res <- tryMaybe x + case res of + Nothing => oneOfE err xs + Just y => pure y + +||| Attempt to parse 0+ of a thing +export +many : (f : PS a) -> PS (List a) +many f = do + Just next <- tryMaybe f + | _ => pure [] + map (next ::) (many f) + +||| Attempt to parse at least one of a thing, giving the supplied error on +||| failure +export +atLeastOne : (err : ParseError) -> (f : PS a) -> PS (List1 a) +atLeastOne err f = do + Just head <- tryMaybe f + | _ => throw err + tail <- many f + pure $ head ::: tail + +||| Attempt to parse one of a list of strings +export +theseStrings : List String -> PS String +theseStrings strs = theseStrings' strs + where + theseStrings' : List String -> PS String + theseStrings' [] = throw "Expected one of \{show strs}" + theseStrings' (x :: xs) = do + res <- parseExact x + case res of + Got y => pure y + _ => theseStrings' xs + +||| Attempt to parse one of a list of chars +export +theseChars : List Char -> PS Char +theseChars cs = do + Just [next] <- peek 1 + | _ => throw "Unexpected EoF" + if any (== next) cs + then pure next + else throw "Expected one of \{show cs}, got \{show next}" + +||| Attempt to parse any char not in the list +export +notTheseChars : List Char -> PS Char +notTheseChars cs = do + Just [next] <- peek 1 + | _ => throw "Unexpected EoF" + if any (== next) cs + then throw "Expected not one of \{show cs}, got \{show next}" + else pure next diff --git a/todo.org b/todo.org index a8cb81f..1a2d61b 100644 --- a/todo.org +++ b/todo.org @@ -6,3 +6,4 @@ Probably want to refine the attribute and value strings, and be smarter about ho 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 From 98ed90a9bcb3da1ce7ae410c83110dd1def96752 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 02:49:47 -0500 Subject: [PATCH 04/33] Inline text parsing --- SSG.ipkg | 3 +- src/SSG/Parser/Core.idr | 20 ++- src/SSG/Parser/Djot.idr | 267 ++++++++++++++++++++++++++++++++++++ src/SSG/Parser/Markdown.idr | 10 -- src/SSG/Parser/Util.idr | 41 +++++- todo.org | 47 +++++++ 6 files changed, 373 insertions(+), 15 deletions(-) create mode 100644 src/SSG/Parser/Djot.idr delete mode 100644 src/SSG/Parser/Markdown.idr diff --git a/SSG.ipkg b/SSG.ipkg index 5775c67..5189c9b 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -16,11 +16,12 @@ authors = "Nathan McCarty" depends = structures , eff , refined + , elab-util -- modules to install modules = SSG.Parser.Core , SSG.Parser.Util - , SSG.Parser.Markdown + , SSG.Parser.Djot , SSG.HTML , SSG.HTML.ElementTypes diff --git a/src/SSG/Parser/Core.idr b/src/SSG/Parser/Core.idr index ab8cc92..9cea39d 100644 --- a/src/SSG/Parser/Core.idr +++ b/src/SSG/Parser/Core.idr @@ -4,6 +4,9 @@ import Data.Vect import Data.String import Control.Eff +import Derive.Prelude + +%language ElabReflection --------------------------- -- Internal parser state -- @@ -15,12 +18,14 @@ data ParserLocation : Type where AtPoint : (length : Int) -> (location : Int) -> ParserLocation EndOfInput : (length : Int) -> ParserLocation +%runElab derive "ParserLocation" [Show] + namespace ParserLocation export fromString : String -> ParserLocation fromString str = if strLength str > 0 - then AtPoint 0 (strLength str) + then AtPoint (strLength str) 0 else EndOfInput 0 ||| The state of a parser @@ -30,6 +35,8 @@ record ParserState where input : String location : ParserLocation +%runElab derive "ParserState" [Show] + namespace ParserState export fromString : String -> ParserState @@ -69,6 +76,15 @@ data Parser : Type -> Type where -- Detect the end of input ParseEoF : Parser Bool +Show (Parser a) where + show Save = "save" + show (Load x) = "load: \{show x}" + show (Peek n) = "peek: \{show n}]" + show (ParseChar predicate) = "ParseChar" + show (ParseExact str) = "ParseExact: \{str}" + show (SkipChars predicate) = "SkipChars" + show ParseEoF = "ParseEof" + ----------------------- -- Effectful Actions -- ----------------------- @@ -136,7 +152,7 @@ unParser s@(MkPS input (AtPoint length location)) (ParseChar predicate) = let c = assert_total $ strIndex input location in if predicate c then if location + 1 < length - then (Got c, MkPS input (AtPoint length location)) + then (Got c, MkPS input (AtPoint length (location + 1))) else (Got c, MkPS input (EndOfInput length)) else (Failed c, s) unParser s@(MkPS input (EndOfInput length)) (ParseChar predicate) = diff --git a/src/SSG/Parser/Djot.idr b/src/SSG/Parser/Djot.idr new file mode 100644 index 0000000..7d19cee --- /dev/null +++ b/src/SSG/Parser/Djot.idr @@ -0,0 +1,267 @@ +module SSG.Parser.Djot + +import SSG.Parser.Core +import SSG.Parser.Util + +import Data.List1 +import Data.Vect +import Data.Nat +import Data.String + +import Control.Eff +import Derive.Prelude + +-- For iutils unit tests +import System + +%language ElabReflection + +--***************************************** +--* Data Types * +--***************************************** + +public export +data Inline : Type where + HardLineBreak : Inline + SoftLineBreak : Inline + NonBreakingSpace : Inline + Text : (c : Char) -> Inline + +%runElab derive "Inline" [Show, Eq] + +public export +data Block : Type where + +--***************************************** +--* Character Classes and String Escaping * +--***************************************** + +----------------------- +-- Character classes -- +----------------------- + +-- Class contents + +punctuationChars : List Char +punctuationChars = + [ + '!', '"', '#', '$', '%', '&', '\'' + , '(' , ')' , '*' , '+' , ',' , '-' + , '.' , '/' , ':' , ';' , '<' , '=' + , '>' , '?' , '@' , '[' , ']' , '^' + , '_' , '`' , '{' , '|' , '}' , '~' + ] + +horizontalWhitespaceChars : List Char +horizontalWhitespaceChars = + [' ', '\t'] + +verticalWhitespaceChars : List Char +verticalWhitespaceChars = + ['\n', '\r'] + +-- Class parsers + +punctuation : PS Char +punctuation = theseChars punctuationChars + +-------------- +-- Escaping -- +-------------- + +escapedChar : PS Char +escapedChar = do + _ <- thisString "\\" + oneOfE "Expected an escapable code" + [ punctuation + , exactReplace "n" '\n' + , exactReplace "t" '\t' + , exactReplace "r" '\r' + ] + +------------------------------------ +-- Line Qualifying And Whitespace -- +------------------------------------ + +spaces : PS Nat +spaces = do + xs <- many $ theseChars horizontalWhitespaceChars + pure $ length xs + +nonTerminal : PS Char +nonTerminal = notTheseChars verticalWhitespaceChars + +lineEnding : PS String +lineEnding = theseStrings ["\r\n", "\n", "\r"] + +terminal : PS () +terminal = do + Nothing <- tryMaybe lineEnding + | _ => pure () + test <- parseEoF + case test of + False => throw "Expected line terminal" + True => pure () + +line : PS (List Char) +line = do + cs <- many nonTerminal + terminal + pure cs + +isHorizontalWhitespace : Char -> Bool +isHorizontalWhitespace c = any (== c) horizontalWhitespaceChars + +blankLine : PS (List Char) +blankLine = do + cs <- line + case all isHorizontalWhitespace cs of + False => throw "nonblank line" + True => pure cs + +--***************************************** +--* Inline syntax * +--***************************************** + +inlineElement : PS Inline + +------------------------ +-- Escaped Whitespace -- +------------------------ + +hardLineBreak : PS Inline +hardLineBreak = do + _ <- thisString "\\" + _ <- spaces + _ <- lineEnding + pure $ HardLineBreak + +nbsp : PS Inline +nbsp = do + _ <- thisString "\\ " + pure $ NonBreakingSpace + +softLineBreak : PS Inline +softLineBreak = do + _ <- lineEnding + -- Check to see if the next line is empty, if it is, we are at the end of the inline + -- content, go ahead and bail + state <- save + Nothing <- tryMaybe blankLine + | Just _ => throw "End of inline" + load state + pure $ SoftLineBreak + +--------------------- +-- Emphasis/Strong -- +--------------------- + +---------- +-- Text -- +---------- + +-- Process escape codes before processing as text +escapedText : PS Inline +escapedText = do + c <- escapedChar + pure $ Text c + +-- Any non-line-ending character can be part of regular text +text : PS Inline +text = do + c <- nonTerminal + pure $ Text c + +--------------------------- +-- Overall Inline Parser -- +--------------------------- + +inlineElement = oneOfE "" [ + hardLineBreak + , nbsp + , escapedText + , softLineBreak + -- Text is last so that anything can superseed it + , text + ] + +inline : PS (List1 Inline) +inline = atLeastOne "Expected Inline Content" inlineElement + + +--***************************************** +--* Utility Functions * +--***************************************** + +------------------ +-- Constructors -- +------------------ + +namespace Inline + export + fromString : String -> List (Inline) + fromString str with (asList str) + fromString "" | [] = [] + fromString (strCons c str) | (c :: x) = + Text c :: fromString str | x + +--***************************************** +--* Unit Tests * +--***************************************** + +------------------------------- +-- Testing Utility Functions -- +------------------------------- + +-- Test a parser against a golden value with the supplied input +golden : Show a => Eq a => + (input : String) -> (reference : a) -> (parser : PS a) -> IO Bool +golden input ref parser = do + putStrLn "Input: \{input}" + putStrLn "Expected: \{show ref}" + let got = runPS parser input + case got of + Left err => do + putStrLn "Failed with error: \{err}" + pure False + Right x => do + putStrLn "Output: \{show x}" + pure $ x == ref + +------------------------- +-- Inline Syntax Tests -- +------------------------- + +-- @@test Plain Text Hello World +inlineTextSmoke : IO Bool +inlineTextSmoke = + let input = "Hello World!" in + golden input (map Text . unpack $ input) (map forget inline) + +-- @@test Escaped Text +inlineEscapedSmoke : IO Bool +inlineEscapedSmoke = + let input = "Hello\\n\\*World" + ref = fromString "Hello" ++ [Text '\n', Text '*'] ++ fromString "World" + in golden input ref (map forget inline) + +-- @@test Hard Line Break +inlineHardBreakSmoke : IO Bool +inlineHardBreakSmoke = + let input = "Hello\\\nWorld" + ref = fromString "Hello" ++ [HardLineBreak] ++ fromString "World" + in golden input ref (map forget inline) + +-- @@test Soft Line Break +inlineSoftBreakSmoke : IO Bool +inlineSoftBreakSmoke = + let input = "Hello\nWorld" + ref = fromString "Hello" ++ [SoftLineBreak] ++ fromString "World" + in golden input ref (map forget inline) + +-- @@test Nonbreaking Space +inlineNbspSmoke : IO Bool +inlineNbspSmoke = + let input = "Hello\\ World" + ref = fromString "Hello" ++ [NonBreakingSpace] ++ fromString "World" + in golden input ref (map forget inline) diff --git a/src/SSG/Parser/Markdown.idr b/src/SSG/Parser/Markdown.idr deleted file mode 100644 index 4f4ade3..0000000 --- a/src/SSG/Parser/Markdown.idr +++ /dev/null @@ -1,10 +0,0 @@ -module SSG.Parser.Markdown - -import SSG.Parser.Core -import SSG.Parser.Util - -import Data.List1 -import Data.Vect -import Data.Nat -import Control.Eff - diff --git a/src/SSG/Parser/Util.idr b/src/SSG/Parser/Util.idr index 22aeeeb..a195236 100644 --- a/src/SSG/Parser/Util.idr +++ b/src/SSG/Parser/Util.idr @@ -16,6 +16,12 @@ public export PS : Type -> Type PS a = Eff [Parser, Except ParseError] a +||| Run a parser and extact the parsed value +export +runPS : PS a -> (str : String) -> Either String a +runPS x str = + fst . extract . runParser str . runExcept $ x + ||| Attempt to run a fallible parser, backtracking on failure export try : (f : PS a) -> (err : ParseError -> PS a) -> PS a @@ -67,6 +73,16 @@ atLeastOne err f = do tail <- many f pure $ head ::: tail +||| Attempt to parse an exact string +export +thisString : String -> PS String +thisString str = do + res <- parseExact str + case res of + Got x => pure x + Failed x => throw "Expected \{show str} Got \{show x}" + EoF => throw "Unexpected EoF" + ||| Attempt to parse one of a list of strings export theseStrings : List String -> PS String @@ -87,7 +103,9 @@ theseChars cs = do Just [next] <- peek 1 | _ => throw "Unexpected EoF" if any (== next) cs - then pure next + then do + _ <- parseChar (const True) + pure next else throw "Expected one of \{show cs}, got \{show next}" ||| Attempt to parse any char not in the list @@ -98,4 +116,23 @@ notTheseChars cs = do | _ => throw "Unexpected EoF" if any (== next) cs then throw "Expected not one of \{show cs}, got \{show next}" - else pure next + else do + _ <- parseChar (const True) + pure next + +||| Parse an exact match, but 'replace' it with the provided value +export +exactReplace : (str : String) -> (replacement : a) -> PS a +exactReplace str replacement = do + _ <- parseExact str + pure replacement + +||| Any character +export +any : PS Char +any = do + x <- parseChar (const True) + case x of + Got y => pure y + (Failed y) => throw "What?" + EoF => throw "Unexpected EoF" diff --git a/todo.org b/todo.org index 1a2d61b..0ac9266 100644 --- a/todo.org +++ b/todo.org @@ -7,3 +7,50 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se * Parser Core ** TODO Refine =location= in =ParserLocation= ** TODO Error messages +** TODO Combinators for predictive parsing +* Djot [2/40] +:PROPERTIES: +:COOKIE_DATA: recursive +:END: +** Inline Syntax [2/18] +*** DONE Ordinary 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 +*** DONE Linebreak +*** TODO Comment +*** TODO Symbols +*** TODO Raw inline +*** TODO Span +*** TODO Inline attributes +** Block Syntax [0/15] +*** TODO Paragraph +*** TODO Heading +*** 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 +*** TODO definition +*** TODO Footnote +*** TODO Block attributes +*** TODO Links to headings +** TODO Predictive parsing +** TODO Support all types of whitespace +*** TODO Escaping +*** TODO Whitespace class +** TODO hex escapes +** TODO GFM style alerts +** TODO Group adjacent =Text=s into a =String= From f60e209073514454516967f1c6250f2e6fca6087 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 03:20:46 -0500 Subject: [PATCH 05/33] Paragraph Support --- src/SSG/Parser/Djot.idr | 119 ++++++++++++++++++++++++++++++++-------- todo.org | 77 ++++++++++++++------------ 2 files changed, 136 insertions(+), 60 deletions(-) diff --git a/src/SSG/Parser/Djot.idr b/src/SSG/Parser/Djot.idr index 7d19cee..2900b9b 100644 --- a/src/SSG/Parser/Djot.idr +++ b/src/SSG/Parser/Djot.idr @@ -31,6 +31,9 @@ data Inline : Type where public export data Block : Type where + Paragraph : (contents : List1 Inline) -> Block + +%runElab derive "Block" [Show, Eq] --***************************************** --* Character Classes and String Escaping * @@ -83,9 +86,12 @@ escapedChar = do -- Line Qualifying And Whitespace -- ------------------------------------ +space : PS Char +space = theseChars horizontalWhitespaceChars + spaces : PS Nat spaces = do - xs <- many $ theseChars horizontalWhitespaceChars + xs <- many space pure $ length xs nonTerminal : PS Char @@ -106,7 +112,7 @@ terminal = do line : PS (List Char) line = do cs <- many nonTerminal - terminal + _ <- lineEnding pure cs isHorizontalWhitespace : Char -> Bool @@ -119,12 +125,26 @@ blankLine = do False => throw "nonblank line" True => pure cs +blankLineOrEnd : PS () +blankLineOrEnd = do + Nothing <- tryMaybe blankLine + | Just _ => pure () + eof <- parseEoF + case eof of + False => throw "Expected newline or end of document" + True => pure () + +blankLines : PS () +blankLines = do + xs <- many blankLine + if length xs > 0 + then pure () + else blankLineOrEnd + --***************************************** --* Inline syntax * --***************************************** -inlineElement : PS Inline - ------------------------ -- Escaped Whitespace -- ------------------------ @@ -176,34 +196,52 @@ text = do -- Overall Inline Parser -- --------------------------- -inlineElement = oneOfE "" [ - hardLineBreak - , nbsp +inlineElementsNoNewlines : PS Inline +inlineElementsNoNewlines = oneOfE "" [ + nbsp , escapedText - , softLineBreak -- Text is last so that anything can superseed it , text ] +inlineElement : PS Inline +inlineElement = oneOfE "" [ + hardLineBreak + , softLineBreak + , inlineElementsNoNewlines + ] + inline : PS (List1 Inline) inline = atLeastOne "Expected Inline Content" inlineElement - --***************************************** ---* Utility Functions * +--* Block Syntax * --***************************************** ------------------- --- Constructors -- ------------------- +--------------- +-- Paragraph -- +--------------- -namespace Inline - export - fromString : String -> List (Inline) - fromString str with (asList str) - fromString "" | [] = [] - fromString (strCons c str) | (c :: x) = - Text c :: fromString str | x +paragraph : PS Block +paragraph = do + inlines <- inline + blankLineOrEnd + pure $ Paragraph inlines + +-------------------------- +-- Overall Block Parser -- +-------------------------- + +block : PS Block +block = do + -- eat up any blank lines + _ <- many blankLine + oneOfE "" [ + paragraph + ] + +blocks : PS (List Block) +blocks = many block --***************************************** --* Unit Tests * @@ -228,6 +266,18 @@ golden input ref parser = do putStrLn "Output: \{show x}" pure $ x == ref +inlineFromString : String -> List (Inline) +inlineFromString str with (asList str) + inlineFromString "" | [] = [] + inlineFromString (strCons c str) | (c :: x) = + Text c :: inlineFromString str | x + +inlineFromString' : String -> List1 (Inline) +inlineFromString' str = + case inlineFromString str of + [] => assert_total $ idris_crash "Bad unit test fromString" + (x :: xs) => x ::: xs + ------------------------- -- Inline Syntax Tests -- ------------------------- @@ -242,26 +292,47 @@ inlineTextSmoke = inlineEscapedSmoke : IO Bool inlineEscapedSmoke = let input = "Hello\\n\\*World" - ref = fromString "Hello" ++ [Text '\n', Text '*'] ++ fromString "World" + ref = inlineFromString "Hello" ++ [Text '\n', Text '*'] ++ inlineFromString "World" in golden input ref (map forget inline) -- @@test Hard Line Break inlineHardBreakSmoke : IO Bool inlineHardBreakSmoke = let input = "Hello\\\nWorld" - ref = fromString "Hello" ++ [HardLineBreak] ++ fromString "World" + ref = inlineFromString "Hello" ++ [HardLineBreak] ++ inlineFromString "World" in golden input ref (map forget inline) -- @@test Soft Line Break inlineSoftBreakSmoke : IO Bool inlineSoftBreakSmoke = let input = "Hello\nWorld" - ref = fromString "Hello" ++ [SoftLineBreak] ++ fromString "World" + ref = inlineFromString "Hello" ++ [SoftLineBreak] ++ inlineFromString "World" in golden input ref (map forget inline) -- @@test Nonbreaking Space inlineNbspSmoke : IO Bool inlineNbspSmoke = let input = "Hello\\ World" - ref = fromString "Hello" ++ [NonBreakingSpace] ++ fromString "World" + ref = inlineFromString "Hello" ++ [NonBreakingSpace] ++ inlineFromString "World" in golden input ref (map forget inline) + +------------------------ +-- Block Syntax Tests -- +------------------------ + +-- @@test Paragraph +blockParagraphSmoke : IO Bool +blockParagraphSmoke = + let input = "Hello World" + ref = [Paragraph (inlineFromString' "Hello World")] + in golden input ref blocks + +-- @@test Two Paragraph +blockTwoParagraphSmoke : IO Bool +blockTwoParagraphSmoke = + let input = "Hello World\n\nHello Again" + ref = [ + Paragraph (inlineFromString' "Hello World") + , Paragraph (inlineFromString' "Hello Again") + ] + in golden input ref blocks diff --git a/todo.org b/todo.org index 0ac9266..2d3b362 100644 --- a/todo.org +++ b/todo.org @@ -8,45 +8,50 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [2/40] +* Djot [3/42] :PROPERTIES: :COOKIE_DATA: recursive :END: -** Inline Syntax [2/18] -*** DONE Ordinary 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 -*** DONE Linebreak -*** TODO Comment -*** TODO Symbols -*** TODO Raw inline -*** TODO Span -*** TODO Inline attributes -** Block Syntax [0/15] -*** TODO Paragraph -*** TODO Heading -*** 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 -*** TODO definition -*** TODO Footnote -*** TODO Block attributes -*** TODO Links to headings +** Parsing +*** Inline Syntax [2/18] +**** DONE Ordinary 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 +**** DONE Linebreak +**** TODO Comment +**** TODO Symbols +**** TODO Raw inline +**** TODO Span +**** TODO Inline attributes +*** Block Syntax [1/16] +**** DONE Paragraph +**** Heading +***** TODO Multiline without leading count +***** TODO Basic +**** 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 +**** TODO definition +**** TODO Footnote +**** TODO Block attributes +**** TODO Links to headings +** TODO Rendering +** Bugs [0/0] ** TODO Predictive parsing ** TODO Support all types of whitespace *** TODO Escaping From f0718bbf2c79b9130dd519b9fe53e90859160bbc Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 03:26:12 -0500 Subject: [PATCH 06/33] Move Djot module --- SSG.ipkg | 2 +- src/SSG/{Parser => }/Djot.idr | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) rename src/SSG/{Parser => }/Djot.idr (99%) diff --git a/SSG.ipkg b/SSG.ipkg index 5189c9b..ef48458 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -21,7 +21,7 @@ depends = structures -- modules to install modules = SSG.Parser.Core , SSG.Parser.Util - , SSG.Parser.Djot + , SSG.Djot , SSG.HTML , SSG.HTML.ElementTypes diff --git a/src/SSG/Parser/Djot.idr b/src/SSG/Djot.idr similarity index 99% rename from src/SSG/Parser/Djot.idr rename to src/SSG/Djot.idr index 2900b9b..131e2bf 100644 --- a/src/SSG/Parser/Djot.idr +++ b/src/SSG/Djot.idr @@ -1,4 +1,4 @@ -module SSG.Parser.Djot +module SSG.Djot import SSG.Parser.Core import SSG.Parser.Util From 79c74426c1c3f424fa296cc2c4c36ba3159c38c3 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 03:56:30 -0500 Subject: [PATCH 07/33] Basic Heading Parsing --- src/SSG/Djot.idr | 71 +++++++++++++++++++++++++++++++++++++++++++++++- todo.org | 7 ++--- 2 files changed, 73 insertions(+), 5 deletions(-) diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr index 131e2bf..41924ca 100644 --- a/src/SSG/Djot.idr +++ b/src/SSG/Djot.idr @@ -29,9 +29,45 @@ data Inline : Type where %runElab derive "Inline" [Show, Eq] +public export +data HeaderLevel : Type where + H1 : HeaderLevel + H2 : HeaderLevel + H3 : HeaderLevel + H4 : HeaderLevel + H5 : HeaderLevel + H6 : HeaderLevel + +%runElab derive "HeaderLevel" [Eq] + +export +Show HeaderLevel where + show H1 = "1" + show H2 = "2" + show H3 = "3" + show H4 = "4" + show H5 = "5" + show H6 = "6" + +namespace HeaderLevel + public export + integerToHeader : Integer -> Maybe HeaderLevel + integerToHeader 1 = Just H1 + integerToHeader 2 = Just H2 + integerToHeader 3 = Just H3 + integerToHeader 4 = Just H4 + integerToHeader 5 = Just H5 + integerToHeader 6 = Just H6 + integerToHeader i = Nothing + + export + fromInteger : (x : Integer) -> {auto prf : IsJust (integerToHeader x)} -> HeaderLevel + fromInteger x = fromJust $ integerToHeader x + public export data Block : Type where Paragraph : (contents : List1 Inline) -> Block + Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block %runElab derive "Block" [Show, Eq] @@ -228,6 +264,20 @@ paragraph = do blankLineOrEnd pure $ Paragraph inlines +------------- +-- Heading -- +------------- + +heading : PS Block +heading = do + levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#" + ws <- atLeastOne "Expected Whitespace after header marker" $ space + case integerToHeader (natToInteger $ length levelMarker) of + Nothing => throw "Invalid header length: \{show $ length levelMarker}" + Just level => do + inlines <- inline + pure $ Heading level inlines + -------------------------- -- Overall Block Parser -- -------------------------- @@ -237,7 +287,8 @@ block = do -- eat up any blank lines _ <- many blankLine oneOfE "" [ - paragraph + heading + , paragraph ] blocks : PS (List Block) @@ -336,3 +387,21 @@ blockTwoParagraphSmoke = , Paragraph (inlineFromString' "Hello Again") ] in golden input ref blocks + +-- @@test Level 1 heading +blockLevelOneHeadingSmoke : IO Bool +blockLevelOneHeadingSmoke = + let input = "# Level 1" + ref = [ + Heading 1 (inlineFromString' "Level 1") + ] + in golden input ref blocks + +-- @@test Level 2 heading +blockLevelTwoHeadingSmoke : IO Bool +blockLevelTwoHeadingSmoke = + let input = "## Level 2" + ref = [ + Heading 2 (inlineFromString' "Level 2") + ] + in golden input ref blocks diff --git a/todo.org b/todo.org index 2d3b362..aad08f1 100644 --- a/todo.org +++ b/todo.org @@ -8,7 +8,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [3/42] +* Djot [4/42] :PROPERTIES: :COOKIE_DATA: recursive :END: @@ -32,11 +32,11 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Raw inline **** TODO Span **** TODO Inline attributes -*** Block Syntax [1/16] +*** Block Syntax [2/16] **** DONE Paragraph **** Heading ***** TODO Multiline without leading count -***** TODO Basic +***** DONE Basic **** TODO Block quote **** TODO List item **** TODO List @@ -51,7 +51,6 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Block attributes **** TODO Links to headings ** TODO Rendering -** Bugs [0/0] ** TODO Predictive parsing ** TODO Support all types of whitespace *** TODO Escaping From 6c36d6e62a5aadad997ffad37f5759a437d163ea Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 04:16:28 -0500 Subject: [PATCH 08/33] Refactor Djot into modules --- SSG.ipkg | 3 + src/SSG/Djot.idr | 407 +--------------------------------------- src/SSG/Djot/Block.idr | 153 +++++++++++++++ src/SSG/Djot/Common.idr | 151 +++++++++++++++ src/SSG/Djot/Inline.idr | 161 ++++++++++++++++ 5 files changed, 470 insertions(+), 405 deletions(-) create mode 100644 src/SSG/Djot/Block.idr create mode 100644 src/SSG/Djot/Common.idr create mode 100644 src/SSG/Djot/Inline.idr diff --git a/SSG.ipkg b/SSG.ipkg index ef48458..adfdb9e 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -22,6 +22,9 @@ depends = structures modules = SSG.Parser.Core , SSG.Parser.Util , SSG.Djot + , SSG.Djot.Common + , SSG.Djot.Inline + , SSG.Djot.Block , SSG.HTML , SSG.HTML.ElementTypes diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr index 41924ca..274ed75 100644 --- a/src/SSG/Djot.idr +++ b/src/SSG/Djot.idr @@ -1,407 +1,4 @@ module SSG.Djot -import SSG.Parser.Core -import SSG.Parser.Util - -import Data.List1 -import Data.Vect -import Data.Nat -import Data.String - -import Control.Eff -import Derive.Prelude - --- For iutils unit tests -import System - -%language ElabReflection - ---***************************************** ---* Data Types * ---***************************************** - -public export -data Inline : Type where - HardLineBreak : Inline - SoftLineBreak : Inline - NonBreakingSpace : Inline - Text : (c : Char) -> Inline - -%runElab derive "Inline" [Show, Eq] - -public export -data HeaderLevel : Type where - H1 : HeaderLevel - H2 : HeaderLevel - H3 : HeaderLevel - H4 : HeaderLevel - H5 : HeaderLevel - H6 : HeaderLevel - -%runElab derive "HeaderLevel" [Eq] - -export -Show HeaderLevel where - show H1 = "1" - show H2 = "2" - show H3 = "3" - show H4 = "4" - show H5 = "5" - show H6 = "6" - -namespace HeaderLevel - public export - integerToHeader : Integer -> Maybe HeaderLevel - integerToHeader 1 = Just H1 - integerToHeader 2 = Just H2 - integerToHeader 3 = Just H3 - integerToHeader 4 = Just H4 - integerToHeader 5 = Just H5 - integerToHeader 6 = Just H6 - integerToHeader i = Nothing - - export - fromInteger : (x : Integer) -> {auto prf : IsJust (integerToHeader x)} -> HeaderLevel - fromInteger x = fromJust $ integerToHeader x - -public export -data Block : Type where - Paragraph : (contents : List1 Inline) -> Block - Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block - -%runElab derive "Block" [Show, Eq] - ---***************************************** ---* Character Classes and String Escaping * ---***************************************** - ------------------------ --- Character classes -- ------------------------ - --- Class contents - -punctuationChars : List Char -punctuationChars = - [ - '!', '"', '#', '$', '%', '&', '\'' - , '(' , ')' , '*' , '+' , ',' , '-' - , '.' , '/' , ':' , ';' , '<' , '=' - , '>' , '?' , '@' , '[' , ']' , '^' - , '_' , '`' , '{' , '|' , '}' , '~' - ] - -horizontalWhitespaceChars : List Char -horizontalWhitespaceChars = - [' ', '\t'] - -verticalWhitespaceChars : List Char -verticalWhitespaceChars = - ['\n', '\r'] - --- Class parsers - -punctuation : PS Char -punctuation = theseChars punctuationChars - --------------- --- Escaping -- --------------- - -escapedChar : PS Char -escapedChar = do - _ <- thisString "\\" - oneOfE "Expected an escapable code" - [ punctuation - , exactReplace "n" '\n' - , exactReplace "t" '\t' - , exactReplace "r" '\r' - ] - ------------------------------------- --- Line Qualifying And Whitespace -- ------------------------------------- - -space : PS Char -space = theseChars horizontalWhitespaceChars - -spaces : PS Nat -spaces = do - xs <- many space - pure $ length xs - -nonTerminal : PS Char -nonTerminal = notTheseChars verticalWhitespaceChars - -lineEnding : PS String -lineEnding = theseStrings ["\r\n", "\n", "\r"] - -terminal : PS () -terminal = do - Nothing <- tryMaybe lineEnding - | _ => pure () - test <- parseEoF - case test of - False => throw "Expected line terminal" - True => pure () - -line : PS (List Char) -line = do - cs <- many nonTerminal - _ <- lineEnding - pure cs - -isHorizontalWhitespace : Char -> Bool -isHorizontalWhitespace c = any (== c) horizontalWhitespaceChars - -blankLine : PS (List Char) -blankLine = do - cs <- line - case all isHorizontalWhitespace cs of - False => throw "nonblank line" - True => pure cs - -blankLineOrEnd : PS () -blankLineOrEnd = do - Nothing <- tryMaybe blankLine - | Just _ => pure () - eof <- parseEoF - case eof of - False => throw "Expected newline or end of document" - True => pure () - -blankLines : PS () -blankLines = do - xs <- many blankLine - if length xs > 0 - then pure () - else blankLineOrEnd - ---***************************************** ---* Inline syntax * ---***************************************** - ------------------------- --- Escaped Whitespace -- ------------------------- - -hardLineBreak : PS Inline -hardLineBreak = do - _ <- thisString "\\" - _ <- spaces - _ <- lineEnding - pure $ HardLineBreak - -nbsp : PS Inline -nbsp = do - _ <- thisString "\\ " - pure $ NonBreakingSpace - -softLineBreak : PS Inline -softLineBreak = do - _ <- lineEnding - -- Check to see if the next line is empty, if it is, we are at the end of the inline - -- content, go ahead and bail - state <- save - Nothing <- tryMaybe blankLine - | Just _ => throw "End of inline" - load state - pure $ SoftLineBreak - ---------------------- --- Emphasis/Strong -- ---------------------- - ----------- --- Text -- ----------- - --- Process escape codes before processing as text -escapedText : PS Inline -escapedText = do - c <- escapedChar - pure $ Text c - --- Any non-line-ending character can be part of regular text -text : PS Inline -text = do - c <- nonTerminal - pure $ Text c - ---------------------------- --- Overall Inline Parser -- ---------------------------- - -inlineElementsNoNewlines : PS Inline -inlineElementsNoNewlines = oneOfE "" [ - nbsp - , escapedText - -- Text is last so that anything can superseed it - , text - ] - -inlineElement : PS Inline -inlineElement = oneOfE "" [ - hardLineBreak - , softLineBreak - , inlineElementsNoNewlines - ] - -inline : PS (List1 Inline) -inline = atLeastOne "Expected Inline Content" inlineElement - ---***************************************** ---* Block Syntax * ---***************************************** - ---------------- --- Paragraph -- ---------------- - -paragraph : PS Block -paragraph = do - inlines <- inline - blankLineOrEnd - pure $ Paragraph inlines - -------------- --- Heading -- -------------- - -heading : PS Block -heading = do - levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#" - ws <- atLeastOne "Expected Whitespace after header marker" $ space - case integerToHeader (natToInteger $ length levelMarker) of - Nothing => throw "Invalid header length: \{show $ length levelMarker}" - Just level => do - inlines <- inline - pure $ Heading level inlines - --------------------------- --- Overall Block Parser -- --------------------------- - -block : PS Block -block = do - -- eat up any blank lines - _ <- many blankLine - oneOfE "" [ - heading - , paragraph - ] - -blocks : PS (List Block) -blocks = many block - ---***************************************** ---* Unit Tests * ---***************************************** - -------------------------------- --- Testing Utility Functions -- -------------------------------- - --- Test a parser against a golden value with the supplied input -golden : Show a => Eq a => - (input : String) -> (reference : a) -> (parser : PS a) -> IO Bool -golden input ref parser = do - putStrLn "Input: \{input}" - putStrLn "Expected: \{show ref}" - let got = runPS parser input - case got of - Left err => do - putStrLn "Failed with error: \{err}" - pure False - Right x => do - putStrLn "Output: \{show x}" - pure $ x == ref - -inlineFromString : String -> List (Inline) -inlineFromString str with (asList str) - inlineFromString "" | [] = [] - inlineFromString (strCons c str) | (c :: x) = - Text c :: inlineFromString str | x - -inlineFromString' : String -> List1 (Inline) -inlineFromString' str = - case inlineFromString str of - [] => assert_total $ idris_crash "Bad unit test fromString" - (x :: xs) => x ::: xs - -------------------------- --- Inline Syntax Tests -- -------------------------- - --- @@test Plain Text Hello World -inlineTextSmoke : IO Bool -inlineTextSmoke = - let input = "Hello World!" in - golden input (map Text . unpack $ input) (map forget inline) - --- @@test Escaped Text -inlineEscapedSmoke : IO Bool -inlineEscapedSmoke = - let input = "Hello\\n\\*World" - ref = inlineFromString "Hello" ++ [Text '\n', Text '*'] ++ inlineFromString "World" - in golden input ref (map forget inline) - --- @@test Hard Line Break -inlineHardBreakSmoke : IO Bool -inlineHardBreakSmoke = - let input = "Hello\\\nWorld" - ref = inlineFromString "Hello" ++ [HardLineBreak] ++ inlineFromString "World" - in golden input ref (map forget inline) - --- @@test Soft Line Break -inlineSoftBreakSmoke : IO Bool -inlineSoftBreakSmoke = - let input = "Hello\nWorld" - ref = inlineFromString "Hello" ++ [SoftLineBreak] ++ inlineFromString "World" - in golden input ref (map forget inline) - --- @@test Nonbreaking Space -inlineNbspSmoke : IO Bool -inlineNbspSmoke = - let input = "Hello\\ World" - ref = inlineFromString "Hello" ++ [NonBreakingSpace] ++ inlineFromString "World" - in golden input ref (map forget inline) - ------------------------- --- Block Syntax Tests -- ------------------------- - --- @@test Paragraph -blockParagraphSmoke : IO Bool -blockParagraphSmoke = - let input = "Hello World" - ref = [Paragraph (inlineFromString' "Hello World")] - in golden input ref blocks - --- @@test Two Paragraph -blockTwoParagraphSmoke : IO Bool -blockTwoParagraphSmoke = - let input = "Hello World\n\nHello Again" - ref = [ - Paragraph (inlineFromString' "Hello World") - , Paragraph (inlineFromString' "Hello Again") - ] - in golden input ref blocks - --- @@test Level 1 heading -blockLevelOneHeadingSmoke : IO Bool -blockLevelOneHeadingSmoke = - let input = "# Level 1" - ref = [ - Heading 1 (inlineFromString' "Level 1") - ] - in golden input ref blocks - --- @@test Level 2 heading -blockLevelTwoHeadingSmoke : IO Bool -blockLevelTwoHeadingSmoke = - let input = "## Level 2" - ref = [ - Heading 2 (inlineFromString' "Level 2") - ] - in golden input ref blocks +import public SSG.Djot.Inline as SSG.Djot +import public SSG.Djot.Block as SSG.Djot diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr new file mode 100644 index 0000000..f3f8522 --- /dev/null +++ b/src/SSG/Djot/Block.idr @@ -0,0 +1,153 @@ +module SSG.Djot.Block + +import SSG.Parser.Core +import SSG.Parser.Util + +import SSG.Djot.Common +import SSG.Djot.Inline + +import Data.List1 +import Data.Vect +import Data.Nat +import Data.String + +import Control.Eff +import Derive.Prelude + +-- For iutils unit tests +import System + +%language ElabReflection + +--************** +--* Data Types * +--************** + +public export +data HeaderLevel : Type where + H1 : HeaderLevel + H2 : HeaderLevel + H3 : HeaderLevel + H4 : HeaderLevel + H5 : HeaderLevel + H6 : HeaderLevel + +%runElab derive "HeaderLevel" [Eq] + +export +Show HeaderLevel where + show H1 = "1" + show H2 = "2" + show H3 = "3" + show H4 = "4" + show H5 = "5" + show H6 = "6" + +namespace HeaderLevel + public export + integerToHeader : Integer -> Maybe HeaderLevel + integerToHeader 1 = Just H1 + integerToHeader 2 = Just H2 + integerToHeader 3 = Just H3 + integerToHeader 4 = Just H4 + integerToHeader 5 = Just H5 + integerToHeader 6 = Just H6 + integerToHeader i = Nothing + + export + fromInteger : (x : Integer) -> {auto prf : IsJust (integerToHeader x)} -> HeaderLevel + fromInteger x = fromJust $ integerToHeader x + +public export +data Block : Type where + Paragraph : (contents : List1 Inline) -> Block + Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block + +%runElab derive "Block" [Show, Eq] + +--************** +--* Syntax * +--************** + +--------------- +-- Paragraph -- +--------------- + +paragraph : PS Block +paragraph = do + inlines <- inline + blankLineOrEnd + pure $ Paragraph inlines + +------------- +-- Heading -- +------------- + +heading : PS Block +heading = do + levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#" + ws <- atLeastOne "Expected Whitespace after header marker" $ space + case integerToHeader (natToInteger $ length levelMarker) of + Nothing => throw "Invalid header length: \{show $ length levelMarker}" + Just level => do + inlines <- inline + pure $ Heading level inlines + +-------------------------- +-- Overall Block Parser -- +-------------------------- + +block : PS Block +block = do + -- eat up any blank lines + _ <- many blankLine + oneOfE "" [ + heading + , paragraph + ] + +blocks : PS (List Block) +blocks = many block + +--************** +--* Unit Tests * +--************** + +------------------------ +-- Block Syntax Tests -- +------------------------ + +-- @@test Paragraph +blockParagraphSmoke : IO Bool +blockParagraphSmoke = + let input = "Hello World" + ref = [Paragraph (inlineFromString' "Hello World")] + in golden input ref blocks + +-- @@test Two Paragraph +blockTwoParagraphSmoke : IO Bool +blockTwoParagraphSmoke = + let input = "Hello World\n\nHello Again" + ref = [ + Paragraph (inlineFromString' "Hello World") + , Paragraph (inlineFromString' "Hello Again") + ] + in golden input ref blocks + +-- @@test Level 1 heading +blockLevelOneHeadingSmoke : IO Bool +blockLevelOneHeadingSmoke = + let input = "# Level 1" + ref = [ + Heading 1 (inlineFromString' "Level 1") + ] + in golden input ref blocks + +-- @@test Level 2 heading +blockLevelTwoHeadingSmoke : IO Bool +blockLevelTwoHeadingSmoke = + let input = "## Level 2" + ref = [ + Heading 2 (inlineFromString' "Level 2") + ] + in golden input ref blocks diff --git a/src/SSG/Djot/Common.idr b/src/SSG/Djot/Common.idr new file mode 100644 index 0000000..addd20e --- /dev/null +++ b/src/SSG/Djot/Common.idr @@ -0,0 +1,151 @@ +module SSG.Djot.Common + +import SSG.Parser.Core +import SSG.Parser.Util + +import Control.Eff + +--***************************************** +--* Character Classes and String Escaping * +--***************************************** + +----------------------- +-- Character classes -- +----------------------- + +-- Class contents + +export +punctuationChars : List Char +punctuationChars = + [ + '!', '"', '#', '$', '%', '&', '\'' + , '(' , ')' , '*' , '+' , ',' , '-' + , '.' , '/' , ':' , ';' , '<' , '=' + , '>' , '?' , '@' , '[' , ']' , '^' + , '_' , '`' , '{' , '|' , '}' , '~' + ] + +export +horizontalWhitespaceChars : List Char +horizontalWhitespaceChars = + [' ', '\t'] + +export +verticalWhitespaceChars : List Char +verticalWhitespaceChars = + ['\n', '\r'] + +-- Class parsers + +export +punctuation : PS Char +punctuation = theseChars punctuationChars + +-------------- +-- Escaping -- +-------------- + +export +escapedChar : PS Char +escapedChar = do + _ <- thisString "\\" + oneOfE "Expected an escapable code" + [ punctuation + , exactReplace "n" '\n' + , exactReplace "t" '\t' + , exactReplace "r" '\r' + ] + +------------------------------------ +-- Line Qualifying And Whitespace -- +------------------------------------ + +export +space : PS Char +space = theseChars horizontalWhitespaceChars + +export +spaces : PS Nat +spaces = do + xs <- many space + pure $ length xs + +export +nonTerminal : PS Char +nonTerminal = notTheseChars verticalWhitespaceChars + +export +lineEnding : PS String +lineEnding = theseStrings ["\r\n", "\n", "\r"] + +export +terminal : PS () +terminal = do + Nothing <- tryMaybe lineEnding + | _ => pure () + test <- parseEoF + case test of + False => throw "Expected line terminal" + True => pure () + +export +line : PS (List Char) +line = do + cs <- many nonTerminal + _ <- lineEnding + pure cs + +export +isHorizontalWhitespace : Char -> Bool +isHorizontalWhitespace c = any (== c) horizontalWhitespaceChars + +export +blankLine : PS (List Char) +blankLine = do + cs <- line + case all isHorizontalWhitespace cs of + False => throw "nonblank line" + True => pure cs + +export +blankLineOrEnd : PS () +blankLineOrEnd = do + Nothing <- tryMaybe blankLine + | Just _ => pure () + eof <- parseEoF + case eof of + False => throw "Expected newline or end of document" + True => pure () + +export +blankLines : PS () +blankLines = do + xs <- many blankLine + if length xs > 0 + then pure () + else blankLineOrEnd + +--***************************************** +--* Unit Tests * +--***************************************** + +------------------------------- +-- Testing Utility Functions -- +------------------------------- + +-- Test a parser against a golden value with the supplied input +export +golden : Show a => Eq a => + (input : String) -> (reference : a) -> (parser : PS a) -> IO Bool +golden input ref parser = do + putStrLn "Input: \{input}" + putStrLn "Expected: \{show ref}" + let got = runPS parser input + case got of + Left err => do + putStrLn "Failed with error: \{err}" + pure False + Right x => do + putStrLn "Output: \{show x}" + pure $ x == ref diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr new file mode 100644 index 0000000..7573062 --- /dev/null +++ b/src/SSG/Djot/Inline.idr @@ -0,0 +1,161 @@ +module SSG.Djot.Inline + +import SSG.Parser.Core +import SSG.Parser.Util + +import SSG.Djot.Common + +import Control.Eff +import Derive.Prelude + +-- For iutils unit tests +import System + +%language ElabReflection + +--************** +--* Data Types * +--************** + +public export +data Inline : Type where + HardLineBreak : Inline + SoftLineBreak : Inline + NonBreakingSpace : Inline + Text : (c : Char) -> Inline + +%runElab derive "Inline" [Show, Eq] + +--************** +--* Syntax * +--************** + +------------------------ +-- Escaped Whitespace -- +------------------------ + +hardLineBreak : PS Inline +hardLineBreak = do + _ <- thisString "\\" + _ <- spaces + _ <- lineEnding + pure $ HardLineBreak + +nbsp : PS Inline +nbsp = do + _ <- thisString "\\ " + pure $ NonBreakingSpace + +softLineBreak : PS Inline +softLineBreak = do + _ <- lineEnding + -- Check to see if the next line is empty, if it is, we are at the end of the inline + -- content, go ahead and bail + state <- save + Nothing <- tryMaybe blankLine + | Just _ => throw "End of inline" + load state + pure $ SoftLineBreak + +--------------------- +-- Emphasis/Strong -- +--------------------- + +---------- +-- Text -- +---------- + +-- Process escape codes before processing as text +escapedText : PS Inline +escapedText = do + c <- escapedChar + pure $ Text c + +-- Any non-line-ending character can be part of regular text +text : PS Inline +text = do + c <- nonTerminal + pure $ Text c + +--------------------------- +-- Overall Inline Parser -- +--------------------------- + +inlineElementsNoNewlines : PS Inline +inlineElementsNoNewlines = oneOfE "" [ + nbsp + , escapedText + -- Text is last so that anything can superseed it + , text + ] + +inlineElement : PS Inline +inlineElement = oneOfE "" [ + hardLineBreak + , softLineBreak + , inlineElementsNoNewlines + ] + +export +inline : PS (List1 Inline) +inline = atLeastOne "Expected Inline Content" inlineElement + +--************** +--* Unit Tests * +--************** + +------------------------------- +-- Testing Utility Functions -- +------------------------------- + +export +inlineFromString : String -> List (Inline) +inlineFromString str with (asList str) + inlineFromString "" | [] = [] + inlineFromString (strCons c str) | (c :: x) = + Text c :: inlineFromString str | x + +export +inlineFromString' : String -> List1 (Inline) +inlineFromString' str = + case inlineFromString str of + [] => assert_total $ idris_crash "Bad unit test fromString" + (x :: xs) => x ::: xs + +----------- +-- Tests -- +----------- + +-- @@test Plain Text Hello World +inlineTextSmoke : IO Bool +inlineTextSmoke = + let input = "Hello World!" in + golden input (map Text . unpack $ input) (map forget inline) + +-- @@test Escaped Text +inlineEscapedSmoke : IO Bool +inlineEscapedSmoke = + let input = "Hello\\n\\*World" + ref = inlineFromString "Hello" ++ [Text '\n', Text '*'] ++ inlineFromString "World" + in golden input ref (map forget inline) + +-- @@test Hard Line Break +inlineHardBreakSmoke : IO Bool +inlineHardBreakSmoke = + let input = "Hello\\\nWorld" + ref = inlineFromString "Hello" ++ [HardLineBreak] ++ inlineFromString "World" + in golden input ref (map forget inline) + +-- @@test Soft Line Break +inlineSoftBreakSmoke : IO Bool +inlineSoftBreakSmoke = + let input = "Hello\nWorld" + ref = inlineFromString "Hello" ++ [SoftLineBreak] ++ inlineFromString "World" + in golden input ref (map forget inline) + +-- @@test Nonbreaking Space +inlineNbspSmoke : IO Bool +inlineNbspSmoke = + let input = "Hello\\ World" + ref = inlineFromString "Hello" ++ [NonBreakingSpace] ++ inlineFromString "World" + in golden input ref (map forget inline) From 2ce4579e08a16ea2ff9b8780ef24ebdb0b05b9b4 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 05:13:19 -0500 Subject: [PATCH 09/33] Basic Html Rendering --- SSG.ipkg | 2 ++ bin/Djot.ipkg | 47 +++++++++++++++++++++++++++ bin/src/Djot.idr | 21 +++++++++++++ pack.toml | 5 +++ src/SSG/Djot.idr | 13 ++++++++ src/SSG/Djot/Block.idr | 2 ++ src/SSG/Djot/Inline.idr | 12 +++---- src/SSG/Djot/Render.idr | 70 +++++++++++++++++++++++++++++++++++++++++ todo.org | 4 +-- 9 files changed, 168 insertions(+), 8 deletions(-) create mode 100644 bin/Djot.ipkg create mode 100644 bin/src/Djot.idr create mode 100644 src/SSG/Djot/Render.idr diff --git a/SSG.ipkg b/SSG.ipkg index adfdb9e..1df6058 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -14,6 +14,7 @@ authors = "Nathan McCarty" -- packages to add to search path depends = structures + , tailrec , eff , refined , elab-util @@ -25,6 +26,7 @@ modules = SSG.Parser.Core , SSG.Djot.Common , SSG.Djot.Inline , SSG.Djot.Block + , SSG.Djot.Render , SSG.HTML , SSG.HTML.ElementTypes diff --git a/bin/Djot.ipkg b/bin/Djot.ipkg new file mode 100644 index 0000000..bc3a2dc --- /dev/null +++ b/bin/Djot.ipkg @@ -0,0 +1,47 @@ +package Djot +version = 0.1.0 +authors = "Nathan McCarty" +-- maintainers = +-- license = +-- brief = +-- readme = +-- homepage = +-- sourceloc = +-- bugtracker = + +-- the Idris2 version required (e.g. langversion >= 0.5.1) +-- langversion + +-- packages to add to search path +depends = SSG + +-- modules to install +-- modules = + +-- main file (i.e. file to load at REPL) +main = Djot + +-- name of executable +executable = "djot" +-- opts = +sourcedir = "src" +-- builddir = +-- outputdir = + +-- script to run before building +-- prebuild = + +-- script to run after building +-- postbuild = + +-- script to run after building, before installing +-- preinstall = + +-- script to run after installing +-- postinstall = + +-- script to run before cleaning +-- preclean = + +-- script to run after cleaning +-- postclean = diff --git a/bin/src/Djot.idr b/bin/src/Djot.idr new file mode 100644 index 0000000..3bdfc57 --- /dev/null +++ b/bin/src/Djot.idr @@ -0,0 +1,21 @@ +module Djot + +import System +import System.File + +import SSG.Djot +import SSG.HTML + +main : IO () +main = do + args <- getArgs + case args of + [_, file] => do + Right contents <- readFile file + | Left err => printLn err + let parsed = djot contents + printLn parsed + putStr . render $ renderHtml parsed + _ => do + putStrLn "?" + exitFailure diff --git a/pack.toml b/pack.toml index eed6e77..303ca46 100644 --- a/pack.toml +++ b/pack.toml @@ -4,6 +4,11 @@ path = "." ipkg = "SSG.ipkg" test = "test/test.ipkg" +[custom.all.Djot] +type = "local" +path = "bin" +ipkg = "Djot.ipkg" + [custom.all.SSG-test] type = "local" path = "test" diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr index 274ed75..84636b1 100644 --- a/src/SSG/Djot.idr +++ b/src/SSG/Djot.idr @@ -1,4 +1,17 @@ module SSG.Djot +import SSG.Parser.Util + +import Control.Eff + import public SSG.Djot.Inline as SSG.Djot import public SSG.Djot.Block as SSG.Djot +import public SSG.Djot.Render as SSG.Djot + +export +||| Parse a djot document +djot : String -> List Block +djot str = + case runPS blocks str of + Left _ => [] + Right x => x diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index f3f8522..14cdbed 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -97,6 +97,7 @@ heading = do -- Overall Block Parser -- -------------------------- +export block : PS Block block = do -- eat up any blank lines @@ -106,6 +107,7 @@ block = do , paragraph ] +export blocks : PS (List Block) blocks = many block diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index 7573062..eed029d 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -22,7 +22,7 @@ data Inline : Type where HardLineBreak : Inline SoftLineBreak : Inline NonBreakingSpace : Inline - Text : (c : Char) -> Inline + Text : (c : String) -> Inline %runElab derive "Inline" [Show, Eq] @@ -69,13 +69,13 @@ softLineBreak = do escapedText : PS Inline escapedText = do c <- escapedChar - pure $ Text c + pure $ Text (singleton c) -- Any non-line-ending character can be part of regular text text : PS Inline text = do c <- nonTerminal - pure $ Text c + pure $ Text (singleton c) --------------------------- -- Overall Inline Parser -- @@ -113,7 +113,7 @@ inlineFromString : String -> List (Inline) inlineFromString str with (asList str) inlineFromString "" | [] = [] inlineFromString (strCons c str) | (c :: x) = - Text c :: inlineFromString str | x + Text (singleton c) :: inlineFromString str | x export inlineFromString' : String -> List1 (Inline) @@ -130,13 +130,13 @@ inlineFromString' str = inlineTextSmoke : IO Bool inlineTextSmoke = let input = "Hello World!" in - golden input (map Text . unpack $ input) (map forget inline) + golden input (map (Text . singleton) . unpack $ input) (map forget inline) -- @@test Escaped Text inlineEscapedSmoke : IO Bool inlineEscapedSmoke = let input = "Hello\\n\\*World" - ref = inlineFromString "Hello" ++ [Text '\n', Text '*'] ++ inlineFromString "World" + ref = inlineFromString "Hello" ++ [Text "\n", Text "*"] ++ inlineFromString "World" in golden input ref (map forget inline) -- @@test Hard Line Break diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr new file mode 100644 index 0000000..7bc1b06 --- /dev/null +++ b/src/SSG/Djot/Render.idr @@ -0,0 +1,70 @@ +module SSG.Djot.Render + +import SSG.HTML + +import SSG.Djot.Inline +import SSG.Djot.Block + +import Data.String +import Data.List1 + +import Structures.Dependent.DList + +export +renderInline : Inline -> (type : String ** Html type) +renderInline HardLineBreak = + (_ ** Void "br" []) +renderInline SoftLineBreak = + (_ ** Text "\n") +renderInline NonBreakingSpace = + (_ ** Text " ") +renderInline (Text c) = + (_ ** Text c) + +-- BUG: Coverage checker bug here? +partial +combineTexts : (types : List String ** DList _ Html types) + -> (types' : List String ** DList _ Html types') +combineTexts (_ ** []) = (_ ** []) +combineTexts xs@(_ ** (elem :: [])) = xs +combineTexts (_ ** Text content :: (Text str :: rest)) = + combineTexts (_ ** Text (content ++ str) :: rest) +combineTexts (_ ** Text content :: (next :: rest)) = + let (_ ** rest) = combineTexts (_ ** (next :: rest)) + in (_ ** Text content :: rest) +combineTexts (_ ** (x :: (next :: rest))) = + let (_ ** rest) = combineTexts (_ ** (next :: rest)) + in (_ ** x :: rest) + +export +renderInlines : List Inline -> (types : List String ** DList _ Html types) +renderInlines xs = assert_total $ + combineTexts . fromList . map renderInline $ xs + +headingLevel : HeaderLevel -> (h : String ** IsNormal h) +headingLevel H1 = ("h1" ** IsH1) +headingLevel H2 = ("h2" ** IsH2) +headingLevel H3 = ("h3" ** IsH3) +headingLevel H4 = ("h4" ** IsH4) +headingLevel H5 = ("h5" ** IsH5) +headingLevel H6 = ("h6" ** IsH6) + +export +renderBlock : Block -> (type : String ** Html type) +renderBlock (Paragraph contents) = + let (_ ** xs) = renderInlines $ forget contents + in (_ ** Normal "p" [] xs) +renderBlock (Heading level contents) = + let (_ ** xs) = renderInlines $ forget contents + (level ** _ ) = headingLevel level + in (_ ** Normal level [] xs) + +export +renderBlocks : List Block -> (types : List String ** DList _ Html types) +renderBlocks xs = fromList $ map renderBlock xs + +export +renderHtml : List Block -> Html "html" +renderHtml xs = + let (_ ** xs) = renderBlocks xs + in Normal "html" ["lang" =$ "en"] xs diff --git a/todo.org b/todo.org index aad08f1..bb2b3c9 100644 --- a/todo.org +++ b/todo.org @@ -8,7 +8,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [4/42] +* Djot [5/42] :PROPERTIES: :COOKIE_DATA: recursive :END: @@ -50,7 +50,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Footnote **** TODO Block attributes **** TODO Links to headings -** TODO Rendering +** DONE Rendering ** TODO Predictive parsing ** TODO Support all types of whitespace *** TODO Escaping From d1e1dd5f59844b66b45ad7d7d1faad588ef7bad5 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 05:40:02 -0500 Subject: [PATCH 10/33] Post process inline parsing --- src/SSG/Djot/Inline.idr | 82 ++++++++++++++++++++++++++++++----------- src/SSG/Djot/Render.idr | 19 +--------- 2 files changed, 62 insertions(+), 39 deletions(-) diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index eed029d..19b07ed 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -6,6 +6,7 @@ import SSG.Parser.Util import SSG.Djot.Common import Control.Eff +import Control.Monad.Eval import Derive.Prelude -- For iutils unit tests @@ -13,9 +14,9 @@ import System %language ElabReflection ---************** ---* Data Types * ---************** +--****************** +--* Data Types * +--****************** public export data Inline : Type where @@ -26,9 +27,51 @@ data Inline : Type where %runElab derive "Inline" [Show, Eq] ---************** ---* Syntax * ---************** +--****************** +--* PostProcessing * +--****************** + +-- Combine adjacent `Text`s in the parsed output +combineTexts : List1 Inline -> Eval (List1 Inline) +combineTexts xs@(Text c ::: []) = pure xs +combineTexts (Text c ::: (Text d :: xs)) = + combineTexts (Text (c ++ d) ::: xs) +combineTexts (x ::: tail) = do + rest <- combineTexts' tail + pure $ x ::: rest + where + combineTexts' : List Inline -> Eval (List Inline) + combineTexts' [] = pure [] + combineTexts' (y :: []) = pure [y] + combineTexts' (Text c :: (Text d :: xs)) = + combineTexts' (Text (c ++ d) :: xs) + combineTexts' (y :: ys) = do + rest <- combineTexts' ys + pure $ y :: rest + +-- Remove a trailing soft line break from a list of inlines +removeTrailingSoftBreak : List1 Inline -> Eval (List1 Inline) +removeTrailingSoftBreak (head ::: tail) = do + tail <- inner tail + pure $ head ::: tail + where + inner : List Inline -> Eval (List Inline) + inner [] = pure [] + inner (SoftLineBreak :: []) = pure [] + inner (x :: xs) = do + xs <- inner xs + pure $ x :: xs + +-- Combine all post processing steps +postProcess : List1 Inline -> List1 Inline +postProcess xs = eval $ do + xs <- combineTexts xs + xs <- removeTrailingSoftBreak xs + pure xs + +--****************** +--* Syntax * +--****************** ------------------------ -- Escaped Whitespace -- @@ -98,30 +141,25 @@ inlineElement = oneOfE "" [ export inline : PS (List1 Inline) -inline = atLeastOne "Expected Inline Content" inlineElement +inline = map postProcess $ + atLeastOne "Expected Inline Content" inlineElement ---************** ---* Unit Tests * ---************** +--****************** +--* Unit Tests * +--****************** ------------------------------- -- Testing Utility Functions -- ------------------------------- -export -inlineFromString : String -> List (Inline) -inlineFromString str with (asList str) - inlineFromString "" | [] = [] - inlineFromString (strCons c str) | (c :: x) = - Text (singleton c) :: inlineFromString str | x export inlineFromString' : String -> List1 (Inline) -inlineFromString' str = - case inlineFromString str of - [] => assert_total $ idris_crash "Bad unit test fromString" - (x :: xs) => x ::: xs +inlineFromString' str = Text str ::: [] +export +inlineFromString : String -> List (Inline) +inlineFromString = forget . inlineFromString' ----------- -- Tests -- ----------- @@ -130,13 +168,13 @@ inlineFromString' str = inlineTextSmoke : IO Bool inlineTextSmoke = let input = "Hello World!" in - golden input (map (Text . singleton) . unpack $ input) (map forget inline) + golden input (inlineFromString input) (map forget inline) -- @@test Escaped Text inlineEscapedSmoke : IO Bool inlineEscapedSmoke = let input = "Hello\\n\\*World" - ref = inlineFromString "Hello" ++ [Text "\n", Text "*"] ++ inlineFromString "World" + ref = inlineFromString "Hello\n*World" in golden input ref (map forget inline) -- @@test Hard Line Break diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index 7bc1b06..4daf1ce 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -21,25 +21,10 @@ renderInline NonBreakingSpace = renderInline (Text c) = (_ ** Text c) --- BUG: Coverage checker bug here? -partial -combineTexts : (types : List String ** DList _ Html types) - -> (types' : List String ** DList _ Html types') -combineTexts (_ ** []) = (_ ** []) -combineTexts xs@(_ ** (elem :: [])) = xs -combineTexts (_ ** Text content :: (Text str :: rest)) = - combineTexts (_ ** Text (content ++ str) :: rest) -combineTexts (_ ** Text content :: (next :: rest)) = - let (_ ** rest) = combineTexts (_ ** (next :: rest)) - in (_ ** Text content :: rest) -combineTexts (_ ** (x :: (next :: rest))) = - let (_ ** rest) = combineTexts (_ ** (next :: rest)) - in (_ ** x :: rest) - export renderInlines : List Inline -> (types : List String ** DList _ Html types) -renderInlines xs = assert_total $ - combineTexts . fromList . map renderInline $ xs +renderInlines xs = + fromList . map renderInline $ xs headingLevel : HeaderLevel -> (h : String ** IsNormal h) headingLevel H1 = ("h1" ** IsH1) From c11bf35cc8f081b7fc763d2afb65b00cc68e8d14 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 05:42:04 -0500 Subject: [PATCH 11/33] Fix misssing indend in html void tag generation --- src/SSG/HTML.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/SSG/HTML.idr b/src/SSG/HTML.idr index 4262e4e..ebfde18 100644 --- a/src/SSG/HTML.idr +++ b/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 From 67a07a0523a4e55553bf15a149aef89e3b49e812 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 05:43:34 -0500 Subject: [PATCH 12/33] Don't generate trailing slash for void tags --- src/SSG/HTML.idr | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/SSG/HTML.idr b/src/SSG/HTML.idr index ebfde18..7e9a481 100644 --- a/src/SSG/HTML.idr +++ b/src/SSG/HTML.idr @@ -63,8 +63,8 @@ namespace Html if length attributes > 0 then let attrs = joinBy " " $ map toString attributes - in "\{indent}<\{type} \{attrs} />" - else "\{indent}<\{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 From 72418a0b8897e9a365ca5e119b5c7f2be023a3c4 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 05:47:46 -0500 Subject: [PATCH 13/33] Fix softbreak rendering --- src/SSG/Djot/Render.idr | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index 4daf1ce..bffca50 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -7,24 +7,27 @@ import SSG.Djot.Block import Data.String import Data.List1 +import Data.List import Structures.Dependent.DList +-- Maybe because specifically Soft line breaks don't generate any html of their +-- own export -renderInline : Inline -> (type : String ** Html type) +renderInline : Inline -> Maybe (type : String ** Html type) renderInline HardLineBreak = - (_ ** Void "br" []) + Just (_ ** Void "br" []) renderInline SoftLineBreak = - (_ ** Text "\n") + Nothing renderInline NonBreakingSpace = - (_ ** Text " ") + Just (_ ** Text " ") renderInline (Text c) = - (_ ** Text c) + Just (_ ** Text c) export renderInlines : List Inline -> (types : List String ** DList _ Html types) renderInlines xs = - fromList . map renderInline $ xs + fromList . catMaybes . map renderInline $ xs headingLevel : HeaderLevel -> (h : String ** IsNormal h) headingLevel H1 = ("h1" ** IsH1) From 4e83ca8d483bfd62e360c6b6250e5bacb9fc114b Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 05:51:26 -0500 Subject: [PATCH 14/33] Todos --- todo.org | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/todo.org b/todo.org index bb2b3c9..bc61011 100644 --- a/todo.org +++ b/todo.org @@ -2,6 +2,7 @@ ** 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= ** NO Move =Raw= out of =Tag= Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make sense * Parser Core @@ -14,7 +15,6 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se :END: ** Parsing *** Inline Syntax [2/18] -**** DONE Ordinary Text **** TODO Link **** TODO Image **** TODO Autolink @@ -26,14 +26,14 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Smart punctuation **** TODO Math **** TODO Footnote reference -**** DONE Linebreak **** TODO Comment **** TODO Symbols **** TODO Raw inline **** TODO Span **** TODO Inline attributes +**** DONE Ordinary Text +**** DONE Linebreak *** Block Syntax [2/16] -**** DONE Paragraph **** Heading ***** TODO Multiline without leading count ***** DONE Basic @@ -50,7 +50,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Footnote **** TODO Block attributes **** TODO Links to headings -** DONE Rendering +**** DONE Paragraph ** TODO Predictive parsing ** TODO Support all types of whitespace *** TODO Escaping @@ -58,3 +58,4 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO hex escapes ** TODO GFM style alerts ** TODO Group adjacent =Text=s into a =String= +** DONE Rendering From 72b102d071793425af62636d96221a0c92c21e85 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 15:29:25 -0500 Subject: [PATCH 15/33] Setup golden value testing --- .gitignore | 2 ++ src/SSG/Djot/Render.idr | 3 ++- test/Main.idr | 8 ++++++++ test/djot-to-html/001-hello-world/Main.idr | 16 ++++++++++++++++ test/djot-to-html/001-hello-world/expected | 6 ++++++ test/djot-to-html/001-hello-world/run | 6 ++++++ test/djot-to-html/001-hello-world/test.dj | 1 + test/djot-to-html/001-hello-world/test.ipkg | 7 +++++++ test/src/Main.idr | 4 ---- test/test.ipkg | 3 ++- 10 files changed, 50 insertions(+), 6 deletions(-) create mode 100644 test/Main.idr create mode 100644 test/djot-to-html/001-hello-world/Main.idr create mode 100644 test/djot-to-html/001-hello-world/expected create mode 100644 test/djot-to-html/001-hello-world/run create mode 100644 test/djot-to-html/001-hello-world/test.dj create mode 100644 test/djot-to-html/001-hello-world/test.ipkg delete mode 100644 test/src/Main.idr diff --git a/.gitignore b/.gitignore index 2784b39..87db7aa 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,4 @@ build/ *.*~ +test/failures +test/*/*/output diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index bffca50..d9a4a58 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -55,4 +55,5 @@ export renderHtml : List Block -> Html "html" renderHtml xs = let (_ ** xs) = renderBlocks xs - in Normal "html" ["lang" =$ "en"] xs + in Normal "html" ["lang" =$ "en"] + [ Normal "body" [] xs ] diff --git a/test/Main.idr b/test/Main.idr new file mode 100644 index 0000000..0437780 --- /dev/null +++ b/test/Main.idr @@ -0,0 +1,8 @@ +module Main + +import Test.Golden.RunnerHelper + +main : IO () +main = goldenRunner + [ "Djot -> HTML Golden Values" `atDir` "djot-to-html" + ] diff --git a/test/djot-to-html/001-hello-world/Main.idr b/test/djot-to-html/001-hello-world/Main.idr new file mode 100644 index 0000000..97d8771 --- /dev/null +++ b/test/djot-to-html/001-hello-world/Main.idr @@ -0,0 +1,16 @@ +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 parsed = djot contents + putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/001-hello-world/expected b/test/djot-to-html/001-hello-world/expected new file mode 100644 index 0000000..130955a --- /dev/null +++ b/test/djot-to-html/001-hello-world/expected @@ -0,0 +1,6 @@ + + + +

Hello World!

+ + \ No newline at end of file diff --git a/test/djot-to-html/001-hello-world/run b/test/djot-to-html/001-hello-world/run new file mode 100644 index 0000000..6b5ab53 --- /dev/null +++ b/test/djot-to-html/001-hello-world/run @@ -0,0 +1,6 @@ +rm -rf build/ + +flock "$1" pack -q install-deps test.ipkg +pack -q run test.ipkg + +rm -rf build/ diff --git a/test/djot-to-html/001-hello-world/test.dj b/test/djot-to-html/001-hello-world/test.dj new file mode 100644 index 0000000..980a0d5 --- /dev/null +++ b/test/djot-to-html/001-hello-world/test.dj @@ -0,0 +1 @@ +Hello World! diff --git a/test/djot-to-html/001-hello-world/test.ipkg b/test/djot-to-html/001-hello-world/test.ipkg new file mode 100644 index 0000000..0efef9e --- /dev/null +++ b/test/djot-to-html/001-hello-world/test.ipkg @@ -0,0 +1,7 @@ +package a-test + +depends = SSG + +main = Main + +executable = test diff --git a/test/src/Main.idr b/test/src/Main.idr deleted file mode 100644 index 1047866..0000000 --- a/test/src/Main.idr +++ /dev/null @@ -1,4 +0,0 @@ -module Main - -main : IO () -main = putStrLn "Test successful!" diff --git a/test/test.ipkg b/test/test.ipkg index 81f240b..b1e7e47 100644 --- a/test/test.ipkg +++ b/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 = From 85ead54619a5007474496ec14786a842551639e8 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 16:17:31 -0500 Subject: [PATCH 16/33] Test linebreaks and nbsps --- src/SSG/Djot/Inline.idr | 46 +++++++++++++++---- src/SSG/Djot/Render.idr | 20 +++++++- .../002-linebreaks-and-nbsp/Main.idr | 16 +++++++ .../002-linebreaks-and-nbsp/expected | 26 +++++++++++ test/djot-to-html/002-linebreaks-and-nbsp/run | 6 +++ .../002-linebreaks-and-nbsp/test.dj | 22 +++++++++ .../002-linebreaks-and-nbsp/test.ipkg | 7 +++ 7 files changed, 132 insertions(+), 11 deletions(-) create mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/Main.idr create mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/expected create mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/run create mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/test.dj create mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/test.ipkg diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index 19b07ed..824221a 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -33,7 +33,6 @@ data Inline : Type where -- Combine adjacent `Text`s in the parsed output combineTexts : List1 Inline -> Eval (List1 Inline) -combineTexts xs@(Text c ::: []) = pure xs combineTexts (Text c ::: (Text d :: xs)) = combineTexts (Text (c ++ d) ::: xs) combineTexts (x ::: tail) = do @@ -49,6 +48,23 @@ combineTexts (x ::: tail) = do rest <- combineTexts' ys pure $ y :: rest +-- Combine adjacent soft line breaks into one +combineSoftBreaks : List1 Inline -> Eval (List1 Inline) +combineSoftBreaks (SoftLineBreak ::: (SoftLineBreak :: xs)) = + combineSoftBreaks (SoftLineBreak ::: xs) +combineSoftBreaks (head ::: tail) = do + tail <- combineSoftBreaks' tail + pure $ head ::: tail + where + combineSoftBreaks' : List Inline -> Eval (List Inline) + combineSoftBreaks' [] = pure [] + combineSoftBreaks' (x :: []) = pure [x] + combineSoftBreaks' (SoftLineBreak :: (SoftLineBreak :: xs)) = + combineSoftBreaks' (SoftLineBreak :: xs) + combineSoftBreaks' (x :: xs) = do + rest <- combineSoftBreaks' xs + pure $ x :: rest + -- Remove a trailing soft line break from a list of inlines removeTrailingSoftBreak : List1 Inline -> Eval (List1 Inline) removeTrailingSoftBreak (head ::: tail) = do @@ -66,6 +82,7 @@ removeTrailingSoftBreak (head ::: tail) = do postProcess : List1 Inline -> List1 Inline postProcess xs = eval $ do xs <- combineTexts xs + xs <- combineSoftBreaks xs xs <- removeTrailingSoftBreak xs pure xs @@ -91,6 +108,8 @@ nbsp = do softLineBreak : PS Inline softLineBreak = do + -- Slurp up any horizontal whitespace before the line break + _ <- spaces _ <- lineEnding -- Check to see if the next line is empty, if it is, we are at the end of the inline -- content, go ahead and bail @@ -98,6 +117,17 @@ softLineBreak = do Nothing <- tryMaybe blankLine | Just _ => throw "End of inline" load state + -- Slurp up any horizontal whitespace after the line break + _ <- spaces + pure $ SoftLineBreak + +escapedNewLine : PS Inline +escapedNewLine = do + -- Slurp up any horizontal whitespace before the line break + _ <- spaces + _ <- thisString "\\n" + -- Slurp up any horizontal whitespace after the line break + _ <- spaces pure $ SoftLineBreak --------------------- @@ -124,19 +154,15 @@ text = do -- Overall Inline Parser -- --------------------------- -inlineElementsNoNewlines : PS Inline -inlineElementsNoNewlines = oneOfE "" [ - nbsp - , escapedText - -- Text is last so that anything can superseed it - , text - ] - inlineElement : PS Inline inlineElement = oneOfE "" [ hardLineBreak , softLineBreak - , inlineElementsNoNewlines + , escapedNewLine + , nbsp + , escapedText + -- Text is last so that anything can superseed it + , text ] export diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index d9a4a58..b218f6b 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -9,6 +9,7 @@ import Data.String import Data.List1 import Data.List +import Control.Monad.Eval import Structures.Dependent.DList -- Maybe because specifically Soft line breaks don't generate any html of their @@ -24,10 +25,27 @@ renderInline NonBreakingSpace = renderInline (Text c) = Just (_ ** Text c) +combineTexts : (types : List String ** DList _ Html types) + -> Eval (types : List String ** DList _ Html types) +combineTexts (_ ** []) = pure (_ ** []) +-- We do a little bit of magic insert of whitespace, so we have some special handling for +-- nbsps to not insert spaces around them +combineTexts (_ ** (Text c :: Text " " :: Text " " :: rest)) = + combineTexts (_ ** Text (c ++ " ") :: Text " " :: rest) +combineTexts (_ ** (Text c :: Text " " :: Text d :: rest)) = + combineTexts (_ ** Text (c ++ " " ++ d) :: rest) +combineTexts (_ ** (Text c :: Text " " :: rest)) = + combineTexts (_ ** Text (c ++ " ") :: rest) +combineTexts (_ ** (Text c :: Text d :: rest)) = + combineTexts (_ ** Text (c ++ " " ++ d) :: rest) +combineTexts (_ ** (elem :: rest)) = do + (_ ** rest) <- combineTexts (_ ** rest) + pure $ (_ ** elem :: rest) + export renderInlines : List Inline -> (types : List String ** DList _ Html types) renderInlines xs = - fromList . catMaybes . map renderInline $ xs + eval . combineTexts . fromList . catMaybes . map renderInline $ xs headingLevel : HeaderLevel -> (h : String ** IsNormal h) headingLevel H1 = ("h1" ** IsH1) diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/Main.idr b/test/djot-to-html/002-linebreaks-and-nbsp/Main.idr new file mode 100644 index 0000000..97d8771 --- /dev/null +++ b/test/djot-to-html/002-linebreaks-and-nbsp/Main.idr @@ -0,0 +1,16 @@ +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 parsed = djot contents + putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/expected b/test/djot-to-html/002-linebreaks-and-nbsp/expected new file mode 100644 index 0000000..d344ee1 --- /dev/null +++ b/test/djot-to-html/002-linebreaks-and-nbsp/expected @@ -0,0 +1,26 @@ + + + +

A paragraph with a normal newline in the middle of it

+

+ A paragraph with a hard line break +
+ in the middle of it +

+

+ A paragraph with a hard line break +
+ in the middle of it with extra spaces +

+

+ A paragraph with a hard line break +
+ in the middle of it with no spaces +

+

A paragraph with an explicit soft line break in the middle of it

+

Multiple soft breaks should coalesce into one

+

Same should apply when mixing explicit and implied soft breaks

+

An escaped space should render as a nonbreaking space

+

We also want to test  multiple   nonbreaking    spaces     in a row

+ + \ No newline at end of file diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/run b/test/djot-to-html/002-linebreaks-and-nbsp/run new file mode 100644 index 0000000..6b5ab53 --- /dev/null +++ b/test/djot-to-html/002-linebreaks-and-nbsp/run @@ -0,0 +1,6 @@ +rm -rf build/ + +flock "$1" pack -q install-deps test.ipkg +pack -q run test.ipkg + +rm -rf build/ diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/test.dj b/test/djot-to-html/002-linebreaks-and-nbsp/test.dj new file mode 100644 index 0000000..24e3421 --- /dev/null +++ b/test/djot-to-html/002-linebreaks-and-nbsp/test.dj @@ -0,0 +1,22 @@ +A paragraph with a normal newline +in the middle of it + +A paragraph with a hard line break \ +in the middle of it + +A paragraph with a hard line break \ +in the middle of it with extra spaces + +A paragraph with a hard line break \ +in the middle of it with no spaces + +A paragraph with an explicit soft line break \n in the middle of it + +Multiple soft breaks should coalesce \n\n\n into one + +Same should apply when mixing explicit \n +and implied soft breaks + +An escaped space\ should render as a nonbreaking space + +We also want to test\ \ multiple\ \ \ nonbreaking\ \ \ \ spaces\ \ \ \ \ in a row diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/test.ipkg b/test/djot-to-html/002-linebreaks-and-nbsp/test.ipkg new file mode 100644 index 0000000..0efef9e --- /dev/null +++ b/test/djot-to-html/002-linebreaks-and-nbsp/test.ipkg @@ -0,0 +1,7 @@ +package a-test + +depends = SSG + +main = Main + +executable = test From 68928aeb20ea4f283ab31b4604ea953c0d0e6afd Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 16:23:02 -0500 Subject: [PATCH 17/33] Test Headings --- test/djot-to-html/003-headings/Main.idr | 16 ++++++++++++++ test/djot-to-html/003-headings/expected | 19 ++++++++++++++++ test/djot-to-html/003-headings/run | 6 +++++ test/djot-to-html/003-headings/test.dj | 28 ++++++++++++++++++++++++ test/djot-to-html/003-headings/test.ipkg | 7 ++++++ 5 files changed, 76 insertions(+) create mode 100644 test/djot-to-html/003-headings/Main.idr create mode 100644 test/djot-to-html/003-headings/expected create mode 100644 test/djot-to-html/003-headings/run create mode 100644 test/djot-to-html/003-headings/test.dj create mode 100644 test/djot-to-html/003-headings/test.ipkg diff --git a/test/djot-to-html/003-headings/Main.idr b/test/djot-to-html/003-headings/Main.idr new file mode 100644 index 0000000..97d8771 --- /dev/null +++ b/test/djot-to-html/003-headings/Main.idr @@ -0,0 +1,16 @@ +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 parsed = djot contents + putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/003-headings/expected b/test/djot-to-html/003-headings/expected new file mode 100644 index 0000000..f281872 --- /dev/null +++ b/test/djot-to-html/003-headings/expected @@ -0,0 +1,19 @@ + + + +

Level 1 Heading

+

Level 2 Heading

+

Level 3 Heading

+

Level 4 Heading

+
Level 5 Heading
+
Level 6 Heading
+

####### Level 7 Not a Heading

+

A heading that spans multiple lines

+

Heading

+

Some content

+

A sub heading

+

Even more content

+

Back up

+

Some final content

+ + \ No newline at end of file diff --git a/test/djot-to-html/003-headings/run b/test/djot-to-html/003-headings/run new file mode 100644 index 0000000..6b5ab53 --- /dev/null +++ b/test/djot-to-html/003-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/ diff --git a/test/djot-to-html/003-headings/test.dj b/test/djot-to-html/003-headings/test.dj new file mode 100644 index 0000000..e43c08b --- /dev/null +++ b/test/djot-to-html/003-headings/test.dj @@ -0,0 +1,28 @@ +# Level 1 Heading + +## Level 2 Heading + +### Level 3 Heading + +#### Level 4 Heading + +##### Level 5 Heading + +###### Level 6 Heading + +####### Level 7 Not a Heading + +# A heading that +spans multiple lines + +# Heading + +Some content + +## A sub heading + +Even more content + +# Back up + +Some final content diff --git a/test/djot-to-html/003-headings/test.ipkg b/test/djot-to-html/003-headings/test.ipkg new file mode 100644 index 0000000..0efef9e --- /dev/null +++ b/test/djot-to-html/003-headings/test.ipkg @@ -0,0 +1,7 @@ +package a-test + +depends = SSG + +main = Main + +executable = test From f54df1d2a457fe58b84f17c76d11f91997e8bd87 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 16:34:41 -0500 Subject: [PATCH 18/33] Pretty print internal representation in Djot utility --- SSG.ipkg | 2 ++ bin/src/Djot.idr | 8 +++++++- src/SSG/Djot/Block.idr | 6 ++++-- src/SSG/Djot/Inline.idr | 3 ++- 4 files changed, 15 insertions(+), 4 deletions(-) diff --git a/SSG.ipkg b/SSG.ipkg index 1df6058..ec92d59 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -18,6 +18,8 @@ depends = structures , eff , refined , elab-util + , elab-pretty + , prettier -- modules to install modules = SSG.Parser.Core diff --git a/bin/src/Djot.idr b/bin/src/Djot.idr index 3bdfc57..85a0767 100644 --- a/bin/src/Djot.idr +++ b/bin/src/Djot.idr @@ -6,6 +6,8 @@ import System.File import SSG.Djot import SSG.HTML +import Text.PrettyPrint.Bernardy + main : IO () main = do args <- getArgs @@ -14,8 +16,12 @@ main = do Right contents <- readFile file | Left err => printLn err let parsed = djot contents - printLn parsed putStr . render $ renderHtml parsed + [_, "raw", file] => do + Right contents <- readFile file + | Left err => printLn err + let parsed = djot contents + putStrLn . Doc.render (Opts 80) $ pretty parsed _ => do putStrLn "?" exitFailure diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index 14cdbed..067feb0 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -13,6 +13,7 @@ import Data.String import Control.Eff import Derive.Prelude +import Derive.Pretty -- For iutils unit tests import System @@ -32,7 +33,7 @@ data HeaderLevel : Type where H5 : HeaderLevel H6 : HeaderLevel -%runElab derive "HeaderLevel" [Eq] +%runElab derive "HeaderLevel" [Eq, Pretty] export Show HeaderLevel where @@ -63,7 +64,8 @@ data Block : Type where Paragraph : (contents : List1 Inline) -> Block Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block -%runElab derive "Block" [Show, Eq] +%runElab derive "List1" [Pretty] +%runElab derive "Block" [Show, Eq, Pretty] --************** --* Syntax * diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index 824221a..f5db77f 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -8,6 +8,7 @@ import SSG.Djot.Common import Control.Eff import Control.Monad.Eval import Derive.Prelude +import Derive.Pretty -- For iutils unit tests import System @@ -25,7 +26,7 @@ data Inline : Type where NonBreakingSpace : Inline Text : (c : String) -> Inline -%runElab derive "Inline" [Show, Eq] +%runElab derive "Inline" [Show, Eq, Pretty] --****************** --* PostProcessing * From fe239e287bf6ed224ca19f4a3f10d4f862c38397 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 20:36:04 -0500 Subject: [PATCH 19/33] Handle Multiline headings properly --- src/SSG/Djot/Block.idr | 84 ++++++++++++++++++++++--- src/SSG/Djot/Common.idr | 9 +++ src/SSG/Djot/Inline.idr | 2 +- src/SSG/Parser/Util.idr | 10 +++ test/djot-to-html/003-headings/expected | 8 +++ test/djot-to-html/003-headings/test.dj | 24 +++++++ todo.org | 10 +-- 7 files changed, 131 insertions(+), 16 deletions(-) diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index 067feb0..273f481 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -20,9 +20,9 @@ import System %language ElabReflection ---************** ---* Data Types * ---************** +--***************** +--* Data Types * +--***************** public export data HeaderLevel : Type where @@ -67,9 +67,27 @@ data Block : Type where %runElab derive "List1" [Pretty] %runElab derive "Block" [Show, Eq, Pretty] ---************** ---* Syntax * ---************** +--***************** +--* Parsing Utils * +--***************** + +-- Parse a prefixed line, stripping the prefix +prefixedLine : (pfx : PS b) -> PS String +prefixedLine pfx = do + _ <- pfx + cs <- nonBlankLine + pure $ pack cs + +-- Parses a block prefixed by the given character string with the given parser +parsePrefixedBlock : (pfx : PS b) -> (parser : PS a) -> PS a +parsePrefixedBlock pfx parser = do + lines <- atLeastOne "No lines in block" $ prefixedLine pfx + let block = joinBy "\n" . forget $ lines + runPS' parser block + +--***************** +--* Syntax * +--***************** --------------- -- Paragraph -- @@ -85,14 +103,42 @@ paragraph = do -- Heading -- ------------- +headingPrefix : (level : Nat) -> PS String +headingPrefix level = oneOfE "" [notPrefixP, prefixP] + where + notPrefixed : PS () + notPrefixed = do + -- peek the first character to check and see if its a heading marker + Just [first] <- peek 1 + | _ => throw "End of File" + case first of + '#' => throw "Header prefix" + _ => pure () + notPrefixP : PS String + notPrefixP = do + notPrefixed + map pack $ many space + prefixP : PS String + prefixP = do + levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#" + ws <- atLeastOne "Expected Whitespace after header marker" $ space + case length levelMarker == level of + False => throw "Mismatched levels" + True => pure $ (concat . forget $ levelMarker) ++ (pack . forget $ ws) + heading : PS Block heading = do + -- peek the level marker, then parse as a prefixed block + state <- save levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#" ws <- atLeastOne "Expected Whitespace after header marker" $ space case integerToHeader (natToInteger $ length levelMarker) of Nothing => throw "Invalid header length: \{show $ length levelMarker}" Just level => do - inlines <- inline + load state + inlines <- parsePrefixedBlock (headingPrefix (length levelMarker)) inline + -- djot demands a blank line or the end of file after a heading + _ <- blankLineOrEnd pure $ Heading level inlines -------------------------- @@ -113,9 +159,9 @@ export blocks : PS (List Block) blocks = many block ---************** ---* Unit Tests * ---************** +--***************** +--* Unit Tests * +--***************** ------------------------ -- Block Syntax Tests -- @@ -155,3 +201,21 @@ blockLevelTwoHeadingSmoke = Heading 2 (inlineFromString' "Level 2") ] in golden input ref blocks + +-- @@test Multiline prefixed headings +blockMultilinePrefixed : IO Bool +blockMultilinePrefixed = + let input = "# Level 1\n# More text" + ref = [ + Heading 1 (Text "Level 1" ::: [SoftLineBreak, Text "More text"]) + ] + in golden input ref blocks + +-- @@test Multiline unprefixed headings +blockMultilineUnprefixed : IO Bool +blockMultilineUnprefixed = + let input = "# Level 1\nMore text" + ref = [ + Heading 1 (Text "Level 1" ::: [SoftLineBreak, Text "More text"]) + ] + in golden input ref blocks diff --git a/src/SSG/Djot/Common.idr b/src/SSG/Djot/Common.idr index addd20e..8f8b71b 100644 --- a/src/SSG/Djot/Common.idr +++ b/src/SSG/Djot/Common.idr @@ -108,6 +108,15 @@ blankLine = do False => throw "nonblank line" True => pure cs +export +nonBlankLine : PS (List Char) +nonBlankLine = do + cs <- many nonTerminal + _ <- terminal + case all isHorizontalWhitespace cs of + True => throw "blank line" + False => pure cs + export blankLineOrEnd : PS () blankLineOrEnd = do diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index f5db77f..66a0ee9 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -201,7 +201,7 @@ inlineTextSmoke = inlineEscapedSmoke : IO Bool inlineEscapedSmoke = let input = "Hello\\n\\*World" - ref = inlineFromString "Hello\n*World" + ref = [Text "Hello", SoftLineBreak, Text "*World"] in golden input ref (map forget inline) -- @@test Hard Line Break diff --git a/src/SSG/Parser/Util.idr b/src/SSG/Parser/Util.idr index a195236..4777f7b 100644 --- a/src/SSG/Parser/Util.idr +++ b/src/SSG/Parser/Util.idr @@ -4,6 +4,7 @@ import SSG.Parser.Core import Data.List1 import Data.Vect +import Data.String import Control.Eff ||| Type alias for parsing errors @@ -22,6 +23,15 @@ runPS : PS a -> (str : String) -> Either String a runPS x str = fst . extract . runParser str . runExcept $ x +||| Run a parser, extracting the parsed value, and throwing an error if the parse was not +||| complete or if it failed +export +runPS' : PS a -> (str : String) -> PS a +runPS' x str = do + (res, rest) <- lift . runParser str . runExcept $ x + unless (null rest) $ throw "Incomplete parse" + rethrow res + ||| Attempt to run a fallible parser, backtracking on failure export try : (f : PS a) -> (err : ParseError -> PS a) -> PS a diff --git a/test/djot-to-html/003-headings/expected b/test/djot-to-html/003-headings/expected index f281872..91f7ee8 100644 --- a/test/djot-to-html/003-headings/expected +++ b/test/djot-to-html/003-headings/expected @@ -15,5 +15,13 @@

Even more content

Back up

Some final content

+

A Multiline Heading

+

A Level 2 Multiline Heading

+

## Heading ### Not a heading

+

### Heading ## Not a heading

+

A Multiline Heading

+

A Level 2 Multiline Heading

+

A Multiline Heading

+

A Level 2 Multiline Heading

\ No newline at end of file diff --git a/test/djot-to-html/003-headings/test.dj b/test/djot-to-html/003-headings/test.dj index e43c08b..d6eb8ec 100644 --- a/test/djot-to-html/003-headings/test.dj +++ b/test/djot-to-html/003-headings/test.dj @@ -26,3 +26,27 @@ Even more content # Back up Some final content + +# A Multiline +# Heading + +## A Level 2 +## Multiline Heading + +## Heading +### Not a heading + +### Heading +## Not a heading + +# A Multiline +Heading + +## A Level 2 +Multiline Heading + +# A Multiline + Heading + +## A Level 2 + Multiline Heading diff --git a/todo.org b/todo.org index bc61011..d263555 100644 --- a/todo.org +++ b/todo.org @@ -9,7 +9,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [5/42] +* Djot [7/43] :PROPERTIES: :COOKIE_DATA: recursive :END: @@ -33,10 +33,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Inline attributes **** DONE Ordinary Text **** DONE Linebreak -*** Block Syntax [2/16] -**** Heading -***** TODO Multiline without leading count -***** DONE Basic +*** Block Syntax [4/17] **** TODO Block quote **** TODO List item **** TODO List @@ -51,6 +48,9 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Block attributes **** TODO Links to headings **** DONE Paragraph +**** DONE Heading +***** DONE Multiline without leading count +***** DONE Basic ** TODO Predictive parsing ** TODO Support all types of whitespace *** TODO Escaping From 75a21b8da69067ea88c021ea210320631d9f5ede Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 21 Feb 2025 23:27:18 -0500 Subject: [PATCH 20/33] Move djot binary --- bin/Djot.ipkg => Djot.ipkg | 0 pack.toml | 2 +- {bin/src => src}/Djot.idr | 0 3 files changed, 1 insertion(+), 1 deletion(-) rename bin/Djot.ipkg => Djot.ipkg (100%) rename {bin/src => src}/Djot.idr (100%) diff --git a/bin/Djot.ipkg b/Djot.ipkg similarity index 100% rename from bin/Djot.ipkg rename to Djot.ipkg diff --git a/pack.toml b/pack.toml index 303ca46..4a7cd19 100644 --- a/pack.toml +++ b/pack.toml @@ -6,7 +6,7 @@ test = "test/test.ipkg" [custom.all.Djot] type = "local" -path = "bin" +path = "." ipkg = "Djot.ipkg" [custom.all.SSG-test] diff --git a/bin/src/Djot.idr b/src/Djot.idr similarity index 100% rename from bin/src/Djot.idr rename to src/Djot.idr From 7ef90867f25697c704c37ddab6b7261cc162d873 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 23 Feb 2025 17:05:28 -0500 Subject: [PATCH 21/33] checkpoint --- src/SSG/Djot/Block.idr | 50 ++++++++++++++++++--- src/SSG/Djot/Common.idr | 7 +-- src/SSG/Djot/Render.idr | 3 ++ test/djot-to-html/003-headings/expected | 16 ++++--- test/djot-to-html/004-blockquotes/Main.idr | 16 +++++++ test/djot-to-html/004-blockquotes/expected | 22 +++++++++ test/djot-to-html/004-blockquotes/run | 6 +++ test/djot-to-html/004-blockquotes/test.dj | 11 +++++ test/djot-to-html/004-blockquotes/test.ipkg | 7 +++ todo.org | 3 +- 10 files changed, 124 insertions(+), 17 deletions(-) create mode 100644 test/djot-to-html/004-blockquotes/Main.idr create mode 100644 test/djot-to-html/004-blockquotes/expected create mode 100644 test/djot-to-html/004-blockquotes/run create mode 100644 test/djot-to-html/004-blockquotes/test.dj create mode 100644 test/djot-to-html/004-blockquotes/test.ipkg diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index 273f481..e9754d7 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -17,6 +17,7 @@ import Derive.Pretty -- For iutils unit tests import System +import Debug.Trace %language ElabReflection @@ -63,6 +64,7 @@ public export data Block : Type where Paragraph : (contents : List1 Inline) -> Block Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block + BlockQuote : (contents : List1 Block) -> Block %runElab derive "List1" [Pretty] %runElab derive "Block" [Show, Eq, Pretty] @@ -75,7 +77,7 @@ data Block : Type where prefixedLine : (pfx : PS b) -> PS String prefixedLine pfx = do _ <- pfx - cs <- nonBlankLine + cs <- line pure $ pack cs -- Parses a block prefixed by the given character string with the given parser @@ -89,6 +91,14 @@ parsePrefixedBlock pfx parser = do --* Syntax * --***************** +-- Forward declare our top level parsers, so we can get mutually recursive + +export +block : PS Block + +export +blocks : PS (List Block) + --------------- -- Paragraph -- --------------- @@ -138,25 +148,44 @@ heading = do load state inlines <- parsePrefixedBlock (headingPrefix (length levelMarker)) inline -- djot demands a blank line or the end of file after a heading - _ <- blankLineOrEnd + _ <- many blankLine pure $ Heading level inlines +---------------- +-- Blockquote -- +---------------- + +blockquote : PS Block +blockquote = do + blocks <- parsePrefixedBlock (oneOfE "" [prefixedEmpty, thisString "> "]) blocks + case blocks of + [] => throw "Empty block quote" + (x :: xs) => pure $ BlockQuote (x ::: xs) + where + prefixedEmpty : PS String + prefixedEmpty = do + _ <- thisString ">" + -- peek the rest of the line, make sure it's empty + state <- save + cs <- many nonTerminal + load state + if all isHorizontalWhitespace cs + then pure ">" + else throw "Invalid blockquote line" + -------------------------- -- Overall Block Parser -- -------------------------- -export -block : PS Block block = do -- eat up any blank lines _ <- many blankLine oneOfE "" [ heading + , blockquote , paragraph ] -export -blocks : PS (List Block) blocks = many block --***************** @@ -219,3 +248,12 @@ blockMultilineUnprefixed = Heading 1 (Text "Level 1" ::: [SoftLineBreak, Text "More text"]) ] in golden input ref blocks + +-- @@test Single Line Blockquote +blockSingleLineBlockquote : IO Bool +blockSingleLineBlockquote = + let input = "> Blockquote" + ref = [ + BlockQuote ( Paragraph (inlineFromString' "Blockquote") ::: []) + ] + in golden input ref blocks diff --git a/src/SSG/Djot/Common.idr b/src/SSG/Djot/Common.idr index 8f8b71b..0f35892 100644 --- a/src/SSG/Djot/Common.idr +++ b/src/SSG/Djot/Common.idr @@ -92,8 +92,10 @@ terminal = do export line : PS (List Char) line = do + False <- parseEoF + | True => throw "Already at EoF" cs <- many nonTerminal - _ <- lineEnding + terminal pure cs export @@ -111,8 +113,7 @@ blankLine = do export nonBlankLine : PS (List Char) nonBlankLine = do - cs <- many nonTerminal - _ <- terminal + cs <- line case all isHorizontalWhitespace cs of True => throw "blank line" False => pure cs diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index b218f6b..e88f984 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -64,6 +64,9 @@ renderBlock (Heading level contents) = let (_ ** xs) = renderInlines $ forget contents (level ** _ ) = headingLevel level in (_ ** Normal level [] xs) +renderBlock (BlockQuote contents) = + let (_ ** contents) = fromList . map renderBlock . forget $ contents + in (_ ** Normal "blockquote" [] contents) export renderBlocks : List Block -> (types : List String ** DList _ Html types) diff --git a/test/djot-to-html/003-headings/expected b/test/djot-to-html/003-headings/expected index 91f7ee8..ae84cb0 100644 --- a/test/djot-to-html/003-headings/expected +++ b/test/djot-to-html/003-headings/expected @@ -8,17 +8,19 @@
Level 5 Heading
Level 6 Heading

####### Level 7 Not a Heading

-

A heading that spans multiple lines

-

Heading

+

# A heading that spans multiple lines

+

# Heading

Some content

-

A sub heading

+

## A sub heading

Even more content

-

Back up

+

# Back up

Some final content

A Multiline Heading

-

A Level 2 Multiline Heading

-

## Heading ### Not a heading

-

### Heading ## Not a heading

+

## A Level 2 ## Multiline Heading

+

Heading

+

### Not a heading

+

Heading

+

Not a heading

A Multiline Heading

A Level 2 Multiline Heading

A Multiline Heading

diff --git a/test/djot-to-html/004-blockquotes/Main.idr b/test/djot-to-html/004-blockquotes/Main.idr new file mode 100644 index 0000000..97d8771 --- /dev/null +++ b/test/djot-to-html/004-blockquotes/Main.idr @@ -0,0 +1,16 @@ +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 parsed = djot contents + putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/004-blockquotes/expected b/test/djot-to-html/004-blockquotes/expected new file mode 100644 index 0000000..1efa208 --- /dev/null +++ b/test/djot-to-html/004-blockquotes/expected @@ -0,0 +1,22 @@ + + + +
+

A single line block quote

+
+
+

This is a multi-line blockquote With no linebreaks

+
+
+

This is a multi-line block quote with

+

A line break

+
+
+

+ This is a block quote with a +
+ hard break in it +

+
+ + \ No newline at end of file diff --git a/test/djot-to-html/004-blockquotes/run b/test/djot-to-html/004-blockquotes/run new file mode 100644 index 0000000..6b5ab53 --- /dev/null +++ b/test/djot-to-html/004-blockquotes/run @@ -0,0 +1,6 @@ +rm -rf build/ + +flock "$1" pack -q install-deps test.ipkg +pack -q run test.ipkg + +rm -rf build/ diff --git a/test/djot-to-html/004-blockquotes/test.dj b/test/djot-to-html/004-blockquotes/test.dj new file mode 100644 index 0000000..69790d6 --- /dev/null +++ b/test/djot-to-html/004-blockquotes/test.dj @@ -0,0 +1,11 @@ +> A single line block quote + +> This is a multi-line blockquote +> With no linebreaks + +> This is a multi-line block quote with +> +> A line break + +> This is a block quote with a \ +> hard break in it diff --git a/test/djot-to-html/004-blockquotes/test.ipkg b/test/djot-to-html/004-blockquotes/test.ipkg new file mode 100644 index 0000000..0efef9e --- /dev/null +++ b/test/djot-to-html/004-blockquotes/test.ipkg @@ -0,0 +1,7 @@ +package a-test + +depends = SSG + +main = Main + +executable = test diff --git a/todo.org b/todo.org index d263555..7f89a0d 100644 --- a/todo.org +++ b/todo.org @@ -9,7 +9,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [7/43] +* Djot [7/44] :PROPERTIES: :COOKIE_DATA: recursive :END: @@ -55,6 +55,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Support all types of whitespace *** TODO Escaping *** TODO Whitespace class +** TODO Lazy indentation ** TODO hex escapes ** TODO GFM style alerts ** TODO Group adjacent =Text=s into a =String= From 81a7f09623dc56e095b35c8219a846fe03118b61 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 23 Feb 2025 17:12:19 -0500 Subject: [PATCH 22/33] Undo everything to switch over to an event based parser --- Djot.ipkg | 47 ---- SSG.ipkg | 9 +- src/Djot.idr | 27 -- src/SSG/Djot.idr | 17 -- src/SSG/Djot/Block.idr | 259 ------------------ src/SSG/Djot/Common.idr | 161 ----------- src/SSG/Djot/Inline.idr | 226 --------------- src/SSG/Djot/Render.idr | 80 ------ src/SSG/Parser/Core.idr | 192 ------------- src/SSG/Parser/Util.idr | 148 ---------- .../002-linebreaks-and-nbsp/Main.idr | 16 -- .../002-linebreaks-and-nbsp/expected | 26 -- test/djot-to-html/002-linebreaks-and-nbsp/run | 6 - .../002-linebreaks-and-nbsp/test.dj | 22 -- .../002-linebreaks-and-nbsp/test.ipkg | 7 - test/djot-to-html/003-headings/Main.idr | 16 -- test/djot-to-html/003-headings/expected | 29 -- test/djot-to-html/003-headings/run | 6 - test/djot-to-html/003-headings/test.dj | 52 ---- test/djot-to-html/003-headings/test.ipkg | 7 - test/djot-to-html/004-blockquotes/Main.idr | 16 -- test/djot-to-html/004-blockquotes/expected | 22 -- test/djot-to-html/004-blockquotes/run | 6 - test/djot-to-html/004-blockquotes/test.dj | 11 - test/djot-to-html/004-blockquotes/test.ipkg | 7 - 25 files changed, 1 insertion(+), 1414 deletions(-) delete mode 100644 Djot.ipkg delete mode 100644 src/Djot.idr delete mode 100644 src/SSG/Djot.idr delete mode 100644 src/SSG/Djot/Block.idr delete mode 100644 src/SSG/Djot/Common.idr delete mode 100644 src/SSG/Djot/Inline.idr delete mode 100644 src/SSG/Djot/Render.idr delete mode 100644 src/SSG/Parser/Core.idr delete mode 100644 src/SSG/Parser/Util.idr delete mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/Main.idr delete mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/expected delete mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/run delete mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/test.dj delete mode 100644 test/djot-to-html/002-linebreaks-and-nbsp/test.ipkg delete mode 100644 test/djot-to-html/003-headings/Main.idr delete mode 100644 test/djot-to-html/003-headings/expected delete mode 100644 test/djot-to-html/003-headings/run delete mode 100644 test/djot-to-html/003-headings/test.dj delete mode 100644 test/djot-to-html/003-headings/test.ipkg delete mode 100644 test/djot-to-html/004-blockquotes/Main.idr delete mode 100644 test/djot-to-html/004-blockquotes/expected delete mode 100644 test/djot-to-html/004-blockquotes/run delete mode 100644 test/djot-to-html/004-blockquotes/test.dj delete mode 100644 test/djot-to-html/004-blockquotes/test.ipkg diff --git a/Djot.ipkg b/Djot.ipkg deleted file mode 100644 index bc3a2dc..0000000 --- a/Djot.ipkg +++ /dev/null @@ -1,47 +0,0 @@ -package Djot -version = 0.1.0 -authors = "Nathan McCarty" --- maintainers = --- license = --- brief = --- readme = --- homepage = --- sourceloc = --- bugtracker = - --- the Idris2 version required (e.g. langversion >= 0.5.1) --- langversion - --- packages to add to search path -depends = SSG - --- modules to install --- modules = - --- main file (i.e. file to load at REPL) -main = Djot - --- name of executable -executable = "djot" --- opts = -sourcedir = "src" --- builddir = --- outputdir = - --- script to run before building --- prebuild = - --- script to run after building --- postbuild = - --- script to run after building, before installing --- preinstall = - --- script to run after installing --- postinstall = - --- script to run before cleaning --- preclean = - --- script to run after cleaning --- postclean = diff --git a/SSG.ipkg b/SSG.ipkg index ec92d59..6c9228d 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -22,14 +22,7 @@ depends = structures , prettier -- modules to install -modules = SSG.Parser.Core - , SSG.Parser.Util - , SSG.Djot - , SSG.Djot.Common - , SSG.Djot.Inline - , SSG.Djot.Block - , SSG.Djot.Render - , SSG.HTML +modules = SSG.HTML , SSG.HTML.ElementTypes -- main file (i.e. file to load at REPL) diff --git a/src/Djot.idr b/src/Djot.idr deleted file mode 100644 index 85a0767..0000000 --- a/src/Djot.idr +++ /dev/null @@ -1,27 +0,0 @@ -module Djot - -import System -import System.File - -import SSG.Djot -import SSG.HTML - -import Text.PrettyPrint.Bernardy - -main : IO () -main = do - args <- getArgs - case args of - [_, file] => do - Right contents <- readFile file - | Left err => printLn err - let parsed = djot contents - putStr . render $ renderHtml parsed - [_, "raw", file] => do - Right contents <- readFile file - | Left err => printLn err - let parsed = djot contents - putStrLn . Doc.render (Opts 80) $ pretty parsed - _ => do - putStrLn "?" - exitFailure diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr deleted file mode 100644 index 84636b1..0000000 --- a/src/SSG/Djot.idr +++ /dev/null @@ -1,17 +0,0 @@ -module SSG.Djot - -import SSG.Parser.Util - -import Control.Eff - -import public SSG.Djot.Inline as SSG.Djot -import public SSG.Djot.Block as SSG.Djot -import public SSG.Djot.Render as SSG.Djot - -export -||| Parse a djot document -djot : String -> List Block -djot str = - case runPS blocks str of - Left _ => [] - Right x => x diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr deleted file mode 100644 index e9754d7..0000000 --- a/src/SSG/Djot/Block.idr +++ /dev/null @@ -1,259 +0,0 @@ -module SSG.Djot.Block - -import SSG.Parser.Core -import SSG.Parser.Util - -import SSG.Djot.Common -import SSG.Djot.Inline - -import Data.List1 -import Data.Vect -import Data.Nat -import Data.String - -import Control.Eff -import Derive.Prelude -import Derive.Pretty - --- For iutils unit tests -import System -import Debug.Trace - -%language ElabReflection - ---***************** ---* Data Types * ---***************** - -public export -data HeaderLevel : Type where - H1 : HeaderLevel - H2 : HeaderLevel - H3 : HeaderLevel - H4 : HeaderLevel - H5 : HeaderLevel - H6 : HeaderLevel - -%runElab derive "HeaderLevel" [Eq, Pretty] - -export -Show HeaderLevel where - show H1 = "1" - show H2 = "2" - show H3 = "3" - show H4 = "4" - show H5 = "5" - show H6 = "6" - -namespace HeaderLevel - public export - integerToHeader : Integer -> Maybe HeaderLevel - integerToHeader 1 = Just H1 - integerToHeader 2 = Just H2 - integerToHeader 3 = Just H3 - integerToHeader 4 = Just H4 - integerToHeader 5 = Just H5 - integerToHeader 6 = Just H6 - integerToHeader i = Nothing - - export - fromInteger : (x : Integer) -> {auto prf : IsJust (integerToHeader x)} -> HeaderLevel - fromInteger x = fromJust $ integerToHeader x - -public export -data Block : Type where - Paragraph : (contents : List1 Inline) -> Block - Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block - BlockQuote : (contents : List1 Block) -> Block - -%runElab derive "List1" [Pretty] -%runElab derive "Block" [Show, Eq, Pretty] - ---***************** ---* Parsing Utils * ---***************** - --- Parse a prefixed line, stripping the prefix -prefixedLine : (pfx : PS b) -> PS String -prefixedLine pfx = do - _ <- pfx - cs <- line - pure $ pack cs - --- Parses a block prefixed by the given character string with the given parser -parsePrefixedBlock : (pfx : PS b) -> (parser : PS a) -> PS a -parsePrefixedBlock pfx parser = do - lines <- atLeastOne "No lines in block" $ prefixedLine pfx - let block = joinBy "\n" . forget $ lines - runPS' parser block - ---***************** ---* Syntax * ---***************** - --- Forward declare our top level parsers, so we can get mutually recursive - -export -block : PS Block - -export -blocks : PS (List Block) - ---------------- --- Paragraph -- ---------------- - -paragraph : PS Block -paragraph = do - inlines <- inline - blankLineOrEnd - pure $ Paragraph inlines - -------------- --- Heading -- -------------- - -headingPrefix : (level : Nat) -> PS String -headingPrefix level = oneOfE "" [notPrefixP, prefixP] - where - notPrefixed : PS () - notPrefixed = do - -- peek the first character to check and see if its a heading marker - Just [first] <- peek 1 - | _ => throw "End of File" - case first of - '#' => throw "Header prefix" - _ => pure () - notPrefixP : PS String - notPrefixP = do - notPrefixed - map pack $ many space - prefixP : PS String - prefixP = do - levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#" - ws <- atLeastOne "Expected Whitespace after header marker" $ space - case length levelMarker == level of - False => throw "Mismatched levels" - True => pure $ (concat . forget $ levelMarker) ++ (pack . forget $ ws) - -heading : PS Block -heading = do - -- peek the level marker, then parse as a prefixed block - state <- save - levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#" - ws <- atLeastOne "Expected Whitespace after header marker" $ space - case integerToHeader (natToInteger $ length levelMarker) of - Nothing => throw "Invalid header length: \{show $ length levelMarker}" - Just level => do - load state - inlines <- parsePrefixedBlock (headingPrefix (length levelMarker)) inline - -- djot demands a blank line or the end of file after a heading - _ <- many blankLine - pure $ Heading level inlines - ----------------- --- Blockquote -- ----------------- - -blockquote : PS Block -blockquote = do - blocks <- parsePrefixedBlock (oneOfE "" [prefixedEmpty, thisString "> "]) blocks - case blocks of - [] => throw "Empty block quote" - (x :: xs) => pure $ BlockQuote (x ::: xs) - where - prefixedEmpty : PS String - prefixedEmpty = do - _ <- thisString ">" - -- peek the rest of the line, make sure it's empty - state <- save - cs <- many nonTerminal - load state - if all isHorizontalWhitespace cs - then pure ">" - else throw "Invalid blockquote line" - --------------------------- --- Overall Block Parser -- --------------------------- - -block = do - -- eat up any blank lines - _ <- many blankLine - oneOfE "" [ - heading - , blockquote - , paragraph - ] - -blocks = many block - ---***************** ---* Unit Tests * ---***************** - ------------------------- --- Block Syntax Tests -- ------------------------- - --- @@test Paragraph -blockParagraphSmoke : IO Bool -blockParagraphSmoke = - let input = "Hello World" - ref = [Paragraph (inlineFromString' "Hello World")] - in golden input ref blocks - --- @@test Two Paragraph -blockTwoParagraphSmoke : IO Bool -blockTwoParagraphSmoke = - let input = "Hello World\n\nHello Again" - ref = [ - Paragraph (inlineFromString' "Hello World") - , Paragraph (inlineFromString' "Hello Again") - ] - in golden input ref blocks - --- @@test Level 1 heading -blockLevelOneHeadingSmoke : IO Bool -blockLevelOneHeadingSmoke = - let input = "# Level 1" - ref = [ - Heading 1 (inlineFromString' "Level 1") - ] - in golden input ref blocks - --- @@test Level 2 heading -blockLevelTwoHeadingSmoke : IO Bool -blockLevelTwoHeadingSmoke = - let input = "## Level 2" - ref = [ - Heading 2 (inlineFromString' "Level 2") - ] - in golden input ref blocks - --- @@test Multiline prefixed headings -blockMultilinePrefixed : IO Bool -blockMultilinePrefixed = - let input = "# Level 1\n# More text" - ref = [ - Heading 1 (Text "Level 1" ::: [SoftLineBreak, Text "More text"]) - ] - in golden input ref blocks - --- @@test Multiline unprefixed headings -blockMultilineUnprefixed : IO Bool -blockMultilineUnprefixed = - let input = "# Level 1\nMore text" - ref = [ - Heading 1 (Text "Level 1" ::: [SoftLineBreak, Text "More text"]) - ] - in golden input ref blocks - --- @@test Single Line Blockquote -blockSingleLineBlockquote : IO Bool -blockSingleLineBlockquote = - let input = "> Blockquote" - ref = [ - BlockQuote ( Paragraph (inlineFromString' "Blockquote") ::: []) - ] - in golden input ref blocks diff --git a/src/SSG/Djot/Common.idr b/src/SSG/Djot/Common.idr deleted file mode 100644 index 0f35892..0000000 --- a/src/SSG/Djot/Common.idr +++ /dev/null @@ -1,161 +0,0 @@ -module SSG.Djot.Common - -import SSG.Parser.Core -import SSG.Parser.Util - -import Control.Eff - ---***************************************** ---* Character Classes and String Escaping * ---***************************************** - ------------------------ --- Character classes -- ------------------------ - --- Class contents - -export -punctuationChars : List Char -punctuationChars = - [ - '!', '"', '#', '$', '%', '&', '\'' - , '(' , ')' , '*' , '+' , ',' , '-' - , '.' , '/' , ':' , ';' , '<' , '=' - , '>' , '?' , '@' , '[' , ']' , '^' - , '_' , '`' , '{' , '|' , '}' , '~' - ] - -export -horizontalWhitespaceChars : List Char -horizontalWhitespaceChars = - [' ', '\t'] - -export -verticalWhitespaceChars : List Char -verticalWhitespaceChars = - ['\n', '\r'] - --- Class parsers - -export -punctuation : PS Char -punctuation = theseChars punctuationChars - --------------- --- Escaping -- --------------- - -export -escapedChar : PS Char -escapedChar = do - _ <- thisString "\\" - oneOfE "Expected an escapable code" - [ punctuation - , exactReplace "n" '\n' - , exactReplace "t" '\t' - , exactReplace "r" '\r' - ] - ------------------------------------- --- Line Qualifying And Whitespace -- ------------------------------------- - -export -space : PS Char -space = theseChars horizontalWhitespaceChars - -export -spaces : PS Nat -spaces = do - xs <- many space - pure $ length xs - -export -nonTerminal : PS Char -nonTerminal = notTheseChars verticalWhitespaceChars - -export -lineEnding : PS String -lineEnding = theseStrings ["\r\n", "\n", "\r"] - -export -terminal : PS () -terminal = do - Nothing <- tryMaybe lineEnding - | _ => pure () - test <- parseEoF - case test of - False => throw "Expected line terminal" - True => pure () - -export -line : PS (List Char) -line = do - False <- parseEoF - | True => throw "Already at EoF" - cs <- many nonTerminal - terminal - pure cs - -export -isHorizontalWhitespace : Char -> Bool -isHorizontalWhitespace c = any (== c) horizontalWhitespaceChars - -export -blankLine : PS (List Char) -blankLine = do - cs <- line - case all isHorizontalWhitespace cs of - False => throw "nonblank line" - True => pure cs - -export -nonBlankLine : PS (List Char) -nonBlankLine = do - cs <- line - case all isHorizontalWhitespace cs of - True => throw "blank line" - False => pure cs - -export -blankLineOrEnd : PS () -blankLineOrEnd = do - Nothing <- tryMaybe blankLine - | Just _ => pure () - eof <- parseEoF - case eof of - False => throw "Expected newline or end of document" - True => pure () - -export -blankLines : PS () -blankLines = do - xs <- many blankLine - if length xs > 0 - then pure () - else blankLineOrEnd - ---***************************************** ---* Unit Tests * ---***************************************** - -------------------------------- --- Testing Utility Functions -- -------------------------------- - --- Test a parser against a golden value with the supplied input -export -golden : Show a => Eq a => - (input : String) -> (reference : a) -> (parser : PS a) -> IO Bool -golden input ref parser = do - putStrLn "Input: \{input}" - putStrLn "Expected: \{show ref}" - let got = runPS parser input - case got of - Left err => do - putStrLn "Failed with error: \{err}" - pure False - Right x => do - putStrLn "Output: \{show x}" - pure $ x == ref diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr deleted file mode 100644 index 66a0ee9..0000000 --- a/src/SSG/Djot/Inline.idr +++ /dev/null @@ -1,226 +0,0 @@ -module SSG.Djot.Inline - -import SSG.Parser.Core -import SSG.Parser.Util - -import SSG.Djot.Common - -import Control.Eff -import Control.Monad.Eval -import Derive.Prelude -import Derive.Pretty - --- For iutils unit tests -import System - -%language ElabReflection - ---****************** ---* Data Types * ---****************** - -public export -data Inline : Type where - HardLineBreak : Inline - SoftLineBreak : Inline - NonBreakingSpace : Inline - Text : (c : String) -> Inline - -%runElab derive "Inline" [Show, Eq, Pretty] - ---****************** ---* PostProcessing * ---****************** - --- Combine adjacent `Text`s in the parsed output -combineTexts : List1 Inline -> Eval (List1 Inline) -combineTexts (Text c ::: (Text d :: xs)) = - combineTexts (Text (c ++ d) ::: xs) -combineTexts (x ::: tail) = do - rest <- combineTexts' tail - pure $ x ::: rest - where - combineTexts' : List Inline -> Eval (List Inline) - combineTexts' [] = pure [] - combineTexts' (y :: []) = pure [y] - combineTexts' (Text c :: (Text d :: xs)) = - combineTexts' (Text (c ++ d) :: xs) - combineTexts' (y :: ys) = do - rest <- combineTexts' ys - pure $ y :: rest - --- Combine adjacent soft line breaks into one -combineSoftBreaks : List1 Inline -> Eval (List1 Inline) -combineSoftBreaks (SoftLineBreak ::: (SoftLineBreak :: xs)) = - combineSoftBreaks (SoftLineBreak ::: xs) -combineSoftBreaks (head ::: tail) = do - tail <- combineSoftBreaks' tail - pure $ head ::: tail - where - combineSoftBreaks' : List Inline -> Eval (List Inline) - combineSoftBreaks' [] = pure [] - combineSoftBreaks' (x :: []) = pure [x] - combineSoftBreaks' (SoftLineBreak :: (SoftLineBreak :: xs)) = - combineSoftBreaks' (SoftLineBreak :: xs) - combineSoftBreaks' (x :: xs) = do - rest <- combineSoftBreaks' xs - pure $ x :: rest - --- Remove a trailing soft line break from a list of inlines -removeTrailingSoftBreak : List1 Inline -> Eval (List1 Inline) -removeTrailingSoftBreak (head ::: tail) = do - tail <- inner tail - pure $ head ::: tail - where - inner : List Inline -> Eval (List Inline) - inner [] = pure [] - inner (SoftLineBreak :: []) = pure [] - inner (x :: xs) = do - xs <- inner xs - pure $ x :: xs - --- Combine all post processing steps -postProcess : List1 Inline -> List1 Inline -postProcess xs = eval $ do - xs <- combineTexts xs - xs <- combineSoftBreaks xs - xs <- removeTrailingSoftBreak xs - pure xs - ---****************** ---* Syntax * ---****************** - ------------------------- --- Escaped Whitespace -- ------------------------- - -hardLineBreak : PS Inline -hardLineBreak = do - _ <- thisString "\\" - _ <- spaces - _ <- lineEnding - pure $ HardLineBreak - -nbsp : PS Inline -nbsp = do - _ <- thisString "\\ " - pure $ NonBreakingSpace - -softLineBreak : PS Inline -softLineBreak = do - -- Slurp up any horizontal whitespace before the line break - _ <- spaces - _ <- lineEnding - -- Check to see if the next line is empty, if it is, we are at the end of the inline - -- content, go ahead and bail - state <- save - Nothing <- tryMaybe blankLine - | Just _ => throw "End of inline" - load state - -- Slurp up any horizontal whitespace after the line break - _ <- spaces - pure $ SoftLineBreak - -escapedNewLine : PS Inline -escapedNewLine = do - -- Slurp up any horizontal whitespace before the line break - _ <- spaces - _ <- thisString "\\n" - -- Slurp up any horizontal whitespace after the line break - _ <- spaces - pure $ SoftLineBreak - ---------------------- --- Emphasis/Strong -- ---------------------- - ----------- --- Text -- ----------- - --- Process escape codes before processing as text -escapedText : PS Inline -escapedText = do - c <- escapedChar - pure $ Text (singleton c) - --- Any non-line-ending character can be part of regular text -text : PS Inline -text = do - c <- nonTerminal - pure $ Text (singleton c) - ---------------------------- --- Overall Inline Parser -- ---------------------------- - -inlineElement : PS Inline -inlineElement = oneOfE "" [ - hardLineBreak - , softLineBreak - , escapedNewLine - , nbsp - , escapedText - -- Text is last so that anything can superseed it - , text - ] - -export -inline : PS (List1 Inline) -inline = map postProcess $ - atLeastOne "Expected Inline Content" inlineElement - ---****************** ---* Unit Tests * ---****************** - -------------------------------- --- Testing Utility Functions -- -------------------------------- - - -export -inlineFromString' : String -> List1 (Inline) -inlineFromString' str = Text str ::: [] - -export -inlineFromString : String -> List (Inline) -inlineFromString = forget . inlineFromString' ------------ --- Tests -- ------------ - --- @@test Plain Text Hello World -inlineTextSmoke : IO Bool -inlineTextSmoke = - let input = "Hello World!" in - golden input (inlineFromString input) (map forget inline) - --- @@test Escaped Text -inlineEscapedSmoke : IO Bool -inlineEscapedSmoke = - let input = "Hello\\n\\*World" - ref = [Text "Hello", SoftLineBreak, Text "*World"] - in golden input ref (map forget inline) - --- @@test Hard Line Break -inlineHardBreakSmoke : IO Bool -inlineHardBreakSmoke = - let input = "Hello\\\nWorld" - ref = inlineFromString "Hello" ++ [HardLineBreak] ++ inlineFromString "World" - in golden input ref (map forget inline) - --- @@test Soft Line Break -inlineSoftBreakSmoke : IO Bool -inlineSoftBreakSmoke = - let input = "Hello\nWorld" - ref = inlineFromString "Hello" ++ [SoftLineBreak] ++ inlineFromString "World" - in golden input ref (map forget inline) - --- @@test Nonbreaking Space -inlineNbspSmoke : IO Bool -inlineNbspSmoke = - let input = "Hello\\ World" - ref = inlineFromString "Hello" ++ [NonBreakingSpace] ++ inlineFromString "World" - in golden input ref (map forget inline) diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr deleted file mode 100644 index e88f984..0000000 --- a/src/SSG/Djot/Render.idr +++ /dev/null @@ -1,80 +0,0 @@ -module SSG.Djot.Render - -import SSG.HTML - -import SSG.Djot.Inline -import SSG.Djot.Block - -import Data.String -import Data.List1 -import Data.List - -import Control.Monad.Eval -import Structures.Dependent.DList - --- Maybe because specifically Soft line breaks don't generate any html of their --- own -export -renderInline : Inline -> Maybe (type : String ** Html type) -renderInline HardLineBreak = - Just (_ ** Void "br" []) -renderInline SoftLineBreak = - Nothing -renderInline NonBreakingSpace = - Just (_ ** Text " ") -renderInline (Text c) = - Just (_ ** Text c) - -combineTexts : (types : List String ** DList _ Html types) - -> Eval (types : List String ** DList _ Html types) -combineTexts (_ ** []) = pure (_ ** []) --- We do a little bit of magic insert of whitespace, so we have some special handling for --- nbsps to not insert spaces around them -combineTexts (_ ** (Text c :: Text " " :: Text " " :: rest)) = - combineTexts (_ ** Text (c ++ " ") :: Text " " :: rest) -combineTexts (_ ** (Text c :: Text " " :: Text d :: rest)) = - combineTexts (_ ** Text (c ++ " " ++ d) :: rest) -combineTexts (_ ** (Text c :: Text " " :: rest)) = - combineTexts (_ ** Text (c ++ " ") :: rest) -combineTexts (_ ** (Text c :: Text d :: rest)) = - combineTexts (_ ** Text (c ++ " " ++ d) :: rest) -combineTexts (_ ** (elem :: rest)) = do - (_ ** rest) <- combineTexts (_ ** rest) - pure $ (_ ** elem :: rest) - -export -renderInlines : List Inline -> (types : List String ** DList _ Html types) -renderInlines xs = - eval . combineTexts . fromList . catMaybes . map renderInline $ xs - -headingLevel : HeaderLevel -> (h : String ** IsNormal h) -headingLevel H1 = ("h1" ** IsH1) -headingLevel H2 = ("h2" ** IsH2) -headingLevel H3 = ("h3" ** IsH3) -headingLevel H4 = ("h4" ** IsH4) -headingLevel H5 = ("h5" ** IsH5) -headingLevel H6 = ("h6" ** IsH6) - -export -renderBlock : Block -> (type : String ** Html type) -renderBlock (Paragraph contents) = - let (_ ** xs) = renderInlines $ forget contents - in (_ ** Normal "p" [] xs) -renderBlock (Heading level contents) = - let (_ ** xs) = renderInlines $ forget contents - (level ** _ ) = headingLevel level - in (_ ** Normal level [] xs) -renderBlock (BlockQuote contents) = - let (_ ** contents) = fromList . map renderBlock . forget $ contents - in (_ ** Normal "blockquote" [] contents) - -export -renderBlocks : List Block -> (types : List String ** DList _ Html types) -renderBlocks xs = fromList $ map renderBlock xs - -export -renderHtml : List Block -> Html "html" -renderHtml xs = - let (_ ** xs) = renderBlocks xs - in Normal "html" ["lang" =$ "en"] - [ Normal "body" [] xs ] diff --git a/src/SSG/Parser/Core.idr b/src/SSG/Parser/Core.idr deleted file mode 100644 index 9cea39d..0000000 --- a/src/SSG/Parser/Core.idr +++ /dev/null @@ -1,192 +0,0 @@ -module SSG.Parser.Core - -import Data.Vect -import Data.String - -import Control.Eff -import Derive.Prelude - -%language ElabReflection - ---------------------------- --- Internal parser state -- ---------------------------- - -||| The location of a parser within a string -public export -data ParserLocation : Type where - AtPoint : (length : Int) -> (location : Int) -> ParserLocation - EndOfInput : (length : Int) -> ParserLocation - -%runElab derive "ParserLocation" [Show] - -namespace ParserLocation - export - fromString : String -> ParserLocation - fromString str = - if strLength str > 0 - then AtPoint (strLength str) 0 - else EndOfInput 0 - -||| The state of a parser -public export -record ParserState where - constructor MkPS - input : String - location : ParserLocation - -%runElab derive "ParserState" [Show] - -namespace ParserState - export - fromString : String -> ParserState - fromString str = MkPS str (fromString str) - - export - toString : ParserState -> String - toString (MkPS input (AtPoint length location)) = strSubstr location length input - toString (MkPS input (EndOfInput length)) = "" - - -||| Three way result of parsing -public export -data ParseResult : Type -> Type where - Got : t -> ParseResult t - Failed : t -> ParseResult t - EoF : ParseResult t - ------------------ --- Effect Type -- ------------------ - -||| The parser effect -export -data Parser : Type -> Type where - -- Save and load the state - Save : Parser ParserState - Load : ParserState -> Parser () - -- Peek the next `n` characters, if there are enough, without altering the parser state - Peek : (n : Nat) -> Parser (Maybe (Vect n Char)) - -- Parse a single char, if it satisfies a predicate - ParseChar : (predicate : Char -> Bool) -> Parser (ParseResult Char) - -- Parse an exact string match - ParseExact : (str : String) -> Parser (ParseResult String) - -- Skip a run of 0 or more chars all satisfying a predicate - SkipChars : (predicate : Char -> Bool) -> Parser () - -- Detect the end of input - ParseEoF : Parser Bool - -Show (Parser a) where - show Save = "save" - show (Load x) = "load: \{show x}" - show (Peek n) = "peek: \{show n}]" - show (ParseChar predicate) = "ParseChar" - show (ParseExact str) = "ParseExact: \{str}" - show (SkipChars predicate) = "SkipChars" - show ParseEoF = "ParseEof" - ------------------------ --- Effectful Actions -- ------------------------ - -||| Aquire a copy of the current parser state -||| -||| Intended to be used for backtracking -export -save : Has Parser fs => Eff fs ParserState -save = send Save - -||| Restore the parser state to a previousy persisted copy -export -load : Has Parser fs => ParserState -> Eff fs () -load x = send $ Load x - -||| Look ahead exactly `n` characters -export -peek : Has Parser fs => (n : Nat) -> Eff fs (Maybe (Vect n Char)) -peek n = send $ Peek n - -||| Attempt to parse a single char satisfying the given predicate, leaving the parser -||| state unchanged on failure -export -parseChar : Has Parser fs => (predicate : Char -> Bool) -> Eff fs (ParseResult Char) -parseChar predicate = send $ ParseChar predicate - -||| Parse an exact match of the given string -export -parseExact : Has Parser fs => (str : String) -> Eff fs (ParseResult String) -parseExact str = send $ ParseExact str - -||| Skip a run of any number of characters satisfying the given predicate -export -skipChars : Has Parser fs => (predicate : Char -> Bool) -> Eff fs () -skipChars predicate = send $ SkipChars predicate - -||| Detect EoF -export -parseEoF : Has Parser fs => Eff fs Bool -parseEoF = send ParseEoF - --------------------- --- Effect handler -- --------------------- - -export -unParser : ParserState -> Parser a -> (a, ParserState) --- Save the parser state -unParser s Save = - (s, s) --- Load a provided parser state -unParser s (Load x) = - ((), x) --- Look ahead exactly `n` characters -unParser s@(MkPS input (AtPoint length location)) (Peek n) = - let cs = unpack . strSubstr location (cast n) $ input - in (toVect n cs, s) -unParser s@(MkPS input (EndOfInput length)) (Peek n) = - (Nothing, s) --- Attempt to parse a single character matching a given predicate, bail out without --- affecting the parser state otherwise -unParser s@(MkPS input (AtPoint length location)) (ParseChar predicate) = - -- Saftey: We maintain location < length as a type invariant - let c = assert_total $ strIndex input location - in if predicate c - then if location + 1 < length - then (Got c, MkPS input (AtPoint length (location + 1))) - else (Got c, MkPS input (EndOfInput length)) - else (Failed c, s) -unParser s@(MkPS input (EndOfInput length)) (ParseChar predicate) = - (EoF, s) --- Parse an exact string match -unParser s@(MkPS input (AtPoint length location)) (ParseExact str) = - let substr = strSubstr location (strLength str) input - in if substr == str - then if location + (strLength str) < length - then (Got substr, MkPS input (AtPoint length (location + strLength str))) - else (Got substr, MkPS input (EndOfInput length)) - else (Failed substr, s) -unParser s@(MkPS input (EndOfInput length)) (ParseExact str) = (EoF, s) --- Skip any number of chars satisfying a given predicate -unParser s@(MkPS input (AtPoint length location)) (SkipChars predicate) = - case unParser s (ParseChar predicate) of - (Got _, s) => unParser s (SkipChars predicate) - (_, s) => ((), s) -unParser s@(MkPS input (EndOfInput length)) (SkipChars predicate) = - ((), s) --- "Parse" the end of input -unParser s@(MkPS input (AtPoint length location)) ParseEoF = (False, s) -unParser s@(MkPS input (EndOfInput length)) ParseEoF = (True, s) - -export -runParser' : Has Parser fs => - (s : ParserState) -> Eff fs t -> Eff (fs - Parser) (t, ParserState) -runParser' s = - handleRelayS s (\state, t => pure (t, state)) $ \s2, ps, f => - let (a, st) = unParser s2 ps - in f st a - -export -runParser : Has Parser fs => - (s : String) -> Eff fs t -> Eff (fs - Parser) (t, String) -runParser s x = - map (\(x,y) => (x, toString y)) $ runParser' (fromString s) x diff --git a/src/SSG/Parser/Util.idr b/src/SSG/Parser/Util.idr deleted file mode 100644 index 4777f7b..0000000 --- a/src/SSG/Parser/Util.idr +++ /dev/null @@ -1,148 +0,0 @@ -module SSG.Parser.Util - -import SSG.Parser.Core - -import Data.List1 -import Data.Vect -import Data.String -import Control.Eff - -||| Type alias for parsing errors -public export -ParseError : Type -ParseError = String - -||| Type alias for a parser equipped with exception handling -public export -PS : Type -> Type -PS a = Eff [Parser, Except ParseError] a - -||| Run a parser and extact the parsed value -export -runPS : PS a -> (str : String) -> Either String a -runPS x str = - fst . extract . runParser str . runExcept $ x - -||| Run a parser, extracting the parsed value, and throwing an error if the parse was not -||| complete or if it failed -export -runPS' : PS a -> (str : String) -> PS a -runPS' x str = do - (res, rest) <- lift . runParser str . runExcept $ x - unless (null rest) $ throw "Incomplete parse" - rethrow res - -||| Attempt to run a fallible parser, backtracking on failure -export -try : (f : PS a) -> (err : ParseError -> PS a) -> PS a -try f err = do - state <- save - result <- lift . runExcept $ f - case result of - Left e => do - load state - err e - Right result => pure result - -||| Variant of `try` that wraps the result in a `Maybe` -export -tryMaybe : (f : PS a) -> PS (Maybe a) -tryMaybe f = try (map Just f) (\_ => pure Nothing) - -||| Variant of `try` that wraps the result in an `Either` -export -tryEither : (f : PS a) -> PS (Either ParseError a) -tryEither f = try (map Right f) (\e => pure $ Left e) - -||| Attempt to parse each of a list of parsers, returning the first that -||| succeeds -export -oneOfE : (err : ParseError) -> List (PS a) -> PS a -oneOfE err [] = throw err -oneOfE err (x :: xs) = do - res <- tryMaybe x - case res of - Nothing => oneOfE err xs - Just y => pure y - -||| Attempt to parse 0+ of a thing -export -many : (f : PS a) -> PS (List a) -many f = do - Just next <- tryMaybe f - | _ => pure [] - map (next ::) (many f) - -||| Attempt to parse at least one of a thing, giving the supplied error on -||| failure -export -atLeastOne : (err : ParseError) -> (f : PS a) -> PS (List1 a) -atLeastOne err f = do - Just head <- tryMaybe f - | _ => throw err - tail <- many f - pure $ head ::: tail - -||| Attempt to parse an exact string -export -thisString : String -> PS String -thisString str = do - res <- parseExact str - case res of - Got x => pure x - Failed x => throw "Expected \{show str} Got \{show x}" - EoF => throw "Unexpected EoF" - -||| Attempt to parse one of a list of strings -export -theseStrings : List String -> PS String -theseStrings strs = theseStrings' strs - where - theseStrings' : List String -> PS String - theseStrings' [] = throw "Expected one of \{show strs}" - theseStrings' (x :: xs) = do - res <- parseExact x - case res of - Got y => pure y - _ => theseStrings' xs - -||| Attempt to parse one of a list of chars -export -theseChars : List Char -> PS Char -theseChars cs = do - Just [next] <- peek 1 - | _ => throw "Unexpected EoF" - if any (== next) cs - then do - _ <- parseChar (const True) - pure next - else throw "Expected one of \{show cs}, got \{show next}" - -||| Attempt to parse any char not in the list -export -notTheseChars : List Char -> PS Char -notTheseChars cs = do - Just [next] <- peek 1 - | _ => throw "Unexpected EoF" - if any (== next) cs - then throw "Expected not one of \{show cs}, got \{show next}" - else do - _ <- parseChar (const True) - pure next - -||| Parse an exact match, but 'replace' it with the provided value -export -exactReplace : (str : String) -> (replacement : a) -> PS a -exactReplace str replacement = do - _ <- parseExact str - pure replacement - -||| Any character -export -any : PS Char -any = do - x <- parseChar (const True) - case x of - Got y => pure y - (Failed y) => throw "What?" - EoF => throw "Unexpected EoF" diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/Main.idr b/test/djot-to-html/002-linebreaks-and-nbsp/Main.idr deleted file mode 100644 index 97d8771..0000000 --- a/test/djot-to-html/002-linebreaks-and-nbsp/Main.idr +++ /dev/null @@ -1,16 +0,0 @@ -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 parsed = djot contents - putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/expected b/test/djot-to-html/002-linebreaks-and-nbsp/expected deleted file mode 100644 index d344ee1..0000000 --- a/test/djot-to-html/002-linebreaks-and-nbsp/expected +++ /dev/null @@ -1,26 +0,0 @@ - - - -

A paragraph with a normal newline in the middle of it

-

- A paragraph with a hard line break -
- in the middle of it -

-

- A paragraph with a hard line break -
- in the middle of it with extra spaces -

-

- A paragraph with a hard line break -
- in the middle of it with no spaces -

-

A paragraph with an explicit soft line break in the middle of it

-

Multiple soft breaks should coalesce into one

-

Same should apply when mixing explicit and implied soft breaks

-

An escaped space should render as a nonbreaking space

-

We also want to test  multiple   nonbreaking    spaces     in a row

- - \ No newline at end of file diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/run b/test/djot-to-html/002-linebreaks-and-nbsp/run deleted file mode 100644 index 6b5ab53..0000000 --- a/test/djot-to-html/002-linebreaks-and-nbsp/run +++ /dev/null @@ -1,6 +0,0 @@ -rm -rf build/ - -flock "$1" pack -q install-deps test.ipkg -pack -q run test.ipkg - -rm -rf build/ diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/test.dj b/test/djot-to-html/002-linebreaks-and-nbsp/test.dj deleted file mode 100644 index 24e3421..0000000 --- a/test/djot-to-html/002-linebreaks-and-nbsp/test.dj +++ /dev/null @@ -1,22 +0,0 @@ -A paragraph with a normal newline -in the middle of it - -A paragraph with a hard line break \ -in the middle of it - -A paragraph with a hard line break \ -in the middle of it with extra spaces - -A paragraph with a hard line break \ -in the middle of it with no spaces - -A paragraph with an explicit soft line break \n in the middle of it - -Multiple soft breaks should coalesce \n\n\n into one - -Same should apply when mixing explicit \n -and implied soft breaks - -An escaped space\ should render as a nonbreaking space - -We also want to test\ \ multiple\ \ \ nonbreaking\ \ \ \ spaces\ \ \ \ \ in a row diff --git a/test/djot-to-html/002-linebreaks-and-nbsp/test.ipkg b/test/djot-to-html/002-linebreaks-and-nbsp/test.ipkg deleted file mode 100644 index 0efef9e..0000000 --- a/test/djot-to-html/002-linebreaks-and-nbsp/test.ipkg +++ /dev/null @@ -1,7 +0,0 @@ -package a-test - -depends = SSG - -main = Main - -executable = test diff --git a/test/djot-to-html/003-headings/Main.idr b/test/djot-to-html/003-headings/Main.idr deleted file mode 100644 index 97d8771..0000000 --- a/test/djot-to-html/003-headings/Main.idr +++ /dev/null @@ -1,16 +0,0 @@ -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 parsed = djot contents - putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/003-headings/expected b/test/djot-to-html/003-headings/expected deleted file mode 100644 index ae84cb0..0000000 --- a/test/djot-to-html/003-headings/expected +++ /dev/null @@ -1,29 +0,0 @@ - - - -

Level 1 Heading

-

Level 2 Heading

-

Level 3 Heading

-

Level 4 Heading

-
Level 5 Heading
-
Level 6 Heading
-

####### Level 7 Not a Heading

-

# A heading that spans multiple lines

-

# Heading

-

Some content

-

## A sub heading

-

Even more content

-

# Back up

-

Some final content

-

A Multiline Heading

-

## A Level 2 ## Multiline Heading

-

Heading

-

### Not a heading

-

Heading

-

Not a heading

-

A Multiline Heading

-

A Level 2 Multiline Heading

-

A Multiline Heading

-

A Level 2 Multiline Heading

- - \ No newline at end of file diff --git a/test/djot-to-html/003-headings/run b/test/djot-to-html/003-headings/run deleted file mode 100644 index 6b5ab53..0000000 --- a/test/djot-to-html/003-headings/run +++ /dev/null @@ -1,6 +0,0 @@ -rm -rf build/ - -flock "$1" pack -q install-deps test.ipkg -pack -q run test.ipkg - -rm -rf build/ diff --git a/test/djot-to-html/003-headings/test.dj b/test/djot-to-html/003-headings/test.dj deleted file mode 100644 index d6eb8ec..0000000 --- a/test/djot-to-html/003-headings/test.dj +++ /dev/null @@ -1,52 +0,0 @@ -# Level 1 Heading - -## Level 2 Heading - -### Level 3 Heading - -#### Level 4 Heading - -##### Level 5 Heading - -###### Level 6 Heading - -####### Level 7 Not a Heading - -# A heading that -spans multiple lines - -# Heading - -Some content - -## A sub heading - -Even more content - -# Back up - -Some final content - -# A Multiline -# Heading - -## A Level 2 -## Multiline Heading - -## Heading -### Not a heading - -### Heading -## Not a heading - -# A Multiline -Heading - -## A Level 2 -Multiline Heading - -# A Multiline - Heading - -## A Level 2 - Multiline Heading diff --git a/test/djot-to-html/003-headings/test.ipkg b/test/djot-to-html/003-headings/test.ipkg deleted file mode 100644 index 0efef9e..0000000 --- a/test/djot-to-html/003-headings/test.ipkg +++ /dev/null @@ -1,7 +0,0 @@ -package a-test - -depends = SSG - -main = Main - -executable = test diff --git a/test/djot-to-html/004-blockquotes/Main.idr b/test/djot-to-html/004-blockquotes/Main.idr deleted file mode 100644 index 97d8771..0000000 --- a/test/djot-to-html/004-blockquotes/Main.idr +++ /dev/null @@ -1,16 +0,0 @@ -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 parsed = djot contents - putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/004-blockquotes/expected b/test/djot-to-html/004-blockquotes/expected deleted file mode 100644 index 1efa208..0000000 --- a/test/djot-to-html/004-blockquotes/expected +++ /dev/null @@ -1,22 +0,0 @@ - - - -
-

A single line block quote

-
-
-

This is a multi-line blockquote With no linebreaks

-
-
-

This is a multi-line block quote with

-

A line break

-
-
-

- This is a block quote with a -
- hard break in it -

-
- - \ No newline at end of file diff --git a/test/djot-to-html/004-blockquotes/run b/test/djot-to-html/004-blockquotes/run deleted file mode 100644 index 6b5ab53..0000000 --- a/test/djot-to-html/004-blockquotes/run +++ /dev/null @@ -1,6 +0,0 @@ -rm -rf build/ - -flock "$1" pack -q install-deps test.ipkg -pack -q run test.ipkg - -rm -rf build/ diff --git a/test/djot-to-html/004-blockquotes/test.dj b/test/djot-to-html/004-blockquotes/test.dj deleted file mode 100644 index 69790d6..0000000 --- a/test/djot-to-html/004-blockquotes/test.dj +++ /dev/null @@ -1,11 +0,0 @@ -> A single line block quote - -> This is a multi-line blockquote -> With no linebreaks - -> This is a multi-line block quote with -> -> A line break - -> This is a block quote with a \ -> hard break in it diff --git a/test/djot-to-html/004-blockquotes/test.ipkg b/test/djot-to-html/004-blockquotes/test.ipkg deleted file mode 100644 index 0efef9e..0000000 --- a/test/djot-to-html/004-blockquotes/test.ipkg +++ /dev/null @@ -1,7 +0,0 @@ -package a-test - -depends = SSG - -main = Main - -executable = test From db0f3a0427224b67cdd3ee49602b0b1d4737a4f6 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 23 Feb 2025 17:37:13 -0500 Subject: [PATCH 23/33] prep to restart --- SSG.ipkg | 4 +++- src/SSG/Djot.idr | 1 + todo.org | 61 +++++++++++++++++++----------------------------- 3 files changed, 28 insertions(+), 38 deletions(-) create mode 100644 src/SSG/Djot.idr diff --git a/SSG.ipkg b/SSG.ipkg index 6c9228d..d156215 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -13,7 +13,8 @@ authors = "Nathan McCarty" -- langversion -- packages to add to search path -depends = structures +depends = contrib + , structures , tailrec , eff , refined @@ -24,6 +25,7 @@ depends = structures -- modules to install modules = SSG.HTML , SSG.HTML.ElementTypes + , SSG.Djot -- main file (i.e. file to load at REPL) main = Main diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr new file mode 100644 index 0000000..2f11ffc --- /dev/null +++ b/src/SSG/Djot.idr @@ -0,0 +1 @@ +module Djot diff --git a/todo.org b/todo.org index 7f89a0d..330438e 100644 --- a/todo.org +++ b/todo.org @@ -9,54 +9,41 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [7/44] +* Djot [0/31] :PROPERTIES: :COOKIE_DATA: recursive :END: ** Parsing -*** Inline Syntax [2/18] +*** Block Level +**** TODO Paragraph +**** TODO Heading +**** 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 +*** Inline +**** TODO Ordinary Text **** TODO Link **** TODO Image **** TODO Autolink **** TODO Verbatim -**** TODO Emphasis/strong +**** TODO Emphasis/Strong **** TODO Highlighted **** TODO Super/subscript **** TODO Insert/delete -**** TODO Smart punctuation +**** TODO Smart Puncuation **** TODO Math -**** TODO Footnote reference +**** TODO Footnote Reference +**** TODO Linebreak **** TODO Comment **** TODO Symbols -**** TODO Raw inline -**** TODO Span -**** TODO Inline attributes -**** DONE Ordinary Text -**** DONE Linebreak -*** Block Syntax [4/17] -**** 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 -**** TODO definition -**** TODO Footnote -**** TODO Block attributes -**** TODO Links to headings -**** DONE Paragraph -**** DONE Heading -***** DONE Multiline without leading count -***** DONE Basic -** TODO Predictive parsing -** TODO Support all types of whitespace -*** TODO Escaping -*** TODO Whitespace class -** TODO Lazy indentation -** TODO hex escapes -** TODO GFM style alerts -** TODO Group adjacent =Text=s into a =String= -** DONE Rendering +**** TODO Raw Inline +**** TODO Inline Attributes From bd94410c019a6c46a70e4e47023d43ea61b5b6c8 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Sun, 23 Feb 2025 21:34:10 -0500 Subject: [PATCH 24/33] Lines effect --- SSG.ipkg | 2 +- src/SSG/Djot.idr | 2 +- src/SSG/Djot/Lines.idr | 102 ++++++++++++++++++ test/Main.idr | 2 +- test/djot-to-html/001-hello-world/Main.idr | 16 --- test/djot-to-html/001-hello-world/expected | 6 -- test/djot-to-html/001-hello-world/test.dj | 1 - test/hedgehog/001-lines/Main.idr | 28 +++++ test/hedgehog/001-lines/expected | 3 + test/hedgehog/001-lines/pack.toml | 5 + .../001-lines}/run | 2 +- .../001-lines}/test.ipkg | 2 + todo.org | 2 + 13 files changed, 146 insertions(+), 27 deletions(-) create mode 100644 src/SSG/Djot/Lines.idr delete mode 100644 test/djot-to-html/001-hello-world/Main.idr delete mode 100644 test/djot-to-html/001-hello-world/expected delete mode 100644 test/djot-to-html/001-hello-world/test.dj create mode 100644 test/hedgehog/001-lines/Main.idr create mode 100644 test/hedgehog/001-lines/expected create mode 100644 test/hedgehog/001-lines/pack.toml rename test/{djot-to-html/001-hello-world => hedgehog/001-lines}/run (60%) rename test/{djot-to-html/001-hello-world => hedgehog/001-lines}/test.ipkg (65%) diff --git a/SSG.ipkg b/SSG.ipkg index d156215..3b2c315 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -17,7 +17,6 @@ depends = contrib , structures , tailrec , eff - , refined , elab-util , elab-pretty , prettier @@ -26,6 +25,7 @@ depends = contrib modules = SSG.HTML , SSG.HTML.ElementTypes , SSG.Djot + , SSG.Djot.Lines -- main file (i.e. file to load at REPL) main = Main diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr index 2f11ffc..584fa6a 100644 --- a/src/SSG/Djot.idr +++ b/src/SSG/Djot.idr @@ -1 +1 @@ -module Djot +module SSG.Djot diff --git a/src/SSG/Djot/Lines.idr b/src/SSG/Djot/Lines.idr new file mode 100644 index 0000000..f8fa26d --- /dev/null +++ b/src/SSG/Djot/Lines.idr @@ -0,0 +1,102 @@ +||| 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 + +--********************* +--* 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' diff --git a/test/Main.idr b/test/Main.idr index 0437780..b8ffd00 100644 --- a/test/Main.idr +++ b/test/Main.idr @@ -4,5 +4,5 @@ import Test.Golden.RunnerHelper main : IO () main = goldenRunner - [ "Djot -> HTML Golden Values" `atDir` "djot-to-html" + [ "Hedgehog Tests" `atDir` "hedgehog" ] diff --git a/test/djot-to-html/001-hello-world/Main.idr b/test/djot-to-html/001-hello-world/Main.idr deleted file mode 100644 index 97d8771..0000000 --- a/test/djot-to-html/001-hello-world/Main.idr +++ /dev/null @@ -1,16 +0,0 @@ -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 parsed = djot contents - putStr . render . renderHtml $ parsed diff --git a/test/djot-to-html/001-hello-world/expected b/test/djot-to-html/001-hello-world/expected deleted file mode 100644 index 130955a..0000000 --- a/test/djot-to-html/001-hello-world/expected +++ /dev/null @@ -1,6 +0,0 @@ - - - -

Hello World!

- - \ No newline at end of file diff --git a/test/djot-to-html/001-hello-world/test.dj b/test/djot-to-html/001-hello-world/test.dj deleted file mode 100644 index 980a0d5..0000000 --- a/test/djot-to-html/001-hello-world/test.dj +++ /dev/null @@ -1 +0,0 @@ -Hello World! diff --git a/test/hedgehog/001-lines/Main.idr b/test/hedgehog/001-lines/Main.idr new file mode 100644 index 0000000..4d35aff --- /dev/null +++ b/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) + ] + ] diff --git a/test/hedgehog/001-lines/expected b/test/hedgehog/001-lines/expected new file mode 100644 index 0000000..9050bda --- /dev/null +++ b/test/hedgehog/001-lines/expected @@ -0,0 +1,3 @@ +━━━ Lines effect ━━━ + ✓ Lines effect equivalent to lines passed 1000 tests. + ✓ 1 succeeded. diff --git a/test/hedgehog/001-lines/pack.toml b/test/hedgehog/001-lines/pack.toml new file mode 100644 index 0000000..d2e5465 --- /dev/null +++ b/test/hedgehog/001-lines/pack.toml @@ -0,0 +1,5 @@ +[custom.all.SSG] +type = "local" +path = "../../.." +ipkg = "SSG.ipkg" +test = "test/test.ipkg" diff --git a/test/djot-to-html/001-hello-world/run b/test/hedgehog/001-lines/run similarity index 60% rename from test/djot-to-html/001-hello-world/run rename to test/hedgehog/001-lines/run index 6b5ab53..4d6fd1b 100644 --- a/test/djot-to-html/001-hello-world/run +++ b/test/hedgehog/001-lines/run @@ -1,6 +1,6 @@ rm -rf build/ flock "$1" pack -q install-deps test.ipkg -pack -q run test.ipkg +HEDGEHOG_COLOR=0 pack -q run test.ipkg -n 1000 rm -rf build/ diff --git a/test/djot-to-html/001-hello-world/test.ipkg b/test/hedgehog/001-lines/test.ipkg similarity index 65% rename from test/djot-to-html/001-hello-world/test.ipkg rename to test/hedgehog/001-lines/test.ipkg index 0efef9e..e727cbf 100644 --- a/test/djot-to-html/001-hello-world/test.ipkg +++ b/test/hedgehog/001-lines/test.ipkg @@ -1,6 +1,8 @@ package a-test depends = SSG + , hedgehog + , eff main = Main diff --git a/todo.org b/todo.org index 330438e..baee7e9 100644 --- a/todo.org +++ b/todo.org @@ -47,3 +47,5 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Symbols **** TODO Raw Inline **** TODO Inline Attributes +*** Lines effect +**** TODO =IO= Backed implementation From 77890ba54934b3307f2548766996da605cb940b5 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 00:47:28 -0500 Subject: [PATCH 25/33] Parse inline text --- SSG.ipkg | 2 + src/SSG/Djot/Block.idr | 1 + src/SSG/Djot/Inline.idr | 139 ++++++++++++++++++++++++++++++++++++++++ todo.org | 5 +- 4 files changed, 145 insertions(+), 2 deletions(-) create mode 100644 src/SSG/Djot/Block.idr create mode 100644 src/SSG/Djot/Inline.idr diff --git a/SSG.ipkg b/SSG.ipkg index 3b2c315..f9dc0c4 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -26,6 +26,8 @@ modules = SSG.HTML , SSG.HTML.ElementTypes , SSG.Djot , SSG.Djot.Lines + , SSG.Djot.Block + , SSG.Djot.Inline -- main file (i.e. file to load at REPL) main = Main diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr new file mode 100644 index 0000000..5601433 --- /dev/null +++ b/src/SSG/Djot/Block.idr @@ -0,0 +1 @@ +module SSG.Djot.Block diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr new file mode 100644 index 0000000..ecc713d --- /dev/null +++ b/src/SSG/Djot/Inline.idr @@ -0,0 +1,139 @@ +||| Djot inline formatting parser +module SSG.Djot.Inline + +import Control.Eff +import Data.List.Lazy +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 + +%runElab derive "Inline" [Eq, Show, Pretty] + +--****************************** +--* Parsing Utilities * +--****************************** + +||| Type alias for inline parsing +IParser : Type -> Type +IParser t = Eff [State (List Char), Choose] t + +||| Get the next char, modifiying the state +popChar : IParser Char +popChar = do + x :: xs <- get + | [] => empty + put xs + pure x + +||| Get the next char, without modifying the state +peekChar : IParser Char +peekChar = do + x :: xs <- get + | [] => empty + pure x + +||| Attempt to parse something without propagating the failure +try : IParser t -> IParser (Maybe t) +try x = do + state <- get + x <- lift . runChoose {f = Maybe} $ 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 [] = empty +oneOf (x :: xs) = x `alt` oneOf xs + +||| Parse 0+ of something +many : IParser t -> IParser (List t) +many x = do + Just y <- try x + | _ => pure [] + map (y ::) $ many x + +||| Run a parser +runIParser : (str : String) -> IParser t -> Maybe t +runIParser str x = + fst . extract . runState (unpack str) . runChoose {f = Maybe} $ 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) + +-- Definition of pInline +pInline = oneOf + [ text + ] + +--****************************** +--* Post Processing * +--****************************** + +||| Combine adjacent Text entries +combineTexts : List Inline -> List Inline +combineTexts (Text a :: (Text b :: xs)) = + combineTexts (Text (a ++ b) :: xs) +combineTexts xs = xs + +||| Top level post processor +postProcess : List Inline -> List Inline +postProcess xs = 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!"] diff --git a/todo.org b/todo.org index baee7e9..72f3155 100644 --- a/todo.org +++ b/todo.org @@ -9,7 +9,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [0/31] +* Djot [1/33] :PROPERTIES: :COOKIE_DATA: recursive :END: @@ -30,7 +30,8 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Block Attributes **** TODO Heading Links *** Inline -**** TODO Ordinary Text +**** DONE Ordinary Text +**** TODO Escaped Text **** TODO Link **** TODO Image **** TODO Autolink From 86fa9da4743e2593084afa158c2c087a6be4caf9 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 02:18:56 -0500 Subject: [PATCH 26/33] more todos --- todo.org | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/todo.org b/todo.org index 72f3155..f09188d 100644 --- a/todo.org +++ b/todo.org @@ -9,11 +9,11 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [1/33] +* Djot [1/38] :PROPERTIES: :COOKIE_DATA: recursive :END: -** Parsing +** Parsing [1/33] *** Block Level **** TODO Paragraph **** TODO Heading @@ -50,3 +50,10 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Inline Attributes *** Lines effect **** TODO =IO= Backed implementation +*** Known Inaccuracies +** Extensions +*** TODO GFM-style alerts +*** TODO Emoji extension +**** TODO Unicode Emoji +**** TODO Icon font emoji +**** TODO Autolink for source forges From 626245e629546aa3c740cd1cb86643db5342b406 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 02:24:14 -0500 Subject: [PATCH 27/33] Add slurp utility function --- src/SSG/Djot/Lines.idr | 44 ++++++++++++++++++++++++++++++------------ 1 file changed, 32 insertions(+), 12 deletions(-) diff --git a/src/SSG/Djot/Lines.idr b/src/SSG/Djot/Lines.idr index f8fa26d..4bd9483 100644 --- a/src/SSG/Djot/Lines.idr +++ b/src/SSG/Djot/Lines.idr @@ -8,9 +8,9 @@ import Control.Eff -- Only for iutils unit tests import System ---********************* ---* Effect Definition * ---********************* +--************************ +--* Effect Definition * +--************************ export data Lines : Type -> Type where @@ -19,9 +19,9 @@ data Lines : Type -> Type where ||| Take the next line Take : Lines (Maybe String) ---********************* ---* Effect Actions * ---********************* +--************************ +--* Effect Actions * +--************************ export peek : Has Lines fs => Eff fs (Maybe String) @@ -31,9 +31,29 @@ export take : Has Lines fs => Eff fs (Maybe String) take = send Take ---********************* ---* Effect Handlers * ---********************* +--************************ +--* Extra Effect Actions * +--************************ + +||| Take lines until a line matching the given predicate is encountered, dropping the +||| matching line +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 + pure [] + else do + Just x <- take + | _ => pure [] + map (x ::) (slurp predicate) + +--************************ +--* Effect Handlers * +--************************ ||| Split the next line from a string nextLine : String -> Maybe (String, String) @@ -79,9 +99,9 @@ runLines input = let (vv, input3) = unLines input2 lns in f input3 vv ---********************* ---* Unit Tests * ---********************* +--************************ +--* Unit Tests * +--************************ -- @@test runLines Smoke Test runLinesSmoke : IO Bool From a09f3b60dfa736599ab13d9784787f3ffea61523 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 03:37:10 -0500 Subject: [PATCH 28/33] Paragraph parsing --- SSG.ipkg | 1 + src/SSG/Djot/Block.idr | 129 +++++++++++++++++++++++++++++++++++++++++ src/SSG/Djot/Lines.idr | 6 +- todo.org | 8 +-- 4 files changed, 138 insertions(+), 6 deletions(-) diff --git a/SSG.ipkg b/SSG.ipkg index f9dc0c4..2a04ca2 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -19,6 +19,7 @@ depends = contrib , eff , elab-util , elab-pretty + , sop , prettier -- modules to install diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index 5601433..057c7ea 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -1 +1,130 @@ +||| DJot Block formatting parser module SSG.Djot.Block + +import SSG.Djot.Inline +import SSG.Djot.Lines + +import Control.Eff +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 + +%runElab derive "BlockType" [Generic, Show, Eq, DecEq] + +||| A block element +public export +data Block : BlockType -> Type where + Paragraph : (content : List (Inline)) -> Block TParagraph + +%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 + +--* Syntax * + +-- Forward declare for mutual recursion +||| Top level block parser +pBlock : BParser (t : BlockType ** Block t) + +paragraph : BParser (Block TParagraph) +paragraph = do + contents <- map (inline . joinBy "\n") $ slurp blankLine + pure $ Paragraph contents + +-- Definition for top level block parser +pBlock = selectParser paragraph [] + + +--****************************** +--* 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!"]] diff --git a/src/SSG/Djot/Lines.idr b/src/SSG/Djot/Lines.idr index 4bd9483..a445b39 100644 --- a/src/SSG/Djot/Lines.idr +++ b/src/SSG/Djot/Lines.idr @@ -36,7 +36,9 @@ take = send Take --************************ ||| Take lines until a line matching the given predicate is encountered, dropping the -||| matching line +||| 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 @@ -45,7 +47,7 @@ slurp predicate = do if predicate line then do _ <- take - pure [] + slurp predicate else do Just x <- take | _ => pure [] diff --git a/todo.org b/todo.org index f09188d..e3c77c7 100644 --- a/todo.org +++ b/todo.org @@ -9,13 +9,12 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [1/38] +* Djot [2/38] :PROPERTIES: :COOKIE_DATA: recursive :END: -** Parsing [1/33] +** Parsing [2/33] *** Block Level -**** TODO Paragraph **** TODO Heading **** TODO Block Quote **** TODO List Item @@ -29,8 +28,8 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Footnote **** TODO Block Attributes **** TODO Heading Links +**** DONE Paragraph *** Inline -**** DONE Ordinary Text **** TODO Escaped Text **** TODO Link **** TODO Image @@ -48,6 +47,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Symbols **** TODO Raw Inline **** TODO Inline Attributes +**** DONE Ordinary Text *** Lines effect **** TODO =IO= Backed implementation *** Known Inaccuracies From 135b8782339480fba3c00432a07c193c7b0cf063 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 04:23:25 -0500 Subject: [PATCH 29/33] HTML rendering --- SSG.ipkg | 1 + src/SSG/Djot.idr | 4 ++++ src/SSG/Djot/Render.idr | 37 +++++++++++++++++++++++++++++++++++++ todo.org | 1 + 4 files changed, 43 insertions(+) create mode 100644 src/SSG/Djot/Render.idr diff --git a/SSG.ipkg b/SSG.ipkg index 2a04ca2..f462141 100644 --- a/SSG.ipkg +++ b/SSG.ipkg @@ -29,6 +29,7 @@ modules = SSG.HTML , SSG.Djot.Lines , SSG.Djot.Block , SSG.Djot.Inline + , SSG.Djot.Render -- main file (i.e. file to load at REPL) main = Main diff --git a/src/SSG/Djot.idr b/src/SSG/Djot.idr index 584fa6a..0fb4599 100644 --- a/src/SSG/Djot.idr +++ b/src/SSG/Djot.idr @@ -1 +1,5 @@ module SSG.Djot + +import public SSG.Djot.Inline +import public SSG.Djot.Block +import public SSG.Djot.Render diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr new file mode 100644 index 0000000..73cf01b --- /dev/null +++ b/src/SSG/Djot/Render.idr @@ -0,0 +1,37 @@ +||| Render Djot to HTML +module SSG.Djot.Render + +import SSG.HTML +import SSG.Djot.Inline +import SSG.Djot.Block + +||| Render a single inline element as HTML +export +renderInline : Inline -> (t ** Html t) +-- FIXME: escape text +renderInline (Text text) = (_ ** Text text) + +||| Render a list of inline elments to html +export +renderInlines : List Inline -> (types ** DList _ Html types) +renderInlines xs = fromList $ 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))) + +renderBlocks xs = dMap' (\_, x => renderBlock x) xs + +||| Render a complete html document from a list of block level elements +renderDocument : {types : _} -> DList _ Block types -> Html "html" +renderDocument xs = + Normal "html" ["lang" =$ "en"] [ + Normal "body" [] (snd (renderBlocks xs)) + ] diff --git a/todo.org b/todo.org index e3c77c7..ce5e9de 100644 --- a/todo.org +++ b/todo.org @@ -3,6 +3,7 @@ ** 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 From 2e66b03baa41ff751d6303d53091189cda6880ee Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 04:41:09 -0500 Subject: [PATCH 30/33] Paragraph testing --- src/SSG/Djot/Block.idr | 12 +++++++++++- src/SSG/Djot/Lines.idr | 6 +++++- src/SSG/Djot/Render.idr | 1 + test/Main.idr | 1 + test/djotToHtml/001-paragraph/Main.idr | 18 ++++++++++++++++++ test/djotToHtml/001-paragraph/expected | 12 ++++++++++++ test/djotToHtml/001-paragraph/pack.toml | 5 +++++ test/djotToHtml/001-paragraph/run | 6 ++++++ test/djotToHtml/001-paragraph/test.dj | 12 ++++++++++++ test/djotToHtml/001-paragraph/test.ipkg | 9 +++++++++ 10 files changed, 80 insertions(+), 2 deletions(-) create mode 100644 test/djotToHtml/001-paragraph/Main.idr create mode 100644 test/djotToHtml/001-paragraph/expected create mode 100644 test/djotToHtml/001-paragraph/pack.toml create mode 100644 test/djotToHtml/001-paragraph/run create mode 100644 test/djotToHtml/001-paragraph/test.dj create mode 100644 test/djotToHtml/001-paragraph/test.ipkg diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index 057c7ea..d2b0677 100644 --- a/src/SSG/Djot/Block.idr +++ b/src/SSG/Djot/Block.idr @@ -127,4 +127,14 @@ golden input ref = do -- @@test Paragraph Smoke smokeParagraph : IO Bool -smokeParagraph = golden "Hello World!" [Paragraph [Text "Hello World!"]] +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!"]] diff --git a/src/SSG/Djot/Lines.idr b/src/SSG/Djot/Lines.idr index a445b39..4108762 100644 --- a/src/SSG/Djot/Lines.idr +++ b/src/SSG/Djot/Lines.idr @@ -47,7 +47,11 @@ slurp predicate = do if predicate line then do _ <- take - slurp predicate + Just next <- peek + | _ => pure [] + if predicate next + then slurp predicate + else pure [] else do Just x <- take | _ => pure [] diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index 73cf01b..a2a0092 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -30,6 +30,7 @@ renderBlock (Paragraph content) = 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"] [ diff --git a/test/Main.idr b/test/Main.idr index b8ffd00..04cd676 100644 --- a/test/Main.idr +++ b/test/Main.idr @@ -5,4 +5,5 @@ import Test.Golden.RunnerHelper main : IO () main = goldenRunner [ "Hedgehog Tests" `atDir` "hedgehog" + , "Djot -> HTML Tests" `atDir` "djotToHtml" ] diff --git a/test/djotToHtml/001-paragraph/Main.idr b/test/djotToHtml/001-paragraph/Main.idr new file mode 100644 index 0000000..64b3cdf --- /dev/null +++ b/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 diff --git a/test/djotToHtml/001-paragraph/expected b/test/djotToHtml/001-paragraph/expected new file mode 100644 index 0000000..d83d19b --- /dev/null +++ b/test/djotToHtml/001-paragraph/expected @@ -0,0 +1,12 @@ + + + +

Hello World!

+

Hello Alice!

+

A Multi-line +Paragraph

+

Two line breaks

+

A multiline paragraph + with some indentation

+ + diff --git a/test/djotToHtml/001-paragraph/pack.toml b/test/djotToHtml/001-paragraph/pack.toml new file mode 100644 index 0000000..d2e5465 --- /dev/null +++ b/test/djotToHtml/001-paragraph/pack.toml @@ -0,0 +1,5 @@ +[custom.all.SSG] +type = "local" +path = "../../.." +ipkg = "SSG.ipkg" +test = "test/test.ipkg" diff --git a/test/djotToHtml/001-paragraph/run b/test/djotToHtml/001-paragraph/run new file mode 100644 index 0000000..6b5ab53 --- /dev/null +++ b/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/ diff --git a/test/djotToHtml/001-paragraph/test.dj b/test/djotToHtml/001-paragraph/test.dj new file mode 100644 index 0000000..d4ab1bf --- /dev/null +++ b/test/djotToHtml/001-paragraph/test.dj @@ -0,0 +1,12 @@ +Hello World! + +Hello Alice! + +A Multi-line +Paragraph + + +Two line breaks + +A multiline paragraph + with some indentation diff --git a/test/djotToHtml/001-paragraph/test.ipkg b/test/djotToHtml/001-paragraph/test.ipkg new file mode 100644 index 0000000..e727cbf --- /dev/null +++ b/test/djotToHtml/001-paragraph/test.ipkg @@ -0,0 +1,9 @@ +package a-test + +depends = SSG + , hedgehog + , eff + +main = Main + +executable = test From e4fe5f98e68d5843e3254ae65d0bb248cdd13e2e Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 05:20:59 -0500 Subject: [PATCH 31/33] Soft line break support --- src/SSG/Djot/Inline.idr | 108 ++++++++++++++++++++++--- src/SSG/Djot/Render.idr | 9 ++- test/djotToHtml/001-paragraph/expected | 12 ++- 3 files changed, 111 insertions(+), 18 deletions(-) diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index ecc713d..80d11f1 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -2,7 +2,7 @@ module SSG.Djot.Inline import Control.Eff -import Data.List.Lazy +import Data.List1 import Data.Maybe import Data.String import Derive.Prelude @@ -21,6 +21,7 @@ import System public export data Inline : Type where Text : (text : String) -> Inline + SoftLineBreak : Inline %runElab derive "Inline" [Eq, Show, Pretty] @@ -30,13 +31,13 @@ data Inline : Type where ||| Type alias for inline parsing IParser : Type -> Type -IParser t = Eff [State (List Char), Choose] t +IParser t = Eff [State (List Char), Fail] t ||| Get the next char, modifiying the state popChar : IParser Char popChar = do x :: xs <- get - | [] => empty + | [] => fail put xs pure x @@ -44,24 +45,32 @@ popChar = do peekChar : IParser Char peekChar = do x :: xs <- get - | [] => empty + | [] => fail pure x ||| Attempt to parse something without propagating the failure try : IParser t -> IParser (Maybe t) try x = do state <- get - x <- lift . runChoose {f = Maybe} $ x + 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 [] = empty -oneOf (x :: xs) = x `alt` oneOf xs +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) @@ -70,10 +79,44 @@ many x = do | _ => 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) . runChoose {f = Maybe} $ x + fst . extract . runState (unpack str) . runFail $ x --****************************** --* Syntax * @@ -89,9 +132,23 @@ 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 () + -- Definition of pInline pInline = oneOf - [ text + [ softLineBreak + , text ] --****************************** @@ -100,13 +157,22 @@ pInline = oneOf ||| Combine adjacent Text entries combineTexts : List Inline -> List Inline +combineTexts [] = [] combineTexts (Text a :: (Text b :: xs)) = combineTexts (Text (a ++ b) :: xs) -combineTexts xs = 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 = combineTexts xs +postProcess xs = removeTrailingSoftbreak . combineTexts $ xs --****************************** --* Top Level Parsing Function * @@ -137,3 +203,23 @@ golden input reference = do 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!"] diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index a2a0092..a6b8b03 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -5,16 +5,19 @@ import SSG.HTML import SSG.Djot.Inline import SSG.Djot.Block +import Data.List + ||| Render a single inline element as HTML export -renderInline : Inline -> (t ** Html t) +renderInline : Inline -> Maybe (t ** Html t) -- FIXME: escape text -renderInline (Text text) = (_ ** Text text) +renderInline (Text text) = Just (_ ** Text text) +renderInline SoftLineBreak = Nothing ||| Render a list of inline elments to html export renderInlines : List Inline -> (types ** DList _ Html types) -renderInlines xs = fromList $ map renderInline xs +renderInlines xs = fromList . catMaybes $ map renderInline xs ||| Render a single block element as HTML export diff --git a/test/djotToHtml/001-paragraph/expected b/test/djotToHtml/001-paragraph/expected index d83d19b..6875061 100644 --- a/test/djotToHtml/001-paragraph/expected +++ b/test/djotToHtml/001-paragraph/expected @@ -3,10 +3,14 @@

Hello World!

Hello Alice!

-

A Multi-line -Paragraph

+

+ A Multi-line + Paragraph +

Two line breaks

-

A multiline paragraph - with some indentation

+

+ A multiline paragraph + with some indentation +

From 72c73ec99d31587297f0c8d626b7e8a3a7faddaa Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 05:28:06 -0500 Subject: [PATCH 32/33] Hard line break support --- src/SSG/Djot/Inline.idr | 17 ++++++++++++++++- src/SSG/Djot/Render.idr | 1 + test/djotToHtml/001-paragraph/expected | 17 +++++++++++++++++ test/djotToHtml/001-paragraph/test.dj | 11 +++++++++++ todo.org | 6 +++--- 5 files changed, 48 insertions(+), 4 deletions(-) diff --git a/src/SSG/Djot/Inline.idr b/src/SSG/Djot/Inline.idr index 80d11f1..d547c43 100644 --- a/src/SSG/Djot/Inline.idr +++ b/src/SSG/Djot/Inline.idr @@ -22,6 +22,7 @@ public export data Inline : Type where Text : (text : String) -> Inline SoftLineBreak : Inline + HardLineBreak : Inline %runElab derive "Inline" [Eq, Show, Pretty] @@ -145,9 +146,18 @@ softLineBreak = do _ <- many horiz pure () +hardLineBreak : IParser Inline +hardLineBreak = do + _ <- exactly "\\" + _ <- many horiz + _ <- vert + _ <- many horiz + pure HardLineBreak + -- Definition of pInline pInline = oneOf - [ softLineBreak + [ hardLineBreak + , softLineBreak , text ] @@ -223,3 +233,8 @@ testTrailingSoftLineBreak = 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!"] diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index a6b8b03..b610349 100644 --- a/src/SSG/Djot/Render.idr +++ b/src/SSG/Djot/Render.idr @@ -13,6 +13,7 @@ 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 diff --git a/test/djotToHtml/001-paragraph/expected b/test/djotToHtml/001-paragraph/expected index 6875061..612076b 100644 --- a/test/djotToHtml/001-paragraph/expected +++ b/test/djotToHtml/001-paragraph/expected @@ -12,5 +12,22 @@ 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 +

diff --git a/test/djotToHtml/001-paragraph/test.dj b/test/djotToHtml/001-paragraph/test.dj index d4ab1bf..1525f0b 100644 --- a/test/djotToHtml/001-paragraph/test.dj +++ b/test/djotToHtml/001-paragraph/test.dj @@ -10,3 +10,14 @@ 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 diff --git a/todo.org b/todo.org index ce5e9de..cce0eed 100644 --- a/todo.org +++ b/todo.org @@ -10,11 +10,11 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [2/38] +* Djot [3/38] :PROPERTIES: :COOKIE_DATA: recursive :END: -** Parsing [2/33] +** Parsing [3/33] *** Block Level **** TODO Heading **** TODO Block Quote @@ -43,12 +43,12 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Smart Puncuation **** TODO Math **** TODO Footnote Reference -**** TODO Linebreak **** TODO Comment **** TODO Symbols **** TODO Raw Inline **** TODO Inline Attributes **** DONE Ordinary Text +**** DONE Linebreak *** Lines effect **** TODO =IO= Backed implementation *** Known Inaccuracies From 6263a02f891cbeb1efa65049ecb86f69c13310b1 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Thu, 27 Feb 2025 21:05:04 -0500 Subject: [PATCH 33/33] Heading support --- src/SSG/Djot/Block.idr | 103 +++++++++++++++++++++++-- src/SSG/Djot/Lines.idr | 7 ++ src/SSG/Djot/Render.idr | 15 ++++ test/djotToHtml/002-headings/Main.idr | 18 +++++ test/djotToHtml/002-headings/expected | 44 +++++++++++ test/djotToHtml/002-headings/pack.toml | 5 ++ test/djotToHtml/002-headings/run | 6 ++ test/djotToHtml/002-headings/test.dj | 38 +++++++++ test/djotToHtml/002-headings/test.ipkg | 9 +++ todo.org | 16 +++- 10 files changed, 251 insertions(+), 10 deletions(-) create mode 100644 test/djotToHtml/002-headings/Main.idr create mode 100644 test/djotToHtml/002-headings/expected create mode 100644 test/djotToHtml/002-headings/pack.toml create mode 100644 test/djotToHtml/002-headings/run create mode 100644 test/djotToHtml/002-headings/test.dj create mode 100644 test/djotToHtml/002-headings/test.ipkg diff --git a/src/SSG/Djot/Block.idr b/src/SSG/Djot/Block.idr index d2b0677..64bc98a 100644 --- a/src/SSG/Djot/Block.idr +++ b/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"]] diff --git a/src/SSG/Djot/Lines.idr b/src/SSG/Djot/Lines.idr index 4108762..1dd7a8b 100644 --- a/src/SSG/Djot/Lines.idr +++ b/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 * --************************ diff --git a/src/SSG/Djot/Render.idr b/src/SSG/Djot/Render.idr index b610349..2e7aebd 100644 --- a/src/SSG/Djot/Render.idr +++ b/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 diff --git a/test/djotToHtml/002-headings/Main.idr b/test/djotToHtml/002-headings/Main.idr new file mode 100644 index 0000000..64b3cdf --- /dev/null +++ b/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 diff --git a/test/djotToHtml/002-headings/expected b/test/djotToHtml/002-headings/expected new file mode 100644 index 0000000..950af1d --- /dev/null +++ b/test/djotToHtml/002-headings/expected @@ -0,0 +1,44 @@ + + + +

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) +

+ + diff --git a/test/djotToHtml/002-headings/pack.toml b/test/djotToHtml/002-headings/pack.toml new file mode 100644 index 0000000..d2e5465 --- /dev/null +++ b/test/djotToHtml/002-headings/pack.toml @@ -0,0 +1,5 @@ +[custom.all.SSG] +type = "local" +path = "../../.." +ipkg = "SSG.ipkg" +test = "test/test.ipkg" diff --git a/test/djotToHtml/002-headings/run b/test/djotToHtml/002-headings/run new file mode 100644 index 0000000..6b5ab53 --- /dev/null +++ b/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/ diff --git a/test/djotToHtml/002-headings/test.dj b/test/djotToHtml/002-headings/test.dj new file mode 100644 index 0000000..3f1319e --- /dev/null +++ b/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) diff --git a/test/djotToHtml/002-headings/test.ipkg b/test/djotToHtml/002-headings/test.ipkg new file mode 100644 index 0000000..e727cbf --- /dev/null +++ b/test/djotToHtml/002-headings/test.ipkg @@ -0,0 +1,9 @@ +package a-test + +depends = SSG + , hedgehog + , eff + +main = Main + +executable = test diff --git a/todo.org b/todo.org index cce0eed..df1305b 100644 --- a/todo.org +++ b/todo.org @@ -10,13 +10,12 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se ** TODO Refine =location= in =ParserLocation= ** TODO Error messages ** TODO Combinators for predictive parsing -* Djot [3/38] +* Djot [4/40] :PROPERTIES: :COOKIE_DATA: recursive :END: -** Parsing [3/33] +** Parsing [4/34] *** Block Level -**** TODO Heading **** TODO Block Quote **** TODO List Item **** TODO List @@ -30,6 +29,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Block Attributes **** TODO Heading Links **** DONE Paragraph +**** DONE Heading *** Inline **** TODO Escaped Text **** TODO Link @@ -40,7 +40,7 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se **** TODO Highlighted **** TODO Super/subscript **** TODO Insert/delete -**** TODO Smart Puncuation +**** TODO Smart Punctuation **** TODO Math **** TODO Footnote Reference **** TODO Comment @@ -52,9 +52,17 @@ Decided to rename =Tag= to =Html=, and =Raw= to =Text=, which makes this make se *** 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