0 | module HTTP.API.Decode
  1 |
  2 | import Data.List.Quantifiers as L
  3 | import Derive.Prelude
  4 | import HTTP.FormData
  5 | import HTTP.Header.Types
  6 | import HTTP.RequestErr
  7 | import HTTP.Status
  8 | import HTTP.URI
  9 | import JSON.Simple
 10 | import JSON.Simple.Derive
 11 |
 12 | %default total
 13 | %language ElabReflection
 14 |
 15 | ||| Error type that occurs when decoding a value or other piece of
 16 | ||| information.
 17 | public export
 18 | data DecodeErr : Type where
 19 |   ||| A `ReadErr` typically occurs when reading a single value
 20 |   ||| from a string or bytestring.
 21 |   |||
 22 |   ||| @type    : String description of the type we tried to read
 23 |   ||| @value   : The string from which the value should be read
 24 |   ||| @details : Additional information about why reading the value failed.
 25 |   ReadErr    : (type, value : String) -> (details : String) -> DecodeErr
 26 |
 27 |   ||| A `ContentErr` is - in general - a more technical error that happend
 28 |   ||| when parsing the body of a message. The `details` field typically
 29 |   ||| holds the detailed description from the parser about what went
 30 |   ||| actually wrong.
 31 |   ContentErr : (type : String) -> (details : String) -> DecodeErr
 32 |
 33 |   ||| An arbitrary custom error message.
 34 |   Msg        : (message : String) -> DecodeErr
 35 |
 36 | %runElab derive "DecodeErr" [Show,Eq,FromJSON,ToJSON]
 37 |
 38 | ||| Utility constructor for `ReadErr`.
 39 | export %inline
 40 | readErr : (type : String) -> (value : ByteString) -> DecodeErr
 41 | readErr type value = ReadErr type (toString value) ""
 42 |
 43 | ||| Utility constructor for `ContentErr`.
 44 | export %inline
 45 | contentErr : (type : String) -> Interpolation a => a -> DecodeErr
 46 | contentErr type = ContentErr type . interpolate
 47 |
 48 | ||| Adjusts the `type` field of a decode error.
 49 | export
 50 | setType : String -> DecodeErr -> DecodeErr
 51 | setType t (ReadErr _ v d)  = ReadErr t v d
 52 | setType t (ContentErr _ d) = ContentErr t d
 53 | setType t (Msg m)          = Msg m
 54 |
 55 | ||| Adjusts the `type` field of a decode error.
 56 | export
 57 | setValue : String -> DecodeErr -> DecodeErr
 58 | setValue v (ReadErr t _ d)  = ReadErr t v d
 59 | setValue _ err              = err
 60 |
 61 | ||| Adjusts the `message` or `details` field of a decode error.
 62 | export
 63 | modMsg : (String -> String) -> DecodeErr -> DecodeErr
 64 | modMsg f (ReadErr t v d)  = ReadErr t v (f d)
 65 | modMsg f (ContentErr t d) = ContentErr t (f d)
 66 | modMsg f (Msg m)          = Msg (f m)
 67 |
 68 | --------------------------------------------------------------------------------
 69 | -- Decode Interface
 70 | --------------------------------------------------------------------------------
 71 |
 72 | ||| An interface for decoding value from a sequence of raw bytes.
 73 | public export
 74 | interface Decode (0 a : Type) where
 75 |   decode : ByteString -> Either DecodeErr a
 76 |
 77 | ||| Utiliy alias for `decode` that allows to explicitly specify the
 78 | ||| target type.
 79 | public export %inline
 80 | decodeAs : (0 a : Type) -> Decode a => ByteString -> Either DecodeErr a
 81 | decodeAs _ = decode
 82 |
 83 | ||| An interface for decoding values by reading a prefix
 84 | ||| of a list of bytestrings such as a path in a URL.
 85 | public export
 86 | interface DecodeMany (0 a : Type) where
 87 |   simulateDecode : List ByteString -> Maybe (List ByteString)
 88 |
 89 |   decodeMany : List ByteString -> Either DecodeErr (List ByteString, a)
 90 |
 91 | export
 92 | Decode a => DecodeMany a where
 93 |   simulateDecode []      = Nothing
 94 |   simulateDecode (b::bs) = Just bs
 95 |
 96 |   decodeMany []      = Left (Msg "Unexpected end of URL path")
 97 |   decodeMany (b::bs) = (bs,) <$> decode b
 98 |
 99 | export
