These SQLite bindings are forked from IdrisWeb.
To install:
Make sure your idris command was built with libffi support (if not rebuild it so - you will need to create a custom.mk file - copy custom.mk-alldeps and edit it)
idris --install sqlite.ipkg
to test installation:
idris --build sqlite_test.ipkg ./sqlite_test
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