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