[ new ] pretty tables with column headers

docs/src/README.md

@@ -29,16 +29,16 @@ while each unit has a supervisor, who are themselves employees:
 
 ```idris
 public export
-Units : Table
+Units : SQLTable
 Units =
   table "units"
-  [ C "unit_id" INTEGER
-  , C "name"    TEXT
-  , C "head"    INTEGER
-  ]
+    [ C "unit_id" INTEGER
+    , C "name"    TEXT
+    , C "head"    INTEGER
+    ]
 
 public export
-Employees : Table
+Employees : SQLTable
 Employees =
   table "employees"
     [ C "employee_id" INTEGER
@@ -245,10 +245,11 @@ app = withDB ":memory:" $ do
     , insertEmployee $ E "Valeri" 5010.0 1
     , insertEmployee $ E "Ronja" 4010.0 1
     ]
-  es <- query employee 1000
-  traverse_ printLn es
-  ss <- query unitStats 1000
-  traverse_ printLn ss
+  putStrLn "\nEmployees:"
+  queryTable employee 1000 >>= printTable
+
+  putStrLn "\nUnit stats:"
+  queryTable unitStats 1000 >>= printTable
 
 main : IO ()
 main = runApp handlers app

docs/src/Tutorial.md

@@ -64,7 +64,7 @@ basic:
 
 ```idris
 public export
-Students : Table
+Students : SQLTable
 Students =
   table "students"
     [ C "student_id" INTEGER
@@ -73,7 +73,7 @@ Students =
     ]
 ```
 
-As you can see, a `Table` consists of a name and a list of columns,
+As you can see, a `SQLTable` consists of a name and a list of columns,
 where each column again has a name and an associated SQLite type.
 
 Actually, a table is a record of three field, where the third field
@@ -85,7 +85,7 @@ Here are the other tables we are going to use:
 
 ```idris
 public export
-Problems : Table
+Problems : SQLTable
 Problems =
   table "problems"
     [ C "problem_id"   INTEGER
@@ -94,7 +94,7 @@ Problems =
     ]
 
 public export
-Exams : Table
+Exams : SQLTable
 Exams =
   table "exams"
     [ C "exam_id"      INTEGER
@@ -104,15 +104,15 @@ Exams =
     ]
 
 public export
-ExamProblems : Table
+ExamProblems : SQLTable
 ExamProblems =
   table "exam_problems"
     [ C "problem_id"   INTEGER
     , C "exam_id"      INTEGER
     ]
 
 public export
