
  0 | module HTTP.API.Method
  1 | 
  2 | import public Data.Maybe0
  3 | import HTTP.Method
  4 | import HTTP.Status
  5 | 
  6 | ||| Data type describing the method (verb), response status code,
  7 | ||| as well as encoding formats and content type (if any) of a HTTP
  8 | ||| endpoint.
  9 | |||
 10 | ||| Please note that `format` and `result` refer to the format and
 11 | ||| type of the content in the server's *response* body.
 12 | |||
 13 | ||| See `HTTP.API.Content` for a way to describe format and content type
 14 | ||| in the HTTP *request* body.
 15 | public export
 16 | record ReqMethod where
 17 |   constructor M
 18 |   method    : Method
 19 |   status    : Status
 20 |   0 formats : List Type
 21 |   result  : Maybe0 Type
 22 | 
 23 | public export
 24 | 0 MethodResults : ReqMethod -> List Type
 25 | MethodResults (M _ _ _ $ Just0 t)  = [t]
 26 | MethodResults (M _ _ _ $ Nothing0) = []
 27 | 
 28 | public export
 29 | Get : (0 formats : List Type) -> (0 val : Type) -> ReqMethod
 30 | Get fs v = M GET ok200 fs (Just0 v)
 31 | 
 32 | public export
 33 | Post : (0 formats : List Type) -> (0 val : Type) -> ReqMethod
 34 | Post fs v = M POST ok200 fs (Just0 v)
 35 | 
 36 | public export
 37 | PostCreated : (0 formats : List Type) -> (0 val : Type) -> ReqMethod
 38 | PostCreated fs v = M POST created201 fs (Just0 v)
 39 | 
 40 | public export
 41 | Put : (0 formats : List Type) -> (0 val : Type) -> ReqMethod
 42 | Put fs v = M PUT ok200 fs (Just0 v)
 43 | 
 44 | public export
 45 | PutCreated : (0 formats : List Type) -> (0 val : Type) -> ReqMethod
 46 | PutCreated fs v = M PUT created201 fs (Just0 v)
 47 | 
 48 | public export
 49 | Patch : (0 formats : List Type) -> (0 val : Type) -> ReqMethod
 50 | Patch fs v = M PATCH ok200 fs (Just0 v)
 51 | 
 52 | public export
 53 | Head : ReqMethod
 54 | Head = M HEAD noContent204 [] Nothing0
 55 | 
 56 | public export
 57 | Delete : ReqMethod
 58 | Delete = M DELETE noContent204 [] Nothing0
 59 | 
 60 | public export
 61 | Post' : ReqMethod
 62 | Post' = M POST noContent204 [] Nothing0
 63 | 
 64 | public export
 65 | Put' : ReqMethod
 66 | Put' = M PUT noContent204 [] Nothing0
 67 | 
 68 | public export
 69 | Patch' : ReqMethod
 70 | Patch' = M PATCH noContent204 [] Nothing0
 71 |