0 | module JSON.Parser

  2 | import Derive.Prelude

  3 | import public Text.Parse.Manual

  5 | %default total

  6 | %language ElabReflection

 12 | public export

 13 | hexChar : Integer -> Char

 14 | hexChar 0 = '0'

 15 | hexChar 1 = '1'

 16 | hexChar 2 = '2'

 17 | hexChar 3 = '3'

 18 | hexChar 4 = '4'

 19 | hexChar 5 = '5'

 20 | hexChar 6 = '6'

 21 | hexChar 7 = '7'

 22 | hexChar 8 = '8'

 23 | hexChar 9 = '9'

 24 | hexChar 10 = 'a'

 25 | hexChar 11 = 'b'

 26 | hexChar 12 = 'c'

 27 | hexChar 13 = 'd'

 28 | hexChar 14 = 'e'

 29 | hexChar _  = 'f'

 31 | public export

 32 | escape : SnocList Char -> Char -> SnocList Char

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

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

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

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

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

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

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

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

 41 | escape sc c =

 42 |   if isControl c

 43 |     then

 44 |       let x  := the Integer $ cast c 

 45 |           d1 := hexChar $ x `div` 0x1000

 46 |           d2 := hexChar $ (x `mod` 0x1000) `div` 0x100

 47 |           d3 := hexChar $ (x `mod` 0x100)  `div` 0x10

 48 |           d4 := hexChar $ x `mod` 0x10

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

 50 |     else sc :< c

 52 | public export

 53 | encode : String -> String

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

 60 | public export

 61 | data JSON : Type where

 62 |   JNull   : JSON

 63 |   JInteger : Integer -> JSON

 64 |   JDouble : Double -> JSON

 65 |   JBool   : Bool   -> JSON

 66 |   JString : String -> JSON

 67 |   JArray  : List JSON -> JSON

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

 70 | %runElab derive "JSON" [Eq]

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

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

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

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

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

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

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

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

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

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

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

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

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

 89 |    in showArray ss' t

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

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

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

 93 |    in showObject ss' t

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

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

 98 | showArray ss (h :: t) =

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

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

102 | showObject ss (h :: t) =

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

105 | showImpl : JSON -> String

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

108 | export %inline

109 | Show JSON where

110 |   show = showImpl

114 | dropNull : JSON -> JSON

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

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

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

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

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

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

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

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

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

127 | dropNull x            = x

133 | public export

134 | data JSToken : Type where

135 |   Symbol   : Char -> JSToken

136 |   Lit      : JSON -> JSToken

137 |   EOI      : JSToken

140 | fromChar : Char -> JSToken

141 | fromChar = Symbol

143 | %runElab derive "JSToken" [Show,Eq]

146 | Interpolation JSToken where

147 |   interpolate (Symbol c) = singleton c

148 |   interpolate (Lit x)  = "\{show x}"

149 |   interpolate EOI      = "end of input"

151 | public export %tcinline

152 | 0 ParseErr : Type

153 | ParseErr = InnerError Void

155 | strLit : SnocList Char -> JSToken

156 | strLit = Lit . JString . cast

158 | str : SnocList Char -> AutoTok e JSToken

159 | str sc ('\\' :: c  :: xs) = case c of

160 |   '"'  => str (sc :< '"') xs

161 |   'n'  => str (sc :< '\n') xs

162 |   'f'  => str (sc :< '\f') xs

163 |   'b'  => str (sc :< '\b') xs

164 |   'r'  => str (sc :< '\r') xs

165 |   't'  => str (sc :< '\t') xs

166 |   '\\' => str (sc :< '\\') xs

167 |   '/'  => str (sc :< '/') xs

168 |   'u'  => case xs of

169 |     w :: x :: y :: z :: t' =>

170 |       if isHexDigit w && isHexDigit x && isHexDigit y && isHexDigit z

171 |         then

172 |           let c :=

173 |                 cast $

174 |                   hexDigit w * 0x1000 +

175 |                   hexDigit x * 0x100 +

176 |                   hexDigit y * 0x10 +

177 |                   hexDigit z

178 |            in str (sc :< c) t'

179 |         else invalidEscape p t'

180 |     _    => invalidEscape p xs

181 |   _    => invalidEscape p xs

182 | str sc ('"'  :: xs) = Succ (strLit sc) xs

183 | str sc (c    :: xs) =

184 |   if isControl c then range (InvalidControl c) p xs

185 |   else str (sc :< c) xs

186 | str sc []           = eoiAt p

188 | invalidKey : StrictTok e JSToken

189 | invalidKey (x::xs) =

190 |   if isAlpha x then invalidKey xs else unknownRange Same (x::xs)

191 | invalidKey []      = unknownRange Same []

193 | toToken : Cast String a => (a -> JSON) -> SnocList Char -> JSToken

194 | toToken toJSON = (Lit . toJSON . cast . cast {to = String})

196 | numberToken : SnocList Char -> JSToken

197 | numberToken l = case find (\c =>  c == '.' || c == 'e' || c == 'E') l of

