0 | module HTTP.API.Encode
  1 |
  2 | import Data.List.Quantifiers as L
  3 | import Data.Vect
  4 | import public Data.ByteString
  5 | import public HTTP.Header.Types
  6 | import JSON.Simple
  7 |
  8 | %default total
  9 |
 10 | ||| An interface for encode a value as raw bytes
 11 | |||
 12 | ||| This is used for encoding values in URL paths and query strings
 13 | ||| but - in general - not for encoding value in the message body.
 14 | ||| Use `EncodeVia` for that.
 15 | public export
 16 | interface Encode (0 a : Type) where
 17 |   encode : a -> ByteString
 18 |
 19 | ||| An interface for encoding values as a list of bytestrings.
 20 | public export
 21 | interface EncodeMany (0 a : Type) where
 22 |   encodeMany : a -> List ByteString
 23 |
 24 | export %inline
 25 | Encode a => EncodeMany a where
 26 |   encodeMany v = [encode v]
 27 |
 28 | encodeHL :
 29 |      {auto all : L.All.All (EncodeMany . f) ts}
 30 |   -> L.All.All f ts
 31 |   -> List ByteString
 32 | encodeHL           []      = []
 33 | encodeHL @{_ :: _} (x::xs) = encodeMany x ++ encodeHL xs
 34 |
 35 | export %inline
 36 | L.All.All (EncodeMany . f) ts => EncodeMany (L.All.All f ts) where
 37 |   encodeMany = encodeHL
 38 |
 39 | encodeList : EncodeMany t => List t -> List ByteString
 40 | encodeList []      = []
 41 | encodeList (x::xs) = encodeMany x ++ encodeList xs
 42 |
 43 | export %inline
 44 | EncodeMany a => EncodeMany (Vect n a) where
 45 |   encodeMany = encodeList . toList
 46 |
 47 | export %inline
 48 | EncodeMany a => EncodeMany (List a) where
 49 |   encodeMany = encodeList
 50 |
 51 | export %inline
 52 | EncodeMany a => EncodeMany (SnocList a) where
 53 |   encodeMany = encodeList . (<>> [])
 54 |
 55 | --------------------------------------------------------------------------------
 56 | -- EncodeVia interface
 57 | --------------------------------------------------------------------------------
 58 |
 59 | public export
 60 | 0 Text : Type
 61 | Text = String
 62 |
 63 | public export
 64 | 0 Octett : Type
 65 | Octett = ByteString
 66 |
 67 | public export
 68 | 0 OctettList : Type
 69 | OctettList = List ByteString
 70 |
 71 | public export
 72 | interface EncodeVia (0 from, to : Type) where
 73 |   encodeAs : from -> to
 74 |   toBytes  : to -> List ByteString
 75 |   mediaType : MediaType
 76 |
 77 | export %inline
 78 | encodeVia : (v : f) -> EncodeVia f t -> List ByteString
 79 | encodeVia v c = toBytes @{c} $ encodeAs @{c} v
 80 |
 81 | export %inline
 82 | Interpolation a => EncodeVia a String where
 83 |   encodeAs  = interpolate
 84 |   toBytes   = pure . fromString
 85 |   mediaType = MT "text" "plain"
 86 |
 87 | export %inline
 88 | Cast a ByteString => EncodeVia a ByteString where
 89 |   encodeAs  = cast
 90 |   toBytes   = pure
 91 |   mediaType = MT "application" "octett-stream"
 92 |
 93 | export %inline
 94 | Cast a (List ByteString) => EncodeVia a (List ByteString) where
 95 |   encodeAs  = cast
 96 |   toBytes   = id
 97 |   mediaType = MT "application" "octett-stream"
 98 |
 99 | export %inline
100 | ToJSON a => EncodeVia a JSON where
101 |   encodeAs  = toJSON
102 |   toBytes   = pure . fromString . show
103 |   mediaType = MT "application" "json"
104 |
105 | --------------------------------------------------------------------------------
106 | -- Implementations
107 | --------------------------------------------------------------------------------
108 |
109 | export %inline
110 | Encode ByteString where encode = id
111 |
112 | export %inline
113 | Encode String where encode = fromString
114 |
115 | export
116 | Encode Nat where
117 |   encode = encode . show
118 |
119 | export
120 | Encode Integer where
121 |   encode = encode. show
122 |
123 | export
124 | Encode Bits8 where
125 |   encode = encode. show
126 |
127 | export
128 | Encode Bits16 where
129 |   encode = encode. show
130 |
131 | export
132 | Encode Bits32 where
133 |   encode = encode. show
134 |
135 | export
136 | Encode Bits64 where
137 |   encode = encode. show
138 |
139 | export
140 | Encode Int8 where
141 |   encode = encode. show
142 |
143 | export
144 | Encode Int16 where
145 |   encode = encode. show
146 |
147 | export
148 | Encode Int32 where
149 |   encode = encode. show
150 |
151 | export
152 | Encode Int64 where
153 |   encode = encode. show
154 |
155 | export
156 | Encode Double where
157 |   encode = encode. show
158 |