diff --git a/docs/src/Tutorial.md b/docs/src/Tutorial.md index ae2bdd8..6227632 100644 --- a/docs/src/Tutorial.md +++ b/docs/src/Tutorial.md @@ -29,13 +29,13 @@ is reflected in the `Sqlite3.Types.SqliteType` enumeration: `INTEGER` for signed 64 bit integers, `REAL` for 64 bit floating point numbers, `TEXT`for strings of unicode characters, and `BLOB` for byte arrays. -Data type `SqliteType` comes with a fifth value called `BOOL` for boolean -values. In database tables, this is represented as an integer with `0` +In addition, `BOOL` is defined as an alias for `INTEGER`. +In database tables, this is represented as an integer with `0` corresponding to `False` and every other value (typically `1`) corresponding -to `True`. Although this is not an official SQLite type, it helps with -defining and typing predicate expressions as we will later see. +to `True`. It has no effect on type safety or -inference, but it helps +making the intention behind certain expressions clearer. -Each of the five values of `SqliteType` corresponds to an Idris type, +Each of the four values of `SqliteType` corresponds to an Idris type, to which values are converted when reading from and writing to the database. This is reflected in function `Sqlite3.Types.IdrisType` and summarized in the following table: @@ -46,7 +46,6 @@ in the following table: | REAL | Double | 64 bit floating point number | | TEXT | String | sequence of unicode characters | | BLOB | ByteString | byte array | -| BOOL | Bool | 64 bit signed integer | All SQLite types are nullable, that is, `NULL` is a valid value in a column, unless the `NOT NULL` constraint has been set (see below). Therefore, diff --git a/src/Sqlite3/Expr.idr b/src/Sqlite3/Expr.idr index 7345716..3f31bfc 100644 --- a/src/Sqlite3/Expr.idr +++ b/src/Sqlite3/Expr.idr @@ -357,10 +357,6 @@ encodeText = go [ String -encBool True = "1" -encBool False = "0" - ||| Encodes an SQL literal as a string. export encodeLit : (t : SqliteType) -> IdrisType t -> String @@ -368,7 +364,6 @@ encodeLit BLOB x = encodeBytes x encodeLit TEXT x = encodeText x encodeLit INTEGER x = show x encodeLit REAL x = show x -encodeLit BOOL x = encBool x encOp : String -> Expr s t -> Expr s t -> String diff --git a/src/Sqlite3/Prim.idr b/src/Sqlite3/Prim.idr index 9ff996f..4cf83e8 100644 --- a/src/Sqlite3/Prim.idr +++ b/src/Sqlite3/Prim.idr @@ -325,10 +325,6 @@ sqlitePrepare s = withPtrAlloc $ \stmt_ptr => do | r => sqlFail r Right . S <$> dereference stmt_ptr -%inline boolToInt : Bool -> Int64 -boolToInt True = 1 -boolToInt False = 0 - bindParam : DB => Stmt -> Parameter -> IO Int bindParam s (P n t v) = do ix <- fromPrim $ prim__sqlite3_bind_parameter_index s.stmt n @@ -336,7 +332,6 @@ bindParam s (P n t v) = do INTEGER => fromPrim $ prim__sqlite3_bind_int64 s.stmt ix v REAL => fromPrim $ prim__sqlite3_bind_double s.stmt ix v TEXT => fromPrim $ prim__sqlite3_bind_text s.stmt ix v - BOOL => fromPrim $ prim__sqlite3_bind_int64 s.stmt ix (boolToInt v) BLOB => do buf <- toBuffer v fromPrim $ prim__sqlite3_bind_blob s.stmt ix buf (cast v.size) diff --git a/src/Sqlite3/Types.idr b/src/Sqlite3/Types.idr index 9e6e7ca..1cab671 100644 --- a/src/Sqlite3/Types.idr +++ b/src/Sqlite3/Types.idr @@ -103,10 +103,19 @@ data SqliteType : Type where TEXT : SqliteType INTEGER : SqliteType REAL : SqliteType - BOOL : SqliteType %runElab derive "SqliteType" [Show,Eq,Ord] +||| This is an alias for `INTEGER` that helps with making the intention +||| behind certain SQL expressions clearer. +||| +||| SQLite does not have a native boolean type, so this is used +||| as a reminder than some expression are used in accordance with +||| boolean logic. +public export %inline +BOOL : SqliteType +BOOL = INTEGER + ||| Associates an `SqliteType` with the corresponding Idris type. public export 0 IdrisType : SqliteType -> Type @@ -114,7 +123,6 @@ IdrisType BLOB = ByteString IdrisType TEXT = String IdrisType INTEGER = Int64 IdrisType REAL = Double -IdrisType BOOL = Bool -------------------------------------------------------------------------------- -- Error Type