-
Notifications
You must be signed in to change notification settings - Fork 5
/
Yaml.idr
150 lines (122 loc) · 5.21 KB
/
Yaml.idr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
module Yaml
import public Control.Monad.Identity
import public Lightyear
import public Lightyear.Char
import public Lightyear.Strings
import public Data.SortedMap
%access public export
data YamlValue = YamlString String
| YamlNumber Double
| YamlBool Bool
| YamlNull
| YamlObject (SortedMap String YamlValue)
| YamlArray (List YamlValue) -- TODO: YamlObject
implementation Show YamlValue where
show (YamlString s) = show s
show (YamlNumber x) = show x
show (YamlBool True ) = "true"
show (YamlBool False) = "false"
show YamlNull = "null"
show (YamlObject xs) =
"{" ++ intercalate ", " (map fmtItem $ SortedMap.toList xs) ++ "}"
where
intercalate : String -> List String -> String
intercalate sep [] = ""
intercalate sep [x] = x
intercalate sep (x :: xs) = x ++ sep ++ intercalate sep xs
fmtItem (k, v) = k ++ ": " ++ show v
show (YamlArray xs) = show xs
hex : Parser Int
hex = do
c <- map (ord . toUpper) $ satisfy isHexDigit
pure $ if c >= ord '0' && c <= ord '9' then c - ord '0'
else 10 + c - ord 'A'
hexQuad : Parser Int
hexQuad = do a <- hex
b <- hex
c <- hex
d <- hex
pure $ a * 4096 + b * 256 + c * 16 + d
specialChar : Parser Char
specialChar = do
c <- satisfy (const True)
case c of
'"' => pure '"'
'\\' => pure '\\'
'/' => pure '/'
'b' => pure '\b'
'f' => pure '\f'
'n' => pure '\n'
'r' => pure '\r'
't' => pure '\t'
'u' => map chr hexQuad
_ => fail "expected special char"
yamlString' : Parser (List Char)
yamlString' = (char '"' *!> pure Prelude.List.Nil) <|> do
c <- satisfy (/= '"')
if (c == '\\') then map (::) specialChar <*> yamlString'
else map (c ::) yamlString'
yamlString : Parser String
yamlString = char '"' *> map pack yamlString' <?> "Yaml string"
-- inspired by Haskell's Data.Scientific module
record Scientific where
constructor MkScientific
coefficient : Integer
exponent : Integer
scientificToDouble : Scientific -> Double
scientificToDouble (MkScientific c e) = fromInteger c * exp
where exp = if e < 0 then 1 / pow 10 (fromIntegerNat (- e))
else pow 10 (fromIntegerNat e)
parseScientific : Parser Scientific
parseScientific = do sign <- maybe 1 (const (-1)) `map` opt (char '-')
digits <- some digit
hasComma <- isJust `map` opt (char '.')
decimals <- if hasComma then some digit else pure Prelude.List.Nil
hasExponent <- isJust `map` opt (char 'e')
exponent <- if hasExponent then integer else pure 0
pure $ MkScientific (sign * fromDigits (digits ++ decimals))
(exponent - cast (length decimals))
where fromDigits : List (Fin 10) -> Integer
fromDigits = foldl (\a, b => 10 * a + cast b) 0
yamlNumber : Parser Double
yamlNumber = map scientificToDouble parseScientific
yamlBool : Parser Bool
yamlBool = (char 't' >! string "rue" *> pure True)
<|> (char 'f' >! string "alse" *> pure False) <?> "Yaml Bool"
yamlNull : Parser ()
yamlNull = (char 'n' >! string "ull" >! pure ()) <?> "Yaml Null"
||| A parser that skips whitespace without jumping over lines
yamlSpace : Monad m => ParserT String m ()
yamlSpace = skip (many $ satisfy (\c => c /= '\n' && isSpace c)) <?> "yamlSpace"
mutual
yamlArray : Parser (List YamlValue)
yamlArray = char '-' *!> (yamlArrayValue `sepBy` (char '-'))
keyValuePair : Parser (String, YamlValue)
keyValuePair = do key <- map pack (many (satisfy $ not . isSpace)) <* space
val <- char ':' *> yamlValue
pure (key, val)
yamlObject : Parser (SortedMap String YamlValue)
yamlObject = map fromList $ keyValuePair `sepBy` (char '\n') --(pure '\n')
-- TODO check id indent is bigger than in array start
yamlObjectA : Parser (SortedMap String YamlValue)
yamlObjectA = map fromList $ keyValuePair `sepBy` (char '\n') --(pure '\n')
yamlValue' : Parser YamlValue
yamlValue' = (map YamlString yamlString)
<|> (map YamlNumber yamlNumber)
<|> (map YamlBool yamlBool)
<|> (pure YamlNull <* yamlNull)
<|>| map YamlArray yamlArray
<|>| map YamlObject yamlObject
yamlValueA' : Parser YamlValue
yamlValueA' = (map YamlString yamlString)
<|> (map YamlNumber yamlNumber)
<|> (map YamlBool yamlBool)
<|> (pure YamlNull <* yamlNull)
<|>| map YamlArray yamlArray
<|>| map YamlObject yamlObjectA
yamlArrayValue : Parser YamlValue
yamlArrayValue = spaces *> yamlValueA' <* spaces
yamlValue : Parser YamlValue
yamlValue = yamlSpace *> yamlValue' <* yamlSpace
yamlToplevelValue : Parser YamlValue
yamlToplevelValue = (map YamlArray yamlArray) <|> (map YamlObject yamlObject)