diff --git a/.gitignore b/.gitignore index 039edc2..45f7479 100644 --- a/.gitignore +++ b/.gitignore @@ -3,4 +3,5 @@ *.o sqlite_test src/sqlite3api.so -src/sqlite3api.o \ No newline at end of file +src/sqlite3api.o +test diff --git a/README.md b/README.md index 2fa3a75..433e5ed 100644 --- a/README.md +++ b/README.md @@ -19,4 +19,75 @@ expected output is: Done [[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 diff --git a/type-provider-demo/ErrorTest.idr b/error_test/ErrorTest.idr similarity index 89% rename from type-provider-demo/ErrorTest.idr rename to error_test/ErrorTest.idr index aeecc51..e148cbb 100644 --- a/type-provider-demo/ErrorTest.idr +++ b/error_test/ErrorTest.idr @@ -19,10 +19,9 @@ import SQLiteTypes %include C "sqlite3api.h" %lib C "sqlite3" +%auto_implicits off - - -%provide (db : DB "test.sqlite") with run (getSchemas "test.sqlite") +%provide (db : DB "test.sqlite") with run {m=IO} (getSchemas "test.sqlite") %error_handlers Col ok hasColErr %error_handlers Select ok notSubSchemaErr @@ -30,8 +29,6 @@ import SQLiteTypes speakers : Query db ["name":::TEXT, "bio":::TEXT] speakers = SELECT ["name":::TEXT, "bio":::TEXT] FROM "speaker" WHERE 1 --- :x unsafePerformIO $ run $ query speakers - talks : Query db ["title":::TEXT, "abstract":::TEXT] 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" WHERE Col "id" == Col "speaker_id" - - -printRes : Query db s -> IO () +printRes : {s : Schema} -> Query db s -> IO () printRes q = do res <- runInit [()] (query q) case res of Left err => putStrLn (show err) diff --git a/error_test/error_test.ipkg b/error_test/error_test.ipkg new file mode 100644 index 0000000..2e95326 --- /dev/null +++ b/error_test/error_test.ipkg @@ -0,0 +1,10 @@ +package error_test + +modules = ErrorTest + +executable = test + +main = ErrorTest + +pkgs = sqlite_provider, effects, sqlite + diff --git a/type-provider-demo/test.sqlite b/error_test/test.sqlite similarity index 100% rename from type-provider-demo/test.sqlite rename to error_test/test.sqlite diff --git a/type-provider-demo/demo.ipkg b/type-provider-demo/demo.ipkg deleted file mode 100644 index 1b9f9b4..0000000 --- a/type-provider-demo/demo.ipkg +++ /dev/null @@ -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 - diff --git a/type-provider-demo/Database.idr b/type-provider/Database.idr similarity index 100% rename from type-provider-demo/Database.idr rename to type-provider/Database.idr diff --git a/type-provider-demo/ErrorHandlers.idr b/type-provider/ErrorHandlers.idr similarity index 98% rename from type-provider-demo/ErrorHandlers.idr rename to type-provider/ErrorHandlers.idr index 485a795..8428803 100644 --- a/type-provider-demo/ErrorHandlers.idr +++ b/type-provider/ErrorHandlers.idr @@ -8,6 +8,8 @@ import Language.Reflection.Errors %language ErrorReflection +%access public export + ||| Convert a reflected schema to a nice formatted error view getAttrs : TT -> List ErrorReportPart getAttrs `(~a ::: ~b) = [SubReport diff --git a/type-provider-demo/Parser.idr b/type-provider/Parser.idr similarity index 100% rename from type-provider-demo/Parser.idr rename to type-provider/Parser.idr diff --git a/type-provider-demo/ParserHack.idr b/type-provider/ParserHack.idr similarity index 100% rename from type-provider-demo/ParserHack.idr rename to type-provider/ParserHack.idr diff --git a/type-provider-demo/Provider.idr b/type-provider/Provider.idr similarity index 100% rename from type-provider-demo/Provider.idr rename to type-provider/Provider.idr diff --git a/type-provider-demo/Queries.idr b/type-provider/Queries.idr similarity index 97% rename from type-provider-demo/Queries.idr rename to type-provider/Queries.idr index d32cdd7..1ac382e 100644 --- a/type-provider-demo/Queries.idr +++ b/type-provider/Queries.idr @@ -109,11 +109,11 @@ namespace Query data Tables : DB file -> Schema -> Type where T : (name : String) -> - {default tactics { byReflection solveHasTable;} + {default tactics { byReflection solveHasTable; } ok : HasTable db name s} -> Tables (MkDB file db) s (*) : (t1 : String) -> - {default tactics { byReflection solveHasTable; } + {auto ok : HasTable db t1 s1} -> Tables (MkDB file db) s2 -> {auto disj : isDisjoint s1 s2 = Disjoint} -> @@ -121,7 +121,7 @@ namespace Query implicit toTables : (tbl : String) -> - {default tactics { byReflection solveHasTable; } + {auto ok : HasTable db tbl s} -> Tables (MkDB name db) s toTables tbl {ok = ok} = T tbl {ok = ok} @@ -137,7 +137,7 @@ namespace Query (values : Table s) -> Cmd (MkDB f db) Delete : (from : String) -> (s : Schema) -> - {default tactics { byReflection solveHasTable;} + {default tactics { byReflection solveHasTable; } ok : HasTable db from s} -> (when : Expr s INTEGER) -> Cmd (MkDB f db) diff --git a/type-provider-demo/SQLiteTypes.idr b/type-provider/SQLiteTypes.idr similarity index 100% rename from type-provider-demo/SQLiteTypes.idr rename to type-provider/SQLiteTypes.idr diff --git a/type-provider-demo/Schema.idr b/type-provider/Schema.idr similarity index 85% rename from type-provider-demo/Schema.idr rename to type-provider/Schema.idr index 5dcbad7..bc39f1e 100644 --- a/type-provider-demo/Schema.idr +++ b/type-provider/Schema.idr @@ -5,20 +5,22 @@ import SQLiteTypes import Decidable.Equality import Language.Reflection +%access public export %default total +%auto_implicits on infix 5 ::: -public export data Attribute = (:::) String SQLiteType +data Attribute = (:::) String SQLiteType %name Attribute attr,attr' -export getName : Attribute -> String +getName : Attribute -> String getName (c:::_) = c -public export getTy : Attribute -> SQLiteType +getTy : Attribute -> SQLiteType 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 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) (z ::: w) | (No prf, _) = No $ prf . fst . attrInj -public export data Schema = Nil | (::) Attribute Schema +data Schema = Nil | (::) Attribute Schema %name Schema s,s' -export append : (s1, s2 : Schema) -> Schema +append : (s1, s2 : Schema) -> Schema append [] s2 = s2 append (attr :: s) s2 = attr :: (append s s2) @@ -50,7 +52,7 @@ names [] = [] 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 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 -public export data SubSchema : Schema -> Schema -> Type where +data SubSchema : Schema -> Schema -> Type where Empty : SubSchema [] s Head : (tailSub : SubSchema small large) -> (alsoThere : HasCol large attr) -> @@ -100,15 +102,15 @@ decHasColNamed ((col' ::: ty) :: s) col with (decEq col' col) Yes (fst x ** There (snd x)) 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 ((col ::: _) :: s) = col :: colNames s -public export data Disjointness : Type where +data Disjointness : Type where Disjoint : Disjointness Overlap : (attr : Attribute) -> Disjointness -export isDisjoint : (s1, s2 : Schema) -> Disjointness +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/sqlite_provider.ipkg b/type-provider/sqlite_provider.ipkg new file mode 100644 index 0000000..238ba45 --- /dev/null +++ b/type-provider/sqlite_provider.ipkg @@ -0,0 +1,6 @@ +package sqlite_provider + +modules = ErrorHandlers, Schema, Database, Provider, SQLiteTypes, ParserHack, Queries + +pkgs = effects, sqlite, lightyear + diff --git a/type-provider-demo/Test.idr b/type_provider-demo/Test.idr similarity index 87% rename from type-provider-demo/Test.idr rename to type_provider-demo/Test.idr index d11b9f3..3a86c26 100644 --- a/type-provider-demo/Test.idr +++ b/type_provider-demo/Test.idr @@ -16,20 +16,15 @@ import SQLiteTypes %include C "sqlite3api.h" %lib C "sqlite3" - - - +%auto_implicits off %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 = SELECT ["name":::TEXT, "bio":::NULLABLE TEXT] FROM "speaker" WHERE 1 - --- :x unsafePerformIO $ run $ query speakers talks : Query db ["title":::TEXT, "abstract":::TEXT] talks = SELECT ["title":::TEXT, "abstract":::TEXT] @@ -41,11 +36,13 @@ program = SELECT ["name":::TEXT, "title":::TEXT, "abstract":::TEXT] FROM "speaker" * "talk" 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 Left err => putStrLn (show err) Right table => putStrLn (showTable _ table) + namespace Main main : IO () main = do putStrLn "The speakers are:" diff --git a/type_provider-demo/demo.ipkg b/type_provider-demo/demo.ipkg new file mode 100644 index 0000000..e5a8fe9 --- /dev/null +++ b/type_provider-demo/demo.ipkg @@ -0,0 +1,10 @@ +package demo + +modules = Test + +executable = test + +main = Test + +pkgs = sqlite_provider, effects, sqlite + diff --git a/type_provider-demo/test.sqlite b/type_provider-demo/test.sqlite new file mode 100644 index 0000000..26f481e Binary files /dev/null and b/type_provider-demo/test.sqlite differ