0 | module Text.YAML.Compose
  1 |
  2 | import Data.List.Suffix
  3 | import Data.List.Suffix.Result0
  4 | import Data.SortedMap
  5 | import Data.SortedSet
  6 | import Text.YAML.Parser
  7 | import public Text.YAML.Node
  8 | import public Text.YAML.Types
  9 |
 10 | %default total
 11 |
 12 | --------------------------------------------------------------------------------
 13 | --          Composing
 14 | --------------------------------------------------------------------------------
 15 |
 16 | 0 Anchors : Type
 17 | Anchors = SortedMap Anchor Node
 18 |
 19 | anchored : Maybe Anchor -> Node -> Anchors -> Anchors
 20 | anchored Nothing  _ as = as
 21 | anchored (Just a) n as = insert a n as
 22 |
 23 | livePlus : Maybe Anchor -> SortedSet Anchor -> SortedSet Anchor
 24 | livePlus Nothing  live = live
 25 | livePlus (Just a) live = insert a live
 26 |
 27 | hasKey : Node -> SnocList (Node, Node) -> Bool
 28 | hasKey k [<]              = False
 29 | hasKey k (ps :< (k2, _))  = k == k2 || hasKey k ps
 30 |
 31 | ||| A composing rule over the remaining events, consuming a strict
 32 | ||| prefix when `b` is `True`. Errors carry the bounds of the events
 33 | ||| they refer to.
 34 | |||
 35 | ||| Totality: unlike the character-level parser, every node consumes at
 36 | ||| least one event, so all rules below are strict and the `SuffixAcc`
 37 | ||| recursion is straightforward.
 38 | 0 CRule : Bool -> Type -> Type
 39 | CRule b a =
 40 |      (es : List (Bounded Event))
 41 |   -> (0 acc : SuffixAcc es)
 42 |   -> Result0 b (Bounded Event) es (BoundedErr YErr) a
 43 |
 44 | -- Anchors become visible once their node is complete: scalars insert
 45 | -- immediately, collections only after their children have composed, so
 46 | -- sibling references (`[&a 1, *a]`) resolve while self references
 47 | -- (`&a [*a]`) fail. The `live` set holds the anchors of enclosing,
 48 | -- still open collections; it flows downward only (lexical scoping) and
 49 | -- serves to distinguish `CyclicAlias` from `UndefinedAlias`.
 50 | mutual
 51 |   ||| A single node: scalar, alias, sequence or mapping. Returns the
 52 |   ||| node together with its full source span.
 53 |   node :
 54 |        Schema
 55 |     -> Anchors
 56 |     -> (live : SortedSet Anchor)
 57 |     -> CRule True (Node, Bounds, Anchors)
 58 |   node sch as live (B (Scalar ma t sty s) bs :: es) _ =
 59 |     let n := NScalar (scalarTag sch t sty s) sty s
 60 |      in Succ0 (n, bs, anchored ma n as) es
 61 |   node sch as live (B (Alias a) bs :: es) _ = case lookup a as of
 62 |     Just n  => Succ0 (n, bs, as) es
 63 |     Nothing =>
 64 |       custom bs $ if contains a live then CyclicAlias a else UndefinedAlias a
 65 |   node sch as live (B (SeqStart _ ma t) bs :: es) (SA r) =
 66 |     case seqItems sch as (livePlus ma live) [<] es (r @{uncons Same}) of
 67 |       Fail0 e => Fail0 e
 68 |       Succ0 (ns, be, as2) rest @{q} =>
 69 |         let n := NSeq (collTag sch t TSeq) ns
 70 |          in Succ0 (n, bs <+> be, anchored ma n as2) rest @{trans q (uncons Same)}
 71 |   node sch as live (B (MapStart _ ma t) bs :: es) (SA r) =
 72 |     case mapItems sch as (livePlus ma live) [<] es (r @{uncons Same}) of
 73 |       Fail0 e => Fail0 e
 74 |       Succ0 (ps, be, as2) rest @{q} =>
 75 |         let n := NMap (collTag sch t TMap) ps
 76 |          in Succ0 (n, bs <+> be, anchored ma n as2) rest @{trans q (uncons Same)}
 77 |   node _ _ _ (B e bs :: _) _ = custom bs (UnexpectedEvent (printEvent e))
 78 |   node _ _ _ []            _ = custom NoBounds UnexpectedEnd
 79 |
 80 |   ||| The remaining entries of a sequence, up to its end event, whose
 81 |   ||| bounds are returned.
 82 |   seqItems :
 83 |        Schema
 84 |     -> Anchors
 85 |     -> SortedSet Anchor
 86 |     -> SnocList Node
 87 |     -> CRule True (List Node, Bounds, Anchors)
 88 |   seqItems sch as live acc (B SeqEnd be :: es) _ = Succ0 (acc <>> [], be, as) es
 89 |   seqItems sch as live acc []                  _ = custom NoBounds UnexpectedEnd
 90 |   seqItems sch as live acc es sa@(SA r)          = case node sch as live es sa of
 91 |     Fail0 e => Fail0 e
 92 |     Succ0 (n, _, as2) rest @{q} =>
 93 |       succT $ seqItems sch as2 live (acc :< n) rest (r @{q})
 94 |
 95 |   ||| The remaining entries of a mapping, up to its end event, whose
 96 |   ||| bounds are returned.
 97 |   mapItems :
 98 |        Schema
 99 |     -> Anchors
