
  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 | Interpolation RequestErr where
 23 |   interpolate (RE s e m d p) =
 24 |     """
 25 |     Error Details:
 26 |     status  : \{show s}
 27 |     error   : \{e}
 28 |     message : \{m}
 29 |     details : \{d}
 30 |     path    : \{p}
 31 |     """
 32 | 
 33 | export
 34 | requestErr : Status -> RequestErr
 35 | requestErr (MkStatus c e) = RE c e "" "" ""
 36 | 
 37 | export
 38 | requestErrMsg : String -> Status -> RequestErr
 39 | requestErrMsg m (MkStatus c e) = RE c e m "" ""
 40 | 
 41 | export
 42 | requestErrDetails : Interpolation a => a -> Status -> RequestErr
 43 | requestErrDetails v (MkStatus c e) = RE c e "" "\{v}" ""
 44 |