
   0 | ||| Contain all the types of requests responses and how to interact with them
   1 | module Stellar.HTTP.Types
   2 | 
   3 | import Stellar.API
   4 | 
   5 | import public Data.Buffer
   6 | 
   7 | import TyTTP.HTTP
   8 | import public TyTTP.URL
   9 | 
  10 | import public System.Path
  11 | import System
  12 | import System.Utils
  13 | 
  14 | import public JSON.Simple.Derive
  15 | 
  16 | ------------------------------------------------------------------------------------
  17 | -- Richer types for URL and requests
  18 | ------------------------------------------------------------------------------------
  19 | ||| Well-formed URLs with a valid filesystem path and a list of query parameters
  20 | public export
  21 | WFURL : Type
  22 | WFURL = URL String System.Path.Path (List (String, String))
  23 | 
  24 | public export
  25 | allowsBody : Method -> Bool
  26 | allowsBody GET = False
  27 | allowsBody HEAD = False
  28 | allowsBody DELETE = False
  29 | allowsBody CONNECT = False
  30 | allowsBody _ = True
  31 | 
  32 | ||| The body of a request depending on the request method used
  33 | ||| TODO: remove body for HEAD , TRACE and OPTIONS
  34 | public export
  35 | DepBody : Method -> Type -> Type
  36 | DepBody m = if allowsBody m then id else const Unit
  37 | 
  38 | ||| A request with a well formed url and a dependent body
  39 | ||| The fields of `RichRequest` are private the fields are accessible
  40 | export
  41 | record RichRequest (bodyType : Type) where
  42 |   constructor MkRichReq
  43 |   method : Method
  44 |   url : WFURL
  45 |   version : Version
  46 |   headers : List (String, String)
  47 |   body : DepBody method bodyType
  48 | 
  49 | export
  50 | (.getBody') : RichRequest b -> Maybe b
  51 | (.getBody') (MkRichReq method url version headers body) with (allowsBody method )
  52 |   (.getBody') (MkRichReq method url version headers body) | True = Just body
  53 |   (.getBody') (MkRichReq method url version headers body) | False = Nothing
  54 | 
  55 | ||| Public constructor for `RichRequest`
  56 | export
  57 | MkRichRequest : {0 body : Type} -> (m : Method) -> WFURL -> Version -> List (String, String) -> DepBody m body -> RichRequest body
  58 | MkRichRequest = MkRichReq
  59 | 
  60 | ------------------------------------------------------------------------------------
  61 | -- Interface to deal with requests generically
  62 | ------------------------------------------------------------------------------------
  63 | 
  64 | ||| Interface for accessing headers of a request or response
  65 | public export
  66 | interface HasHeaders (0 t : Type) where
  67 |   (.headers) : t -> List (String, String)
  68 | 
  69 | ||| Interface for accessing http version of a request
  70 | public export
  71 | interface HasVersion (0 t : Type) where
  72 |   (.version) : t -> Version
  73 | 
  74 | ||| Interface for accessing the http method of a request
  75 | public export
  76 | interface HasMethod (0 t : Type) where
  77 |   (.method) : t -> Method
  78 | 
  79 | ||| Interface for accessing the body of a request or response
  80 | public export
  81 | interface HasBody (0 r : Type) (0 t : Type) | r where
  82 |   (.body) : r -> t
  83 | 
  84 | ||| Interface for accessing the url of a request
  85 | public export
  86 | interface HasURL (0 t : Type)  where
  87 |   (.url) : t -> WFURL
  88 | 
  89 | ------------------------------------------------------------------------------------
  90 | -- Basic implementations for requests and responses
  91 | ------------------------------------------------------------------------------------
  92 | 
  93 | ||| Requests have a version field
  94 | export
  95 | HasVersion (Request m u Version h b) where
  96 |   (.version) = Request.version
  97 | 
  98 | ||| Requests have a method field
  99 | export
 100 | HasMethod (Request Method u v h b) where
 101 |   (.method) = Request.method
 102 | 
 103 | ||| Requests have headers
 104 | export
 105 | HasHeaders (Request m u v (List (String, String)) b) where
 106 |   (.headers) = Request.headers
 107 | 
 108 | ||| Responses have headers
 109 | export
 110 | HasHeaders (Response v (List (String, String)) b) where
 111 |   (.headers) = Response.headers
 112 | 
 113 | ||| Responses have a body
 114 | export
 115 | HasBody (Response v h b) b where
 116 |   (.body) = Response.body
 117 | 
 118 | ||| Requests have a body
 119 | export
 120 | HasBody (Request m u v h b) b where
 121 |   (.body) = Request.body
 122 | 
 123 | export
 124 | HasURL (Request m WFURL v h b) where
 125 |   (.url) = Request.url
 126 | 
 127 | ||| Rich requests have headers
 128 | export
 129 | HasHeaders (RichRequest t) where
 130 |   (.headers) = RichRequest.headers
 131 | 
 132 | ||| Rich requests have an http version
 133 | export
 134 | HasVersion (RichRequest t) where
 135 |   (.version) = RichRequest.version
 136 | 
 137 | ||| Rich requests have an http method
 138 | export
 139 | HasMethod (RichRequest t) where
 140 |   (.method) = RichRequest.method
 141 | 
 142 | public export
 143 | HasURL (RichRequest t) where
 144 |   (.url) = RichRequest.url
 145 | 
 146 | %hide RichRequest.headers
 147 | %hide RichRequest.(.headers)
 148 | %hide RichRequest.method
 149 | %hide RichRequest.(.method)
 150 | %hide RichRequest.version
 151 | %hide RichRequest.(.version)
 152 | %hide RichRequest.url
 153 | %hide RichRequest.(.url)
 154 | %hide Request.(.headers)
 155 | %hide Request.headers
 156 | %hide Request.(.version)
 157 | %hide Request.version
 158 | %hide Request.(.method)
 159 | %hide Request.method
 160 | %hide Request.url
 161 | %hide Request.(.url)
 162 | 
 163 | ------------------------------------------------------------------------------------
 164 | -- we put this here so that the `.method` projection from the instance is used
 165 | -- otherwise this becomes unusable outside this module
 166 | 
 167 | ||| Given a rich GET request, coerce the type of its body to anything else
 168 | export
 169 | anyGet : (r : RichRequest t) -> (noBody : allowsBody r.method === False) => RichRequest s
 170 | anyGet (MkRichReq m url version headers body) = MkRichReq m url version headers (rewrite noBody in ())
 171 | 
 172 | ||| Obtain the body of a rich request, requires evidence that the method is _not_ a `GET` request
 173 | export
 174 | (.getBody) : (r : RichRequest t) -> (hasBody : allowsBody r.method  === True) => t
 175 | (.getBody) (MkRichReq method url version headers body) with (allowsBody method ) proof p
 176 |   (.getBody) (MkRichReq method url version headers body) | True = body
 177 |   (.getBody) (MkRichReq method url version headers body) | False = absurd hasBody
 178 | 
 179 | ------------------------------------------------------------------------------------
 180 | -- Different kinds of HTTP APIs
 181 | ------------------------------------------------------------------------------------
 182 | 
 183 | ||| The most generic kind of HTTP request using string headers
 184 | public export
 185 | GenericHttpResponse : Type -> Type
 186 | GenericHttpResponse = Response Status (List (String, String))
 187 | 
 188 | public export
 189 | PlainRequest : Type
 190 | PlainRequest = HttpRequest String (List (String, String)) Buffer
 191 | 
 192 | public export
 193 | PlainResponse : Type
 194 | PlainResponse = GenericHttpResponse Buffer
 195 | 
 196 | public export
 197 | JSONRequest : Type
 198 | JSONRequest = RichRequest JSON
 199 | 
 200 | ||| A JSON response might not contain a response body. For this, we use Maybe.
 201 | ||| A `Nothing` response body is an empty body
 202 | public export
 203 | JSONResponse : Type
 204 | JSONResponse = GenericHttpResponse (Maybe JSON)
 205 | 
 206 | namespace Canned
 207 |   export
 208 |   Ok : PlainResponse
 209 |   Ok = MkResponse OK [] emptyBuffer
 210 | 
 211 |   export
 212 |   Bad : PlainResponse
 213 |   Bad = MkResponse BAD_REQUEST [] emptyBuffer
 214 | 
 215 |   export
 216 |   BadJSON : JSONResponse
 217 |   BadJSON = MkResponse BAD_REQUEST [] Nothing
 218 | 
 219 | ||| The HTTP container that represents an http request and its matching http response
 220 | public export
 221 | PlainHTTP : API
 222 | PlainHTTP = PlainRequest :- PlainResponse
 223 | 
 224 | ||| The HTTP container that represents 1 http request and its matching http response
 225 | public export
 226 | RichHTTP : API
 227 | RichHTTP = RichRequest Buffer :- PlainResponse
 228 | 
 229 | ||| The API for requests and responses with JSON request body
 230 | public export
 231 | JSONHTTP : API
 232 | JSONHTTP = JSONRequest :- JSONResponse
 233 | 
 234 | public export
 235 | URLHttpRequest : Type -> Type
 236 | URLHttpRequest = HttpRequest WFURL (List (String, String))
 237 | 
 238 | ------------------------------------------------------------------------------------
 239 | -- Debuging interface and utilities
 240 | ------------------------------------------------------------------------------------
 241 | 
 242 | ||| A debug interface to avoid conflicting with `Show`.
 243 | public export
 244 | interface HTTPDebug (0 t : Type) where
 245 |   renderDebug : t -> String
 246 | 
 247 | ||| Byte buffers are converted into ascii strings and printed as is. If the data
 248 | ||| is not within ascii then we print garbage
 249 | export
 250 | HTTPDebug Buffer where
 251 |   renderDebug = bufferToStringUnsafe
 252 | 
 253 | ||| Well-formed url print everything about them using the default `Maybe` instances
 254 | export
 255 | HTTPDebug WFURL where
 256 |   renderDebug (MkURL host auth path params) = "\{show host}://\{show auth}\{show path}?\{show params}"
 257 | 
 258 | printHeaders : List (String, String) -> String
 259 | printHeaders headers = unlines (map (\(x, y) => "\{x}: \{y}") headers)
 260 | 
 261 | ||| Headers are printed as a list of `key: value`
 262 | export
 263 | HTTPDebug (List (String, String)) where
 264 |   renderDebug = printHeaders
 265 | 
 266 | export
 267 | HTTPDebug JSON where
 268 |   renderDebug = show
 269 | 
 270 | ||| For debug purposes we only print the code associated with the request status
 271 | export
 272 | HTTPDebug Status where
 273 |   renderDebug = show . (.code)
 274 | 
 275 | ||| strings are printed as-is
 276 | export
 277 | HTTPDebug String where
 278 |   renderDebug = id
 279 | 
 280 | ||| HttRequests can be printed provided the url, headers and body can be printed
 281 | export
 282 | HTTPDebug a => HTTPDebug b => HTTPDebug h => Show (HttpRequest a h b) where
 283 |   show (MkRequest method url version headers body) =
 284 |     """
 285 |       \{show method} \{renderDebug url} \{show version}
 286 |       --- headers:
 287 |       \{renderDebug headers}
 288 |       --- body:
 289 |       \{renderDebug body}
 290 |       """
 291 | 
 292 | ||| Generic responses can be printed provided the response body can be printed
 293 | export
 294 | HTTPDebug a => Show (GenericHttpResponse a) where
 295 |   show (MkResponse status headers body) =
 296 |     """
 297 |       \{show status.code}
 298 |       --- headers:
 299 |       \{printHeaders headers}
 300 |       --- body:
 301 |       \{renderDebug body}
 302 |       """
 303 |