diff --git a/.gitignore b/.gitignore index ab30580..039edc2 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,6 @@ *~ *.ibc -*.o \ No newline at end of file +*.o +sqlite_test +src/sqlite3api.so +src/sqlite3api.o \ No newline at end of file diff --git a/README.md b/README.md index 944afec..2a2c49c 100644 --- a/README.md +++ b/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)"]] + + diff --git a/sqlite.ipkg b/sqlite.ipkg index 11ccde3..2e34296 100644 --- a/sqlite.ipkg +++ b/sqlite.ipkg @@ -1,6 +1,6 @@ package sqlite -opts = "-p effects" +pkgs = effects sourcedir = src modules = DB.SQLite.Effect, DB.SQLite.SQLiteCodes diff --git a/src/DB/SQLite/Effect.idr b/src/DB/SQLite/Effect.idr index c0d00de..f8a8835 100644 --- a/src/DB/SQLite/Effect.idr +++ b/src/DB/SQLite/Effect.idr @@ -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: diff --git a/src/DB/SQLite/SQLiteTest.idr b/src/DB/SQLite/SQLiteTest.idr index 808a740..80cffd0 100644 --- a/src/DB/SQLite/SQLiteTest.idr +++ b/src/DB/SQLite/SQLiteTest.idr @@ -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 diff --git a/test.db b/test.db index 5c42f62..26f6bca 100644 Binary files a/test.db and b/test.db differ diff --git a/type-provider-demo/Database.idr b/type-provider-demo/Database.idr index 410e508..cd7c8d3 100644 --- a/type-provider-demo/Database.idr +++ b/type-provider-demo/Database.idr @@ -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 diff --git a/type-provider-demo/Provider.idr b/type-provider-demo/Provider.idr index 99283e6..948e283 100644 --- a/type-provider-demo/Provider.idr +++ b/type-provider-demo/Provider.idr @@ -1,7 +1,5 @@ module Provider -import public Providers - import DB.SQLite.Effect import DB.SQLite.SQLiteCodes import Effects diff --git a/type-provider-demo/Queries.idr b/type-provider-demo/Queries.idr index adef256..d7a90b7 100644 --- a/type-provider-demo/Queries.idr +++ b/type-provider-demo/Queries.idr @@ -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) diff --git a/type-provider-demo/SQLiteTypes.idr b/type-provider-demo/SQLiteTypes.idr index 29ab172..a7e749e 100644 --- a/type-provider-demo/SQLiteTypes.idr +++ b/type-provider-demo/SQLiteTypes.idr @@ -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 diff --git a/type-provider-demo/Schema.idr b/type-provider-demo/Schema.idr index 3676481..5dcbad7 100644 --- a/type-provider-demo/Schema.idr +++ b/type-provider-demo/Schema.idr @@ -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 diff --git a/type-provider-demo/demo.ipkg b/type-provider-demo/demo.ipkg index 02ba319..755c58b 100644 --- a/type-provider-demo/demo.ipkg +++ b/type-provider-demo/demo.ipkg @@ -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