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.Derive

  9 | import public Text.ILex

 11 | %default total

 12 | %language ElabReflection

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

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

 19 | jdouble : String -> Double

 25 | public export

 26 | escape : SnocList Char -> Char -> SnocList Char

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

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

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

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

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

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

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

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

 35 | escape sc c =

 36 |   if isControl c

 37 |     then

 38 |       let x  := the Integer $ cast c

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

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

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

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

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

 44 |     else sc :< c

 46 | public export

 47 | encode : String -> String

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

 54 | public export

 55 | data JSON : Type where

 56 |   JNull   : JSON

 57 |   JInteger : Integer -> JSON

 58 |   JDouble : Double -> JSON

 59 |   JBool   : Bool   -> JSON

 60 |   JString : String -> JSON

 61 |   JArray  : List JSON -> JSON

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

 64 | %runElab derive "JSON" [Eq]

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

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

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

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

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

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

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

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

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

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

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

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

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

 83 |    in showArray ss' t

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

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

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

 87 |    in showObject ss' t

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

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

 92 | showArray ss (h :: t) =

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

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

 96 | showObject ss (h :: t) =

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

 99 | showImpl : JSON -> String

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

102 | export %inline

103 | Show JSON where

104 |   show = showImpl

108 | dropNull : JSON -> JSON

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

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

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

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

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

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

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

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

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

121 | dropNull x            = x

127 | %runElab deriveParserState "JSz" "JST"

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

130 | data Part : Type where

131 |   PA : Part -> SnocList JSON -> Part -- partial array

132 |   PO : Part -> SnocList (String,JSON) -> Part -- partial object

133 |   PL : Part -> SnocList (String,JSON) -> String -> Part -- partial object

134 |   PI : Part -- initial value

135 |   PV : SnocList JSON -> Part -- initial value for value streaming

136 |   PF : JSON -> Part -- final value

138 | public export

139 | 0 SK : Type -> Type

140 | SK = Stack Void Part JSz

146 | parameters {auto sk : SK q}

148 |   %inline

149 |   part : JSON -> Part -> F1 q JST

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

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

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

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

155 |   %inline

156 |   onVal : JSON -> F1 q JST

157 |   onVal v = getStack >>= part v

159 |   %inline

160 |   endStr : String -> F1 q JST

161 |   endStr s = T1.do

162 |    getStack >>= \case

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

164 |      p      => part (JString s) p

166 |   %inline

167 |   closeVal : F1 q JST

168 |   closeVal =

169 |     getStack >>= \case

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

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

172 |       _       => pure JDone

179 | spaced : Index r -> Steps q r SK -> DFA q r SK

180 | spaced x = dfa . jsonSpaced x

183 | jsonDouble : RExp True

184 | jsonDouble =

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

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

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

190 | valTok : JST -> Steps q JSz SK -> DFA q JSz SK

191 | valTok x ts =

192 |   spaced x $

193 |     [ cexpr "null"  (onVal JNull)

194 |     , cexpr "true"  (onVal $ JBool True)

195 |     , cexpr "false" (onVal $ JBool False)

196 |     , conv (opt '-' >> decimal) (onVal . JInteger . integer)

197 |     , read jsonDouble (onVal . JDouble . jdouble)

198 |     , copen '{' (modStackAs SK (`PO` [<]) ONew)

199 |     , copen '[' (modStackAs SK (`PA` [<]) ANew)

200 |     , copen' '"' JStr

201 |     ] ++ ts

203 | codepoint : RExp True

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

206 | decode : ByteString -> String

207 | decode (BS 6 bv) =

208 |  singleton $ cast {to = Char} $

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

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

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

212 |    hexdigit (bv `at` 5)

213 | decode _         = "" -- impossible

215 | jchar : RExp True

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

219 | strTok : DFA q JSz SK

220 | strTok =

221 |   dfa

222 |     [ ccloseStr '"' endStr

223 |     , read (plus jchar) (pushStr JStr)

224 |     , cexpr #"\""# (pushStr JStr "\"")

225 |     , cexpr #"\n"# (pushStr JStr "\n")

226 |     , cexpr #"\f"# (pushStr JStr "\f")

227 |     , cexpr #"\b"# (pushStr JStr "\b")

228 |     , cexpr #"\r"# (pushStr JStr "\r")

229 |     , cexpr #"\t"# (pushStr JStr "\t")

230 |     , cexpr #"\\"# (pushStr JStr "\\")

231 |     , cexpr #"\/"# (pushStr JStr "\/")

232 |     , conv codepoint (pushStr JStr . decode)

233 |     ]

239 | jsonTrans : Lex1 q JSz SK

240 | jsonTrans =

241 |   lex1

242 |     [ E JIni (valTok JIni [])

243 |     , E JDone (spaced JDone [])

245 |     , E ANew (valTok ANew [cclose ']' closeVal])

246 |     , E ACom (valTok ACom [])

247 |     , E AVal $ spaced AVal [cexpr' ',' ACom, cclose ']' closeVal]

249 |     , E ONew $ spaced ONew [cclose '}' closeVal, copen' '"' JStr]

250 |     , E OVal $ spaced OVal [cclose '}' closeVal, cexpr' ',' OCom]

251 |     , E OCom $ spaced OCom [copen' '"' JStr]

252 |     , E OLbl $ spaced OLbl [cexpr' ':' OCol]

253 |     , E OCol (valTok OCol [])

255 |     , E JStr strTok

256 |     ]

258 | jsonErr : Arr32 JSz (SK q -> F1 q (BoundedErr Void))

259 | jsonErr =

260 |   arr32 JSz (unexpected [])

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

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

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

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

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

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

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

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

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

270 |     ]

272 | jsonEOI : JST -> SK q -> F1 q (Either (BoundedErr Void) JSON)

273 | jsonEOI sk s t =

274 |   case sk == JDone of

275 |     False => arrFail SK jsonErr sk s t

276 |     True  => case getStack t of

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

278 |       _    # t => Right JNull # t

280 | public export

281 | json : P1 q (BoundedErr Void) JSON

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

284 | export %inline

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

286 | parseJSON = parseString json

292 | extract : Part -> (Part, Maybe $ List JSON)

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

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

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

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

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

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

299 | extract p                = (p, Nothing)

301 | arrChunk : SK q -> F1 q (Maybe $ List JSON)

302 | arrChunk sk = T1.do

303 |   p <- getStack

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

305 |   putStackAs p2 res

307 | arrEOI : JST -> SK q -> F1 q (Either (BoundedErr Void) (List JSON))

308 | arrEOI st sk t =

309 |   case st == JIni of

310 |     True  => case getStack t of

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

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

313 |     False => case jsonEOI st sk t of

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

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

316 |       Left x            # t => Left x # t

320 | public export

321 | jsonArray : P1 q (BoundedErr Void) (List JSON)

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

329 | public export

330 | jsonValues : P1 q (BoundedErr Void) (List JSON)

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