0 | module Postgres.Data.PostgresValue
  1 |
  2 | import Data.Either
  3 | import Data.String
  4 | import Data.List
  5 | import Data.List1
  6 | import Postgres.Data.PostgresType
  7 | import JSON.Parser
  8 |
  9 | public export
 10 | data PValue : (p : PType) -> Type where
 11 |   Raw : (rawString : String) -> PValue p
 12 |
 13 | export
 14 | Semigroup (PValue p) where
 15 |   (Raw x) <+> (Raw y) = Raw (x <+> y)
 16 |
 17 | export
 18 | Monoid (PValue p) where
 19 |   neutral = Raw ""
 20 |
 21 | export
 22 | rawString : PValue t -> String
 23 | rawString (Raw r) = r
 24 |
 25 | ||| Represents an ability to cast a Postgres type of value (pt) to
 26 | ||| a particular Idris type (ty).
 27 | ||| @param pt A Postgres type to cast from.
 28 | ||| @param ty An Idris type to cast to.
 29 | public export
 30 | interface IdrCast pt ty where
 31 |   toIdris : PValue pt -> Maybe ty
 32 |
 33 | public export
 34 | interface PGCast pt ty where
 35 |   toPostgres : ty -> PValue pt
 36 |
 37 | -- Integer
 38 |
 39 | export
 40 | IdrCast PInteger Int where
 41 |   toIdris = parseInteger . rawString
 42 |
 43 | export
 44 | PGCast PInteger Int where
 45 |   toPostgres = Raw . show
 46 |
 47 | export
 48 | IdrCast PInteger Integer where
 49 |   toIdris = parseInteger . rawString
 50 |
 51 | export
 52 | PGCast PInteger Integer where
 53 |   toPostgres = Raw . show
 54 |
 55 | export
 56 | IdrCast PInteger Double where
 57 |   toIdris = parseDouble . rawString
 58 |
 59 | export
 60 | PGCast PInteger Nat where
 61 |   toPostgres = Raw . show
 62 |
 63 | -- Double
 64 |
 65 | export
 66 | IdrCast PDouble Double where
 67 |   toIdris = parseDouble . rawString
 68 |   
 69 | export
 70 | PGCast PDouble Double where
 71 |   toPostgres = Raw . show
 72 |
 73 | export
 74 | PGCast PDouble Integer where
 75 |   toPostgres = Raw . show
 76 |
 77 | export
 78 | PGCast PDouble Int where
 79 |   toPostgres = Raw . show
 80 |
 81 | -- Char
 82 |
 83 | export
 84 | IdrCast PChar Char where
 85 |   toIdris (Raw str) with (unpack str)
 86 |     toIdris (Raw str) | [c] = Just c
 87 |     toIdris (Raw str) | _ = Nothing
 88 |
 89 | export
 90 | PGCast PChar Char where
 91 |   toPostgres c = Raw $ "'\{String.singleton c}'"
 92 |
 93 | -- Boolean
 94 |
 95 | export
 96 | IdrCast PBoolean Bool where
 97 |   toIdris (Raw "t")     = Just True
 98 |   toIdris (Raw "f")     = Just False
 99 |   toIdris (Raw "true")  = Just True