100 |     -> SortedSet Anchor
101 |     -> SnocList (Node, Node)
102 |     -> CRule True (List (Node, Node), Bounds, Anchors)
103 |   mapItems sch as live acc (B MapEnd be :: es) _ = Succ0 (acc <>> [], be, as) es
104 |   mapItems sch as live acc []                  _ = custom NoBounds UnexpectedEnd
105 |   mapItems sch as live acc es sa@(SA r)          = case node sch as live es sa of
106 |     Fail0 e => Fail0 e
107 |     Succ0 (k, kbs, as2) rest @{q} =>
108 |       if hasKey k acc
109 |         then custom kbs (DuplicateKey (canon k))
110 |         else case node sch as2 live rest (r @{q}) of
111 |           Fail0 e => Fail0 e
112 |           Succ0 (v, _, as3) rest2 @{q2} =>
113 |             let 0 pp := trans q2 q
114 |              in succT $ mapItems sch as3 live (acc :< (k, v)) rest2 (r @{pp})
115 |
116 | --------------------------------------------------------------------------------
117 | --          Entry Points
118 | --------------------------------------------------------------------------------
119 |
120 | ||| Composes an event stream into one node tree per document: aliases
121 | ||| are substituted by the nodes they reference (sharing structure),
122 | ||| tags of untagged nodes are resolved against the given schema, and
123 | ||| mapping keys are checked for uniqueness. Anchors are scoped to
124 | ||| their document; redefining an anchor shadows the previous node.
125 | |||
126 | ||| Errors carry the source bounds of the events they refer to; pair
127 | ||| them with the (line break normalized) input via `toParseError` for
128 | ||| a rendered excerpt, or use `parseDocsWith`, which does so.
129 | export
130 | composeWith : Schema -> List (Bounded Event) -> Either (BoundedErr YErr) (List Node)
131 | composeWith sch (B StreamStart _ :: es) = go [<] es suffixAcc
132 |   where
133 |     go :
134 |          SnocList Node
135 |       -> (es : List (Bounded Event))
136 |       -> (0 acc : SuffixAcc es)
137 |       -> Either (BoundedErr YErr) (List Node)
138 |     go acc (B StreamEnd _ :: [])          _      = Right (acc <>> [])
139 |     go acc (B StreamEnd _ :: B e bs :: _) _      =
140 |       custom bs (UnexpectedEvent (printEvent e))
141 |     go acc (B (DocStart _) _ :: es2)      (SA r) =
142 |       case node sch empty empty es2 (r @{uncons Same}) of
143 |         Fail0 e => Left e
144 |         Succ0 (n, _, _) (B (DocEnd _) _ :: rest) @{q} =>
145 |           let 0 pp := trans (uncons q) (uncons Same)
146 |            in go (acc :< n) rest (r @{pp})
147 |         Succ0 _ (B e bs :: _) => custom bs (UnexpectedEvent (printEvent e))
148 |         Succ0 _ []            => custom NoBounds UnexpectedEnd
149 |     go acc (B e bs :: _) _ = custom bs (UnexpectedEvent (printEvent e))
150 |     go acc []            _ = custom NoBounds UnexpectedEnd
151 | composeWith _ (B e bs :: _) = custom bs (UnexpectedEvent (printEvent e))
152 | composeWith _ []            = custom NoBounds UnexpectedEnd
153 |
154 | ||| `composeWith` under the core schema.
155 | export %inline
156 | compose : List (Bounded Event) -> Either (BoundedErr YErr) (List Node)
157 | compose = composeWith Core
158 |
159 | ||| Parses and composes a YAML stream into one node tree per document.
160 | export
161 | parseDocsWith : Schema -> Origin -> String -> Either (ParseError YErr) (List Node)
162 | parseDocsWith sch o s =
163 |   case parseEvents o s of
164 |     Left e   => Left e
165 |     Right es => case composeWith sch es of
166 |       Left e   => Left (toParseError o (normalized s) e)
167 |       Right ns => Right ns
168 |
169 | ||| `parseDocsWith` under the core schema.
170 | export %inline
171 | parseDocs : Origin -> String -> Either (ParseError YErr) (List Node)
172 | parseDocs = parseDocsWith Core
173 |