
    0 | module Text.YAML.Parser
    1 | 
    2 | import Data.Maybe
    3 | import Data.String
    4 | import public Text.Parse.Manual
    5 | import public Text.YAML.Types
    6 | import Text.YAML.Lexer
    7 | 
    8 | %default total
    9 | 
   10 | --------------------------------------------------------------------------------
   11 | --          Parser State
   12 | --------------------------------------------------------------------------------
   13 | 
   14 | ||| State threaded through all parsing rules: the current position in
   15 | ||| the input and the events emitted so far.
   16 | public export
   17 | record YState where
   18 |   constructor YS
   19 |   pos : Position
   20 |   evs : SnocList (Bounded Event)
   21 | 
   22 | %inline
   23 | emit : Bounds -> Event -> YState -> YState
   24 | emit bs e = {evs $= (:< B e bs)}
   25 | 
   26 | ||| An empty node with the given properties [spec: e-scalar], at the
   27 | ||| position where the node would have been.
   28 | %inline
   29 | emptyScalarP : Props -> Position -> SnocList (Bounded Event) -> SnocList (Bounded Event)
   30 | emptyScalarP pr p = (:< oneChar (Scalar pr.anchor pr.tag Plain "") p)
   31 | 
   32 | %inline
   33 | emptyScalar : Position -> SnocList (Bounded Event) -> SnocList (Bounded Event)
   34 | emptyScalar = emptyScalarP noProps
   35 | 
   36 | ||| An inline node candidate for implicit-key detection: a single-line
   37 | ||| scalar (its event not yet emitted, since a plain scalar might yet
   38 | ||| grow by line folding), an alias, node properties not followed by
   39 | ||| inline content, or a flow collection parsed into its own event
   40 | ||| buffer.
   41 | data Pending : Type where
   42 |   PScalar : Props -> Style -> String -> Pending
   43 |   PAlias  : Anchor -> Pending
   44 |   PProps  : Props -> Pending
   45 |   PFlow   : SnocList (Bounded Event) -> Pending
   46 | 
   47 | flushPend : (start, end : Position) -> SnocList (Bounded Event) -> Pending -> SnocList (Bounded Event)
   48 | flushPend s e evs (PScalar pr sty str) = evs :< bounded (Scalar pr.anchor pr.tag sty str) s e
   49 | flushPend s e evs (PAlias a)           = evs :< bounded (Alias a) s e
   50 | flushPend s _ evs (PProps pr)          = emptyScalarP pr s evs
   51 | flushPend _ _ evs (PFlow d)            = evs ++ d
   52 | 
   53 | ||| Attaches properties from a preceding line to a flow collection's
   54 | ||| opening event.
   55 | patchFlow : Props -> SnocList (Bounded Event) -> Either YErr (SnocList (Bounded Event))
   56 | patchFlow pr evs = case evs <>> [] of
   57 |   B (SeqStart f a t) bs :: es =>
   58 |     (\p => [<] <>< (B (SeqStart f p.anchor p.tag) bs :: es)) <$> mergeProps pr (MkProps a t)
   59 |   B (MapStart f a t) bs :: es =>
   60 |     (\p => [<] <>< (B (MapStart f p.anchor p.tag) bs :: es)) <$> mergeProps pr (MkProps a t)
   61 |   _ => Right evs
   62 | 
   63 | -- Is the next token a `:` value indicator in block context?
   64 | colonBlock : List Char -> Bool
   65 | colonBlock (':' :: t) = wordEnd t
   66 | colonBlock _          = False
   67 | 
   68 | -- Is the next token a `:` value indicator in flow context?
   69 | colonFlow : List Char -> Bool
   70 | colonFlow (':' :: n :: _) = not (isPlainSafe True n)
   71 | colonFlow (':' :: [])     = True
   72 | colonFlow _               = False
   73 | 
   74 | -- Does a `- ` sequence entry indicator follow?
   75 | dashNext : List Char -> Bool
   76 | dashNext ('-' :: t) = wordEnd t
   77 | dashNext _          = False
   78 | 
   79 | plainSafeNext : List Char -> Bool
   80 | plainSafeNext (c :: _) = isPlainSafe True c
   81 | plainSafeNext []       = False
   82 | 
   83 | -- Can an inline node candidate start here?
   84 | candStart : (inFlow : Bool) -> List Char -> Bool
   85 | candStart inFlow (c :: cs) =
   86 |   c == '[' || c == '{' || c == '\'' || c == '"' || c == '*' ||
   87 |   isPlainFirst inFlow c cs
   88 | candStart _ [] = False
   89 | 
   90 | -- Does a block scalar start here? Returns whether it is folded.
   91 | bsStart : List Char -> Maybe Bool
   92 | bsStart ('|' :: _) = Just False
   93 | bsStart ('>' :: _) = Just True
   94 | bsStart _          = Nothing
   95 | 
   96 | breakStart : List Char -> Bool
   97 | breakStart (c :: _) = isBreak c || c == '#'
   98 | breakStart []       = False
   99 | 
  100 | propStart : List Char -> Bool
  101 | propStart (c :: _) = c == '&' || c == '!'
  102 | propStart []       = False
  103 | 
  104 | colonNext : List Char -> Bool
  105 | colonNext (':' :: _) = True
  106 | colonNext _          = False
  107 | 
  108 | -- Does this line hold only node properties (and perhaps a comment)?
  109 | propsOnlyLine : List Char -> Bool
  110 | propsOnlyLine = go
  111 |   where
  112 |     mutual
  113 |       tok : List Char -> Bool
  114 |       tok (c :: cs) =
  115 |         if isWhite c || isBreak c then go (c :: cs) else tok cs
  116 |       tok [] = True
  117 | 
  118 |       go : List Char -> Bool
  119 |       go (' '  :: cs) = go cs
  120 |       go ('\t' :: cs) = go cs
  121 |       go ('\n' :: _)  = True
  122 |       go ('#'  :: _)  = True
  123 |       go ('&'  :: cs) = tok cs
  124 |       go ('!'  :: cs) = tok cs
  125 |       go []           = True
  126 |       go _            = False
  127 | 
  128 | -- JSON-like nodes allow an adjacent `:` value indicator
  129 | -- [spec: c-ns-flow-map-json-key-entry].
  130 | jsonLike : Pending -> Bool
  131 | jsonLike (PScalar _ SingleQ _) = True
  132 | jsonLike (PScalar _ DoubleQ _) = True
  133 | jsonLike (PFlow _)             = True
  134 | jsonLike _                     = False
  135 | 
  136 | -- Does the candidate carry node properties?
  137 | pendProps : Pending -> Bool
  138 | pendProps (PScalar pr _ _) = not (isNoProps pr)
  139 | pendProps (PProps _)       = True
  140 | pendProps _                = False
  141 | 
  142 | --------------------------------------------------------------------------------
  143 | --          Rule Type
  144 | --------------------------------------------------------------------------------
  145 | 
  146 | ||| A parsing rule, consuming a prefix of the remaining input (a strict
  147 | ||| one if `b` is `True`).
  148 | |||
  149 | ||| Totality: all recursion in the rules below runs over the strictly
  150 | ||| shrinking character list via `SuffixAcc`. Since some nodes may be
  151 | ||| empty (consuming nothing), every loop derives its strictness from a
  152 | ||| separator it consumed itself (a comma, colon, dash, marker, or line
  153 | ||| break) before recursing. Lookahead over blank and comment lines
  154 | ||| (`skipToContent`) returns a non-erased, possibly-empty `Suffix`:
  155 | ||| where a rule continues after such a skip without other consumption,
  156 | ||| it matches `Same`/`Uncons` explicitly so the recursion goes through
  157 | ||| a projection of its `SuffixAcc` argument.
  158 | public export
  159 | 0 Rule : Bool -> Type -> Type
  160 | Rule b a =
  161 |      YState
  162 |   -> (cs : List Char)
  163 |   -> (0 acc : SuffixAcc cs)
  164 |   -> Result0 b Char cs (BoundedErr YErr) a
  165 | 
  166 | --------------------------------------------------------------------------------
  167 | --          Node Properties
  168 | --------------------------------------------------------------------------------
  169 | 
  170 | ||| Parses node properties [spec: c-ns-properties]: an anchor and a tag
  171 | ||| in either order, separated by white space within the line. Must be
  172 | ||| called at a `&` or `!`.
  173 | pProps :
  174 |      TagEnv
  175 |   -> Props
  176 |   -> Position
  177 |   -> (cs : List Char)
  178 |   -> (0 a : SuffixAcc cs)
  179 |   -> Result0 True Char cs (BoundedErr YErr) (Props, Position)
  180 | pProps env pr pos ('&' :: cs) sa@(SA r) = case pr.anchor of
  181 |   Just _  => custom (oneChar pos) MultipleAnchors
  182 |   Nothing => case anchorName ('&' :: cs) of
  183 |     Succ nm rem @{prf} =>
  184 |       let IL cnt tbw2 rem2 w := inlineWhite rem
  185 |           pos2 := addCol cnt (move pos prf)
  186 |           pr2  := {anchor := Just nm} pr
  187 |           0 pp := trans w prf
  188 |        in if propStart rem2
  189 |             then succT (pProps env pr2 pos2 rem2 (r @{pp})) @{pp}
  190 |             else Succ0 (pr2, pos2) rem2 @{pp}
  191 |     Fail start errEnd err => Fail0 (boundedErr pos start errEnd err)
  192 | pProps env pr pos ('!' :: cs) sa@(SA r) = case pr.tag of
  193 |   NoTag => case tagToken ('!' :: cs) of
  194 |     Succ et rem @{prf} =>
  195 |       let pos1 := move pos prf
  196 |        in case resolved et of
  197 |             Left e   => custom (BS pos pos1) e
  198 |             Right tg =>
  199 |               let IL cnt tbw2 rem2 w := inlineWhite rem
  200 |                   pr2  := {tag := tg} pr
  201 |                   0 pp := trans w prf
  202 |                in if propStart rem2
  203 |                     then succT (pProps env pr2 (addCol cnt pos1) rem2 (r @{pp})) @{pp}
  204 |                     else Succ0 (pr2, addCol cnt pos1) rem2 @{pp}
  205 |     Fail start errEnd err => Fail0 (boundedErr pos start errEnd err)
  206 |   _ => custom (oneChar pos) MultipleTags
  207 | 
  208 |   where
  209 |     resolved : Either Tag (String, String) -> Either YErr Tag
  210 |     resolved (Left t)       = Right t
  211 |     resolved (Right (h, s)) = resolveTag env h s
  212 | pProps env pr pos [] _ = eoi
  213 | pProps env pr pos (c :: cs) _ =
  214 |   parseFail (oneChar pos) (Expected ["'&'", "'!'"] (pack [c]))
  215 | 
  216 | --------------------------------------------------------------------------------
  217 | --          Separation in Flow Context
  218 | --------------------------------------------------------------------------------
  219 | 
  220 | -- Blank and comment lines between flow tokens: continuation lines must
  221 | -- not be document markers and must be indented at least `mi` spaces.
  222 | flowLines :
  223 |      (tok : String)
  224 |   -> (b : Bounds)
  225 |   -> (mi : Nat)
  226 |   -> Position
  227 |   -> (cs : List Char)
  228 |   -> Result0 False Char cs (BoundedErr YErr) Position
  229 | flowLines tok b mi pos cs = case skipToContent cs of
  230 |   SR (L _ LEnd _) rem prf => Succ0 (endPos pos prf) rem @{prf}
  231 |   SR (L ind LContent tb) rem prf =>
  232 |     if ind >= mi
  233 |       then Succ0 (endPos pos prf) rem @{prf}
  234 |       else custom (oneChar $ endPos pos prf) BadIndent
  235 |   SR (L _ _ _) rem prf => unclosed b tok
  236 | 
  237 | -- A comment within flow content: consumes the rest of the line.
  238 | flowComment :
  239 |      (tok : String)
  240 |   -> (b : Bounds)
  241 |   -> (mi : Nat)
  242 |   -> Position
  243 |   -> (cs : List Char)
  244 |   -> Result0 False Char cs (BoundedErr YErr) Position
  245 | flowComment tok b mi pos (c :: cs) =
  246 |   if isBreak c
  247 |     then succF $ flowLines tok b mi (incLine pos) cs
  248 |     else succF $ flowComment tok b mi (incCol pos) cs
  249 | flowComment _ _ _ pos [] = Succ0 pos []
  250 | 
  251 | ||| Skips separation white space, comments and line breaks between flow
  252 | ||| tokens [spec: s-separate]. A `#` starts a comment only when preceded
  253 | ||| by white space or a line break (`sw` tracks whether white space was
  254 | ||| already seen).
  255 | flowSkip :
  256 |      (tok : String)
  257 |   -> (b : Bounds)
  258 |   -> (mi : Nat)
  259 |   -> (sw : Bool)
  260 |   -> Position
  261 |   -> (cs : List Char)
  262 |   -> Result0 False Char cs (BoundedErr YErr) Position
  263 | flowSkip tok b mi sw pos (c :: cs) =
  264 |   if isWhite c then succF $ flowSkip tok b mi True (incCol pos) cs
  265 |   else if isBreak c then succF $ flowLines tok b mi (incLine pos) cs
  266 |   else if c == '#' && sw then succF $ flowComment tok b mi (incCol pos) cs
  267 |   else Succ0 pos (c :: cs)
  268 | flowSkip _ _ _ _ pos [] = Succ0 pos []
  269 | 
  270 | --------------------------------------------------------------------------------
  271 | --          Line Ends in Block Context
  272 | --------------------------------------------------------------------------------
  273 | 
  274 | -- The rest of a `lineEnd` comment.
  275 | lineEndC : Position -> (cs : List Char) -> Result0 False Char cs (BoundedErr YErr) Position
  276 | lineEndC pos [] = Succ0 pos []
  277 | lineEndC pos (c :: cs) =
  278 |   if isBreak c
  279 |     then Succ0 pos (c :: cs)
  280 |     else succF $ lineEndC (incCol pos) cs
  281 | 
  282 | -- After a node that ends within a line (a flow collection, quoted
  283 | -- scalar or alias) in block context: only white space and a comment
  284 | -- may follow on the same line. Stops before the line break.
  285 | lineEnd : (sw : Bool) -> Position -> (cs : List Char) -> Result0 False Char cs (BoundedErr YErr) Position
  286 | lineEnd sw pos [] = Succ0 pos []
  287 | lineEnd sw pos (c :: cs) =
  288 |   if isWhite c then succF $ lineEnd True (incCol pos) cs
  289 |   else if isBreak c then Succ0 pos (c :: cs)
  290 |   else if c == '#' && sw then succF $ lineEndC (incCol pos) cs
  291 |   else custom (oneChar pos) TrailingContent
  292 | 
  293 | --------------------------------------------------------------------------------
  294 | --          Directives
  295 | --------------------------------------------------------------------------------
  296 | 
  297 | ||| Interprets a directive line [spec: l-directive]: `%YAML` (at most
  298 | ||| once per document, major version 1), `%TAG` (no duplicate handles),
  299 | ||| anything else is reserved and ignored.
  300 | parseDirective : TagEnv -> (sawYaml : Bool) -> String -> Either YErr (TagEnv, Bool)
  301 | parseDirective env sy ln = case takeWhile (not . isPrefixOf "#") (words ln) of
  302 |   ["%YAML", v]     =>
  303 |     if sy then Left (BadDirective "duplicate %YAML directive")
  304 |     else if versionOk (unpack v) then Right (env, True)
  305 |     else Left (BadVersion v)
  306 |   ("%YAML" :: _)   => Left (BadDirective ln)
  307 |   ["%TAG", h, pre] => case lookup h env.handles of
  308 |     Just _  => Left (DuplicateHandle h)
  309 |     Nothing =>
  310 |       if handleOk (unpack h)
  311 |         then Right (TE ((h, pre) :: env.handles), sy)
  312 |         else Left (BadDirective ln)
  313 |   ("%TAG" :: _)    => Left (BadDirective ln)
  314 |   _                => Right (env, sy)
  315 | 
  316 |   where
  317 |     versionOk : List Char -> Bool
  318 |     versionOk ('1' :: '.' :: ds@(_ :: _)) = all isDigit ds
  319 |     versionOk _                           = False
  320 | 
  321 |     inner : List Char -> Bool
  322 |     inner ['!']     = True
  323 |     inner (c :: t)  = isWordChar c && inner t
  324 |     inner []        = False
  325 | 
  326 |     handleOk : List Char -> Bool
  327 |     handleOk ['!']      = True
  328 |     handleOk ('!' :: t) = inner t
  329 |     handleOk _          = False
  330 | 
  331 | --------------------------------------------------------------------------------
  332 | --          Nodes
  333 | --------------------------------------------------------------------------------
  334 | 
  335 | -- Spec context note: `inFlow` distinguishes the FLOW-IN/FLOW-KEY
  336 | -- contexts (inside a flow collection) from FLOW-OUT/BLOCK-* (outside),
  337 | -- which changes where plain scalars end. `mi` is the minimum number of
  338 | -- indentation spaces for continuation lines (the spec's `n + 1`); `n`
  339 | -- is the column at which a block collection's entries are anchored.
  340 | 
  341 | mutual
  342 |   ||| Continuation lines of a plain scalar [spec: ns-plain-multi-line],
  343 |   ||| folded onto the text accumulated so far.
  344 |   plainMore :
  345 |        (inFlow : Bool)
  346 |     -> (mi : Nat)
  347 |     -> (acc : String)
  348 |     -> (pos : Position)
  349 |     -> (cs : List Char)
  350 |     -> (0 a : SuffixAcc cs)
  351 |     -> Result0 False Char cs (BoundedErr YErr) (String, Position)
  352 |   plainMore inFlow mi acc pos cs (SA r) = case plainCont inFlow mi cs of
  353 |     Stop => Succ0 (acc, pos) cs
  354 |     More k rem prf => case plainSegment inFlow rem of
  355 |       Succ s rem2 @{p2} =>
  356 |         let acc2 := acc ++ fold k ++ s
  357 |             pos2 := move (endPos pos prf) p2
  358 |             0 pp := trans p2 prf
  359 |          in trans (plainMore inFlow mi acc2 pos2 rem2 (r @{pp})) (weaken pp)
  360 |       Fail start errEnd err => Fail0 (boundedErr (endPos pos prf) start errEnd err)
  361 | 
  362 |     where
  363 |       fold : Nat -> String
  364 |       fold 0 = " "
  365 |       fold k = replicate k '\n'
  366 | 
  367 |   ||| An inline node candidate: properties, an alias, a single-line
  368 |   ||| scalar or a flow collection, parsed into its own event buffer so
  369 |   ||| callers can detect implicit mapping keys.
  370 |   cand :
  371 |        (inFlow : Bool)
  372 |     -> (mi : Nat)
  373 |     -> TagEnv
  374 |     -> Props
  375 |     -> Position
  376 |     -> (cs : List Char)
  377 |     -> (0 a : SuffixAcc cs)
  378 |     -> Result0 True Char cs (BoundedErr YErr) (Pending, Position)
  379 |   cand inFlow mi env pr pos [] _ = eoi
  380 |   cand inFlow mi env pr pos (c :: cs) sa@(SA r) =
  381 |     if c == '&' || c == '!'
  382 |       then case pProps env pr pos (c :: cs) sa of
  383 |         Fail0 e => Fail0 e
  384 |         Succ0 (pr2, p1) r1 @{q1} =>
  385 |           if candStart inFlow r1
  386 |             then succT (cand inFlow mi env pr2 p1 r1 (r @{q1})) @{q1}
  387 |             else Succ0 (PProps pr2, p1) r1 @{q1}
  388 |     else if c == '*'
  389 |       then
  390 |         if isNoProps pr
  391 |           then case anchorName (c :: cs) of
  392 |             Succ nm rem @{prf}    => Succ0 (PAlias nm, move pos prf) rem
  393 |             Fail start errEnd err => Fail0 (boundedErr pos start errEnd err)
  394 |           else parseFail (oneChar pos) (Unknown "properties on alias node")
  395 |     else if c == '[' || c == '{'
  396 |       then case flowNode inFlow mi env pr pos (YS pos [<]) (c :: cs) sa of
  397 |         Fail0 e => Fail0 e
  398 |         Succ0 st1 r1 => Succ0 (PFlow st1.evs, st1.pos) r1
  399 |     else if c == '\'' || c == '"'
  400 |       then
  401 |         let (tok, sty) := if c == '"'
  402 |                             then (doubleQuoted mi, DoubleQ)
  403 |                             else (singleQuoted mi, SingleQ)
  404 |          in case tok (c :: cs) of
  405 |               Succ s rem @{prf}     => Succ0 (PScalar pr sty s, endPos pos prf) rem
  406 |               Fail start errEnd err => Fail0 (boundedErr pos start errEnd err)
  407 |     else if isPlainFirst inFlow c cs
  408 |       then case plainSegment inFlow (c :: cs) of
  409 |         Succ s rem @{prf}     => Succ0 (PScalar pr Plain s, move pos prf) rem
  410 |         Fail start errEnd err => Fail0 (boundedErr pos start errEnd err)
  411 |       else parseFail (oneChar pos) (Unknown $ pack [c])
  412 | 
  413 |   ||| A single flow node [spec: ns-flow-node]: properties, an alias, a
  414 |   ||| scalar or a flow collection. Expects the input to be at a content
  415 |   ||| character. `sp` is the node's span start, which may lie before
  416 |   ||| `st.pos` when same-line properties were already consumed.
  417 |   flowNode : (inFlow : Bool) -> (mi : Nat) -> TagEnv -> Props -> (sp : Position) -> Rule True YState
  418 |   flowNode inFlow mi env pr sp st [] _ = eoi
  419 |   flowNode inFlow mi env pr sp st (c :: cs) sa@(SA r) = case c of
  420 |     '&' => flowProps inFlow mi env pr sp st (c :: cs) sa
  421 |     '!' => flowProps inFlow mi env pr sp st (c :: cs) sa
  422 |     '*' =>
  423 |       if isNoProps pr
  424 |         then case anchorName ('*' :: cs) of
  425 |           Succ nm rem @{prf} =>
  426 |             let pe := move st.pos prf
  427 |              in Succ0 (YS pe (st.evs :< bounded (Alias nm) st.pos pe)) rem @{prf}
  428 |           Fail start errEnd err => Fail0 (boundedErr st.pos start errEnd err)
  429 |         else parseFail (oneChar st.pos) (Unknown "properties on alias node")
  430 |     '[' => case flowSkip "[" (oneChar st.pos) mi False (incCol st.pos) cs of
  431 |       Fail0 e => Fail0 e
  432 |       Succ0 p1 r1 @{q1} =>
  433 |         let 0 pp := trans q1 (uncons Same)
  434 |             st1  := YS p1 (st.evs :< oneChar (SeqStart True pr.anchor pr.tag) st.pos)
  435 |          in succT (flowSeq env mi (oneChar st.pos) st1 r1 (r @{pp})) @{pp}
  436 |     '{' => case flowSkip "{" (oneChar st.pos) mi False (incCol st.pos) cs of
  437 |       Fail0 e => Fail0 e
  438 |       Succ0 p1 r1 @{q1} =>
  439 |         let 0 pp := trans q1 (uncons Same)
  440 |             st1  := YS p1 (st.evs :< oneChar (MapStart True pr.anchor pr.tag) st.pos)
  441 |          in succT (flowMap env mi (oneChar st.pos) st1 r1 (r @{pp})) @{pp}
  442 |     '\'' => case singleQuoted mi (c :: cs) of
  443 |       Succ s rem @{prf} =>
  444 |         let pe := endPos st.pos prf
  445 |          in Succ0 (YS pe (st.evs :< bounded (Scalar pr.anchor pr.tag SingleQ s) sp pe)) rem
  446 |       Fail start errEnd err => Fail0 (boundedErr st.pos start errEnd err)
  447 |     '"' => case doubleQuoted mi (c :: cs) of
  448 |       Succ s rem @{prf} =>
  449 |         let pe := endPos st.pos prf
  450 |          in Succ0 (YS pe (st.evs :< bounded (Scalar pr.anchor pr.tag DoubleQ s) sp pe)) rem
  451 |       Fail start errEnd err => Fail0 (boundedErr st.pos start errEnd err)
  452 |     _   =>
  453 |       if isPlainFirst inFlow c cs
  454 |         then case plainSegment inFlow (c :: cs) of
  455 |           Succ s rem @{prf} =>
  456 |             case plainMore inFlow mi s (move st.pos prf) rem (r @{prf}) of
  457 |               Fail0 e => Fail0 e
  458 |               Succ0 (s2, p2) rem2 @{q2} =>
  459 |                 Succ0 (YS p2 (st.evs :< bounded (Scalar pr.anchor pr.tag Plain s2) sp p2)) rem2
  460 |                   @{trans q2 prf}
  461 |           Fail start errEnd err => Fail0 (boundedErr st.pos start errEnd err)
  462 |         else parseFail (oneChar st.pos) (Unknown $ pack [c])
  463 | 
  464 |   ||| Properties of a flow node, then the node itself, which may sit on
  465 |   ||| a following line or be empty.
  466 |   flowProps : (inFlow : Bool) -> (mi : Nat) -> TagEnv -> Props -> (sp : Position) -> Rule True YState
  467 |   flowProps inFlow mi env pr sp st cs sa@(SA r) = case pProps env pr st.pos cs sa of
  468 |     Fail0 e => Fail0 e
  469 |     Succ0 (pr2, p1) r1 @{q1} =>
  470 |       if candStart inFlow r1
  471 |         then succT (flowNode inFlow mi env pr2 sp (YS p1 st.evs) r1 (r @{q1})) @{q1}
  472 |         else if breakStart r1
  473 |           then case skipToContent r1 of
  474 |             SR (L ind LContent tb) r2 prf2 =>
  475 |               if ind >= mi
  476 |                 then
  477 |                   let 0 pp := trans prf2 q1
  478 |                       pc   := endPos p1 prf2
  479 |                    in succT (flowNode inFlow mi env pr2 pc (YS pc st.evs) r2 (r @{pp})) @{pp}
  480 |                 else custom (oneChar $ endPos p1 prf2) BadIndent
  481 |             SR _ _ _ => Succ0 (YS p1 (emptyScalarP pr2 sp st.evs)) r1 @{q1}
  482 |           else Succ0 (YS p1 (emptyScalarP pr2 sp st.evs)) r1 @{q1}
  483 | 
  484 |   ||| Inside a flow sequence [spec: c-flow-sequence], at a content
  485 |   ||| character: an entry (possibly a `key: value` pair, implicit or
  486 |   ||| explicit) or the closing bracket.
  487 |   flowSeq : TagEnv -> (mi : Nat) -> (b : Bounds) -> Rule True YState
  488 |   flowSeq env mi b st (']' :: cs) _ =
  489 |     Succ0 (emit (oneChar st.pos) SeqEnd $ {pos $= incCol} st) cs
  490 |   flowSeq env mi b st []          _ = unclosed b "["
  491 |   flowSeq env mi b st (':' :: cs) sa@(SA r) =
  492 |     -- a pair with an empty key, unless the colon starts a plain scalar
  493 |     if plainSafeNext cs
  494 |       then seqItem env mi b st (':' :: cs) sa
  495 |       else
  496 |         let evs1 := emptyScalar st.pos (st.evs :< oneChar (MapStart True Nothing NoTag) st.pos)
  497 |          in case flowSkip "[" b mi False (incCol st.pos) cs of
  498 |               Fail0 e => Fail0 e
  499 |               Succ0 p1 r1 @{q1} =>
  500 |                 let 0 pp := trans q1 (uncons Same)
  501 |                  in case flowVal env mi (YS p1 evs1) r1 (r @{pp}) of
  502 |                       Fail0 e => Fail0 e
  503 |                       Succ0 st2 r2 @{q2} =>
  504 |                         let 0 p2c := trans q2 pp
  505 |                          in succT (seqTail env mi b False (emit (oneChar st2.pos) MapEnd st2) r2 (r @{p2c})) @{p2c}
  506 |   flowSeq env mi b st ('?' :: cs) sa@(SA r) =
  507 |     -- an explicit pair [spec: ns-flow-map-explicit-entry]
  508 |     if plainSafeNext cs
  509 |       then seqItem env mi b st ('?' :: cs) sa
  510 |       else
  511 |         let evs1 := st.evs :< oneChar (MapStart True Nothing NoTag) st.pos
  512 |          in case flowSkip "[" b mi False (incCol st.pos) cs of
  513 |               Fail0 e => Fail0 e
  514 |               Succ0 p1 r1 @{q1} =>
  515 |                 let 0 pp := trans q1 (uncons Same)
  516 |                  in case pairKey env mi b (YS p1 evs1) r1 (r @{pp}) of
  517 |                       Fail0 e => Fail0 e
  518 |                       Succ0 st2 r2 @{q2} =>
  519 |                         let 0 p2c := trans q2 pp
  520 |                          in succT (seqTail env mi b False st2 r2 (r @{p2c})) @{p2c}
  521 |   flowSeq env mi b st cs sa = seqItem env mi b st cs sa
  522 | 
  523 |   ||| The key (or whole content) of an explicit flow pair, after its
  524 |   ||| `?` indicator, followed by an optional `: value`; emits the
  525 |   ||| closing MapEnd.
  526 |   pairKey : TagEnv -> (mi : Nat) -> (b : Bounds) -> Rule False YState
  527 |   pairKey env mi b st cs sa@(SA r) =
  528 |     if emptyNext cs
  529 |       then Succ0 ({evs $= (:< oneChar MapEnd st.pos) . emptyScalar st.pos . emptyScalar st.pos} st) cs
  530 |       else case flowNode True mi env noProps st.pos st cs sa of
  531 |         Fail0 e => Fail0 e
  532 |         Succ0 st1 r1 @{q1} => case flowSkip "[" b mi False st1.pos r1 of
  533 |           Fail0 e => Fail0 e
  534 |           Succ0 p2 (':' :: r2) @{q2} =>
  535 |             case flowSkip "[" b mi False (incCol p2) r2 of
  536 |               Fail0 e => Fail0 e
  537 |               Succ0 p3 r3 @{q3} =>
  538 |                 let 0 pp := trans q3 (trans (uncons Same) (trans q2 q1))
  539 |                  in case flowVal env mi (YS p3 st1.evs) r3 (r @{pp}) of
  540 |                       Fail0 e => Fail0 e
  541 |                       Succ0 st4 r4 @{q4} =>
  542 |                         Succ0 (emit (oneChar st4.pos) MapEnd st4) r4 @{weaken $ trans q4 pp}
  543 |           Succ0 p2 r2 @{q2} =>
  544 |             Succ0 (YS p2 (st1.evs :< oneChar (Scalar Nothing NoTag Plain "") p2 :< oneChar MapEnd p2)) r2
  545 |               @{weaken $ trans q2 q1}
  546 | 
  547 |     where
  548 |       emptyNext : List Char -> Bool
  549 |       emptyNext (c :: _) = c == ']' || c == ','
  550 |       emptyNext []       = False
  551 | 
  552 |   ||| An ordinary flow sequence entry: an inline candidate, possibly
  553 |   ||| forming an implicit single pair [spec: ns-flow-pair].
  554 |   seqItem : TagEnv -> (mi : Nat) -> (b : Bounds) -> Rule True YState
  555 |   seqItem env mi b st cs sa@(SA r) =
  556 |     case cand True mi env noProps st.pos cs sa of
  557 |       Fail0 e => Fail0 e
  558 |       Succ0 (pend, p1) r1 @{q1} =>
  559 |         let IL cnt tbw r2 w := inlineWhite r1
  560 |             p2   := addCol cnt p1
  561 |             0 pw := trans w q1
  562 |          in if colonFlow r2 || (jsonLike pend && colonNext r2)
  563 |               then -- a single pair, an implicit mapping [spec: ns-flow-pair]
  564 |                 if p1.line /= st.pos.line
  565 |                   then custom (BS st.pos p1) InvalidKey
  566 |                   else case r2 of
  567 |                     ':' :: r3 =>
  568 |                       let evs1 := flushPend st.pos p1 (st.evs :< oneChar (MapStart True Nothing NoTag) st.pos) pend
  569 |                           0 pc := trans (uncons Same) (trans w q1)
  570 |                        in case flowSkip "[" b mi False (incCol p2) r3 of
  571 |                             Fail0 e => Fail0 e
  572 |                             Succ0 p4 r4 @{q4} =>
  573 |                               let 0 p4c := trans q4 pc
  574 |                                in case flowVal env mi (YS p4 evs1) r4 (r @{p4c}) of
  575 |                                     Fail0 e => Fail0 e
  576 |                                     Succ0 st5 r5 @{q5} =>
  577 |                                       let 0 p5c := trans q5 p4c
  578 |                                        in succT (seqTail env mi b False (emit (oneChar st5.pos) MapEnd st5) r5 (r @{p5c})) @{p5c}
  579 |                     _ => unclosed b "["
  580 |               else case pend of
  581 |                 PFlow d   =>
  582 |                   succT (seqTail env mi b (cnt > 0) (YS p2 (st.evs ++ d)) r2 (r @{pw})) @{pw}
  583 |                 PAlias a  =>
  584 |                   succT (seqTail env mi b (cnt > 0) (YS p2 (st.evs :< bounded (Alias a) st.pos p1)) r2 (r @{pw})) @{pw}
  585 |                 PProps pr =>
  586 |                   succT (seqTail env mi b (cnt > 0) (YS p2 (emptyScalarP pr st.pos st.evs)) r2 (r @{pw})) @{pw}
  587 |                 PScalar pr Plain s =>
  588 |                   case plainMore True mi s p2 r2 (r @{pw}) of
  589 |                     Fail0 e => Fail0 e
  590 |                     Succ0 (s2, p3) r3 @{q3} =>
  591 |                       let 0 pp := trans q3 pw
  592 |                           st3  := YS p3 (st.evs :< bounded (Scalar pr.anchor pr.tag Plain s2) st.pos p3)
  593 |                        in succT (seqTail env mi b (cnt > 0) st3 r3 (r @{pp})) @{pp}
  594 |                 PScalar pr sty s =>
  595 |                   let st2 := YS p2 (st.evs :< bounded (Scalar pr.anchor pr.tag sty s) st.pos p1)
  596 |                    in succT (seqTail env mi b (cnt > 0) st2 r2 (r @{pw})) @{pw}
  597 | 
  598 |   ||| After a flow sequence entry: a comma and further entries, or the
  599 |   ||| closing bracket.
  600 |   seqTail : TagEnv -> (mi : Nat) -> (b : Bounds) -> (sw : Bool) -> Rule True YState
  601 |   seqTail env mi b sw st cs (SA r) = case flowSkip "[" b mi sw st.pos cs of
  602 |     Fail0 e => Fail0 e
  603 |     Succ0 p2 (']' :: r2) @{q2} =>
  604 |       Succ0 (YS (incCol p2) (st.evs :< oneChar SeqEnd p2)) r2 @{trans (uncons Same) q2}
  605 |     Succ0 p2 (',' :: r2) @{q2} =>
  606 |       case flowSkip "[" b mi False (incCol p2) r2 of
  607 |         Fail0 e => Fail0 e
  608 |         Succ0 p3 r3 @{q3} =>
  609 |           let 0 pp := trans q3 (trans (uncons Same) q2)
  610 |            in succT (flowSeq env mi b (YS p3 st.evs) r3 (r @{pp})) @{pp}
  611 |     Succ0 p2 [] => unclosed b "["
  612 |     Succ0 p2 (x :: _) =>
  613 |       parseFail (oneChar p2) (Expected ["','", "']'"] (pack [x]))
  614 | 
  615 |   ||| Inside a flow mapping [spec: c-flow-mapping], at a content
  616 |   ||| character: an entry or the closing brace.
  617 |   flowMap : TagEnv -> (mi : Nat) -> (b : Bounds) -> Rule True YState
  618 |   flowMap env mi b st ('}' :: cs) _ =
  619 |     Succ0 (emit (oneChar st.pos) MapEnd $ {pos $= incCol} st) cs
  620 |   flowMap env mi b st []          _ = unclosed b "{"
  621 |   flowMap env mi b st ('?' :: cs) sa@(SA r) =
  622 |     -- an explicit entry [spec: ns-flow-map-explicit-entry], unless the
  623 |     -- question mark starts a plain scalar
  624 |     if plainSafeNext cs
  625 |       then flowEntry env mi b st ('?' :: cs) sa
  626 |       else case flowSkip "{" b mi False (incCol st.pos) cs of
  627 |         Fail0 e => Fail0 e
  628 |         Succ0 p1 r1 @{q1} =>
  629 |           let 0 pp := trans q1 (uncons Same)
  630 |            in if emptyNext r1
  631 |                 then succT (mapTail env mi b (YS p1 ({evs $= emptyScalar st.pos . emptyScalar st.pos} st).evs) r1 (r @{pp})) @{pp}
  632 |                 else succT (flowEntry env mi b (YS p1 st.evs) r1 (r @{pp})) @{pp}
  633 | 
  634 |     where
  635 |       emptyNext : List Char -> Bool
  636 |       emptyNext (c2 :: _) = c2 == '}' || c2 == ','
  637 |       emptyNext []        = False
  638 | 
  639 |   flowMap env mi b st cs sa = flowEntry env mi b st cs sa
  640 | 
  641 |   ||| A single flow mapping entry (without a leading `?` indicator).
  642 |   flowEntry : TagEnv -> (mi : Nat) -> (b : Bounds) -> Rule True YState
  643 |   flowEntry env mi b st [] _ = unclosed b "{"
  644 |   flowEntry env mi b st (c :: cs) sa@(SA r) =
  645 |     if c == ':' && not (plainSafeNext cs)
  646 |       then -- an entry with an empty key [spec: c-ns-flow-map-empty-key-entry]
  647 |         case flowSkip "{" b mi False (incCol st.pos) cs of
  648 |           Fail0 e => Fail0 e
  649 |           Succ0 p1 r1 @{q1} =>
  650 |             let 0 pp := trans q1 (uncons Same)
  651 |              in case flowVal env mi (YS p1 (emptyScalar st.pos st.evs)) r1 (r @{pp}) of
  652 |                   Fail0 e => Fail0 e
  653 |                   Succ0 st2 r2 @{q2} => case flowSkip "{" b mi False st2.pos r2 of
  654 |                     Fail0 e => Fail0 e
  655 |                     Succ0 p3 r3 @{q3} =>
  656 |                       let 0 pp3 := trans (trans q3 (trans q2 q1)) (uncons Same)
  657 |                        in succT (mapTail env mi b (YS p3 st2.evs) r3 (r @{pp3})) @{pp3}
  658 |       else -- an entry starting with a key node
  659 |         case flowNode True mi env noProps st.pos st (c :: cs) sa of
  660 |           Fail0 e => Fail0 e
  661 |           Succ0 st1 r1 @{q1} => case flowSkip "{" b mi False st1.pos r1 of
  662 |             Fail0 e => Fail0 e
  663 |             Succ0 p2 (':' :: r2) @{q2} =>
  664 |               case flowSkip "{" b mi False (incCol p2) r2 of
  665 |                 Fail0 e => Fail0 e
  666 |                 Succ0 p3 r3 @{q3} =>
  667 |                   let 0 pp := trans q3 (trans (uncons Same) (trans q2 q1))
  668 |                    in case flowVal env mi (YS p3 st1.evs) r3 (r @{pp}) of
  669 |                         Fail0 e => Fail0 e
  670 |                         Succ0 st4 r4 @{q4} =>
  671 |                           case flowSkip "{" b mi False st4.pos r4 of
  672 |                             Fail0 e => Fail0 e
  673 |                             Succ0 p5 r5 @{q5} =>
  674 |                               let 0 pp5 := trans q5 (trans q4 pp)
  675 |                                in succT (mapTail env mi b (YS p5 st4.evs) r5 (r @{pp5})) @{pp5}
  676 |             Succ0 p2 r2 @{q2} =>
  677 |               -- no colon: the value is empty [spec: ns-flow-map-yaml-key-entry]
  678 |               let 0 pp := trans q2 q1
  679 |                in succT (mapTail env mi b (YS p2 (emptyScalar p2 st1.evs)) r2 (r @{pp})) @{pp}
  680 | 
  681 |   ||| The value of a flow mapping entry or pair, after its `:`
  682 |   ||| indicator and any separation: empty if the entry ends here.
  683 |   flowVal : TagEnv -> (mi : Nat) -> Rule False YState
  684 |   flowVal env mi st []          _   = Succ0 ({evs $= emptyScalar st.pos} st) []
  685 |   flowVal env mi st (',' :: cs) _   = Succ0 ({evs $= emptyScalar st.pos} st) (',' :: cs)
  686 |   flowVal env mi st ('}' :: cs) _   = Succ0 ({evs $= emptyScalar st.pos} st) ('}' :: cs)
  687 |   flowVal env mi st (']' :: cs) _   = Succ0 ({evs $= emptyScalar st.pos} st) (']' :: cs)
  688 |   flowVal env mi st cs          acc = weaken $ flowNode True mi env noProps st.pos st cs acc
  689 | 
  690 |   ||| After a complete flow mapping entry: a comma followed by the next
  691 |   ||| entry, or the closing brace.
  692 |   mapTail : TagEnv -> (mi : Nat) -> (b : Bounds) -> Rule True YState
  693 |   mapTail env mi b st ('}' :: cs) _ =
  694 |     Succ0 (emit (oneChar st.pos) MapEnd $ {pos $= incCol} st) cs
  695 |   mapTail env mi b st (',' :: cs) (SA r) =
  696 |     case flowSkip "{" b mi False (incCol st.pos) cs of
  697 |       Fail0 e => Fail0 e
  698 |       Succ0 p1 r1 @{q1} =>
  699 |         let 0 pp := trans q1 (uncons Same)
  700 |          in succT (flowMap env mi b (YS p1 st.evs) r1 (r @{pp})) @{pp}
  701 |   mapTail env mi b st []          _ = unclosed b "{"
  702 |   mapTail env mi b st (x :: _)    _ =
  703 |     parseFail (oneChar st.pos) (Expected ["','", "'}'"] (pack [x]))
  704 | 
  705 |   ||| A block node [spec: s-l+block-node]: input at a content
  706 |   ||| character, whose column defines the node's indentation (unless
  707 |   ||| overridden by `nOv`, as for nodes on a `---` marker's line).
  708 |   ||| `oprops` are properties from a preceding line, belonging to a
  709 |   ||| block collection found here (or merged into a scalar). With
  710 |   ||| `tabSep`, the content was preceded by tabs, which is an error for
  711 |   ||| block structure [spec 6.1].
  712 |   blockNode : (mi : Nat) -> (nOv : Maybe Nat) -> (tabSep : Bool) -> TagEnv -> Props -> Rule True YState
  713 |   blockNode mi nOv tabSep env oprops st [] _ = eoi
  714 |   blockNode mi nOv tabSep env oprops st (c :: cs) sa@(SA r) =
  715 |     let n := maybe st.pos.col id nOv
  716 |      in if c == '-' && wordEnd cs
  717 |           then
  718 |             if tabSep
  719 |               then custom (oneChar st.pos) TabIndent
  720 |               else seqLoop env n (emit (oneChar st.pos) (SeqStart False oprops.anchor oprops.tag) st) (c :: cs) sa
  721 |         else if c == '?' && wordEnd cs
  722 |           then
  723 |             if tabSep
  724 |               then custom (oneChar st.pos) TabIndent
  725 |               else case expEntry env n (emit (oneChar st.pos) (MapStart False oprops.anchor oprops.tag) st) (c :: cs) sa of
  726 |                 Fail0 e => Fail0 e
  727 |                 Succ0 st1 r1 @{q1} => trans (blockMap env n st1 r1 (r @{q1})) q1
  728 |         else if c == ':' && wordEnd cs
  729 |           then
  730 |             if tabSep
  731 |               then custom (oneChar st.pos) TabIndent
  732 |               else
  733 |                 let evs1 := emptyScalar st.pos (st.evs :< oneChar (MapStart False oprops.anchor oprops.tag) st.pos)
  734 |                  in case afterKey env n False noProps (YS (incCol st.pos) evs1) cs (r @{uncons Same}) of
  735 |                       Fail0 e => Fail0 e
  736 |                       Succ0 st1 r1 @{q1} =>
  737 |                         let 0 p1 := trans q1 (uncons Same)
  738 |                          in trans (blockMap env n st1 r1 (r @{p1})) p1
  739 |         else if c == '|' || c == '>'
  740 |           then case blockScalar (c == '>') mi (c :: cs) of
  741 |             Succ s rem @{prf} =>
  742 |               let sty := if c == '>' then Folded else Literal
  743 |                in let pe := endPos st.pos prf
  744 |                    in Succ0 (YS pe (st.evs :< bounded (Scalar oprops.anchor oprops.tag sty s) st.pos pe)) rem
  745 |             Fail start errEnd err => Fail0 (boundedErr st.pos start errEnd err)
  746 |         else case cand False mi env noProps st.pos (c :: cs) sa of
  747 |           Fail0 e => Fail0 e
  748 |           Succ0 (pend, p1) r1 @{q1} =>
  749 |             let IL cnt tbw r2 w := inlineWhite r1
  750 |                 p2   := addCol cnt p1
  751 |                 0 pw := trans w q1
  752 |              in if colonBlock r2
  753 |                   then -- this node is a block mapping; `pend` its first key
  754 |                     if tabSep
  755 |                       then custom (oneChar st.pos) TabIndent
  756 |                     else if p1.line /= st.pos.line
  757 |                       then custom (BS st.pos p1) InvalidKey
  758 |                     else if isJust nOv && pendProps pend
  759 |                       then custom (BS st.pos p1) InvalidKey
  760 |                       else case r2 of
  761 |                         ':' :: r3 =>
  762 |                           let evs1 := flushPend st.pos p1 (st.evs :< oneChar (MapStart False oprops.anchor oprops.tag) st.pos) pend
  763 |                               0 pc := trans (uncons Same) (trans w q1)
  764 |                            in case afterKey env n False noProps (YS (incCol p2) evs1) r3 (r @{pc}) of
  765 |                                 Fail0 e => Fail0 e
  766 |                                 Succ0 st4 r4 @{q4} =>
  767 |                                   let 0 p4 := trans q4 pc
  768 |                                    in trans (blockMap env n st4 r4 (r @{p4})) p4
  769 |                         _ => eoi
  770 |                   else case pend of
  771 |                     PFlow d => case patchFlow oprops d of
  772 |                       Left e   => custom (BS st.pos p1) e
  773 |                       Right d2 => case lineEnd (cnt > 0) p2 r2 of
  774 |                         Fail0 e => Fail0 e
  775 |                         Succ0 p3 r3 @{q3} =>
  776 |                           Succ0 (YS p3 (st.evs ++ d2)) r3 @{trans q3 pw}
  777 |                     PAlias a =>
  778 |                       if isNoProps oprops
  779 |                         then case lineEnd (cnt > 0) p2 r2 of
  780 |                           Fail0 e => Fail0 e
  781 |                           Succ0 p3 r3 @{q3} =>
  782 |                             Succ0 (YS p3 (st.evs :< bounded (Alias a) st.pos p1)) r3 @{trans q3 pw}
  783 |                         else parseFail (oneChar st.pos) (Unknown "properties on alias node")
  784 |                     PProps pr => case mergeProps oprops pr of
  785 |                       Left e    => custom (BS st.pos p1) e
  786 |                       Right prm => case bsStart r2 of
  787 |                         Just f => case blockScalar f mi r2 of
  788 |                           Succ s rem @{prf} =>
  789 |                             let sty := if f then Folded else Literal
  790 |                              in let pe := endPos p2 prf
  791 |                                  in Succ0 (YS pe (st.evs :< bounded (Scalar prm.anchor prm.tag sty s) st.pos pe)) rem
  792 |                                       @{trans prf pw}
  793 |                           Fail start errEnd err => Fail0 (boundedErr p2 start errEnd err)
  794 |                         Nothing =>
  795 |                           if breakStart r2
  796 |                             then case skipToContent r2 of
  797 |                               SR (L ind LContent tb) r3 prf3 =>
  798 |                                 if ind >= mi
  799 |                                   then
  800 |                                     let 0 p3 := trans prf3 pw
  801 |                                      in succT (blockNode mi Nothing tb env prm (YS (endPos p2 prf3) st.evs) r3 (r @{p3})) @{p3}
  802 |                                   else Succ0 (YS p2 (emptyScalarP prm st.pos st.evs)) r2 @{pw}
  803 |                               SR _ _ _ => Succ0 (YS p2 (emptyScalarP prm st.pos st.evs)) r2 @{pw}
  804 |                             else if null r2
  805 |                               then Succ0 (YS p2 (emptyScalarP prm st.pos st.evs)) r2 @{pw}
  806 |                               else parseFail (oneChar p2) (Unknown "content after node properties")
  807 |                     PScalar pr Plain s => case mergeProps oprops pr of
  808 |                       Left e    => custom (BS st.pos p1) e
  809 |                       Right prm => case plainMore False mi s p2 r2 (r @{pw}) of
  810 |                         Fail0 e => Fail0 e
  811 |                         Succ0 (s2, p3) r3 @{q3} =>
  812 |                           if colonBlock r3
  813 |                             then custom (BS st.pos p3) InvalidKey
  814 |                             else
  815 |                               Succ0 (YS p3 (st.evs :< bounded (Scalar prm.anchor prm.tag Plain s2) st.pos p3)) r3
  816 |                                 @{trans q3 pw}
  817 |                     PScalar pr sty s => case mergeProps oprops pr of
  818 |                       Left e    => custom (BS st.pos p1) e
  819 |                       Right prm => case lineEnd (cnt > 0) p2 r2 of
  820 |                         Fail0 e => Fail0 e
  821 |                         Succ0 p3 r3 @{q3} =>
  822 |                           Succ0 (YS p3 (st.evs :< bounded (Scalar prm.anchor prm.tag sty s) st.pos p1)) r3
  823 |                             @{trans q3 pw}
  824 | 
  825 |   ||| Entries of a block sequence anchored at column `n` [spec:
  826 |   ||| l+block-sequence], starting at a `- ` indicator. Emits the SeqEnd
  827 |   ||| when the indentation ends.
  828 |   seqLoop : TagEnv -> (n : Nat) -> Rule True YState
  829 |   seqLoop env n st ('-' :: cs) (SA r) =
  830 |     case seqEntry env n (YS (incCol st.pos) st.evs) cs (r @{uncons Same}) of
  831 |       Fail0 e => Fail0 e
  832 |       Succ0 st1 r1 @{q1} =>
  833 |         let 0 p1 := trans q1 (uncons Same)
  834 |          in case skipToContent r1 of
  835 |               SR (L ind LContent tb) r2 prf2 =>
  836 |                 if ind == n && dashNext r2
  837 |                   then
  838 |                     if tb
  839 |                       then custom (oneChar $ endPos st1.pos prf2) TabIndent
  840 |                       else
  841 |                         let 0 pp := trans prf2 p1
  842 |                          in succT (seqLoop env n (YS (endPos st1.pos prf2) st1.evs) r2 (r @{pp})) @{pp}
  843 |                   else Succ0 (emit (oneChar st1.pos) SeqEnd st1) r1 @{p1}
  844 |               SR _ _ _ => Succ0 (emit (oneChar st1.pos) SeqEnd st1) r1 @{p1}
  845 |   seqLoop env n st (x :: _) _ = parseFail (oneChar st.pos) (Expected ["'-'"] (pack [x]))
  846 |   seqLoop env n st []       _ = eoi
  847 | 
  848 |   ||| A block sequence entry after its `- ` indicator [spec:
  849 |   ||| c-l-block-seq-entry]: same-line content (including compact
  850 |   ||| collections), a more indented node on following lines, or empty.
  851 |   seqEntry : TagEnv -> (n : Nat) -> Rule False YState
  852 |   seqEntry env n st cs sa@(SA r) =
  853 |     let IL cnt tbw r2 w := inlineWhite cs
  854 |         p2 := addCol cnt st.pos
  855 |      in case r2 of
  856 |           [] => Succ0 (YS p2 (emptyScalar p2 st.evs)) [] @{w}
  857 |           x :: xs =>
  858 |             if isBreak x || x == '#'
  859 |               then case skipToContent (x :: xs) of
  860 |                 SR (L ind LContent tb) r3 prf3 =>
  861 |                   if ind >= S n
  862 |                     then
  863 |                       let st3 := YS (endPos p2 prf3) st.evs
  864 |                        in case trans prf3 w of
  865 |                             Same     => weaken $ blockNode (S n) Nothing tb env noProps st3 r3 sa
  866 |                             Uncons u =>
  867 |                               weaken $ trans (blockNode (S n) Nothing tb env noProps st3 r3 (r @{uncons u}))
  868 |                                              (weaken (uncons u))
  869 |                     else Succ0 (YS p2 (emptyScalar p2 st.evs)) (x :: xs) @{w}
  870 |                 SR _ _ _ => Succ0 (YS p2 (emptyScalar p2 st.evs)) (x :: xs) @{w}
  871 |               else
  872 |                 let st2 := YS p2 st.evs
  873 |                  in case w of
  874 |                       Same     => weaken $ blockNode (S n) Nothing tbw env noProps st2 (x :: xs) sa
  875 |                       Uncons u =>
  876 |                         weaken $ trans (blockNode (S n) Nothing tbw env noProps st2 (x :: xs) (r @{uncons u}))
  877 |                                        (weaken (uncons u))
  878 | 
  879 |   ||| Further entries of a block mapping anchored at column `n` [spec:
  880 |   ||| l+block-mapping]: emits the MapEnd when the indentation ends.
  881 |   blockMap : TagEnv -> (n : Nat) -> Rule False YState
  882 |   blockMap env n st cs sa@(SA r) = case skipToContent cs of
  883 |     SR (L ind LContent tb) r2 prf2 =>
  884 |       if ind == n
  885 |         then
  886 |           if tb then custom (oneChar $ endPos st.pos prf2) TabIndent else
  887 |           let st2 := YS (endPos st.pos prf2) st.evs
  888 |            in case prf2 of
  889 |                 Same => case mapEntry env n st2 r2 sa of
  890 |                   Fail0 e => Fail0 e
  891 |                   Succ0 st3 r3 @{q3} =>
  892 |                     trans (blockMap env n st3 r3 (r @{q3})) (weaken q3)
  893 |                 Uncons u => case mapEntry env n st2 r2 (r @{uncons u}) of
  894 |                   Fail0 e => Fail0 e
  895 |                   Succ0 st3 r3 @{q3} =>
  896 |                     let 0 p3 := trans q3 (uncons u)
  897 |                      in trans (blockMap env n st3 r3 (r @{p3})) (weaken p3)
  898 |         else Succ0 (emit (oneChar st.pos) MapEnd st) cs
  899 |     SR _ _ _ => Succ0 (emit (oneChar st.pos) MapEnd st) cs
  900 | 
  901 |   ||| A single block mapping entry at indent `n` [spec:
  902 |   ||| ns-l-block-map-entry]: explicit (`? `), an empty key (`: `), or
  903 |   ||| an implicit single-line key followed by `:`.
  904 |   mapEntry : TagEnv -> (n : Nat) -> Rule True YState
  905 |   mapEntry env n st [] _ = eoi
  906 |   mapEntry env n st (c :: cs) sa@(SA r) =
  907 |     if c == '?' && wordEnd cs
  908 |       then expEntry env n st (c :: cs) sa
  909 |     else if c == ':' && wordEnd cs
  910 |       then case afterKey env n False noProps (YS (incCol st.pos) (emptyScalar st.pos st.evs)) cs (r @{uncons Same}) of
  911 |         Fail0 e => Fail0 e
  912 |         Succ0 st1 r1 @{q1} => Succ0 st1 r1 @{trans q1 (uncons Same)}
  913 |     else case cand False (S n) env noProps st.pos (c :: cs) sa of
  914 |       Fail0 e => Fail0 e
  915 |       Succ0 (pend, p1) r1 @{q1} =>
  916 |         let IL cnt tbw r2 w := inlineWhite r1
  917 |             p2   := addCol cnt p1
  918 |             0 pw := trans w q1
  919 |          in if colonBlock r2
  920 |               then
  921 |                 if p1.line /= st.pos.line
  922 |                   then custom (BS st.pos p1) InvalidKey
  923 |                   else case r2 of
  924 |                     ':' :: r3 =>
  925 |                       let 0 pc := trans (uncons Same) (trans w q1)
  926 |                        in case afterKey env n False noProps (YS (incCol p2) (flushPend st.pos p1 st.evs pend)) r3 (r @{pc}) of
  927 |                             Fail0 e => Fail0 e
  928 |                             Succ0 st4 r4 @{q4} => Succ0 st4 r4 @{trans q4 pc}
  929 |                     _ => eoi
  930 |               else case r2 of
  931 |                 x :: _ => parseFail (oneChar p2) (Expected ["':'"] (pack [x]))
  932 |                 []     => eoi
  933 | 
  934 |   ||| An explicit block mapping entry [spec:
  935 |   ||| c-l-block-map-explicit-entry], starting at its `?` indicator at
  936 |   ||| indent `n`: a block node as key, then optionally a `:` line at
  937 |   ||| the same indent with the value.
  938 |   expEntry : TagEnv -> (n : Nat) -> Rule True YState
  939 |   expEntry env n st ('?' :: cs) sa@(SA r) =
  940 |     let IL cnt tbw r2 w := inlineWhite cs
  941 |         p2 := addCol cnt (incCol st.pos)
  942 |         keyRes : Result0 True Char ('?' :: cs) (BoundedErr YErr) YState :=
  943 |           case r2 of
  944 |             [] => Succ0 (YS p2 (emptyScalar p2 st.evs)) [] @{trans w (uncons Same)}
  945 |             x :: xs =>
  946 |               if isBreak x || x == '#'
  947 |                 then case skipToContent (x :: xs) of
  948 |                   SR (L ind LContent tb) r3 prf3 =>
  949 |                     -- a zero-indented sequence may sit at the same
  950 |                     -- indent as the `?` indicator [spec: seq-spaces]
  951 |                     if ind >= S n || (ind == n && dashNext r3)
  952 |                       then
  953 |                         let 0 p3 := trans prf3 (trans w (uncons Same))
  954 |                          in succT (blockNode (S n) Nothing tb env noProps (YS (endPos p2 prf3) st.evs) r3 (r @{p3})) @{p3}
  955 |                       else Succ0 (YS p2 (emptyScalar p2 st.evs)) (x :: xs) @{trans w (uncons Same)}
  956 |                   SR _ _ _ => Succ0 (YS p2 (emptyScalar p2 st.evs)) (x :: xs) @{trans w (uncons Same)}
  957 |                 else
  958 |                   let 0 pw := trans w (uncons Same)
  959 |                    in succT (blockNode (S n) Nothing tbw env noProps (YS p2 st.evs) (x :: xs) (r @{pw})) @{pw}
  960 |      in case keyRes of
  961 |           Fail0 e => Fail0 e
  962 |           Succ0 stK remK @{qK} => case skipToContent remK of
  963 |             SR (L ind LContent tb) rV prfV =>
  964 |               if ind == n && colonBlock rV
  965 |                 then
  966 |                   if tb then custom (oneChar $ endPos stK.pos prfV) TabIndent else
  967 |                   case rV of
  968 |                   ':' :: rV2 =>
  969 |                     let pV   := incCol (endPos stK.pos prfV)
  970 |                         0 pc := trans (uncons Same) (trans prfV qK)
  971 |                      in case afterKey env n True noProps (YS pV stK.evs) rV2 (r @{pc}) of
  972 |                           Fail0 e => Fail0 e
  973 |                           Succ0 stF rF @{qF} => Succ0 stF rF @{trans qF pc}
  974 |                   _ => eoi
  975 |                 else Succ0 ({evs $= emptyScalar stK.pos} stK) remK @{qK}
  976 |             SR _ _ _ => Succ0 ({evs $= emptyScalar stK.pos} stK) remK @{qK}
  977 |   expEntry env n st (x :: _) _ = parseFail (oneChar st.pos) (Expected ["'?'"] (pack [x]))
  978 |   expEntry env n st []       _ = eoi
  979 | 
  980 |   ||| The value of a block mapping entry, after its `:` indicator
  981 |   ||| [spec: c-l-block-map-implicit-value]: an inline value on the same
  982 |   ||| line, a block node on following lines, a sequence at the same
  983 |   ||| indent (the "seq-spaces" exception), or empty. `pr` holds
  984 |   ||| properties already parsed on the indicator's line.
  985 |   afterKey : TagEnv -> (n : Nat) -> (cpt : Bool) -> Props -> Rule False YState
  986 |   afterKey env n cpt pr st cs sa@(SA r) =
  987 |     let IL cnt tbw r2 w := inlineWhite cs
  988 |         p2 := addCol cnt st.pos
  989 |      in case r2 of
  990 |           [] => Succ0 (YS p2 (emptyScalarP pr p2 st.evs)) [] @{w}
  991 |           x :: xs =>
  992 |             if x == '&' || x == '!'
  993 |               then case w of
  994 |                 Same     => case pProps env pr p2 (x :: xs) sa of
  995 |                   Fail0 e => Fail0 e
  996 |                   Succ0 (pr2, p3) r3 @{q3} =>
  997 |                     trans (afterKey env n cpt pr2 (YS p3 st.evs) r3 (r @{q3})) (weaken q3)
  998 |                 Uncons u => case pProps env pr p2 (x :: xs) (r @{uncons u}) of
  999 |                   Fail0 e => Fail0 e
 1000 |                   Succ0 (pr2, p3) r3 @{q3} =>
 1001 |                     let 0 pc := trans q3 (uncons u)
 1002 |                      in trans (afterKey env n cpt pr2 (YS p3 st.evs) r3 (r @{pc})) (weaken pc)
 1003 |             else if isBreak x || x == '#'
 1004 |               then case skipToContent (x :: xs) of
 1005 |                 SR (L ind LContent tb) r3 prf3 =>
 1006 |                   let st3 := YS (endPos p2 prf3) st.evs
 1007 |                    in if ind >= S n && propStart r3 && propsOnlyLine r3
 1008 |                         -- properties on their own line: they may yet
 1009 |                         -- belong to a sequence at the parent's indent
 1010 |                         -- [spec: seq-spaces], so continue in this rule
 1011 |                         then case trans prf3 w of
 1012 |                           Same => case pProps env pr st3.pos r3 sa of
 1013 |                             Fail0 e => Fail0 e
 1014 |                             Succ0 (pr2, p4) r4 @{q4} =>
 1015 |                               trans (afterKey env n cpt pr2 (YS p4 st.evs) r4 (r @{q4})) (weaken q4)
 1016 |                           Uncons u => case pProps env pr st3.pos r3 (r @{uncons u}) of
 1017 |                             Fail0 e => Fail0 e
 1018 |                             Succ0 (pr2, p4) r4 @{q4} =>
 1019 |                               let 0 pc := trans q4 (uncons u)
 1020 |                                in trans (afterKey env n cpt pr2 (YS p4 st.evs) r4 (r @{pc})) (weaken pc)
 1021 |                       else if ind >= S n
 1022 |                         then case trans prf3 w of
 1023 |                           Same     => weaken $ blockNode (S n) Nothing tb env pr st3 r3 sa
 1024 |                           Uncons u =>
 1025 |                             weaken $ trans (blockNode (S n) Nothing tb env pr st3 r3 (r @{uncons u}))
 1026 |                                            (weaken (uncons u))
 1027 |                         else if ind == n && dashNext r3
 1028 |                           then
 1029 |                             let st3s := emit (oneChar st3.pos) (SeqStart False pr.anchor pr.tag) st3
 1030 |                              in case trans prf3 w of
 1031 |                                   Same     => weaken $ seqLoop env n st3s r3 sa
 1032 |                                   Uncons u =>
 1033 |                                     weaken $ trans (seqLoop env n st3s r3 (r @{uncons u}))
 1034 |                                                    (weaken (uncons u))
 1035 |                           else Succ0 (YS p2 (emptyScalarP pr p2 st.evs)) (x :: xs) @{w}
 1036 |                 SR _ _ _ => Succ0 (YS p2 (emptyScalarP pr p2 st.evs)) (x :: xs) @{w}
 1037 |               else if cpt
 1038 |                 -- an explicit entry's value: compact collections are
 1039 |                 -- allowed on the same line [spec: s-l+block-indented]
 1040 |                 then case w of
 1041 |                   Same     => weaken $ blockNode (S n) Nothing tbw env pr (YS p2 st.evs) (x :: xs) sa
 1042 |                   Uncons u =>
 1043 |                     weaken $ trans (blockNode (S n) Nothing tbw env pr (YS p2 st.evs) (x :: xs) (r @{uncons u}))
 1044 |                                    (weaken (uncons u))
 1045 |                 else case w of
 1046 |                   Same     => weaken $ inlineVal env n pr (YS p2 st.evs) (x :: xs) sa
 1047 |                   Uncons u =>
 1048 |                     weaken $ trans (inlineVal env n pr (YS p2 st.evs) (x :: xs) (r @{uncons u}))
 1049 |                                    (weaken (uncons u))
 1050 | 
 1051 |   ||| A mapping value on the same line as its `:` indicator: a flow
 1052 |   ||| node or a block scalar [spec: s-l+flow-in-block, s-l+block-scalar].
 1053 |   inlineVal : TagEnv -> (n : Nat) -> Props -> Rule True YState
 1054 |   inlineVal env n pr st [] _ = eoi
 1055 |   inlineVal env n pr st (c :: cs) sa@(SA r) =
 1056 |     if c == '[' || c == '{' || c == '\'' || c == '"' || c == '*'
 1057 |       then case flowNode False (S n) env pr st.pos st (c :: cs) sa of
 1058 |         Fail0 e => Fail0 e
 1059 |         Succ0 st1 r1 @{q1} => case lineEnd False st1.pos r1 of
 1060 |           Fail0 e => Fail0 e
 1061 |           Succ0 p2 r2 @{q2} => Succ0 (YS p2 st1.evs) r2 @{trans q2 q1}
 1062 |       else if c == '|' || c == '>'
 1063 |         then case blockScalar (c == '>') (S n) (c :: cs) of
 1064 |           Succ s rem @{prf} =>
 1065 |             let sty := if c == '>' then Folded else Literal
 1066 |              in let pe := endPos st.pos prf
 1067 |                  in Succ0 (YS pe (st.evs :< bounded (Scalar pr.anchor pr.tag sty s) st.pos pe)) rem
 1068 |           Fail start errEnd err => Fail0 (boundedErr st.pos start errEnd err)
 1069 |       else if isPlainFirst False c cs
 1070 |         then case plainSegment False (c :: cs) of
 1071 |           Succ s rem @{prf} =>
 1072 |             case plainMore False (S n) s (move st.pos prf) rem (r @{prf}) of
 1073 |               Fail0 e => Fail0 e
 1074 |               Succ0 (s2, p2) r2 @{q2} =>
 1075 |                 if colonBlock r2
 1076 |                   then custom (BS st.pos p2) InvalidKey
 1077 |                   else
 1078 |                     Succ0 (YS p2 (st.evs :< bounded (Scalar pr.anchor pr.tag Plain s2) st.pos p2)) r2
 1079 |                       @{trans q2 prf}
 1080 |           Fail start errEnd err => Fail0 (boundedErr st.pos start errEnd err)
 1081 |         else parseFail (oneChar st.pos) (Unknown $ pack [c])
 1082 | 
 1083 | --------------------------------------------------------------------------------
 1084 | --          Documents
 1085 | --------------------------------------------------------------------------------
 1086 | 
 1087 | mutual
 1088 |   ||| The documents of a YAML stream [spec: l-yaml-stream]. `ab` is
 1089 |   ||| true where a document may start without an explicit `---` marker:
 1090 |   ||| at the start of the stream and after a `...` marker.
 1091 |   stream : (ab : Bool) -> TagEnv -> (sawYaml : Bool) -> Rule False YState
 1092 |   stream ab env sy st cs sa@(SA r) = case skipToContent cs of
 1093 |     SR (L _ LEnd _) rem prf =>
 1094 |       if dirty
 1095 |         then parseFail (oneChar $ endPos st.pos prf) (Expected ["'---'"] "end of input")
 1096 |         else Succ0 ({pos := endPos st.pos prf} st) rem @{prf}
 1097 |     SR (L _ LDocEnd _) rem prf =>
 1098 |       -- a document end marker without an open document is consumed
 1099 |       -- silently, but pending directives require a document
 1100 |       -- [spec: l-yaml-stream]
 1101 |       if dirty
 1102 |         then parseFail (oneChar $ endPos st.pos prf) (Expected ["'---'"] "'...'")
 1103 |         else
 1104 |           let st1 := YS (endPos st.pos prf) st.evs
 1105 |            in case prf of
 1106 |                 Same     => weaken $ docSuffix False st1 cs sa
 1107 |                 Uncons u =>
 1108 |                   weaken $ trans (docSuffix False st1 rem (r @{uncons u})) (weaken (uncons u))
 1109 |     SR (L _ LDocStart _) rem prf =>
 1110 |       let pM  := endPos st.pos prf
 1111 |           st1 := emit (BS pM (addCol 3 pM)) (DocStart True) ({pos := pM} st)
 1112 |        in case prf of
 1113 |             Same     => weaken $ docStart env st1 cs sa
 1114 |             Uncons u =>
 1115 |               weaken $ trans (docStart env st1 rem (r @{uncons u})) (weaken (uncons u))
 1116 |     SR (L ind LContent tb) rem prf =>
 1117 |       let pC  := endPos st.pos prf
 1118 |           st1 := {pos := pC} st
 1119 |        in if bomStart rem && ind == 0
 1120 |             then case prf of
 1121 |               Same     => weaken $ bomDoc ab env sy st1 cs sa
 1122 |               Uncons u =>
 1123 |                 weaken $ trans (bomDoc ab env sy st1 rem (r @{uncons u})) (weaken (uncons u))
 1124 |           else if dirStart rem && ind == 0
 1125 |             then
 1126 |               if ab || dirty
 1127 |                 then case prf of
 1128 |                   Same     => weaken $ dirDoc ab env sy st1 cs sa
 1129 |                   Uncons u =>
 1130 |                     weaken $ trans (dirDoc ab env sy st1 rem (r @{uncons u})) (weaken (uncons u))
 1131 |                 else custom (oneChar pC) TrailingContent
 1132 |           else if ab && not dirty
 1133 |             then
 1134 |               let st2 := emit (oneChar st1.pos) (DocStart False) st1
 1135 |                in case prf of
 1136 |                     Same     => weaken $ bareDoc tb env st2 cs sa
 1137 |                     Uncons u =>
 1138 |                       weaken $ trans (bareDoc tb env st2 rem (r @{uncons u})) (weaken (uncons u))
 1139 |             else custom (oneChar pC) TrailingContent
 1140 | 
 1141 |     where
 1142 |       dirty : Bool
 1143 |       dirty = sy || not (null env.handles)
 1144 | 
 1145 |       bomStart : List Char -> Bool
 1146 |       bomStart ('\xfeff' :: _) = True
 1147 |       bomStart _               = False
 1148 | 
 1149 |       dirStart : List Char -> Bool
 1150 |       dirStart ('%' :: _) = True
 1151 |       dirStart _          = False
 1152 | 
 1153 |   ||| A byte order mark before a document [spec: l-document-prefix].
 1154 |   bomDoc : (ab : Bool) -> TagEnv -> (sawYaml : Bool) -> Rule True YState
 1155 |   bomDoc ab env sy st ('\xfeff' :: t) (SA r) =
 1156 |     succT (stream ab env sy ({pos $= incCol} st) t (r @{uncons Same})) @{uncons Same}
 1157 |   bomDoc _ _ _ st _ _ = eoi
 1158 | 
 1159 |   ||| A directive line before a document [spec: l-directive].
 1160 |   dirDoc : (ab : Bool) -> TagEnv -> (sawYaml : Bool) -> Rule True YState
 1161 |   dirDoc ab env sy st cs (SA r) = case dirLine cs of
 1162 |     Succ ln rem @{prf} =>
 1163 |       let pos2 := endPos st.pos prf
 1164 |        in case parseDirective env sy ln of
 1165 |             Left e             => custom (BS st.pos pos2) e
 1166 |             Right (env2, sy2)  =>
 1167 |               succT (stream ab env2 sy2 (YS pos2 st.evs) rem (r @{prf})) @{prf}
 1168 |     Fail start errEnd err => Fail0 (boundedErr st.pos start errEnd err)
 1169 | 
 1170 |   ||| An explicit document, at its `---` marker (the DocStart event has
 1171 |   ||| already been emitted).
 1172 |   docStart : TagEnv -> Rule True YState
 1173 |   docStart env st ('-' :: '-' :: '-' :: t) (SA r) =
 1174 |     let IL cnt tbw r2 w := inlineWhite t
 1175 |         p2 := addCol cnt (addCol 3 st.pos)
 1176 |      in case r2 of
 1177 |           [] =>
 1178 |             -- an empty document at the very end of the input: docTail
 1179 |             -- still emits its DocEnd
 1180 |             let 0 p3 := trans w (uncons $ uncons $ uncons Same)
 1181 |              in trans (docTail (YS p2 (emptyScalar p2 st.evs)) [] (r @{p3})) p3
 1182 |           x :: xs =>
 1183 |             if isBreak x || x == '#'
 1184 |               then case skipToContent (x :: xs) of
 1185 |                 SR (L ind LContent tb) r3 prf3 =>
 1186 |                   let 0 pc := trans prf3 (trans w (uncons $ uncons $ uncons Same))
 1187 |                    in case blockNode 0 Nothing tb env noProps (YS (endPos p2 prf3) st.evs) r3 (r @{pc}) of
 1188 |                         Fail0 e => Fail0 e
 1189 |                         Succ0 st4 r4 @{q4} =>
 1190 |                           let 0 p4 := trans q4 pc
 1191 |                            in trans (docTail st4 r4 (r @{p4})) p4
 1192 |                 SR _ _ _ =>
 1193 |                   -- an empty document; docTail handles what follows
 1194 |                   let 0 p3 := trans w (uncons $ uncons $ uncons Same)
 1195 |                    in trans (docTail (YS p2 (emptyScalar p2 st.evs)) (x :: xs) (r @{p3})) p3
 1196 |               else
 1197 |                 let 0 p3 := trans w (uncons $ uncons $ uncons Same)
 1198 |                  in case blockNode 0 (Just 0) tbw env noProps (YS p2 st.evs) (x :: xs) (r @{p3}) of
 1199 |                       Fail0 e => Fail0 e
 1200 |                       Succ0 st4 r4 @{q4} =>
 1201 |                         let 0 p4 := trans q4 p3
 1202 |                          in trans (docTail st4 r4 (r @{p4})) p4
 1203 |   docStart env st _ _ = eoi
 1204 | 
 1205 |   ||| A document starting without a `---` marker (the DocStart event
 1206 |   ||| has already been emitted).
 1207 |   bareDoc : (tabSep : Bool) -> TagEnv -> Rule True YState
 1208 |   bareDoc tabSep env st cs sa@(SA r) = case blockNode 0 Nothing tabSep env noProps st cs sa of
 1209 |     Fail0 e => Fail0 e
 1210 |     Succ0 st1 r1 @{q1} => trans (docTail st1 r1 (r @{q1})) q1
 1211 | 
 1212 |   ||| After a document's root node: an explicit `...` end, the start of
 1213 |   ||| the next document, the end of the stream, or an error.
 1214 |   docTail : Rule False YState
 1215 |   docTail st cs sa@(SA r) = case skipToContent cs of
 1216 |     SR (L _ LEnd _) rem prf =>
 1217 |       Succ0 (YS (endPos st.pos prf) (st.evs :< oneChar (DocEnd False) st.pos)) rem @{prf}
 1218 |     SR (L _ LDocStart _) rem prf =>
 1219 |       let st1 := emit (oneChar st.pos) (DocEnd False) ({pos := endPos st.pos prf} st)
 1220 |        in case prf of
 1221 |             Same     => stream False defaultEnv False st1 cs sa
 1222 |             Uncons u =>
 1223 |               trans (stream False defaultEnv False st1 rem (r @{uncons u})) (weaken (uncons u))
 1224 |     SR (L _ LDocEnd _) rem prf =>
 1225 |       let st1 := YS (endPos st.pos prf) st.evs
 1226 |        in case prf of
 1227 |             Same     => weaken $ docSuffix True st1 cs sa
 1228 |             Uncons u =>
 1229 |               weaken $ trans (docSuffix True st1 rem (r @{uncons u})) (weaken (uncons u))
 1230 |     SR (L _ LContent tb) rem prf =>
 1231 |       custom (oneChar $ endPos st.pos prf) TrailingContent
 1232 | 
 1233 |   ||| A `...` document end marker [spec: l-document-suffix]. The DocEnd
 1234 |   ||| event is only emitted when the marker closes an open document.
 1235 |   docSuffix : (emitEnd : Bool) -> Rule True YState
 1236 |   docSuffix emitEnd st ('.' :: '.' :: '.' :: t) (SA r) =
 1237 |     let evs1 := if emitEnd then st.evs :< bounded (DocEnd True) st.pos (addCol 3 st.pos) else st.evs
 1238 |         st1  := YS (addCol 3 st.pos) evs1
 1239 |      in case lineEnd False st1.pos t of
 1240 |           Fail0 e => Fail0 e
 1241 |           Succ0 p2 r2 @{q2} =>
 1242 |             let 0 pp := trans q2 (uncons $ uncons $ uncons Same)
 1243 |              in succT (stream True defaultEnv False (YS p2 st1.evs) r2 (r @{pp})) @{pp}
 1244 |   docSuffix _ st _ _ = eoi
 1245 | 
 1246 | --------------------------------------------------------------------------------
 1247 | --          Entry Point
 1248 | --------------------------------------------------------------------------------
 1249 | 
 1250 | ||| Line break normalization [spec 5.4]: CRLF and lone CR become LF.
 1251 | normalize : List Char -> List Char
 1252 | normalize ('\r' :: '\n' :: cs) = '\n' :: normalize cs
 1253 | normalize ('\r' :: cs)         = '\n' :: normalize cs
 1254 | normalize (c :: cs)            = c    :: normalize cs
 1255 | normalize []                   = []
 1256 | 
 1257 | ||| The text a stream's positions refer to: the input with line breaks
 1258 | ||| normalized [spec 5.4]. Render error excerpts against this.
 1259 | export
 1260 | normalized : String -> String
 1261 | normalized = pack . normalize . unpack
 1262 | 
 1263 | ||| Parses a complete YAML stream into its sequence of events, each
 1264 | ||| paired with the source bounds it was parsed from.
 1265 | export
 1266 | parseEvents : Origin -> String -> Either (ParseError YErr) (List (Bounded Event))
 1267 | parseEvents o str =
 1268 |   let ns := normalized str
 1269 |    in case stream True defaultEnv False (YS begin [<oneChar StreamStart begin]) (unpack ns) suffixAcc of
 1270 |         Succ0 st _ => Right (st.evs <>> [oneChar StreamEnd st.pos])
 1271 |         Fail0 err  => Left (toParseError o ns err)
 1272 |