
  0 | module HTTP.RequestErr
  1 | 
  2 | import Derive.Prelude
  3 | import HTTP.Status
  4 | import JSON.Simple
  5 | import JSON.Simple.Derive
  6 | 
  7 | %default total
  8 | %language ElabReflection
  9 | 
 10 | public export
 11 | record RequestErr where
 12 |   constructor RE
 13 |   status  : Bits16
 14 |   error   : String
 15 |   message : String
 16 |   details : String
 17 |   path    : String
 18 | 
 19 | %runElab derive "RequestErr" [Show,Eq,FromJSON,ToJSON]
 20 | 
 21 | export
 22 | requestErr : Status -> RequestErr
 23 | requestErr (MkStatus c e) = RE c e "" "" ""
 24 | 
 25 | export
 26 | requestErrMsg : String -> Status -> RequestErr
 27 | requestErrMsg m (MkStatus c e) = RE c e m "" ""
 28 | 
 29 | export
 30 | requestErrDetails : Interpolation a => a -> Status -> RequestErr
 31 | requestErrDetails v (MkStatus c e) = RE c e "" "\{v}" ""
 32 |