0 | module JSON.Parser

  2 | import Data.Bits

  3 | import Data.Buffer

  4 | import Data.Linear.Ref1

  5 | import Derive.Prelude

  6 | import Syntax.T1

  7 | import Text.ILex.State.Derive

  8 | import Text.ILex.State.Regular

  9 | import public Text.ILex

 11 | %default total

 12 | %hide Data.Linear.(.)

 13 | %hide Data.Linear.Ref1.ST

 14 | %language ElabReflection

 19 | export %foreign "scheme:(lambda (s) (string->number s))"

 20 |                 "javascript:lambda:(s) => Number(s)"

 21 | jdouble : String -> Double

 27 | public export

 28 | escape : SnocList Char -> Char -> SnocList Char

 29 | escape sc '"'  = sc :< '\\' :< '"'

 30 | escape sc '\n' = sc :< '\\' :< 'n'

 31 | escape sc '\f' = sc :< '\\' :< 'f'

 32 | escape sc '\b' = sc :< '\\' :< 'b'

 33 | escape sc '\r' = sc :< '\\' :< 'r'

 34 | escape sc '\t' = sc :< '\\' :< 't'

 35 | escape sc '\\' = sc :< '\\' :< '\\'

 36 | escape sc '/'  = sc :< '\\' :< '/'

 37 | escape sc c =

 38 |   if isControl c

 39 |     then

 40 |       let x  := the Integer $ cast c

 41 |           d1 := hexChar $ cast $ (shiftR x 12 .&. 0xf)

 42 |           d2 := hexChar $ cast $ (shiftR x 8 .&. 0xf)

 43 |           d3 := hexChar $ cast $ (shiftR x 4 .&. 0xf)

 44 |           d4 := hexChar $ cast (x .&. 0xf)

 45 |        in sc :< '\\' :< 'u' :< d1 :< d2 :< d3 :< d4

 46 |     else sc :< c

 48 | public export

 49 | encode : String -> String

 50 | encode s = pack (foldl escape [<'"'] (unpack s) <>> ['"'])

 56 | public export

 57 | data JSON : Type where

 58 |   JNull   : JSON

 59 |   JInteger : Integer -> JSON

 60 |   JDouble : Double -> JSON

 61 |   JBool   : Bool   -> JSON

 62 |   JString : String -> JSON

 63 |   JArray  : List JSON -> JSON

 64 |   JObject : List (String, JSON) -> JSON

 66 | %runElab derive "JSON" [Eq]

 68 | showValue : SnocList String -> JSON -> SnocList String

 70 | showPair : SnocList String -> (String,JSON) -> SnocList String

 72 | showArray : SnocList String -> List JSON -> SnocList String

 74 | showObject : SnocList String -> List (String,JSON) -> SnocList String

 76 | showValue ss JNull              = ss :< "null"

 77 | showValue ss (JInteger ntgr)      = ss :< show ntgr

 78 | showValue ss (JDouble dbl)      = ss :< show dbl

 79 | showValue ss (JBool True)       = ss :< "true"

 80 | showValue ss (JBool False)      = ss :< "false"

 81 | showValue ss (JString str)      = ss :< encode str

 82 | showValue ss (JArray [])        = ss :< "[]"

 83 | showValue ss (JArray $ h :: t)  =

 84 |   let ss' = showValue (ss :< "[") h

 85 |    in showArray ss' t

 86 | showValue ss (JObject [])       = ss :< "{}"

 87 | showValue ss (JObject $ h :: t) =

 88 |   let ss' = showPair (ss :< "{") h

 89 |    in showObject ss' t

 91 | showPair ss (s,v) = showValue (ss :< encode s :< ":") v

 93 | showArray ss [] = ss :< "]"

 94 | showArray ss (h :: t) =

 95 |   let ss' = showValue (ss :< ",") h in showArray ss' t

 97 | showObject ss [] = ss :< "}"

 98 | showObject ss (h :: t) =

 99 |   let ss' = showPair (ss :< ",") h in showObject ss' t

101 | showImpl : JSON -> String

102 | showImpl v = fastConcat $ showValue Lin v <>> Nil

104 | export %inline

105 | Show JSON where

106 |   show = showImpl

110 | dropNull : JSON -> JSON

112 | dropNulls : SnocList JSON -> List JSON -> JSON

113 | dropNulls sx []        = JArray $ sx <>> []

