0 | module Postgres.Result
  1 |
  2 | import public Data.Vect
  3 |
  4 | import Postgres.FFI.Utility
  5 | import Postgres.Data.ResultStatus
  6 | import Postgres.Data.PostgresType
  7 | import Data.Fin
  8 |
  9 | ||| Internal phantom type used to mark pointers to the
 10 | ||| `libpq` struct of the same name.
 11 | export 
 12 | data PGresult : Type
 13 |
 14 | %foreign libpq "PQclear"
 15 |          nLibpq "PQclear"
 16 | prim__dbClearResult : Ptr PGresult -> PrimIO ()
 17 |
 18 | ||| The result of executing a command. See `Postgres.Exec`
 19 | ||| for more.
 20 | export
 21 | data Result : Type where
 22 |   MkResult : Ptr PGresult -> Result
 23 |
 24 |
 25 | ||| All of the various forms of execution supported by libpq
 26 | ||| provide types that conform to the `ResultProducer` interface.
 27 | public export
 28 | interface ResultProducer source input where
 29 |   exec : source -> input -> IO (Ptr PGresult)
 30 |
 31 | ||| Execute the given result producer, do the given thing with the
 32 | ||| result, and then free the memory used for the result.
 33 | export
 34 | withResult : ResultProducer source a => source -> a -> (Result -> IO b) -> IO b
 35 | withResult src cmd f = do resPtr <- exec src cmd
 36 |                           out <- f $ MkResult resPtr
 37 |                           primIO $ prim__dbClearResult resPtr
 38 |                           pure out
 39 |
 40 |
 41 | --
 42 | -- Result Status
 43 | --
 44 |
 45 | resultStatus : Int -> ResultStatus
 46 | resultStatus i =
 47 |   case i of
 48 |        0 => EMPTY_QUERY
 49 |        1 => COMMAND_OK
 50 |        2 => TUPLES_OK
 51 |        3 => COPY_OUT
 52 |        4 => COPY_IN
 53 |        5 => BAD_RESPONSE
 54 |        6 => NONFATAL_ERROR
 55 |        7 => FATAL_ERROR
 56 |        8 => COPY_BOTH
 57 |        9 => SINGLE_TUPLE
 58 |        x => OTHER x
 59 |
 60 | %foreign libpq "PQresultStatus"
 61 |          nLibpq "PQresultStatus"
 62 | prim__dbResultStatus : Ptr PGresult -> Int
 63 |
 64 | export
 65 | pgResultStatus : Result -> ResultStatus
 66 | pgResultStatus (MkResult res) = resultStatus $ prim__dbResultStatus res
 67 |
 68 | export
 69 | pgResultSuccess : Result -> Bool
 70 | pgResultSuccess res with (pgResultStatus res)
 71 |   pgResultSuccess _ | EMPTY_QUERY = True
 72 |   pgResultSuccess _ | COMMAND_OK = True
 73 |   pgResultSuccess _ | TUPLES_OK = True
 74 |   pgResultSuccess _ | COPY_OUT = True
 75 |   pgResultSuccess _ | COPY_IN = True
 76 |   pgResultSuccess _ | COPY_BOTH = True
 77 |   pgResultSuccess _ | SINGLE_TUPLE = True
 78 |   pgResultSuccess _ | x = False
 79 |
 80 | %foreign libpq "PQresultErrorMessage"
 81 |          nLibpq "PQresultErrorMessage"
 82 | prim__dbResultErrorMessage : Ptr PGresult -> String
 83 |
 84 | ||| Get the Postgres error message for the given result or
 85 | ||| Nothing if the result was a success.
 86 | export
 87 | pgResultErrorMessage : Result -> Maybe String
 88 | pgResultErrorMessage result@(MkResult res) = case pgResultSuccess result of
 89 |                                                   False => Just $ prim__dbResultErrorMessage res
 90 |                                                   True  => Nothing
 91 |
 92 | --
 93 | -- Tuple Result
 94 | --
 95 |
 96 | %foreign libpq "PQntuples"
 97 |          nLibpq "PQntuples"
 98 | prim__dbResultRowCount : Ptr PGresult -> Int
 99 |
