6ce39ad · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

changed TBL String to list

commit6ce39adc6a613d785fb8978942758bf685c3fea3 authormelissam <mfm6@st-andrews.ac.uk> dateWed 8 Aug 2012, 16:54 (14 years ago) parentc4da836

6 files changed+94−71

compare with master

unifiedsplit

contribs/lib/SQLite3/._sqlexpr.idr contribs/lib/SQLite3/._sqlite3.idr contribs/lib/SQLite3/._testunit.idr contribs/lib/SQLite3/sqlexpr.idr+23−18 contribs/lib/SQLite3/sqlite3.idr+44−42 contribs/lib/SQLite3/testunit.idr+27−11

contribs/lib/SQLite3/._sqlexpr.idr

Binary file not shown.

contribs/lib/SQLite3/._sqlite3.idr

Binary file not shown.

contribs/lib/SQLite3/._testunit.idr

Binary file not shown.

contribs/lib/SQLite3/sqlexpr.idr+23−18

@@ -55,7 +55,7 @@ data Constr = NOTNULL

5555

5656

5757data SQL = SELECT SelVar SQL Clause

58− | TBL String

58+ | TBL (List String)

5959 | INSERT SQL (List Value)

6060 | INSERTC SQL (List Value) (List Value)

6161 | UPDATE SQL condClause

@@ -142,6 +142,7 @@ listValType xs ((val, types, constr) :: vs) = let (str , newxs) = valString xs v

142142 let (finalstr, finalxs) = listValType newxs'' vs in

