0 | module HTTP.API.Decode

  2 | import Data.List.Quantifiers as L

  3 | import Derive.Prelude

  4 | import HTTP.FormData

  5 | import HTTP.Header.Types

  6 | import HTTP.RequestErr

  7 | import HTTP.Status

  8 | import HTTP.URI

  9 | import JSON.Simple

 10 | import JSON.Simple.Derive

 12 | %default total

 13 | %language ElabReflection

 17 | public export

 18 | data DecodeErr : Type where

 19 |   ||| A `ReadErr` typically occurs when reading a single value

 25 |   ReadErr    : (type, value : String) -> (details : String) -> DecodeErr

 27 |   ||| A `ContentErr` is - in general - a more technical error that happend

 31 |   ContentErr : (type : String) -> (details : String) -> DecodeErr

 33 |   ||| An arbitrary custom error message.

 34 |   Msg        : (message : String) -> DecodeErr

 36 | %runElab derive "DecodeErr" [Show,Eq,FromJSON,ToJSON]

 39 | export %inline

 40 | readErr : (type : String) -> (value : ByteString) -> DecodeErr

 41 | readErr type value = ReadErr type (toString value) ""

 44 | export %inline

 45 | contentErr : (type : String) -> Interpolation a => a -> DecodeErr

 46 | contentErr type = ContentErr type . interpolate

 50 | setType : String -> DecodeErr -> DecodeErr

 51 | setType t (ReadErr _ v d)  = ReadErr t v d

 52 | setType t (ContentErr _ d) = ContentErr t d

 53 | setType t (Msg m)          = Msg m

 57 | setValue : String -> DecodeErr -> DecodeErr

 58 | setValue v (ReadErr t _ d)  = ReadErr t v d

 59 | setValue _ err              = err

 63 | modMsg : (String -> String) -> DecodeErr -> DecodeErr

 64 | modMsg f (ReadErr t v d)  = ReadErr t v (f d)

 65 | modMsg f (ContentErr t d) = ContentErr t (f d)

 66 | modMsg f (Msg m)          = Msg (f m)

 72 | detailString : String -> String

 73 | detailString "" = ""

 74 | detailString s  = " \{s}."

 76 | valueString : String -> String

 77 | valueString "" = ""

 78 | valueString s  = ": '\{s}'"

 81 | Interpolation DecodeErr where

 82 |   interpolate (ReadErr t s d) = "Invalid \{t}\{valueString s}.\{detailString d}"

 83 |   interpolate (ContentErr t d) = "Invalid \{t}."

 84 |   interpolate (Msg msg) = msg

 90 | dets : DecodeErr -> String

 91 | dets (ContentErr _ ds) = ds

 92 | dets _                 = ""

 95 | decodeErr : Status -> DecodeErr -> RequestErr

 96 | decodeErr s de = {message := "\{de}", details := dets de} (requestErr s)

103 | public export

104 | interface Decode (0 a : Type) where

105 |   decode : ByteString -> Either DecodeErr a

109 | public export %inline

110 | decodeAs : (0 a : Type) -> Decode a => ByteString -> Either DecodeErr a

111 | decodeAs _ = decode

115 | public export

116 | interface DecodeMany (0 a : Type) where

117 |   simulateDecode : List ByteString -> Maybe (List ByteString)

119 |   decodeMany : List ByteString -> Either DecodeErr (List ByteString, a)

122 | Decode a => DecodeMany a where

123 |   simulateDecode []      = Nothing

124 |   simulateDecode (b::bs) = Just bs

126 |   decodeMany []      = Left (Msg "Unexpected end of URL path")

127 |   decodeMany (b::bs) = (bs,) <$> decode b

130 | decodeAll :

131 |      SnocList a

132 |   -> Decode a

133 |   -> List ByteString

134 |   -> Either DecodeErr (List ByteString,SnocList a)

135 | decodeAll sx d []        = Right ([],sx)

136 | decodeAll sx d (x :: xs) =

137 |   case decode @{d} x of

138 |     Right v  => decodeAll (sx:<v) d xs