-StudentProblems : Table
+StudentProblems : SQLTable
 StudentProblems =
   table "student_problems"
     [ C "problem_id"   INTEGER
@@ -164,7 +164,7 @@ a data constructor or function, so that the commands and expressions
 we write in Idris typically resemble the corresponding SQL expressions
 quite closely.
 
-Besides a `Table` argument, `CREATE_TABLE` takes a list of
+Besides a `SQLTable` argument, `CREATE_TABLE` takes a list of
 table constraints of type `Sqlite3.Cmd.Constraint`, which is indexed by
 the table for which we define the constraints. And this is where the
 interesting stuff begins: Whenever we use a string literal to identify
@@ -289,7 +289,7 @@ by the default proof search limit: We can lookup names in very
 large lists of columns. For instance:
 
 ```idris
-Tbl : Table
+Tbl : SQLTable
 Tbl =
   table "foo" $
     map (\n => C (prim__cast_Bits8String n) INTEGER) [0..55]
@@ -316,7 +316,7 @@ but this is what we currently have.
 
 In addition to `ListColType`, there is also function
 `TableColType`, which does exactly the same thing but for
-the columns wrapped up in a value of type `Table`. The
+the columns wrapped up in a value of type `SQLTable`. The
 interesting thing is, that we can now define a data type
 for typed column names (called `Sqlite3.Table.TColumn`),
 that represents a column in a table indexed by the column's
@@ -374,7 +374,7 @@ necessary to achieve similar results.
 Once one understands how name resolution behaves for columns
 and tables, it is only a small step to understanding name
 resolution for column names in schemata. A `Schema` is just
-a type alias for `SnocList Table`. We use a `SnocList` here
+a type alias for `SnocList SQLTable`. We use a `SnocList` here
 instead of a `List`, because when defining a query via a
 `SELECT` statement, the schema is assembled from left to
 right via the `FROM` part and possibly via any named
@@ -409,7 +409,7 @@ unqualifiedName1 = "email"
 
 -- using an unqualified name in a schema with an unnamed table
 -- at the end is OK
-unqualifiedName2 : Expr [<Students,T "" "" [C "total" REAL]] REAL
+unqualifiedName2 : Expr [<Students, ST "" "" [C "total" REAL]] REAL
 unqualifiedName2 = "total"
 ```
 
@@ -1185,25 +1185,20 @@ app =
     putStrLn "Populating the database"
     populateDB
 
-    putStrLn "\nMissing problem points"
-    ips <- query invalidPoints 1000
-    putStrLn $ printRows ips
+    putStrLn "\nInvalid problem points"
+    queryTable invalidPoints 1000 >>= printTable
 
     putStrLn "\nInvalid email addresses"
-    email <- query invalidEmail 1000
-    putStrLn $ printRows email
+    queryTable invalidEmail 1000 >>= printTable
 
     putStrLn "\nStudent-problem combos without points:"
-    nps <- query noPointsYet 1000
-    putStrLn $ printRows nps
+    queryTable noPointsYet 1000 >>= printTable
 
     putStrLn "\nPoints per student and exam:"
-    tot <- query totPoints 1000
-    putStrLn $ printRows tot
+    queryTable totPoints 1000 >>= printTable
 
     putStrLn "\nFailed exams:"
-    failed <- query failed 1000
-    putStrLn $ printRows failed
+    queryTable failed 1000 >>= printTable
 ```
 
 All that's left to do is to provide the actual `main` function.

pack.toml

@@ -13,3 +13,9 @@ ipkg   = "sqlite3-rio.ipkg"
 type   = "local"
 path   = "docs"
 ipkg   = "docs.ipkg"
+
+[custom.all.quantifiers-extra]
+type   = "git"
+url    = "https://github.com/stefan-hoeck/idris2-quantifiers-extra"
+commit = "latest:main"
+ipkg   = "quantifiers-extra.ipkg"

sqlite3-rio/src/Control/RIO/Sqlite3.idr

@@ -114,6 +114,23 @@ parameters {auto has : Has SqlError es}
       runCommands []      = pure ()
       runCommands (c::cs) = cmd c >> runCommands cs
 
+  ||| Runs the given query and accumulates at most `n` rows.
   export %inline
-  query : {auto db : DB} -> Query t -> Nat -> App es (List t)
+  query : DB => Query t -> (n : Nat) -> App es (List t)
   query q = selectRows (encodeQuery q)
+
+  ||| Runs the given query and accumulates at most `n` rows.
+  |||
+  ||| The result is stored in a `Table` with a proper header of
+  ||| column names.
+  export
+  queryTable :
+       {auto db : DB}
+    -> {auto tr : ToRow t}
+    -> (q : Query t)
+    -> {auto 0 prf : ToRowTypes t === FromRowTypes t}
+    -> Nat
+    -> App es (Table t)
+  queryTable {prf} q n = do
+    rs <- query q n
+    pure (T (rewrite prf in hmap columnName q.columns) rs)

sqlite3.ipkg

@@ -8,6 +8,7 @@ brief        = "Idris2 bindings to the sqlite3 API"
 depends = base >= 0.6.0
         , elab-util
         , bytestring
+        , quantifiers-extra
 
 sourcedir = "src"
 

src/Sqlite3/Cmd.idr

@@ -19,7 +19,7 @@ toExprs {ts = t::ts} (v::vs) = maybe NULL (Lit t) v :: toExprs vs
 
 ||| A single name-value pair in an `UPDATE` statement.
 public export
-record Val (t : Table) where
+record Val (t : SQLTable) where
   constructor V
   name        : String
   {auto 0 prf : IsJust (FindCol name t.cols)}
@@ -30,7 +30,7 @@ record Val (t : Table) where
 ||| `ToCell` implementation.
 public export %inline
 (.=) :
-     {0 t        : Table}
+     {0 t        : SQLTable}
   -> {auto to    : ToCell a}
   -> (name       : String)
   -> {auto 0 prf : IsJust (FindCol name t.cols)}
@@ -41,21 +41,21 @@ public export %inline
 
 ||| Column and table constraints to be used when creating a new table.
 public export
-data Constraint : Table -> Type where
+data Constraint : SQLTable -> Type where
   NOT_NULL      : {0 x : _} -> TColumn t x -> Constraint t
   AUTOINCREMENT : {0 x : _} -> TColumn t x -> Constraint t
   UNIQUE        : {0 xs : _} -> LAll (TColumn t) xs -> Constraint t
   PRIMARY_KEY   : {0 xs : _} -> LAll (TColumn t) xs -> Constraint t
   FOREIGN_KEY   :
        {0 xs : _}
-    -> (s       : Table)
+    -> (s       : SQLTable)
     -> LAll (TColumn t) xs
     -> LAll (TColumn s) xs
     -> Constraint t
 
   CHECK         : Expr [<t] BOOL -> Constraint t
   DEFAULT       :
-       {0 t        : Table}
+       {0 t        : SQLTable}
     -> (s          : String)
     -> {auto 0 prf : IsJust (FindCol s t.cols)}
     -> (expr       : Expr [<t] (TableColType s t))
@@ -83,12 +83,12 @@ data Cmd : CmdType -> Type where
   ||| It is recommended to use a combination of `CREATE_TABLE` and
   ||| `IF_NOT_EXISTS` instead of using this constructor directly.
   CreateTable :
-       (t           : Table)
+       (t           : SQLTable)
     -> (attrs       : List (Constraint t))
     -> (ifNotExists : Bool)
     -> Cmd TCreate
 
-  DropTable : (t : Table) -> (ifExists : Bool) -> Cmd TDrop
+  DropTable : (t : SQLTable) -> (ifExists : Bool) -> Cmd TDrop
 
   ||| Information required to insert data into a table.
   |||
@@ -98,7 +98,7 @@ data Cmd : CmdType -> Type where
   ||| consider using function `insert` instead.
   INSERT :
        {0 ts : List SqliteType}
-    -> (t    : Table)
+    -> (t    : SQLTable)
     -> (cols : LAll (TColumn t) ts)
     -> (vals : LAll (Expr [<t]) ts)
     -> Cmd TInsert
@@ -115,21 +115,21 @@ data Cmd : CmdType -> Type where
   ||| consider using function `replace` instead.
   REPLACE :
        {0 ts : List SqliteType}
-    -> (t : Table)
+    -> (t : SQLTable)
     -> (cols : LAll (TColumn t) ts)
     -> (vals : LAll (Expr [<t]) ts)
     -> Cmd TInsert
 
   ||| Information required to update values in table.
   UPDATE :
-       (t      : Table)
+       (t      : SQLTable)
     -> (set    : List (Val t))
     -> (where_ : Expr [<t] BOOL)
     -> Cmd TUpdate
 
   ||| Information required to delete values from a table.
   DELETE :
-       (t      : Table)
+       (t      : SQLTable)
     -> (where_ : Expr [<t] BOOL)
     -> Cmd TDelete
 
@@ -138,7 +138,7 @@ data Cmd : CmdType -> Type where
 export
 insert :
     {auto as : ToRow v}
-  ->(t       : Table)
+  ->(t       : SQLTable)
   -> LAll (TColumn t) (ToRowTypes v)
   -> (value : v)
   -> Cmd TInsert
@@ -149,7 +149,7 @@ insert t cs value = INSERT t cs (toExprs $ toRow value)
 export
 replace :
     {auto as : ToRow v}
-  ->(t       : Table)
+  ->(t       : SQLTable)
   -> LAll (TColumn t) (ToRowTypes v)
   -> (value : v)
   -> Cmd TInsert
@@ -191,37 +191,37 @@ IF_EXISTS (DropTable t _) = DropTable t True
 
 ||| Convenience constructor for the `CreateTable` command
 public export %inline
-CREATE_TABLE : (t : Table) -> List (Constraint t) -> Cmd TCreate
+CREATE_TABLE : (t : SQLTable) -> List (Constraint t) -> Cmd TCreate
 CREATE_TABLE t as = CreateTable t as False
 
 ||| Convenience constructor for the `DropTable` command
 public export %inline
-DROP_TABLE : (t : Table) -> Cmd TDrop
+DROP_TABLE : (t : SQLTable) -> Cmd TDrop
 DROP_TABLE t = DropTable t False
 
 public export
-0 JoinPred : Schema -> Table -> Type
+0 JoinPred : Schema -> SQLTable -> Type
 JoinPred s t = Either (List $ JColumn  s t) (Expr (s:<t) BOOL)
 
 public export
-data Join : (s : Schema) -> (t : Table) -> Type where
+data Join : (s : Schema) -> (t : SQLTable) -> Type where
   JOIN :
-       {0 t0 : Table}
+       {0 t0 : SQLTable}
     -> {0 s  : Schema}
-    -> (t : Table)
+    -> (t : SQLTable)
     -> JoinPred (s:<t0) t
     -> Join (s:<t0) t
 
   OUTER_JOIN :
-       {0 t0 : Table}
+       {0 t0 : SQLTable}
     -> {0 s  : Schema}
-    -> (t : Table)
+    -> (t : SQLTable)
     -> JoinPred (s:<t0) t
     -> Join (s:<t0) t
 
-  CROSS_JOIN : {0 t0 : _} -> {0 s : _} -> (t : Table) -> Join (s:<t0) t
+  CROSS_JOIN : {0 t0 : _} -> {0 s : _} -> (t : SQLTable) -> Join (s:<t0) t
 
-  FROM : (t : Table) -> Join [<] t
+  FROM : (t : SQLTable) -> Join [<] t
 
 public export %inline
 USING : (JoinPred s t -> Join s t) -> List (JColumn s t) -> Join s t
@@ -305,6 +305,17 @@ namespace NameExpr
     -> NamedExpr s (SchemaColType col s)
   fromString col = Col col `AS` ""
 
+||| Extracts the column name we use to reference a named
+||| expression.
+|||
+||| If a custom name has been set, this will be returned. Otherwise,
+||| if the expression references a table column, that columns (possibly
+||| qualified) name will be returned.
+export
+columnName : NamedExpr s t -> String
+columnName (AS (Col col) "") = col
+columnName (AS _         n)  = n
+
 ||| Computes a list of named and typed columns from a list of
 ||| name expressions.
 |||
@@ -330,7 +341,7 @@ ExprSchema : {s : _} -> {ts : _} -> LAll (NamedExpr s) ts -> Schema
 ExprSchema xs =
   case ExprColumns xs of
     [] => s
-    cs => s :< T "" "" cs
+    cs => s :< ST "" "" cs
 
 ||| Different types of `SELECT` commands.
 public export