0 | module Web.MVC.Http
  1 |
  2 | import Control.Monad.Either.Extra
  3 | import Derive.Prelude
  4 | import JS
  5 | import JSON.Simple
  6 | import Web.Html
  7 | import Web.Raw.Xhr
  8 | import Web.MVC.Cmd
  9 |
 10 | %default total
 11 | %language ElabReflection
 12 |
 13 | --------------------------------------------------------------------------------
 14 | --          Utilities
 15 | --------------------------------------------------------------------------------
 16 |
 17 | export %inline
 18 | Cast String JS.ByteString.ByteString where
 19 |   cast = believe_me
 20 |
 21 | export %inline
 22 | Cast JS.ByteString.ByteString String where
 23 |   cast = believe_me
 24 |
 25 | --------------------------------------------------------------------------------
 26 | --          Types
 27 | --------------------------------------------------------------------------------
 28 |
 29 | ||| HTTP methods currently supported.
 30 | public export
 31 | data Method = GET | POST
 32 |
 33 | %runElab derive "Method" [Show,Eq,Ord]
 34 |
 35 | ||| A HTTP header is just a pair of strings.
 36 | public export
 37 | 0 Header : Type
 38 | Header = (String,String)
 39 |
 40 | ||| Part in a formdata request.
 41 | public export
 42 | data Part : Type where
 43 |   StringPart : (name, value : String) -> Part
 44 |   FilePart   : (name : String) -> (file : File) -> Part
 45 |
 46 | ||| Body of a HTTP request.
 47 | public export
 48 | data RequestBody : Type where
 49 |   Empty      : RequestBody
 50 |   StringBody : (mimeType : String) -> (content : String) -> RequestBody
 51 |   JSONBody   : ToJSON a => a -> RequestBody
 52 |   FormBody   : List Part -> RequestBody
 53 |
 54 | ||| HTTP Errors
 55 | public export
 56 | data HTTPError : Type where
 57 |   Timeout      : HTTPError
 58 |   NetworkError : HTTPError
 59 |   BadStatus    : Bits16 -> HTTPError
 60 |   JSONError    : String -> DecodingErr -> HTTPError
 61 |
 62 | ||| Type of expected respons.
 63 | |||
 64 | ||| Every constructor takes a function for wrapping a request
 65 | ||| result of type `Either HTTPError x` into the result type.
 66 | public export
 67 | data Expect : Type -> Type where
 68 |   ExpectJSON   : FromJSON a => (Either HTTPError a -> r) -> Expect r
 69 |   ExpectString : (Either HTTPError String -> r) -> Expect r
 70 |   ExpectAny    : (Either HTTPError () -> r) -> Expect r
 71 |
 72 | bodyHeaders : RequestBody -> List Header
 73 | bodyHeaders Empty            = []
 74 | bodyHeaders (StringBody m _) = [("Content-Type", m)]
 75 | bodyHeaders (JSONBody x)     = [("Content-Type", "application/json")]
 76 | bodyHeaders (FormBody x)     = []
 77 |
 78 | append : FormData -> Part -> JSIO ()
 79 | append fd (StringPart name value) = FormData.append  fd name value
 80 | append fd (FilePart name file)    = FormData.append1 fd name file
 81 |
 82 | parameters {0 r    : Type}
 83 |
 84 |   onerror : (r -> JSIO ()) -> Expect r -> HTTPError -> JSIO ()
 85 |   onerror h (ExpectJSON f)   err = h (f $ Left err)
 86 |   onerror h (ExpectString f) err = h (f $ Left err)
 87 |   onerror h (ExpectAny f)    err = h (f $ Left err)
 88 |
 89 |   onsuccess : (r -> JSIO ()) -> Expect r -> XMLHttpRequest -> JSIO ()
 90 |   onsuccess h (ExpectString f)   x = responseText x >>= h . f . Right
 91 |   onsuccess h (ExpectAny f)      x = h (f $ Right ())
 92 |   onsuccess h (ExpectJSON {a} f) x = do
 93 |     s <- responseText x
 94 |     h . f . mapFst (JSONError s) $ decode s
 95 |
 96 |   onload : (r -> JSIO ()) -> Expect r -> XMLHttpRequest -> JSIO ()
 97 |   onload h exp x = do
 98 |     st   <- status x
 99 |     case st >= 200 && st < 300 of
100 |       False => onerror h exp (BadStatus st)
101 |       True  => onsuccess h exp x
102 |
103 |   xsend : RequestBody -> XMLHttpRequest -> JSIO ()
104 |   xsend Empty            x = XMLHttpRequest.send x
105 |   xsend (StringBody _ s) x = XMLHttpRequest.send' x (Def . Just $ inject s)
106 |   xsend (JSONBody d)     x = XMLHttpRequest.send' x (Def . Just $ inject $ encode d)
107 |   xsend (FormBody ps)    x = do
108 |     fd <- FormData.new
109 |     traverseList_ (append fd) ps
110 |     XMLHttpRequest.send' x (Def . Just $ inject fd)
111 |
112 |   ||| Sends a HTTP request.
113 |   |||
114 |   ||| Converts the response to an event of type `r`.
115 |   export
116 |   request :
117 |        (method  : Method)
118 |     -> (headers : List Header)
119 |     -> (url     : String)
120 |     -> (body    : RequestBody)
121 |     -> (expect  : Expect r)
122 |     -> (timeout : Maybe Bits32)
123 |     -> Cmd r
124 |   request m headers url body exp tout = C $ \h => Prelude.do
125 |     -- create new Http request
126 |     x <- XMLHttpRequest.new
127 |
128 |     -- register event listeners
129 |     XMLHttpRequestEventTarget.onerror x ?> onerror h exp NetworkError
130 |     XMLHttpRequestEventTarget.onload x ?> onload h exp x
131 |     XMLHttpRequestEventTarget.ontimeout x ?> onerror h exp Timeout
132 |
133 |     -- open url
134 |     open_ x (cast $ show m) url
135 |
136 |     -- set message headers
137 |     let hs := bodyHeaders body ++ headers
138 |     traverseList_ (\(n,h) => setRequestHeader x (cast n) (cast h)) hs
139 |
140 |     -- set timeout (if any)
141 |     traverse_ (set (timeout x)) tout
142 |
143 |     -- send request
144 |     xsend body x
145 |
146 | ||| Send a GET HTTP request.
147 | export %inline
148 | get : (url : String) -> (expect : Expect r) -> Cmd r
149 | get u e = request GET [] u Empty e Nothing
150 |
151 | ||| Send a GET request, reading the response as plain text.
152 | export %inline
153 | getText : (url : String) -> (f : Either HTTPError String -> r) -> Cmd r
154 | getText u = get u . ExpectString
155 |
156 | ||| Send a GET request, decoding the result as a JSON string
157 | ||| and converting it to the result type `a`.
158 | export %inline
159 | getJSON : FromJSON a => (url : String) -> (f : Either HTTPError a -> r) -> Cmd r
160 | getJSON u = get u . ExpectJSON
161 |
162 | ||| Send a POST request.
163 | export %inline
164 | post : (url : String) -> (body : RequestBody) -> (expect : Expect r) -> Cmd r
165 | post u b e = request POST [] u b e Nothing
166 |