Undo everything to switch over to an event based parser
This commit is contained in:
parent
7ef90867f2
commit
81a7f09623
25 changed files with 1 additions and 1414 deletions
27
src/Djot.idr
27
src/Djot.idr
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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)
|
||||
|
|
@ -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 ]
|
||||
|
|
@ -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
|
||||
|
|
@ -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"
|
||||
Loading…
Add table
Add a link
Reference in a new issue