100 |   toIdris (Raw "false") = Just False
101 |   toIdris (Raw "1")     = Just True
102 |   toIdris (Raw "0")     = Just False
103 |   toIdris (Raw _)       = Nothing
104 |
105 | export
106 | PGCast PBoolean Bool where
107 |   toPostgres True = Raw "true"
108 |   toPostgres False = Raw "false"
109 |
110 | -- TODO: Date
111 |
112 | -- TODO: Time
113 |
114 | -- TODO: Datetime
115 |
116 | -- String
117 |
118 | export
119 | Cast (PValue PString) String where
120 |   cast = rawString
121 |
122 | export
123 | IdrCast PString String where
124 |   toIdris = Just . cast
125 |
126 | export
127 | PGCast PString String where
128 |   toPostgres s = Raw $ "'\{s}'"
129 |
130 | -- JSON
131 |
132 | export
133 | IdrCast PJson JSON where
134 |   toIdris json =
135 |     eitherToMaybe $ parseJSON Virtual (rawString json)
136 |
137 | export
138 | PGCast PJson JSON where
139 |   toPostgres j = Raw $ "'\{show j}'"
140 |
141 | -- TODO: UUID
142 |
143 | -- OID
144 |
145 | export
146 | IdrCast POid Integer where
147 |   toIdris = parseInteger . rawString
148 |
149 | export
150 | PGCast POid Integer where
151 |   toPostgres = Raw . show
152 |
153 | -- Arrays
154 |
155 | parseArray : String -> Maybe (List String)
156 | parseArray str = 
157 |   let stripped = trim str
158 |   in
159 |       do guard (("{" `isPrefixOf` stripped) && ("}" `isSuffixOf` stripped))
160 |          let middle = reverse . (drop 1) . reverse . (drop 1) $ unpack stripped
161 |          pure . forget $ pack <$> (splitOn ',' middle)
162 |
163 | export
164 | IdrCast from to => IdrCast (PArray from) (List to) where
165 |   toIdris (Raw rawString) = (parseArray rawString) >>= (traverse (toIdris . (Raw {p=from})))
166 |
167 | export
168 | PGCast to from => PGCast (PArray to) (List from) where
169 |   toPostgres xs = 
170 |     let values = concat . intersperse "," $ escaped . toPostgres {pt=to} <$> xs
171 |     in Raw $ "'{" ++ values ++ "}'"
172 |     where
173 |       escaped : PValue t -> String
174 |       escaped (Raw str) = if "'" `isPrefixOf` str
175 |                              then "'\{str}'"
176 |                              else str
177 |
178 | -- Maybe
179 |
180 | export
181 | PGCast to (Maybe from) => PGCast to from where
182 |   toPostgres = toPostgres . Just
183 |
184 | --
185 | -- Default Types
186 | --
187 |
188 | getSafeCast : (t1 : PType) -> IdrCast t1 t2 => IdrCast t1 t2
189 | getSafeCast t1 @{safe} = safe
190 |
191 | export
192 | interface DBStringCast a where
193 |   ||| Cast the string representation of a database value to
194 |   ||| the given Idris type if possible or provide an error
195 |   ||| message.  
196 |   dbCast : String -> Either String a
197 |
198 | export
199 | DBStringCast Integer where
200 |   dbCast str = maybeToEither "Failed to parse an integer from '\{str}'" . toIdris @{getSafeCast PInteger} $ Raw str
201 |
202 | export
203 | DBStringCast Double where
204 |   dbCast str = maybeToEither "Failed to parse a double from '\{str}'" . toIdris @{getSafeCast PDouble} $ Raw str
205 |
206 | export
207 | DBStringCast Char where
208 |   dbCast str = maybeToEither "Failed to parse a char from '\{str}'" . toIdris @{getSafeCast PChar} $ Raw str
209 |
210 | export
211 | DBStringCast Bool where
212 |   dbCast str = maybeToEither "Failed to parse a boolean from '\{str}'" . toIdris @{getSafeCast PBoolean} $ Raw str
213 |
214 | export
215 | DBStringCast String where
216 |   dbCast str = maybeToEither "Failed to parse a string from '\{str}'" . toIdris @{getSafeCast PString} $ Raw str
217 |
218 | export
219 | DBStringCast JSON where
220 |   dbCast str = maybeToEither "Failed to parse json from '\{str}'" . toIdris @{getSafeCast PJson} $ Raw str
221 |
222 | export
223 | DBStringCast a => DBStringCast (List a) where
224 |   dbCast str = traverse dbCast <=< maybeToEither "Failed to parse an array '\{str}'" $ parseArray str
225 |
226 | export
227 | [IdrCastString] IdrCast pt ty => DBStringCast ty where
228 |   dbCast str = maybeToEither "Failed to parse '\{str}' as expected type." . toIdris {pt} $ Raw str
229 |
230 | public export
231 | data Castable : Type -> Type where
232 |   Cast      : DBStringCast ty => Castable ty
233 |   CastMaybe : DBStringCast ty => Castable (Maybe ty)
234 |
235 | ||| Turn the string coming from Postgres into its default Idris type.
236 | |||
237 | ||| You can create your own `DBStringCast` implementations if you wish to
238 | ||| be able to parse additional types using this library's builtin functions.
239 | public export
240 | asDefaultType : Castable t -> (columnValue : Maybe String) -> Either String t
241 | asDefaultType (Cast      @{dbcast}) = dbCast <=< maybeToEither "Unexpected null while casting Postgres values!"
242 | asDefaultType (CastMaybe @{dbcast}) = traverse dbCast
243 |
244 |