
   0 | module Postgres.Data.PostgresTable
   1 | 
   2 | import Postgres.Data.PostgresType
   3 | import public Data.DPair
   4 | 
   5 | import Postgres.Data.PostgresValue
   6 | import Data.List
   7 | import public Data.List1
   8 | import public Data.List.Elem
   9 | import Data.Vect
  10 | import Data.Vect.Elem
  11 | import public Data.Vect.Quantifiers
  12 | import public Data.String
  13 | 
  14 | %default total
  15 | 
  16 | ||| A Postgres identifier, generally speaking. Could be a table name
  17 | ||| or a column name or more broadly speaking any proper name that
  18 | ||| Postgres syntactically recognizes between double-quotes.
  19 | public export
  20 | data Ident = Id String
  21 | 
  22 | %name Ident id, id2, id3
  23 | 
  24 | export
  25 | Show Ident where
  26 |   show (Id name) = "\"\{name}\""
  27 | 
  28 | ||| An Alias is a valid table identifier that may either
  29 | ||| be a string specified by the programmer or it may be
  30 | ||| auto-generated in the course of creating subqueries.
  31 | public export
  32 | data Alias = Named String
  33 |            | Generated Nat
  34 | 
  35 | %name Alias alias, alias1, alias2
  36 | 
  37 | ||| Aliases can always be turned into identifiers.
  38 | public export
  39 | aliasIdentifier : Alias -> Ident
  40 | aliasIdentifier (Named str) = Id str
  41 | aliasIdentifier (Generated k) = Id "_idr_t_\{show k}"
  42 | 
  43 | export
  44 | Show Alias where
  45 |   show = show . aliasIdentifier
  46 | 
  47 | export
  48 | Eq Alias where
  49 |   (Named str) == (Named str') = str == str'
  50 |   (Generated k) == (Generated k') = k == k'
  51 |   _ == _ = False
  52 | 
  53 | ||| Turning an identifier into an alias is not inteded to be the lossless
  54 | ||| reversal of `aliasIdentifier`. An identifier will always become a named
  55 | ||| alias even if it was at one point a generated alias before being turned into
  56 | ||| an identifier.
  57 | public export
  58 | toAlias : Ident -> Alias
  59 | toAlias (Id str) = Named str
  60 | 
  61 | ||| Show an AS statement fragment for the given
  62 | ||| alias.
  63 | ||| For a table alias of myTable this will be the string
  64 | ||| literal (including double-quotes and leading space but
  65 | ||| excluding single quotes): ' AS "myTable"'
  66 | maybeShowAsAlias : Maybe Alias -> String
  67 | maybeShowAsAlias Nothing = ""
  68 | maybeShowAsAlias (Just a) = " AS \{show a}"
  69 | 
  70 | ||| Show an alias prefix for a fully qualified column.
  71 | ||| For a table aliased as myTable this will be the string
  72 | ||| literal (including double-quotes and trailing dot but
  73 | ||| excluding single quotes): '"myTable".'
  74 | maybeShowAliasColumnPrefix : Maybe Alias -> String
  75 | maybeShowAliasColumnPrefix Nothing = ""
  76 | maybeShowAliasColumnPrefix (Just a) = "\{show a}."
  77 | 
  78 | ||| A table name or subquery.
  79 | public export
  80 | data TableStatement = ||| A table name.
  81 |                       Identifier String (Maybe Alias)
  82 |                     | ||| A subquery.
  83 |                       Subquery String Alias
  84 |                     | ||| A fragment (can be selected against, but is not named or aliased)
  85 |                       Fragment String
  86 | 
  87 | public export
  88 | tableAlias : TableStatement -> Maybe Alias
  89 | tableAlias (Identifier str a) = a
  90 | tableAlias (Subquery str a) = Just a
  91 | tableAlias (Fragment str) = Nothing
  92 | 
  93 | ||| The table alias or name.
  94 | public export
  95 | tableAliasOrName : TableStatement -> Maybe Ident
  96 | tableAliasOrName (Identifier name alias) = Just $ maybe (Id name) aliasIdentifier alias
  97 | tableAliasOrName (Subquery _ alias) = Just $ aliasIdentifier alias
  98 | tableAliasOrName (Fragment _) = Nothing
  99 | 
 100 | export
 101 | Show TableStatement where
 102 |   show (Identifier n a) = "\{show $ Id n}\{maybeShowAsAlias a}"
 103 |   show (Subquery query a) = "(\{query}) AS \{show a}"
 104 |   show (Fragment query) = query
 105 | 
 106 | ||| Construct a table statement for a table with the given name.
 107 | public export
 108 | named : String -> {default Nothing alias : Maybe Alias} -> TableStatement
 109 | named str {alias} = Identifier str alias
 110 | 
 111 | ||| Construct a table statement using a subquery.
 112 | export
 113 | subquery : String -> Alias -> TableStatement
 114 | subquery = Subquery
 115 | 
 116 | ||| A column is identified by its name and optionally the alias
 117 | ||| of a table the column comes from. In some situations the `sourceTable`
 118 | ||| for a column will be needed in order to unambiguously refer to one
 119 | ||| of a few columns in the same query with the same name.
 120 | |||
 121 | ||| Generally it will be clunky to create ColumnIdentifiers using the type's
 122 | ||| consutrctor directly so most column identifiers will come from string values
 123 | ||| because ColumnIdentifier's `FromString` conformance allows Idris 2 to transform
 124 | ||| strings into ColumnIdentifiers. This allows for:
 125 | ||| - "table1.column1" = MkColumnId (Just $ Named "table1") "column1"
 126 | ||| - "column1" = MkColumnId Nothing "column1"
 127 | |||
 128 | ||| Table aliases here do not necessarily need to refer to a table that has
 129 | ||| been given a Postgres alias (a la "(select ...) AS an_alias"). A normal table
 130 | ||| or view name is appropriate and can be turned into an alias for use in a column
 131 | ||| identifier with the `toAlias` function.
 132 | public export
 133 | record ColumnIdentifier where
 134 |   constructor MkColumnId
 135 |   sourceTable : Maybe Alias
 136 |   name : String
 137 | 
 138 | public export
 139 | replaceSource : Maybe Alias -> ColumnIdentifier -> ColumnIdentifier
 140 | replaceSource newSource (MkColumnId _ name) = MkColumnId newSource name
 141 | 
 142 | public export
 143 | forgetSource : ColumnIdentifier -> ColumnIdentifier
 144 | forgetSource = replaceSource Nothing
 145 | 
 146 | public export
 147 | data AnonymousColumnIdentifier : ColumnIdentifier -> Type where
 148 |   Anon : AnonymousColumnIdentifier (MkColumnId Nothing _)
 149 | 
 150 | export
 151 | Show ColumnIdentifier where
 152 |   show (MkColumnId sourceTable name) = "\{maybeShowAliasColumnPrefix sourceTable}\{show . Id $ name}"
 153 | 
 154 | public export
 155 | FromString ColumnIdentifier where
 156 |   fromString str =
 157 |     case (split (== '.') str) of
 158 |       (column ::: []) => MkColumnId Nothing column
 159 |       (table ::: column@(x :: xs)) => MkColumnId (Just $ Named table) (joinBy "." column)
 160 |       -- ^ not great, just chooses not to handle x.y.z very well at all
 161 | 
 162 | ||| Some representation of a Postgres table.
 163 | public export
 164 | interface PostgresTable t where
 165 |   ||| A table name or subselect statement from which the following columns could be selected.
 166 |   tableStatement : t -> TableStatement
 167 |   ||| The columns this table offers. Column names should not include double quotes, even where they
 168 |   ||| are needed when written down in SQL statements.
 169 |   columns : t -> List (ColumnIdentifier, Exists PColType)
 170 |   ||| Set the alias on a table.
 171 |   as : t -> String -> t
 172 | 
 173 | export
 174 | infix 0 `as`
 175 | 
 176 | export
 177 | alias : PostgresTable t => (table : t) -> Maybe Alias
 178 | alias = tableAlias . tableStatement
 179 | 
 180 | ||| Get the alias or name of a table; prefer the alias, as a renamed table
 181 | ||| _should_ be referred to by its alias, but use the table's original name
 182 | ||| if one is available and there is no alias set.
 183 | public export
 184 | aliasOrName : PostgresTable t => (table : t) -> Maybe Alias
 185 | aliasOrName = map toAlias . tableAliasOrName . tableStatement
 186 | 
 187 | ||| A runtime representation of a table. These have string fields and table statements so as to not limit
 188 | ||| themselves to nominal postgres tables; you can also represent joins naturally where the table statement is
 189 | ||| a SELECT with a JOIN instead of just a table's name.
 190 | public export
 191 | record RuntimeTable where
 192 |   constructor RT
 193 |   tableStatement : TableStatement
 194 |   columns : List (ColumnIdentifier, Exists PColType)
 195 | 
 196 | public export
 197 | PostgresTable RuntimeTable where
 198 |   tableStatement = .tableStatement
 199 |   columns = .columns
 200 | 
 201 |   as (RT (Identifier str x) columns) a = 
 202 |     RT (Identifier str (Just $ Named a))
 203 |        (mapFst (replaceSource . Just $ Named a) <$> columns)
 204 |   as (RT (Subquery str x) columns) a = 
 205 |     RT (Subquery str (Named a))
 206 |        (mapFst (replaceSource . Just $ Named a) <$> columns)
 207 |   as (RT (Fragment str) columns) a = 
 208 |     RT (Subquery "SELECT * FROM \{str}" (Named a))
 209 |        (mapFst (replaceSource . Just $ Named a) <$> columns)
 210 | 
 211 | ||| A persisted table is an actual named (or view) table in the database.
 212 | public export
 213 | record PersistedTable where
 214 |   constructor PT
 215 |   tableName : String
 216 |   {default Nothing alias : Maybe Alias}
 217 |   columns : List (String, Exists PColType)
 218 | 
 219 | namespace PersistedTable
 220 |   public export
 221 |   aliasOrName : (table : PersistedTable) -> Alias
 222 |   aliasOrName (PT tableName {alias} columns) = maybe (toAlias $ Id tableName) id alias
 223 | 
 224 | public export
 225 | PostgresTable PersistedTable where
 226 |   columns table = mapFst (MkColumnId (Just . aliasOrName $ table)) <$> table.columns
 227 | 
 228 |   tableStatement (PT n {alias} _) = named n {alias}
 229 | 
 230 |   as (PT tableName columns) a = PT tableName {alias=Just $ Named a} columns
 231 | 
 232 | ||| Construct an existential column type from a Postgres type and its
 233 | ||| nullability.
 234 | public export
 235 | col : (nullable : Nullability) -> (pt : PType) -> Exists PColType
 236 | col nullable pt = Evidence pt (MkColType nullable pt)
 237 | 
 238 | ||| Construct a persisted table representation (a table name and the names,
 239 | ||| types, and nullabilities of the columns of a table.)
 240 | |||
 241 | ||| ```idris example
 242 | ||| myTable = table "table1" [ ("id"            , NonNullable, PInteger)
 243 | |||                          , ("name"          , NonNullable, PString)
 244 | |||                          , ("favorite_color", Nullable   , PString)
 245 | |||                          ]
 246 | ||| ```
 247 | public export
 248 | pgTable : (name : String) 
 249 |        -> (columns : List (String, Nullability, PType))
 250 |        -> PersistedTable
 251 | pgTable name columns = PT name (mapSnd (uncurry col) <$> columns)
 252 | 
 253 | ||| A mapping between a column name and Idris type to some element in a list of column identifiers
 254 | ||| and Postgres types. This mapping proves that the column identifiers exists and that the Postgres
 255 | ||| type for that column can be cast to the Idris type specified. This mapping allows for "loose"
 256 | ||| matches where the ColumnIdentifier being matched against does not specify a source table but the
 257 | ||| column name can be found in the list of columns given. Loose matching is only ok if the match would
 258 | ||| not succeed against multiple columns (Postgres will complain of ambiguity, for good reason). Use the
 259 | ||| ColumnMapping type to avoid loose matches.
 260 | public export
 261 | data LooseColumnMapping : (0 _ : PType -> Type -> Type)
 262 |                        -> List (ColumnIdentifier, Exists PColType)
 263 |                        -> (ColumnIdentifier, Type)
 264 |                        -> Type where
 265 |   HereNul       : (ident : ColumnIdentifier) -> (ty : Type) -> castTy pt ty => LooseColumnMapping castTy ((ident, (Evidence pt (MkColType Nullable pt))) :: xs) (ident, Maybe ty)
 266 |   HereNulLoose  : (columnName : String) -> (ty : Type) -> castTy pt ty => LooseColumnMapping castTy ((MkColumnId _ columnName, (Evidence pt (MkColType Nullable pt))) :: xs) (MkColumnId Nothing columnName, Maybe ty)
 267 |   Here          : (ident : ColumnIdentifier) -> (ty : Type) -> castTy pt ty => LooseColumnMapping castTy ((ident, (Evidence pt (MkColType NonNullable pt))) :: xs) (ident, ty)
 268 |   HereLoose     : (columnName : String) -> (ty : Type) -> castTy pt ty => LooseColumnMapping castTy ((MkColumnId _ columnName, (Evidence pt (MkColType NonNullable pt))) :: xs) (MkColumnId Nothing columnName, ty)
 269 |   There         : LooseColumnMapping castTy xs (ident, ty) -> LooseColumnMapping castTy (x :: xs) (ident, ty)
 270 | 
 271 | public export
 272 | HasLooseMappings : {n : _} 
 273 |                 -> (0 castTy : PType -> Type -> Type)
 274 |                 -> PostgresTable t => 
 275 |                    (table : t)
 276 |                 -> (cols : Vect n (ColumnIdentifier, Type))
 277 |                 -> Type
 278 | HasLooseMappings castTy table cols = All (LooseColumnMapping castTy (columns table)) cols
 279 | 
 280 | namespace Strict
 281 |   ||| A mapping between a column name and Idris type to some element in a list of column identifiers
 282 |   ||| and Postgres types. This mapping proves that the column identifiers exists and that the Postgres
 283 |   ||| type for that column can be cast to the Idris type specified.
 284 |   public export
 285 |   data ColumnMapping : (0 _ : PType -> Type -> Type)
 286 |                     -> List (ColumnIdentifier, Exists PColType)
 287 |                     -> (ColumnIdentifier, Type)
 288 |                     -> Type where
 289 |     HereNul       : (ident : ColumnIdentifier) -> (ty : Type) -> castTy pt ty => ColumnMapping castTy ((ident, (Evidence pt (MkColType Nullable pt))) :: xs) (ident, Maybe ty)
 290 |     Here          : (ident : ColumnIdentifier) -> (ty : Type) -> castTy pt ty => ColumnMapping castTy ((ident, (Evidence pt (MkColType NonNullable pt))) :: xs) (ident, ty)
 291 |     There         : ColumnMapping castTy xs (ident, ty) -> ColumnMapping castTy (x :: xs) (ident, ty)
 292 | 
 293 |   public export
 294 |   HasMappings : {n : _} 
 295 |              -> (0 castTy : PType -> Type -> Type)
 296 |              -> PostgresTable t =>
 297 |                 (table : t)
 298 |              -> (cols : Vect n (ColumnIdentifier, Type))
 299 |              -> Type
 300 |   HasMappings castTy table cols = All (ColumnMapping castTy (columns table)) cols
 301 | 
 302 | toString : LooseColumnMapping PGCast table (colName, colType) -> colType -> String
 303 | toString (HereNul name ty @{prf}) = \case Nothing => "null"; Just x => rawString $ toPostgres @{prf} x
 304 | toString (HereNulLoose name ty @{prf}) = \case Nothing => "null"; Just x => rawString $ toPostgres @{prf} x
 305 | toString (Here name ty @{prf}) = rawString . toPostgres @{prf}
 306 | toString (HereLoose name ty @{prf}) = rawString . toPostgres @{prf}
 307 | toString (There y) = toString y
 308 | 
 309 | ||| Create a select statement based on the columns you would like to grab from the
 310 | ||| given table.
 311 | public export
 312 | select : PostgresTable t => 
 313 |          (table : t)
 314 |       -> (cols : Vect n (ColumnIdentifier, Type))
 315 |       -> (0 _ : HasMappings IdrCast table cols) =>
 316 |          String
 317 | select table cols =
 318 |   let tableStatement = show $ tableStatement table
 319 |       columnNames    = joinBy "," $ show . fst <$> (toList cols)
 320 |   in  "SELECT \{columnNames} FROM \{tableStatement}"
 321 | 
 322 | ||| Insert the given values into the given columns of a new row in the given table.
 323 | public export
 324 | insert : {n : _}
 325 |       -> (table : PersistedTable)
 326 |       -> (cols : Vect n ColumnIdentifier)
 327 |       -> {colTypes : Vect n Type}
 328 |       -> (values : HVect colTypes)
 329 |       -> HasLooseMappings PGCast table (zip cols colTypes) =>
 330 |          String
 331 | insert table cols vs @{mappings} =
 332 |   let tableIdentifier = show $ Id table.tableName
 333 |       columnNames     = (strCons '(' (joinBy "," $ show . .name <$> (toList cols))) ++ ")"
 334 |       values          = values table cols vs
 335 |       valueStrings    = (strCons '(' (joinBy "," $ values)) ++ ")"
 336 |   in  "INSERT INTO \{tableIdentifier} \{columnNames} VALUES \{valueStrings}"
 337 |   where
 338 |     values : {l : _} 
 339 |           -> (table : PersistedTable)
 340 |           -> (cols : Vect l ColumnIdentifier)
 341 |           -> {colTypes : Vect l Type}
 342 |           -> (values : HVect colTypes)
 343 |           -> HasLooseMappings PGCast table (zip cols colTypes) =>
 344 |              List String
 345 |     values table [] [] = []
 346 |     values table (x :: xs) (v :: vs) @{m :: ms} = toString m v :: values table xs vs @{ms}
 347 | 
 348 | public export
 349 | data Join : t1 -> t2 -> Type where
 350 |   On : PostgresTable t => PostgresTable u => {t1 : t} -> {t2 : u} -> (c1 : ColumnIdentifier) -> (c2 : ColumnIdentifier) -> (0 _ : Elem c1 (Builtin.fst <$> (columns t1))) => (0 _ : Elem c2 (Builtin.fst <$> (columns t2))) => Join t1 t2
 351 | 
 352 | public export
 353 | HasOnMapping : ColumnIdentifier -> PostgresTable t => (table : t) -> Type
 354 | HasOnMapping c table = Either (Elem c (fst <$> (columns table))) (AnonymousColumnIdentifier c, Elem (replaceSource (aliasOrName table) c) (fst <$> (columns table)))
 355 | 
 356 | public export
 357 | elemForOnMapping : PostgresTable t =>
 358 |                    (table : t)
 359 |                 -> (c : ColumnIdentifier)
 360 |                 -> HasOnMapping c table
 361 |                 -> (c' ** Elem c' (Builtin.fst <$> (columns table)))
 362 | elemForOnMapping table c (Left m) = (c ** m)
 363 | elemForOnMapping table c (Right (_, m)) = (replaceSource (aliasOrName table) c ** m)
 364 | 
 365 | ||| In a join-statement, produce the clause that links the two tables together by
 366 | ||| a shared column. In pseudo-code: "table1 join table2 'on' col1 = col2".
 367 | |||
 368 | ||| ```idris example
 369 | ||| innerJoin' table1 table2 ("col_from_table1" == "col_from_table2")
 370 | ||| ```
 371 | public export
 372 | (==) : PostgresTable t => 
 373 |        PostgresTable u =>
 374 |        {t1 : t}
 375 |     -> {t2 : u}
 376 |     -> (c1 : ColumnIdentifier)
 377 |     -> (c2 : ColumnIdentifier)
 378 |     -> {auto on1 : HasOnMapping c1 t1}
 379 |     -> {auto on2 : HasOnMapping c2 t2}
 380 |     -> Join t1 t2
 381 | (==) c1 c2 {on1} {on2} with (elemForOnMapping t1 c1 on1, elemForOnMapping t2 c2 on2)
 382 |   (==) c1 c2 {on1} {on2} | ((c1' ** on1'), (c2' ** on2')) = On c1' c2'
 383 | 
 384 | namespace Join
 385 |   public export
 386 |   column1 : Join t u -> ColumnIdentifier
 387 |   column1 (On c1 c2) = c1
 388 | 
 389 |   public export
 390 |   column2 : Join t u -> ColumnIdentifier
 391 |   column2 (On c1 c2) = c2
 392 | 
 393 | ||| Construct a runtime table by inner-joining two other tables on a specified column.
 394 | |||
 395 | ||| ```idris example
 396 | ||| innerJoin' table1 table2 ("col_from_table1" == "col_from_table2")
 397 | ||| ```
 398 | public export
 399 | innerJoin' : PostgresTable t => (table1 : t) -> PostgresTable u => (table2 : u) -> (on : Join table1 table2) -> RuntimeTable
 400 | innerJoin' table1 table2 joinOn = 
 401 |   let table1Statement = show $ tableStatement table1
 402 |       table2Statement = show $ tableStatement table2
 403 |       table1JoinName = show $ column1 joinOn
 404 |       table2JoinName = show $ column2 joinOn
 405 |       subquery = "\{table1Statement} JOIN \{table2Statement} ON \{table1JoinName} = \{table2JoinName}"
 406 |       table1Cols = columns table1
 407 |       table2Cols = columns table2
 408 |   in  RT (Fragment subquery) (table1Cols ++ table2Cols)
 409 | 
 410 | ||| Construct a runtime table by left-joining two other tables on a specified column.
 411 | |||
 412 | ||| ```idris example
 413 | ||| leftJoin' table1 table2 ("col_from_table1" == "col_from_table2")
 414 | ||| ```
 415 | public export 
 416 | leftJoin' : PostgresTable t => (table1 : t) -> PostgresTable u => (table2 : u) -> (on : Join table1 table2) -> RuntimeTable
 417 | leftJoin' table1 table2 joinOn =
 418 |   let table1Statement = show $ tableStatement table1
 419 |       table2Statement = show $ tableStatement table2
 420 |       table1JoinName = show $ column1 joinOn
 421 |       table2JoinName = show $ column2 joinOn
 422 |       subquery = "\{table1Statement} LEFT JOIN \{table2Statement} ON \{table1JoinName} = \{table2JoinName}"
 423 |       table1Cols = columns table1
 424 |       table2Cols = mapSnd (bimap (\t => t) makeNullable) <$> columns table2
 425 |       -- ^ need to make table2's columns possibly null because of the left-join.
 426 |   in  RT (Fragment subquery) (table1Cols ++ table2Cols)
 427 | 
 428 | ||| Construct a runtime table by right-joining two other tables on a specified column.
 429 | |||
 430 | ||| ```idris example
 431 | ||| rightJoin' table1 table2 ("col_from_table1" == "col_from_table2")
 432 | ||| ```
 433 | public export 
 434 | rightJoin' : PostgresTable t => (table1 : t) -> PostgresTable u => (table2 : u) -> (on : Join table1 table2) -> RuntimeTable
 435 | rightJoin' table1 table2 joinOn =
 436 |   let table1Statement = show $ tableStatement table1
 437 |       table2Statement = show $ tableStatement table2
 438 |       table1JoinName = show $ column1 joinOn
 439 |       table2JoinName = show $ column2 joinOn
 440 |       subquery = "\{table1Statement} LEFT JOIN \{table2Statement} ON \{table1JoinName} = \{table2JoinName}"
 441 |       table1Cols = mapSnd (bimap (\t => t) makeNullable) <$> columns table1
 442 |       -- ^ need to make table1's columns possibly null because of the right-join.
 443 |       table2Cols = columns table2
 444 |   in  RT (Fragment subquery) (table1Cols ++ table2Cols)
 445 | 
 446 | public export
 447 | data JoinType = Inner | Left | Right
 448 | 
 449 | public export
 450 | data TablePair : table1 -> table2 -> Type where
 451 |   MkTP : JoinType -> PostgresTable t => PostgresTable u => (table1 : t) -> (table2 : u) -> TablePair table1 table2
 452 | 
 453 | ||| Inner-join two tables.
 454 | ||| This produces a pair of tables and a join strategy. You then need to use `onColumns` to take the table pair
 455 | ||| and add the columns that the join should occur over.
 456 | public export
 457 | innerJoin : PostgresTable t => PostgresTable u => (table1 : t) -> (table2 : u) -> TablePair table1 table2
 458 | innerJoin = MkTP Inner
 459 | 
 460 | ||| Left-join two tables.
 461 | ||| This produces a pair of tables and a join strategy. You then need to use `onColumns` to take the table pair
 462 | ||| and add the columns that the join should occur over.
 463 | public export
 464 | leftJoin : PostgresTable t => PostgresTable u => (table1 : t) -> (table2 : u) -> TablePair table1 table2
 465 | leftJoin = MkTP Left
 466 | 
 467 | ||| Right-join two tables.
 468 | ||| This produces a pair of tables and a join strategy. You then need to use `onColumns` to take the table pair
 469 | ||| and add the columns that the join should occur over.
 470 | public export
 471 | rightJoin : PostgresTable t => PostgresTable u => (table1 : t) -> (table2 : u) -> TablePair table1 table2
 472 | rightJoin = MkTP Right
 473 | 
 474 | ||| Given that you've already paired two tables up (see `innerJoin`, `leftJoin`, `rightJoin`)
 475 | ||| you use `onColumns` to specify which columns from each table in the pair should be equal
 476 | ||| in the joined table. The end result is a new table.
 477 | |||
 478 | ||| Psuedo-example:
 479 | |||   table1 `innerJoin` table2 `onColumns` ("table1.col1" == "table2.col2")
 480 | public export
 481 | onColumns : TablePair table1 table2 -> Join table1 table2 -> RuntimeTable
 482 | onColumns (MkTP Inner table1 table2) joinOn = innerJoin' table1 table2 joinOn
 483 | onColumns (MkTP Left table1 table2) joinOn = leftJoin' table1 table2 joinOn
 484 | onColumns (MkTP Right table1 table2) joinOn = rightJoin' table1 table2 joinOn
 485 | 
 486 | export
 487 | infixl 10 `innerJoin`, `leftJoin`, `rightJoin`, `onColumns`
 488 | 
 489 | mappingCastable : {cs : _} -> ColumnMapping IdrCast cs (ident, ty) => Castable ty
 490 | mappingCastable {cs = ((ident, Evidence pt (MkColType Nullable pt)) :: xs)} @{(HereNul ident x @{sc})} = CastMaybe @{IdrCastString {pt}}
 491 | mappingCastable {cs = ((ident, Evidence pt (MkColType NonNullable pt)) :: xs)} @{(Here ident ty @{sc})} = Cast @{IdrCastString {pt}}
 492 | mappingCastable {cs = (x :: xs)} @{(There y)} = mappingCastable {cs=xs} @{y}
 493 | 
 494 | export
 495 | allCastable : PostgresTable t => {n : _} -> (table : t) -> {cols : Vect n _} -> HasMappings IdrCast table cols => All Castable (Builtin.snd <$> cols)
 496 | allCastable @{_} table {cols = []} @{[]} = []
 497 | allCastable @{_} table {cols = ((x, y) :: xs)} @{(m :: ms)} = (mappingCastable @{m}) :: allCastable table {cols=xs}
 498 | 
 499 |