From fba6ea11cdbf23902a1ac4f3e6a9375bf8540d4a Mon Sep 17 00:00:00 2001 From: stefan-hoeck Date: Thu, 16 Nov 2023 08:08:37 +0100 Subject: [PATCH] [ new ] pretty tables with column headers --- docs/src/README.md | 21 ++-- docs/src/Tutorial.md | 39 +++--- pack.toml | 6 + sqlite3-rio/src/Control/RIO/Sqlite3.idr | 19 ++- sqlite3.ipkg | 1 + src/Sqlite3/Cmd.idr | 59 +++++---- src/Sqlite3/Marshall.idr | 98 +-------------- src/Sqlite3/Parameter.idr | 6 +- src/Sqlite3/Table.idr | 152 +++++++++++++++++++++--- test/src/Main.idr | 22 ++-- test/src/Schema.idr | 22 ++-- 11 files changed, 246 insertions(+), 199 deletions(-) diff --git a/docs/src/README.md b/docs/src/README.md index ed6d176..e21be4e 100644 --- a/docs/src/README.md +++ b/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 diff --git a/docs/src/Tutorial.md b/docs/src/Tutorial.md index a4fb5ce..e0d24f3 100644 --- a/docs/src/Tutorial.md +++ b/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,7 +104,7 @@ Exams = ] public export -ExamProblems : Table +ExamProblems : SQLTable ExamProblems = table "exam_problems" [ C "problem_id" INTEGER @@ -112,7 +112,7 @@ ExamProblems = ] 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 [>= 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. diff --git a/pack.toml b/pack.toml index 392c4db..0a785e9 100644 --- a/pack.toml +++ b/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" diff --git a/sqlite3-rio/src/Control/RIO/Sqlite3.idr b/sqlite3-rio/src/Control/RIO/Sqlite3.idr index 8364628..9e8a3bb 100644 --- a/sqlite3-rio/src/Control/RIO/Sqlite3.idr +++ b/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) diff --git a/sqlite3.ipkg b/sqlite3.ipkg index 14caf86..16227a8 100644 --- a/sqlite3.ipkg +++ b/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" diff --git a/src/Sqlite3/Cmd.idr b/src/Sqlite3/Cmd.idr index 11e05e7..38a867f 100644 --- a/src/Sqlite3/Cmd.idr +++ b/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 [ Constraint t DEFAULT : - {0 t : Table} + {0 t : SQLTable} -> (s : String) -> {auto 0 prf : IsJust (FindCol s t.cols)} -> (expr : Expr [ 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 [ 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 [ Cmd TInsert ||| Information required to update values in table. UPDATE : - (t : Table) + (t : SQLTable) -> (set : List (Val t)) -> (where_ : Expr [ Cmd TUpdate ||| Information required to delete values from a table. DELETE : - (t : Table) + (t : SQLTable) -> (where_ : Expr [ 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 : 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: Join (s: {0 s : Schema} - -> (t : Table) + -> (t : SQLTable) -> JoinPred (s: Join (s: {0 s : _} -> (t : Table) -> Join (s: {0 s : _} -> (t : SQLTable) -> Join (s: 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 diff --git a/src/Sqlite3/Marshall.idr b/src/Sqlite3/Marshall.idr index 3838a3f..cd6bed8 100644 --- a/src/Sqlite3/Marshall.idr +++ b/src/Sqlite3/Marshall.idr @@ -6,7 +6,7 @@ import Data.ByteString import Data.String import Data.Vect import Sqlite3.Types -import public Data.List.Quantifiers +import public Data.List.Quantifiers.Extra %default total @@ -352,99 +352,3 @@ splitAll [] [] = [] splitAll (xs :: xss) ys = let (zs,r) := splitAt xs ys in zs :: splitAll xss r - --------------------------------------------------------------------------------- --- Printing Tables --------------------------------------------------------------------------------- - -hexChar : Bits8 -> Char -hexChar 0 = '0' -hexChar 1 = '1' -hexChar 2 = '2' -hexChar 3 = '3' -hexChar 4 = '4' -hexChar 5 = '5' -hexChar 6 = '6' -hexChar 7 = '7' -hexChar 8 = '8' -hexChar 9 = '9' -hexChar 10 = 'a' -hexChar 11 = 'b' -hexChar 12 = 'c' -hexChar 13 = 'd' -hexChar 14 = 'e' -hexChar _ = 'f' - -export %inline -quote : Char -quote = '\'' - -||| Encodes a `ByteString` as an SQL literal. -||| -||| Every byte is encodec with two hexadecimal digits, and the -||| whole string is wrapped in single quotes prefixed with an "X". -||| -||| For instance, `encodeBytes (fromList [0xa1, 0x77])` yields the -||| string "X'a177'". -export -encodeBytes : ByteString -> String -encodeBytes = pack . (\x => 'X'::quote::x) . foldr acc [quote] - where - %inline acc : Bits8 -> List Char -> List Char - acc b cs = hexChar (b `shiftR` 4) :: hexChar (b .&. 0xf) :: cs - -encode : (t : SqliteType) -> Maybe (IdrisType t) -> String -encode _ Nothing = "NULL" -encode BLOB (Just v) = encodeBytes v -encode TEXT (Just v) = v -encode INTEGER (Just v) = show v -encode REAL (Just v) = show v - -pad : SqliteType -> Nat -> String -> String -pad BLOB k = padRight k ' ' -pad TEXT k = padRight k ' ' -pad INTEGER k = padLeft k ' ' -pad REAL k = padLeft k ' ' - -export -printTable : - (ts : List SqliteType) - -> List (LAll (Maybe . IdrisType) ts) - -> String -printTable ts vs = - let cells := map (printRow ts) vs - lengths := foldl maxLengths (zeros ts) cells - rows := map (alignColumns [<] ts lengths) cells - in fastUnlines rows - - where - zeros : (xs : List SqliteType) -> LAll (Prelude.const Nat) xs - zeros [] = [] - zeros (_ :: xs) = 0 :: zeros xs - - printRow : - (xs : List SqliteType) - -> LAll (Maybe . IdrisType) xs - -> LAll (Prelude.const String) xs - printRow [] [] = [] - printRow (x :: xs) (y::ys) = encode x y :: printRow xs ys - - maxLengths : - LAll (Prelude.const Nat) xs - -> LAll (Prelude.const String) xs - -> LAll (Prelude.const Nat) xs - maxLengths = zipPropertyWith (\n,s => max n $ length s) - - alignColumns : - SnocList String - -> (xs : List SqliteType) - -> LAll (Prelude.const Nat) xs - -> LAll (Prelude.const String) xs - -> String - alignColumns ss [] [] [] = fastConcat . intersperse " | " $ ss <>> [] - alignColumns ss (x :: xs) (y::ys) (z::zs) = - alignColumns (ss :< pad x y z) xs ys zs - -export -printRows : ToRow a => List a -> String -printRows = printTable (ToRowTypes a) . map toRow diff --git a/src/Sqlite3/Parameter.idr b/src/Sqlite3/Parameter.idr index 72bfe4d..df7a83f 100644 --- a/src/Sqlite3/Parameter.idr +++ b/src/Sqlite3/Parameter.idr @@ -162,7 +162,7 @@ names sc (TC c :: cs) = names (sc :< c) cs encodeDflt : Expr s t -> String encodeDflt x = "DEFAULT (\{encodeExpr x})" -references : (t : Table) -> LAll (TColumn t) xs -> String +references : (t : SQLTable) -> LAll (TColumn t) xs -> String references t cs = "REFERENCES \{t.name} (\{names [<] cs})" encConstraint : Constraints -> Constraint t -> Constraints @@ -252,8 +252,8 @@ joinPred (Right x) = do ez <- encodeExprP x pure "ON \{ez}" -tbl : Table -> String -tbl (T n a _) = if n == a then n else "\{n} AS \{a}" +tbl : SQLTable -> String +tbl (ST n a _) = if n == a then n else "\{n} AS \{a}" join : Join s t -> ParamStmt join (JOIN t p) = do diff --git a/src/Sqlite3/Table.idr b/src/Sqlite3/Table.idr index 7599133..118fa94 100644 --- a/src/Sqlite3/Table.idr +++ b/src/Sqlite3/Table.idr @@ -4,10 +4,18 @@ import public Data.List1 import public Data.Maybe import public Data.SnocList import public Data.String +import Data.Bits +import Data.Buffer.Indexed +import Data.ByteString +import Sqlite3.Marshall import Sqlite3.Types %default total +-------------------------------------------------------------------------------- +-- SQL Columns and Tables +-------------------------------------------------------------------------------- + ||| A column in an SQLite table: A name paired with the type of ||| values stored in the column. ||| @@ -22,8 +30,8 @@ record Column where ||| An SQLite table: A name paired with a list of columns. public export -record Table where - constructor T +record SQLTable where + constructor ST ||| The table's name name : String @@ -37,8 +45,8 @@ record Table where ||| Utility constructor for tables that sets fields `name` and `as` ||| both the value of the string argument. public export %inline -table : String -> List Column -> Table -table n = T n n +table : String -> List Column -> SQLTable +table n = ST n n ||| Utility to change the name of a table in a `SELECT` statement. ||| @@ -49,12 +57,12 @@ table n = T n n ||| students `AS` "st" ||| ``` public export %inline -AS : Table -> String -> Table -AS (T n _ cs) as = T n as cs +AS : SQLTable -> String -> SQLTable +AS (ST n _ cs) as = ST n as cs ||| Computes the types of columns stored in a table. public export %inline -ColTypes : Table -> List SqliteType +ColTypes : SQLTable -> List SqliteType ColTypes = map type . cols ||| Tries to look up a column type by name @@ -87,18 +95,22 @@ ListColType s cs = fromJust (FindCol s cs) public export %inline TableColType : (s : String) - -> (t : Table) + -> (t : SQLTable) -> {auto 0 p : IsJust (FindCol s t.cols)} -> SqliteType TableColType s t = fromJust (FindCol s t.cols) +-------------------------------------------------------------------------------- +-- Typed SQL Columns +-------------------------------------------------------------------------------- + ||| A column in the given table: This is just a column name ||| paired with a proof that the column exists in table `t` ||| and has type `tpe`. public export -data TColumn : (t : Table) -> (tpe : SqliteType) -> Type where +data TColumn : (t : SQLTable) -> (tpe : SqliteType) -> Type where TC : - {0 t : Table} + {0 t : SQLTable} -> (name : String) -> {auto 0 prf : IsJust (FindCol name t.cols)} -> TColumn t (TableColType name t) @@ -111,12 +123,16 @@ public export %inline namespace TColumn public export %inline fromString : - {0 t : Table} + {0 t : SQLTable} -> (name : String) -> {auto 0 p : IsJust (FindCol name t.cols)} -> TColumn t (TableColType name t) fromString = TC +-------------------------------------------------------------------------------- +-- Schemata +-------------------------------------------------------------------------------- + ||| A database schema is a (snoc-)list of tables. ||| ||| The reason for preferring `SnocList` over `List` is that we @@ -125,7 +141,7 @@ namespace TColumn ||| join statement than the other way round. public export 0 Schema : Type -Schema = SnocList Table +Schema = SnocList SQLTable ||| Looks up a table and column name in a schema. ||| @@ -156,9 +172,9 @@ FindSchemaCol2 t c (sx :< x) = ||| the schema. public export FindSchemaCol1 : String -> Schema -> Maybe SqliteType -FindSchemaCol1 n [< t] = FindCol n t.cols -FindSchemaCol1 n (_: String -> Bool SchemaHasCol [<] s = False SchemaHasCol (sx :< x) s = any ((s==) . name) x.cols || SchemaHasCol sx s +-------------------------------------------------------------------------------- +-- Shared Columns +-------------------------------------------------------------------------------- + ||| A column used in a `JOIN ... USING` statement: The column name must ||| appear in both schemata. public export -record JColumn (s : Schema) (t : Table) where +record JColumn (s : Schema) (t : SQLTable) where constructor JC name : String {auto 0 p1 : SchemaHasCol s name === True} @@ -204,9 +224,107 @@ namespace JColumn public export %inline fromString : {0 s : Schema} - -> {0 t : Table} + -> {0 t : SQLTable} -> (name : String) -> {auto 0 p1 : SchemaHasCol s name === True} -> {auto 0 p2 : IsJust (FindCol name t.cols)} -> JColumn s t fromString = JC + +-------------------------------------------------------------------------------- +-- Idris Tables +-------------------------------------------------------------------------------- + +||| A table of values together with a fitting header +public export +record Table a where + constructor T + {auto torow : ToRow a} + header : LAll (const String) (ToRowTypes a) + rows : List a + +hexChar : Bits8 -> Char +hexChar 0 = '0' +hexChar 1 = '1' +hexChar 2 = '2' +hexChar 3 = '3' +hexChar 4 = '4' +hexChar 5 = '5' +hexChar 6 = '6' +hexChar 7 = '7' +hexChar 8 = '8' +hexChar 9 = '9' +hexChar 10 = 'a' +hexChar 11 = 'b' +hexChar 12 = 'c' +hexChar 13 = 'd' +hexChar 14 = 'e' +hexChar _ = 'f' + +export %inline +quote : Char +quote = '\'' + +||| Encodes a `ByteString` as an SQL literal. +||| +||| Every byte is encodec with two hexadecimal digits, and the +||| whole string is wrapped in single quotes prefixed with an "X". +||| +||| For instance, `encodeBytes (fromList [0xa1, 0x77])` yields the +||| string "X'a177'". +export +encodeBytes : ByteString -> String +encodeBytes = pack . (\x => 'X'::quote::x) . foldr acc [quote] + where + %inline acc : Bits8 -> List Char -> List Char + acc b cs = hexChar (b `shiftR` 4) :: hexChar (b .&. 0xf) :: cs + +encode : (t : SqliteType) -> Maybe (IdrisType t) -> String +encode _ Nothing = "NULL" +encode BLOB (Just v) = encodeBytes v +encode TEXT (Just v) = v +encode INTEGER (Just v) = show v +encode REAL (Just v) = show v + +pad : SqliteType -> Nat -> String -> String +pad BLOB k = padRight k ' ' +pad TEXT k = padRight k ' ' +pad INTEGER k = padLeft k ' ' +pad REAL k = padLeft k ' ' + +center : Nat -> String -> String +center k s = + let ki := cast {to = Integer} (k `minus` length s) + pl := ki `div` 2 + pr := ki - pl + in replicate (cast pl) ' ' ++ s ++ replicate (cast pr) ' ' + +maxLength : Nat -> String -> Nat +maxLength n = max n . length + +barSep : LAll (const String) ts -> String +barSep = fastConcat . intersperse " | " . forget + +bar : LAll (const Nat) ts -> String +bar = fastConcat . intersperse "---" . map (`replicate` '-') . forget + +export +prettyRows : + {ts : _} + -> (header : LAll (const String) ts) + -> (rows : List (LAll (Maybe . IdrisType) ts)) + -> String +prettyRows h rs = + let cells := map (hmapW encode) rs + lengths := foldl (hzipWith maxLength) (hconst 0) (h :: cells) + rows := map (barSep . hzipWithW pad lengths) cells + header := barSep $ hzipWith center lengths h + in fastUnlines (header :: bar lengths :: rows) + +export +prettyTable : Table a -> String +prettyTable (T h rs) = prettyRows h (map toRow rs) + +export %inline +printTable : HasIO io => Table a -> io () +printTable = putStrLn . prettyTable diff --git a/test/src/Main.idr b/test/src/Main.idr index 92543b7..33581f4 100644 --- a/test/src/Main.idr +++ b/test/src/Main.idr @@ -56,32 +56,26 @@ app = withDB ":memory:" $ do , insertEmployee $ E "Valeri" 5010.0 1 , insertEmployee $ E "Ronja" 4010.0 1 ] ++ fromList (insertFile . file <$> [0..255]) - ms <- query (mol TRUE) 1000 - putStrLn $ printRows ms + + queryTable (mol TRUE) 1000 >>= printTable putStrLn "" - fs <- query (file TRUE `LIMIT` 20) 1000 - traverse_ (putStrLn . encodeBytes . content . value) fs + queryTable (file TRUE `LIMIT` 20) 1000 >>= printTable putStrLn "" - es <- query employee 1000 - putStrLn $ printRows es + queryTable employee 1000 >>= printTable putStrLn "" - hs <- query heads 1000 - putStrLn $ printRows hs + queryTable heads 1000 >>= printTable putStrLn "" - ts <- query tuples 1000 - putStrLn $ printRows ts + queryTable tuples 1000 >>= printTable putStrLn "" - ps <- query nonHeads 1000 - putStrLn $ printRows ps + queryTable nonHeads 1000 >>= printTable putStrLn "" - ss <- query unitStats 1000 - putStrLn $ printRows ss + queryTable unitStats 1000 >>= printTable putStrLn "" main : IO () diff --git a/test/src/Schema.idr b/test/src/Schema.idr index e954790..d0572bb 100644 --- a/test/src/Schema.idr +++ b/test/src/Schema.idr @@ -11,7 +11,7 @@ import Enum %language ElabReflection public export -Units : Table +Units : SQLTable Units = table "units" [ C "unit_id" INTEGER @@ -20,7 +20,7 @@ Units = ] public export -Employees : Table +Employees : SQLTable Employees = table "employees" [ C "employee_id" INTEGER @@ -30,7 +30,7 @@ Employees = ] public export -Molecules : Table +Molecules : SQLTable Molecules = table "molecules" [ C "molecule_id" INTEGER @@ -41,7 +41,7 @@ Molecules = ] public export -Files : Table +Files : SQLTable Files = table "files" [ C "file_id" INTEGER @@ -161,7 +161,7 @@ insertFile = insert Files ["content"] -- Query -------------------------------------------------------------------------------- -export +public export mol : Expr [ Query (WithID Molecule) mol x = SELECT @@ -169,11 +169,11 @@ mol x = [ Query (WithID File) file x = SELECT ["file_id", "content"] [ 3000.0) `ORDER_BY` [ASC "e.salary", ASC "e.name"] -export +public export unitStats : LQuery [String,Bits32,Salary,Salary,Salary] unitStats = SELECT @@ -201,7 +201,7 @@ unitStats = `HAVING` ("num_employees" > 3) `ORDER_BY` [ASC "average_salary"] -export +public export heads : Query (OrgUnit String) heads = SELECT @@ -210,7 +210,7 @@ heads = , JOIN (Units `AS` "u") `ON` ("e.employee_id" == "u.head") ] -export +public export nonHeads : LQuery [Bits32, String] nonHeads = SELECT @@ -221,7 +221,7 @@ nonHeads = `WHERE` IS NULL "u.head" `ORDER_BY` [ASC "e.name"] -export +public export tuples : LQuery [String,Double,Double,MolType] tuples = SELECT