0 | module Text.TOML.Parser

  2 | import Data.SortedMap

  3 | import Data.String

  4 | import Data.Linear.Ref1

  5 | import Text.ILex.Derive

  6 | import Text.ILex

  7 | import Text.TOML.Lexer

  8 | import Text.TOML.Types

  9 | import Text.TOML.Internal.TStack

 10 | import Syntax.T1

 12 | %hide Data.Linear.(.)

 13 | %default total

 14 | %language ElabReflection

 21 | data TStack : Type where

 22 |   STbl : TreeTable -> SnocList Key -> TStack

 23 |   SArr : TreeTable -> SnocList Key -> TStack

 24 |   STop : TView Tree -> SnocList Key -> TreeTable -> TStack

 25 |   VArr : TStack -> SnocList TomlValue -> TStack

 26 |   VTbl : TStack -> SnocList Key -> TreeTable -> TStack

 28 | toRoot : TStack -> TreeTable

 29 | toRoot (STbl t sk)   = t

 30 | toRoot (SArr t sk)   = t

 31 | toRoot (STop v sk t) = reduceT Undef t (tagAsHDef v)

 32 | toRoot (VArr x sv)   = toRoot x

 33 | toRoot (VTbl x sk y) = toRoot x

 35 | toTable : TStack -> Either e TomlTable

 36 | toTable = Right . toTbl . toRoot

 38 | empty : TStack

 39 | empty = STop VR [<] empty

 47 | %runElab deriveParserState "TSz" "TST"

 48 |   [ "TIni", "EKey", "ESep", "EVal", "EOL", "Err", "TSep", "ASep"

 49 |   -- arrays and inline tables (`Val` after value, `Com` after comma)

 50 |   , "ANew", "AVal", "ACom", "TVal", "TCom", "TNew"

 51 |   -- quoted keys and strings

 52 |   , "QKey", "LKey", "QStr", "LStr", "MLQStr", "MLLStr"

 53 |   ]

 55 | public export

 56 | 0 TSTCK : Type -> Type

 57 | TSTCK = Stack TomlParseError TStack TSz

 63 | parameters {auto sk : TSTCK q}

 65 |   addkey : KeyType -> Bounded String -> F1 q TST

 66 |   addkey kt (B s bs) =

 67 |    let k := KT s kt bs

 68 |     in getStack >>= \case

 69 |       STbl x ks   => putStackAs (STbl x $ ks:<k) TSep

 70 |       SArr x ks   => putStackAs (SArr x $ ks:<k) ASep

 71 |       STop x ks t => putStackAs (STop x (ks:<k) t) ESep

 72 |       VTbl x ks t => putStackAs (VTbl x (ks:<k) t) ESep

 73 |       VArr x sv   => putStackAs (VArr x sv) Err

 75 |   onkey : String -> F1 q TST

 76 |   onkey s = T1.do

 77 |     bs <- tokenBounds (length s)

 78 |     addkey Plain (B s bs)

 80 |   escape : TST -> ByteString -> F1 q TST

 81 |   escape res bs =

 82 |    let hex := cast {to = Bits32} $ hexadecimal (drop 2 bs)

 83 |     in case has unicode hex && not (has surrogate hex) of

 84 |          True  => inccol (size bs) >> pushBits32 res hex

 85 |          False => unexpected [] sk >>= flip failWith Err

 87 |   end : TST -> Either TErr TStack -> F1 q TST

 88 |   end x (Left y)  = failWith y Err

 89 |   end x (Right y) = putStackAs y x

 91 |   onval : TomlValue -> TStack -> F1 q TST

 92 |   onval v (STop x sk t) = end EOL  $ STop x [<] <$> addVal t sk v

 93 |   onval v (VArr x sv)   = end AVal $ Right (VArr x (sv:<v))

 94 |   onval v (VTbl x sk t) = end TVal $ VTbl x [<] <$> addVal t sk v

 95 |   onval v s             = end Err (Right s)

 97 |   openStdTable : F1 q TST

 98 |   openStdTable = getStack >>= \s => putStackAs (STbl (toRoot s) [<]) EKey

100 |   openArrayTable : F1 q TST

101 |   openArrayTable = getStack >>= \s => putStackAs (SArr (toRoot s) [<]) EKey

103 |   openArray : F1 q TST

104 |   openArray = getStack >>= \s => putStackAs (VArr s [<]) ANew

106 |   openInlineTable : F1 q TST

107 |   openInlineTable = getStack >>= \s => putStackAs (VTbl s [<] empty) TNew

109 |   close : F1 q TST

110 |   close =

111 |     getStack >>= \case

112 |       STbl t sk =>

113 |         case tview t (sk <>> []) of

114 |           Right (v,t) => putStackAs (STop v [<] t) EOL

115 |           Left  x     => failWith x Err

116 |       SArr t sk =>

