0 | module Text.TOML.Parser

  2 | import Data.SortedMap

  3 | import Data.String

  4 | import Data.Linear.Ref1

  5 | import Text.ILex

  6 | import Text.ILex.State.Derive

  7 | import Text.ILex.State.Regular

  8 | import Text.TOML.Lexer

  9 | import Text.TOML.Types

 10 | import Text.TOML.Internal.TStack

 11 | import Syntax.T1

 13 | %hide Data.Linear.(.)

 14 | %hide Data.Linear.Ref1.ST

 15 | %default total

 16 | %language ElabReflection

 23 | data TStack : Type where

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

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

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

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

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

 30 | toRoot : TStack -> TreeTable

 31 | toRoot (STbl t sk)   = t

 32 | toRoot (SArr t sk)   = t

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

 34 | toRoot (VArr x sv)   = toRoot x

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

 37 | toTable : TStack -> Either e TomlTable

 38 | toTable = Right . toTbl . toRoot

 40 | empty : TStack

 41 | empty = STop VR [<] empty

 49 | %runElab deriveParserState "TSz" "TST"

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

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

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

 53 |   -- quoted keys and strings

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

 55 |   ]

 57 | public export

 58 | 0 ST : Type -> Type

 59 | ST = State TomlParseError TStack TSz

 65 | parameters {auto sk : ST q}

 67 |   addkey : KeyType -> ByteBounded String -> F1 q TST

 68 |   addkey kt (B s bs) =

 69 |    let k := KT s kt bs

 70 |     in getStack >>= \case

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

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

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

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

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

 77 |   onkey : String -> F1 q TST

 78 |   onkey s = T1.do

 79 |     bs <- Interfaces.bounds

 80 |     addkey Plain (B s bs)

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

 83 |   escape res bs =

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

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

 86 |          True  => pushBits32 res hex

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

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

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

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

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

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

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

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

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

 99 |   openStdTable : F1 q TST

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

102 |   openArrayTable : F1 q TST

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

105 |   openArray : F1 q TST

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

108 |   openInlineTable : F1 q TST

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

111 |   close : F1 q TST

112 |   close =

113 |     getStack >>= \case

114 |       STbl t sk =>

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

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

117 |           Left  x     => failWith x Err

118 |       SArr t sk =>

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

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

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

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

123 |           Left  x                 => failWith x Err

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

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

126 |       s           => end Err (Right s)

128 |   qstr : String -> F1 q TST

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

132 | val : a -> (ByteString -> TomlValue) -> (a, Step q TSz ST)

133 | val x f = bytes x $ \bs => getStack >>= onval (f bs)

135 | valE : a -> (ByteString -> AnyTime) -> (a, Step q TSz ST)

136 | valE x f =

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

138 |     Right v => getStack >>= onval (TTime v)

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

142 | val' : a -> TomlValue -> (a, Step q TSz ST)

143 | val' x = val x . const

149 | tomlSpaced : Steps q TSz ST -> DFA q TSz ST

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

152 | tomlIgnore : TST -> Steps q TSz ST -> DFA q TSz ST

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

155 | keySteps : Steps q TSz ST

156 | keySteps =

157 |   [ string unquotedKey onkey

158 |   , opn' '\'' LKey

159 |   , opn' '"'  QKey

160 |   ]

162 | valSteps : Steps q TSz ST

163 | valSteps =

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

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

167 |   -- integers

168 |   , val  decInt  (TInt . readDecInt)

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

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

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

173 |   -- floats

174 |   , val' nan     (TDbl NaN)

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

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

177 |   , val float    (TDbl . readFloat)

179 |   -- Date and Time

180 |   , valE fullDate  (ATLocalDate . readLocalDate)

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

182 |   , valE localTime (ATLocalTime . readLocalTime)

183 |   , valE localDateTime (ATLocalDateTime . readLocalDateTime)

184 |   , valE offsetDateTime (ATOffsetDateTime . readOffsetDateTime)

186 |   -- Nested Values

187 |   , opn '[' openArray

188 |   , opn '{' openInlineTable

190 |   -- Strings

191 |   , opn' '"'  QStr

192 |   , opn' '\'' LStr

193 |   , opn' #"""""# MLQStr

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

195 |   , opn' "'''" MLLStr

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

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

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

199 |   ]

201 | escapes : TST -> Steps q TSz ST

202 | escapes res =

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

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

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

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

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

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

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

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

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

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

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

214 |     ]

216 | mlqDFA : DFA q TSz ST

217 | mlqDFA =

218 |   dfa $

219 |     [ closeStr #"""""# qstr

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

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

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

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

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

225 |     , step' mlbEscapedNL MLQStr

226 |     ] ++ escapes MLQStr

228 | mllDFA : DFA q TSz ST

229 | mllDFA =

230 |   dfa $

231 |     [ closeStr "'''" qstr

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

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

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

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

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

237 |     , string literalChars (pushStr MLLStr)

238 |     ]

244 | tomlTrans : Lex1 q TSz ST

245 | tomlTrans =

246 |   lex1

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

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

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

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

251 |     , E EKey $ tomlSpaced keySteps

252 |     , E EVal $ tomlSpaced valSteps

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

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

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

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

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

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

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

260 |     , E MLQStr mlqDFA

261 |     , E MLLStr mllDFA

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

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

264 |     , E TCom $ tomlSpaced keySteps

265 |     , E EOL  $ tomlIgnore TIni []

266 |     ]

268 | tomlErr : Arr32 TSz (ST q -> F1 q TErr)

269 | tomlErr =

270 |   arr32 TSz (unexpected [])

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

286 |     ]

288 | tomlEOI : TST -> ST q -> F1 q (Either TErr TomlTable)

289 | tomlEOI st sk =

290 |   case st == TIni || st == EOL of

291 |     False => arrFail ST tomlErr st sk

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

295 | toml : P1 q TErr TomlTable

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