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 -> ByteBounded 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 <- Interfaces.bounds

 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  => 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 = bytes x $ \bs => getStack >>= onval (f bs)

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

134 | valE x f =

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

136 |     Right v => 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 : Steps q TSz TSTCK -> DFA q TSz TSTCK

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

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

151 | tomlIgnore nl ss = tomlSpaced $ [ignore' comment, step' newline nl] ++ ss

153 | keySteps : Steps q TSz TSTCK

154 | keySteps =

155 |   [ string unquotedKey onkey

156 |   , opn' '\'' LKey

157 |   , opn' '"'  QKey

158 |   ]

160 | valSteps : Steps q TSz TSTCK

161 | valSteps =

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

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

165 |   -- integers

166 |   , val  decInt  (TInt . readDecInt)

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

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

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

171 |   -- floats

172 |   , val' nan     (TDbl NaN)

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

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

175 |   , val float    (TDbl . readFloat)

177 |   -- Date and Time

178 |   , valE fullDate  (ATLocalDate . readLocalDate)

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

180 |   , valE localTime (ATLocalTime . readLocalTime)

181 |   , valE localDateTime (ATLocalDateTime . readLocalDateTime)

182 |   , valE offsetDateTime (ATOffsetDateTime . readOffsetDateTime)

184 |   -- Nested Values

185 |   , opn '[' openArray

186 |   , opn '{' openInlineTable

188 |   -- Strings

189 |   , opn' '"'  QStr

190 |   , opn' '\'' LStr

191 |   , opn' #"""""# MLQStr

192 |   , opn' (#"""""# >> newline) MLQStr

193 |   , opn' "'''" MLLStr

194 |   , opn' ("'''" >> newline) MLLStr

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

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

197 |   ]

199 | escapes : TST -> Steps q TSz TSTCK

200 | escapes res =

201 |     [ string (plus basicUnescaped) (pushStr res)

202 |     , step #"\""# (pushStr res "\"")

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

204 |     , step #"\b"# (pushStr res "\b")

205 |     , step #"\e"# (pushStr res "\e")

206 |     , step #"\f"# (pushStr res "\f")

207 |     , step #"\n"# (pushStr res "\n")

208 |     , step #"\r"# (pushStr res "\r")

209 |     , step #"\t"# (pushStr res "\t")

210 |     , bytes ("\\u" >> repeat 4 hexdigit) (escape res)

211 |     , bytes ("\\U" >> repeat 8 hexdigit) (escape res)

212 |     ]

214 | mlqDFA : DFA q TSz TSTCK

215 | mlqDFA =

216 |   dfa $

217 |     [ closeStr #"""""# qstr

218 |     , close #""""""# (pushStr' "\"" >> getStr >>= qstr)

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

220 |     , step #"""# (pushStr MLQStr "\"")

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

222 |     , step newline (pushStr MLQStr "\n")

223 |     , step' mlbEscapedNL MLQStr

224 |     ] ++ escapes MLQStr

226 | mllDFA : DFA q TSz TSTCK

227 | mllDFA =

228 |   dfa $

229 |     [ closeStr "'''" qstr

230 |     , close "''''" (pushStr' "'" >> getStr >>= qstr)

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

232 |     , step "'" (pushStr MLLStr "'")

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

234 |     , step newline (pushStr MLLStr "\n")

235 |     , string literalChars (pushStr MLLStr)

236 |     ]

242 | tomlTrans : Lex1 q TSz TSTCK

243 | tomlTrans =

244 |   lex1

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

246 |     , E ESep $ tomlSpaced [step' '.' EKey, step' '=' EVal]

247 |     , E TSep $ tomlSpaced [step' '.' EKey, close ']' close]

248 |     , E ASep $ tomlSpaced [step' '.' EKey, close "]]" close]

249 |     , E EKey $ tomlSpaced keySteps

250 |     , E EVal $ tomlSpaced valSteps

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

252 |     , E AVal $ tomlIgnore AVal [close ']' close, step' ',' ACom]

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

254 |     , E QKey $ dfa $ closeBoundedStr '"' (addkey Quoted) :: escapes QKey

255 |     , E LKey $ dfa [closeBoundedStr '\'' (addkey Plain), string literalChars (pushStr LKey)]

256 |     , E QStr $ dfa $ closeStr '"' qstr :: escapes QStr

257 |     , E LStr $ dfa [closeStr '\'' qstr, string literalChars (pushStr LStr)]

258 |     , E MLQStr mlqDFA

259 |     , E MLLStr mllDFA

260 |     , E TVal $ tomlSpaced [step' ',' TCom, close '}' close]

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

262 |     , E TCom $ tomlSpaced keySteps

263 |     , E EOL  $ tomlIgnore TIni []

264 |     ]

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

267 | tomlErr =

268 |   arr32 TSz (unexpected [])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

284 |     ]

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

287 | tomlEOI st sk =

288 |   case st == TIni || st == EOL of

289 |     False => arrFail TSTCK tomlErr st sk

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

292 | public export

293 | toml : P1 q TErr TomlTable

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