139 |     Left err => Left err

142 | Decode a => DecodeMany (SnocList a) where

143 |   simulateDecode bs = Just []

144 |   decodeMany = decodeAll [<] %search

147 | Decode a => DecodeMany (List a) where

148 |   simulateDecode bs = Just []

149 |   decodeMany bs = map (<>> []) <$> decodeAll [<] %search bs

151 | simulateHL :

152 |      L.All.All (DecodeMany . f) ts

153 |   -> List ByteString

154 |   -> Maybe (List ByteString)

155 | simulateHL []       xs = Just xs

156 | simulateHL (x :: y) xs =

157 |   case simulateDecode @{x} xs of

158 |     Nothing  => Nothing

159 |     Just xs2 => simulateHL y xs2

161 | decodeHL :

162 |      L.All.All (DecodeMany . f) ts

163 |   -> List ByteString

164 |   -> Either DecodeErr (List ByteString, L.All.All f ts)

165 | decodeHL []       xs = Right (xs, [])

166 | decodeHL (x :: y) xs =

167 |   case decodeMany @{x} xs of

168 |     Left err       => Left err

169 |     Right (xs2, v) => map (v::) <$> decodeHL y xs2

171 | export %inline

172 | (all : L.All.All (DecodeMany . f) ts) => DecodeMany (L.All.All f ts) where

173 |   simulateDecode = simulateHL all

174 |   decodeMany = decodeHL all

176 | simulateN :

177 |      DecodeMany t

178 |   -> (n : Nat)

179 |   -> List ByteString

180 |   -> Maybe (List ByteString)

181 | simulateN x 0     xs = Just xs

182 | simulateN x (S n) xs =

183 |   case simulateDecode @{x} xs of

184 |     Nothing  => Nothing

185 |     Just xs2 => simulateN x n xs2

187 | decodeN :

188 |      DecodeMany t

189 |   -> (n : Nat)

190 |   -> List ByteString

191 |   -> Either DecodeErr (List ByteString, Vect n t)

192 | decodeN x 0     xs = Right (xs, [])

193 | decodeN x (S n) xs =

194 |   case decodeMany @{x} xs of

195 |     Left err       => Left err

196 |     Right (xs2, v) => map (v::) <$> decodeN x n xs2

198 | export %inline

199 | {n : Nat} -> (x : DecodeMany a) => DecodeMany (Vect n a) where

200 |   simulateDecode = simulateN x n

201 |   decodeMany = decodeN x n

207 | namespace DecodeVia

208 |   public export

209 |   interface DecodeVia (0 from, to : Type) where

210 |     fromBytes  : Parameters -> ByteString -> Either DecodeErr from

211 |     decodeFrom : from -> Either DecodeErr to

212 |     mediaType  : MediaType

215 | decodeVia :

216 |      {auto d : DecodeVia from to}

217 |   -> Parameters

218 |   -> ByteString

219 |   -> Either DecodeErr to

220 | decodeVia ps bs = fromBytes @{d} ps bs >>= decodeFrom

223 | FromJSON a => DecodeVia JSON a where

224 |   fromBytes _ = mapFst (contentErr "JSON value") . parseBytes json Virtual

225 |   decodeFrom  = mapFst (contentErr "JSON value" . JErr) . fromJSON

226 |   mediaType   = MT "application" "json"

228 | public export

229 | interface FromFormData a where

230 |   fromFormData : FormData -> Either DecodeErr a

233 | FromFormData a => DecodeVia FormData a where

234 |   fromBytes ps bs =

235 |     case parameter "boundary" ps of

236 |       Just b  => Right $ multipart (fromString b) bs

237 |       Nothing => Left $ Msg "invalid form-data header: missing boundary"

238 |   decodeFrom      = fromFormData

239 |   mediaType       = MT "multipart" "form-data"

242 | getFDBytes : String -> FormData -> Either DecodeErr ByteString

243 | getFDBytes s xs =

244 |   case find ((s ==) . name) xs of

245 |     Nothing => Left $ Msg "missing form-data part: \{s} (parts: \{show $ map name xs})"

