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