
   0 | module Text.YAML.Lexer
   1 | 
   2 | import public Text.Lex.Manual
   3 | import Text.YAML.Types
   4 | 
   5 | %default total
   6 | 
   7 | --------------------------------------------------------------------------------
   8 | --          Character Classes
   9 | --------------------------------------------------------------------------------
  10 | 
  11 | ||| A line break. Input is normalized before parsing (see
  12 | ||| `Text.YAML.Parser.parseEvents`), so only line feeds occur [spec 5.4].
  13 | public export %inline
  14 | isBreak : Char -> Bool
  15 | isBreak '\n' = True
  16 | isBreak _    = False
  17 | 
  18 | ||| White space within a line [spec: s-white].
  19 | public export %inline
  20 | isWhite : Char -> Bool
  21 | isWhite ' '  = True
  22 | isWhite '\t' = True
  23 | isWhite _    = False
  24 | 
  25 | ||| A flow collection indicator [spec: c-flow-indicator].
  26 | public export
  27 | isFlowInd : Char -> Bool
  28 | isFlowInd ',' = True
  29 | isFlowInd '[' = True
  30 | isFlowInd ']' = True
  31 | isFlowInd '{' = True
  32 | isFlowInd '}' = True
  33 | isFlowInd _   = False
  34 | 
  35 | ||| A character that cannot start a plain scalar [spec: c-indicator].
  36 | public export
  37 | isIndicator : Char -> Bool
  38 | isIndicator '-'  = True
  39 | isIndicator '?'  = True
  40 | isIndicator ':'  = True
  41 | isIndicator '#'  = True
  42 | isIndicator '&'  = True
  43 | isIndicator '*'  = True
  44 | isIndicator '!'  = True
  45 | isIndicator '|'  = True
  46 | isIndicator '>'  = True
  47 | isIndicator '\'' = True
  48 | isIndicator '"'  = True
  49 | isIndicator '%'  = True
  50 | isIndicator '@'  = True
  51 | isIndicator '`'  = True
  52 | isIndicator c    = isFlowInd c
  53 | 
  54 | ||| A character that may occur in the middle of a plain scalar
  55 | ||| [spec: ns-plain-safe]. In flow context, flow indicators end a
  56 | ||| plain scalar.
  57 | public export
  58 | isPlainSafe : (inFlow : Bool) -> Char -> Bool
  59 | isPlainSafe inFlow c =
  60 |   not (isWhite c || isBreak c || isControl c || (inFlow && isFlowInd c))
  61 | 
  62 | ||| May the given character start a plain scalar when followed by the
  63 | ||| given remainder [spec: ns-plain-first]?
  64 | public export
  65 | isPlainFirst : (inFlow : Bool) -> Char -> List Char -> Bool
  66 | isPlainFirst inFlow '-' (c :: _) = isPlainSafe inFlow c
  67 | isPlainFirst inFlow '?' (c :: _) = isPlainSafe inFlow c
  68 | isPlainFirst inFlow ':' (c :: _) = isPlainSafe inFlow c
  69 | isPlainFirst inFlow c   _        =
  70 |   not (isIndicator c || isWhite c || isBreak c || isControl c)
  71 | 
  72 | --------------------------------------------------------------------------------
  73 | --          Line Structure
  74 | --------------------------------------------------------------------------------
  75 | 
  76 | ||| Does a token like `-`, `?` or `:` end here, that is, is it followed
  77 | ||| by white space, a line break, or the end of input?
  78 | public export
  79 | wordEnd : List Char -> Bool
  80 | wordEnd []       = True
  81 | wordEnd (c :: _) = isWhite c || isBreak c
  82 | 
  83 | ||| Classification of the next content found by `skipToContent`.
  84 | public export
  85 | data LineKind : Type where
  86 |   ||| A line holding regular content.
  87 |   LContent  : LineKind
  88 | 
  89 |   ||| A `---` document marker at column zero.
  90 |   LDocStart : LineKind
  91 | 
  92 |   ||| A `...` document marker at column zero.
  93 |   LDocEnd   : LineKind
  94 | 
  95 |   ||| The end of the input.
  96 |   LEnd      : LineKind
  97 | 
  98 | public export
  99 | record Look where
 100 |   constructor L
 101 |   ||| Number of indentation spaces before the content. Only meaningful
 102 |   ||| for `LContent`.
 103 |   indent : Nat
 104 |   kind   : LineKind
 105 |   ||| Did tabs occur between the indentation and the content? Block
 106 |   ||| structure must not be preceded by tabs [spec 6.1].
 107 |   tabbed : Bool
 108 | 
 109 | ||| Result of `skipToContent`: the classification of what follows, the
 110 | ||| remaining input, and a proof relating it to the original input.
 111 | public export
 112 | record SkipRes (cs : List Char) where
 113 |   constructor SR
 114 |   look : Look
 115 |   rem  : List Char
 116 |   prf  : Suffix False rem cs
 117 | 
 118 | ||| Consumes blank and comment-only lines, classifying what follows.
 119 | |||
 120 | ||| Must be called at the start of a line. Document markers (at column
 121 | ||| zero) and the end of input are reported without consuming them. For
 122 | ||| a content line, the leading indentation (and any further white
 123 | ||| space separation before the first content character) is consumed
 124 | ||| and the number of indentation spaces is reported. Tabs never count
 125 | ||| as indentation [spec 6.1].
 126 | export
 127 | skipToContent : (cs : List Char) -> SkipRes cs
 128 | skipToContent cs = line cs Same
 129 | 
 130 |   where
 131 |     mutual
 132 |       -- at the start of a line
 133 |       line : (rem : List Char) -> Suffix False rem cs -> SkipRes cs
 134 |       line ('-' :: '-' :: '-' :: t) p =
 135 |         if wordEnd t
 136 |           then SR (L 0 LDocStart False) ('-' :: '-' :: '-' :: t) p
 137 |           else indent 0 ('-' :: '-' :: '-' :: t) p
 138 |       line ('.' :: '.' :: '.' :: t) p =
 139 |         if wordEnd t
 140 |           then SR (L 0 LDocEnd False) ('.' :: '.' :: '.' :: t) p
 141 |           else indent 0 ('.' :: '.' :: '.' :: t) p
 142 |       line rem p = indent 0 rem p
 143 | 
 144 |       -- counting indentation spaces
 145 |       indent : Nat -> (rem : List Char) -> Suffix False rem cs -> SkipRes cs
 146 |       indent n (' ' :: t) p = indent (S n) t (Uncons p)
 147 |       indent n rem        p = white n False rem p
 148 | 
 149 |       -- white space beyond the indentation (tabs are separation,
 150 |       -- not indentation)
 151 |       white : Nat -> (tb : Bool) -> (rem : List Char) -> Suffix False rem cs -> SkipRes cs
 152 |       white n tb ('\t' :: t) p = white n True t (Uncons p)
 153 |       white n tb (' '  :: t) p = white n tb t (Uncons p)
 154 |       white n tb ('\n' :: t) p = line t (Uncons p)
 155 |       white n tb ('#'  :: t) p = comment t (Uncons p)
 156 |       white n tb []          p = SR (L 0 LEnd False) [] p
 157 |       white n tb rem         p = SR (L n LContent tb) rem p
 158 | 
 159 |       -- the rest of a comment line
 160 |       comment : (rem : List Char) -> Suffix False rem cs -> SkipRes cs
 161 |       comment ('\n' :: t) p = line t (Uncons p)
 162 |       comment (_    :: t) p = comment t (Uncons p)
 163 |       comment []          p = SR (L 0 LEnd False) [] p
 164 | 
 165 | ||| Result of `inlineWhite`: a count of skipped white space characters,
 166 | ||| the remaining input, and a proof relating it to the original input.
 167 | public export
 168 | record Inl (cs : List Char) where
 169 |   constructor IL
 170 |   count : Nat
 171 |   ||| Was any of the white space a tab?
 172 |   tab   : Bool
 173 |   rem   : List Char
 174 |   prf   : Suffix False rem cs
 175 | 
 176 | ||| Consumes white space within a line.
 177 | export
 178 | inlineWhite : (cs : List Char) -> Inl cs
 179 | inlineWhite cs = go 0 False cs Same
 180 | 
 181 |   where
 182 |     go : Nat -> Bool -> (rem : List Char) -> Suffix False rem cs -> Inl cs
 183 |     go n tb (' '  :: t) p = go (S n) tb t (Uncons p)
 184 |     go n tb ('\t' :: t) p = go (S n) True t (Uncons p)
 185 |     go n tb rem         p = IL n tb rem p
 186 | 
 187 | --------------------------------------------------------------------------------
 188 | --          Anchors and Tags
 189 | --------------------------------------------------------------------------------
 190 | 
 191 | ||| May the given character occur in a URI [spec: ns-uri-char]?
 192 | public export
 193 | isUriChar : Char -> Bool
 194 | isUriChar '#'  = True
 195 | isUriChar ';'  = True
 196 | isUriChar '/'  = True
 197 | isUriChar '?'  = True
 198 | isUriChar ':'  = True
 199 | isUriChar '@'  = True
 200 | isUriChar '&'  = True
 201 | isUriChar '='  = True
 202 | isUriChar '+'  = True
 203 | isUriChar '$'  = True
 204 | isUriChar ','  = True
 205 | isUriChar '-'  = True
 206 | isUriChar '_'  = True
 207 | isUriChar '.'  = True
 208 | isUriChar '!'  = True
 209 | isUriChar '~'  = True
 210 | isUriChar '*'  = True
 211 | isUriChar '\'' = True
 212 | isUriChar '('  = True
 213 | isUriChar ')'  = True
 214 | isUriChar '['  = True
 215 | isUriChar ']'  = True
 216 | isUriChar '%'  = True
 217 | isUriChar c    = isAlphaNum c
 218 | 
 219 | ||| A word character [spec: ns-word-char], as used in tag handles.
 220 | public export
 221 | isWordChar : Char -> Bool
 222 | isWordChar '-' = True
 223 | isWordChar c   = isAlphaNum c
 224 | 
 225 | ||| A character of a tag shorthand's suffix [spec: ns-tag-char].
 226 | public export
 227 | isTagChar : Char -> Bool
 228 | isTagChar '!' = False
 229 | isTagChar c   = isUriChar c && not (isFlowInd c)
 230 | 
 231 | ||| An anchor or alias name [spec: ns-anchor-name], starting at its
 232 | ||| `&` or `*` indicator.
 233 | export
 234 | anchorName : Tok True YErr String
 235 | anchorName (c :: cs) = go [<] cs
 236 | 
 237 |   where
 238 |     go : SnocList Char -> AutoTok YErr String
 239 |     go acc (x :: xs) =
 240 |       if isPlainSafe True x
 241 |         then go (acc :< x) xs
 242 |         else case acc of
 243 |           [<] => fail p
 244 |           _   => Succ (cast acc) (x :: xs)
 245 |     go acc [] = case acc of
 246 |       [<] => fail p
 247 |       _   => Succ (cast acc) []
 248 | 
 249 | anchorName [] = eoiAt Same
 250 | 
 251 | ||| A tag property [spec: c-ns-tag-property], starting at its `!`
 252 | ||| indicator: verbatim (`!<...>`), a shorthand to be resolved against
 253 | ||| the active tag handles, or the non-specific tag `!`.
 254 | export
 255 | tagToken : Tok True YErr (Either Tag (String, String))
 256 | tagToken ('!' :: '<' :: cs) = verb [<] cs
 257 | 
 258 |   where
 259 |     verb : SnocList Char -> AutoTok YErr (Either Tag (String, String))
 260 |     verb acc ('>' :: t) = case acc of
 261 |       [<] => fail p
 262 |       _   => Succ (Left (Verbatim (cast acc))) t
 263 |     verb acc ('%' :: x :: y :: t) =
 264 |       if isHexDigit x && isHexDigit y
 265 |         then verb (acc :< chr (cast $ hexDigit x * 16 + hexDigit y)) t
 266 |         else invalidEscape p t
 267 |     verb acc (x :: t)   =
 268 |       if isUriChar x then verb (acc :< x) t else fail p
 269 |     verb acc []         = eoiAt p
 270 | 
 271 | tagToken ('!' :: cs) = sh [<] True cs
 272 | 
 273 |   where
 274 |     -- the suffix after a named or secondary handle
 275 |     suff : String -> SnocList Char -> AutoTok YErr (Either Tag (String, String))
 276 |     suff h acc ('%' :: x :: y :: t) =
 277 |       if isHexDigit x && isHexDigit y
 278 |         then suff h (acc :< chr (cast $ hexDigit x * 16 + hexDigit y)) t
 279 |         else invalidEscape p t
 280 |     suff h acc (x :: t) =
 281 |       if isTagChar x && x /= '%'
 282 |         then suff h (acc :< x) t
 283 |         else case acc of
 284 |           [<] => fail p
 285 |           _   => Succ (Right (h, cast acc)) (x :: t)
 286 |     suff h acc [] = case acc of
 287 |       [<] => fail p
 288 |       _   => Succ (Right (h, cast acc)) []
 289 | 
 290 |     -- the shorthand: tag characters, possibly closing a handle with a
 291 |     -- second `!`
 292 |     sh : SnocList Char -> (word : Bool) -> AutoTok YErr (Either Tag (String, String))
 293 |     sh acc word ('!' :: t) =
 294 |       if word then suff ("!" ++ cast acc ++ "!") [<] t else fail p
 295 |     sh acc word ('%' :: x :: y :: t) =
 296 |       if isHexDigit x && isHexDigit y
 297 |         then sh (acc :< chr (cast $ hexDigit x * 16 + hexDigit y)) False t
 298 |         else invalidEscape p t
 299 |     sh acc word (x :: t)  =
 300 |       if isTagChar x && x /= '%'
 301 |         then sh (acc :< x) (word && isWordChar x) t
 302 |         else case acc of
 303 |           [<] => Succ (Left NonSpec) (x :: t)
 304 |           _   => Succ (Right ("!", cast acc)) (x :: t)
 305 |     sh acc word [] = case acc of
 306 |       [<] => Succ (Left NonSpec) []
 307 |       _   => Succ (Right ("!", cast acc)) []
 308 | 
 309 | tagToken cs = fail Same
 310 | 
 311 | ||| A whole directive line including its line break (the break is not
 312 | ||| part of the result).
 313 | export
 314 | dirLine : Tok True YErr String
 315 | dirLine (c :: cs) = go [<c] cs
 316 | 
 317 |   where
 318 |     go : SnocList Char -> AutoTok YErr String
 319 |     go acc ('\n' :: t) = Succ (cast acc) t
 320 |     go acc (x :: t)    = go (acc :< x) t
 321 |     go acc []          = Succ (cast acc) []
 322 | 
 323 | dirLine [] = eoiAt Same
 324 | 
 325 | --------------------------------------------------------------------------------
 326 | --          Quoted Scalars
 327 | --------------------------------------------------------------------------------
 328 | 
 329 | ||| Is the input at a `---` or `...` document marker? Only valid at
 330 | ||| column zero.
 331 | public export
 332 | isDocMarker : List Char -> Bool
 333 | isDocMarker ('-' :: '-' :: '-' :: t) = wordEnd t
 334 | isDocMarker ('.' :: '.' :: '.' :: t) = wordEnd t
 335 | isDocMarker _                        = False
 336 | 
 337 | -- appends k line feeds
 338 | addNl : SnocList Char -> Nat -> SnocList Char
 339 | addNl acc 0     = acc
 340 | addNl acc (S k) = addNl (acc :< '\n') k
 341 | 
 342 | -- the contribution of folding over k empty lines [spec: b-l-folded]
 343 | foldNl : SnocList Char -> Nat -> SnocList Char
 344 | foldNl acc 0 = acc :< ' '
 345 | foldNl acc k = addNl acc k
 346 | 
 347 | ||| A single quoted scalar [spec: c-single-quoted], starting at its
 348 | ||| opening quote. A pair of quotes escapes a quote; line breaks fold;
 349 | ||| continuation lines must be indented at least `mi` spaces and must
 350 | ||| not be document markers.
 351 | export
 352 | singleQuoted : (mi : Nat) -> Tok True YErr String
 353 | singleQuoted mi ('\'' :: cs) = go [<] [<] cs
 354 | 
 355 |   where
 356 |     mutual
 357 |       -- content within a line; pend holds white space that is dropped
 358 |       -- if the line ends
 359 |       go : (acc, pend : SnocList Char) -> AutoTok YErr String
 360 |       go acc pend ('\'' :: '\'' :: t) = go ((acc ++ pend) :< '\'') [<] t
 361 |       go acc pend ('\'' :: t)         = Succ (cast (acc ++ pend)) t
 362 |       go acc pend ('\n' :: t)         = lines acc 0 0 t
 363 |       go acc pend (' '  :: t)         = go acc (pend :< ' ') t
 364 |       go acc pend ('\t' :: t)         = go acc (pend :< '\t') t
 365 |       go acc pend (c :: t)            =
 366 |         if isControl c
 367 |           then single (InvalidControl c) p
 368 |           else go ((acc ++ pend) :< c) [<] t
 369 |       go acc pend []                  = eoiAt p
 370 | 
 371 |       -- at a line start: empty lines, then the next line's indentation
 372 |       lines : (acc : SnocList Char) -> (k, ind : Nat) -> AutoTok YErr String
 373 |       lines acc k ind ('\n' :: t) = lines acc (S k) 0 t
 374 |       lines acc k ind (' '  :: t) = lines acc k (S ind) t
 375 |       lines acc k ind ('\t' :: t) =
 376 |         if ind >= mi then sep acc k t else single (Custom TabIndent) p
 377 |       lines acc k ind []          = eoiAt p
 378 |       lines acc k ind (c :: t)    =
 379 |         if ind == 0 && isDocMarker (c :: t)
 380 |           then single (Unknown "document marker") p
 381 |         else if ind < mi
 382 |           then single (Custom BadIndent) p
 383 |         else go (foldNl acc k) [<] (c :: t)
 384 | 
 385 |       -- white space separation beyond the indentation
 386 |       sep : (acc : SnocList Char) -> (k : Nat) -> AutoTok YErr String
 387 |       sep acc k (' '  :: t) = sep acc k t
 388 |       sep acc k ('\t' :: t) = sep acc k t
 389 |       sep acc k ('\n' :: t) = lines acc (S k) 0 t
 390 |       sep acc k []          = eoiAt p
 391 |       sep acc k (c :: t)    = go (foldNl acc k) [<] (c :: t)
 392 | 
 393 | singleQuoted _ cs = fail Same
 394 | 
 395 | ||| A double quoted scalar [spec: c-double-quoted], starting at its
 396 | ||| opening quote: backslash escape sequences (including escaped line
 397 | ||| breaks), line folding, and the same indentation and document marker
 398 | ||| rules as single quoted scalars.
 399 | export
 400 | doubleQuoted : (mi : Nat) -> Tok True YErr String
 401 | doubleQuoted mi ('"' :: cs) = go [<] [<] cs
 402 | 
 403 |   where
 404 |     escChar : Char -> Maybe Char
 405 |     escChar '0'  = Just '\0'
 406 |     escChar 'a'  = Just '\x07'
 407 |     escChar 'b'  = Just '\b'
 408 |     escChar 't'  = Just '\t'
 409 |     escChar '\t' = Just '\t'
 410 |     escChar 'n'  = Just '\n'
 411 |     escChar 'v'  = Just '\x0b'
 412 |     escChar 'f'  = Just '\x0c'
 413 |     escChar 'r'  = Just '\r'
 414 |     escChar 'e'  = Just '\x1b'
 415 |     escChar ' '  = Just ' '
 416 |     escChar '"'  = Just '"'
 417 |     escChar '/'  = Just '/'
 418 |     escChar '\\' = Just '\\'
 419 |     escChar 'N'  = Just '\x85'
 420 |     escChar '_'  = Just '\xa0'
 421 |     escChar 'L'  = Just '\x2028'
 422 |     escChar 'P'  = Just '\x2029'
 423 |     escChar _    = Nothing
 424 | 
 425 |     toChar : Nat -> Maybe Char
 426 |     toChar n =
 427 |       if n > 0x10ffff || (n >= 0xd800 && n <= 0xdfff)
 428 |         then Nothing
 429 |         else Just (chr $ cast n)
 430 | 
 431 |     mutual
 432 |       go : (acc, pend : SnocList Char) -> AutoTok YErr String
 433 |       go acc pend ('"'  :: t)      = Succ (cast (acc ++ pend)) t
 434 |       go acc pend ('\\' :: c :: t) = case c of
 435 |         -- an escaped break: white space before it is kept, lines do
 436 |         -- not fold [spec: s-double-escaped]
 437 |         '\n' => lines (acc ++ pend) True 0 0 t
 438 |         'x'  => hex (acc ++ pend) 2 0 t
 439 |         'u'  => hex (acc ++ pend) 4 0 t
 440 |         'U'  => hex (acc ++ pend) 8 0 t
 441 |         _    => case escChar c of
 442 |           Just ch => go ((acc ++ pend) :< ch) [<] t
 443 |           Nothing => invalidEscape p t
 444 |       go acc pend ('\\' :: [])     = invalidEscape p []
 445 |       go acc pend ('\n' :: t)      = lines acc False 0 0 t
 446 |       go acc pend (' '  :: t)      = go acc (pend :< ' ') t
 447 |       go acc pend ('\t' :: t)      = go acc (pend :< '\t') t
 448 |       go acc pend (c :: t)         =
 449 |         if isControl c
 450 |           then single (InvalidControl c) p
 451 |           else go ((acc ++ pend) :< c) [<] t
 452 |       go acc pend []               = eoiAt p
 453 | 
 454 |       -- a fixed number of hex digits of a character escape
 455 |       hex : (acc : SnocList Char) -> (k, val : Nat) -> AutoTok YErr String
 456 |       hex acc 0     val cs2 = case toChar val of
 457 |         Just ch => go (acc :< ch) [<] cs2
 458 |         Nothing => invalidEscape p cs2
 459 |       hex acc (S k) val (c :: t) =
 460 |         if isHexDigit c
 461 |           then hex acc k (val * 16 + hexDigit c) t
 462 |           else invalidEscape p t
 463 |       hex acc (S k) val [] = eoiAt p
 464 | 
 465 |       -- at a line start; `eb` is true after an escaped break, which
 466 |       -- suppresses the folding space
 467 |       lines : (acc : SnocList Char) -> (eb : Bool) -> (k, ind : Nat) -> AutoTok YErr String
 468 |       lines acc eb k ind ('\n' :: t) = lines acc eb (S k) 0 t
 469 |       lines acc eb k ind (' '  :: t) = lines acc eb k (S ind) t
 470 |       lines acc eb k ind ('\t' :: t) =
 471 |         if ind >= mi then sep acc eb k t else single (Custom TabIndent) p
 472 |       lines acc eb k ind []          = eoiAt p
 473 |       lines acc eb k ind (c :: t)    =
 474 |         if ind == 0 && isDocMarker (c :: t)
 475 |           then single (Unknown "document marker") p
 476 |         else if ind < mi
 477 |           then single (Custom BadIndent) p
 478 |         else go (if eb then addNl acc k else foldNl acc k) [<] (c :: t)
 479 | 
 480 |       -- white space separation beyond the indentation
 481 |       sep : (acc : SnocList Char) -> (eb : Bool) -> (k : Nat) -> AutoTok YErr String
 482 |       sep acc eb k (' '  :: t) = sep acc eb k t
 483 |       sep acc eb k ('\t' :: t) = sep acc eb k t
 484 |       sep acc eb k ('\n' :: t) = lines acc eb (S k) 0 t
 485 |       sep acc eb k []          = eoiAt p
 486 |       sep acc eb k (c :: t)    = go (if eb then addNl acc k else foldNl acc k) [<] (c :: t)
 487 | 
 488 | doubleQuoted _ cs = fail Same
 489 | 
 490 | --------------------------------------------------------------------------------
 491 | --          Block Scalars
 492 | --------------------------------------------------------------------------------
 493 | 
 494 | ||| Chomping of a block scalar's trailing line breaks
 495 | ||| [spec: c-chomping-indicator].
 496 | public export
 497 | data Chomp = Strip | Clip | Keep
 498 | 
 499 | ||| A block scalar [spec: c-l+literal, c-l+folded], starting at its `|`
 500 | ||| or `>` indicator: the header (indentation and chomping indicators
 501 | ||| plus an optional comment), then the indented content lines.
 502 | |||
 503 | ||| `mi` is the minimum content indentation, that is, the parent
 504 | ||| node's indentation plus one; an explicit indentation indicator `d`
 505 | ||| anchors the content at `mi + d - 1` columns.
 506 | export
 507 | blockScalar : (folded : Bool) -> (mi : Nat) -> Tok True YErr String
 508 | blockScalar folded mi (c :: cs) = hdr Nothing Nothing cs
 509 | 
 510 |   where
 511 |     -- assembles the final scalar from the accumulated content and the
 512 |     -- pending trailing line breaks
 513 |     fin : Chomp -> (acc : SnocList Char) -> (brk : Nat) -> String
 514 |     fin Strip acc _   = cast acc
 515 |     fin Keep  acc brk = cast (addNl acc brk)
 516 |     fin Clip  acc brk = case acc of
 517 |       [<] => ""
 518 |       _   => if brk > 0 then cast (acc :< '\n') else cast acc
 519 | 
 520 |     -- the contribution of a content line: pending breaks (folded where
 521 |     -- applicable), then the line itself [spec: b-l-folded]
 522 |     contrib :
 523 |          (prev : Maybe Bool)   -- spacedness of the previous line, if any
 524 |       -> (brk : Nat)           -- pending line breaks
 525 |       -> (spaced : Bool)       -- does this line start with white space?
 526 |       -> (acc, line : SnocList Char)
 527 |       -> SnocList Char
 528 |     contrib prev brk spaced acc line =
 529 |       let joined := case prev of
 530 |             Nothing => addNl acc brk
 531 |             Just pSp =>
 532 |               if folded && not pSp && not spaced
 533 |                 then (if brk == 1 then acc :< ' ' else addNl acc (brk `minus` 1))
 534 |                 else addNl acc brk
 535 |        in joined ++ line
 536 | 
 537 |     -- the content indentation: fixed (explicit or detected), or still
 538 |     -- to be detected (tracking the deepest empty line seen so far)
 539 |     data Ci = Fixed Nat | Auto Nat
 540 | 
 541 |     -- classification of the next line, without consuming it: an empty
 542 |     -- line, white space before the end of input, or content (with a
 543 |     -- document marker or tab flag)
 544 |     data PLine = PBlank Nat | PEnd Nat | PCont Nat Bool Bool
 545 | 
 546 |     peek : Nat -> List Char -> PLine
 547 |     peek n (' '  :: t) = peek (S n) t
 548 |     peek n ('\n' :: _) = PBlank n
 549 |     peek n []          = PEnd n
 550 |     peek n cs2@(x :: _) = PCont n (n == 0 && isDocMarker cs2) (x == '\t')
 551 | 
 552 |     startCi : Maybe Nat -> Ci
 553 |     startCi Nothing  = Auto 0
 554 |     startCi (Just d) = Fixed ((mi + d) `minus` 1)
 555 | 
 556 |     mutual
 557 |       -- at a line start: decide whether the next line still belongs to
 558 |       -- the scalar before consuming anything
 559 |       atLine :
 560 |            Chomp -> Ci -> (prev : Maybe Bool) -> (acc : SnocList Char)
 561 |         -> (brk : Nat) -> AutoTok YErr String
 562 |       atLine ch ci prev acc brk cs2 = case peek 0 cs2 of
 563 |         PEnd n => case ci of
 564 |           -- trailing white space before the end of input: a content
 565 |           -- line of spaces if more indented, an empty line otherwise
 566 |           Fixed n2 =>
 567 |             if n > n2
 568 |               then capture ch n2 prev acc brk 0 [<] cs2
 569 |               else Succ (fin ch acc (if n > 0 then S brk else brk)) cs2
 570 |           Auto _ => Succ (fin ch acc (if n > 0 then S brk else brk)) cs2
 571 |         PBlank n => case ci of
 572 |           Auto mb => blank ch (Auto $ max mb n) prev acc brk cs2
 573 |           Fixed n2 =>
 574 |             if n > n2
 575 |               then capture ch n2 prev acc brk 0 [<] cs2
 576 |               else blank ch (Fixed n2) prev acc brk cs2
 577 |         PCont n marker tab => case ci of
 578 |           Auto mb =>
 579 |             if tab && n < mi
 580 |               then range (Custom TabIndent) p cs2
 581 |             else if n < mi || marker
 582 |               then Succ (fin ch acc brk) cs2
 583 |             else if mb > n
 584 |               then fail Same
 585 |             else capture ch n prev acc brk 0 [<] cs2
 586 |           Fixed n2 =>
 587 |             if tab && n < n2
 588 |               then range (Custom TabIndent) p cs2
 589 |             else if n < n2 || marker
 590 |               then Succ (fin ch acc brk) cs2
 591 |               else capture ch n2 prev acc brk 0 [<] cs2
 592 | 
 593 |       -- consumes an empty line
 594 |       blank :
 595 |            Chomp -> Ci -> (prev : Maybe Bool) -> (acc : SnocList Char)
 596 |         -> (brk : Nat) -> AutoTok YErr String
 597 |       blank ch ci prev acc brk (' '  :: t) = blank ch ci prev acc brk t
 598 |       blank ch ci prev acc brk ('\n' :: t) = atLine ch ci prev acc (S brk) t
 599 |       blank ch ci prev acc brk (_ :: t)    = fail Same
 600 |       blank ch ci prev acc brk []          = Succ (fin ch acc brk) []
 601 | 
 602 |       -- consumes a content line: its indentation (spaces beyond the
 603 |       -- content indent are content), then the raw text
 604 |       capture :
 605 |            Chomp -> (n : Nat) -> (prev : Maybe Bool) -> (acc : SnocList Char)
 606 |         -> (brk, m : Nat) -> (line : SnocList Char) -> AutoTok YErr String
 607 |       capture ch n prev acc brk m line (' ' :: t) =
 608 |         if m >= n
 609 |           then capture ch n prev acc brk (S m) (line :< ' ') t
 610 |           else capture ch n prev acc brk (S m) line t
 611 |       capture ch n prev acc brk m line ('\t' :: t) =
 612 |         if m >= n
 613 |           then capLine ch n prev acc brk True (line :< '\t') t
 614 |           else single (Custom TabIndent) p
 615 |       capture ch n prev acc brk m line ('\n' :: t) =
 616 |         let spaced := m > n
 617 |          in atLine ch (Fixed n) (Just spaced) (contrib prev brk spaced acc line) 1 t
 618 |       capture ch n prev acc brk m line [] =
 619 |         -- a content line ending at the end of input still counts as
 620 |         -- ended by a break for chomping [spec: b-chomped-last]
 621 |         let spaced := m > n
 622 |          in Succ (fin ch (contrib prev brk spaced acc line) 1) []
 623 |       capture ch n prev acc brk m line (x :: t) =
 624 |         if isControl x
 625 |           then single (InvalidControl x) p
 626 |           else capLine ch n prev acc brk (m > n) (line :< x) t
 627 | 
 628 |       -- the raw remainder of a content line
 629 |       capLine :
 630 |            Chomp -> (n : Nat) -> (prev : Maybe Bool) -> (acc : SnocList Char)
 631 |         -> (brk : Nat) -> (spaced : Bool) -> (line : SnocList Char)
 632 |         -> AutoTok YErr String
 633 |       capLine ch n prev acc brk spaced line ('\n' :: t) =
 634 |         atLine ch (Fixed n) (Just spaced) (contrib prev brk spaced acc line) 1 t
 635 |       capLine ch n prev acc brk spaced line (x :: t) =
 636 |         if isControl x && x /= '\t'
 637 |           then single (InvalidControl x) p
 638 |           else capLine ch n prev acc brk spaced (line :< x) t
 639 |       capLine ch n prev acc brk spaced line [] =
 640 |         Succ (fin ch (contrib prev brk spaced acc line) 1) []
 641 | 
 642 |       -- the header: at most one indentation digit and one chomping
 643 |       -- indicator, optional comment, then the first line break
 644 |       hdr : (d : Maybe Nat) -> (ch : Maybe Chomp) -> AutoTok YErr String
 645 |       hdr d ch ('-' :: t)  = case ch of
 646 |         Nothing => hdr d (Just Strip) t
 647 |         Just _  => fail Same
 648 |       hdr d ch ('+' :: t)  = case ch of
 649 |         Nothing => hdr d (Just Keep) t
 650 |         Just _  => fail Same
 651 |       hdr d ch ('\n' :: t) = atLine (maybe Clip id ch) (startCi d) Nothing [<] 0 t
 652 |       hdr d ch (' '  :: t) = hdrEnd d ch t
 653 |       hdr d ch ('\t' :: t) = hdrEnd d ch t
 654 |       hdr d ch []          = Succ (fin (maybe Clip id ch) [<] 0) []
 655 |       hdr d ch (x :: t)    =
 656 |         if isDigit x && x /= '0'
 657 |           then case d of
 658 |             Nothing => hdr (Just $ digit x) ch t
 659 |             Just _  => fail Same
 660 |           else fail Same
 661 | 
 662 |       -- after the header's indicators: separation and a comment
 663 |       hdrEnd : (d : Maybe Nat) -> (ch : Maybe Chomp) -> AutoTok YErr String
 664 |       hdrEnd d ch (' '  :: t) = hdrEnd d ch t
 665 |       hdrEnd d ch ('\t' :: t) = hdrEnd d ch t
 666 |       hdrEnd d ch ('#'  :: t) = hdrCom d ch t
 667 |       hdrEnd d ch ('\n' :: t) = atLine (maybe Clip id ch) (startCi d) Nothing [<] 0 t
 668 |       hdrEnd d ch []          = Succ (fin (maybe Clip id ch) [<] 0) []
 669 |       hdrEnd d ch (x :: t)    = fail Same
 670 | 
 671 |       -- the header's comment
 672 |       hdrCom : (d : Maybe Nat) -> (ch : Maybe Chomp) -> AutoTok YErr String
 673 |       hdrCom d ch ('\n' :: t) = atLine (maybe Clip id ch) (startCi d) Nothing [<] 0 t
 674 |       hdrCom d ch (_ :: t)    = hdrCom d ch t
 675 |       hdrCom d ch []          = Succ (fin (maybe Clip id ch) [<] 0) []
 676 | 
 677 | blockScalar _ _ [] = eoiAt Same
 678 | 
 679 | --------------------------------------------------------------------------------
 680 | --          Plain Scalars
 681 | --------------------------------------------------------------------------------
 682 | 
 683 | ||| Continuation of a plain scalar onto the next line (see `plainCont`).
 684 | public export
 685 | data Cont : (cs : List Char) -> Type where
 686 |   ||| The scalar ends here: nothing is consumed.
 687 |   Stop : Cont cs
 688 | 
 689 |   ||| The scalar continues at `rem`, with `blanks` empty lines between
 690 |   ||| the segments (zero empty lines fold into a single space).
 691 |   More : (blanks : Nat) -> (rem : List Char) -> Suffix True rem cs -> Cont cs
 692 | 
 693 | ||| From the end of a plain-scalar segment (at its trailing white space
 694 | ||| or line break): does the scalar continue on a following line
 695 | ||| [spec: s-flow-folded]?
 696 | |||
 697 | ||| Stops at comment lines, document markers, lines indented less than
 698 | ||| `mi`, and lines starting with a character that cannot continue a
 699 | ||| plain scalar. This must mirror the stop conditions of
 700 | ||| `plainSegment`'s lookahead.
 701 | export
 702 | plainCont : (inFlow : Bool) -> (mi : Nat) -> (cs : List Char) -> Cont cs
 703 | plainCont inFlow mi cs = pre cs Same
 704 | 
 705 |   where
 706 |     isMarker : List Char -> Bool
 707 |     isMarker ('-' :: '-' :: '-' :: t) = wordEnd t
 708 |     isMarker ('.' :: '.' :: '.' :: t) = wordEnd t
 709 |     isMarker _                        = False
 710 | 
 711 |     -- may a continuation line start with this content [spec:
 712 |     -- ns-plain-char]?
 713 |     contFirst : Char -> List Char -> Bool
 714 |     contFirst '#' _        = False
 715 |     contFirst ':' (n :: _) = isPlainSafe inFlow n
 716 |     contFirst ':' []       = False
 717 |     contFirst c   _        = not (inFlow && isFlowInd c)
 718 | 
 719 |     mutual
 720 |       -- at the start of a line (the first break already consumed)
 721 |       line : Nat -> (rem : List Char) -> Suffix True rem cs -> Cont cs
 722 |       line k rem p = if isMarker rem then Stop else indent k 0 rem p
 723 | 
 724 |       -- counting indentation spaces
 725 |       indent : Nat -> Nat -> (rem : List Char) -> Suffix True rem cs -> Cont cs
 726 |       indent k n (' ' :: t) p = indent k (S n) t (Uncons p)
 727 |       indent k n rem        p = white k n rem p
 728 | 
 729 |       -- separation white space beyond the indentation
 730 |       white : Nat -> Nat -> (rem : List Char) -> Suffix True rem cs -> Cont cs
 731 |       white k n ('\t' :: t) p = white k n t (Uncons p)
 732 |       white k n (' '  :: t) p = white k n t (Uncons p)
 733 |       white k n ('\n' :: t) p = line (S k) t (Uncons p)
 734 |       white k n []          p = Stop
 735 |       white k n (c :: t)    p =
 736 |         if n >= mi && contFirst c t then More k (c :: t) p else Stop
 737 | 
 738 |     -- white space before the first line break
 739 |     pre : (rem : List Char) -> Suffix False rem cs -> Cont cs
 740 |     pre (' '  :: t) p = pre t (Uncons p)
 741 |     pre ('\t' :: t) p = pre t (Uncons p)
 742 |     pre ('\n' :: t) p = line 0 t (Uncons p)
 743 |     pre _           p = Stop
 744 | 
 745 | ||| A single line's worth of a plain scalar [spec: ns-plain-one-line],
 746 | ||| assuming the first character of the input starts a plain scalar
 747 | ||| (see `isPlainFirst`; verified by the caller).
 748 | |||
 749 | ||| Stops without consuming at the scalar's end: the end of the line, a
 750 | ||| ` #` comment, a `:` followed by white space (or, in flow context, a
 751 | ||| flow indicator or the end of the line), or, in flow context, any
 752 | ||| flow indicator. Trailing white space is neither part of the result
 753 | ||| nor consumed.
 754 | export
 755 | plainSegment : (inFlow : Bool) -> Tok True YErr String
 756 | plainSegment inFlow (c :: cs) =
 757 |   if isControl c then single (InvalidControl c) Same else go [<c] cs
 758 | 
 759 |   where
 760 |     -- is a `:` at this point part of the scalar rather than a value
 761 |     -- indicator [spec: ns-plain-char]?
 762 |     colonCont : List Char -> Bool
 763 |     colonCont (n :: _) = isPlainSafe inFlow n
 764 |     colonCont []       = False
 765 | 
 766 |     -- non-consuming lookahead: may the scalar continue beyond a run
 767 |     -- of white space?
 768 |     cont : List Char -> Bool
 769 |     cont (x :: xs) =
 770 |       if isWhite x then cont xs
 771 |       else if isBreak x then False
 772 |       else case x of
 773 |         '#' => False
 774 |         ':' => colonCont xs
 775 |         _   => not (inFlow && isFlowInd x)
 776 |     cont [] = False
 777 | 
 778 |     go : SnocList Char -> AutoTok YErr String
 779 |     go acc []        = Succ (cast acc) []
 780 |     go acc (x :: xs) =
 781 |       if isWhite x then
 782 |         if cont xs then go (acc :< x) xs else Succ (cast acc) (x :: xs)
 783 |       else if isBreak x then Succ (cast acc) (x :: xs)
 784 |       else if x == ':' then
 785 |         if colonCont xs
 786 |           then go (acc :< ':') xs
 787 |           else Succ (cast acc) (x :: xs)
 788 |       else if inFlow && isFlowInd x then Succ (cast acc) (x :: xs)
 789 |       else if isControl x then single (InvalidControl x) p
 790 |       else go (acc :< x) xs
 791 | 
 792 | plainSegment _ [] = eoiAt Same
 793 |