From ef7e3891d4ba7d6156948ab9013f76f2ea7ab22b Mon Sep 17 00:00:00 2001 From: Colin Adams Date: Thu, 21 Apr 2016 08:27:24 +0100 Subject: [PATCH] Ready for pull request --- .gitignore | 3 +- README.md | 71 ++++++++++++++++++ .../ErrorTest.idr | 11 +-- error_test/error_test.ipkg | 10 +++ .../test.sqlite | Bin type-provider-demo/demo.ipkg | 10 --- .../Database.idr | 0 .../ErrorHandlers.idr | 2 + .../Parser.idr | 0 .../ParserHack.idr | 0 .../Provider.idr | 0 .../Queries.idr | 8 +- .../SQLiteTypes.idr | 0 .../Schema.idr | 24 +++--- type-provider/sqlite_provider.ipkg | 6 ++ .../Test.idr | 15 ++-- type_provider-demo/demo.ipkg | 10 +++ type_provider-demo/test.sqlite | Bin 0 -> 4096 bytes 18 files changed, 127 insertions(+), 43 deletions(-) rename {type-provider-demo => error_test}/ErrorTest.idr (89%) create mode 100644 error_test/error_test.ipkg rename {type-provider-demo => error_test}/test.sqlite (100%) delete mode 100644 type-provider-demo/demo.ipkg rename {type-provider-demo => type-provider}/Database.idr (100%) rename {type-provider-demo => type-provider}/ErrorHandlers.idr (98%) rename {type-provider-demo => type-provider}/Parser.idr (100%) rename {type-provider-demo => type-provider}/ParserHack.idr (100%) rename {type-provider-demo => type-provider}/Provider.idr (100%) rename {type-provider-demo => type-provider}/Queries.idr (97%) rename {type-provider-demo => type-provider}/SQLiteTypes.idr (100%) rename {type-provider-demo => type-provider}/Schema.idr (85%) create mode 100644 type-provider/sqlite_provider.ipkg rename {type-provider-demo => type_provider-demo}/Test.idr (87%) create mode 100644 type_provider-demo/demo.ipkg create mode 100644 type_provider-demo/test.sqlite 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 0000000000000000000000000000000000000000..26f481e50c1c8b0fc7bb561070b8b099da233f4c GIT binary patch literal 4096 zcmeHK&1%~~5Z={_h7x>f35K|b2^4B$n-EIRjT1W%kim&vN>61ijqJtp%Gq7D^&yA! z8A@KD_dY{kqOVZsxi8R>YD1m=Krew74O&J!JKAsbu`?PC&jRHT;?&HggU8HgoU=m! z#@H?mpT=6Y>E_2dUoZSY@3Qvit%`WZg!hn%Bkw(_QvNXpF8!@)t;Vm;oE#@;7bs_F zR?0g*?{!8!7Of~n0t=(&(kx+yOOTmMl@1NgQM(psIY)5# zhCEl^Ef}k`Fg30oh^^|*4u4xK@SRL%`4Ah(xdrM@x#Xvf9lA=lXQ??7k4J9i+}e8pALz%}P)1d4e@NR7$5*e+wfT0;~Q4utGK=PMG*0E=iSA zGEg$`*9<%ne!I^*8akoNq){?~?l9=$0(G9N$r9Xhfe|DsMrw>~W+e3yV&C(h?(=@C zWu!vrD{B?CFM-T-IHfcmst5t&7(+_$lhN}%Z@_)*-yP9jFfb`q2kOH>>Iizqqz2A0 zPRLoMnn2(*qQViNdt{;LjvVz