0 | module HTTP.I18n
  1 |
  2 | import Data.ByteString
  3 | import HTTP.API.Decode
  4 | import HTTP.FormData
  5 | import HTTP.Header.Types
  6 | import HTTP.RequestErr
  7 | import HTTP.Status
  8 | import JSON.Simple
  9 | import IO.Async.Logging
 10 | import Text.ILex
 11 |
 12 | %default total
 13 |
 14 | public export
 15 | interface HTTPLocal where
 16 |   endOfURIPath           : String
 17 |   floatingPointNumber    : String
 18 |   integer                : String
 19 |   invalidPath            : String
 20 |   jsonValue              : String
 21 |   logLevel               : LogLevel -> String
 22 |   missingBoundary        : String
 23 |   missingFormDataPart    : (part, parts : String) -> String
 24 |   missingHeader          : String -> String
 25 |   missingQueryParameter  : String -> String
 26 |   missingQueryValue      : String -> String
 27 |   myMediaTypeNotAccepted : String -> String -> String
 28 |   naturalNumber          : String
 29 |   outOfBounds            : Show a => (min,max : a) -> String
 30 |   prettyDecodeErr        : DecodeErr -> String
 31 |   prettyRequestErr       : RequestErr -> String
 32 |   unsignedInteger        : String
 33 |
 34 |
 35 | --------------------------------------------------------------------------------
 36 | -- Utilities
 37 | --------------------------------------------------------------------------------
 38 |
 39 | ||| Utility for quoting non-empty strings in decode errors.
 40 | export
 41 | valueString : String -> String
 42 | valueString "" = ""
 43 | valueString s  = ": '\{s}'"
 44 |
 45 | dets : DecodeErr -> String
 46 | dets (ContentErr _ ds) = ds
 47 | dets (ReadErr _ _ ds)  = ds
 48 | dets _                 = ""
 49 |
 50 | export
 51 | commaSep : List String -> String
 52 | commaSep = fastConcat . intersperse ","
 53 |
 54 | export
 55 | commaSepI : Interpolation a => List a -> String
 56 | commaSepI = commaSep . map interpolate
 57 |
 58 | export
 59 | commaSepS : Show a => List a -> String
 60 | commaSepS = commaSep . map show
 61 |
 62 | parameters {auto loc : HTTPLocal}
 63 |
 64 |   export %inline
 65 |   Interpolation RequestErr where
 66 |     interpolate = prettyRequestErr
 67 |
 68 |   export %inline
 69 |   Interpolation DecodeErr where
 70 |     interpolate = prettyDecodeErr
 71 |
 72 |   export
 73 |   decodeErr : Status -> DecodeErr -> RequestErr
 74 |   decodeErr s de = {message := "\{de}", details := dets de} (requestErr s)
 75 |
 76 |   export
 77 |   bounded :
 78 |        (0 a    : Type)
 79 |     -> {auto r : Decode a}
 80 |     -> {auto o : Ord a}
 81 |     -> {auto s : Show a}
 82 |     -> {auto c : Cast a b}
 83 |     -> (type    : String)
 84 |     -> (min,max : a)
 85 |     -> ByteString
 86 |     -> Either DecodeErr b
 87 |   bounded a t min max = refined t (outOfBounds min max) $ \v =>
 88 |     if (min <= v && v <= max) then Just (cast v) else Nothing
 89 |
 90 |   export
 91 |   Decode Nat where
 92 |     decode (BS 0 _) = Left $ readErr naturalNumber empty
 93 |     decode bs =
 94 |       if all isDigit bs
 95 |          then Right (cast $ decimal bs)
 96 |          else Left $ readErr naturalNumber bs
 97 |
 98 |   export
 99 |   Decode Integer where
100 |     decode (BS 0 _) = Left $ readErr integer empty
101 |     decode bs@(BS (S k) bv) =
102 |       mapFst (setType integer) $ case head bv of
103 |         45 => map (negate . cast) (decodeAs Nat (BS k $ tail bv))
104 |         _  => map cast $ decodeAs Nat bs
105 |
106 |   export
107 |   Decode Bits8 where
108 |     decode = bounded Integer unsignedInteger 0 0xff
109 |
110 |   export
111 |   Decode Bits16 where
112 |     decode = bounded Integer unsignedInteger 0 0xffff
113 |
114 |   export
115 |   Decode Bits32 where
116 |     decode = bounded Integer unsignedInteger 0 0xffff_ffff
117 |
118 |   export
119 |   Decode Bits64 where
120 |     decode = bounded Integer unsignedInteger 0 0xffff_ffff_ffff_ffff
121 |
122 |   export
123 |   Decode Int8 where
124 |     decode = bounded Integer integer (-0x80) 0x7f
125 |
126 |   export
127 |   Decode Int16 where
128 |     decode = bounded Integer integer (-0x8000) 0x7fff
129 |
130 |   export
131 |   Decode Int32 where
132 |     decode = bounded Integer integer (-0x8000_0000) 0x7fff_ffff
133 |
134 |   export
135 |   Decode Int64 where
136 |     decode = bounded Integer integer (-0x8000_0000_0000_0000) 0x7fff_ffff_ffff_ffff
137 |
138 |   export
139 |   Decode Double where
140 |     decode bs =
141 |       case runBytes json bs of
142 |         Right (JDouble x)  => Right x
143 |         Right (JInteger x) => Right $ cast x
144 |         _                  => Left $ readErr floatingPointNumber bs
145 |
146 |   parameters {auto fj : FromJSON a}
147 |
148 |     export
149 |     DecodeVia JSON a where
150 |       fromBytes _ = mapFst (contentErr jsonValue) . parseBytes json Virtual
151 |       decodeFrom  = mapFst (contentErr jsonValue . JErr) . fromJSON
152 |       mediaType   = MT "application" "json"
153 |
154 |   parameters {auto fd : FromFormData a}
155 |
156 |     export
157 |     DecodeVia FormData a where
158 |       fromBytes ps bs =
159 |         case parameter "boundary" ps of
160 |           Just b  => Right $ multipart (fromString b) bs
161 |           Nothing => Left $ Msg missingBoundary
162 |       decodeFrom      = fromFormData
163 |       mediaType       = MT "multipart" "form-data"
164 |
165 |   export
166 |   getFDBytes : String -> FormData -> Either DecodeErr ByteString
167 |   getFDBytes s xs =
168 |     case find ((s ==) . name) xs of
169 |       Nothing => Left $ Msg $ missingFormDataPart s (commaSep $ map name xs)
170 |       Just p  => Right p.content
171 |