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