mirror of
https://github.com/ilyakooo0/IdrisSqlite.git
synced 2024-08-16 04:20:23 +03:00
Ready for pull request
This commit is contained in:
parent
c6b602557a
commit
ef7e3891d4
1
.gitignore
vendored
1
.gitignore
vendored
@ -4,3 +4,4 @@
|
|||||||
sqlite_test
|
sqlite_test
|
||||||
src/sqlite3api.so
|
src/sqlite3api.so
|
||||||
src/sqlite3api.o
|
src/sqlite3api.o
|
||||||
|
test
|
||||||
|
71
README.md
71
README.md
@ -19,4 +19,75 @@ expected output is:
|
|||||||
Done
|
Done
|
||||||
[[DBText "test", DBText "CREATE TABLE test (name INT, age INT)"]]
|
[[DBText "test", DBText "CREATE TABLE test (name INT, age INT)"]]
|
||||||
|
|
||||||
|
To install the type provider:
|
||||||
|
|
||||||
|
cd type-provider
|
||||||
|
|
||||||
|
idris --install sqlite_provider.ipkg
|
||||||
|
|
||||||
|
to run the type-provider demo:
|
||||||
|
|
||||||
|
cd ../type_provider-demo
|
||||||
|
|
||||||
|
idris --build demo.ipkg
|
||||||
|
|
||||||
|
./test
|
||||||
|
|
||||||
|
The expected output is:
|
||||||
|
|
||||||
|
|
||||||
|
The speakers are:
|
||||||
|
name|bio|
|
||||||
|
"David Christiansen"|"PhD student at ITU"|
|
||||||
|
"Another Speaker"|null|
|
||||||
|
"Lots of Speaking"|null|
|
||||||
|
|
||||||
|
The talks are:
|
||||||
|
title|abstract|
|
||||||
|
"Type Providers and Error Reflection in Idris"|"Let's talk to the outside world!"|
|
||||||
|
"Monadic Missile Launching"|"Side effects FTW!"|
|
||||||
|
"An Actuarial DSL"|"Dependently typed life insurance"|
|
||||||
|
|
||||||
|
Conference program
|
||||||
|
name|title|abstract|
|
||||||
|
"David Christiansen"|"Type Providers and Error Reflection in Idris"|"Let's talk to the outside world!"|
|
||||||
|
"Another Speaker"|"Monadic Missile Launching"|"Side effects FTW!"|
|
||||||
|
"Lots of Speaking"|"An Actuarial DSL"|"Dependently typed life insurance"|
|
||||||
|
|
||||||
|
ok
|
||||||
|
|
||||||
|
|
||||||
|
To run the error test demo:
|
||||||
|
|
||||||
|
cd ../error_test
|
||||||
|
idris --build error_test.ipkg
|
||||||
|
|
||||||
|
The expected output is:
|
||||||
|
|
||||||
|
Type checking ./ErrorTest.idr
|
||||||
|
ErrorTest.idr:30:12-32:1:
|
||||||
|
When checking right hand side of speakers with expected type
|
||||||
|
Query db ["name" ::: TEXT, "bio" ::: TEXT]
|
||||||
|
|
||||||
|
When checking argument ok to constructor Queries.Query.Select:
|
||||||
|
Bad schema:
|
||||||
|
"name" ::: TEXT
|
||||||
|
"bio" ::: TEXT
|
||||||
|
Expected subschema of
|
||||||
|
"id" ::: INTEGER
|
||||||
|
"name" ::: TEXT
|
||||||
|
"bio" ::: NULLABLE TEXT
|
||||||
|
ErrorTest.idr:39:33:
|
||||||
|
When checking right hand side of program with expected type
|
||||||
|
Query db
|
||||||
|
["name" ::: TEXT, "title" ::: TEXT, "abstract" ::: TEXT]
|
||||||
|
|
||||||
|
When checking argument ok to constructor Queries.Expr.Col:
|
||||||
|
The column "speaker_id" was not found with type INTEGER in the
|
||||||
|
schema
|
||||||
|
"id" ::: INTEGER
|
||||||
|
"name" ::: TEXT
|
||||||
|
"bio" ::: NULLABLE TEXT
|
||||||
|
"title" ::: TEXT
|
||||||
|
"abstract" ::: TEXT
|
||||||
|
"speaker" ::: INTEGER
|
||||||
|
@ -19,10 +19,9 @@ import SQLiteTypes
|
|||||||
%include C "sqlite3api.h"
|
%include C "sqlite3api.h"
|
||||||
%lib C "sqlite3"
|
%lib C "sqlite3"
|
||||||
|
|
||||||
|
%auto_implicits off
|
||||||
|
|
||||||
|
%provide (db : DB "test.sqlite") with run {m=IO} (getSchemas "test.sqlite")
|
||||||
|
|
||||||
%provide (db : DB "test.sqlite") with run (getSchemas "test.sqlite")
|
|
||||||
|
|
||||||
%error_handlers Col ok hasColErr
|
%error_handlers Col ok hasColErr
|
||||||
%error_handlers Select ok notSubSchemaErr
|
%error_handlers Select ok notSubSchemaErr
|
||||||
@ -30,8 +29,6 @@ import SQLiteTypes
|
|||||||
speakers : Query db ["name":::TEXT, "bio":::TEXT]
|
speakers : Query db ["name":::TEXT, "bio":::TEXT]
|
||||||
speakers = SELECT ["name":::TEXT, "bio":::TEXT] FROM "speaker" WHERE 1
|
speakers = SELECT ["name":::TEXT, "bio":::TEXT] FROM "speaker" WHERE 1
|
||||||
|
|
||||||
-- :x unsafePerformIO $ run $ query speakers
|
|
||||||
|
|
||||||
talks : Query db ["title":::TEXT, "abstract":::TEXT]
|
talks : Query db ["title":::TEXT, "abstract":::TEXT]
|
||||||
talks = SELECT ["title":::TEXT, "abstract":::TEXT] FROM "talk" WHERE 1
|
talks = SELECT ["title":::TEXT, "abstract":::TEXT] FROM "talk" WHERE 1
|
||||||
|
|
||||||
@ -41,9 +38,7 @@ program = SELECT ["name":::TEXT, "title":::TEXT, "abstract":::TEXT]
|
|||||||
FROM "speaker" * "talk"
|
FROM "speaker" * "talk"
|
||||||
WHERE Col "id" == Col "speaker_id"
|
WHERE Col "id" == Col "speaker_id"
|
||||||
|
|
||||||
|
printRes : {s : Schema} -> Query db s -> IO ()
|
||||||
|
|
||||||
printRes : Query db s -> IO ()
|
|
||||||
printRes q = do res <- runInit [()] (query q)
|
printRes q = do res <- runInit [()] (query q)
|
||||||
case res of
|
case res of
|
||||||
Left err => putStrLn (show err)
|
Left err => putStrLn (show err)
|
10
error_test/error_test.ipkg
Normal file
10
error_test/error_test.ipkg
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
package error_test
|
||||||
|
|
||||||
|
modules = ErrorTest
|
||||||
|
|
||||||
|
executable = test
|
||||||
|
|
||||||
|
main = ErrorTest
|
||||||
|
|
||||||
|
pkgs = sqlite_provider, effects, sqlite
|
||||||
|
|
@ -1,10 +0,0 @@
|
|||||||
package demo
|
|
||||||
|
|
||||||
modules = Test, ErrorHandlers, Parser, Schema, Database, ErrorTest, Provider, SQLiteTypes, ParserHack, Queries
|
|
||||||
|
|
||||||
executable = test
|
|
||||||
|
|
||||||
main = Test
|
|
||||||
|
|
||||||
pkgs = effects, sqlite, lightyear
|
|
||||||
|
|
@ -8,6 +8,8 @@ import Language.Reflection.Errors
|
|||||||
|
|
||||||
%language ErrorReflection
|
%language ErrorReflection
|
||||||
|
|
||||||
|
%access public export
|
||||||
|
|
||||||
||| Convert a reflected schema to a nice formatted error view
|
||| Convert a reflected schema to a nice formatted error view
|
||||||
getAttrs : TT -> List ErrorReportPart
|
getAttrs : TT -> List ErrorReportPart
|
||||||
getAttrs `(~a ::: ~b) = [SubReport
|
getAttrs `(~a ::: ~b) = [SubReport
|
@ -109,11 +109,11 @@ namespace Query
|
|||||||
|
|
||||||
data Tables : DB file -> Schema -> Type where
|
data Tables : DB file -> Schema -> Type where
|
||||||
T : (name : String) ->
|
T : (name : String) ->
|
||||||
{default tactics { byReflection solveHasTable;}
|
{default tactics { byReflection solveHasTable; }
|
||||||
ok : HasTable db name s} ->
|
ok : HasTable db name s} ->
|
||||||
Tables (MkDB file db) s
|
Tables (MkDB file db) s
|
||||||
(*) : (t1 : String) ->
|
(*) : (t1 : String) ->
|
||||||
{default tactics { byReflection solveHasTable; }
|
{auto
|
||||||
ok : HasTable db t1 s1} ->
|
ok : HasTable db t1 s1} ->
|
||||||
Tables (MkDB file db) s2 ->
|
Tables (MkDB file db) s2 ->
|
||||||
{auto disj : isDisjoint s1 s2 = Disjoint} ->
|
{auto disj : isDisjoint s1 s2 = Disjoint} ->
|
||||||
@ -121,7 +121,7 @@ namespace Query
|
|||||||
|
|
||||||
implicit
|
implicit
|
||||||
toTables : (tbl : String) ->
|
toTables : (tbl : String) ->
|
||||||
{default tactics { byReflection solveHasTable; }
|
{auto
|
||||||
ok : HasTable db tbl s} ->
|
ok : HasTable db tbl s} ->
|
||||||
Tables (MkDB name db) s
|
Tables (MkDB name db) s
|
||||||
toTables tbl {ok = ok} = T tbl {ok = ok}
|
toTables tbl {ok = ok} = T tbl {ok = ok}
|
||||||
@ -137,7 +137,7 @@ namespace Query
|
|||||||
(values : Table s) ->
|
(values : Table s) ->
|
||||||
Cmd (MkDB f db)
|
Cmd (MkDB f db)
|
||||||
Delete : (from : String) -> (s : Schema) ->
|
Delete : (from : String) -> (s : Schema) ->
|
||||||
{default tactics { byReflection solveHasTable;}
|
{default tactics { byReflection solveHasTable; }
|
||||||
ok : HasTable db from s} ->
|
ok : HasTable db from s} ->
|
||||||
(when : Expr s INTEGER) ->
|
(when : Expr s INTEGER) ->
|
||||||
Cmd (MkDB f db)
|
Cmd (MkDB f db)
|
@ -5,20 +5,22 @@ import SQLiteTypes
|
|||||||
import Decidable.Equality
|
import Decidable.Equality
|
||||||
import Language.Reflection
|
import Language.Reflection
|
||||||
|
|
||||||
|
%access public export
|
||||||
%default total
|
%default total
|
||||||
|
|
||||||
|
%auto_implicits on
|
||||||
|
|
||||||
infix 5 :::
|
infix 5 :::
|
||||||
public export data Attribute = (:::) String SQLiteType
|
data Attribute = (:::) String SQLiteType
|
||||||
%name Attribute attr,attr'
|
%name Attribute attr,attr'
|
||||||
|
|
||||||
export getName : Attribute -> String
|
getName : Attribute -> String
|
||||||
getName (c:::_) = c
|
getName (c:::_) = c
|
||||||
|
|
||||||
public export getTy : Attribute -> SQLiteType
|
getTy : Attribute -> SQLiteType
|
||||||
getTy (_:::t) = t
|
getTy (_:::t) = t
|
||||||
|
|
||||||
public export attrEta : (attr : Attribute) -> (getName attr ::: getTy attr) = attr
|
attrEta : (attr : Attribute) -> (getName attr ::: getTy attr) = attr
|
||||||
attrEta (x ::: y) = Refl
|
attrEta (x ::: y) = Refl
|
||||||
|
|
||||||
attrInj : (c ::: t = c' ::: t') -> (c=c', t=t')
|
attrInj : (c ::: t = c' ::: t') -> (c=c', t=t')
|
||||||
@ -38,10 +40,10 @@ implementation DecEq Attribute where
|
|||||||
decEq (x ::: y) (x ::: w) | (Yes Refl, No prf) = No $ prf . snd . attrInj
|
decEq (x ::: y) (x ::: w) | (Yes Refl, No prf) = No $ prf . snd . attrInj
|
||||||
decEq (x ::: y) (z ::: w) | (No prf, _) = No $ prf . fst . attrInj
|
decEq (x ::: y) (z ::: w) | (No prf, _) = No $ prf . fst . attrInj
|
||||||
|
|
||||||
public export data Schema = Nil | (::) Attribute Schema
|
data Schema = Nil | (::) Attribute Schema
|
||||||
%name Schema s,s'
|
%name Schema s,s'
|
||||||
|
|
||||||
export append : (s1, s2 : Schema) -> Schema
|
append : (s1, s2 : Schema) -> Schema
|
||||||
append [] s2 = s2
|
append [] s2 = s2
|
||||||
append (attr :: s) s2 = attr :: (append s s2)
|
append (attr :: s) s2 = attr :: (append s s2)
|
||||||
|
|
||||||
@ -50,7 +52,7 @@ names [] = []
|
|||||||
names ((n ::: _) :: s) = n :: names s
|
names ((n ::: _) :: s) = n :: names s
|
||||||
|
|
||||||
|
|
||||||
public export data HasCol : Schema -> Attribute -> Type where
|
data HasCol : Schema -> Attribute -> Type where
|
||||||
Here : HasCol (attr::s) attr
|
Here : HasCol (attr::s) attr
|
||||||
There : HasCol s attr -> HasCol (attr'::s) attr
|
There : HasCol s attr -> HasCol (attr'::s) attr
|
||||||
|
|
||||||
@ -76,7 +78,7 @@ decHasCol (attr' :: s) attr with (decEq attr' attr)
|
|||||||
decHasCol (attr' :: s) attr | (No f) | (No g) = No $ \h => decHasColLemma g f h
|
decHasCol (attr' :: s) attr | (No f) | (No g) = No $ \h => decHasColLemma g f h
|
||||||
|
|
||||||
|
|
||||||
public export data SubSchema : Schema -> Schema -> Type where
|
data SubSchema : Schema -> Schema -> Type where
|
||||||
Empty : SubSchema [] s
|
Empty : SubSchema [] s
|
||||||
Head : (tailSub : SubSchema small large) ->
|
Head : (tailSub : SubSchema small large) ->
|
||||||
(alsoThere : HasCol large attr) ->
|
(alsoThere : HasCol large attr) ->
|
||||||
@ -100,15 +102,15 @@ decHasColNamed ((col' ::: ty) :: s) col with (decEq col' col)
|
|||||||
Yes (fst x ** There (snd x))
|
Yes (fst x ** There (snd x))
|
||||||
decHasColNamed ((col' ::: ty) :: s) col | (No f) | (No g) = No (decHasColNamed_lemma g f)
|
decHasColNamed ((col' ::: ty) :: s) col | (No f) | (No g) = No (decHasColNamed_lemma g f)
|
||||||
|
|
||||||
export colNames : Schema -> List String
|
colNames : Schema -> List String
|
||||||
colNames [] = []
|
colNames [] = []
|
||||||
colNames ((col ::: _) :: s) = col :: colNames s
|
colNames ((col ::: _) :: s) = col :: colNames s
|
||||||
|
|
||||||
public export data Disjointness : Type where
|
data Disjointness : Type where
|
||||||
Disjoint : Disjointness
|
Disjoint : Disjointness
|
||||||
Overlap : (attr : Attribute) -> Disjointness
|
Overlap : (attr : Attribute) -> Disjointness
|
||||||
|
|
||||||
export isDisjoint : (s1, s2 : Schema) -> Disjointness
|
isDisjoint : (s1, s2 : Schema) -> Disjointness
|
||||||
isDisjoint [] s2 = Disjoint
|
isDisjoint [] s2 = Disjoint
|
||||||
isDisjoint (attr :: s) s2 with (decHasColNamed s2 (getName attr))
|
isDisjoint (attr :: s) s2 with (decHasColNamed s2 (getName attr))
|
||||||
isDisjoint (attr :: s) s2 | (Yes x) = Overlap attr
|
isDisjoint (attr :: s) s2 | (Yes x) = Overlap attr
|
6
type-provider/sqlite_provider.ipkg
Normal file
6
type-provider/sqlite_provider.ipkg
Normal file
@ -0,0 +1,6 @@
|
|||||||
|
package sqlite_provider
|
||||||
|
|
||||||
|
modules = ErrorHandlers, Schema, Database, Provider, SQLiteTypes, ParserHack, Queries
|
||||||
|
|
||||||
|
pkgs = effects, sqlite, lightyear
|
||||||
|
|
@ -16,12 +16,9 @@ import SQLiteTypes
|
|||||||
%include C "sqlite3api.h"
|
%include C "sqlite3api.h"
|
||||||
%lib C "sqlite3"
|
%lib C "sqlite3"
|
||||||
|
|
||||||
|
%auto_implicits off
|
||||||
|
|
||||||
|
|
||||||
%provide (db : DB "test.sqlite")
|
%provide (db : DB "test.sqlite")
|
||||||
with run (getSchemas "test.sqlite")
|
with run {m = IO} (getSchemas "test.sqlite")
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
speakers : Query db ["name":::TEXT, "bio":::NULLABLE TEXT]
|
speakers : Query db ["name":::TEXT, "bio":::NULLABLE TEXT]
|
||||||
@ -29,8 +26,6 @@ speakers = SELECT ["name":::TEXT, "bio":::NULLABLE TEXT]
|
|||||||
FROM "speaker"
|
FROM "speaker"
|
||||||
WHERE 1
|
WHERE 1
|
||||||
|
|
||||||
-- :x unsafePerformIO $ run $ query speakers
|
|
||||||
|
|
||||||
talks : Query db ["title":::TEXT, "abstract":::TEXT]
|
talks : Query db ["title":::TEXT, "abstract":::TEXT]
|
||||||
talks = SELECT ["title":::TEXT, "abstract":::TEXT]
|
talks = SELECT ["title":::TEXT, "abstract":::TEXT]
|
||||||
FROM "talk"
|
FROM "talk"
|
||||||
@ -41,11 +36,13 @@ program = SELECT ["name":::TEXT, "title":::TEXT, "abstract":::TEXT]
|
|||||||
FROM "speaker" * "talk"
|
FROM "speaker" * "talk"
|
||||||
WHERE Col "id" == Col "speaker"
|
WHERE Col "id" == Col "speaker"
|
||||||
|
|
||||||
printRes : Query db s -> IO ()
|
|
||||||
printRes q = do res <- runInit [()] (query q)
|
printRes : {s : Schema} -> Query db s -> IO ()
|
||||||
|
printRes q = do res <- runInit {m = IO} [()] (query q)
|
||||||
case res of
|
case res of
|
||||||
Left err => putStrLn (show err)
|
Left err => putStrLn (show err)
|
||||||
Right table => putStrLn (showTable _ table)
|
Right table => putStrLn (showTable _ table)
|
||||||
|
|
||||||
namespace Main
|
namespace Main
|
||||||
main : IO ()
|
main : IO ()
|
||||||
main = do putStrLn "The speakers are:"
|
main = do putStrLn "The speakers are:"
|
10
type_provider-demo/demo.ipkg
Normal file
10
type_provider-demo/demo.ipkg
Normal file
@ -0,0 +1,10 @@
|
|||||||
|
package demo
|
||||||
|
|
||||||
|
modules = Test
|
||||||
|
|
||||||
|
executable = test
|
||||||
|
|
||||||
|
main = Test
|
||||||
|
|
||||||
|
pkgs = sqlite_provider, effects, sqlite
|
||||||
|
|
BIN
type_provider-demo/test.sqlite
Normal file
BIN
type_provider-demo/test.sqlite
Normal file
Binary file not shown.
Loading…
Reference in New Issue
Block a user