
   0 | module Web.Async.HTTP
   1 | 
   2 | import Data.Linear.Traverse1
   3 | import Derive.Prelude
   4 | import JSON.Simple
   5 | import Syntax.T1
   6 | import Web.Async.Util
   7 | import Web.Async.View
   8 | import Web.Internal.Types
   9 | 
  10 | %default total
  11 | %language ElabReflection
  12 | 
  13 | --------------------------------------------------------------------------------
  14 | --          FFI
  15 | --------------------------------------------------------------------------------
  16 | 
  17 | %foreign "browser:lambda:(x,a,b,w)=>x.append(a,b)"
  18 | prim__append : FormData -> String -> String -> PrimIO ()
  19 | 
  20 | 
  21 | %foreign "browser:lambda:(x,a,b,w)=>x.append(a,b)"
  22 | prim__appendBlob : FormData -> String -> Blob -> PrimIO ()
  23 | 
  24 | %foreign "browser:lambda:x=>x.responseText"
  25 | prim__responseText : XMLHttpRequest -> PrimIO String
  26 | 
  27 | %foreign "browser:lambda:x=>x.status"
  28 | prim__status : XMLHttpRequest -> PrimIO Bits16
  29 | 
  30 | %foreign "browser:lambda:(x,w)=>x.send()"
  31 | prim__send : XMLHttpRequest -> PrimIO ()
  32 | 
  33 | %foreign "browser:lambda:(x,s,w)=>x.send(s)"
  34 | prim__sendTxt : XMLHttpRequest -> String -> PrimIO ()
  35 | 
  36 | %foreign "browser:lambda:(w)=> new FormData()"
  37 | prim__newFD : PrimIO FormData
  38 | 
  39 | %foreign "browser:lambda:(x,s,w)=>x.send(s)"
  40 | prim__sendFD : XMLHttpRequest -> FormData -> PrimIO ()
  41 | 
  42 | %foreign "browser:lambda:(w)=> new XMLHttpRequest()"
  43 | prim__request : PrimIO XMLHttpRequest
  44 | 
  45 | %foreign "browser:lambda:(x,w)=>x.readyState"
  46 | prim__readyState : XMLHttpRequest -> PrimIO Bits16
  47 | 
  48 | %foreign "browser:lambda:(x,v,w)=>{x.timeout = v}"
  49 | prim__setTimeout : XMLHttpRequest -> Bits32 -> PrimIO ()
  50 | 
  51 | %foreign "browser:lambda:(x,w)=>x.abort()"
  52 | prim__abort : XMLHttpRequest -> PrimIO ()
  53 | 
  54 | %foreign "browser:lambda:(x,me,url,w)=>x.open(me,url)"
  55 | prim__open : XMLHttpRequest -> String -> String -> PrimIO ()
  56 | 
  57 | %foreign "browser:lambda:(x,a,b,w)=>x.setRequestHeader(a,b)"
  58 | prim__setRequestHeader : XMLHttpRequest -> (h,v : String) -> PrimIO ()
  59 | 
  60 | --------------------------------------------------------------------------------
  61 | --          Types
  62 | --------------------------------------------------------------------------------
  63 | 
  64 | ||| HTTP methods currently supported.
  65 | public export
  66 | data Method = GET | POST
  67 | 
  68 | %runElab derive "Method" [Show,Eq,Ord]
  69 | 
  70 | ||| A HTTP header is just a pair of strings.
  71 | public export
  72 | 0 Header : Type
  73 | Header = (String,String)
  74 | 
  75 | ||| Part in a formdata request.
  76 | public export
  77 | data Part : Type where
  78 |   StringPart : (name, value : String) -> Part
  79 |   FilePart   : (name : String) -> (file : File) -> Part
  80 | 
  81 | ||| Body of a HTTP request.
  82 | public export
  83 | data RequestBody : Type where
  84 |   Empty      : RequestBody
  85 |   StringBody : (mimeType : String) -> (content : String) -> RequestBody
  86 |   JSONBody   : {0 a : Type} -> ToJSON a => a -> RequestBody
  87 |   FormBody   : List Part -> RequestBody
  88 | 
  89 | ||| HTTP Errors
  90 | public export
  91 | data HTTPError : Type where
  92 |   Timeout      : HTTPError
  93 |   NetworkError : HTTPError
  94 |   BadStatus    : Bits16 -> HTTPError
  95 |   JSONError    : String -> DecodingErr -> HTTPError
  96 | 
  97 | ||| Type of expected respons.
  98 | |||
  99 | ||| Every constructor takes a function for wrapping a request
 100 | ||| result of type `Either HTTPError x` into the result type.
 101 | public export
 102 | data Expect : Type -> Type where
 103 |   ExpectJSON   : {0 a : _} -> FromJSON a => (Either HTTPError a -> r) -> Expect r
 104 |   ExpectString : (Either HTTPError String -> r) -> Expect r
 105 |   ExpectAny    : (Either HTTPError () -> r) -> Expect r
 106 | 
 107 | bodyHeaders : RequestBody -> List Header
 108 | bodyHeaders Empty            = []
 109 | bodyHeaders (StringBody m _) = [("Content-Type", m)]
 110 | bodyHeaders (JSONBody x)     = [("Content-Type", "application/json")]
 111 | bodyHeaders (FormBody x)     = []
 112 | 
 113 | append : FormData -> Part -> IO1 ()
 114 | append fd (StringPart name value) = ffi $ prim__append  fd name value
 115 | append fd (FilePart name file)    = ffi $ prim__appendBlob fd name (up file)
 116 | 
 117 | parameters {0 r    : Type}
 118 |            {auto s : Sink r}
 119 | 
 120 |   onerror : Expect r -> HTTPError -> Event -> IO1 ()
 121 |   onerror (ExpectJSON f)   err _ = s.sink1 (f $ Left err)
 122 |   onerror (ExpectString f) err _ = s.sink1 (f $ Left err)
 123 |   onerror (ExpectAny f)    err _ = s.sink1 (f $ Left err)
 124 | 
 125 |   onsuccess : Expect r -> XMLHttpRequest -> Event -> IO1 ()
 126 |   onsuccess (ExpectString f)   x _ = T1.do
 127 |     txt <- ffi (prim__responseText x)
 128 |     s.sink1 (f $ Right txt)
 129 |   onsuccess (ExpectAny f)      x _ = s.sink1 (f $ Right ())
 130 |   onsuccess (ExpectJSON {a} f) x _ = T1.do
 131 |     txt <- ffi (prim__responseText x)
 132 |     s.sink1 (f $ mapFst (JSONError txt) $ decode txt)
 133 | 
 134 |   onload : Expect r -> XMLHttpRequest -> Event -> IO1 ()
 135 |   onload exp x ev = T1.do
 136 |     st   <- ffi (prim__status x)
 137 |     case st >= 200 && st < 300 of
 138 |       False => onerror exp (BadStatus st) ev
 139 |       True  => onsuccess exp x ev
 140 | 
 141 |   xsend : RequestBody -> XMLHttpRequest -> IO1 ()
 142 |   xsend Empty            x = ffi (prim__send x)
 143 |   xsend (StringBody _ s) x = ffi (prim__sendTxt x s)
 144 |   xsend (JSONBody d)     x = ffi (prim__sendTxt x $ encode d)
 145 |   xsend (FormBody ps)    x = T1.do
 146 |     fd <- ffi $ prim__newFD
 147 |     traverse1_ (append fd) ps
 148 |     ffi $ prim__sendFD x fd
 149 | 
 150 |   ||| Sends a HTTP request.
 151 |   |||
 152 |   ||| Converts the response to an event of type `r`.
 153 |   export
 154 |   request :
 155 |        (method  : Method)
 156 |     -> (headers : List Header)
 157 |     -> (url     : String)
 158 |     -> (body    : RequestBody)
 159 |     -> (expect  : Expect r)
 160 |     -> (timeout : Maybe Bits32)
 161 |     -> IO1 (IO1 ())
 162 |   request m headers url body exp tout = T1.do
 163 |     -- create new Http request
 164 |     x <- ffi $ prim__request
 165 | 
 166 |     -- register event listeners
 167 |     addEventListener (up x) "error" $ onerror exp NetworkError
 168 |     addEventListener (up x) "load" $ onload exp x
 169 |     addEventListener (up x) "timeout" $ onerror exp Timeout
 170 | 
 171 |     -- open url
 172 |     ffi $ prim__open x (show m) url
 173 | 
 174 |     -- set message headers
 175 |     let hs := bodyHeaders body ++ headers
 176 |     for1_ hs $ \(n,h) => ffi $ prim__setRequestHeader x n h
 177 | 
 178 |     -- set timeout (if any)
 179 |     for1_ tout $ \v => ffi $ prim__setTimeout x v
 180 | 
 181 |     xsend body x
 182 |     pure (ffi $ prim__abort x)
 183 | 
 184 |   ||| Send a GET HTTP request.
 185 |   export %inline
 186 |   get : (url : String) -> (expect : Expect r) -> IO1 (IO1 ())
 187 |   get u e = request GET [] u Empty e Nothing
 188 | 
 189 |   ||| Send a GET request, reading the response as plain text.
 190 |   export %inline
 191 |   getText : (url : String) -> (f : Either HTTPError String -> r) -> IO1 (IO1 ())
 192 |   getText u = get u . ExpectString
 193 | 
 194 |   ||| Send a GET request, decoding the result as a JSON string
 195 |   ||| and converting it to the result type `a`.
 196 |   export %inline
 197 |   getJSON : FromJSON t => (url : String) -> (f : Either HTTPError t -> r) -> IO1 (IO1 ())
 198 |   getJSON u = get u . ExpectJSON
 199 | 
 200 |   ||| Send a POST request.
 201 |   export %inline
 202 |   post : (url : String) -> (body : RequestBody) -> (expect : Expect r) -> IO1 (IO1 ())
 203 |   post u b e = request POST [] u b e Nothing
 204 |