114 | dropNulls sx (x :: xs) = dropNulls (sx :< dropNull x) xs

116 | dropNullsP : SnocList (String,JSON) -> List (String,JSON) -> JSON

117 | dropNullsP sx []                = JObject $ sx <>> []

118 | dropNullsP sx ((_,JNull) :: xs) = dropNullsP sx xs

119 | dropNullsP sx ((s,j)     :: xs) = dropNullsP (sx :< (s, dropNull j)) xs

121 | dropNull (JArray xs)  = dropNulls [<] xs

122 | dropNull (JObject xs) = dropNullsP [<] xs

123 | dropNull x            = x

129 | %runElab deriveParserState "JSz" "JST"

130 |   ["JIni","ANew","AVal","ACom","ONew","OVal","OCom","OLbl","OCol","JStr","JDone"]

132 | data Stack : Type where

133 |   PA : Stack -> SnocList JSON -> Stack -- partial array

134 |   PO : Stack -> SnocList (String,JSON) -> Stack -- partial object

135 |   PL : Stack -> SnocList (String,JSON) -> String -> Stack -- partial object

136 |   PI : Stack -- initial value

137 |   PV : SnocList JSON -> Stack -- initial value for value streaming

138 |   PF : JSON -> Stack -- final value

140 | public export

141 | 0 ST : Type -> Type

142 | ST = State Void Stack JSz

148 | parameters {auto sk : ST q}

150 |   %inline

151 |   part : JSON -> Stack -> F1 q JST

152 |   part v (PA p sy)   = putStackAs (PA p (sy :< v)) AVal

153 |   part v (PL p sy l) = putStackAs (PO p (sy :< (l,v))) OVal

154 |   part v (PV sy)     = putStackAs (PV (sy :< v)) JIni

155 |   part v _           = putStackAs (PF v) JDone

157 |   %inline

158 |   onVal : JSON -> F1 q JST

159 |   onVal v = getStack >>= part v

161 |   %inline

162 |   endStr : String -> F1 q JST

163 |   endStr s = T1.do

164 |    getStack >>= \case

165 |      PO a b => putStackAs (PL a b s) OLbl

166 |      p      => part (JString s) p

168 |   %inline

169 |   closeVal : F1 q JST

170 |   closeVal =

171 |     getStack >>= \case

172 |       PO p sp => part (JObject $ sp <>> []) p

173 |       PA p sp => part (JArray $ sp <>> []) p

174 |       _       => pure JDone

181 | spaced : Steps q r ST -> DFA q r ST

182 | spaced = dfa . jsonSpaced

185 | jsonDouble : RExp True

186 | jsonDouble =

187 |   let frac  = '.' >> plus digit

188 |       exp   = oneof ['e','E'] >> opt (oneof ['+','-']) >> plus digit

189 |    in opt '-' >> decimal >> opt frac >> opt exp

192 | valTok : Steps q JSz ST -> DFA q JSz ST

193 | valTok ts =

194 |   spaced $

195 |     [ step "null"  (onVal JNull)

196 |     , step "true"  (onVal $ JBool True)

197 |     , step "false" (onVal $ JBool False)

198 |     , bytes (opt '-' >> decimal) (onVal . JInteger . Util.integer)

199 |     , string jsonDouble (onVal . JDouble . jdouble)

200 |     , opn '{' (modStackAs ST (`PO` [<]) ONew)

201 |     , opn '[' (modStackAs ST (`PA` [<]) ANew)

202 |     , opn' '"' JStr

203 |     ] ++ ts

205 | codepoint : RExp True

206 | codepoint = #"\u"# >> hexdigit >> hexdigit >> hexdigit >> hexdigit

208 | decode : ByteString -> String

209 | decode (BS 6 bv) =

210 |  singleton $ cast {to = Char} $

211 |    hexdigit (bv `at` 2) * 0x1000 +

212 |    hexdigit (bv `at` 3) * 0x100  +

213 |    hexdigit (bv `at` 4) * 0x10   +

214 |    hexdigit (bv `at` 5)

215 | decode _         = "" -- impossible

217 | jchar : RExp True

218 | jchar = range32 0x20 0x10ffff && not '"' && not '\\'

221 | strTok : DFA q JSz ST

222 | strTok =

223 |   dfa