100 | decodeAll :
101 |      SnocList a
102 |   -> Decode a
103 |   -> List ByteString
104 |   -> Either DecodeErr (List ByteString,SnocList a)
105 | decodeAll sx d []        = Right ([],sx)
106 | decodeAll sx d (x :: xs) =
107 |   case decode @{d} x of
108 |     Right v  => decodeAll (sx:<v) d xs
109 |     Left err => Left err
110 |
111 | export
112 | Decode a => DecodeMany (SnocList a) where
113 |   simulateDecode bs = Just []
114 |   decodeMany = decodeAll [<] %search
115 |
116 | export
117 | Decode a => DecodeMany (List a) where
118 |   simulateDecode bs = Just []
119 |   decodeMany bs = map (<>> []) <$> decodeAll [<] %search bs
120 |
121 | simulateHL :
122 |      L.All.All (DecodeMany . f) ts
123 |   -> List ByteString
124 |   -> Maybe (List ByteString)
125 | simulateHL []       xs = Just xs
126 | simulateHL (x :: y) xs =
127 |   case simulateDecode @{x} xs of
128 |     Nothing  => Nothing
129 |     Just xs2 => simulateHL y xs2
130 |
131 | decodeHL :
132 |      L.All.All (DecodeMany . f) ts
133 |   -> List ByteString
134 |   -> Either DecodeErr (List ByteString, L.All.All f ts)
135 | decodeHL []       xs = Right (xs, [])
136 | decodeHL (x :: y) xs =
137 |   case decodeMany @{x} xs of
138 |     Left err       => Left err
139 |     Right (xs2, v) => map (v::) <$> decodeHL y xs2
140 |
141 | export %inline
142 | (all : L.All.All (DecodeMany . f) ts) => DecodeMany (L.All.All f ts) where
143 |   simulateDecode = simulateHL all
144 |   decodeMany = decodeHL all
145 |
146 | simulateN :
147 |      DecodeMany t
148 |   -> (n : Nat)
149 |   -> List ByteString
150 |   -> Maybe (List ByteString)
151 | simulateN x 0     xs = Just xs
152 | simulateN x (S n) xs =
153 |   case simulateDecode @{x} xs of
154 |     Nothing  => Nothing
155 |     Just xs2 => simulateN x n xs2
156 |
157 | decodeN :
158 |      DecodeMany t
159 |   -> (n : Nat)
160 |   -> List ByteString
161 |   -> Either DecodeErr (List ByteString, Vect n t)
162 | decodeN x 0     xs = Right (xs, [])
163 | decodeN x (S n) xs =
164 |   case decodeMany @{x} xs of
165 |     Left err       => Left err
166 |     Right (xs2, v) => map (v::) <$> decodeN x n xs2
167 |
168 | export %inline
169 | {n : Nat} -> (x : DecodeMany a) => DecodeMany (Vect n a) where
170 |   simulateDecode = simulateN x n
171 |   decodeMany = decodeN x n
172 |
173 | --------------------------------------------------------------------------------
174 | -- DecodeVia
175 | --------------------------------------------------------------------------------
176 |
177 | namespace DecodeVia
178 |   public export
179 |   interface DecodeVia (0 from, to : Type) where
180 |     fromBytes  : Parameters -> ByteString -> Either DecodeErr from
181 |     decodeFrom : from -> Either DecodeErr to
182 |     mediaType  : MediaType
183 |
184 | export
185 | decodeVia :
186 |      {auto d : DecodeVia from to}
187 |   -> Parameters
188 |   -> ByteString
189 |   -> Either DecodeErr to
190 | decodeVia ps bs = fromBytes @{d} ps bs >>= decodeFrom
191 |
192 | public export
193 | interface FromFormData a where
194 |   fromFormData : FormData -> Either DecodeErr a
195 |
196 | --------------------------------------------------------------------------------
197 | -- Utilities
198 | --------------------------------------------------------------------------------
199 |
200 | export %inline
201 | Decode ByteString where decode = Right
202 |
203 | export %inline
204 | Decode String where decode = Right . toString
205 |
206 | export
207 | refinedEither :
208 |      {auto r : Decode a}
209 |   -> (type : String)
210 |   -> (a -> Either String b)
211 |   -> ByteString
212 |   -> Either DecodeErr b
213 | refinedEither t f bs = Prelude.do
214 |   v <- mapFst (setType t) $ decodeAs a bs
215 |   mapFst (ReadErr t (toString bs)) (f v)
216 |
217 | export
218 | refined :
219 |      {auto r  : Decode a}
220 |   -> (type    : String)
221 |   -> (details : Lazy String)
222 |   -> (a -> Maybe b)
223 |   -> ByteString
224 |   -> Either DecodeErr b
225 | refined t details f bs = Prelude.do
226 |   v <- mapFst (setType t) $ decodeAs a bs
227 |   case f v of
228 |     Nothing => Left $ ReadErr t (toString bs) details
229 |     Just x  => Right x
230 |