mirror of
https://github.com/ilyakooo0/IdrisSqlite.git
synced 2024-07-07 06:56:22 +03:00
Completed changes from previous commit (missed some files) and updated README.md
This commit is contained in:
Colin Adams
parent
81df5a6421
commit
aa7151b811
5
.gitignore
vendored
5
.gitignore
vendored
|
|
@ -1,3 +1,6 @@
|
|||
*~
|
||||
*.ibc
|
||||
*.o
|
||||
*.o
|
||||
sqlite_test
|
||||
src/sqlite3api.so
|
||||
src/sqlite3api.o
|
||||
16
README.md
16
README.md
|
|
@ -2,3 +2,19 @@ SQLite bindings for Idris
|
|||
========
|
||||
|
||||
These SQLite bindings are forked from IdrisWeb.
|
||||
|
||||
To install:
|
||||
|
||||
idris --install sqlite.ipkg
|
||||
|
||||
to test installation:
|
||||
|
||||
idris --build sqlite_test.ipkg (a C compiler warning of an implicit function declaration is issued (TODO - fix that)
|
||||
./sqlite_test
|
||||
|
||||
expected output is:
|
||||
|
||||
Done
|
||||
[[DBText "test", DBText "CREATE TABLE test (name INT, age INT)"]]
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
package sqlite
|
||||
|
||||
opts = "-p effects"
|
||||
pkgs = effects
|
||||
sourcedir = src
|
||||
modules = DB.SQLite.Effect, DB.SQLite.SQLiteCodes
|
||||
|
||||
|
|
|
|||
|
|
@ -10,17 +10,17 @@ import DB.SQLite.SQLiteCodes
|
|||
|
||||
%dynamic "libsqlite3"
|
||||
%dynamic "sqlite3api.so"
|
||||
%access public
|
||||
%access public export
|
||||
|
||||
data ConnectionPtr = ConnPtr Ptr
|
||||
data StmtPtr = PSPtr Ptr
|
||||
|
||||
data DBVal = DBInt Int
|
||||
| DBText String
|
||||
| DBFloat Float
|
||||
| DBFloat Double
|
||||
| DBNull
|
||||
|
||||
instance Show DBVal where
|
||||
implementation Show DBVal where
|
||||
show (DBInt i) = "DBInt " ++ show i
|
||||
show (DBText t) = "DBText " ++ show t
|
||||
show (DBFloat f) = "DBFloat " ++ show f
|
||||
|
|
@ -78,7 +78,7 @@ data QueryError = ConnectionError SQLiteCode
|
|||
| ExecError String
|
||||
| InternalError
|
||||
|
||||
instance Show QueryError where
|
||||
implementation Show QueryError where
|
||||
show (ConnectionError code) = "Error connecting to database, code: " ++ (show code)
|
||||
show (BindingError (BE ap code)) = "Error binding variable, pos: " ++ (show ap) ++ ", code: " ++ (show code)
|
||||
show (StatementError code) = "Error creating prepared statement, code: " ++ (show code)
|
||||
|
|
@ -87,61 +87,56 @@ instance Show QueryError where
|
|||
|
||||
data Sqlite : Effect where
|
||||
-- Opens a connection to the database
|
||||
OpenDB : DBName ->
|
||||
{ () ==> either (const ()) (const SQLiteConnected) result } Sqlite (Either QueryError ())
|
||||
OpenDB : DBName -> sig Sqlite (Either QueryError ()) () (\result => (either (const ()) (const SQLiteConnected) result))
|
||||
-- Closes the database handle
|
||||
CloseDB : { SQLiteConnected ==> () } Sqlite ()
|
||||
CloseDB : sig Sqlite () SQLiteConnected ()
|
||||
-- Prepares a statement, given a basic query string
|
||||
PrepareStatement : QueryString ->
|
||||
{ SQLiteConnected ==>
|
||||
either (const SQLitePSFail)
|
||||
(const $ SQLitePSSuccess Binding) result } Sqlite (Either QueryError ())
|
||||
PrepareStatement : QueryString -> sig Sqlite (Either QueryError ())
|
||||
(SQLiteConnected)
|
||||
(\result => either (const SQLitePSFail)
|
||||
(const $ SQLitePSSuccess Binding) result)
|
||||
-- Binds arguments to the given argument position
|
||||
BindInt : ArgPos -> Int -> { SQLitePSSuccess Binding } Sqlite ()
|
||||
BindFloat : ArgPos -> Float ->
|
||||
{ SQLitePSSuccess Binding } Sqlite ()
|
||||
BindText : ArgPos -> String -> Int ->
|
||||
{ SQLitePSSuccess Binding } Sqlite ()
|
||||
BindNull : ArgPos -> { SQLitePSSuccess Binding } Sqlite ()
|
||||
BindInt : ArgPos -> Int -> sig Sqlite () (SQLitePSSuccess Binding)
|
||||
BindFloat : ArgPos -> Double -> sig Sqlite () (SQLitePSSuccess Binding)
|
||||
BindText : ArgPos -> String -> Int -> sig Sqlite () (SQLitePSSuccess Binding)
|
||||
BindNull : ArgPos -> sig Sqlite () (SQLitePSSuccess Binding)
|
||||
|
||||
-- Checks to see whether all the binds were successful, if not then fails with the bind error
|
||||
FinishBind : {SQLitePSSuccess Binding ==>
|
||||
maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result } Sqlite (Maybe QueryError)
|
||||
FinishBind : sig Sqlite (Maybe QueryError) (SQLitePSSuccess Binding) (\result => maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result)
|
||||
|
||||
-- Executes the statement, and fetches the first row
|
||||
ExecuteStatement : { SQLitePSSuccess Bound ==>
|
||||
if hasMoreRows result
|
||||
ExecuteStatement : sig Sqlite (StepResult) (SQLitePSSuccess Bound)
|
||||
(\result => if hasMoreRows result
|
||||
then SQLiteExecuting ValidRow
|
||||
else SQLiteExecuting InvalidRow } Sqlite StepResult
|
||||
else SQLiteExecuting InvalidRow)
|
||||
|
||||
RowStep : { SQLiteExecuting ValidRow ==>
|
||||
if hasMoreRows result
|
||||
RowStep : sig Sqlite (StepResult) (SQLiteExecuting ValidRow)
|
||||
(\result => if hasMoreRows result
|
||||
then SQLiteExecuting ValidRow
|
||||
else SQLiteExecuting InvalidRow } Sqlite StepResult
|
||||
else SQLiteExecuting InvalidRow)
|
||||
|
||||
-- We need two separate effects, but this is entirely non-user-facing due to
|
||||
-- if_valid in the wrapper function
|
||||
Reset : { SQLiteExecuting state ==>
|
||||
if hasMoreRows result
|
||||
Reset : sig Sqlite (StepResult) (SQLiteExecuting state)
|
||||
(\result => if hasMoreRows result
|
||||
then SQLiteExecuting ValidRow
|
||||
else SQLiteExecuting InvalidRow} Sqlite StepResult
|
||||
else SQLiteExecuting InvalidRow)
|
||||
|
||||
-- Column access functions
|
||||
GetColumnName : Column -> { SQLiteExecuting ValidRow } Sqlite String
|
||||
GetColumnDataSize : Column -> { SQLiteExecuting ValidRow } Sqlite Int
|
||||
GetColumnText : Column -> { SQLiteExecuting ValidRow } Sqlite String
|
||||
GetColumnInt : Column -> { SQLiteExecuting ValidRow } Sqlite Int
|
||||
GetColumnFloat : Column -> { SQLiteExecuting ValidRow } Sqlite Float
|
||||
IsColumnNull : Column -> { SQLiteExecuting ValidRow } Sqlite Bool
|
||||
GetColumnName : Column -> sig Sqlite String (SQLiteExecuting ValidRow)
|
||||
GetColumnDataSize : Column -> sig Sqlite Int (SQLiteExecuting ValidRow)
|
||||
GetColumnText : Column -> sig Sqlite String (SQLiteExecuting ValidRow)
|
||||
GetColumnInt : Column -> sig Sqlite Int (SQLiteExecuting ValidRow)
|
||||
GetColumnFloat : Column -> sig Sqlite Double (SQLiteExecuting ValidRow)
|
||||
IsColumnNull : Column -> sig Sqlite Bool (SQLiteExecuting ValidRow)
|
||||
|
||||
-- Finalisation Functions
|
||||
Finalise : { SQLiteExecuting s ==> SQLiteConnected } Sqlite ()
|
||||
Finalise : sig Sqlite () (SQLiteExecuting s) SQLiteConnected
|
||||
|
||||
|
||||
-- Cleanup functions to handle error states
|
||||
CleanupPSFail : { SQLitePSFail ==> () } Sqlite ()
|
||||
CleanupBindFail : { SQLiteFinishBindFail ==> () } Sqlite ()
|
||||
|
||||
CleanupPSFail : sig Sqlite () SQLitePSFail ()
|
||||
CleanupBindFail : sig Sqlite () SQLiteFinishBindFail ()
|
||||
|
||||
|
||||
private
|
||||
|
|
@ -165,7 +160,7 @@ foreignClose (ConnPtr c) = do foreign FFI_C "sqlite3_close_idr" (Ptr -> IO Int)
|
|||
|
||||
-- That's the painful bit done, since exception branching will allow us to not have to do
|
||||
-- the ugliness of pass-through handlers
|
||||
instance Handler Sqlite IO where
|
||||
implementation Handler Sqlite IO where
|
||||
handle () (OpenDB file) k = do
|
||||
ff <- foreign FFI_C "sqlite3_open_idr" (String -> IO Ptr) file
|
||||
is_null <- nullPtr ff
|
||||
|
|
@ -192,7 +187,7 @@ instance Handler Sqlite IO where
|
|||
k () (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err))
|
||||
|
||||
handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindFloat pos f) k = do
|
||||
res <- foreign FFI_C "sqlite3_bind_double_idr" (Ptr -> Int -> Float -> IO Ptr) conn pos f
|
||||
res <- foreign FFI_C "sqlite3_bind_double_idr" (Ptr -> Int -> Double -> IO Ptr) conn pos f
|
||||
is_null <- nullPtr res
|
||||
if (not is_null) then k () (SQLitePS (ConnPtr conn) (PSPtr res))
|
||||
else do err <- foreignGetError (ConnPtr conn)
|
||||
|
|
@ -259,7 +254,7 @@ instance Handler Sqlite IO where
|
|||
k res (SQLiteE (ConnPtr c) (PSPtr p))
|
||||
|
||||
handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnFloat i) k = do
|
||||
res <- foreign FFI_C "sqlite3_column_double_idr" (Ptr -> Int -> IO Float) c i
|
||||
res <- foreign FFI_C "sqlite3_column_double_idr" (Ptr -> Int -> IO Double) c i
|
||||
k res (SQLiteE (ConnPtr c) (PSPtr p))
|
||||
|
||||
handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnText i) k = do
|
||||
|
|
@ -309,27 +304,26 @@ instance Handler Sqlite IO where
|
|||
SQLITE : Type -> EFFECT
|
||||
SQLITE t = MkEff t Sqlite
|
||||
{- User-facing functions -}
|
||||
openDB : DBName -> { [SQLITE ()] ==>
|
||||
[SQLITE (either (const ()) (const SQLiteConnected) result)] } Eff (Either QueryError ())
|
||||
openDB : DBName -> Eff (Either QueryError ()) [SQLITE ()]
|
||||
(\result => [SQLITE (either (const ()) (const SQLiteConnected) result)])
|
||||
openDB name = call $ OpenDB name
|
||||
|
||||
closeDB : { [SQLITE (SQLiteConnected)] ==> [SQLITE ()] } Eff ()
|
||||
closeDB : Eff () [SQLITE (SQLiteConnected)] [SQLITE ()]
|
||||
closeDB = call CloseDB
|
||||
|
||||
prepareStatement : QueryString ->
|
||||
{ [SQLITE SQLiteConnected] ==>
|
||||
[SQLITE ( either (const SQLitePSFail)
|
||||
(const $ SQLitePSSuccess Binding) result)] } Eff (Either QueryError ())
|
||||
prepareStatement : QueryString -> Eff (Either QueryError ())
|
||||
[SQLITE SQLiteConnected]
|
||||
(\result => [SQLITE ( either (const SQLitePSFail)
|
||||
(const $ SQLitePSSuccess Binding) result)])
|
||||
prepareStatement stmt = call $ PrepareStatement stmt
|
||||
|
||||
bindInt : ArgPos -> Int ->
|
||||
{ [SQLITE (SQLitePSSuccess Binding)] } Eff ()
|
||||
bindInt : ArgPos -> Int -> Eff () [SQLITE (SQLitePSSuccess Binding)]
|
||||
bindInt pos i = call $ BindInt pos i
|
||||
|
||||
bindFloat : ArgPos -> Float -> { [SQLITE (SQLitePSSuccess Binding)] } Eff ()
|
||||
bindFloat : ArgPos -> Double -> Eff () [SQLITE (SQLitePSSuccess Binding)]
|
||||
bindFloat pos f = call $ BindFloat pos f
|
||||
|
||||
bindText : ArgPos -> String -> { [SQLITE (SQLitePSSuccess Binding)] } Eff ()
|
||||
bindText : ArgPos -> String -> Eff () [SQLITE (SQLitePSSuccess Binding)]
|
||||
bindText pos str = call $ BindText pos str str_len
|
||||
where natToInt : Nat -> Int
|
||||
natToInt Z = 0
|
||||
|
|
@ -338,59 +332,58 @@ bindText pos str = call $ BindText pos str str_len
|
|||
str_len : Int
|
||||
str_len = natToInt (length str)
|
||||
|
||||
bindNull : ArgPos -> { [SQLITE (SQLitePSSuccess Binding)] } Eff ()
|
||||
bindNull : ArgPos -> Eff () [SQLITE (SQLitePSSuccess Binding)]
|
||||
bindNull pos = call $ BindNull pos
|
||||
|
||||
finishBind : { [SQLITE (SQLitePSSuccess Binding)] ==>
|
||||
[SQLITE (maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result)] } Eff (Maybe QueryError)
|
||||
finishBind : Eff (Maybe QueryError) [SQLITE (SQLitePSSuccess Binding)]
|
||||
(\result => [SQLITE (maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result)])
|
||||
finishBind = call FinishBind
|
||||
|
||||
nextRow : { [SQLITE (SQLiteExecuting ValidRow)] ==>
|
||||
[SQLITE (if hasMoreRows result
|
||||
nextRow : Eff StepResult [SQLITE (SQLiteExecuting ValidRow)]
|
||||
(\result => [SQLITE (if hasMoreRows result
|
||||
then SQLiteExecuting ValidRow
|
||||
else SQLiteExecuting InvalidRow)] } Eff StepResult
|
||||
else SQLiteExecuting InvalidRow)])
|
||||
nextRow = call RowStep
|
||||
|
||||
reset : { [SQLITE (SQLiteExecuting state)] ==>
|
||||
[SQLITE (if hasMoreRows result
|
||||
reset : Eff StepResult [SQLITE (SQLiteExecuting state)]
|
||||
(\result => [SQLITE (if hasMoreRows result
|
||||
then SQLiteExecuting ValidRow
|
||||
else SQLiteExecuting InvalidRow)] } Eff StepResult
|
||||
else SQLiteExecuting InvalidRow)])
|
||||
reset = call Reset
|
||||
|
||||
|
||||
getColumnName : Column -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff String
|
||||
getColumnName : Column -> Eff String [SQLITE (SQLiteExecuting ValidRow)]
|
||||
getColumnName col = call $ GetColumnName col
|
||||
|
||||
getColumnText : Column -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff String
|
||||
getColumnText : Column -> Eff String [SQLITE (SQLiteExecuting ValidRow)]
|
||||
getColumnText col = call $ GetColumnText col
|
||||
|
||||
getColumnInt : Column -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff Int
|
||||
getColumnInt : Column -> Eff Int [SQLITE (SQLiteExecuting ValidRow)]
|
||||
getColumnInt col = call $ GetColumnInt col
|
||||
|
||||
getColumnFloat : Column -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff Float
|
||||
getColumnFloat : Column -> Eff Double [SQLITE (SQLiteExecuting ValidRow)]
|
||||
getColumnFloat col = call $ GetColumnFloat col
|
||||
|
||||
isColumnNull : Column -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff Bool
|
||||
isColumnNull : Column -> Eff Bool [SQLITE (SQLiteExecuting ValidRow)]
|
||||
isColumnNull col = call $ IsColumnNull col
|
||||
|
||||
getColumnDataSize : Column -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff Int
|
||||
getColumnDataSize : Column -> Eff Int [SQLITE (SQLiteExecuting ValidRow)]
|
||||
getColumnDataSize col = call $ GetColumnDataSize col
|
||||
|
||||
finalise : { [SQLITE (SQLiteExecuting s)] ==>
|
||||
[SQLITE SQLiteConnected] } Eff ()
|
||||
finalise : Eff () [SQLITE (SQLiteExecuting s)] [SQLITE SQLiteConnected]
|
||||
finalise = call Finalise
|
||||
|
||||
cleanupPSFail : { [SQLITE (SQLitePSFail)] ==> [SQLITE ()] } Eff ()
|
||||
cleanupPSFail : Eff () [SQLITE (SQLitePSFail)] [SQLITE ()]
|
||||
cleanupPSFail = call CleanupPSFail
|
||||
|
||||
cleanupBindFail : { [SQLITE (SQLiteFinishBindFail)] ==> [SQLITE ()] } Eff ()
|
||||
cleanupBindFail : Eff () [SQLITE (SQLiteFinishBindFail)] [SQLITE ()]
|
||||
cleanupBindFail = call CleanupBindFail
|
||||
|
||||
-- Just makes it a tad nicer to write
|
||||
executeStatement : { [SQLITE (SQLitePSSuccess Bound)] ==>
|
||||
[SQLITE (if hasMoreRows result
|
||||
executeStatement : Eff StepResult [SQLITE (SQLitePSSuccess Bound)]
|
||||
(\result => [SQLITE (if hasMoreRows result
|
||||
then SQLiteExecuting ValidRow
|
||||
else SQLiteExecuting InvalidRow)] } Eff StepResult
|
||||
else SQLiteExecuting InvalidRow)])
|
||||
executeStatement = call ExecuteStatement
|
||||
|
||||
|
||||
|
|
@ -399,7 +392,7 @@ getQueryError (Left qe) = qe
|
|||
getQueryError _ = InternalError
|
||||
|
||||
total
|
||||
multiBind' : List (Int, DBVal) -> { [SQLITE (SQLitePSSuccess Binding)] } Eff ()
|
||||
multiBind' : List (Int, DBVal) -> Eff () [SQLITE (SQLitePSSuccess Binding)]
|
||||
multiBind' [] = Effects.pure ()
|
||||
multiBind' ((pos, (DBInt i)) :: xs) = do bindInt pos i
|
||||
multiBind' xs
|
||||
|
|
@ -411,19 +404,18 @@ multiBind' ((pos, DBNull) :: xs) = do bindNull pos
|
|||
multiBind' xs
|
||||
-- Binds multiple values within a query
|
||||
|
||||
multiBind : List (Int, DBVal) ->
|
||||
{ [SQLITE (SQLitePSSuccess Binding)] ==>
|
||||
[SQLITE (maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result)] }
|
||||
Eff (Maybe QueryError)
|
||||
multiBind : List (Int, DBVal) -> Eff (Maybe QueryError)
|
||||
[SQLITE (SQLitePSSuccess Binding)]
|
||||
(\result => [SQLITE (maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result)])
|
||||
|
||||
multiBind vals = do
|
||||
multiBind' vals
|
||||
finishBind
|
||||
|
||||
|
||||
|
||||
getRowCount' : StepResult ->
|
||||
{ [SQLITE (SQLiteExecuting s)] ==> [SQLITE ()] }
|
||||
Eff (Either QueryError Int)
|
||||
getRowCount' : StepResult -> Eff (Either QueryError Int) [SQLITE (SQLiteExecuting s)] [SQLITE ()]
|
||||
|
||||
getRowCount' NoMoreRows = do finalise
|
||||
closeDB
|
||||
return $ Left (ExecError "Unable to get row count")
|
||||
|
|
@ -446,7 +438,7 @@ getBindError (Just (BindingError be)) = (BindingError be)
|
|||
getBindError _ = InternalError
|
||||
|
||||
|
||||
getRowCount : { [SQLITE SQLiteConnected] ==> [SQLITE ()] } Eff (Either QueryError Int)
|
||||
getRowCount : Eff (Either QueryError Int) [SQLITE SQLiteConnected] [SQLITE ()]
|
||||
getRowCount = do
|
||||
let insert_id_sql = "SELECT last_insert_rowid()"
|
||||
sql_prep_res <- prepareStatement insert_id_sql
|
||||
|
|
@ -470,7 +462,7 @@ getRowCount = do
|
|||
executeInsert : String ->
|
||||
String ->
|
||||
List (Int, DBVal) ->
|
||||
{ [SQLITE ()] } Eff (Either QueryError Int)
|
||||
Eff (Either QueryError Int) [SQLITE ()]
|
||||
executeInsert db_name query bind_vals =
|
||||
do db_res <- openDB db_name
|
||||
case db_res of
|
||||
|
|
@ -487,9 +479,8 @@ executeInsert db_name query bind_vals =
|
|||
return (Left err)
|
||||
Nothing => executeIt
|
||||
-- split out to make typechecking faster
|
||||
where executeIt : { [SQLITE (SQLitePSSuccess Bound)] ==>
|
||||
[SQLITE ()] }
|
||||
Eff (Either QueryError Int)
|
||||
where executeIt : Eff (Either QueryError Int) [SQLITE (SQLitePSSuccess Bound)] [SQLITE ()]
|
||||
|
||||
executeIt =
|
||||
do er_1 <- executeStatement
|
||||
case er_1 of
|
||||
|
|
@ -507,9 +498,8 @@ executeInsert db_name query bind_vals =
|
|||
|
||||
-- Helper functions for selection from a DB
|
||||
partial
|
||||
collectResults : ({ [SQLITE (SQLiteExecuting ValidRow)] } Eff (List DBVal)) ->
|
||||
{ [SQLITE (SQLiteExecuting ValidRow)] ==>
|
||||
[SQLITE (SQLiteExecuting InvalidRow)] } Eff ResultSet
|
||||
collectResults : (Eff (List DBVal) [SQLITE (SQLiteExecuting ValidRow)]) ->
|
||||
Eff ResultSet [SQLITE (SQLiteExecuting ValidRow)] [SQLITE (SQLiteExecuting InvalidRow)]
|
||||
collectResults fn =
|
||||
do results <- fn
|
||||
case !nextRow of
|
||||
|
|
@ -524,8 +514,8 @@ collectResults fn =
|
|||
-- a function to process the returned data,
|
||||
partial
|
||||
executeSelect : (db_name : String) -> (q : String) -> List (Int, DBVal) ->
|
||||
({ [SQLITE (SQLiteExecuting ValidRow)] } Eff (List DBVal)) ->
|
||||
{ [SQLITE ()] } Eff (Either QueryError ResultSet)
|
||||
(Eff (List DBVal) [SQLITE (SQLiteExecuting ValidRow)]) ->
|
||||
Eff (Either QueryError ResultSet) [SQLITE ()]
|
||||
executeSelect db_name q bind_vals fn =
|
||||
do Right () <- openDB db_name | Left err => return (Left err)
|
||||
Right () <- prepareStatement q | Left err => do cleanupPSFail
|
||||
|
|
@ -549,10 +539,3 @@ executeSelect db_name q bind_vals fn =
|
|||
closeDB
|
||||
return $ Right []
|
||||
|
||||
-- -}
|
||||
-- -}
|
||||
-- -}
|
||||
|
||||
-- Local Variables:
|
||||
-- idris-packages: ("effects" "sqlite")
|
||||
-- End:
|
||||
|
|
|
|||
|
|
@ -5,7 +5,7 @@ import DB.SQLite.Effect
|
|||
import DB.SQLite.SQLiteCodes
|
||||
|
||||
|
||||
testInsert : String -> Int -> { [SQLITE ()] } Eff IO (Either QueryError ())
|
||||
testInsert : String -> Int -> Eff (Either QueryError ()) [SQLITE ()]
|
||||
testInsert name age =
|
||||
do open_db <- openDB "test.db"
|
||||
case open_db of
|
||||
|
|
@ -39,7 +39,7 @@ testInsert name age =
|
|||
|
||||
|
||||
|
||||
testSelect : { [SQLITE ()] } Eff IO (Either QueryError ResultSet)
|
||||
testSelect : Eff (Either QueryError ResultSet) [SQLITE ()]
|
||||
testSelect =
|
||||
executeSelect "test.db" "SELECT `name`, `sql` FROM `sqlite_master`;" [] $
|
||||
do name <- getColumnText 0
|
||||
|
|
|
|||
|
|
@ -4,13 +4,13 @@ import Schema
|
|||
|
||||
import Decidable.Equality
|
||||
|
||||
data DB : String -> Type where
|
||||
public export data DB : String -> Type where
|
||||
MkDB : (dbFile : String) ->
|
||||
(dbTables : List (String, Schema)) -> DB dbFile
|
||||
|
||||
%name DB db
|
||||
|
||||
data HasTable : List (String, Schema) -> String -> Schema -> Type where
|
||||
public export data HasTable : List (String, Schema) -> String -> Schema -> Type where
|
||||
Here : HasTable ((name, s)::ts) name s
|
||||
There : HasTable ts name s ->
|
||||
HasTable ((name',s')::ts) name s
|
||||
|
|
|
|||
|
|
@ -1,7 +1,5 @@
|
|||
module Provider
|
||||
|
||||
import public Providers
|
||||
|
||||
import DB.SQLite.Effect
|
||||
import DB.SQLite.SQLiteCodes
|
||||
import Effects
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ import Language.Reflection.Utils
|
|||
%default total
|
||||
%language ErrorReflection
|
||||
|
||||
namespace Row
|
||||
namespace Row0
|
||||
data Row : Schema -> Type where
|
||||
Nil : Row []
|
||||
(::) : (x : interpSql t) -> (xs : Row s) -> Row ((c:::t) :: s)
|
||||
|
|
@ -90,16 +90,16 @@ namespace Expr
|
|||
namespace Query
|
||||
%reflection
|
||||
reflectListPrf : List a -> Tactic
|
||||
reflectListPrf [] = Refine "Here" `Seq` Solve
|
||||
reflectListPrf [] = Refine (UN "Here") `Seq` Solve
|
||||
reflectListPrf (x :: xs)
|
||||
= Try (Refine "Here" `Seq` Solve)
|
||||
(Refine "There" `Seq` (Solve `Seq` reflectListPrf xs))
|
||||
= Try (Refine (UN "Here") `Seq` Solve)
|
||||
(Refine (UN "There") `Seq` (Solve `Seq` reflectListPrf xs))
|
||||
-- TMP HACK! FIXME!
|
||||
-- The evaluator needs a 'function case' to know its a reflection function
|
||||
-- until we propagate that information! Without this, the _ case won't get
|
||||
-- matched.
|
||||
--reflectListPrf (x ++ y) = Refine "Here" `Seq` Solve
|
||||
reflectListPrf _ = Refine "Here" `Seq` Solve
|
||||
reflectListPrf _ = Refine (UN "Here") `Seq` Solve
|
||||
|
||||
%reflection
|
||||
solveHasTable : Type -> Tactic
|
||||
|
|
@ -174,7 +174,7 @@ namespace Query
|
|||
-- -}
|
||||
|
||||
---------- Proofs ----------
|
||||
|
||||
Queries.Row.projectRow_lemma : Row s
|
||||
Queries.Row.projectRow_lemma = proof
|
||||
intros
|
||||
rewrite (attrEta attr)
|
||||
|
|
|
|||
|
|
@ -5,13 +5,13 @@ import Decidable.Equality
|
|||
%default total
|
||||
|
||||
|
||||
data SQLiteType = TEXT | INTEGER | REAL
|
||||
public export data SQLiteType = TEXT | INTEGER | REAL
|
||||
| NULLABLE SQLiteType
|
||||
|
||||
interpSql : SQLiteType -> Type
|
||||
export interpSql : SQLiteType -> Type
|
||||
interpSql TEXT = String
|
||||
interpSql INTEGER = Integer
|
||||
interpSql REAL = Float
|
||||
interpSql REAL = Double
|
||||
interpSql (NULLABLE x) = Maybe (interpSql x)
|
||||
|
||||
equalSql : (t : SQLiteType) -> (x, y : interpSql t) -> Bool
|
||||
|
|
@ -22,7 +22,7 @@ equalSql (NULLABLE ty) (Just x) (Just y) = equalSql ty x y
|
|||
equalSql (NULLABLE ty) Nothing Nothing = True
|
||||
equalSql (NULLABLE ty) _ _ = False
|
||||
|
||||
showSql : (t : SQLiteType) -> (x : interpSql t) -> String
|
||||
export showSql : (t : SQLiteType) -> (x : interpSql t) -> String
|
||||
showSql TEXT x = show x
|
||||
showSql INTEGER x = show x
|
||||
showSql REAL x = show x
|
||||
|
|
@ -48,8 +48,7 @@ nullableNotInteger Refl impossible
|
|||
nullableNotReal : NULLABLE t = REAL -> Void
|
||||
nullableNotReal Refl impossible
|
||||
|
||||
|
||||
instance DecEq SQLiteType where
|
||||
export implementation DecEq SQLiteType where
|
||||
decEq TEXT TEXT = Yes Refl
|
||||
decEq INTEGER TEXT = No integerNotText
|
||||
decEq REAL TEXT = No realNotText
|
||||
|
|
|
|||
|
|
@ -9,16 +9,16 @@ import Language.Reflection
|
|||
|
||||
|
||||
infix 5 :::
|
||||
data Attribute = (:::) String SQLiteType
|
||||
public export data Attribute = (:::) String SQLiteType
|
||||
%name Attribute attr,attr'
|
||||
|
||||
getName : Attribute -> String
|
||||
export getName : Attribute -> String
|
||||
getName (c:::_) = c
|
||||
|
||||
getTy : Attribute -> SQLiteType
|
||||
public export getTy : Attribute -> SQLiteType
|
||||
getTy (_:::t) = t
|
||||
|
||||
attrEta : (attr : Attribute) -> (getName attr ::: getTy attr) = attr
|
||||
public export attrEta : (attr : Attribute) -> (getName attr ::: getTy attr) = attr
|
||||
attrEta (x ::: y) = Refl
|
||||
|
||||
attrInj : (c ::: t = c' ::: t') -> (c=c', t=t')
|
||||
|
|
@ -32,16 +32,16 @@ foo x y with (decEq x y)
|
|||
foo x y | No urgh = No urgh
|
||||
|
||||
|
||||
instance DecEq Attribute where
|
||||
implementation DecEq Attribute where
|
||||
decEq (x ::: y) (z ::: w) with (foo x z, decEq y w)
|
||||
decEq (x ::: y) (x ::: y) | (Yes Refl, Yes Refl) = Yes Refl
|
||||
decEq (x ::: y) (x ::: w) | (Yes Refl, No prf) = No $ prf . snd . attrInj
|
||||
decEq (x ::: y) (z ::: w) | (No prf, _) = No $ prf . fst . attrInj
|
||||
|
||||
data Schema = Nil | (::) Attribute Schema
|
||||
public export data Schema = Nil | (::) Attribute Schema
|
||||
%name Schema s,s'
|
||||
|
||||
append : (s1, s2 : Schema) -> Schema
|
||||
export append : (s1, s2 : Schema) -> Schema
|
||||
append [] s2 = s2
|
||||
append (attr :: s) s2 = attr :: (append s s2)
|
||||
|
||||
|
|
@ -50,7 +50,7 @@ names [] = []
|
|||
names ((n ::: _) :: s) = n :: names s
|
||||
|
||||
|
||||
data HasCol : Schema -> Attribute -> Type where
|
||||
public export data HasCol : Schema -> Attribute -> Type where
|
||||
Here : HasCol (attr::s) attr
|
||||
There : HasCol s attr -> HasCol (attr'::s) attr
|
||||
|
||||
|
|
@ -58,7 +58,7 @@ HasColNotEmpty : HasCol [] a -> Void
|
|||
HasColNotEmpty Here impossible
|
||||
HasColNotEmpty (There _) impossible
|
||||
|
||||
instance Uninhabited (HasCol [] a) where
|
||||
implementation Uninhabited (HasCol [] a) where
|
||||
uninhabited x = HasColNotEmpty x
|
||||
|
||||
decHasColLemma : (HasCol s attr -> Void) ->
|
||||
|
|
@ -76,7 +76,7 @@ decHasCol (attr' :: s) attr with (decEq attr' attr)
|
|||
decHasCol (attr' :: s) attr | (No f) | (No g) = No $ \h => decHasColLemma g f h
|
||||
|
||||
|
||||
data SubSchema : Schema -> Schema -> Type where
|
||||
public export data SubSchema : Schema -> Schema -> Type where
|
||||
Empty : SubSchema [] s
|
||||
Head : (tailSub : SubSchema small large) ->
|
||||
(alsoThere : HasCol large attr) ->
|
||||
|
|
@ -92,23 +92,23 @@ decHasColNamed_lemma notThere notHere (ty ** (There more)) = notThere (ty ** mor
|
|||
|
||||
|
||||
decHasColNamed : (s : Schema) -> (col : String) -> Dec (HasColNamed s col)
|
||||
decHasColNamed [] col = No $ \h => HasColNotEmpty (getProof h)
|
||||
decHasColNamed [] col = No $ \h => HasColNotEmpty (snd h)
|
||||
decHasColNamed ((col' ::: ty) :: s) col with (decEq col' col)
|
||||
decHasColNamed ((col ::: ty) :: s) col | (Yes Refl) = Yes (ty ** Here)
|
||||
decHasColNamed ((col' ::: ty) :: s) col | (No f) with (decHasColNamed s col)
|
||||
decHasColNamed ((col' ::: ty) :: s) col | (No f) | (Yes x) =
|
||||
Yes (getWitness x ** There (getProof x))
|
||||
Yes (fst x ** There (snd x))
|
||||
decHasColNamed ((col' ::: ty) :: s) col | (No f) | (No g) = No (decHasColNamed_lemma g f)
|
||||
|
||||
colNames : Schema -> List String
|
||||
export colNames : Schema -> List String
|
||||
colNames [] = []
|
||||
colNames ((col ::: _) :: s) = col :: colNames s
|
||||
|
||||
data Disjointness : Type where
|
||||
public export data Disjointness : Type where
|
||||
Disjoint : Disjointness
|
||||
Overlap : (attr : Attribute) -> Disjointness
|
||||
|
||||
isDisjoint : (s1, s2 : Schema) -> Disjointness
|
||||
export isDisjoint : (s1, s2 : Schema) -> Disjointness
|
||||
isDisjoint [] s2 = Disjoint
|
||||
isDisjoint (attr :: s) s2 with (decHasColNamed s2 (getName attr))
|
||||
isDisjoint (attr :: s) s2 | (Yes x) = Overlap attr
|
||||
|
|
|
|||
|
|
@ -1,4 +1,10 @@
|
|||
package demo
|
||||
|
||||
opts = "-p effects -p sqlite -p lightyear"
|
||||
modules = Test, ErrorHandlers, parser, Schema, Database, ErrorTest, Provider, SQLiteTypes, ParserHack, Queries
|
||||
|
||||
executable = test
|
||||
|
||||
main = Test
|
||||
|
||||
pkgs = effects, sqlite, lightyear
|
||||
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user