117 |         case view VR t (sk <>> []) of

118 |           Right (VT v t k New,t2) => putStackAs (STop (VA v t k [<]) [<] t2) EOL

119 |           Right (VA v t k st,t2)  => putStackAs (STop (VA v t k (st:<t2)) [<] empty) EOL

120 |           Right (v,_)             => failWith (vexists v) Err

121 |           Left  x                 => failWith x Err

122 |       VArr x sx   => onval (TArr $ sx <>> []) x

123 |       VTbl x sk t => onval (TTbl $ toTbl t) x

124 |       s           => end Err (Right s)

126 |   qstr : String -> F1 q TST

127 |   qstr s = getStack >>= onval (TStr s)

130 | val : a -> (ByteString -> TomlValue) -> (a, Step q TSz TSTCK)

131 | val x f = goBS x $ \bs => inccol bs.size >> getStack >>= onval (f bs)

133 | valE : a -> (ByteString -> AnyTime) -> (a, Step q TSz TSTCK)

134 | valE x f =

135 |   goBS x $ \bs => case extraCheckDate (f bs) of

136 |     Right v => inccol bs.size >> getStack >>= onval (TTime v)

137 |     Left  x => raise (Custom $ InvalidLeapDay x) (size bs) Err

140 | val' : a -> TomlValue -> (a, Step q TSz TSTCK)

141 | val' x = val x . const

147 | tomlSpaced : TST -> Steps q TSz TSTCK -> DFA q TSz TSTCK

148 | tomlSpaced res ss = dfa $ conv' (plus wschar) res :: ss

150 | tomlIgnore : TST -> TST -> Steps q TSz TSTCK -> DFA q TSz TSTCK

151 | tomlIgnore res nl ss =

152 |   tomlSpaced res $ [read' comment res, newline' newline nl] ++ ss

154 | keySteps : Steps q TSz TSTCK

155 | keySteps =

156 |   [ goStr unquotedKey onkey

157 |   , copen' '\'' LKey

158 |   , copen' '"'  QKey

159 |   ]

161 | valSteps : Steps q TSz TSTCK

162 | valSteps =

