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