0 | module Postgres.Query
  1 |
  2 | import public JSON.Parser
  3 | import public Data.Vect.Quantifiers
  4 | import public Postgres.Data.PostgresValue
  5 |
  6 | import Postgres.FFI.Utility
  7 | import Postgres.Data.Conn
  8 | import Postgres.Data.PostgresType
  9 | import Postgres.Exec
 10 | import Postgres.Result
 11 | import Decidable.Equality
 12 | import Data.Fin
 13 | import Data.Vect
 14 | import Data.Either
 15 |
 16 | %default total
 17 |
 18 | ||| Get the first row first column from the given
 19 | ||| result. Will return `Nothing` if there are no
 20 | ||| results. 
 21 | maybeFirstRowCol : {r,c : Nat} -> TupleResult r c -> Maybe String
 22 | maybeFirstRowCol res = do row <- natToFin 0 r
 23 |                           col <- natToFin 0 c
 24 |                           pure $ pgResultStringValue res row col
 25 |
 26 | --
 27 | -- Headers
 28 | --
 29 |
 30 | headerNames : {colCount : Nat} -> TupleResult _ colCount -> Vect colCount String
 31 | headerNames t = pgResultsetColNames t
 32 |
 33 | headerTypes : {auto types : TypeDictionary} 
 34 |            -> {colCount : Nat} 
 35 |            -> TupleResult _ colCount 
 36 |            -> Vect colCount PType
 37 | headerTypes t = pgResultsetColTypes t
 38 |
 39 | headers : {auto types : TypeDictionary} 
 40 |        -> {colCount : Nat} 
 41 |        -> TupleResult _ colCount 
 42 |        -> Vect colCount ColHeader
 43 | headers t = (uncurry MkHeader) <$> (zip (headerNames t) (headerTypes t))
 44 |
 45 | --
 46 | -- Stringy (unityped) Results
 47 | --
 48 |
 49 | rows : {rowCount, colCount : Nat} -> TupleResult rowCount colCount -> Vect rowCount (Vect colCount (Maybe String))
 50 | rows t = (map force) <$> pgNullableStringResultset t
 51 |
 52 | export
 53 | pgStringResultsQuery : {auto types : TypeDictionary} 
 54 |                     -> (header : Bool) 
 55 |                     -> (query : String) 
 56 |                     -> Conn 
 57 |                     -> IO (Either String (StringResultset header))
 58 | pgStringResultsQuery header query conn = withExecResult conn query stringResults 
 59 |   where 
 60 |     stringResults : Result -> IO (Either String (StringResultset header))
 61 |     stringResults r = do Nothing <- pure $ pgResultErrorMessage r
 62 |                            | Just err => pure $ Left err
 63 |                          Just tuples <- pure $ tupleResult r
 64 |                            | Nothing  => pure $ Left "query did not result in expected response."
 65 |                          pure $ Right $ if header
 66 |                                         then (_ ** _ ** (headers tuples, rows tuples))
 67 |                                         else (_ ** _ ** rows tuples)
 68 |
 69 | --
 70 | -- JSON Results
 71 | --
 72 |
 73 | ||| Get the result as JSON if it is 1 row and column that can
 74 | ||| be successfully parsed as JSON.
 75 | export
 76 | pgJSONResultQuery : (query: String) -> Conn -> IO (Maybe JSON)
 77 | pgJSONResultQuery query conn = withExecResult conn query toJson where 
 78 |   toJson : Result -> IO (Maybe JSON)
 79 |   toJson r = pure $ [ json | json <- eitherToMaybe $ parseJSON Virtual !(maybeFirstRowCol !(tupleResult r))
 80 |                     ]
 81 |
 82 | --
 83 | -- Expected Type Results
 84 | --
 85 |
 86 | -- Here you pass the vect of types you expect and get back results if possible.
 87 |
 88 | processValue : Castable expectation
 89 |             -> Maybe String
 90 |             -> Either String expectation
 91 | processValue hasDefault = (asDefaultType hasDefault)
 92 |
 93 | processCols : {0 expected : Vect colCount Type}
 94 |            -> All Castable expected 
 95 |            -> Vect colCount (Maybe String)
 96 |            -> Either String (HVect expected)
 97 | processCols [] [] = Right []
 98 | processCols (castable :: castables) (x :: xs) = 
 99 |   [| (processValue castable x) :: (processCols castables xs) |]
100 |
101 | processRows : {0 expected : Vect colCount Type} 
102 |            -> {auto castable : (All Castable expected)}
103 |            -> Vect rowCount (Vect colCount (Maybe String)) 
104 |            -> Either String (Vect rowCount (HVect expected))
105 | processRows xs = traverse (processCols castable) xs 
106 |
107 | ||| Get the result as a rows of the expected types of values if possible.
108 | export
109 | pgResultQuery : {auto types : TypeDictionary} 
110 |              -> {colCount : Nat}
111 |              -> (expected : Vect colCount Type) 
112 |              -> (query : String) 
113 |              -> Conn 
114 |              -> {auto castable : (All Castable expected)}
115 |              -> IO (Either String (rowCount ** Vect rowCount (HVect expected)))
116 | pgResultQuery expected query conn = 
117 |   do Right (rowCount ** receivedCols ** strings) <- pgStringResultsQuery False query conn
118 |        | Left err => pure $ Left err
119 |      pure $ 
120 |        case decEq colCount receivedCols of
121 |             (No _) => 
122 |               Left $ columnMismatchError receivedCols
123 |             (Yes correctCols) => 
124 |               (MkDPair rowCount) <$> processRows (rewrite correctCols in strings)
125 |     where
126 |       columnMismatchError : (received : Nat) -> String
127 |       columnMismatchError received = 
128 |         "Wrong number of columns returned. Expected " ++ (show colCount) ++ " but got " ++ (show received)
129 |
130 |