
   0 | module Text.YAML.Node
   1 | 
   2 | import Data.String
   3 | import Derive.Prelude
   4 | import Text.YAML.Types
   5 | 
   6 | %default total
   7 | %language ElabReflection
   8 | 
   9 | --------------------------------------------------------------------------------
  10 | --          Specific Tags
  11 | --------------------------------------------------------------------------------
  12 | 
  13 | ||| A node's specific tag after schema resolution [spec chapter 10].
  14 | |||
  15 | ||| The tags of the core schema get their own constructors for cheap
  16 | ||| matching; anything else (`tag:yaml.org,2002:set`, local `!foo`
  17 | ||| tags, ...) is `TOther`.
  18 | public export
  19 | data STag : Type where
  20 |   TNull  : STag
  21 |   TBool  : STag
  22 |   TInt   : STag
  23 |   TFloat : STag
  24 |   TStr   : STag
  25 |   TSeq   : STag
  26 |   TMap   : STag
  27 |   TOther : String -> STag
  28 | 
  29 | %runElab derive "STag" [Show,Eq]
  30 | 
  31 | ||| The URI form of a specific tag, e.g. `tag:yaml.org,2002:int`.
  32 | public export
  33 | tagURI : STag -> String
  34 | tagURI TNull      = "tag:yaml.org,2002:null"
  35 | tagURI TBool      = "tag:yaml.org,2002:bool"
  36 | tagURI TInt       = "tag:yaml.org,2002:int"
  37 | tagURI TFloat     = "tag:yaml.org,2002:float"
  38 | tagURI TStr       = "tag:yaml.org,2002:str"
  39 | tagURI TSeq       = "tag:yaml.org,2002:seq"
  40 | tagURI TMap       = "tag:yaml.org,2002:map"
  41 | tagURI (TOther s) = s
  42 | 
  43 | ||| Inverse of `tagURI`: maps the core schema URIs to their
  44 | ||| constructors, anything else to `TOther`.
  45 | public export
  46 | fromURI : String -> STag
  47 | fromURI "tag:yaml.org,2002:null"  = TNull
  48 | fromURI "tag:yaml.org,2002:bool"  = TBool
  49 | fromURI "tag:yaml.org,2002:int"   = TInt
  50 | fromURI "tag:yaml.org,2002:float" = TFloat
  51 | fromURI "tag:yaml.org,2002:str"   = TStr
  52 | fromURI "tag:yaml.org,2002:seq"   = TSeq
  53 | fromURI "tag:yaml.org,2002:map"   = TMap
  54 | fromURI s                         = TOther s
  55 | 
  56 | --------------------------------------------------------------------------------
  57 | --          Nodes
  58 | --------------------------------------------------------------------------------
  59 | 
  60 | ||| A composed YAML node: the output of the composer, with aliases
  61 | ||| substituted and tags resolved.
  62 | |||
  63 | ||| Scalars keep their raw text (interpreted on demand by the views
  64 | ||| below) together with their presentation style.
  65 | public export
  66 | data Node : Type where
  67 |   NScalar : (tag : STag) -> (style : Style) -> (text : String) -> Node
  68 |   NSeq    : (tag : STag) -> List Node -> Node
  69 |   NMap    : (tag : STag) -> List (Node, Node) -> Node
  70 | 
  71 | scText : SnocList String -> String -> SnocList String
  72 | scText ss s = ss :< show s
  73 | 
  74 | mutual
  75 |   showNode : SnocList String -> Node -> SnocList String
  76 |   showNode ss (NScalar _ _ s)       = scText ss s
  77 |   showNode ss (NSeq _ [])           = ss :< "[]"
  78 |   showNode ss (NSeq _ (n :: ns))    = showNodes (showNode (ss :< "[") n) ns
  79 |   showNode ss (NMap _ [])           = ss :< "{}"
  80 |   showNode ss (NMap _ (p :: ps))    = showPairs (showPair (ss :< "{") p) ps
  81 | 
  82 |   showPair : SnocList String -> (Node, Node) -> SnocList String
  83 |   showPair ss (k, v) = showNode (showNode ss k :< ": ") v
  84 | 
  85 |   showNodes : SnocList String -> List Node -> SnocList String
  86 |   showNodes ss []        = ss :< "]"
  87 |   showNodes ss (n :: ns) = showNodes (showNode (ss :< ", ") n) ns
  88 | 
  89 |   showPairs : SnocList String -> List (Node, Node) -> SnocList String
  90 |   showPairs ss []        = ss :< "}"
  91 |   showPairs ss (p :: ps) = showPairs (showPair (ss :< ", ") p) ps
  92 | 
  93 | ||| Renders a node in compact flow style, with all scalars quoted.
  94 | export
  95 | canon : Node -> String
  96 | canon n = fastConcat (showNode [<] n <>> [])
  97 | 
  98 | export %inline
  99 | Show Node where
 100 |   show = canon
 101 | 
 102 | --------------------------------------------------------------------------------
 103 | --          Schemas and Scalar Resolution
 104 | --------------------------------------------------------------------------------
 105 | 
 106 | ||| The schema used to resolve the tags of untagged nodes
 107 | ||| [spec chapter 10].
 108 | public export
 109 | data Schema : Type where
 110 |   ||| Untagged scalars and collections become str/seq/map.
 111 |   Failsafe : Schema
 112 | 
 113 |   ||| Untagged plain scalars additionally resolve to null, bool, int
 114 |   ||| and float by their form. The recommended default.
 115 |   Core     : Schema
 116 | 
 117 | %runElab derive "Schema" [Show,Eq]
 118 | 
 119 | -- non-empty and all characters match
 120 | all1 : (Char -> Bool) -> List Char -> Bool
 121 | all1 f [] = False
 122 | all1 f cs = all f cs
 123 | 
 124 | -- [-+]?[0-9]+ | 0o[0-7]+ | 0x[0-9a-fA-F]+
 125 | isIntCs : List Char -> Bool
 126 | isIntCs ('0' :: 'x' :: cs) = all1 isHexDigit cs
 127 | isIntCs ('0' :: 'o' :: cs) = all1 isOctDigit cs
 128 | isIntCs ('+' :: cs)        = all1 isDigit cs
 129 | isIntCs ('-' :: cs)        = all1 isDigit cs
 130 | isIntCs cs                 = all1 isDigit cs
 131 | 
 132 | -- [eE][-+]?[0-9]+ or nothing
 133 | expPart : List Char -> Bool
 134 | expPart []                = True
 135 | expPart (e :: '+' :: cs)  = (e == 'e' || e == 'E') && all1 isDigit cs
 136 | expPart (e :: '-' :: cs)  = (e == 'e' || e == 'E') && all1 isDigit cs
 137 | expPart (e :: cs)         = (e == 'e' || e == 'E') && all1 isDigit cs
 138 | 
 139 | -- \.[0-9]+ | [0-9]+(\.[0-9]*)? , returning the rest for `expPart`
 140 | mantissa : List Char -> Maybe (List Char)
 141 | mantissa ('.' :: cs) = case span isDigit cs of
 142 |   ([], _) => Nothing
 143 |   (_, r)  => Just r
 144 | mantissa cs = case span isDigit cs of
 145 |   ([], _)        => Nothing
 146 |   (_, '.' :: r)  => Just (snd $ span isDigit r)
 147 |   (_, r)         => Just r
 148 | 
 149 | -- [-+]? mantissa expPart
 150 | isFloatCs : List Char -> Bool
 151 | isFloatCs ('+' :: cs) = maybe False expPart (mantissa cs)
 152 | isFloatCs ('-' :: cs) = maybe False expPart (mantissa cs)
 153 | isFloatCs cs          = maybe False expPart (mantissa cs)
 154 | 
 155 | nullWords, boolWords, infWords, nanWords : List String
 156 | trueWords, falseWords, posInfWords, negInfWords : List String
 157 | trueWords   = ["true", "True", "TRUE"]
 158 | falseWords  = ["false", "False", "FALSE"]
 159 | posInfWords = ["+.inf", ".inf", "+.Inf", ".Inf", "+.INF", ".INF"]
 160 | negInfWords = ["-.inf", "-.Inf", "-.INF"]
 161 | nullWords = ["", "~", "null", "Null", "NULL"]
 162 | boolWords = ["true", "True", "TRUE", "false", "False", "FALSE"]
 163 | infWords  =
 164 |   [ ".inf", "+.inf", "-.inf", ".Inf", "+.Inf", "-.Inf"
 165 |   , ".INF", "+.INF", "-.INF"
 166 |   ]
 167 | nanWords  = [".nan", ".NaN", ".NAN"]
 168 | 
 169 | ||| The specific tag of an untagged plain scalar under the core schema
 170 | ||| [spec 10.3.2].
 171 | export
 172 | resolvePlain : String -> STag
 173 | resolvePlain s =
 174 |   if s `elem` nullWords then TNull
 175 |   else if s `elem` boolWords then TBool
 176 |   else if (s `elem` infWords) || (s `elem` nanWords) then TFloat
 177 |   else
 178 |     let cs := unpack s
 179 |      in if isIntCs cs then TInt
 180 |         else if isFloatCs cs then TFloat
 181 |         else TStr
 182 | 
 183 | ||| The specific tag of a scalar node. Explicitly tagged scalars keep
 184 | ||| their tag without validation: a `!!int abc` node composes fine, and
 185 | ||| the typed views below surface the mismatch on access.
 186 | export
 187 | scalarTag : Schema -> Tag -> Style -> String -> STag
 188 | scalarTag _    (Verbatim t) _     _ = fromURI t
 189 | scalarTag _    NonSpec      _     _ = TStr
 190 | scalarTag Core NoTag        Plain s = resolvePlain s
 191 | scalarTag _    NoTag        _     _ = TStr
 192 | 
 193 | ||| The specific tag of a collection node, given its default
 194 | ||| (`TSeq` or `TMap`).
 195 | export
 196 | collTag : Schema -> Tag -> (dflt : STag) -> STag
 197 | collTag _ (Verbatim t) _    = fromURI t
 198 | collTag _ _            dflt = dflt
 199 | 
 200 | --------------------------------------------------------------------------------
 201 | --          Typed Views
 202 | --------------------------------------------------------------------------------
 203 | 
 204 | public export %inline
 205 | nodeTag : Node -> STag
 206 | nodeTag (NScalar t _ _) = t
 207 | nodeTag (NSeq t _)      = t
 208 | nodeTag (NMap t _)      = t
 209 | 
 210 | public export %inline
 211 | isNull : Node -> Bool
 212 | isNull n = nodeTag n == TNull
 213 | 
 214 | ||| The raw text of any scalar node.
 215 | public export
 216 | asText : Node -> Maybe String
 217 | asText (NScalar _ _ s) = Just s
 218 | asText _               = Nothing
 219 | 
 220 | ||| The text of a str-tagged scalar node.
 221 | public export
 222 | asString : Node -> Maybe String
 223 | asString (NScalar TStr _ s) = Just s
 224 | asString _                  = Nothing
 225 | 
 226 | ||| The value of a bool-tagged scalar node.
 227 | public export
 228 | asBool : Node -> Maybe Bool
 229 | asBool (NScalar TBool _ s) =
 230 |   if s `elem` trueWords then Just True
 231 |   else if s `elem` falseWords then Just False
 232 |   else Nothing
 233 | asBool _ = Nothing
 234 | 
 235 | digits : (base : Integer) -> (Char -> Maybe Integer) -> List Char -> Maybe Integer
 236 | digits base f [] = Nothing
 237 | digits base f cs = go 0 cs
 238 |   where
 239 |     go : Integer -> List Char -> Maybe Integer
 240 |     go acc []        = Just acc
 241 |     go acc (c :: t)  = case f c of
 242 |       Just d  => go (acc * base + d) t
 243 |       Nothing => Nothing
 244 | 
 245 | decDigit, octDigit', hexDigit' : Char -> Maybe Integer
 246 | decDigit c  = if isDigit c then Just (cast (ord c - 0x30)) else Nothing
 247 | octDigit' c = if isOctDigit c then Just (cast (ord c - 0x30)) else Nothing
 248 | hexDigit' c =
 249 |   if isDigit c then Just (cast (ord c - 0x30))
 250 |   else if c >= 'a' && c <= 'f' then Just (cast (ord c - 0x57))
 251 |   else if c >= 'A' && c <= 'F' then Just (cast (ord c - 0x37))
 252 |   else Nothing
 253 | 
 254 | intVal : List Char -> Maybe Integer
 255 | intVal ('0' :: 'x' :: cs) = digits 16 hexDigit' cs
 256 | intVal ('0' :: 'o' :: cs) = digits 8 octDigit' cs
 257 | intVal ('+' :: cs)        = digits 10 decDigit cs
 258 | intVal ('-' :: cs)        = negate <$> digits 10 decDigit cs
 259 | intVal cs                 = digits 10 decDigit cs
 260 | 
 261 | ||| The value of an int-tagged scalar node (decimal with optional
 262 | ||| sign, `0x` hexadecimal or `0o` octal).
 263 | public export
 264 | asInteger : Node -> Maybe Integer
 265 | asInteger (NScalar TInt _ s) = intVal (unpack s)
 266 | asInteger _                  = Nothing
 267 | 
 268 | -- Decomposes a core schema float (sign already stripped) into its
 269 | -- integer digits, fraction digits and exponent value: at least one
 270 | -- mantissa digit, an optional fraction and an optional exponent.
 271 | floatParts : List Char -> Maybe (List Char, List Char, Integer)
 272 | floatParts cs =
 273 |   let (ip, r1) := span isDigit cs
 274 |       (fp, r2) := case r1 of
 275 |                     '.' :: t => span isDigit t
 276 |                     _        => ([], r1)
 277 |    in case (ip, fp) of
 278 |         ([], []) => Nothing
 279 |         _        => (\e => (ip, fp, e)) <$> expVal r2
 280 | 
 281 |   where
 282 |     expVal : List Char -> Maybe Integer
 283 |     expVal []       = Just 0
 284 |     expVal (e :: r) =
 285 |       if e == 'e' || e == 'E'
 286 |         then case r of
 287 |           '+' :: ds => digits 10 decDigit ds
 288 |           '-' :: ds => negate <$> digits 10 decDigit ds
 289 |           ds        => digits 10 decDigit ds
 290 |         else Nothing
 291 | 
 292 | -- Rebuilds a float in a form every backend's `cast String Double`
 293 | -- handles (`.5`, `5.` and `1.e3` are valid YAML but not portable
 294 | -- strtod input).
 295 | dblVal : String -> Maybe Double
 296 | dblVal s =
 297 |   if s `elem` posInfWords
 298 |     then Just (1.0 / 0.0)
 299 |   else if s `elem` negInfWords
 300 |     then Just (-1.0 / 0.0)
 301 |   else if s `elem` nanWords
 302 |     then Just (0.0 / 0.0)
 303 |   else case unpack s of
 304 |     '+' :: cs => build "" cs
 305 |     '-' :: cs => build "-" cs
 306 |     cs        => build "" cs
 307 | 
 308 |   where
 309 |     orZero : List Char -> String
 310 |     orZero [] = "0"
 311 |     orZero cs = pack cs
 312 | 
 313 |     build : String -> List Char -> Maybe Double
 314 |     build sign cs =
 315 |       (\(ip, fp, e) => cast "\{sign}\{orZero ip}.\{orZero fp}e\{show e}")
 316 |         <$> floatParts cs
 317 | 
 318 | ||| The numeric value of a float- or int-tagged scalar node.
 319 | public export
 320 | asDouble : Node -> Maybe Double
 321 | asDouble (NScalar TFloat _ s) = dblVal s
 322 | asDouble n@(NScalar TInt _ _) = cast <$> asInteger n
 323 | asDouble _                    = Nothing
 324 | 
 325 | public export
 326 | asSeq : Node -> Maybe (List Node)
 327 | asSeq (NSeq _ ns) = Just ns
 328 | asSeq _           = Nothing
 329 | 
 330 | public export
 331 | asMap : Node -> Maybe (List (Node, Node))
 332 | asMap (NMap _ ps) = Just ps
 333 | asMap _           = Nothing
 334 | 
 335 | ||| The value of the first mapping entry whose key is a scalar with
 336 | ||| the given raw text.
 337 | public export
 338 | lookupKey : String -> Node -> Maybe Node
 339 | lookupKey s (NMap _ ps) = go ps
 340 |   where
 341 |     go : List (Node, Node) -> Maybe Node
 342 |     go []                          = Nothing
 343 |     go ((NScalar _ _ t, v) :: rest) = if t == s then Just v else go rest
 344 |     go (_ :: rest)                  = go rest
 345 | lookupKey _ _ = Nothing
 346 | 
 347 | --------------------------------------------------------------------------------
 348 | --          Node Equality
 349 | --------------------------------------------------------------------------------
 350 | 
 351 | -- The canonical value of a core schema scalar [spec 10.3.2]. Floats
 352 | -- are kept in exact decimal scientific notation rather than as
 353 | -- `Double`: IEEE comparison would break reflexivity (NaN /= NaN) and
 354 | -- collapse out-of-range values (1e400 == 2e400 == +inf).
 355 | data CScalar : Type where
 356 |   CNull : CScalar
 357 |   CBool : Bool -> CScalar
 358 |   CInt  : Integer -> CScalar
 359 |   CZero : CScalar
 360 |   CInf  : (neg : Bool) -> CScalar
 361 |   CNaN  : CScalar
 362 |   -- value = (-1)^neg * d1.d2...dn * 10^exp, where `digits` are
 363 |   -- d1...dn with d1 and dn nonzero [spec: canonical float form]
 364 |   CSci  : (neg : Bool) -> (digits : String) -> (exp : Integer) -> CScalar
 365 | 
 366 | Eq CScalar where
 367 |   CNull       == CNull       = True
 368 |   CBool x     == CBool y     = x == y
 369 |   CInt x      == CInt y      = x == y
 370 |   CZero       == CZero       = True
 371 |   CInf x      == CInf y      = x == y
 372 |   CNaN        == CNaN        = True
 373 |   CSci n d e  == CSci m f g  = n == m && d == f && e == g
 374 |   _           == _           = False
 375 | 
 376 | canonFloat : String -> Maybe CScalar
 377 | canonFloat s =
 378 |   if s `elem` posInfWords then Just (CInf False)
 379 |   else if s `elem` negInfWords then Just (CInf True)
 380 |   else if s `elem` nanWords then Just CNaN
 381 |   else case unpack s of
 382 |     '+' :: cs => norm False cs
 383 |     '-' :: cs => norm True cs
 384 |     cs        => norm False cs
 385 | 
 386 |   where
 387 |     norm : Bool -> List Char -> Maybe CScalar
 388 |     norm neg cs = do
 389 |       (ip, fp, e) <- floatParts cs
 390 |       let (zs, ds) := span ('0' ==) (ip ++ fp)
 391 |       case reverse (dropWhile ('0' ==) (reverse ds)) of
 392 |         [] => Just CZero
 393 |         ds' =>
 394 |           Just (CSci neg (pack ds') (e + cast (length ip) - cast (length zs) - 1))
 395 | 
 396 | -- The canonical value of a scalar, when its tag defines one for the
 397 | -- given content; `Nothing` requests raw text comparison.
 398 | canonScalar : STag -> String -> Maybe CScalar
 399 | canonScalar TNull  s = if s `elem` nullWords then Just CNull else Nothing
 400 | canonScalar TBool  s =
 401 |   if s `elem` trueWords then Just (CBool True)
 402 |   else if s `elem` falseWords then Just (CBool False)
 403 |   else Nothing
 404 | canonScalar TInt   s = CInt <$> intVal (unpack s)
 405 | canonScalar TFloat s = canonFloat s
 406 | canonScalar _      _ = Nothing
 407 | 
 408 | -- Two canonicalizable contents compare by value; everything else by
 409 | -- raw text. The mixed case can only fall through to inequality:
 410 | -- `canonScalar t` is a function, so equal raw text canonicalizes
 411 | -- identically. This keeps `==` an equivalence relation.
 412 | eqScalar : STag -> String -> String -> Bool
 413 | eqScalar t a b = case (canonScalar t a, canonScalar t b) of
 414 |   (Just x, Just y) => x == y
 415 |   _                => a == b
 416 | 
 417 | mutual
 418 |   eqNode : Node -> Node -> Bool
 419 |   eqNode (NScalar t1 _ s1) (NScalar t2 _ s2) = t1 == t2 && eqScalar t1 s1 s2
 420 |   eqNode (NSeq t1 ns1)     (NSeq t2 ns2)     = t1 == t2 && eqNodes ns1 ns2
 421 |   eqNode (NMap t1 ps1)     (NMap t2 ps2)     = t1 == t2 && eqPairs ps1 ps2
 422 |   eqNode _                 _                 = False
 423 | 
 424 |   eqNodes : List Node -> List Node -> Bool
 425 |   eqNodes []        []        = True
 426 |   eqNodes (x :: xs) (y :: ys) = eqNode x y && eqNodes xs ys
 427 |   eqNodes _         _         = False
 428 | 
 429 |   eqPairs : List (Node, Node) -> List (Node, Node) -> Bool
 430 |   eqPairs []              []              = True
 431 |   eqPairs ((k1,v1) :: xs) ((k2,v2) :: ys) =
 432 |     eqNode k1 k2 && eqNode v1 v2 && eqPairs xs ys
 433 |   eqPairs _               _               = False
 434 | 
 435 | ||| Node equality is tag and content [spec 3.2.1.3]: the presentation
 436 | ||| style does not participate, so the plain key `a` and the quoted key
 437 | ||| `"a"` are equal. Scalar content is compared by canonical value
 438 | ||| where the tag defines one (`1`, `0x1` and `+1` are the same int,
 439 | ||| `10.0` and `1e1` the same float), and as raw text otherwise.
 440 | export %inline
 441 | Eq Node where
 442 |   (==) = eqNode
 443 |