198 |   Just _  => toToken JDouble l

199 |   Nothing => toToken JInteger l

201 | term : Tok True e JSToken

202 | term (x :: xs) = case x of

203 |   ',' => Succ ',' xs

204 |   '"' => str [<] xs

205 |   ':' => Succ ':' xs

206 |   '[' => Succ '[' xs

207 |   ']' => Succ ']' xs

208 |   '{' => Succ '{' xs

209 |   '}' => Succ '}' xs

210 |   'n' => case xs of

211 |     'u' :: 'l' :: 'l' :: t => Succ (Lit JNull) t

212 |     _                      => invalidKey ('n'::xs)

213 |   't' => case xs of

214 |     'r' :: 'u' :: 'e' :: t => Succ (Lit $ JBool True) t

215 |     _                      => invalidKey ('t'::xs)

216 |   'f' => case xs of

217 |     'a' :: 'l' :: 's' :: 'e' :: t => Succ (Lit $ JBool False) t

218 |     _                             => invalidKey ('f'::xs)

219 |   d   => suffix numberToken $

220 |          number [<] (d :: xs)

222 | term []        = eoiAt Same

224 | go :

225 |      SnocList (Bounded JSToken)

226 |  -> (pos   : Position)

227 |  -> (cs    : List Char)

228 |  -> (0 acc : SuffixAcc cs)

229 |  -> Either (Bounded ParseErr) (List (Bounded JSToken))

230 | go sx pos ('\n' :: xs) (SA rec) = go sx (incLine pos) xs rec

231 | go sx pos (x :: xs)    (SA rec) =

232 |   if isSpace x

233 |      then go sx (incCol pos) xs rec

234 |      else case term (x::xs) of

235 |        Succ t xs' @{prf} =>

236 |          let pos2 := addCol (toNat prf) pos

237 |              bt   := bounded t pos pos2

238 |           in go (sx :< bt) pos2 xs' rec

239 |        Fail start errEnd r => Left $ boundedErr pos start errEnd r

240 | go sx pos [] _ = Right (sx <>> [B EOI $ oneChar pos])

243 | lexJSON : String -> Either (Bounded ParseErr) (List (Bounded JSToken))

244 | lexJSON s = go [<] begin (unpack s) suffixAcc

250 | 0 Rule : Bool -> Type -> Type

251 | Rule b t =

252 |      (xs : List $ Bounded JSToken)

253 |   -> (0 acc : SuffixAcc xs)

254 |   -> Res b JSToken xs Void t

256 | array : Bounds -> SnocList JSON -> Rule True JSON

258 | object : Bounds -> SnocList (String,JSON) -> Rule True JSON

260 | value : Rule True JSON

261 | value (B (Lit y) _ :: xs)        _      = Succ0 y xs

262 | value (B '[' _ :: B ']' _ :: xs) _      = Succ0 (JArray []) xs

263 | value (B '[' b :: xs)            (SA r) = succT $ array b [<] xs r

264 | value (B '{' _ :: B '}' _ :: xs) _      = Succ0 (JObject []) xs

265 | value (B '{' b :: xs)            (SA r) = succT $ object b [<] xs r

266 | value xs                         _      = fail xs

273 | array b sv xs sa@(SA r) = case value xs sa of

274 |   Succ0 v (B ',' _ :: ys)    => succT $ array b (sv :< v) ys r

275 |   Succ0 v (B ']' _ :: ys)    => Succ0 (JArray $ sv <>> [v]) ys

276 |   r@(Succ0 v (B EOI _ :: _)) => unclosed b '['

277 |   r@(Fail0 (B (Expected [] "end of input") _)) => unclosed b '['

278 |   r                          => failInParen b '[' r

280 | object b sv (B (Lit $ JString l) _ :: B ':' _ :: xs) (SA r) =

281 |   case succT $ value xs r of

282 |     Succ0 v (B ',' _ :: ys) => succT $ object b (sv :< (l,v)) ys r

283 |     Succ0 v (B '}' _ :: ys) => Succ0 (JObject $ sv <>> [(l,v)]) ys

284 |     r@(Succ0 v (B EOI _ :: _)) => unclosed b '{'

285 |     r@(Fail0 (B (Expected [] "end of input") _)) => unclosed b '{'

286 |     r                          => failInParen b '{' r

287 | object b sv (B (Lit $ JString _) _ :: x :: xs) _ = expected x.bounds ":" "\{x.val}"

288 | object b sv (x :: xs) _ = expected x.bounds "\"" "\{x.val}"

289 | object b sv [] _ = eoi

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

293 | parseJSON o str = case lexJSON str of

294 |   Right ts => case value ts suffixAcc of

295 |     Fail0 x           => Left (toParseError o str x)

296 |     Succ0 v [B EOI _] => Right v

297 |     Succ0 v []        => Right v

298 |     Succ0 v (x::xs)   => leftErr o str $ unexpected x

299 |   Left err => Left (toParseError o str err)