[ new ] fromString for expressions

sqlite3.ipkg

@@ -17,7 +17,6 @@ modules = Sqlite3
         , Sqlite3.Marshall
         , Sqlite3.Parameter
         , Sqlite3.Prim
-        , Sqlite3.Run
         , Sqlite3.Table
         , Sqlite3.Types
 

src/Sqlite3.idr

@@ -5,6 +5,5 @@ import public Sqlite3.Expr
 import public Sqlite3.Marshall
 import public Sqlite3.Parameter
 import public Sqlite3.Prim
-import public Sqlite3.Run
 import public Sqlite3.Table
 import public Sqlite3.Types

src/Sqlite3/Expr.idr

@@ -83,9 +83,12 @@ export %inline
 FromDouble (Expr s REAL) where
   fromDouble = Lit REAL
 
--- export %inline
--- FromString (Expr s TEXT) where
---   fromString = Lit TEXT . Just
+export %inline
+fromString :
+     (col      : String)
+  -> {auto 0 p : TableHasCol t col}
+  -> Expr [t] (ListColType t.cols p)
+fromString = C
 
 ||| Convert a value of a marshallable type to a literal expression.
 export
@@ -95,6 +98,22 @@ val x =
     Nothing => NULL
     Just v  => Lit _ v
 
+export %inline
+text : String -> Expr s TEXT
+text = val
+
+export %inline
+int : Int64 -> Expr s INTEGER
+int = val
+
+export %inline
+blob : ByteString -> Expr s BLOB
+blob = val
+
+export %inline
+real : Double -> Expr s REAL
+real = val
+
 --------------------------------------------------------------------------------
 -- Encode
 --------------------------------------------------------------------------------
@@ -120,12 +139,25 @@ hexChar _  = 'f'
 %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
 
+||| Encodes a `String` as an SQL literal.
+|||
+||| The whole string is wrapped in single quotes. Single quotes withing
+||| the string are escaped by doubling them.
+export
 encodeText : String -> String
 encodeText = go [<quote] . unpack
   where

test/src/Main.idr

@@ -43,8 +43,10 @@ insertFile : ByteString -> Cmd TInsert
 insertFile ix = insert Files ["content"] [ix]
 
 mol : Query [Bits32, String, Maybe String, Maybe Double]
-mol =
-  SELECT_FROM Molecules [C "id", C "name", C "casnr", C "molweight"] (C "id" > 1)
+mol = SELECT_FROM Molecules ["id", "name", "casnr", "molweight"] ("id" > 1)
+
+fil : Query [ByteString]
+fil = SELECT_FROM Files ["content"] ("id" == 1)
 
 app : App Errs ()
 app = withDB ":memory:" $ do
@@ -63,6 +65,8 @@ app = withDB ":memory:" $ do
     ]
   ms <- query mol 1000
   traverse_ printLn ms
+  fs <- query fil 1
+  traverse_ (\[bs] => putStrLn $ encodeBytes bs) fs
 
 main : IO ()
 main = runApp handlers app