143143 ((unwords(intersperse " " (words(str) ++ words(str') ++ words(str'') ++ words(finalstr)))) , finalxs)

144144

145+

145146-----------------------------------------------------------

146147-- | Evaluates a condition after WHERE clause

147148-----------------------------------------------------------

@@ -204,37 +205,41 @@ condClauseStr xs (WHERE setcl1 setcl2) = let (condstr, newxs) = condClauseStr xs

204205 let (condstr', newxs') = clauseString newxs setcl2 in

205206 ( condstr ++ " WHERE " ++ condstr', newxs')

206207

207−--TODO SELECT data from tbl1 where num > (SELECT num from tbl1 where num = 24)

208−-- evalSQL [] ((SELECT ALL) (TBL "tbl") (MkSQL ((SELECT ALL) (TBL "tbl") (MkCond (VCol ") ) ) )

208+-- SELECT data from tbl1 where num > (SELECT num from tbl1 where num = 24)

209+-- evalSQL [] ((SELECT ALL) (TBL "tbl") (MkSQL ((SELECT ALL) (TBL "tbl") (MkCond (VCol ") ) ) )

210+-- NTBF

209211--clauseString xs (MkSQL sql) = (evalSQL xs sql)

210−

211212

212−evalSQL xs (TBL tbl) = (tbl, xs)

213+-- Separate list of tables

214+evalSQL xs (TBL tbl) = ((unwords (intersperse "," ( tbl))), xs)

213215evalSQL xs (SELECT vars sql' c) = let (sqlstring, newxs) = evalSQL xs sql' in

214216 let (csstring, newxs') = clauseString newxs c in

215217 case c of

216218 Empty => case vars of

217219 (ALL ) => if complexType sql' then ("SELECT " ++ "*" ++ " FROM "

218220 ++ (putBrackets sqlstring) ++ csstring, newxs')

219− else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring ++ csstring, newxs')

221+

222+ else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring

223+ ++ csstring, newxs')

220224

221− (Cols selvar) => if complexType sql' then ("SELECT " ++ unwords ( intersperse "" ( selvar ++

222− (words ( " FROM " ++ (putBrackets sqlstring) )))) ++ csstring, newxs')

223− else ("SELECT " ++ unwords ( intersperse "" ( selvar ++

224− (words ( "FROM " ++ sqlstring )))) ++ csstring, newxs')

225+ (Cols selvar) => if complexType sql' then ("SELECT " ++ (unwords selvar) ++

226+ " FROM " ++ (putBrackets sqlstring) ++ csstring, newxs')

227+

228+ else ("SELECT " ++ (unwords selvar )++ " FROM " ++ sqlstring

229+ ++ csstring, newxs')

225230

226231 _ => case vars of

227232 (ALL ) => if complexType sql' then ("SELECT " ++ "*" ++ " FROM "

228− ++ (putBrackets sqlstring) ++ " WHERE " ++ csstring , newxs')

229− else ("SELECT " ++ "*" ++ " FROM "

230− ++ sqlstring ++ " WHERE " ++ csstring , newxs')

233+ ++ " WHERE " ++ csstring , newxs')

234+ else ("SELECT " ++ "*" ++ " FROM " ++ sqlstring

235+ ++ " WHERE " ++ csstring , newxs')

231236

232− (Cols selvar) => if complexType sql' then ("SELECT " ++ unwords ( intersperse "" ( selvar ++

233− (words ( " FROM " ++ (putBrackets sqlstring) ))))

234− ++ " WHERE " ++ csstring , newxs')

237+ (Cols selvar) => if complexType sql' then ("SELECT " ++ (unwords selvar) ++ " FROM " ++

238+ (putBrackets sqlstring) ++ " WHERE "

239+ ++ csstring , newxs')

235240

236− else ("SELECT " ++ unwords ( intersperse "" ( selvar ++

237− (words ( "FROM " ++ sqlstring )))) ++ " WHERE " ++ csstring , newxs')

241+ else ("SELECT " ++ (unwords selvar) ++ " FROM " ++ sqlstring

242+ ++ " WHERE " ++ csstring , newxs')

238243

239244

240245evalSQL xs (INSERT sql vals) = let (tblname, newvals) = evalSQL xs sql in

contribs/lib/SQLite3/sqlite3.idr+44−42

@@ -29,7 +29,7 @@ data DBPointer = MkDBPointer Ptr

2929data TBPointer = MkTBPointer Ptr

3030

3131data StmtPtr = MkStmtPtr Ptr

32−

32+

3333Table : Set

3434Table = List (List DBVal)

3535

@@ -38,31 +38,31 @@ forM : Monad m => List a -> (a -> m b) -> m (List b)

3838forM f xs = mapM xs f

3939

4040

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

42−

43−instance Monad DB where

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

45− case c of

46− Left err => return (Left err)

47− Right v => case k v of

48− MkDB k' => k')

49− return x = MkDB (return (Right x))

50−

51−fail : String -> DB a

52−fail err = MkDB (return (Left err))

53−

54−liftIO : IO a -> DB a

55−liftIO f = MkDB (do f' <- f

56− return (Right f'))

57−

58−ioError : String -> IO a

59−ioError err = do putStrLn err

60− return (believe_me ())

61−

62−runDB : DB a -> IO a

63−runDB (MkDB f) = do f' <- f

64− case f' of

65− Right v => return v

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

42+

43+instance Monad DB where

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

45+ case c of

46+ Left err => return (Left err)

47+ Right v => case k v of

48+ MkDB k' => k')

49+ return x = MkDB (return (Right x))

50+

51+fail : String -> DB a

52+fail err = MkDB (return (Left err))

53+

54+liftIO : IO a -> DB a

55+liftIO f = MkDB (do f' <- f

56+ return (Right f'))

57+

58+ioError : String -> IO a

59+ioError err = do putStrLn err

60+ return (believe_me ())

61+

62+runDB : DB a -> IO a

63+runDB (MkDB f) = do f' <- f

64+ case f' of

65+ Right v => return v

6666 Left str => ioError str

6767

6868-----------------------------------------------------------------------------

@@ -298,19 +298,19 @@ get_data (MkDBPointer pointer) row col = do

298298-- | This function makes use of get_data to get all the result.

299299-----------------------------------------------------------------------------

300300

301−toList : DBPointer -> DB Table

302−toList db = do

301+toList_v1 : DBPointer -> DB Table

302+toList_v1 db = do

303303 nbR <- liftIO (num_row_v2 db)

304304 nmC <- liftIO (num_col_v2 db)

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

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

307− liftIO(get_data db i j)

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

307+ liftIO(get_data db i j)

308308

309309 )

310310 )

311311 return res

312−

313−

312+

313+

314314strcat : String -> String-> String

315315strcat str1 str2 = (str1 ++ str2)

316316

@@ -320,17 +320,17 @@ strcat str1 str2 = (str1 ++ str2)

320320

321321--toList_v2 : String -> String -> DBPointer -> DB Table

322322--toList_v2 name stmt x = do

323−-- ptr <- (get_table x (stmt))

324−-- nbR <- liftIO (num_row ptr)

325−-- nmC <- liftIO (num_col ptr)

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

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

328−-- liftIO(get_data x name i j)

323+-- ptr <- (get_table x (stmt))

324+-- nbR <- liftIO (num_row ptr)

325+-- nmC <- liftIO (num_col ptr)

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

327+-- forM [0..(nmC-1)] (\ j =>

328+-- liftIO(get_data x name i j)

329329--

330−-- )

331−-- )

332−-- liftIO (free_table ptr)

333−-- return res

330+-- )

331+-- )

332+-- liftIO (free_table ptr)

333+-- return res

334334

335335

336336-----------------------------------------------------------------------------

@@ -400,4 +400,6 @@ bindMulti pointer ((Just (indexs, val))::vs) = case val of

400400

401401

402402 (VFloat floatval) => do x <- bind_float pointer indexs floatval

403+

403404 bindMulti(x) vs

405+

contribs/lib/SQLite3/testunit.idr+27−11

@@ -4,14 +4,14 @@ import sqlite3

55testexpr : DB()

66testexpr = do db <- open_db "somedb.db"

7− let sql = (evalSQL [] ((SELECT ALL)(TBL "tbl1") (OR (AND (MkCond (Equals (VCol "data")(VStr "data0"))) (MkCond (Equals (VCol "num")(VInt 1))) ) (MkCond (Equals (VCol "num")(VInt 2))))))

7+ let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (OR (AND (MkCond (Equals (VCol "data")(VStr "data0"))) (MkCond (Equals (VCol "num")(VInt 1))) ) (MkCond (Equals (VCol "num")(VInt 2))))))

88 let x = (fst sql)

99 let list = (snd sql)

1010 liftIO(print x)

1111 stmt <- (prepare_db db x)

1212 bindMulti stmt list

1313 exec_db_v2 stmt

14− res <- toList db

14+ res <- toList_v1 db

1515 liftIO(print res)

1616 finalize_db stmt

1717 close_db db

@@ -19,7 +19,7 @@ testexpr = do db <- open_db "somedb.db"

1919

2020testupdate : DB()

2121testupdate = do db <- open_db "somedb.db"

22− let sql = (evalSQL [] (UPDATE (TBL "tbl1") (WHERE (SET (MkCond (Equals(VCol "data") (VStr "data0"))) ) (MkCond (Equals (VCol "num") (VInt 2))) ) ))

22+ let sql = (evalSQL [] (UPDATE (TBL ["tbl1"]) (WHERE (SET (MkCond (Equals(VCol "data") (VStr "data0"))) ) (MkCond (Equals (VCol "num") (VInt 2))) ) ))

2323 let x = (fst sql)

2424 let list = (snd sql)

2525 liftIO(print x)

@@ -32,7 +32,7 @@ testupdate = do db <- open_db "somedb.db"

3232

3333testInsert : DB()

3434testInsert = do db <- open_db "somedb.db"

35− let sql = (evalSQL [] (INSERT (TBL "tbl1") [(VInt 2),(VStr "histring2")]))

35+ let sql = (evalSQL [] (INSERT (TBL ["tbl1"]) [(VInt 2),(VStr "histring2")]))

3636 let x = (fst sql)

3737 let list = (snd sql)

3838 liftIO(print x)

@@ -45,14 +45,14 @@ testInsert = do db <- open_db "somedb.db"

4545

4646testNull : DB()

4747testNull = do db <- open_db "somedb.db"

48− let sql = (evalSQL [] ((SELECT ALL)(TBL "tbl1") (MkCond (MkNULL (VCol "data")))))

48+ let sql = (evalSQL [] ((SELECT ALL)(TBL ["tbl1"]) (MkCond (MkNULL (VCol "data")))))

4949 let x = (fst sql)

5050 let list = (snd sql)

5151 liftIO(print x)

5252 stmt <- (prepare_db db x)

5353 bindMulti stmt list

5454 exec_db_v2 stmt

55− res <- toList db

55+ res <- toList_v1 db

5656 liftIO(print res)

5757 finalize_db stmt

5858 close_db db

@@ -61,7 +61,7 @@ testNull = do db <- open_db "somedb.db"

6161

6262testInsertWithCond : DB()

6363testInsertWithCond = do db <- open_db "somedb.db"

64− let sql = (evalSQL [] (INSERTC (TBL "tbl1") [(VCol "data"),(VCol "num")] [(VInt 201),(VStr "newinserted")]))

64+ let sql = (evalSQL [] (INSERTC (TBL ["tbl1"]) [(VCol "data"),(VCol "num")] [(VInt 201),(VStr "newinserted")]))

6565 let x = (fst sql)

6666 let list = (snd sql)

6767 liftIO(print x)

@@ -75,14 +75,14 @@ testInsertWithCond = do db <- open_db "somedb.db"

7575-- Nested queries need to have the same column as the outer queries !!!

7676testNestedSel1 : DB()

7777testNestedSel1 = do db <- open_db "somedb.db"

78− let sql = (evalSQL [] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL "tbl1") (MkCond (Equals (VCol "num")(VInt 2))) ) Empty ) )

78+ let sql = (evalSQL [] (SELECT (Cols ["data"]) (SELECT (Cols["num","data"]) (TBL ["tbl1"]) (MkCond (Equals (VCol "num")(VInt 2))) ) Empty ) )

7979 let x = (fst sql)

8080 let list = (snd sql)

8181 liftIO(print x)

8282 stmt <- (prepare_db db x)

8383 bindMulti stmt list

8484 exec_db_v2 stmt

85− res <- toList db

85+ res <- toList_v1 db

8686 liftIO(print res)

8787 finalize_db stmt

8888 close_db db

@@ -91,7 +91,7 @@ testNestedSel1 = do db <- open_db "somedb.db"

9191-- Testing Create Table

9292testCreateTable : DB ()

9393testCreateTable = do db <- open_db "somedb.db"

94− let sql = (evalSQL [] (CREATE (TBL "mynewtbl") [ ((VCol "col"),(CInt "int"),(None)) ] ) )

94+ let sql = (evalSQL [] (CREATE (TBL ["mynewtbl"]) [ ((VCol "col"),(CInt "int"),(None)) ] ) )

9595 let x = (fst sql)

9696 let list = (snd sql)

9797 liftIO(print x)

@@ -102,7 +102,23 @@ testCreateTable = do db <- open_db "somedb.db"

102102 close_db db

103103 return ()

104104

105+testMultiTable : DB ()

106+testMultiTable = do db <- open_db "somedb.db"

107+ let sql = (evalSQL [] ((SELECT ALL )(TBL ["mytable","tbl1"]) (Empty) ) )

108+ let x = (fst sql)

109+ let list = (snd sql)

110+ liftIO(print x)

111+ stmt <- (prepare_db db x)

112+ bindMulti stmt list

113+ exec_db_v2 stmt

114+ res <- toList_v1 db

115+ liftIO(print res)

116+ finalize_db stmt

117+ close_db db

118+ return ()

119+

120+

105121main : IO ()

106−main = do --x <- runDB (test3)

122+main = do x <- runDB (testexpr)

107123 y <- runDB (testNestedSel1)

108124 return ()