git.iko.soy/Idris-dev
on master help sign in
Linux compatibility and Idris updates

The SQLite bindings now work on case-sensitive filesystems. Additionally, they've been updated to work with the latest Idris stdlib.

commit8b7db47f0d1ced64a8c3c685471f6bcc4df1be4c authorDavid Christiansen <david@davidchristiansen.dk> dateTue 30 Apr 2013, 22:20 (13 years ago) parentdfbb3db
3 files changed+56−42
compare with master
unifiedsplit
contribs/lib/SQLite3/Makefile+1−1 contribs/lib/SQLite3/sqlexpr.idr → contribs/lib/SQLite3/Sqlexpr.idr+27−25 contribs/lib/SQLite3/sqlite3.idr → contribs/lib/SQLite3/Sqlite3.idr+28−16
contribs/lib/SQLite3/Makefile+1−1
@@ -3,7 +3,7 @@
33
44.PHONY: all
55
6−sqltest : testunit.idr sqlite3.idr sqlite3api.o
6+sqltest : testunit.idr Sqlite3.idr sqlite3api.o
77 idris testunit.idr -o sqltest
88
99sqlite3api.o : sqlite3api.c
contribs/lib/SQLite3/sqlexpr.idr → contribs/lib/SQLite3/Sqlexpr.idrrenamed+27−25
@@ -33,38 +33,40 @@ data Cond = Equals Value Value
3333 |MkLTE Value Value
3434 |MkNULL Value
3535
36−
37−data Clause = MkCond Cond
38− | AND Clause Clause
39− | OR Clause Clause
40− | Empty
41− | MkSQL SQL
42−
43−data condClause = SET Clause
44− |WHERE condClause Clause
45−
4636data SelVar = Cols (List String)
47− |ALL
37+ | ALL
4838
4939data ColType = CInt String -- parsed as string "int"
50− |Varchar String
51−
52−data Constr = NOTNULL
53− | UNIQUE Constr
54− | None
55− | PRIMARYKEY
56− | FOREIGNKEY
57− | CHECK
58− | DEFAULT
59−
60−
61−data SQL = SELECT SelVar SQL Clause
62− | TBL (List String)
40+ | Varchar String
41+
42+
43+
44+mutual
45+ data Clause = MkCond Cond
46+ | AND Clause Clause
47+ | OR Clause Clause
48+ | Empty
49+ | MkSQL SQL
50+
51+ data condClause = SET Clause
52+ | WHERE condClause Clause
53+
54+ data Constr = NOTNULL
55+ | UNIQUE Constr
56+ | None
57+ | PRIMARYKEY
58+ | FOREIGNKEY
59+ | CHECK
60+ | DEFAULT
61+
62+
63+ data SQL = SELECT SelVar SQL Clause
64+ | TBL (List String)
6365 | INSERT SQL (List Value)
6466 | INSERTC SQL (List Value) (List Value)
6567 | UPDATE SQL condClause
6668 | CREATE SQL (List (Value, ColType , Constr))
67−
69+
6870-- remember to remove these funcs later
6971-- foldr1 : (a -> a -> a) -> List a -> a
7072-- foldr1 f [x] = x
contribs/lib/SQLite3/sqlite3.idr → contribs/lib/SQLite3/Sqlite3.idrrenamed+28−16
@@ -30,16 +30,32 @@ data TBPointer = MkTBPointer Ptr
3030-- Statement pointer
3131data StmtPtr = MkStmtPtr Ptr
3232
33−Table : Set
33+Table : Type
3434Table = List (List DBVal)
3535
3636-- ForMap used in to_list_v1
37−forM : Monad m => List a -> (a -> m b) -> m (List b)
38−forM f xs = mapM xs f
37+forM : Applicative f => List a -> (a -> f b) -> f (List b)
38+forM xs f = (sequence (map f xs))
3939
4040-- Neater error handling done using DB
4141data DB a = MkDB (IO (Either String a))
4242
43+instance Functor DB where
44+ fmap f (MkDB action) = MkDB (do res <- action
45+ case res of
46+ Left x => return (Left x)
47+ Right x => return (Right (f x)))
48+
49+instance Applicative DB where
50+ pure = MkDB . return . Right
51+ (MkDB f) <$> (MkDB x) = MkDB (do f' <- f -- FIXME make pretty
52+ case f' of
53+ Left err => return (Left err)
54+ Right op => do x' <- x
55+ case x' of
56+ Left err => return (Left err)
57+ Right v => return (Right (op v)))
58+
4359instance Monad DB where
4460 (MkDB l) >>= k = MkDB (do c <- l
4561 case c of
@@ -299,20 +315,16 @@ get_data (MkDBPointer pointer) row col = do
299315-----------------------------------------------------------------------------
300316
301317toList_v1 : DBPointer -> DB Table
302−toList_v1 db = do
303− nbR <- liftIO (num_row_v2 db)
304− nmC <- liftIO (num_col_v2 db)
305− res <- forM [0..(nbR-1)] (\ i =>
306− forM [0..(nmC-1)] (\ j =>
307− liftIO(get_data db i j)
308−
309− )
310− )
311− return res
312−
313−
318+toList_v1 db = do nbR <- liftIO (num_row_v2 db)
319+ nmC <- liftIO (num_col_v2 db)
320+
321+ res <- liftIO $ forM [0..(nbR-1)] (\ i =>
322+ forM [0..(nmC-1)] (\ j => get_data db i j)
323+ )
324+ return (the (List (List DBVal)) res)
325+
314326strcat : String -> String-> String
315−strcat str1 str2 = (str1 ++ str2)
327+strcat str1 str2 = (str1 ++ str2)
316328
317329-----------------------------------------------------------------------------
318330-- | This version of toList retunrs result from get_table