Merge pull request #27 from stefan-hoeck/no_bool

[ refactor ] drop BOOL data constructor

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,

src/Sqlite3/Expr.idr

@@ -357,18 +357,13 @@ encodeText = go [<quote] . unpack
     go sc ('\'' :: xs) = go (sc :< quote :< quote) xs
     go sc (x    :: xs) = go (sc :< x) xs
 
-encBool : Bool -> String
-encBool True  = "1"
-encBool False = "0"
-
 ||| Encodes an SQL literal as a string.
 export
 encodeLit : (t : SqliteType) -> IdrisType t -> String
 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
 

src/Sqlite3/Prim.idr

@@ -325,18 +325,13 @@ 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
   case t of
     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)

src/Sqlite3/Types.idr

@@ -103,18 +103,26 @@ 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
 IdrisType BLOB    = ByteString
 IdrisType TEXT    = String
 IdrisType INTEGER = Int64
 IdrisType REAL    = Double
-IdrisType BOOL    = Bool
 
 --------------------------------------------------------------------------------
 --          Error Type