224 |     [ closeStr '"' endStr

225 |     , string (plus jchar) (pushStr JStr)

226 |     , step #"\""# (pushStr JStr "\"")

227 |     , step #"\n"# (pushStr JStr "\n")

228 |     , step #"\f"# (pushStr JStr "\f")

229 |     , step #"\b"# (pushStr JStr "\b")

230 |     , step #"\r"# (pushStr JStr "\r")

231 |     , step #"\t"# (pushStr JStr "\t")

232 |     , step #"\\"# (pushStr JStr "\\")

233 |     , step #"\/"# (pushStr JStr "\/")

234 |     , bytes codepoint (pushStr JStr . decode)

235 |     ]

241 | jsonTrans : Lex1 q JSz ST

242 | jsonTrans =

243 |   lex1

244 |     [ E JIni (valTok [])

245 |     , E JDone (spaced [])

247 |     , E ANew (valTok [close ']' closeVal])

248 |     , E ACom (valTok [])

249 |     , E AVal $ spaced [step' ',' ACom, close ']' closeVal]

251 |     , E ONew $ spaced [close '}' closeVal, opn' '"' JStr]

252 |     , E OVal $ spaced [close '}' closeVal, step' ',' OCom]

253 |     , E OCom $ spaced [opn' '"' JStr]

254 |     , E OLbl $ spaced [step' ':' OCol]

255 |     , E OCol (valTok [])

257 |     , E JStr strTok

258 |     ]

260 | jsonErr : Arr32 JSz (ST q -> F1 q (BBErr Void))

261 | jsonErr =

262 |   arr32 JSz (unexpected [])

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

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

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

266 |     , E ONew $ unclosedIfEOI "{" ["\"", "}"]

267 |     , E OVal $ unclosedIfEOI "{" [",", "}"]

268 |     , E OCom $ unclosedIfEOI "{" ["\""]

269 |     , E OLbl $ unclosedIfEOI "{" [":"]

270 |     , E OCol $ unclosedIfEOI "{" []

271 |     , E JStr $ unclosedIfNLorEOI "\"" []

272 |     ]

274 | jsonEOI : JST -> ST q -> F1 q (Either (BBErr Void) JSON)

275 | jsonEOI sk s t =

276 |   case sk == JDone of

277 |     False => arrFail ST jsonErr sk s t

278 |     True  => case getStack t of

279 |       PF v # t => Right v # t

280 |       _    # t => Right JNull # t

282 | public export

283 | json : P1 q (BBErr Void) JSON

284 | json = P JIni (init PI) jsonTrans (\x => (Nothing #)) jsonErr jsonEOI

286 | export %inline

287 | parseJSON : Origin -> String -> Either (ParseError Void) JSON

288 | parseJSON = parseString json

294 | extract : Stack -> (Stack, Maybe $ List JSON)

295 | extract (PF (JArray vs)) = (PF (JArray []), Just vs)

296 | extract (PA PI sv)       = (PA PI [<], maybeList sv)

297 | extract (PV sv)          = (PV [<], maybeList sv)

298 | extract (PA p sv)        = let (p2,m) := extract p in (PA p2 sv, m)

299 | extract (PO p sv)        = let (p2,m) := extract p in (PO p2 sv, m)

300 | extract (PL p sv l)      = let (p2,m) := extract p in (PL p2 sv l, m)

301 | extract p                = (p, Nothing)

303 | arrChunk : ST q -> F1 q (Maybe $ List JSON)

304 | arrChunk sk = T1.do

305 |   p <- getStack

306 |   let (p2,res) := extract p

307 |   putStackAs p2 res

309 | arrEOI : JST -> ST q -> F1 q (Either (BBErr Void) (List JSON))

310 | arrEOI st sk t =

311 |   case st == JIni of

312 |     True  => case getStack t of

313 |       PV sv # t => Right (sv <>> []) # t

314 |       _     # t => Right [] # t

315 |     False => case jsonEOI st sk t of

316 |       Right (JArray vs) # t => Right vs # t

317 |       Right _           # t => Right [] # t

318 |       Left x            # t => Left x # t

323 | jsonArray : P1 q (BBErr Void) (List JSON)

324 | jsonArray = P JIni (init PI) jsonTrans arrChunk jsonErr arrEOI

332 | jsonValues : P1 q (BBErr Void) (List JSON)

333 | jsonValues = P JIni (init $ PV [<]) jsonTrans arrChunk jsonErr arrEOI