100 | %foreign libpq "PQnfields"
101 |          nLibpq "PQnfields"
102 | prim__dbResultColCount : Ptr PGresult -> Int
103 |
104 | ||| Assumes the result is of type TUPLES_OK. Used
105 | ||| internally to define TupleResult or else it
106 | ||| would require TupleResult itself.
107 | resultRowCount : Result -> Nat
108 | resultRowCount (MkResult res) = integerToNat $ cast $ prim__dbResultRowCount res
109 |
110 | ||| Assumes the result is of type TUPLES_OK. Used
111 | ||| internally to define TupleResult or else it
112 | ||| would require TupleResult itself.
113 | resultColCount : Result -> Nat
114 | resultColCount (MkResult res) = integerToNat $ cast $ prim__dbResultColCount res
115 |
116 | export 
117 | data TupleResult : (rows: Nat) -> (cols: Nat) -> Type where
118 |   MkTupleResult : (res : Result) -> TupleResult (resultRowCount res) (resultColCount res)
119 |
120 | export
121 | tupleResult : (res: Result) -> Maybe (TupleResult (resultRowCount res) (resultColCount res))
122 | tupleResult res = case (pgResultStatus res) of
123 |                        TUPLES_OK => pure $ MkTupleResult res 
124 |                        _ => Nothing
125 |
126 | --
127 | -- Result Value
128 | --
129 |
130 | %foreign libpq "PQfname"
131 |          nLibpq "PQfname"
132 | prim__dbResultColName : Ptr PGresult -> (col : Int) -> String
133 |
134 | %foreign libpq "PQgetisnull"
135 |          nLibpq "PQgetisnull"
136 | prim__dbResultValueIsNull : Ptr PGresult -> (row : Int) -> (col : Int) -> Int
137 |
138 | %foreign libpq "PQfformat"
139 |          nLibpq "PQfformat"
140 | prim__dbResultColFormatCode : Ptr PGresult -> (col : Int) -> Int
141 |
142 | ||| Get the type of the column. The resulting Int is a Postgres OID.
143 | ||| Built-in data types are defined in the file src/include/catalog/pg_type.h
144 | %foreign libpq "PQftype"
145 |          nLibpq "PQftype"
146 | prim__dbResultColType : Ptr PGresult -> (col : Int) -> Int
147 |
148 | ||| Get the name of the given column for this tuple result.
149 | resultColName : TupleResult r c -> (col : Fin c) -> String
150 | resultColName (MkTupleResult (MkResult res)) col = prim__dbResultColName res (cast $ finToInteger col)
151 |
152 | ||| Get whether the value at the given row and column is null or not.
153 | resultValueIsNull : TupleResult r c -> (row : Fin r) -> (col : Fin c) -> Bool
154 | resultValueIsNull (MkTupleResult (MkResult res)) row col = 
155 |   intToBool $ prim__dbResultValueIsNull res (cast $ finToInteger row) (cast $ finToInteger col)
156 |
157 | ||| Get the result column type. Note that this is currently limited
158 | ||| by the few known types that are looked up and stored in the
159 | ||| TypeDictionary.
160 | resultColType : {auto types : TypeDictionary} -> TupleResult r c -> (col : Fin c) -> PType
161 | resultColType (MkTupleResult (MkResult res)) col = 
162 |   let oid = prim__dbResultColType res (cast $ finToInteger col) in
163 |       lookup (MkOid oid) types
164 |
165 | intToFormatCode : Int -> FormatCode
166 | intToFormatCode 0 = Text
167 | intToFormatCode 1 = Binary
168 | intToFormatCode _ = Text -- technically, other codes are reserved for future definition.
169 |
170 | resultColFormatCode : TupleResult r c -> (col : Fin c) -> FormatCode
171 | resultColFormatCode (MkTupleResult (MkResult res)) col = 
172 |   intToFormatCode $ prim__dbResultColFormatCode res (cast $ finToInteger col)
173 |
174 | ||| Get the size of the resultset as (row, col).
175 | export 
176 | pgResultSize : {r: Nat} -> {c: Nat} -> TupleResult r c -> (Nat, Nat)
177 | pgResultSize res = (r, c)
178 |
179 | %foreign libpq "PQgetvalue"
180 |          nLibpq "PQgetvalue"
181 | prim__dbResultValue : Ptr PGresult -> (row: Int) -> (col: Int) -> String
182 |
183 | ||| Get the result value at the given row and column as a String regardless
184 | ||| of what the underlying Postgres type is.
185 | |||
186 | ||| Null postgres values are treated as empty strings.
187 | |||
188 | ||| Use `pgResultNullableStringValue` to handle nulls as Nothing.
189 | export
190 | pgResultStringValue : (res: TupleResult rows cols) -> (row: Fin rows) -> (col: Fin cols) -> String
191 | pgResultStringValue (MkTupleResult (MkResult res)) row col = 
192 |   let r = cast $ the Nat (cast row)
193 |       c = cast $ the Nat (cast col) in 
194 |     prim__dbResultValue res r c
195 |
196 | ||| Get the result value at the given row and column as a (Maybe String) regardless
197 | ||| of what the underlying Postgres type is.
198 | |||
199 | ||| Null postgres values are Nothing, whereas all other values are String (this does not
200 | ||| fail to parse Strings by returning Nothing -- anything non-null is guaranteed to return
201 | ||| a `Just` value).
202 | |||
203 | ||| Use `pgResultStringValue` to handle nulls as empty Strings.
204 | export
205 | pgResultNullableStringValue : (res: TupleResult rows cols) -> (row: Fin rows) -> (col: Fin cols) -> Maybe String
206 | pgResultNullableStringValue (MkTupleResult (MkResult res)) row col = 
207 |   let r = cast $ the Nat (cast row)
208 |       c = cast $ the Nat (cast col) in 
209 |     case intToBool $ prim__dbResultValueIsNull res r c of
210 |          True  => Nothing
211 |          False => Just $ prim__dbResultValue res r c
212 |
213 | ||| The combination of name and type information for a single Postgres result column.
214 | public export
215 | record ColHeader where
216 |   constructor MkHeader
217 |   name : String
218 |   type : PType
219 |
220 | export
221 | Show ColHeader where
222 |   show (MkHeader name type) = name ++ " " ++ (show type)
223 |
224 | --
225 | -- Resultset
226 | --
227 |
228 | resultRow : {cols: Nat} -> (res : TupleResult rows cols) -> (row: Fin rows) -> (Vect cols (Lazy String))
229 | resultRow res row = valueAt <$> (range {len=cols}) where
230 |   valueAt : Fin cols -> Lazy String
231 |   valueAt col = pgResultStringValue res row col
232 |
233 | nullableResultRow : {cols: Nat} -> (res : TupleResult rows cols) -> (row: Fin rows) -> (Vect cols (Lazy (Maybe String)))
234 | nullableResultRow res row = valueAt <$> (range {len=cols}) where
235 |   valueAt : Fin cols -> Lazy (Maybe String)
236 |   valueAt col = pgResultNullableStringValue res row col
237 |
238 | ||| Get the resultset (all rows and columns) with all values as Strings
239 | ||| regardless of the underlying Postgres value type.
240 | |||
241 | ||| Null is treated as the empty String.
242 | |||
243 | ||| To get (Maybe String) where null is Nothing, use `pgNullableStringResultset`
244 | export
245 | pgStringResultset : {rows: Nat} 
246 |                  -> {cols: Nat} 
247 |                  -> (res : TupleResult rows cols) 
248 |                  -> (Vect rows (Vect cols (Lazy String)))
249 | pgStringResultset res = valueAt <$> (range {len=rows}) where
250 |   valueAt : Fin rows -> Vect cols (Lazy String)
251 |   valueAt = resultRow res
252 |
253 | public export
254 | StringResultset : (header : Bool) -> Type
255 | StringResultset False = (rows ** cols ** Vect rows (Vect cols (Maybe String)))
256 | StringResultset True = (rows ** cols ** (Vect cols ColHeader, Vect rows (Vect cols (Maybe String))))
257 |
258 | ||| Get the resultset (all rows and columns) with all values as (Maybe Strings)
259 | ||| regardless of the underlying Postgres value type.
260 | |||
261 | ||| Null is treated as Nothing -- No matter what type the Postgres column is, a non-null
262 | ||| value will be a `Just` value with a String in it; Nothing only means null, not
263 | ||| ever that the value failed to parse as a String.
264 | |||
265 | ||| To get String where null is the empty String, use `pgStringResultset`
266 | export
267 | pgNullableStringResultset : {rows: Nat} 
268 |                          -> {cols: Nat} 
269 |                          -> (res : TupleResult rows cols) 
270 |                          -> (Vect rows (Vect cols (Lazy (Maybe String))))
271 | pgNullableStringResultset res = valueAt <$> (range {len=rows}) where
272 |   valueAt : Fin rows -> Vect cols (Lazy (Maybe String))
273 |   valueAt = nullableResultRow res
274 |
275 | export
276 | pgResultsetColNames : {cols : Nat} -> (res : TupleResult rows cols) -> Vect cols String
277 | pgResultsetColNames res = resultColName res <$> (range {len=cols})
278 |
279 | ||| Get all the column types for the given result. Note that 
280 | ||| this is currently limited by the few known types that
281 | ||| are looked up and stored in the TypeDictionary.
282 | export
283 | pgResultsetColTypes : {auto types : TypeDictionary} -> {cols : Nat} -> (res : TupleResult rows cols) -> Vect cols PType
284 | pgResultsetColTypes res = resultColType res <$> (range {len=cols})
285 |
286 |