163 |   [ val' "true"  (TBool True)

164 |   , val' "false" (TBool False)

166 |   -- integers

167 |   , val  decInt  (TInt . readDecInt)

168 |   , val  binInt  (TInt . binarySep . drop 2)

169 |   , val  octInt  (TInt . octalSep underscore . drop 2)

170 |   , val  hexInt  (TInt . hexadecimalSep underscore . drop 2)

172 |   -- floats

173 |   , val' nan     (TDbl NaN)

174 |   , val' posInf  (TDbl $ Infty Plus)

175 |   , val' "-inf"  (TDbl $ Infty Minus)

176 |   , val float    (TDbl . readFloat)

178 |   -- Date and Time

179 |   , valE fullDate  (ATLocalDate . readLocalDate)

180 |   , valE (fullDate >> ' ')  (ATLocalDate . readLocalDate . trim)

181 |   , valE localTime (ATLocalTime . readLocalTime)

182 |   , valE localDateTime (ATLocalDateTime . readLocalDateTime)

183 |   , valE offsetDateTime (ATOffsetDateTime . readOffsetDateTime)

185 |   -- Nested Values

186 |   , copen '[' openArray

187 |   , copen '{' openInlineTable

189 |   -- Strings

190 |   , copen' '"'  QStr

191 |   , copen' '\'' LStr

192 |   , copen' #"""""# MLQStr

193 |   , go (#"""""# >> newline) (pushPosition >> incline 1 >> pure MLQStr)

194 |   , copen' "'''" MLLStr

195 |   , go ("'''" >> newline) (pushPosition >> incline 1 >> pure MLLStr)

196 |   , val' #""""# (TStr "")

197 |   , val' #"''"# (TStr "")

198 |   ]

200 | escapes : TST -> Steps q TSz TSTCK

201 | escapes res =

202 |     [ read basicUnescaped (pushStr res)

203 |     , cexpr #"\""# (pushStr res "\"")

204 |     , cexpr #"\\"# (pushStr res "\\")

205 |     , cexpr #"\b"# (pushStr res "\b")

206 |     , cexpr #"\e"# (pushStr res "\e")

207 |     , cexpr #"\f"# (pushStr res "\f")

208 |     , cexpr #"\n"# (pushStr res "\n")

209 |     , cexpr #"\r"# (pushStr res "\r")

210 |     , cexpr #"\t"# (pushStr res "\t")

211 |     , goBS ("\\u" >> repeat 4 hexdigit) (escape res)

212 |     , goBS ("\\U" >> repeat 8 hexdigit) (escape res)

213 |     ]

215 | mlqDFA : DFA q TSz TSTCK

216 | mlqDFA =

217 |   dfa $

218 |     [ ccloseStr #"""""# qstr

219 |     , cclose #""""""# (pushStr' "\"" >> getStr >>= qstr)

220 |     , cclose #"""""""# (pushStr' "\"\"" >> getStr >>= qstr)

221 |     , cexpr #"""# (pushStr MLQStr "\"")

222 |     , cexpr #""""# (pushStr MLQStr "\"\"")

223 |     , newline newline (pushStr MLQStr "\n")

224 |     , multiline' mlbEscapedNL MLQStr

225 |     ] ++ escapes MLQStr

227 | mllDFA : DFA q TSz TSTCK

228 | mllDFA =

229 |   dfa $

230 |     [ ccloseStr "'''" qstr

231 |     , cclose "''''" (pushStr' "'" >> getStr >>= qstr)

232 |     , cclose "'''''" (pushStr' "''" >> getStr >>= qstr)

233 |     , cexpr "'" (pushStr MLLStr "'")

234 |     , cexpr "''" (pushStr MLLStr "''")

235 |     , newline newline (pushStr MLLStr "\n")

236 |     , read literalChars (pushStr MLLStr)

237 |     ]

243 | tomlTrans : Lex1 q TSz TSTCK

244 | tomlTrans =

245 |   lex1

246 |     [ E TIni $ tomlIgnore TIni TIni (keySteps ++ [copen '[' openStdTable, copen "[[" openArrayTable])

247 |     , E ESep $ tomlSpaced ESep [cexpr' '.' EKey, cexpr' '=' EVal]

248 |     , E TSep $ tomlSpaced TSep [cexpr' '.' EKey, cclose ']' close]

249 |     , E ASep $ tomlSpaced ASep [cexpr' '.' EKey, cclose "]]" close]

250 |     , E EKey $ tomlSpaced EKey keySteps

251 |     , E EVal $ tomlSpaced EVal valSteps

252 |     , E ANew $ tomlIgnore ANew ANew (cclose ']' close :: valSteps)

253 |     , E AVal $ tomlIgnore AVal AVal [cclose ']' close, cexpr' ',' ACom]

254 |     , E ACom $ tomlIgnore ACom ACom (cclose ']' close :: valSteps)

255 |     , E QKey $ dfa $ ccloseBoundedStr '"' (addkey Quoted) :: escapes QKey

256 |     , E LKey $ dfa [ccloseBoundedStr '\'' (addkey Plain), read literalChars (pushStr LKey)]

257 |     , E QStr $ dfa $ ccloseStr '"' qstr :: escapes QStr

258 |     , E LStr $ dfa [ccloseStr '\'' qstr, read literalChars (pushStr LStr)]

259 |     , E MLQStr mlqDFA

260 |     , E MLLStr mllDFA

261 |     , E TVal $ tomlSpaced TVal [cexpr' ',' TCom, cclose '}' close]

262 |     , E TNew $ tomlSpaced TNew (cclose '}' close :: keySteps)

263 |     , E TCom $ tomlSpaced TCom keySteps

264 |     , E EOL  $ tomlIgnore EOL TIni []

265 |     ]

267 | tomlErr : Arr32 TSz (TSTCK q -> F1 q TErr)

268 | tomlErr =

269 |   arr32 TSz (unexpected [])

270 |     [ E ANew $ unclosedIfEOI "[" []

271 |     , E AVal $ unclosedIfEOI "[" [",", "]"]

272 |     , E ACom $ unclosedIfEOI "[" []

273 |     , E TVal $ unclosedIfNLorEOI "{" [",", "}"]

274 |     , E TCom $ unclosedIfNLorEOI "{" []

275 |     , E TNew $ unclosedIfNLorEOI "{" []

276 |     , E QStr $ unclosedIfNLorEOI "\"" []

277 |     , E QKey $ unclosedIfNLorEOI "\"" []

278 |     , E LStr $ unclosedIfNLorEOI "'" []

279 |     , E LKey $ unclosedIfNLorEOI "'" []

280 |     , E MLQStr $ unclosedIfEOI "\"\"\"" []

281 |     , E MLLStr $ unclosedIfEOI "'''" []

282 |     , E ESep $ unexpected [".", "="]

283 |     , E TSep $ unclosedIfNLorEOI "[" [".", "]"]

284 |     , E ASep $ unclosedIfNLorEOI "[[" [".", "]]"]

285 |     ]

287 | tomlEOI : TST -> TSTCK q -> F1 q (Either TErr TomlTable)

288 | tomlEOI st sk =

289 |   case st == TIni || st == EOL of

290 |     False => arrFail TSTCK tomlErr st sk

291 |     True  => getStack >>= pure . toTable

293 | public export

294 | toml : P1 q TErr TomlTable

295 | toml = P TIni (init empty) tomlTrans (\x => (Nothing #)) tomlErr tomlEOI