8b7db47 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Linux compatibility and Idris updates

8b7db47David Christiansen13 years ago

contribs/lib/SQLite3/Makefile+1−1

compare with master

unifiedsplit

@@ -3,7 +3,7 @@

4.PHONY: all

6−sqltest : testunit.idr sqlite3.idr sqlite3api.o

6+sqltest : testunit.idr Sqlite3.idr sqlite3api.o

7 idris testunit.idr -o sqltest

9sqlite3api.o : sqlite3api.c

contribs/lib/SQLite3/sqlexpr.idr → contribs/lib/SQLite3/Sqlexpr.idrrenamed+27−25

@@ -33,38 +33,40 @@ data Cond = Equals Value Value

33 |MkLTE Value Value

34 |MkNULL Value

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−

46data SelVar = Cols (List String)

36data SelVar = Cols (List String)

47− |ALL

37+ | ALL

49data ColType = CInt String -- parsed as string "int"

39data ColType = CInt String -- parsed as string "int"

50− |Varchar String

40+ | Varchar String

51−

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+

52−data Constr = NOTNULL

54+ data Constr = NOTNULL

53− | UNIQUE Constr

55+ | UNIQUE Constr

54− | None

56+ | None

55− | PRIMARYKEY

57+ | PRIMARYKEY

56− | FOREIGNKEY

58+ | FOREIGNKEY

57− | CHECK

59+ | CHECK

58− | DEFAULT

60+ | DEFAULT

59−

61+

60−

62+

61−data SQL = SELECT SelVar SQL Clause

63+ data SQL = SELECT SelVar SQL Clause

62− | TBL (List String)

64+ | TBL (List String)

63 | INSERT SQL (List Value)

65 | INSERT SQL (List Value)

64 | INSERTC SQL (List Value) (List Value)

66 | INSERTC SQL (List Value) (List Value)

65 | UPDATE SQL condClause

67 | UPDATE SQL condClause

66 | CREATE SQL (List (Value, ColType , Constr))

68 | CREATE SQL (List (Value, ColType , Constr))

67−

69+

68-- remember to remove these funcs later

70-- remember to remove these funcs later

69-- foldr1 : (a -> a -> a) -> List a -> a

71-- foldr1 : (a -> a -> a) -> List a -> a

70-- foldr1 f [x] = x

72-- foldr1 f [x] = x

contribs/lib/SQLite3/sqlite3.idr → contribs/lib/SQLite3/Sqlite3.idrrenamed+28−16

@@ -30,16 +30,32 @@ data TBPointer = MkTBPointer Ptr

30-- Statement pointer

31data StmtPtr = MkStmtPtr Ptr

33−Table : Set

33+Table : Type

34Table = List (List DBVal)

36-- ForMap used in to_list_v1

37−forM : Monad m => List a -> (a -> m b) -> m (List b)

37+forM : Applicative f => List a -> (a -> f b) -> f (List b)

38−forM f xs = mapM xs f

38+forM xs f = (sequence (map f xs))

40-- Neater error handling done using DB

41data DB a = MkDB (IO (Either String a))

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+

43instance Monad DB where

59instance Monad DB where

44 (MkDB l) >>= k = MkDB (do c <- l

60 (MkDB l) >>= k = MkDB (do c <- l

45 case c of

61 case c of

@@ -299,20 +315,16 @@ get_data (MkDBPointer pointer) row col = do

299-----------------------------------------------------------------------------

315-----------------------------------------------------------------------------

300

316

301toList_v1 : DBPointer -> DB Table

317toList_v1 : DBPointer -> DB Table

302−toList_v1 db = do

303− nbR <- liftIO (num_row_v2 db)

318+toList_v1 db = do nbR <- liftIO (num_row_v2 db)

304− nmC <- liftIO (num_col_v2 db)

319+ nmC <- liftIO (num_col_v2 db)

320+

305− res <- forM [0..(nbR-1)] (\ i =>

321+ res <- liftIO $ forM [0..(nbR-1)] (\ i =>

306− forM [0..(nmC-1)] (\ j =>

322+ forM [0..(nmC-1)] (\ j => get_data db i j)

307− liftIO(get_data db i j)

308−

309− )

310− )

323+ )

311− return res

324+ return (the (List (List DBVal)) res)

312−

325+

313−

314strcat : String -> String-> String

326strcat : String -> String-> String

315−strcat str1 str2 = (str1 ++ str2)

327+strcat str1 str2 = (str1 ++ str2)

316

328

317-----------------------------------------------------------------------------

329-----------------------------------------------------------------------------

318-- | This version of toList retunrs result from get_table

330-- | This version of toList retunrs result from get_table