
   0 | module Stellar.HTTP.DSL
   1 | 
   2 | import public Data.Buffer
   3 | import Data.DPair
   4 | import Data.Either
   5 | import Data.Maybe.Any
   6 | import Data.String
   7 | import Data.List1
   8 | import Stellar.API
   9 | import Stellar.API.Interface
  10 | import public Stellar.API.Maybe
  11 | import Stellar.API.Morphism
  12 | import Stellar.API.Maybe as Bi
  13 | import Stellar.HTTP.Types
  14 | 
  15 | import public JSON.Simple.Derive
  16 | 
  17 | import TyTTP
  18 | import TyTTP.HTTP
  19 | import TyTTP.HTTP.Protocol
  20 | import TyTTP.URL
  21 | import TyTTP.Adapter.Node.HTTP
  22 | 
  23 | import System
  24 | import System.Utils
  25 | import System.Path
  26 | 
  27 | import Decidable.Equality
  28 | import Debug.Trace
  29 | 
  30 | %hide Control.Category.Category
  31 | %hide Control.Category.(.)
  32 | %hide IPCOptions.path
  33 | 
  34 | export
  35 | fromBool : Bool -> Maybe ()
  36 | fromBool True = Just ()
  37 | fromBool False = Nothing
  38 | 
  39 | ------------------------------------------------------------------------------------
  40 | -- DSL primitives for parsable data
  41 | ------------------------------------------------------------------------------------
  42 | 
  43 | public export
  44 | interface Parsable t where
  45 |   parse : String -> Maybe t
  46 | 
  47 | public export
  48 | Parsable Int where
  49 |   parse = Prelude.map cast . parseInteger
  50 | 
  51 | public export
  52 | Parsable Integer where
  53 |   parse = parseInteger
  54 | 
  55 | public export
  56 | Parsable Nat where
  57 |   parse = Prelude.map cast . parseInteger
  58 | 
  59 | public export
  60 | Parsable String where
  61 |   parse = Just
  62 | 
  63 | public export
  64 | interface Serializable t where
  65 |   -- IO effect is just for memory allocation of the buffer
  66 |   toBuffer : t -> IO (Int, Buffer)
  67 | 
  68 | export
  69 | Serializable () where
  70 |   toBuffer _ = newBuffer 0 >>= \case Just x => pure (0, x)
  71 |                                      Nothing => die "could not allocate empty buffer"
  72 | 
  73 | export
  74 | Serializable String where
  75 |   toBuffer x = do
  76 |     let len = stringByteLength x
  77 |     (Just buf) <- newBuffer len
  78 |       | Nothing => die "could not allocate string buffer of size \{show len}"
  79 |     setString buf 0 x
  80 |     pure (len, buf)
  81 | 
  82 | export
  83 | Serializable JSON where
  84 |   toBuffer x = toBuffer {t = String} (show x)
  85 | 
  86 | export
  87 | [SerialiseToJSON] ToJSON a => Serializable a where
  88 |   toBuffer x = toBuffer {t = JSON} (toJSON x)
  89 | 
  90 | public export
  91 | interface Deserializable t where
  92 |   fromBuffer : Buffer -> Maybe t
  93 | 
  94 | export
  95 | Deserializable String where
  96 |   fromBuffer = Just . bufferToStringUnsafe
  97 | 
  98 | export
  99 | Deserializable JSON where
 100 |   fromBuffer = fromBuffer {t = String} >=> eitherToMaybe . parseJSON Virtual
 101 | 
 102 | export
 103 | [DeserializeJSON] FromJSON t => Deserializable t where
 104 |   fromBuffer = decodeMaybe . bufferToStringUnsafe
 105 | 
 106 | public export
 107 | record NameTy where
 108 |   constructor (:>)
 109 |   name : String
 110 |   ty : Type
 111 |   {auto p : Parsable ty}
 112 | 
 113 | public export
 114 | data ParsableQueryParam : Type where
 115 |   Nil : ParsableQueryParam
 116 |   (::) : NameTy -> ParsableQueryParam -> ParsableQueryParam
 117 | 
 118 | public export
 119 | QueryType : ParsableQueryParam -> List Type
 120 | QueryType Nil = []
 121 | QueryType ((nm :> ty) :: res) = ty :: QueryType res
 122 | 
 123 | public export
 124 | data ContentType
 125 |   = JSON
 126 |   | Plain
 127 |   | PDF
 128 | 
 129 | printContentType : ContentType -> String
 130 | printContentType JSON = "application/json"
 131 | printContentType Plain = "text/plain"
 132 | printContentType PDF = "application/pdf"
 133 | 
 134 | fromContentType : ContentType -> Type
 135 | fromContentType JSON = JSON.Parser.JSON
 136 | fromContentType Plain = String
 137 | fromContentType PDF = String -- incorrect but that will do for the demo should probably be Buffer or something
 138 | 
 139 | public export
 140 | interface RequestParser (0 c : API) where
 141 |   constructor MkRequestParser
 142 |   parseReq  : PlainRequest -> Either String c.message
 143 |   mkRes : (inp : c.message) -> c.response inp -> IO PlainResponse
 144 | 
 145 | parseSearch : String -> SimpleSearch
 146 | parseSearch = parseSkipQuestionMarks . unpack
 147 |   where
 148 |     parse : List Char -> SimpleSearch
 149 |     parse [] = []
 150 |     parse xs =
 151 |       let sections = splitOn '&' xs
 152 |           params = break (== '=') <$> List.filter (not . null) (forget sections)
 153 |       in
 154 |         Prelude.bimap pack (pack . fromMaybe [] . tail') <$> params
 155 | 
 156 |     parseSkipQuestionMarks : List Char -> SimpleSearch
 157 |     parseSkipQuestionMarks [] = []
 158 |     parseSkipQuestionMarks ('?'::xs) = parseSkipQuestionMarks xs
 159 |     parseSkipQuestionMarks a@(x::xs) = parse a
 160 | 
 161 | parseURL : String -> Either String (URL String System.Path.Path (List (String, String)))
 162 | parseURL url = do
 163 |   url <- mapFst printErr (Simple.parse url)
 164 |   let pp = URL.path url
 165 |   let qry = parseSearch url.search
 166 |   path <- maybeToEither "could not parse path \{pp}" (Path.tryParse pp)
 167 |   pure ({path := path, search := qry} url)
 168 |   where
 169 |     printErr : URLParserError -> String
 170 |     printErr EmptyString = "Could not parse path, string is empty"
 171 |     printErr MissingAuthorityOrPath = "Could not parse path, missing authority or path"
 172 | 
 173 | ||| Lookup a value and pop the found key-value pair from the list if it is present
 174 | lookupPop : Eq a => List (a, b) -> {default [] acc : List (a, b)} -> a -> Maybe (b, List (a, b))
 175 | lookupPop [] v = Nothing
 176 | lookupPop ((x, y) :: xs) v
 177 |   = if x == v
 178 |        then Just (y, reverse acc ++ xs)
 179 |        else lookupPop xs {acc = (x, y) :: acc} v
 180 | 
 181 | 
 182 | ------------------------------------------------------------------------------------
 183 | -- Request parsing
 184 | ------------------------------------------------------------------------------------
 185 | %hide Request.(.url)
 186 | 
 187 | ||| A helper to parse a GET request given a function that parses the URL and the request body
 188 | export
 189 | parseGeneric : (tj : ToJSON t) => (fj : FromJSON argBody) =>
 190 |                (m : Method) -> (matchURL : WFURL -> Maybe argURL) ->
 191 |                (argURL -> DepBody m argBody -> finalResult) ->
 192 |                JSONHTTP =&> Any.Maybe (finalResult :- t)
 193 | parseGeneric method matchURL finalise =
 194 |   !! \x => case matchRequest x of
 195 |                 Just val => Just val ## (\json => MkResponse OK [] (Just $ toJSON {a = t} (extract json)))
 196 |                 Nothing => Nothing ## absurd
 197 |   where
 198 |     matchRequest : RichRequest JSON -> Maybe finalResult
 199 |     matchRequest req with (allowsBody method ) proof q | (allowsBody req.method) proof p
 200 |       matchRequest req | True | True = do
 201 |         let True = method == req.method
 202 |           | False => trace "expected method \{show method}, but this request has method \{show req.method}" Nothing
 203 |         urlArg <- matchURL req.url
 204 |         let (Just bodyArg) = eitherToMaybe $ fromJSON @{fj} req.getBody
 205 |           | Nothing => trace "could not parse json \{show req.getBody}" Nothing
 206 |         pure (finalise urlArg (rewrite q in bodyArg))
 207 |       matchRequest req | False | False = do
 208 |         urlArg <- matchURL req.url
 209 |         pure (finalise urlArg (rewrite q in ()))
 210 |       matchRequest req | _ | _ = Nothing
 211 | 
 212 | ||| A helper to parse a GET request given a function that parses the URL and the body
 213 | export
 214 | parsePost : (tj : ToJSON t) => FromJSON argBody =>
 215 |             (matchURL : WFURL -> Maybe argURL) ->
 216 |             (finalise : argURL -> argBody -> finalResult) ->
 217 |             JSONHTTP =&> Any.Maybe (finalResult :- t)
 218 | parsePost = parseGeneric POST
 219 | 
 220 | ||| A helper to parse a GET request given a function that matches the URL and parses the body from JSON
 221 | export
 222 | parsePost' : (tj : ToJSON t) => FromJSON argBody =>
 223 |              (matchURL : WFURL -> Bool) ->
 224 |              JSONHTTP =&> Any.Maybe (argBody :- t)
 225 | parsePost' matchURL = parseGeneric {argBody, finalResult = argBody} POST (fromBool . matchURL) (const id)
 226 | 
 227 | ||| A helper to parse a GET request given a function that parses the URL and the body
 228 | export
 229 | parsePut : (tj : ToJSON t) => FromJSON argBody =>
 230 |            (matchURL : WFURL -> Maybe argURL) ->
 231 |             (finalise : argURL -> argBody -> finalResult) ->
 232 |            JSONHTTP =&> Any.Maybe (finalResult :- t)
 233 | parsePut = parseGeneric PUT
 234 | 
 235 | ||| A helper to parse a GET request given a function that matches the URL and parses the body from JSON
 236 | export
 237 | parsePut' : (tj : ToJSON t) => FromJSON argBody =>
 238 |            (matchURL : WFURL -> Bool) ->
 239 |            JSONHTTP =&> Any.Maybe (argBody :- t)
 240 | parsePut' matchURL = parseGeneric {argBody, finalResult = argBody} PUT (fromBool . matchURL) (const id)
 241 | 
 242 | ||| A helper to parse a GET request given a function that matches the URL and parses the body from JSON
 243 | export
 244 | parseDelete : (tj : ToJSON t) => FromJSON argBody =>
 245 |               (matchURL : WFURL -> Maybe argURL) ->
 246 |               JSONHTTP =&> Any.Maybe (argURL :- t)
 247 | parseDelete matchURL = parseGeneric DELETE {argBody = ()} matchURL const
 248 | 
 249 | ||| A helper to parse a GET request given a function that parses the URL
 250 | export
 251 | parseGet : forall arg. (tj : ToJSON t) => (matchURL : WFURL -> Maybe arg) -> JSONHTTP =&> Any.Maybe (arg :- t)
 252 | parseGet matchURL = parseGeneric {argBody = ()} GET matchURL const
 253 | 
 254 | ||| A helper to parse a GET request given a function that matches on the URL
 255 | export
 256 | parseGet' : (tj : ToJSON t) => FromJSON argBody =>
 257 |             (matchURL : WFURL -> Bool) ->
 258 |             JSONHTTP =&> Any.Maybe (() :- t)
 259 | parseGet' matchURL = parseGeneric {argBody = (), finalResult = ()} GET (fromBool . matchURL) (const id)
 260 | 
 261 | ||| Root of the file system "/".
 262 | export
 263 | rootPath : System.Path.Path
 264 | rootPath = MkPath Nothing True [] False
 265 | 
 266 | export
 267 | isRoot : WFURL -> Bool
 268 | isRoot url = url.path == rootPath
 269 | 
 270 | export
 271 | parsePath : System.Path.Path -> WFURL -> Bool
 272 | parsePath path url = url.path == path
 273 | 
 274 | ------------------------------------------------------------------------------------
 275 | -- convert HTTP request/responses
 276 | ------------------------------------------------------------------------------------
 277 | 
 278 | ||| parse the URL of an HTTP request into its own URL type for further analysis
 279 | export
 280 | asURL : PlainHTTP =&> Any.Maybe RichHTTP
 281 | asURL = !! \x => case fwd x of
 282 |                       Just req => Just req ## extract
 283 |                       Nothing => Nothing ## absurd
 284 |   where
 285 |     fwd : PlainRequest -> Maybe (RichRequest Buffer)
 286 |     fwd (MkRequest m url version headers body) with (allowsBody m ) proof p
 287 |       fwd (MkRequest m url version headers body) | False = do
 288 |         newURL <- eitherToMaybe (parseURL url)
 289 |         pure $ MkRichRequest GET newURL version headers ()
 290 |       fwd (MkRequest m url version headers body) | True = do
 291 |         newURL <- eitherToMaybe (parseURL url)
 292 |         pure $ MkRichRequest m newURL version headers (rewrite p in body)
 293 | 
 294 | ||| Ensures a request has a specific header
 295 | ||| Returns the request if it does, returns `Nothign` otherwise
 296 | export
 297 | hasHeader : (String, String) -> RichRequest b -> Maybe (RichRequest b)
 298 | hasHeader header y = if header `elem` y.headers
 299 |                         then Just y
 300 |                         else Nothing
 301 | 
 302 | ||| Parse a request body as JSON, does not check for `content-type=application/json`
 303 | export
 304 | hasJSONBody : RichRequest Buffer -> Maybe (RichRequest JSON)
 305 | hasJSONBody r with (allowsBody r.method) proof p
 306 |   hasJSONBody r | True =
 307 |     case fromBuffer (r.getBody {hasBody = p}) of
 308 |          Nothing => trace "could not parse json body" Nothing
 309 |          Just parsed => pure $ MkRichRequest r.method r.url r.version r.headers (rewrite p in parsed)
 310 |   hasJSONBody r | False = Just (anyGet r {noBody = p})
 311 | 
 312 | ||| Parse a request body as JSON, does not check for `content-type=application/json`
 313 | export
 314 | parseJSONBody : FromJSON a => RichRequest Buffer -> Maybe (RichRequest a)
 315 | parseJSONBody r with (allowsBody r.method) proof p
 316 |   parseJSONBody r | True =
 317 |     case fromBuffer @{DeserializeJSON} (r.getBody {hasBody = p}) of
 318 |          Nothing => trace "could not parse json body" Nothing
 319 |          Just parsed => pure $ MkRichRequest r.method r.url r.version r.headers (rewrite p in parsed)
 320 |   parseJSONBody r | False = Just (anyGet r {noBody = p})
 321 | 
 322 | ||| Parses a request body as JSON, checks for `content-type=application/json`
 323 | export
 324 | hasJSONBodyContentType : RichRequest Buffer -> Maybe (RichRequest JSON)
 325 | hasJSONBodyContentType = hasJSONBody >=> hasHeader ("content-type" , "application/json")
 326 | 
 327 | %hide TyTTP.Core.Response.Response.(.body)
 328 | 
 329 | 
 330 | 
 331 | namespace CheckHeader
 332 |   ||| Convert the request body into JSON. Checks for content-type: application/json header
 333 |   export
 334 |   asJSON : RichHTTP =&> Any.Maybe JSONHTTP
 335 |   asJSON = !! \x => case hasJSONBodyContentType x of
 336 |                          Just y => Just y ##  \x => map (maybe emptyBuffer (Builtin.snd . unsafePerformIO . toBuffer)) (extract x)
 337 |                          Nothing => Nothing ## absurd
 338 | 
 339 |   ||| Convert all requests and responses are ones that manipulate JSON
 340 |   export
 341 |   httpJSON : PlainHTTP =&> Any.Maybe JSONHTTP
 342 |   httpJSON = Interface.(>=>) {f = Any.Maybe, c = JSONHTTP} asURL CheckHeader.asJSON
 343 | 
 344 |   ||| Return bad request if the request could not be parsed
 345 |   export
 346 |   httpJSONBody : PlainHTTP =&> All.Maybe JSONHTTP
 347 |   httpJSONBody = AnyToAll {a = PlainHTTP, b = JSONHTTP} (const Bad) httpJSON
 348 | 
 349 |   ||| Convert an execution for JSON-bodied requests to general HTTP requests
 350 |   export
 351 |   execJSON : Costate (IO $- JSONHTTP) -> Costate (IO $- PlainHTTP)
 352 |   execJSON m
 353 |       = map_Lift {a = PlainHTTP, b = All.Maybe JSONHTTP} CheckHeader.httpJSONBody
 354 |       |&> distribMaybe {a = JSONHTTP}
 355 |       |&> map_Maybe {a = IO $- JSONHTTP, b = End} m
 356 |       |&> maybeEnd
 357 | 
 358 | namespace NoCheck
 359 |   ||| Convert the request body into a JSON value, do not check for content-type header
 360 |   export
 361 |   asJSON : RichHTTP =&> Any.Maybe JSONHTTP
 362 |   asJSON = !! \x => case hasJSONBody x of
 363 |                          Nothing => Nothing ## absurd
 364 |                          Just json => Just json ## \vx =>
 365 |                                      map (maybe emptyBuffer (Builtin.snd . unsafePerformIO . toBuffer)) (extract vx)
 366 | 
 367 |   ||| Convert all requests and responses are ones that manipulate JSON, does not check for content-type header
 368 |   export
 369 |   httpJSON : PlainHTTP =&> Any.Maybe JSONHTTP
 370 |   httpJSON = Interface.(>=>) {f = Any.Maybe, c = JSONHTTP} asURL NoCheck.asJSON
 371 | 
 372 |   ||| Return bad request if the request could not be parsed
 373 |   export
 374 |   httpJSONBody : PlainHTTP =&> All.Maybe JSONHTTP
 375 |   httpJSONBody = AnyToAll {a = PlainHTTP, b = JSONHTTP} (const Bad) NoCheck.httpJSON
 376 | 
 377 |   ||| Convert an execution for JSON-bodied requests to general HTTP requests
 378 |   export
 379 |   execJSON : Costate (IO $- JSONHTTP) -> Costate (IO $- PlainHTTP)
 380 |   execJSON m
 381 |       = map_Lift {a = PlainHTTP, b = All.Maybe JSONHTTP} NoCheck.httpJSONBody
 382 |       |&> distribMaybe {a = JSONHTTP}
 383 |       |&> map_Maybe {a = IO $- JSONHTTP, b = End} m
 384 |       |&> maybeEnd
 385 | 
 386 | namespace Generic
 387 |   parameters {0 a : Type} {0 b : Type} {auto frjson : FromJSON a} {auto tojson : ToJSON b}
 388 | 
 389 |     public export 0
 390 |     GenHTTP : API
 391 |     GenHTTP = (RichRequest a :- GenericHttpResponse (Maybe b))
 392 | 
 393 |     ||| Convert the request body into a JSON value, do not check for content-type header
 394 |     export
 395 |     asJSON : RichHTTP =&> Any.Maybe GenHTTP
 396 |     asJSON = !! \x => case parseJSONBody {a} x of
 397 |                            Nothing => Nothing ## absurd
 398 |                            Just json => Just json ## \vx =>
 399 |                                        let ix = extract vx
 400 |                                        in map (maybe emptyBuffer (\xx => Builtin.snd $ unsafePerformIO $ toBuffer @{SerialiseToJSON} xx)) ix
 401 | 
 402 |     ||| Convert all requests and responses are ones that manipulate JSON, does not check for content-type header
 403 |     export
 404 |     httpJSON : PlainHTTP =&> Any.Maybe GenHTTP
 405 |     httpJSON = Interface.(>=>) {f = Any.Maybe, c = GenHTTP} asURL Generic.asJSON
 406 | 
 407 |     ||| Return bad request if the request could not be parsed
 408 |     export
 409 |     httpJSONBody : PlainHTTP =&> All.Maybe GenHTTP
 410 |     httpJSONBody = AnyToAll {a = PlainHTTP, b = GenHTTP} (const Bad) Generic.httpJSON
 411 | 
 412 |     ||| Convert an execution for JSON-bodied requests to general HTTP requests
 413 |     export
 414 |     execJSON : Costate (IO $- GenHTTP) -> Costate (IO $- PlainHTTP)
 415 |     execJSON m
 416 |         = map_Lift {a = PlainHTTP, b = All.Maybe GenHTTP} Generic.httpJSONBody
 417 |         |&> distribMaybe {a = GenHTTP}
 418 |         |&> map_Maybe {a = IO $- GenHTTP, b = End} m
 419 |         |&> maybeEnd
 420 |