Type-providers demo all but compiles - cant find implementation Handler Sqlite m

type-provider-demo/ParserHack.idr

@@ -2,6 +2,8 @@ module ParserHack
 import Schema
 import SQLiteTypes
 
+%access export
+
 people : String
 people = "CREATE TABLE \"people\" (\"id\" INTEGER PRIMARY KEY  AUTOINCREMENT  NOT NULL  UNIQUE , \"name\" VARCHAR NOT NULL , \"age\" INTEGER)"
 

type-provider-demo/Provider.idr

@@ -10,6 +10,8 @@ import Queries
 import Schema
 import SQLiteTypes
 
+%access export
+
 %language TypeProviders
 
 mkDB : ResultSet -> Either String (List (String, Schema))
@@ -22,7 +24,7 @@ mkDB ([DBText v]::rest) =
         Right List.(::) <*> Right (t, tbl) <*> mkDB rest
 mkDB _ = Left "Couldn't understand SQLite output - wrong type"
 
-getSchemas : (filename : String) -> { [SQLITE ()] } Eff (Provider (DB filename))
+getSchemas : (filename : String) -> Eff (Provider (DB filename)) [SQLITE ()] 
 getSchemas file =
   do let ddlQuery = "SELECT `sql` FROM `sqlite_master` " ++
                     "WHERE NOT (sqlite_master.name LIKE \"sqlite%\");"
@@ -35,24 +37,23 @@ getSchemas file =
                       Left err => pure (Error err)
                       Right db => pure (Provide (MkDB file db))
 
-getRow : (s : Schema) -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff (Row s)
+getRow : (s : Schema) -> SimpleEff.Eff (Row s) [SQLITE (SQLiteExecuting ValidRow)]
 getRow s = go 0 s
-  where go : Int -> (s : Schema) -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff (Row s)
+  where go : Int -> (s : Schema) -> Eff (Row s) [SQLITE (SQLiteExecuting ValidRow)]
         go i []          = pure []
         go i ((_ ::: ty) :: s) = [| getCol ty :: go (i+1) s |]
-          where getCol : (t : SQLiteType) -> { [SQLITE (SQLiteExecuting ValidRow)] } Eff (interpSql t)
+          where getCol : (t : SQLiteType) -> Eff (interpSql t) [SQLITE (SQLiteExecuting ValidRow)]
                 getCol TEXT = getColumnText i
                 getCol INTEGER = do int <- getColumnInt i
                                     pure (cast int)
                 getCol REAL = getColumnFloat i
                 getCol (NULLABLE x) = do nullp <- isColumnNull i
-                                         if nullp
+                                         case nullp of
-                                           then pure Nothing
+                                           True => pure Nothing
-                                           else do val <- getCol x
+                                           False => do val <- getCol x
                                                        pure (Just val)
 
-collectRows : (s : Schema) -> { [SQLITE (SQLiteExecuting ValidRow)] ==>
+collectRows : (s : Schema) -> Eff (Table s) [SQLITE (SQLiteExecuting ValidRow)] [SQLITE (SQLiteExecuting InvalidRow)]
-                                [SQLITE (SQLiteExecuting InvalidRow)] } Eff (Table s)
 collectRows s = do row <- getRow s
                    case !nextRow of
                      Unstarted => pure $ row :: !(collectRows s)
@@ -60,8 +61,7 @@ collectRows s = do row <- getRow s
                      StepComplete => pure $ row :: !(collectRows s)
                      NoMoreRows => pure [row]
 
-query : {file : String} -> {db : DB file} -> Query db s ->
+query : {file : String} -> {db : DB file} -> Query db s -> Eff (Either QueryError (Table s)) [SQLITE ()]
-        { [SQLITE ()] } Eff (Either QueryError (Table s))
 query {file=fn} q =
   case !(openDB fn) of
     Left err => pure $ Left err

type-provider-demo/Queries.idr

@@ -9,6 +9,7 @@ import Language.Reflection
 import Language.Reflection.Errors
 import Language.Reflection.Utils
 
+%access public export
 %default total
 %language ErrorReflection
 
@@ -106,7 +107,6 @@ namespace Query
   solveHasTable (HasTable ts n s) = reflectListPrf ts `Seq` Solve
   solveHasTable (HasTable (x ++ y) n s) = Solve
 
-
   data Tables : DB file -> Schema -> Type where
     T : (name : String) ->
         {default tactics { byReflection solveHasTable;}
@@ -164,18 +164,9 @@ namespace Query
     where cols : String
           cols = Foldable.concat . List.intersperse ", " . colNames $ proj
 
-
-
-
-
-
--- -}
--- -}
--- -}
-
 ---------- Proofs ----------
-Queries.Row.projectRow_lemma : Row s
+
-Queries.Row.projectRow_lemma = proof
+Queries.Row0.projectRow_lemma = proof
   intros
   rewrite (attrEta attr)
   exact value

type-provider-demo/SQLiteTypes.idr

@@ -8,7 +8,7 @@ import Decidable.Equality
 public export data SQLiteType = TEXT | INTEGER | REAL
                 | NULLABLE SQLiteType
 
-export interpSql : SQLiteType -> Type
+public export interpSql : SQLiteType -> Type
 interpSql TEXT = String
 interpSql INTEGER = Integer
 interpSql REAL = Double

type-provider-demo/Test.idr

@@ -36,14 +36,11 @@ talks = SELECT ["title":::TEXT, "abstract":::TEXT]
         FROM "talk"
         WHERE 1
 
-
 program : Query db ["name":::TEXT, "title":::TEXT, "abstract":::TEXT]
 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)
                 case res of

type-provider-demo/demo.ipkg

@@ -1,6 +1,6 @@
 package demo
 
-modules = Test, ErrorHandlers, parser, Schema, Database, ErrorTest, Provider, SQLiteTypes, ParserHack, Queries
+modules = Test, ErrorHandlers, Parser, Schema, Database, ErrorTest, Provider, SQLiteTypes, ParserHack, Queries
 
 executable = test