
   0 | module Text.Markdown.Parser
   1 | 
   2 | import Data.List
   3 | import Text.Parser
   4 | import Text.Token
   5 | 
   6 | import Text.Markdown.Errors
   7 | import Text.Markdown.Lexer
   8 | import Text.Markdown.Data
   9 | 
  10 | import Language.Reflection
  11 | import Language.Reflection.Syntax
  12 | import Language.Reflection.Syntax.Ops
  13 | 
  14 | import public Text.Markdown.Tokens
  15 | 
  16 | %default total
  17 | %language ElabReflection
  18 | 
  19 | --------------------------------------------------------------------------------
  20 | -- Utils
  21 | --------------------------------------------------------------------------------
  22 | 
  23 | ||| Check that a HTML closing tag matches the opening tag.
  24 | private
  25 | checkTag : String -> String -> Grammar state MarkdownToken False ()
  26 | checkTag x y = if x == y then pure () else fail "tag mismatch"
  27 | 
  28 | ||| Converts a list of strings to a list of variables.
  29 | private
  30 | toListTTImp : List String -> TTImp
  31 | toListTTImp [] = var "Nil"
  32 | toListTTImp (x :: xs) = var "::" .$ var (fromString x) .$ (toListTTImp xs)
  33 | 
  34 | ||| Generates a list of inline grammars from a list of strings.
  35 | |||
  36 | ||| This allows to:
  37 | |||
  38 | ||| 1) list all inline grammars in the `listInline` function;
  39 | ||| 2) remove the ones which are not needed using the `delete` or `deletes`
  40 | |||    function;
  41 | ||| 3) run the elaboration with this function to generate the final list.
  42 | |||
  43 | ||| As this happens at compile time, there is no impact on the performance and
  44 | ||| the totality checker can then check that the provided list is not
  45 | ||| recursive.
  46 | private
  47 | toListElab :
  48 |      List String
  49 |   -> Elab (List (Grammar state MarkdownToken True Inline))
  50 | toListElab list = check (toListTTImp list)
  51 | 
  52 | ||| Deletes multiple elements from a list.
  53 | |||
  54 | ||| The first argument is the list of elements to delete.
  55 | ||| The second argument is the list to delete from.
  56 | private
  57 | deletes : Eq a => List a -> List a -> List a
  58 | deletes [] list = list
  59 | deletes (x :: xs) list = deletes xs (delete x list)
  60 | 
  61 | ||| Parses an instance of `p` that is between `q`.
  62 | private
  63 | quote :
  64 |      {c : Bool}
  65 |   -> (q : Grammar state tok True l)
  66 |   -> (p : Grammar state tok c a)
  67 |   -> Grammar state tok True a
  68 | quote q contents = q *> contents <* q
  69 | 
  70 | ||| List of inline grammars defined as strings.
  71 | |||
  72 | ||| We then user elab to convert those strings to variables.
  73 | ||| Such variables must have already been defined and must be of type
  74 | ||| `Grammar state MarkdownToken True Inline`.
  75 | private
  76 | listInline : List String
  77 | listInline =
  78 |   [ "pre"
  79 |   , "html"
  80 |   , "italics"
  81 |   , "bold"
  82 |   , "image"
  83 |   , "link"
  84 |   , "newline"
  85 |   , "text"
  86 |   , "textBoldSym"
  87 |   , "textItalicsSym"
  88 |   , "textImageStart"
  89 |   , "textOpeningBracket"
  90 |   , "textClosingBracket"
  91 |   , "textOpeningParenthesis"
  92 |   , "textClosingParenthesis"
  93 |   , "textUListSym"
  94 |   , "textUListSepSym"
  95 |   , "closeTag"
  96 |   ]
  97 | 
  98 | --------------------------------------------------------------------------------
  99 | -- Grammar
 100 | --------------------------------------------------------------------------------
 101 | 
 102 | private
 103 | blankLine : Grammar state MarkdownToken True ()
 104 | blankLine = const () <$> match BlankLine
 105 | 
 106 | ||| Terminates a paragraph.
 107 | |||
 108 | ||| It can be:
 109 | |||
 110 | ||| - a blank line; or
 111 | ||| - the end of the file.
 112 | private
 113 | blockTerminal : Grammar state MarkdownToken False ()
 114 | blockTerminal = blankLine <|> eof
 115 | 
 116 | private
 117 | closer : String -> Grammar state MarkdownToken True ()
 118 | closer tag = do
 119 |   closeTag <- match HtmlCloseTag
 120 |   checkTag closeTag tag
 121 | 
 122 | private
 123 | closeTag : Grammar state MarkdownToken True Inline
 124 | closeTag = Text <$> match HtmlCloseTag
 125 | 
 126 | private
 127 | codeBlock : Grammar state MarkdownToken True Block
 128 | codeBlock = uncurry CodeBlock <$> match MdCodeBlock
 129 | 
 130 | private
 131 | horizontalRules : Grammar state MarkdownToken True Block
 132 | horizontalRules = const HorizontalRules <$> match MdHorizontalRules
 133 | 
 134 | private
 135 | newline : Grammar state MarkdownToken True Inline
 136 | newline =
 137 |   -- Standardise newlines to '\n' character.
 138 |   const (Text "\n") <$> match MdNewLine
 139 | 
 140 | private
 141 | pre : Grammar state MarkdownToken True Inline
 142 | pre = Pre <$> match MdPre
 143 | 
 144 | private
 145 | text : Grammar state MarkdownToken True Inline
 146 | text = Text <$> match MdText
 147 | 
 148 | private
 149 | textBoldSym : Grammar state MarkdownToken True Inline
 150 | textBoldSym = Text <$> match BoldSym
 151 | 
 152 | private
 153 | textImageStart : Grammar state MarkdownToken True Inline
 154 | textImageStart = Text <$> match ImageStart
 155 | 
 156 | private
 157 | textItalicsSym : Grammar state MarkdownToken True Inline
 158 | textItalicsSym = Text <$> match ItalicsSym
 159 | 
 160 | private
 161 | textClosingBracket : Grammar state MarkdownToken True Inline
 162 | textClosingBracket = Text <$> match ClosingBracket
 163 | 
 164 | private
 165 | textClosingParenthesis : Grammar state MarkdownToken True Inline
 166 | textClosingParenthesis = Text <$> match ClosingParenthesis
 167 | 
 168 | private
 169 | textOpeningBracket : Grammar state MarkdownToken True Inline
 170 | textOpeningBracket = Text <$> match OpeningBracket
 171 | 
 172 | private
 173 | textOpeningParenthesis : Grammar state MarkdownToken True Inline
 174 | textOpeningParenthesis = Text <$> match OpeningParenthesis
 175 | 
 176 | private
 177 | textUListSym : Grammar state MarkdownToken True Inline
 178 | textUListSym = Text <$> match UListSym
 179 | 
 180 | private
 181 | textUListSepSym : Grammar state MarkdownToken True Inline
 182 | textUListSepSym = Text <$> match UListSepSym
 183 | 
 184 | mutual
 185 |   private
 186 |   markdown : Grammar state MarkdownToken False Markdown
 187 |   markdown = do
 188 |     els <- many $ choice
 189 |              [ Just <$> horizontalRules
 190 |              , const Nothing <$> blankLine
 191 |              , Just <$> codeBlock
 192 |              , Just <$> header
 193 |              , Just <$> uList
 194 |              , Just <$> paragraph
 195 |              ]
 196 |     pure $ Doc $ mapMaybe id els
 197 | 
 198 |   private
 199 |   inline : Grammar state MarkdownToken True Inline
 200 |   inline = choice (%runElab toListElab listInline)
 201 | 
 202 |   private
 203 |   header : Grammar state MarkdownToken True Block
 204 |   header = do
 205 |     level <- match HeadingSym
 206 |     commit
 207 |     contents <- someTill blockTerminal inline
 208 |     pure $ Header level $ toList contents
 209 | 
 210 |   private
 211 |   uList : Grammar state MarkdownToken True Block
 212 |   uList =
 213 |     let
 214 |     uListInline =
 215 |       choice $ %runElab toListElab $ delete "textUListSepSym" listInline
 216 |     in
 217 |     do
 218 |       _ <- match UListSym
 219 |       items <- sepBy1 (match UListSepSym) (some uListInline)
 220 |       pure $ UList $ toList $ map toList items
 221 | 
 222 |   private
 223 |   paragraph : Grammar state MarkdownToken True Block
 224 |   paragraph = do
 225 |     contents <- some inline
 226 |     pure $ Paragraph $ toList contents
 227 | 
 228 |   ||| Generic bold grammar.
 229 |   |||
 230 |   ||| The accepted inline grammars within bold can be provided as argument.
 231 |   ||| This is done this way to avoid infinite recursion. Typically, a `link`
 232 |   ||| should not be accepted anymore if the bold element is already within a
 233 |   ||| link.
 234 |   private
 235 |   boldGen :
 236 |        List (Grammar state MarkdownToken True Inline)
 237 |     -> Grammar state MarkdownToken True Inline
 238 |   boldGen inlineBold =
 239 |     Bold . toList <$> (quote (match BoldSym) $ some $ choice inlineBold)
 240 | 
 241 |   ||| Base for inline bold grammars.
 242 |   listInlineBold : List String
 243 |   listInlineBold = deletes
 244 |     [ "bold"
 245 |     , "italics"
 246 |     , "link"
 247 |     , "textBoldSym"
 248 |     ]
 249 |     -- Use a link grammar without bold to avoid infinite recursion.
 250 |     ("linkNoBold" :: "italicsNoLinkNoBold" :: listInline)
 251 | 
 252 |   ||| Bold content between two bold symbols.
 253 |   |||
 254 |   ||| Note: we take all the inline content which is in between including
 255 |   ||| newlines. This means that bold can span accross multiple lines.
 256 |   private
 257 |   bold : Grammar state MarkdownToken True Inline
 258 |   bold = boldGen $ %runElab toListElab $ listInlineBold
 259 | 
 260 |   ||| Bold content between two bold symbols without italic.
 261 |   |||
 262 |   ||| This is to be called within the italic grammar to avoid infinite recursion.
 263 |   private
 264 |   boldNoItalic : Grammar state MarkdownToken True Inline
 265 |   boldNoItalic = boldGen
 266 |     $ %runElab toListElab
 267 |     $ delete "textItalicsSym" ("boldNoLinkNoItalic" :: listInlineBold)
 268 | 
 269 |   ||| Bold content between two bold symbols without link nor italic.
 270 |   |||
 271 |   ||| This is to be called within the link grammar to avoid infinite recursion.
 272 |   private
 273 |   boldNoLinkNoItalic : Grammar state MarkdownToken True Inline
 274 |   boldNoLinkNoItalic = boldGen $ %runElab toListElab $ deletes
 275 |     [ "linkNoBold"
 276 |     , "textItalicsSym"
 277 |     ]
 278 |     listInlineBold
 279 | 
 280 |   ||| Generic italic grammar.
 281 |   |||
 282 |   ||| The accepted inline grammars within italic can be provided as argument.
 283 |   ||| This is done this way to avoid infinite recursion. Typically, a `link`
 284 |   ||| should not be accepted anymore if the italic element is already within a
 285 |   ||| link.
 286 |   private
 287 |   italicsGen :
 288 |        List (Grammar state MarkdownToken True Inline)
 289 |     -> Grammar state MarkdownToken True Inline
 290 |   italicsGen inlineItalic =
 291 |     Italics . toList <$> (quote (match ItalicsSym) $ some $ choice inlineItalic)
 292 | 
 293 |   ||| Base for inline italic grammars.
 294 |   listInlineItalics : List String
 295 |   listInlineItalics = deletes
 296 |     [ "italics"
 297 |     , "link"
 298 |     , "textItalicsSym"
 299 |     ]
 300 |     -- Use a link grammar without bold to avoid infinite recursion.
 301 |     ("linkNoItalic" :: listInline)
 302 | 
 303 |   ||| Italic content between two italic symbols.
 304 |   |||
 305 |   ||| Note: we take all the inline content which is in between including
 306 |   ||| newlines. This means that italic can span accross multiple lines.
 307 |   private
 308 |   italics : Grammar state MarkdownToken True Inline
 309 |   italics = italicsGen $ %runElab toListElab listInlineItalics
 310 | 
 311 |   ||| Italic content between two italic symbols within bold.
 312 |   private
 313 |   italicsNoBold : Grammar state MarkdownToken True Inline
 314 |   italicsNoBold = italicsGen $ %runElab toListElab $ deletes
 315 |         [ "bold"
 316 |         , "textBoldSym"
 317 |         ]
 318 |         listInlineItalics
 319 | 
 320 |   ||| Italic content between two bold symbols without link nor bold.
 321 |   |||
 322 |   ||| This is to be called within the link grammar to avoid infinite recursion.
 323 |   private
 324 |   italicsNoLinkNoBold : Grammar state MarkdownToken True Inline
 325 |   italicsNoLinkNoBold = italicsGen $ %runElab toListElab $ deletes
 326 |     [ "bold"
 327 |     , "textBoldSym"
 328 |     , "linkNoItalic"
 329 |     ]
 330 |     listInlineItalics
 331 | 
 332 |   private
 333 |   image : Grammar state MarkdownToken True Inline
 334 |   image =
 335 |     let
 336 |       altText = choice $ %runElab toListElab $ deletes
 337 |         [ "pre"
 338 |         , "html"
 339 |         , "italics"
 340 |         , "bold"
 341 |         , "image"
 342 |         , "link"
 343 |         , "newline"
 344 |         , "textClosingBracket"
 345 |         , "textUListSepSym"
 346 |         ]
 347 |         listInline
 348 | 
 349 |       srcText = choice $ %runElab toListElab $ deletes
 350 |         [ "pre"
 351 |         , "html"
 352 |         , "italics"
 353 |         , "bold"
 354 |         , "image"
 355 |         , "link"
 356 |         , "newline"
 357 |         , "textClosingParenthesis"
 358 |         , "textUListSepSym"
 359 |         ]
 360 |         listInline
 361 |     in
 362 |     do
 363 |       _   <- match ImageStart
 364 |       alt <- some altText
 365 |       _   <- match ClosingBracket
 366 |       _   <- optional (match MdNewLine)
 367 |       _   <- match OpeningParenthesis
 368 |       src <- some srcText
 369 |       _   <- match ClosingParenthesis
 370 |       pure $
 371 |         Image (concatInlineVals $ toList alt) (concatInlineVals $ toList src)
 372 | 
 373 |   ||| Generic link syntax which can then be specialised for precise use cases.
 374 |   |||
 375 |   ||| We do not always want to parse the same inline elements for the link
 376 |   ||| description to avoid infinite recursion.
 377 |   private
 378 |   linkGen :
 379 |        List (Grammar state MarkdownToken True Inline)
 380 |     -> Grammar state MarkdownToken True Inline
 381 |   linkGen desc =
 382 |     let
 383 |       descText = choice desc
 384 |       hrefText = choice $ %runElab toListElab $ deletes
 385 |         [ "pre"
 386 |         , "html"
 387 |         , "italics"
 388 |         , "bold"
 389 |         , "image"
 390 |         , "link"
 391 |         , "newline"
 392 |         , "textClosingParenthesis"
 393 |         , "textUListSepSym"
 394 |         ]
 395 |         listInline
 396 |     in
 397 |     do
 398 |       _    <- match OpeningBracket
 399 |       desc <- some descText
 400 |       _    <- match ClosingBracket
 401 |       _    <- optional (match MdNewLine)
 402 |       _    <- match OpeningParenthesis
 403 |       href <- some hrefText
 404 |       _    <- match ClosingParenthesis
 405 |       pure $ Link (toList desc) (concatInlineVals $ toList href)
 406 | 
 407 |   ||| Base list for inline links.
 408 |   private
 409 |   listInlineLink : List String
 410 |   listInlineLink = deletes
 411 |     [ "pre"
 412 |     , "html"
 413 |     , "image"
 414 |     , "link"
 415 |     , "newline"
 416 |     , "textClosingBracket"
 417 |     , "textUListSepSym"
 418 |     ]
 419 |     listInline
 420 | 
 421 |   private
 422 |   link : Grammar state MarkdownToken True Inline
 423 |   link = linkGen $ %runElab toListElab listInlineLink
 424 | 
 425 |   ||| Link without bold text.
 426 |   |||
 427 |   ||| This is to be used within bold text. As the text is already bold, we don't
 428 |   ||| want to have again bold within the link to avoid infinite recursion.
 429 |   private
 430 |   linkNoBold : Grammar state MarkdownToken True Inline
 431 |   linkNoBold = linkGen $ %runElab toListElab $ deletes
 432 |     [ "bold"
 433 |     , "italics"
 434 |     , "textBoldSym"
 435 |     , "textItalicsSym"
 436 |     ]
 437 |     -- We use another italic grammar without link nor bold to avoid infinite
 438 |     -- recursion.
 439 |     ("italicsNoLinkNoBold" :: listInlineLink)
 440 | 
 441 |   ||| Link without italic text.
 442 |   |||
 443 |   ||| This is to be used within italic text. As the text is already italic, we
 444 |   ||| don't want to have again italic within the link to avoid infinite
 445 |   ||| recursion.
 446 |   private
 447 |   linkNoItalic : Grammar state MarkdownToken True Inline
 448 |   linkNoItalic = linkGen $ %runElab toListElab $ deletes
 449 |     [ "bold"
 450 |     , "italics"
 451 |     , "textBoldSym"
 452 |     , "textItalicsSym"
 453 |     ]
 454 |     -- We use another bold grammar without link nor italic to avoid infinite
 455 |     -- recursion.
 456 |     ("boldNoLinkNoItalic" :: listInlineLink)
 457 | 
 458 |   private
 459 |   html : Grammar state MarkdownToken True Inline
 460 |   html =
 461 |     let
 462 |       htmlInline = choice $ %runElab toListElab $ deletes
 463 |         [ "html"
 464 |         , "italics"
 465 |         , "bold"
 466 |         , "image"
 467 |         , "link"
 468 |         , "closeTag"
 469 |         ]
 470 |         listInline
 471 |     in
 472 |     do
 473 |       openTag  <- match HtmlOpenTag
 474 |       contents <- many htmlInline
 475 |       _        <- optional $ closer openTag
 476 |       pure $ Html openTag contents
 477 | 
 478 | --------------------------------------------------------------------------------
 479 | -- Parsing function
 480 | --------------------------------------------------------------------------------
 481 | 
 482 | ||| Parses a (bounded) list of markdown tokens.
 483 | |||
 484 | ||| A markdown error is returned in case of failures of consuming all tokens.
 485 | export
 486 | parseMarkdown : List (WithBounds MarkdownToken) -> Either MdError Markdown
 487 | parseMarkdown toks =
 488 |   case parse markdown toks of
 489 |     Right (result, [])   => Right (normalise result)
 490 |     Right (_, ts@(x :: xs)) => Left $ MkMdError
 491 |                                ParsingError
 492 |                                x.bounds.startLine
 493 |                                x.bounds.startCol
 494 |                                "cannot parse: \{show $ map val ts}"
 495 |     -- As errors should not occure and are returned for debbuging purposes, we
 496 |     -- can afford returning just the first one.
 497 |     Left (e ::: _)       => Left $ fromParsingError e
 498 |