246 |     Just p  => Right p.content

253 | refinedEither :

254 |      {auto r : Decode a}

255 |   -> (type : String)

256 |   -> (a -> Either String b)

257 |   -> ByteString

258 |   -> Either DecodeErr b

259 | refinedEither t f bs = Prelude.do

260 |   v <- mapFst (setType t) $ decodeAs a bs

261 |   mapFst (ReadErr t (toString bs)) (f v)

264 | refined :

265 |      {auto r  : Decode a}

266 |   -> (type    : String)

267 |   -> (details : Lazy String)

268 |   -> (a -> Maybe b)

269 |   -> ByteString

270 |   -> Either DecodeErr b

271 | refined t details f bs = Prelude.do

272 |   v <- mapFst (setType t) $ decodeAs a bs

273 |   case f v of

274 |     Nothing => Left $ ReadErr t (toString bs) details

275 |     Just x  => Right x

278 | bounded :

279 |      (0 a    : Type)

280 |   -> {auto r : Decode a}

281 |   -> {auto o : Ord a}

282 |   -> {auto c : Cast a b}

283 |   -> (type    : String)

284 |   -> (min,max : a)

285 |   -> ByteString

286 |   -> Either DecodeErr b

287 | bounded a t min max = refined t "Value out of bounds" $ \v =>

288 |   if (min <= v && v <= max) then Just (cast v) else Nothing

290 | export %inline

291 | Decode ByteString where decode = Right

293 | export %inline

294 | Decode String where decode = Right . toString

297 | Decode Nat where

298 |   decode (BS 0 _) = Left $ readErr "natural number" empty

299 |   decode bs =

300 |     if all isDigit bs

301 |        then Right (cast $ decimal bs)

302 |        else Left $ readErr "natural number" bs

305 | Decode Integer where

306 |   decode (BS 0 _) = Left $ readErr "integer" empty

307 |   decode bs@(BS (S k) bv) =

308 |     mapFst (setType "integer") $ case head bv of

309 |       45 => map (negate . cast) (decodeAs Nat (BS k $ tail bv))

310 |       _  => map cast $ decodeAs Nat bs

313 | Decode Bits8 where

314 |   decode = bounded Integer "unsigned integer" 0 0xff

317 | Decode Bits16 where

318 |   decode = bounded Integer "unsigned integer" 0 0xffff

321 | Decode Bits32 where

322 |   decode = bounded Integer "unsigned integer" 0 0xffff_ffff

325 | Decode Bits64 where

326 |   decode = bounded Integer "unsigned integer" 0 0xffff_ffff_ffff_ffff

329 | Decode Int8 where

330 |   decode = bounded Integer "integer" (-0x80) 0x7f

333 | Decode Int16 where

334 |   decode = bounded Integer "integer" (-0x8000) 0x7fff

337 | Decode Int32 where

338 |   decode = bounded Integer "integer" (-0x8000_0000) 0x7fff_ffff

341 | Decode Int64 where

342 |   decode = bounded Integer "integer" (-0x8000_0000_0000_0000) 0x7fff_ffff_ffff_ffff

345 | Decode Double where

346 |   decode bs =

347 |     case runBytes json bs of

348 |       Right (JDouble x)  => Right x

349 |       Right (JInteger x) => Right $ cast x

350 |       _                  => Left $ readErr "floating point number" bs

364 | decodeTest : (0 a : Type) -> Decode a => Show a => String -> IO ()

365 | decodeTest a =

366 |   either (putStrLn . interpolate) printLn . decodeAs a . fromString

376 | decodeManyTest : (0 a : Type) -> DecodeMany a => Show a => String -> IO ()

377 | decodeManyTest a s =

378 |   case parseURI Virtual (fromString s) of

379 |     Left err => putStrLn "\{err}"

380 |     Right u  => case decodeMany {a} u.path of

381 |       Right ([],v) => printLn v

382 |       Right (b::bs,v) => putStrLn "Only consumed up to \{b}: \{show v}"

383 |       Left x => putStrLn "\{x}"